fpf.tools
Library / Computational Thinking DPF
Jump to passage
In this reading
Source · lines 2368–2434

Link to current text

Published source confirmed at last check

Source changed 2026-10-03 10:39:28 UTC · snapshot created 2026-10-03 10:40:04 UTC · last check 2026-10-03 11:25:15 UTC

CMP.12:5 - Archetypal Grounding

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.

CMP.12:5.2 - Preserve a function’s binding when its call site changes

Extend the evaluator with immutable lexical bindings, function values and function application. Evaluate:

let x = 2 in
  let f = (lambda y: x + y) in
    let x = 100 in f(3)

Creating f saves its body, parameter y and the environment in which x is 2. Calling f extends that saved environment with y=3, so the body returns 5. Looking up free x in the caller’s environment would return 103 and implement a different binding rule.

The closure makes a rule available as a value without discarding its needed surroundings. A procedure can return it, receive it as an argument or construct a new closure that composes it with another rule. Each later application follows the saved bindings and the new arguments.

Changed feature: now permit assignment to the original captured x before calling f. If the language specifies capture of that variable’s location, assigning it 7 makes f(3) return 10. Keeping a copied value 2 would instead return 5. Represent the environment as names mapped to locations and obtain current values from the store; a later shadowing declaration must allocate a different binding. Revise the capture and lookup rules without changing the arithmetic rule.

CMP.12:5.3 - Preserve which operation is executed

Let ifzero(test,a,b) evaluate test and then only a when the result is zero, otherwise only b. Let division by zero be a defined execution error. The expression ifzero(x,0,10/x) returns 0 at x=0 and 5 at x=2.

A translation that evaluates all three parts and then selects a value raises the unwanted division error at x=0. Instead generate fresh labels and conditional control:

LOAD x
JZ zero
PUSH 10; LOAD x; DIV
JMP end
zero: PUSH 0
end:

JZ pops the test and jumps when it is zero; otherwise execution continues. JMP transfers control unconditionally. DIV pops right then left and divides left by right, using rational values here. Resolve each fresh label to its instruction position before execution. At x=0 the division instructions are skipped; at x=2 they append 5. Either path preserves earlier stack entries and appends one result.

If the branches instead emit commands, the same construction retains which command occurs. If the source is deliberately changed to evaluate both branches, the preservation claim and translation must change with it. The control rule, rather than a particular programming language’s spelling, determines this choice.

CMP.12:5.4 - Preserve completion through internal steps

The source instruction is return 7; the receiving use requires that return. A target first takes k internal steps and then returns 7, where k is a supplied nonnegative integer. Use a remaining-step counter: each internal step reduces it by one, and at zero the target returns. For every finite k the counter proves that the internal phase finishes, so the target supplies the required result.

Change the target to loop: goto loop, leaving return 7 after this loop. Each internal step goes back to loop, so the return is unreachable. A correspondence that allows arbitrarily many silent steps without a completion argument would hide this failure. Restore a finite internal phase to meet the required return.