Pointwise output semantics for deterministic Turing machines

This module exposes total bounded execution and machine-relative relations for programs that produce complete binary strings. These definitions make no universality assumption, so they can be reused both for arbitrary description machines and for later universal-machine invariance theorems.

Main results

• TM.runCfg_reachesIn -- bounded evaluation agrees with relational execution
• TM.HaltsInTime.iff_runCfg -- executable bounded halting
• TM.ProducesInTime.iff_runCfg -- an executable characterization
• TM.ProducesInTime.take_time -- unread program suffixes can be truncated
• TM.ProducesInTime.mono -- increasing the clock preserves production
• Tape.HasOutput.eq -- a tape has at most one exact binary-string output
• TM.computes_iff_forall_produces -- pointwise production uniformizes by length
• TM.produces_iff_exists_producesInTime -- bounded and unbounded agreement

@[simp]

theorem Complexity.TM.runCfg_zero {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) : tm.runCfg c 0 = c

@[simp]

theorem Complexity.TM.runCfg_succ {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) (steps : ℕ) : tm.runCfg c (steps + 1) = (tm.step (tm.runCfg c steps)).getD (tm.runCfg c steps)

theorem Complexity.TM.runCfg_add {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) (first second : ℕ) : tm.runCfg c (first + second) = tm.runCfg (tm.runCfg c first) second

Bounded execution composes by addition of clocks.

theorem Complexity.TM.runCfg_of_halted {n : ℕ} (tm : TM n) {c : Cfg n tm.Q} (hhalt : tm.halted c) (steps : ℕ) : tm.runCfg c steps = c

Once a configuration is halted, bounded execution stands still.

theorem Complexity.TM.runCfg_of_reachesIn {n : ℕ} (tm : TM n) {c c' : Cfg n tm.Q} {steps : ℕ} (hreach : tm.reachesIn steps c c') : tm.runCfg c steps = c'

An exact relational run agrees with bounded execution at the same clock.

theorem Complexity.TM.runCfg_reachesIn {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) (time : ℕ) : ∃ steps ≤ time, tm.reachesIn steps c (tm.runCfg c time)

The bounded evaluator's endpoint is reachable within its clock.

