Theorems · Definition · logic and foundations

Turing.ToPartrec.Code.Ok

Turing.ToPartrec.Code → Prop

This is a temporary definition, because we will prove in code_is_ok that it always holds. It asserts that c is semantically correct; that is, for any k and v, eval (stepNormal c k v) = eval (Cfg.ret k (Code.eval c v)), as an equality of partial values (so one diverges iff the other does). In particular, we can let k = Cont.halt, and then this asserts that stepNormal c Cont.halt v evaluates to Cfg.halt (Code.eval c v).

Defined in

Mathlib.Computability.TuringMachine.Config

Cited by

3 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms