Parsimonious binary guessing

One fixed machine scans its input, choosing and emitting one bit per symbol, then takes a singleton halting instruction. Its occurrence-labelled terminal traces are in bijection with Boolean words of the input length. The final instruction makes no discarded binary choice.

Main definitions

• Turing.MultiTapeCTM.guessMachine: the zero-work-tape binary scanner.
• Turing.MultiTapeCTM.GuessMachine.trace: the unique occurrence trace for a witness.

Main results

• Turing.MultiTapeCTM.GuessMachine.haltsWithin: every branch halts in n + 1 steps.
• Turing.MultiTapeCTM.GuessMachine.runBranch_halted_iff: exact terminal trace and output.
• Turing.MultiTapeCTM.GuessMachine.trace_bijOn: one terminal branch per length-n word.
• Turing.MultiTapeCTM.GuessMachine.branchCount_eq: preserve every output-predicate count.
• Turing.MultiTapeCTM.GuessMachine.count_interpret_output: the shared FreeM/List program generates each length-n word once.

The scanner is used by the parsimonious guess/verify construction in MultiTape.Counting.Verifier and the #P characterization in Classes.SharpP.Characterization. Balanced signed routing in Classes.SharpP.GapMachine gives the reverse GapP construction and characterization.

References

The witness-guessing construction is standard in counting complexity [Val79b]. The scanner and its configuration invariant adapt MultiTape.Probabilistic.Sampling, credited there to the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8. Here the List choice interface and the singleton halt preserve exact branch multiplicity, rather than only the output law.

def Turing.MultiTapeCTM.GuessMachine.emit (bit : Bool) : Action 0 Bool Unit

The ordinary instruction for one guessed bit.

def Turing.MultiTapeCTM.GuessMachine.halt : Action 0 Bool Unit

The final instruction emits nothing and halts without moving the input head.

def Turing.MultiTapeCTM.guessMachine : MultiTapeCTM 0 Bool Unit

Emit one independently chosen bit per input symbol, then take a single halting occurrence.

theorem Turing.MultiTapeCTM.GuessMachine.nonblocking : guessMachine.Nonblocking

Every scanner local view has two bit occurrences or one final halt occurrence.

def Turing.MultiTapeCTM.GuessMachine.config (input : List Bool) (state : Option Unit) (index : ℕ) (output : List Bool) (h : index ≤ input.length) : Cfg 0 Bool Unit input

The scanner at a position in the input, with its current output prefix.

def Turing.MultiTapeCTM.GuessMachine.trace (word : List Bool) : List ℕ

Each bit selects its occurrence index; the last zero selects the singleton halt.

@[simp]

theorem Turing.MultiTapeCTM.GuessMachine.trace_nil : trace [] = [0]

@[simp]

theorem Turing.MultiTapeCTM.GuessMachine.trace_cons (bit : Bool) (word : List Bool) : trace (bit :: word) = bit.toNat :: trace word

@[simp]

theorem Turing.MultiTapeCTM.GuessMachine.length_trace (word : List Bool) : (trace word).length = word.length + 1

theorem Turing.MultiTapeCTM.GuessMachine.trace_injective : Function.Injective trace

theorem Turing.MultiTapeCTM.GuessMachine.step?_inner {input output : List Bool} {index : ℕ} (h : index < input.length) (choice : ℕ) : guessMachine.step? (config input (some ()) index output ⋯) choice = if choice < 2 then some (config input (some ()) (index + 1) (output ++ [choice == 1]) h) else none

theorem Turing.MultiTapeCTM.GuessMachine.step?_boundary (input output : List Bool) (choice : ℕ) : guessMachine.step? (config input (some ()) input.length output ⋯) choice = if choice = 0 then some (config input none input.length output ⋯) else none

theorem Turing.MultiTapeCTM.GuessMachine.runBranch_bits (input output word : List Bool) (index : ℕ) (h : index + word.length ≤ input.length) : guessMachine.runBranch (config input (some ()) index output ⋯) (List.map Bool.toNat word) = some (config input (some ()) (index + word.length) (output ++ word) h)

Replaying the bit choices writes that word, without taking the final halting instruction.

theorem Turing.MultiTapeCTM.GuessMachine.runBranch_trace (input output word : List Bool) (index : ℕ) (h : index + word.length = input.length) : guessMachine.runBranch (config input (some ()) index output ⋯) (trace word) = some (config input none input.length (output ++ word) ⋯)

A word of the remaining length ends at its output and the right boundary.

theorem Turing.MultiTapeCTM.GuessMachine.init_eq_config (input : List Bool) : Cfg.init guessMachine.initial input = config input (some ()) 0 [] ⋯

Starting from blank tapes is the zero-position scanner invariant.

theorem Turing.MultiTapeCTM.GuessMachine.haltsWithin (input : List Bool) : guessMachine.HaltsWithin (input.length + 1) (Cfg.init guessMachine.initial input)

Every branch halts in n + 1 transitions, with a nonempty choice list at every live node.

theorem Turing.MultiTapeCTM.GuessMachine.runBranch_halted_iff (input : List Bool) (choices : List ℕ) (final : Cfg 0 Bool Unit input) : guessMachine.runBranch (Cfg.init guessMachine.initial input) choices = some final ∧ final.Halted ↔ ∃ (word : List Bool), word.length = input.length ∧ choices = trace word ∧ final = config input none input.length word ⋯

Soundness and completeness of terminal replay, including its exact output.

theorem Turing.MultiTapeCTM.GuessMachine.length_of_terminal {input : List Bool} {choices : List ℕ} {final : Cfg 0 Bool Unit input} (hrun : guessMachine.runBranch (Cfg.init guessMachine.initial input) choices = some final) (hhalt : final.Halted) : choices.length = input.length + 1

Every terminal branch has exactly one instruction per input symbol and one final halt.

theorem Turing.MultiTapeCTM.GuessMachine.mem_branches_iff (input : List Bool) (fuel : ℕ) (choices : List ℕ) : choices ∈ guessMachine.branches fuel (Cfg.init guessMachine.initial input) ↔ input.length + 1 ≤ fuel ∧ ∃ (word : List Bool), word.length = input.length ∧ choices = trace word

The bounded terminal traces are exactly the encoded witnesses, with the exact clock exposed.

theorem Turing.MultiTapeCTM.GuessMachine.trace_bijOn (input : List Bool) : Set.BijOn trace {word : List Bool | word.length = input.length} ↑(guessMachine.branches (input.length + 1) (Cfg.init guessMachine.initial input))

Witness words and first-halting occurrence traces are in bijection.

theorem Turing.MultiTapeCTM.GuessMachine.branches_eq_image (input : List Bool) : guessMachine.branches (input.length + 1) (Cfg.init guessMachine.initial input) = Finset.image (fun (word : Cslib.BitString input.length) => trace (List.ofFn word)) Finset.univ

The same bijection, enumerated by the existing fixed-width bit-string type.

theorem Turing.MultiTapeCTM.GuessMachine.card_branches (input : List Bool) : (guessMachine.branches (input.length + 1) (Cfg.init guessMachine.initial input)).card = 2 ^ input.length

There are exactly 2 ^ n terminal branches, including one when the input is empty.

theorem Turing.MultiTapeCTM.GuessMachine.branchCount_eq (input : List Bool) (verdict : List Bool → Bool) : guessMachine.branchCount verdict (input.length + 1) (Cfg.init guessMachine.initial input) = {word : Cslib.BitString input.length | verdict (List.ofFn word) = true}.card

Counting any output predicate is exactly counting witnesses satisfying that predicate.

theorem Turing.MultiTapeCTM.GuessMachine.interpret_runProgram (input : List Bool) : (Cslib.OracleComp.interpret (fun (n : ℕ) => List.ofFn id) (guessMachine.runProgram (input.length + 1) (Cfg.init guessMachine.initial input))).Perm (List.map (fun (word : List Bool) => config input none input.length word ⋯) (Cslib.BitString.enumList input.length))

List interpretation of the shared program returns each word once, in scanner enumeration order. The existing bit-string enumeration can use a different order, so the result is a permutation.

theorem Turing.MultiTapeCTM.GuessMachine.count_interpret_output (input word : List Bool) : List.count word (Cslib.OracleComp.interpret (fun (n : ℕ) => List.ofFn id) (Cfg.output <$> guessMachine.runProgram (input.length + 1) (Cfg.init guessMachine.initial input))) = if word.length = input.length then 1 else 0

The shared FreeM program generates each word of the input length with multiplicity one.