theorem Complexity.TM.runCfg_eq_of_reachesIn_halted {n : ℕ} (tm : TM n) {c c' : Cfg n tm.Q} {steps time : ℕ} (hreach : tm.reachesIn steps c c') (hhalt : tm.halted c') (hsteps : steps ≤ time) : tm.runCfg c time = c'

A halted exact-step endpoint remains the endpoint at every larger clock.

theorem Complexity.TM.HaltsInTime.iff_runCfg {n : ℕ} (tm : TM n) (program : List Bool) (time : ℕ) : tm.HaltsInTime program time ↔ tm.halted (tm.runCfg (tm.initCfg program) time)

Bounded halting is exactly the decidable property that the bounded evaluator has reached the halt state.

@[instance_reducible]

instance Complexity.TM.instDecidableHaltsInTime {n : ℕ} (tm : TM n) (program : List Bool) (time : ℕ) : Decidable (tm.HaltsInTime program time)

Bounded halting is decidable by executing the advertised clock.

Equations

• tm.instDecidableHaltsInTime program time = decidable_of_iff (tm.halted (tm.runCfg (tm.initCfg program) time)) ⋯

theorem Complexity.TM.HaltsInTime.mono {n : ℕ} {tm : TM n} {program : List Bool} {first second : ℕ} (hbound : first ≤ second) (hhalt : tm.HaltsInTime program first) : tm.HaltsInTime program second

Increasing the clock preserves bounded halting.

theorem Complexity.TM.halts_of_haltsInTime {n : ℕ} {tm : TM n} {program : List Bool} {time : ℕ} (hhalt : tm.HaltsInTime program time) : tm.Halts program

Forgetting a clock turns bounded halting into eventual halting.

theorem Complexity.TM.halts_iff_exists_haltsInTime {n : ℕ} (tm : TM n) (program : List Bool) : tm.Halts program ↔ ∃ (time : ℕ), tm.HaltsInTime program time

Eventual halting is equivalent to halting under some finite clock.

theorem Complexity.TM.ProducesInTime.iff_runCfg {n : ℕ} (tm : TM n) (program output : List Bool) (time : ℕ) : tm.ProducesInTime program output time ↔ tm.halted (tm.runCfg (tm.initCfg program) time) ∧ (tm.runCfg (tm.initCfg program) time).output.HasOutput output

Pointwise bounded production is exactly the decidable property of the bounded evaluator being halted with the requested output.

theorem Complexity.TM.runCfg_initCfg_congr_of_input_cells {n : ℕ} (tm : TM n) (first second : List Bool) (time : ℕ) (hinput : ∀ position ≤ time, (tm.initCfg first).input.cells position = (tm.initCfg second).input.cells position) : (tm.runCfg (tm.initCfg first) time).state = (tm.runCfg (tm.initCfg second) time).state ∧ (tm.runCfg (tm.initCfg first) time).work = (tm.runCfg (tm.initCfg second) time).work ∧ (tm.runCfg (tm.initCfg first) time).output = (tm.runCfg (tm.initCfg second) time).output

Bounded runs on two inputs stay synchronized in state, work, and output when the initialized input tapes agree on every cell reachable by the clock.

theorem Complexity.TM.initCfg_take_input_cells_le {n : ℕ} (tm : TM n) (program : List Bool) (time position : ℕ) (hposition : position ≤ time) : (tm.initCfg program).input.cells position = (tm.initCfg (List.take time program)).input.cells position

Truncating an input to the clock preserves every initialized input cell that can be reached within that clock.

@[instance_reducible]

instance Complexity.TM.instDecidableProducesInTime {n : ℕ} (tm : TM n) (program output : List Bool) (time : ℕ) : Decidable (tm.ProducesInTime program output time)

Pointwise bounded production is decidable by running the machine for its clock and checking the resulting finite output claim.

Equations

• tm.instDecidableProducesInTime program output time = decidable_of_iff (tm.halted (tm.runCfg (tm.initCfg program) time) ∧ (tm.runCfg (tm.initCfg program) time).output.HasOutput output) ⋯

theorem Complexity.TM.ProducesInTime.take_time {n : ℕ} {tm : TM n} {program output : List Bool} {time : ℕ} (hproduce : tm.ProducesInTime program output time) : tm.ProducesInTime (List.take time program) output time

No bounded computation can inspect more than the first time program bits: truncating there preserves exact production within the same clock.

theorem Complexity.TM.ProducesInTime.mono {n : ℕ} {tm : TM n} {program output : List Bool} {first second : ℕ} (hbound : first ≤ second) (hproduce : tm.ProducesInTime program output first) : tm.ProducesInTime program output second

Increasing the clock preserves pointwise production.

theorem Complexity.TM.produces_of_producesInTime {n : ℕ} {tm : TM n} {program output : List Bool} {time : ℕ} (hproduce : tm.ProducesInTime program output time) : tm.Produces program output

Forgetting a clock turns bounded production into eventual production.

theorem Complexity.TM.ProducesInTime.haltsInTime {n : ℕ} {tm : TM n} {program output : List Bool} {time : ℕ} (hproduce : tm.ProducesInTime program output time) : tm.HaltsInTime program time

Producing an output within a clock entails halting within that clock.

theorem Complexity.TM.Produces.halts {n : ℕ} {tm : TM n} {program output : List Bool} (hproduce : tm.Produces program output) : tm.Halts program

Producing an output entails eventual halting.

theorem Complexity.TM.produces_iff_exists_producesInTime {n : ℕ} (tm : TM n) (program output : List Bool) : tm.Produces program output ↔ ∃ (time : ℕ), tm.ProducesInTime program output time

Eventual production is equivalent to production under some finite clock.

theorem Complexity.TM.Tape.HasOutput.length_eq {tape : Tape} {left right : List Bool} (hleft : tape.HasOutput left) (hright : tape.HasOutput right) : left.length = right.length

Two exact output claims about the same tape have equal lengths.

theorem Complexity.TM.Tape.HasOutput.eq {tape : Tape} {left right : List Bool} (hleft : tape.HasOutput left) (hright : tape.HasOutput right) : left = right

A tape has at most one exact binary-string output.

theorem Complexity.TM.ProducesInTime.output_unique {n : ℕ} {tm : TM n} {program left right : List Bool} {leftTime rightTime : ℕ} (hleft : tm.ProducesInTime program left leftTime) (hright : tm.ProducesInTime program right rightTime) : left = right

A deterministic program cannot produce two different outputs, even when the two production claims use different clocks.

theorem Complexity.TM.Produces.output_unique {n : ℕ} {tm : TM n} {program left right : List Bool} (hleft : tm.Produces program left) (hright : tm.Produces program right) : left = right

Eventual production by a deterministic program has a unique output.

theorem Complexity.TM.computesInTime_iff_forall_producesInTime {n : ℕ} (tm : TM n) (function : List Bool → List Bool) (time : ℕ → ℕ) : tm.ComputesInTime function time ↔ ∀ (input : List Bool), tm.ProducesInTime input (function input) (time input.length)

Whole-function bounded computation is exactly pointwise bounded production under the same length-indexed clock.

theorem Complexity.TM.ComputesInTime.producesInTime {n : ℕ} {tm : TM n} {function : List Bool → List Bool} {time : ℕ → ℕ} (hcompute : tm.ComputesInTime function time) (input : List Bool) : tm.ProducesInTime input (function input) (time input.length)

A bounded whole-function computation produces the requested output on a particular input.

theorem Complexity.TM.computes_iff_forall_produces {n : ℕ} (tm : TM n) (function : List Bool → List Bool) : tm.Computes function ↔ ∀ (input : List Bool), tm.Produces input (function input)

Eventual whole-function computation is equivalent to eventual pointwise production. The reverse implication uniformizes halting times over the finite set of Boolean strings at each input length.

theorem Complexity.TM.Computes.produces {n : ℕ} {tm : TM n} {function : List Bool → List Bool} (hcompute : tm.Computes function) (input : List Bool) : tm.Produces input (function input)

A whole-function computation produces the requested output on a particular input.