English
The function List.getI is primitive-recursive in two arguments under the standard encodable/denumerable framework.
Русский
Функция List.getI является примитивно вычислимой по двум аргументам в рамках стандартной кодируемости/денумерабельности.
LaTeX
$$$\\operatorname{Primrec}_2(\\mathrm{List.getI}_\\alpha)$.$$
Lean4
/-- Evaluating `c : Code` in a continuation `k : Cont` and input `v : List ℕ`. This goes by
recursion on `c`, building an augmented continuation and a value to pass to it.
* `zero' v = 0 :: v` evaluates immediately, so we return it to the parent continuation
* `succ v = [v.headI.succ]` evaluates immediately, so we return it to the parent continuation
* `tail v = v.tail` evaluates immediately, so we return it to the parent continuation
* `cons f fs v = (f v).headI :: fs v` requires two sub-evaluations, so we evaluate
`f v` in the continuation `k (_.headI :: fs v)` (called `Cont.cons₁ fs v k`)
* `comp f g v = f (g v)` requires two sub-evaluations, so we evaluate
`g v` in the continuation `k (f _)` (called `Cont.comp f k`)
* `case f g v = v.head.casesOn (f v.tail) (fun n => g (n :: v.tail))` has the information needed
to evaluate the case statement, so we do that and transition to either
`f v` or `g (n :: v.tail)`.
* `fix f v = let v' := f v; if v'.headI = 0 then k v'.tail else fix f v'.tail`
needs to first evaluate `f v`, so we do that and leave the rest for the continuation (called
`Cont.fix f k`)
-/
def stepNormal : Code → Cont → List ℕ → Cfg
| Code.zero' => fun k v => Cfg.ret k (0 :: v)
| Code.succ => fun k v => Cfg.ret k [v.headI.succ]
| Code.tail => fun k v => Cfg.ret k v.tail
| Code.cons f fs => fun k v => stepNormal f (Cont.cons₁ fs v k) v
| Code.comp f g => fun k v => stepNormal g (Cont.comp f k) v
| Code.case f g => fun k v => v.headI.rec (stepNormal f k v.tail) fun y _ => stepNormal g k (y :: v.tail)
| Code.fix f => fun k v => stepNormal f (Cont.fix f k) v
