The input-scanning query machine for inductive counting

The machine first counts the read-only input in binary. It then runs the streaming counting controller on the compact configuration graph of a stored radix, starting from Turing.MultiTapeNTM.ConfigurationGraph.startRadix, in two modes:

• while the radix is unchecked, the controller's bad vertices are those whose source step leaves the radix (Turing.MultiTapeNTM.ConfigurationGraph.overflow). If the final count check of a branch is complete and has met such a vertex, that vertex is certifiably reachable, and the machine moves to four times the radix. If the controller accepts, the radix is closed (Turing.InductiveCounting.Closed), and the machine checks it;
• once the radix is checked, the bad vertices are the accepting ones, and the controller's verdict is final.

So the radix grows only as far as the source's reachable views require, and the source needs no constructible space bound: as in Immerman's remark after his Theorem 1, the space is allowed to increase as needed [Imm88]. Neither the input nor a sequence of choices is stored in the state. Each query phase requests exactly the input symbol of its vertex.

Main definitions

• Turing.InductiveCounting.Runtime: the input counter, the radix, the mode and the controller.
• Turing.InductiveCounting.queryMachine: the complete binary-choice query machine.
• Turing.InductiveCounting.RuntimeInvariant: the semantic invariant of reachable states.

Main results

• Turing.InductiveCounting.runtimeInvariant_run: every prefix satisfies the invariant.
• Turing.InductiveCounting.queryMachine_accepts_iff_not_accepts: the machine accepts exactly the inputs the source does not accept, when some radix is closed.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.6
• N. Immerman, Nondeterministic Space Is Closed under Complementation

structure Turing.InductiveCounting.Runtime : Type

Before counting, counting = none and length is the next input position to inspect. Afterward length is the full input length, radix the current radix, checked records that the radix is closed, and counting is the bounded controller state.

• length : ℕ

  A binary input-length counter.

• radix : ℕ

  The radix of the current compact graph.

• checked : Bool

  Whether the radix has been certified closed.

• counting : Option Cslib.InductiveCounting.State

  The controller is installed only after the end of the input has been read.

def Turing.InductiveCounting.encRuntime : Runtime ↪ List Bool

The state encoding omits the input and every proof-level choice history.

