Reduction you can drive by hand

B-Lambda evaluates every program three times, by three independent methods, and then checks that they agree. This chapter is about the four views that let you watch that happen — and about the one number that legitimately differs between them.

The Semantics dock

Open the bottom panel with Ctrl + J and choose Semantics. Four tabs — and the dock's own tab relabels itself to whichever you are on, so it reads Semantics · Lockstep rather than a bare Semantics:

Call-by-Structure

Call-by-Structure (CbS) is B-Lambda's default evaluation strategy, as it is in MnL. It is the executable form of the λ_Vis calculus, and the single idea behind it is this: a value does not have to arrive stripped of the expression that produced it.

CbS is strict in its argument. It evaluates the argument first, exactly as Call-by-Value does, and exactly once. What differs is what gets bound. CbV binds the bare value. CbS binds a structured value — the computed value paired with the structure it came from, written Vp ⊗ Vv:

(λx. x + x) (3 * 7)

CbS:  evaluate the argument once  →  21, retaining (3 * 7)
      substitute the PAIR         →  (21 ⊗ 3 * 7) + (21 ⊗ 3 * 7)  →  42
      the multiplication happens ONCE; both sites SHOW 3 * 7

CbV:  evaluate the argument once  →  21
      substitute the bare value   →  21 + 21  →  42
      the multiplication happens ONCE; the 3 * 7 is gone

Both reach 42, and both do the same amount of arithmetic. The difference is not work, it is carriage. Under CbS the argument's original structure is still legible at every place the parameter was used, so you can read off where a number came from without re-deriving it. That is what the Copy vs Lookup (CbS ⇄ CbV) example is built to show.

An argument that is already a value — a number, a boolean, or a λ — has nothing to retain, so it binds bare with no ⊗ at all. The pair only appears when the argument actually had to be reduced.

The trace itself renders as a live Blockly workspace, not as text, with the substituted regions labelled — Substituted block for parameter, Function body of CbS — so you can tell which part of the new term came from where. Where a value carries structure, the step's block comment adds a pair: line reading 21 ⊗ (3 * 7) alongside the usual term: and value: lines.

The rules CbS fires

The reduction rules carry their λ_Vis names, and the step label under the trace names the one that just fired:

Frames are a CbS-only construct: a term of the form (Vv ▷ E) is an expression evaluating underneath a retained visual, and E-Frame is what collapses it once the inside is done. Nothing downstream of the semantics sees them — the compiler pipeline erases frames entirely.

Call-by-Value

Call-by-Value reduces the argument to a value first, then substitutes that value. It is the strategy most real functional languages use, and it is available here for exactly one reason: so you can put it next to CbS and see what the choice keeps and what it throws away.

Since CbS is also strict, the two strategies agree on when the argument is evaluated and on how many times. Put the two tabs side by side on Copy vs Lookup and the traces have the same shape; what differs is that CbV's substituted occurrences are bare numbers where CbS's still carry the expression that produced them.

Everything else about the tab is identical — same block rendering, same controls, same right-click entry point.

No reduction under a binder

Under both strategies, B-Lambda does not reduce inside the body of an abstraction. A λ is a value. Its body is only reduced once an application has substituted something for the parameter.

λx. (2 + 3)     -- stays as it is. Already a value.
(λx. (2 + 3)) 7 -- now the body reduces: → 5

The Normal Form example loads a term that is already in normal form, so you can confirm that the stepper genuinely refuses to go further rather than merely happening not to. This matches MnL's behaviour, and it is why the two languages' reduction traces can be compared at all.

The CSEK machine

The second, independent evaluator. Control, Structure, Environment, Kontinuation.

Three columns, in machine order:

• Control — what the machine will evaluate next.
• Environment — the current bindings, innermost first, with shadowed names dimmed. A binding that carries structure prints as its value, then ⊗, then the block it retained — 21 ⊗ 3 * 7. A letrec binding prints with an hourglass, ⛸, because it is the one thing the machine still stores unevaluated.
• Kontinuation — the pending work, innermost first. Empty reads (empty — top level).

Because CbS is strict, the frames spell out what is being deferred and why:

Controls are Load, Back, Step and Play. If you edit the program while a machine is loaded, the panel says Program changed — load it again to restart rather than silently stepping a stale term. When it finishes it reports Value after n step(s); when it cannot, it says ⨤ stuck after n step(s) and why.

The environment's structured entry is the machine's counterpart of the substitution trace's retained structure: where the rewriter shows 3 * 7 beside the 21, the machine binds the two together in one entry. Neither recomputes anything, which is why the machine fires the same salient rules in the same order as the substitution trace — the invariant the Lockstep view checks. Note that the CSEK tab has no per-tab strategy switch — it runs the language default, CbS.

Lockstep

The tab that ties everything together. Lockstep runs three evaluators on the same program and pairs them up:

• Left — the substitution state, as a block tree.
• Middle — the CSEK machine state that has “caught up” to it.
• Right — the register VM, with its frames and registers.

The status line counts matched salient rules and flags divergence. In sync means the substitution semantics, the abstract machine and the compiled bytecode all agree on this program, at this step, under this strategy — the operational-correspondence claim, executed rather than asserted. If it breaks, the badge names both sides: ⚠ diverged — CSEK reason · VM reason.

Unlike the CSEK tab, Lockstep keeps a CbS / CbV switch, defaulting to CbS, so you can check the correspondence under either strategy. If a trace cannot be built at all the panel says so — Could not build the lockstep trace — rather than looking like a program with no reductions.

Why step counts differ

Watch Fig. 2 for a moment and the two counters drift apart — the machine's is always well ahead of the substitution trace's. Neither is wrong. They are counting different things.

So one reduction frame corresponds to several machine micro-steps, and the machine's number is always the larger. E-Frame is a clear case: merging a visual frame is real work for the machine but is not a redex anyone would point at, so it advances the machine's counter and not the trace's. Lockstep advances the machine in bulk between salient rules — the bookkeeping transitions still increment the machine's count but do not add a reduction frame. Both reach the same normal form, and the salient-event count confirms they agree on the trace that matters.

You can also reach the traces without the dock: More → Call-by-Structure Trace, Call-by-Value Trace and Lockstep Debugger, or the matching Run: commands in the palette. The CSEK machine is the one view with no More entry — reach it from the workspace's Run button, the Semantics tab strip, or Run: CSEK Machine in the palette.