MATH.5:4.2 - Extend the assignment recursively

Assign a target value a(x) to every generator x. Define the evaluation E on finite expressions:

• a generator x receives a(x);
• a constant receives its named target value;
• op(t1,...,tn) receives op_target(E(t1),...,E(tn)).

Each recursive call uses a constituent expression. MATH.4 supplies the finite-construction argument and the treatment of a result that needs additional information.

For a word [x1,...,xk], the same move evaluates the assigned generator values in order. The empty word receives e; extending a word by x changes its value from v to v star a(x). Associativity and the identity laws make this evaluation preserve concatenation:

E(p;q)=E(p) star E(q).

For a typed path, set E(id_X)=id_F(X). If p:X -> Y has been evaluated and a:Y -> Z is the next generator, set E(p;a)=E(p) star a_target, where star is again read in execution order. The intermediate object F(Y) makes this composition defined. Recursing by path length evaluates every finite path while keeping its endpoints. In a target of sets and functions, this means applying E(p) first and a_target second.

The image of a composite is now computed from its parts. It is no longer an independently chosen entry in a correspondence table.