English
The evolution of the evaluation machine is governed by stepNormal and stepRet, describing how a Code is executed with a Continuation, and how results propagate back through the continuation chain.
Русский
Эволюция вычислительной машины задаётся функциями stepNormal и stepRet, описывающими выполнение кода в континуации и расходование результатов обратно по цепочке континуаций.
LaTeX
$$$\\text{stepNormal}:\\; \\text{Code} \\to \\text{Cont} \\to \\text{List Nat} \\to \\text{Cfg}$ и далее последовательности равенств, описывающих случаи для 0, succ, tail, cons, comp, case, fix; и аналогичные правила для stepRet.$$
Lean4
/-- Evaluating a continuation `k : Cont` on input `v : List ℕ`. This is the second part of
evaluation, when we receive results from continuations built by `stepNormal`.
* `Cont.halt v = v`, so we are done and transition to the `Cfg.halt v` state
* `Cont.cons₁ fs as k v = k (v.headI :: fs as)`, so we evaluate `fs as` now with the continuation
`k (v.headI :: _)` (called `cons₂ v k`).
* `Cont.cons₂ ns k v = k (ns.headI :: v)`, where we now have everything we need to evaluate
`ns.headI :: v`, so we return it to `k`.
* `Cont.comp f k v = k (f v)`, so we call `f v` with `k` as the continuation.
* `Cont.fix f k v = k (if v.headI = 0 then k v.tail else fix f v.tail)`, where `v` is a value,
so we evaluate the if statement and either call `k` with `v.tail`, or call `fix f v` with `k` as
the continuation (which immediately calls `f` with `Cont.fix f k` as the continuation).
-/
def stepRet : Cont → List ℕ → Cfg
| Cont.halt, v => Cfg.halt v
| Cont.cons₁ fs as k, v => stepNormal fs (Cont.cons₂ v k) as
| Cont.cons₂ ns k, v => stepRet k (ns.headI :: v)
| Cont.comp f k, v => stepNormal f k v
| Cont.fix f k, v => if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail
