Labelled branches of counting machines

MultiTapeCTM specializes the shared multi-tape machine to lists of transition occurrences. An occurrence is identified by its list index: two equal actions in the list remain two choices. Deterministic instructions have singleton lists. Configurations, actions and tape operations are the existing Turing ones; no new machine storage or instruction model is introduced.

A branch records occurrence indices and stops at its first halted configuration. In contrast to the upstream unlabelled step relation, halted configurations have no further labelled steps. An empty list at a running configuration is stuck, not a rejecting halt.

Main definitions

• Turing.MultiTapeCTM: the list-choice specialization of the common machine.
• Turing.MultiTapeCTM.lts: labelled transitions, using the existing Cslib.LTS interface.
• Turing.MultiTapeCTM.runBranch: replay a list of occurrence indices.
• Turing.MultiTapeCTM.branches: first-halting branches of bounded length.
• Turing.MultiTapeCTM.HaltsWithin: an all-branches time bound excluding stuck states.
• Turing.MultiTapeCTM.Nonblocking: no local view has an empty live transition list.
• Turing.MultiTapeCTM.acceptCount, Turing.MultiTapeCTM.rejectCount: terminal branch counts.

Main results

• Turing.MultiTapeCTM.mem_branches_iff: the enumeration is exactly the bounded terminal traces.
• Turing.MultiTapeCTM.HaltsWithin.branches_eq: larger sufficient clocks preserve every branch.
• Turing.MultiTapeCTM.exists_branchBound: finite control and alphabet bound occurrence counts.

This is operational counting semantics, without a claimed polynomial-time verifier or a new storage/instruction model. Canonical certificates are developed in MultiTape.Counting.Certificate.

References

• L. Valiant, The complexity of computing the permanent
• S. Fenner, L. Fortnow, S. Kurtz, Gap-definable counting classes

The shared machine calculus is adapted from the cslib crypto branch; its source and authors are credited in MultiTape.Machine and MultiTape.Machine.Equivalence. The counting layer retains the transition identities forgotten by the relation-based nondeterministic interface.

@[reducible, inline]

abbrev Turing.MultiTapeCTM (k : ℕ) (Symbol : Type u_1) (State : Type u_2) : Type (max (max (max u_1 u_2) 0) u_1 u_2)

A shared-core machine with a finite list of transition occurrences at each local view.

def Turing.MultiTapeCTM.actions {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg : Cfg k Symbol State input) : List (Action k Symbol State)

The live transition occurrences, in their specified order. A halted state has no choices.

