Singleton deterministic counting machines

Embed a native deterministic machine into the shared List-choice core by putting its instruction in a singleton list. A deterministic transition has exactly one occurrence. A halt has one terminal trace, independently of the extra clock allowed after its first halting time.

Main definitions

• Turing.MultiTapeCTM.ofDeterministic: the singleton occurrence lift.

Main results

• Turing.MultiTapeCTM.runList_ofDeterministic: the interpreted run is a singleton native run.
• Turing.MultiTapeCTM.haltsWithin_ofDeterministic_iff: native and counting halting clocks agree.
• Turing.MultiTapeCTM.branchCount_ofDeterministic: a halted run contributes exactly zero or one.

References

The native deterministic machine and tape plumbing are by Christian Reitwiessner and Samuel Schlesinger; see MultiTape.Deterministic and the upstream files it imports. This singleton embedding follows the shared machine core and does not use the two-coin probabilistic lift.

noncomputable def Turing.MultiTapeCTM.ofDeterministic {k : ℕ} {Symbol State : Type} (machine : MultiTapeTM k Symbol State) : MultiTapeCTM k Symbol State

Each deterministic instruction becomes one List occurrence in the common machine core.

theorem Turing.MultiTapeCTM.actions_ofDeterministic {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (state : State) (h : cfg.state = some state) : (ofDeterministic machine).actions cfg = [machine.tr state cfg.inputSymbol cfg.workTapeSymbols]

The live transition list has exactly the original deterministic action.

theorem Turing.MultiTapeCTM.runList_ofDeterministic {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeTM k Symbol State) (fuel : ℕ) (cfg : Cfg k Symbol State input) : (ofDeterministic machine).runList fuel cfg = [MultiTapeTM.runFrom cfg fuel]

Interpreting the singleton lift gives one occurrence of the exact native configuration.

theorem Turing.MultiTapeCTM.nonblocking_ofDeterministic {k : ℕ} {Symbol State : Type} (machine : MultiTapeTM k Symbol State) : (ofDeterministic machine).Nonblocking

Every local view in the singleton lift has exactly one occurrence.

theorem Turing.MultiTapeCTM.haltsWithin_ofDeterministic_iff {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeTM k Symbol State) (fuel : ℕ) (cfg : Cfg k Symbol State input) : (ofDeterministic machine).HaltsWithin fuel cfg ↔ (MultiTapeTM.runFrom cfg fuel).Halted

Halting clocks agree exactly, without inserting a choice or delay after early halting.

theorem Turing.MultiTapeCTM.branchCount_ofDeterministic {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeTM k Symbol State) (verdict : List Symbol → Bool) (fuel : ℕ) (cfg : Cfg k Symbol State input) (h : (MultiTapeTM.runFrom cfg fuel).Halted) : (ofDeterministic machine).branchCount verdict fuel cfg = if verdict (MultiTapeTM.runFrom cfg fuel).output = true then 1 else 0

A halted deterministic computation contributes one branch exactly when its output passes.