ch:inference-rules: ch:inference-rules

Problem and result. Implement the complete grammar and call-by-value one-step relation of definition 1.50, definition 1.62. Every successful step must be alpha-equivalent to the target selected by the corresponding rule, and beta substitution must preserve every free name of the inserted argument. The fueled driver must distinguish a value, a closed stuck term, an open nonvalue with no step, and fuel exhaustion. The required run evaluates the chapter term $t$ to $\mathsf{tt}$ in three steps, classifies $\mathsf{tt}\mathsf{ff}$ as stuck without a step, and reports fuel exhaustion after ten self-reproducing steps of $\omega \omega$. Four further checks cover capture avoidance, all eleven reduction-rule families, the classifiers, and the faulty-substitution witness.

Starting scaffold. Copy artifacts/ch01-ulc-evaluator/starter.kp.template to a file named starter.kp. The template supplies the term and result datatypes, helper functions, printer, and seven named tests. Its four numbered TODO regions have compiling but incorrect bodies for freeNames, capture-avoiding substitution, step, and the fueled driver. Thus kappa check starter.kp succeeds before any implementation work, while kappa run starter.kp prints failed checks until the four bodies are completed. The four-to-six-hour estimate begins with this copied file and an installed Kappa executable; installing the tool is outside the estimate.

Representation. Use a named syntax tree with one constructor for every clause of definition 1.50; natural numbers serve as names. Separate result datatypes record the three final classes and either a finished result or fuel exhaustion with a step count. Named syntax keeps the printed binders and the capture obligation visible. A plausible alternative is a de Bruijn index, a natural number that counts how many enclosing binders separate an occurrence from its binder: the inner occurrence of the outer binder in $\lambda x.\lambda y.x$ has index one. De Bruijn syntax makes alpha-equivalent terms identical, but inserting a term under a binder must increase its free indices. The named representation is selected because the project is meant to execute the chapter’s fresh-name argument directly.

First complete version. Define the term datatype. Restrict the first driver’s inputs to variables, abstractions, zero, successor, and addition. The second stage adds application and conditionals. Implement isNumeral, isValue, and the free-name calculation. Removing a lambda’s binder from the body’s free-name list makes closedness decidable. Implement the successor and four addition step rules, an option-valued one-step function, and the fueled driver. When the stepper returns no successor, the driver uses the classifiers to report a value, a closed stuck term, or an open nonvalue. The arithmetic vertical slice reduces $\mathsf{add}(\mathsf{suc}(\mathsf{0});\mathsf{suc}(\mathsf{0}))$ to $\mathsf{suc}(\mathsf{suc}(\mathsf{0}))$ in two steps. It also classifies $\mathsf{suc}(\lambda x.x)$ as closed and stuck and an unbound variable as an open nonvalue with no step. Function application is absent from the slice because beta contraction first requires capture-avoiding freshening. The freshening requirement determines the remaining cases. Keep duplicates in the finite name list: every client asks only membership or emptiness, so deduplication would add work without changing a result.

Remaining cases. Define a fresh-name floor above every name in the substitution target, replacement, and body. Traverse the body with a finite environment mapping each encountered binder to its output name. At a variable, consult this environment before comparing the variable with the substitution target; this order distinguishes a bound occurrence from a free occurrence spelled with the same number. At a different binder whose name occurs free in the replacement, choose a name above the floor and continue with the extended environment.

Extend the stepper in rule order. An application steps its function, then its argument once the function is a value, then contracts beta when both premises hold. A conditional steps only its guard before branch selection. The successor and addition clauses remain unchanged. Only when no step exists does the driver call the final classifier; otherwise it consumes one fuel unit and recurs. Calling the classifier only after a failed step prevents a diverging term from being classified as stuck. The implementation constructor OpenNeutral denotes exactly the open-nonvalue class; it does not presuppose a separate syntactic grammar of neutral forms.

A failing version. The artifact includes substituteNaive, which descends under every differently named binder without checking whether the binder occurs free in the replacement. Apply beta reduction to $(\lambda 0.\lambda 1.0)(\lambda 2.1)$. The accepted substitution returns $\lambda r.\lambda 2.1$ for a fresh $r$, leaving the inserted occurrence of name $1$ free. The faulty version returns $\lambda 1.\lambda 2.1$, in which that occurrence is bound. The named mutation test checks both free occurrence and alpha-equivalence, so this concrete mutant still typechecks but makes the final oracle line fail.

Acceptance test. Run the four commands in appendix E. Require seven PASS lines, the summary All 7 Chapter 1 corpus cases passed., and an empty audit. The rule-family test separately exercises E-App-L, E-App-R, E-Beta, all three conditional rules, E-Suc, and all four addition rules; passing only the three headline terms is insufficient.

Mathematical boundary. The run illustrates proposition 1.60, theorem 1.70 and the freshness mechanism used in their proofs. Finite tests prove neither alpha compatibility nor determinism for every term. Fuel exhaustion is an observable finite result, not a proof of divergence, and the evaluator proves no normalization theorem.