Counting-machine runs as shared programs

The choice program queries an occurrence index in Fin choices.length. Interpreting such queries by the list of all indices preserves repeated occurrences, and a singleton instruction has one outcome. An empty choice list interprets to no outcomes.

Main definitions

• Turing.MultiTapeCTM.occurrenceSpec: a finite occurrence-index query.
• Turing.MultiTapeCTM.chooseOccurrence: select an entry without identifying equal entries.
• Turing.MultiTapeCTM.runProgram: the existing shared runConfigFrom with this choice handler.

Main results

• Turing.MultiTapeCTM.interpret_chooseOccurrence: List interpretation recovers the exact list.
• Turing.MultiTapeCTM.chooseOccurrence_map: mapping preserves the occurrence query program.
• Turing.MultiTapeCTM.interpret_runProgram_succ: one actual transition unfolds by list bind.

These are programs in the existing PFunctor.FreeM calculus, not a second branch semantics or an efficiency claim about an interpreter. The machine and program infrastructure credits its authors in MultiTape.Machine and MultiTape.Machine.Program; the oracle interface and generic interpretation credit Devon Tuma, Quang Dao and VCVio in Languages.Probabilistic.Basic.

@[reducible, inline]

abbrev Turing.MultiTapeCTM.occurrenceSpec : Cslib.OracleSpec ℕ

Query the index of one of n transition occurrences; n = 0 permits no response.

def Turing.MultiTapeCTM.chooseOccurrence {α : Type} (choices : List α) : Cslib.OracleComp occurrenceSpec α

Select a list entry by its occurrence index, preserving equal entries at distinct positions.

theorem Turing.MultiTapeCTM.chooseOccurrence_map {α β : Type} (f : α → β) (choices : List α) : chooseOccurrence (f <$> choices) = f <$> chooseOccurrence choices

Mapping changes each response value without adding or identifying occurrence queries.

theorem Turing.MultiTapeCTM.interpret_chooseOccurrence {α : Type} (choices : List α) : Cslib.OracleComp.interpret (fun (n : ℕ) => List.ofFn id) (chooseOccurrence choices) = choices

Enumerating responses recovers the original list, including its order and multiplicities.

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

The shared clocked machine program, with finite-index choice and no oracle channels.

@[simp]

theorem Turing.MultiTapeCTM.runProgram_zero {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg : Cfg k Symbol State input) : machine.runProgram 0 cfg = pure cfg

theorem Turing.MultiTapeCTM.runProgram_halted {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) {cfg : Cfg k Symbol State input} (h : cfg.Halted) (fuel : ℕ) : machine.runProgram fuel cfg = pure cfg

theorem Turing.MultiTapeCTM.interpret_runProgram_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) : Cslib.OracleComp.interpret (fun (n : ℕ) => List.ofFn id) (machine.runProgram (fuel + 1) cfg) = List.flatMap (fun (action : Action k Symbol State) => Cslib.OracleComp.interpret (fun (n : ℕ) => List.ofFn id) (machine.runProgram fuel (action.apply cfg))) (machine.actions cfg)

List interpretation executes each live occurrence once and then continues the same program.