CMP.12:5.1 - Derive an arithmetic interpreter and stack translation

Expressions are integer literals, names and binary addition, subtraction or multiplication. An environment ρ supplies every free name. Both source and target use unbounded integers. The source evaluator returns a literal, looks up a name, or evaluates the left operand and then the right operand before applying the operator.

The target stack is written from bottom to top. PUSH n appends n; LOAD x appends ρ(x). For ADD, SUB or MUL, pop the right operand b and then the left operand a, and append respectively a+b, a-b or a*b.

Construct the compiler C:

• C(n) = PUSH n.
• C(x) = LOAD x.
• C(a op b) = C(a); C(b); OP, where OP is the matching target operation.

The useful induction claim is: for every admitted ρ and every initial stack S, running C(e) leaves S · [eval(e,ρ)], with earlier entries unchanged. Literals and names append the required value. For a binary expression, the induction hypothesis for a gives S · [eval(a,ρ)]; applying the hypothesis for b to that whole stack appends eval(b,ρ). OP replaces just those two entries by their required combination. This proves the claim and supplies the composition condition.

With ρ(x)=5, compile (x+1)*(x-2) to:

LOAD x; PUSH 1; ADD; LOAD x; PUSH 2; SUB; MUL

Starting above an earlier stack value 99 gives successive added values 5, 1, then 6; next 5, 2, then 3; multiplication leaves [99,18]. Each syntax-tree node produces one instruction. Integer operation costs and peak live stack values still depend on the values and expression structure.

Changed arithmetic: suppose the target uses unsigned eight-bit wraparound. For x+1 at x=255 it returns 0, while the source returns 256. Preserve the source by using a wider or multiword representation, restrict the admitted inputs by a valid range argument, or deliberately change the source meaning to modular arithmetic. A successful parse and a preserved instruction order do not fix the arithmetic mismatch.