Exact List interpretation of native counting runs

This module connects List interpretation of the existing shared FreeM program to the native occurrence-labelled terminal-branch counts. Repeated final configurations retain their list multiplicity. Running endpoints are filtered out; an empty running choice list remains stuck. The interpreter is an auxiliary mathematical observation, not an uncharged machine instruction.

Main definitions

• Turing.MultiTapeCTM.runList: List interpretation of the shared clocked run program.

Main results

• Turing.MultiTapeCTM.branchCount_succ: terminal counts sum over transition occurrences.
• Turing.MultiTapeCTM.countP_runList: List interpretation equals the native terminal count.
• Turing.MultiTapeCTM.haltsWithin_of_halted: terminal endpoints imply a native halting bound when stuck local views are excluded.

References

The common program and occurrence handler are developed in MultiTape.Counting.Program. Native labelled branches and their source credit are in MultiTape.Counting.

def Turing.MultiTapeCTM.runList {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (fuel : ℕ) (cfg : Cfg k Symbol State input) : List (Cfg k Symbol State input)

Interpret the existing clocked FreeM program by enumerating each finite response once.

theorem Turing.MultiTapeCTM.interpret_runConfigFrom_eq_map_runList {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Empty input) : Cslib.OracleComp.interpret (fun (n : ℕ) => List.ofFn id) (MultiTapeMachine.runConfigFrom machine chooseOccurrence Empty.elim fuel cfg) = List.map (⇑MultiTapeMachine.Config.emptyOracleEquiv.symm) (machine.runList fuel cfg.tapes)

The closed shared-configuration interpreter is the same List, with empty channels restored.

@[simp]

theorem Turing.MultiTapeCTM.runList_zero {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg : Cfg k Symbol State input) : machine.runList 0 cfg = [cfg]

theorem Turing.MultiTapeCTM.runList_halted {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) {cfg : Cfg k Symbol State input} (h : cfg.Halted) (fuel : ℕ) : machine.runList fuel cfg = [cfg]

Halting returns one occurrence of the configuration, for every remaining clock.

theorem Turing.MultiTapeCTM.runList_succ {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg : Cfg k Symbol State input) (fuel : ℕ) (state : State) (h : cfg.state = some state) : machine.runList (fuel + 1) cfg = List.flatMap (fun (action : Action k Symbol State) => machine.runList fuel (action.apply cfg)) (machine.actions cfg)

A live step enumerates every action occurrence before interpreting its continuation.

theorem Turing.MultiTapeCTM.runList_add {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (first second : ℕ) (cfg : Cfg k Symbol State input) : machine.runList (first + second) cfg = List.flatMap (machine.runList second) (machine.runList first cfg)

Pausing and resuming the shared program preserves every endpoint occurrence.

theorem Turing.MultiTapeCTM.runList_add_of_halted {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (first second : ℕ) (cfg : Cfg k Symbol State input) (h : ∀ final ∈ machine.runList first cfg, final.Halted) : machine.runList (first + second) cfg = machine.runList first cfg

Once every endpoint has halted, extra clock steps add no choices or multiplicities.

theorem Turing.MultiTapeCTM.HaltsWithin.halted_of_mem_runList {k : ℕ} {Symbol State : Type} {input : List Symbol} {machine : MultiTapeCTM k Symbol State} {fuel : ℕ} {cfg final : Cfg k Symbol State input} (h : machine.HaltsWithin fuel cfg) (hfinal : final ∈ machine.runList fuel cfg) : final.Halted

An all-branches bound ensures every interpreted endpoint really has halted.

theorem Turing.MultiTapeCTM.haltsWithin_of_halted {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (hnonempty : ∀ (cfg : Cfg k Symbol State input), cfg.state ≠ none → machine.actions cfg ≠ []) (fuel : ℕ) (cfg : Cfg k Symbol State input) (h : ∀ final ∈ machine.runList fuel cfg, final.Halted) : machine.HaltsWithin fuel cfg

A non-stuck machine whose clocked endpoints all halt has the native all-branches bound. The no-stuck hypothesis matters: an empty choice list would otherwise satisfy the endpoint condition vacuously.

theorem Turing.MultiTapeCTM.length_output_of_mem_runList {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (fuel : ℕ) (cfg final : Cfg k Symbol State input) (hfinal : final ∈ machine.runList fuel cfg) : final.output.length ≤ cfg.output.length + fuel

Each actual instruction emits at most one symbol, including on a still-running branch.

theorem Turing.MultiTapeCTM.branchCount_succ {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (verdict : List Symbol → Bool) (cfg : Cfg k Symbol State input) (fuel : ℕ) (state : State) (h : cfg.state = some state) : machine.branchCount verdict (fuel + 1) cfg = ∑ index : Fin (machine.actions cfg).length, machine.branchCount verdict fuel ((machine.actions cfg)[index].apply cfg)

Terminal counts sum over positions in the transition list, even when actions coincide.

theorem Turing.MultiTapeCTM.countP_runList {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (verdict : List Symbol → Bool) (fuel : ℕ) (cfg : Cfg k Symbol State input) : List.countP (fun (final : Cfg k Symbol State input) => final.state.isNone && verdict final.output) (machine.runList fuel cfg) = machine.branchCount verdict fuel cfg

The List interpretation counts exactly the native terminal branches. Filtering for actual halting is essential when the clock is insufficient or a branch is stuck.

theorem Turing.MultiTapeCTM.HaltsWithin.branchCount_eq_countP {k : ℕ} {Symbol State : Type} {input : List Symbol} {machine : MultiTapeCTM k Symbol State} {fuel : ℕ} {cfg : Cfg k Symbol State input} (h : machine.HaltsWithin fuel cfg) (verdict : List Symbol → Bool) : machine.branchCount verdict fuel cfg = List.countP (fun (final : Cfg k Symbol State input) => verdict final.output) (machine.runList fuel cfg)

When all branches halt, counting output occurrences is exactly the native terminal count.