English
The evaluation semantics for a continuation is defined by a function eval: Cont × List Nat → List Nat, with behavior given by the constructors Halt, Cons, Comp, and Fix: halt returns the input; cons and comp perform sub-evaluations; fix Uses conditional recursion on the head of the input.
Русский
Определена семантика вычисления продолжения: eval: Cont × List Nat → List Nat; для конструкторов Halt, Cons, Comp, Fix задаются правила: halt возвращает вход, cons и comp выполняют подвычисления, fix использует рекурсию по голове входа.
LaTeX
$$$\\mathrm{eval}: \\mathrm{Cont} \\to \\mathrm{List}(\\mathbb{N}) \\to \\mathrm{List}(\\mathbb{N})$ is defined by\n\\begin{cases} \\mathrm{eval}(\\mathrm{Cont.halt}, v) = \\mathrm{pure}(v), \\\\ \\mathrm{eval}(\\mathrm{Cont.cons}_1(fs, as, k), v) = \\mathrm{Cont.eval}(k)(v.headI :: \\mathrm{Code.eval}(fs)(as)), \\\\ \\mathrm{eval}(\\mathrm{Cont.cons}_2(ns, k), v) = \\mathrm{Cont.eval}(k)(ns.headI :: v), \\\\ \\mathrm{eval}(\\mathrm{Cont.comp}(f,k), v) = \\mathrm{Code.eval}(f)(v) \\;\\text{bind}\\; \\mathrm{Cont.eval}(k), \\\\ \\mathrm{eval}(\\mathrm{Cont.fix}(f,k), v) = \\begin{cases} \\mathrm{Cont.eval}(k)(v.tail) & \\text{if } v.headI = 0, \\\\ (f.fix).eval(v.tail) \\;\\text{bind}\\; \\mathrm{Cont.eval}(k) & \\text{otherwise} \\end{cases} \\end{cases}$$$
Lean4
/-- The semantics of a continuation. -/
def eval : Cont → List ℕ →. List ℕ
| Cont.halt => pure
| Cont.cons₁ fs as k => fun v => do
let ns ← Code.eval fs as
Cont.eval k (v.headI :: ns)
| Cont.cons₂ ns k => fun v => Cont.eval k (ns.headI :: v)
| Cont.comp f k => fun v => Code.eval f v >>= Cont.eval k
| Cont.fix f k => fun v => if v.headI = 0 then k.eval v.tail else f.fix.eval v.tail >>= k.eval
