Theorems · Definition · logic and foundations

Turing.ToPartrec.stepNormal

Turing.ToPartrec.Code → Turing.ToPartrec.Cont → List ℕ → Turing.ToPartrec.Cfg

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)

Defined in

Mathlib.Computability.TuringMachine.Config

Cited by

13 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms