English
Applying a map to P^n equals applying the map to P before taking the n-th power: map g (P^n) = (map g P)^n.
Русский
Применение отображения к P^n эквивалентно применению отображения к P перед возведением в n-ю степень: map g (P^n) = (map g P)^n.
LaTeX
$$$$ \\mathrm{map}\\; g (\\mathrm{P})^n = (\\mathrm{map}\\; g \\; \\mathrm{P})^n, \\quad n \\in \\mathbb{N}. $$$$
Lean4
/-- The semantics of the `Code` primitives, as partial functions `List ℕ →. List ℕ`. By convention
we functions that return a single result return a singleton `[n]`, or in some cases `n :: v` where
`v` will be ignored by a subsequent function.
* `zero'` appends a `0` to the input. That is, `zero' v = 0 :: v`.
* `succ` returns the successor of the head of the input, defaulting to zero if there is no head:
* `succ [] = [1]`
* `succ (n :: v) = [n + 1]`
* `tail` returns the tail of the input
* `tail [] = []`
* `tail (n :: v) = v`
* `cons f fs` calls `f` and `fs` on the input and conses the results:
* `cons f fs v = (f v).head :: fs v`
* `comp f g` calls `f` on the output of `g`:
* `comp f g v = f (g v)`
* `case f g` cases on the head of the input, calling `f` or `g` depending on whether it is zero or
a successor (similar to `Nat.casesOn`).
* `case f g [] = f []`
* `case f g (0 :: v) = f v`
* `case f g (n+1 :: v) = g (n :: v)`
* `fix f` calls `f` repeatedly, using the head of the result of `f` to decide whether to call `f`
again or finish:
* `fix f v = []` if `f v = []`
* `fix f v = w` if `f v = 0 :: w`
* `fix f v = fix f w` if `f v = n+1 :: w` (the exact value of `n` is discarded)
-/
def eval : Code → List ℕ →. List ℕ
| Code.zero' => fun v => pure (0 :: v)
| Code.succ => fun v => pure [v.headI.succ]
| Code.tail => fun v => pure v.tail
| Code.cons f fs => fun v => do
let n ← Code.eval f v
let ns ← Code.eval fs v
pure (n.headI :: ns)
| Code.comp f g => fun v => g.eval v >>= f.eval
| Code.case f g => fun v => v.headI.rec (f.eval v.tail) fun y _ => g.eval (y :: v.tail)
| Code.fix f => PFun.fix fun v => (f.eval v).map fun v => if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail
