Pointwise output semantics for deterministic Turing machines

This definitions layer treats the input string as a program and records the complete binary string produced by a deterministic machine. The definitions are machine-relative: no universality assumption is built into them.

runCfg is a total bounded evaluator on configurations. It performs the requested number of transitions and stands still after reaching the halt state. ProducesInTime nevertheless records the actual number of transitions before halting, so its clock agrees with the exact-step semantics of TM.reachesIn.

Main definitions

• TM.runCfg -- total bounded execution, frozen after halting
• TM.Halts, TM.HaltsInTime -- raw halting semantics for a program
• TM.Produces -- a program eventually halts with an exact string output
• TM.ProducesInTime -- the same relation with an explicit transition budget

def Complexity.TM.runCfg {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) : ℕ → Cfg n tm.Q

The configuration after steps transitions, standing still once halted.

Equations

• tm.runCfg c 0 = c
• tm.runCfg c steps.succ = (tm.step (tm.runCfg c steps)).getD (tm.runCfg c steps)

def Complexity.TM.Halts {n : ℕ} (tm : TM n) (program : List Bool) : Prop

Machine tm, run on program program, eventually reaches its halt state.

Equations

• tm.Halts program = ∃ (c : Complexity.Cfg n tm.Q), tm.reaches (tm.initCfg program) c ∧ tm.halted c

def Complexity.TM.HaltsInTime {n : ℕ} (tm : TM n) (program : List Bool) (time : ℕ) : Prop

Machine tm, run on program program, reaches its halt state within time transitions. The witness steps is the actual number of transitions.

Equations

• tm.HaltsInTime program time = ∃ (c : Complexity.Cfg n tm.Q), ∃ steps ≤ time, tm.reachesIn steps (tm.initCfg program) c ∧ tm.halted c

def Complexity.TM.Produces {n : ℕ} (tm : TM n) (program output : List Bool) : Prop

Machine tm, run on program program, eventually halts with exact output output.

Equations

• tm.Produces program output = ∃ (c : Complexity.Cfg n tm.Q), tm.reaches (tm.initCfg program) c ∧ tm.halted c ∧ c.output.HasOutput output

def Complexity.TM.ProducesInTime {n : ℕ} (tm : TM n) (program output : List Bool) (time : ℕ) : Prop

Machine tm, run on program program, halts within time transitions with exact output output. The witness steps is the actual number of transitions.

Equations

• tm.ProducesInTime program output time = ∃ (c : Complexity.Cfg n tm.Q), ∃ steps ≤ time, tm.reachesIn steps (tm.initCfg program) c ∧ tm.halted c ∧ c.output.HasOutput output