def Turing.MultiTapeCTM.Nonblocking {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (machine : MultiTapeCTM k Symbol State) : Prop

Every running local view has a transition occurrence. This excludes stuck states even on unreachable configurations; a native HaltsWithin hypothesis only needs the reachable ones.

theorem Turing.MultiTapeCTM.Nonblocking.actions_ne_nil {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {machine : MultiTapeCTM k Symbol State} (h : machine.Nonblocking) (cfg : Cfg k Symbol State input) (hrun : cfg.state ≠ none) : machine.actions cfg ≠ []

A nonblocking transition table has an occurrence at every running configuration.

def Turing.MultiTapeCTM.step? {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg : Cfg k Symbol State input) (index : ℕ) : Option (Cfg k Symbol State input)

Execute one occurrence. Invalid indices and attempts to step a halted configuration fail.

def Turing.MultiTapeCTM.lts {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (machine : MultiTapeCTM k Symbol State) (input : List Symbol) : Cslib.LTS (Cfg k Symbol State input) ℕ

The native labelled transition system; labels identify occurrences, not their effects.

def Turing.MultiTapeCTM.runBranch {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) : Cfg k Symbol State input → List ℕ → Option (Cfg k Symbol State input)

Replay actual transitions, with no implicit padding after halting.

@[simp]

theorem Turing.MultiTapeCTM.runBranch_nil {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg : Cfg k Symbol State input) : machine.runBranch cfg [] = some cfg

theorem Turing.MultiTapeCTM.runBranch_cons {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg : Cfg k Symbol State input) (index : ℕ) (rest : List ℕ) : machine.runBranch cfg (index :: rest) = (machine.step? cfg index).bind fun (next : Cfg k Symbol State input) => machine.runBranch next rest

theorem Turing.MultiTapeCTM.runBranch_eq_some_iff {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg final : Cfg k Symbol State input) (choices : List ℕ) : machine.runBranch cfg choices = some final ↔ (machine.lts input).MTr cfg choices final

Replay is exactly the existing LTS multistep relation, with the occurrence labels retained.

theorem Turing.MultiTapeCTM.actions_of_halted {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) {cfg : Cfg k Symbol State input} (h : cfg.Halted) : machine.actions cfg = []

theorem Turing.MultiTapeCTM.step?_of_halted {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) {cfg : Cfg k Symbol State input} (h : cfg.Halted) (index : ℕ) : machine.step? cfg index = none

theorem Turing.MultiTapeCTM.runBranch_of_halted {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) {cfg : Cfg k Symbol State input} (h : cfg.Halted) (choices : List ℕ) : machine.runBranch cfg choices = if choices = [] then some cfg else none

From a halted configuration, only the empty trace can be replayed.

theorem Turing.MultiTapeCTM.runBranch_append {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg : Cfg k Symbol State input) (first second : List ℕ) : machine.runBranch cfg (first ++ second) = (machine.runBranch cfg first).bind fun (next : Cfg k Symbol State input) => machine.runBranch next second

Replaying concatenated traces is sequential replay; a premature halt cannot be crossed.

def Turing.MultiTapeCTM.branches {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) : ℕ → Cfg k Symbol State input → Finset (List ℕ)

Enumerate first-halting traces of at most the supplied number of actual transitions.

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

theorem Turing.MultiTapeCTM.step?_eq_some_iff {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg final : Cfg k Symbol State input) (index : ℕ) : machine.step? cfg index = some final ↔ ∃ (h : index < (machine.actions cfg).length), (machine.actions cfg)[index].apply cfg = final

A labelled step is exactly an in-range list occurrence, even if other occurrences agree.

@[simp]

theorem Turing.MultiTapeCTM.nil_mem_branches {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg : Cfg k Symbol State input) (fuel : ℕ) : [] ∈ machine.branches fuel cfg ↔ cfg.Halted

theorem Turing.MultiTapeCTM.cons_mem_branches {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg : Cfg k Symbol State input) (fuel index : ℕ) (rest : List ℕ) : index :: rest ∈ machine.branches (fuel + 1) cfg ↔ ∃ (next : Cfg k Symbol State input), machine.step? cfg index = some next ∧ rest ∈ machine.branches fuel next

theorem Turing.MultiTapeCTM.mem_branches_iff {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg : Cfg k Symbol State input) (fuel : ℕ) (choices : List ℕ) : choices ∈ machine.branches fuel cfg ↔ choices.length ≤ fuel ∧ ∃ (final : Cfg k Symbol State input), machine.runBranch cfg choices = some final ∧ final.Halted

The finite enumeration is exactly the first-halting LTS traces within the given clock.

inductive Turing.MultiTapeCTM.HaltsWithin {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) : ℕ → Cfg k Symbol State input → Prop

Every branch halts within this many actual transitions. Running configurations must have at least one occurrence, so a stuck branch cannot make a time bound hold vacuously.

• halt {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {machine : MultiTapeCTM k Symbol State} {fuel : ℕ} {cfg : Cfg k Symbol State input} (halted : cfg.Halted) : machine.HaltsWithin fuel cfg
• step {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {machine : MultiTapeCTM k Symbol State} {fuel : ℕ} {cfg : Cfg k Symbol State input} (nonempty : machine.actions cfg ≠ []) (next : ∀ (index : Fin (machine.actions cfg).length), machine.HaltsWithin fuel ((machine.actions cfg)[index].apply cfg)) : machine.HaltsWithin (fuel + 1) cfg

theorem Turing.MultiTapeCTM.HaltsWithin.mono {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {machine : MultiTapeCTM k Symbol State} {cfg : Cfg k Symbol State input} {fuel larger : ℕ} (h : machine.HaltsWithin fuel cfg) (hle : fuel ≤ larger) : machine.HaltsWithin larger cfg

Enlarging a sufficient clock does not add transitions after a branch halts.

theorem Turing.MultiTapeCTM.HaltsWithin.length_le {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {machine : MultiTapeCTM k Symbol State} {cfg final : Cfg k Symbol State input} {fuel : ℕ} (h : machine.HaltsWithin fuel cfg) {choices : List ℕ} (hrun : machine.runBranch cfg choices = some final) : choices.length ≤ fuel

A successful replay cannot pass the all-branches halting bound.

theorem Turing.MultiTapeCTM.HaltsWithin.branches_eq {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {machine : MultiTapeCTM k Symbol State} {cfg : Cfg k Symbol State input} {fuel larger : ℕ} (h : machine.HaltsWithin fuel cfg) (hle : fuel ≤ larger) : machine.branches larger cfg = machine.branches fuel cfg

A sufficient clock can be increased without changing any terminal branch multiplicity.

theorem Turing.MultiTapeCTM.HaltsWithin.branches_nonempty {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {machine : MultiTapeCTM k Symbol State} {cfg : Cfg k Symbol State input} {fuel : ℕ} (h : machine.HaltsWithin fuel cfg) : (machine.branches fuel cfg).Nonempty

The no-stuck condition guarantees at least one terminal branch.

def Turing.MultiTapeCTM.branchCount {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (verdict : List Symbol → Bool) (fuel : ℕ) (cfg : Cfg k Symbol State input) : ℕ

Count terminal branches whose output satisfies a Boolean verdict. A failed replay is never counted, even for the complementary verdict.

theorem Turing.MultiTapeCTM.branchCount_add_not {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (verdict : List Symbol → Bool) (fuel : ℕ) (cfg : Cfg k Symbol State input) : machine.branchCount verdict fuel cfg + machine.branchCount (fun (out : List Symbol) => !verdict out) fuel cfg = (machine.branches fuel cfg).card

Acceptance and rejection partition the terminal branches, without counting stuck states.

def Turing.MultiTapeCTM.acceptCount {k : ℕ} {State : Type u_2} (machine : MultiTapeCTM k Bool State) {input : List Bool} (fuel : ℕ) (cfg : Cfg k Bool State input) : ℕ

The accepting terminal count uses the standard one-bit true output convention.

def Turing.MultiTapeCTM.rejectCount {k : ℕ} {State : Type u_2} (machine : MultiTapeCTM k Bool State) {input : List Bool} (fuel : ℕ) (cfg : Cfg k Bool State input) : ℕ

Every terminal output other than the one-bit true word rejects. Invalid or stuck traces are not rejecting branches.

theorem Turing.MultiTapeCTM.acceptCount_add_rejectCount {k : ℕ} {State : Type u_2} (machine : MultiTapeCTM k Bool State) {input : List Bool} (fuel : ℕ) (cfg : Cfg k Bool State input) : machine.acceptCount fuel cfg + machine.rejectCount fuel cfg = (machine.branches fuel cfg).card

theorem Turing.MultiTapeCTM.HaltsWithin.branchCount_eq {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {machine : MultiTapeCTM k Symbol State} {cfg : Cfg k Symbol State input} {fuel larger : ℕ} (h : machine.HaltsWithin fuel cfg) (hle : fuel ≤ larger) (verdict : List Symbol → Bool) : machine.branchCount verdict larger cfg = machine.branchCount verdict fuel cfg

theorem Turing.MultiTapeCTM.exists_branchBound {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (machine : MultiTapeCTM k Symbol State) [Finite State] [Finite Symbol] : ∃ (bound : ℕ), ∀ (input : List Symbol) (cfg : Cfg k Symbol State input), (machine.actions cfg).length ≤ bound

Finite control and a fixed finite alphabet give one fixed bound on transition occurrences. Repeated actions are counted separately; their multiplicity is not bounded by Nat.card Action.