ch:computational-type-theory: ch:computational-type-theory

Problem and result. Implement the finite lazy evaluator and PER decisions required by the seminar. Preserve two invariants: membership and equality inspect evaluated canonical integers rather than source syntax, and fuel exhaustion or divergence returns Unknown, never a negative PER verdict. The accepted run contains seven outcome records followed by the corpus summary.

Representation. The artifact uses a closed term datatype with integer literals, addition, three lambda bodies, application, lazy pairs, both spreads, a stuck term, and a divergent term. Values distinguish integers, lambdas, and pairs whose components remain unevaluated terms. Evaluation returns Known Value, StuckEval, or Unknown. A nominal syntax with capture-avoiding substitution would model arbitrary bodies; the closed body enumeration keeps this acceptance slice executable while still testing the opening beta step and discarded arguments. A separate Per tag selects integers, derived naturals, a successor specification at a represented input, or parity; uniform member and equal dispatch through those tags.

First complete version. Begin with literals and addition. Under positive fuel, a literal is a known integer and addition forces both operands; zero fuel is unknown. Define integer equality by evaluating both sides and comparing the resulting integers. Define natural membership by the same evaluation followed by the nonnegativity test. These clauses establish the arithmetic and PER infrastructure; the opening records are not available until application is added.

Remaining cases. Add lambdas and application. Identity forces its argument, addition-by-one evaluates an addition term, and a constant body discards its argument. Add pairs as canonical values without forcing their components. At this stage the opening evaluation, integer equality, negative natural rejection, and opening natural membership produce the first four named decisions. Add a spread that forces only the selected component. The hidden lazy-pair guard selects a terminating left component while its right component diverges. Finally add the successor specification and parity decisions. Parity evaluates both terms and tests whether their difference is divisible by two; this handles negative integer representatives correctly.

A failing version. Mutate the Diverge clause to return Known (VInt 0). The program still typechecks, but the hidden unknown-result guard changes the first line to eval-opening=FAIL. Exact-output testing rejects the mutation. Restore the recursive divergent clause before acceptance.

Acceptance test. Run the four commands recorded in appendix E. Require a silent check, one passing inline test, an empty audit, and exactly this run transcript:

eval-opening=3
int-eq-opening-3=true
nat-member-minus1=false
nat-member-opening=true
inc-spec-2=true
parity-eq-2-4=true
parity-eq-2-3=false
All 7 Chapter 91 corpus cases passed.

Mathematical boundary. The run is an exact finite specialization of the project and detects the divergence mutation. It illustrates the finite cases of theorem 91.18, theorem 91.30, theorem 91.38; it does not prove them. It also does not formalize NuprlInCoq, prove pointwise functionality, construct a universe, or establish general quotient soundness.