noncomputable def Turing.InductiveCounting.modeBad {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (B n : ℕ) (checked : Bool) (u : ℕ) (symbol : Option Bool) : Bool

The bad vertices of a mode: those whose step leaves the radix while it is unchecked, the accepting ones once it is checked.

noncomputable def Turing.InductiveCounting.localAnswer {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (B n : ℕ) (checked : Bool) (c : Cslib.InductiveCounting.State) (symbol : Option Bool) : Bool

Answer a pending graph request using at most the one supplied input symbol.

noncomputable def Turing.InductiveCounting.controllerQuery (k B : ℕ) (c : Cslib.InductiveCounting.State) : ℕ

The input position of the controller's pending request: that of its first vertex.

noncomputable def Turing.InductiveCounting.runtimeQuery (k : ℕ) (s : Runtime) : ℕ

Input lookup for the length scan or the controller's pending request.

noncomputable def Turing.InductiveCounting.install {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (B : ℕ) : Cslib.InductiveCounting.State

The controller installed on the graph of radix B.

def Turing.InductiveCounting.overflowed (c : Cslib.InductiveCounting.State) : Bool

The final count check is complete and has met a bad vertex.

noncomputable def Turing.InductiveCounting.runtimeNext {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (s : Runtime) (symbol : Option Bool) (choice : Bool) : Runtime

The first phase increments a binary input counter. The second executes one checked controller instruction, unless the unchecked radix is found to overflow or to be closed. There is no unbounded search for a valid random guess.

def Turing.InductiveCounting.runtimeHalted (s : Runtime) : Bool

A runtime halts when its controller rejects, or accepts on a checked radix.

def Turing.InductiveCounting.runtimeAccept (s : Runtime) : Bool

Acceptance is the controller's acceptance on a checked radix.

noncomputable def Turing.InductiveCounting.queryMachine {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) : NondeterministicQueryMachine Runtime

The full uniform query machine. The original native machine is fixed when its program is selected; the runtime input does not supply code or advice.

Steps of the machine

noncomputable def Turing.InductiveCounting.graphBad {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (input : List Bool) (B : ℕ) (checked : Bool) : ℕ → Bool

The bad vertices of a mode, on the actual input.

@[reducible, inline]

noncomputable abbrev Turing.InductiveCounting.ctlStep {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (input : List Bool) (B : ℕ) (checked : Bool) (c : Cslib.InductiveCounting.State) (choice : Bool) : Cslib.InductiveCounting.State

One controller step on the graph of radix B.

@[reducible, inline]

noncomputable abbrev Turing.InductiveCounting.ctlReplay {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (input : List Bool) (B : ℕ) (checked : Bool) (c : Cslib.InductiveCounting.State) (choices : List Bool) : Cslib.InductiveCounting.State

A controller replay on the graph of radix B.

theorem Turing.InductiveCounting.localAnswer_eq {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (input : List Bool) (B : ℕ) (checked : Bool) (c : Cslib.InductiveCounting.State) : localAnswer ntm B input.length checked c input[controllerQuery k B c]? = Cslib.InductiveCounting.answer (graphEdge ntm B input) (graphBad ntm input B checked) c

A request reads the same original input symbol as the compact configuration graph.

theorem Turing.InductiveCounting.halted_ctlStep_of_done {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (input : List Bool) {B : ℕ} {checked : Bool} {c : Cslib.InductiveCounting.State} (hp : c.phase = Cslib.InductiveCounting.Phase.done) (hf : c.finalScan = true) (choice : Bool) : Cslib.InductiveCounting.halted (ctlStep ntm input B checked c choice) = true

A controller step from a state at the final count check halts.

theorem Turing.InductiveCounting.halted_ctlReplay {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (input : List Bool) {B : ℕ} {checked : Bool} {c : Cslib.InductiveCounting.State} (h : Cslib.InductiveCounting.halted c = true) (choices : List Bool) : ctlReplay ntm input B checked c choices = c

Replays of a halted controller state stay halted.

theorem Turing.InductiveCounting.step_counting {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (input : List Bool) {B : ℕ} {checked : Bool} {c : Cslib.InductiveCounting.State} (ho : ¬(checked = false ∧ overflowed c = true)) (ha : ¬(checked = false ∧ c.phase = Cslib.InductiveCounting.Phase.accept)) (choice : Bool) : (queryMachine ntm).step input { length := input.length, radix := B, checked := checked, counting := some c } choice = { length := input.length, radix := B, checked := checked, counting := some (ctlStep ntm input B checked c choice) }

After the length scan, a step that neither moves to a larger radix nor checks the radix is exactly one checked controller step, including on halted branches.

theorem Turing.InductiveCounting.step_overflowed {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (input : List Bool) {B : ℕ} {c : Cslib.InductiveCounting.State} (ho : overflowed c = true) (choice : Bool) : (queryMachine ntm).step input { length := input.length, radix := B, checked := false, counting := some c } choice = { length := input.length, radix := 4 * B, checked := false, counting := some (install ntm (4 * B)) }

A complete final count check meeting an overflowing vertex moves to four times the radix.

theorem Turing.InductiveCounting.step_switch {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (input : List Bool) {B : ℕ} {c : Cslib.InductiveCounting.State} (hp : c.phase = Cslib.InductiveCounting.Phase.accept) (choice : Bool) : (queryMachine ntm).step input { length := input.length, radix := B, checked := false, counting := some c } choice = { length := input.length, radix := B, checked := true, counting := some (install ntm B) }

Acceptance on an unchecked radix checks it.

theorem Turing.InductiveCounting.replay_checked {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (input : List Bool) {B : ℕ} (c : Cslib.InductiveCounting.State) (choices : List Bool) : (queryMachine ntm).replay input choices { length := input.length, radix := B, checked := true, counting := some c } = { length := input.length, radix := B, checked := true, counting := some (ctlReplay ntm input B true c choices) }

On a checked radix, the machine's replays are exactly the controller's replays.

theorem Turing.InductiveCounting.replay_unchecked_of_done {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (input : List Bool) {B : ℕ} (c : Cslib.InductiveCounting.State) (choices : List Bool) (hd : (ctlReplay ntm input B false c choices).phase = Cslib.InductiveCounting.Phase.done ∧ (ctlReplay ntm input B false c choices).finalScan = true) : (queryMachine ntm).replay input choices { length := input.length, radix := B, checked := false, counting := some c } = { length := input.length, radix := B, checked := false, counting := some (ctlReplay ntm input B false c choices) }

On an unchecked radix, a controller replay ending at the final count check is also a replay of the machine: no earlier state can move to another radix or check this one.

theorem Turing.InductiveCounting.exists_replay_unchecked_of_accept {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (input : List Bool) {B : ℕ} (c : Cslib.InductiveCounting.State) (choices : List Bool) (ha : (ctlReplay ntm input B false c choices).phase = Cslib.InductiveCounting.Phase.accept) : ∃ (choices' : List Bool) (t : Cslib.InductiveCounting.State), (queryMachine ntm).replay input choices' { length := input.length, radix := B, checked := false, counting := some c } = { length := input.length, radix := B, checked := false, counting := some t } ∧ t.phase = Cslib.InductiveCounting.Phase.accept

On an unchecked radix, a controller replay ending in acceptance has a prefix that is a replay of the machine reaching acceptance on this radix.

theorem Turing.InductiveCounting.step_scan {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (input : List Bool) {j : ℕ} (hj : j < input.length) (choice : Bool) : (queryMachine ntm).step input { length := j, radix := 0, checked := false, counting := none } choice = { length := j + 1, radix := 0, checked := false, counting := none }

The input scan ignores the choice bit and advances exactly one input position.

theorem Turing.InductiveCounting.step_scan_end {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (input : List Bool) (choice : Bool) : (queryMachine ntm).step input { length := input.length, radix := 0, checked := false, counting := none } choice = { length := input.length, radix := MultiTapeNTM.ConfigurationGraph.startRadix State input.length, checked := false, counting := some (install ntm (MultiTapeNTM.ConfigurationGraph.startRadix State input.length)) }

Reading the first absent input bit installs the controller on the first radix.

theorem Turing.InductiveCounting.replay_scan {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (input choices : List Bool) {j : ℕ} (hj : j + choices.length ≤ input.length) : (queryMachine ntm).replay input choices { length := j, radix := 0, checked := false, counting := none } = { length := j + choices.length, radix := 0, checked := false, counting := none }

Every prefix of the input scan has the same binary counter, independently of its choices.

theorem Turing.InductiveCounting.run_bootstrap {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (input choices : List Bool) (hlen : choices.length = input.length + 1) : (queryMachine ntm).run input choices = { length := input.length, radix := MultiTapeNTM.ConfigurationGraph.startRadix State input.length, checked := false, counting := some (install ntm (MultiTapeNTM.ConfigurationGraph.startRadix State input.length)) }

Every choice sequence of bootstrap length reaches exactly the installed controller.

The semantic invariant

def Turing.InductiveCounting.RuntimeInvariant {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (input : List Bool) (s : Runtime) : Prop

The semantic invariant of every runtime state reachable on input: the radix is that of a round whose earlier radices are not closed, the controller satisfies the semantic and storage invariants of its graph and mode, and a checked radix is closed.

theorem Turing.InductiveCounting.not_closed_of_overflowed {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {B : ℕ} (hB : Fintype.card (Option State) + 1 < B) {c : Cslib.InductiveCounting.State} (hi : Cslib.InductiveCounting.Invariant (MultiTapeNTM.ConfigurationGraph.vertexBound B) (graphEdge ntm B input) (graphOverflow ntm B input) (MultiTapeNTM.ConfigurationGraph.startID ntm B) c) (ho : overflowed c = true) : ¬Closed ntm B input

A complete final count check meeting an overflowing vertex shows that the radix is not closed.

theorem Turing.InductiveCounting.runtimeInvariant_install {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {j : ℕ} (hj : ∀ i < j, ¬Closed ntm (MultiTapeNTM.ConfigurationGraph.roundRadix State input.length i) input) : RuntimeInvariant ntm input { length := input.length, radix := MultiTapeNTM.ConfigurationGraph.roundRadix State input.length j, checked := false, counting := some (install ntm (MultiTapeNTM.ConfigurationGraph.roundRadix State input.length j)) }

theorem Turing.InductiveCounting.runtimeInvariant_step {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {s : Runtime} (h : RuntimeInvariant ntm input s) (choice : Bool) : RuntimeInvariant ntm input ((queryMachine ntm).step input s choice)

Every step preserves the invariant, whatever the choice.

theorem Turing.InductiveCounting.runtimeInvariant_replay {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {s : Runtime} (h : RuntimeInvariant ntm input s) (choices : List Bool) : RuntimeInvariant ntm input ((queryMachine ntm).replay input choices s)

theorem Turing.InductiveCounting.runtimeInvariant_run {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} (choices : List Bool) : RuntimeInvariant ntm input ((queryMachine ntm).run input choices)

Every choice prefix satisfies the invariant.

Acceptance

theorem Turing.InductiveCounting.not_accepts_of_queryMachine_accepts {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} (h : (queryMachine ntm).Accepts input) : ¬ntm.Accepts input

Every accepting branch certifies native nonacceptance: it accepted on a checked, hence closed, radix. No space bound of the source is used.

theorem Turing.InductiveCounting.queryMachine_accepts_iff_not_accepts {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} (hJ : ∃ (j : ℕ), Closed ntm (MultiTapeNTM.ConfigurationGraph.roundRadix State input.length j) input) : (queryMachine ntm).Accepts input ↔ ¬ntm.Accepts input

The machine accepts exactly the inputs the source does not accept, provided some round's radix is closed, as a space bound of the source guarantees.