Nondeterministic query machines

A query machine with one binary nondeterministic choice per step. An abstract state can be infinite; it is data to be encoded on work tapes, rather than native finite control. The input is read by position, with none returned beyond its end. Halted states self-loop.

Finite lists of choices describe paths at the proof level. They are not additional inputs or work tapes of the machine. Acceptance requires both halting and an accepting state.

Main definitions

• Turing.NondeterministicQueryMachine: the binary-choice query model.
• Turing.NondeterministicQueryMachine.replay: replay choices from an arbitrary state.
• Turing.NondeterministicQueryMachine.RunPath: finite paths of the step relation.
• Turing.NondeterministicQueryMachine.Accepts: existential acceptance by a halted branch.
• Turing.NondeterministicQueryMachine.withInit: the same machine with another start state.

Main results

• Turing.NondeterministicQueryMachine.exists_runPath_iff: paths are exactly finite replays.
• Turing.NondeterministicQueryMachine.accepts_iff_length: an all-branches halting bound lets acceptance be checked at one common abstract time.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.4

structure Turing.NondeterministicQueryMachine (σ : Type u_1) : Type u_1

A decision-only query machine with one binary nondeterministic choice per step.

• init : σ

  The initial state.

• query : σ → ℕ

  The queried input position.

• next : σ × Option Bool × Bool → σ

  The next state, given the current state, input answer and nondeterministic choice.

• halted : σ → Bool

  Whether the state has halted.

• accept : σ → Bool

  Whether a halted state accepts. This field is ignored before halting.

def Turing.NondeterministicQueryMachine.read {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) (s : σ) : Option Bool

The input answer, none past the end of the input.

def Turing.NondeterministicQueryMachine.step {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) (s : σ) (choice : Bool) : σ

A step selected by one choice; halted states are fixed.

@[reducible, inline]

abbrev Turing.NondeterministicQueryMachine.Step {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) (s s' : σ) : Prop

The existential one-step relation, including halted self-loops.

def Turing.NondeterministicQueryMachine.replay {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input choices : List Bool) (s : σ) : σ

Replay a finite sequence of choices from a supplied state.

def Turing.NondeterministicQueryMachine.run {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input choices : List Bool) : σ

Run from the initial state with a finite sequence of choices.

@[reducible, inline]

abbrev Turing.NondeterministicQueryMachine.RunPath {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) : Type u_1

Finite paths of the abstract step relation.

def Turing.NondeterministicQueryMachine.Reachable {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) (s : σ) : Prop

A state reached by some finite branch.

def Turing.NondeterministicQueryMachine.Accepts {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) : Prop

Some finite branch halts and accepts.

def Turing.NondeterministicQueryMachine.HaltsWithin {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) (t : ℕ) : Prop

Every branch of exactly t abstract steps has halted.

def Turing.NondeterministicQueryMachine.withInit {σ : Type u_1} (M : NondeterministicQueryMachine σ) (s : σ) : NondeterministicQueryMachine σ

The same machine started in s. The compiler uses it to start each input in its own state.

@[simp]

theorem Turing.NondeterministicQueryMachine.withInit_init {σ : Type u_1} (M : NondeterministicQueryMachine σ) : M.withInit M.init = M

@[simp]

theorem Turing.NondeterministicQueryMachine.step_withInit {σ : Type u_1} (M : NondeterministicQueryMachine σ) (s : σ) : (M.withInit s).step = M.step

@[simp]

theorem Turing.NondeterministicQueryMachine.replay_withInit {σ : Type u_1} (M : NondeterministicQueryMachine σ) (s : σ) : (M.withInit s).replay = M.replay

theorem Turing.NondeterministicQueryMachine.run_withInit {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) (s : σ) (choices : List Bool) : (M.withInit s).run input choices = M.replay input choices s

@[simp]

theorem Turing.NondeterministicQueryMachine.replay_nil {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) (s : σ) : M.replay input [] s = s

theorem Turing.NondeterministicQueryMachine.replay_cons {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) (choice : Bool) (choices : List Bool) (s : σ) : M.replay input (choice :: choices) s = M.replay input choices (M.step input s choice)

theorem Turing.NondeterministicQueryMachine.replay_append {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input choices more : List Bool) (s : σ) : M.replay input (choices ++ more) s = M.replay input more (M.replay input choices s)

@[simp]

theorem Turing.NondeterministicQueryMachine.run_nil {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) : M.run input [] = M.init

theorem Turing.NondeterministicQueryMachine.run_append {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input choices more : List Bool) : M.run input (choices ++ more) = M.replay input more (M.run input choices)

theorem Turing.NondeterministicQueryMachine.step_of_halted {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) {s : σ} (h : M.halted s = true) (choice : Bool) : M.step input s choice = s

theorem Turing.NondeterministicQueryMachine.replay_of_halted {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) {s : σ} (h : M.halted s = true) (choices : List Bool) : M.replay input choices s = s

After halting, every further choice is ignored.

theorem Turing.NondeterministicQueryMachine.run_append_of_halted {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) {choices : List Bool} (h : M.halted (M.run input choices) = true) (more : List Bool) : M.run input (choices ++ more) = M.run input choices

theorem Turing.NondeterministicQueryMachine.exists_runPath_iff {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) {s s' : σ} {n : ℕ} : (∃ (p : M.RunPath input), RelSeries.head p = s ∧ p.length = n ∧ RelSeries.last p = s') ↔ ∃ (choices : List Bool), choices.length = n ∧ M.replay input choices s = s'

Every finite relational path is a choice replay of the same length, and conversely.

theorem Turing.NondeterministicQueryMachine.reachable_init {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) : M.Reachable input M.init

theorem Turing.NondeterministicQueryMachine.Reachable.step {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) {s : σ} (h : M.Reachable input s) (choice : Bool) : M.Reachable input (M.step input s choice)

theorem Turing.NondeterministicQueryMachine.HaltsWithin.mono {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) {t t' : ℕ} (h : M.HaltsWithin input t) (ht : t ≤ t') : M.HaltsWithin input t'

A common all-branches clock also bounds every longer branch.

theorem Turing.NondeterministicQueryMachine.accepts_iff_length {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) {t : ℕ} (h : M.HaltsWithin input t) : M.Accepts input ↔ ∃ (choices : List Bool), choices.length = t ∧ M.accept (M.run input choices) = true

Acceptance can be tested at the common clock: short branches are padded by halted self-loops, and longer branches already halted at the clock. The padding is proof-level data only.

theorem Turing.NondeterministicQueryMachine.run_take_of_haltsWithin {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) {t : ℕ} (h : M.HaltsWithin input t) (choices : List Bool) : M.run input (List.take t choices) = M.run input choices

A branch longer than the common clock has the same state as its clock-length prefix.

theorem Turing.NondeterministicQueryMachine.exists_bound_on_reachable {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) {t : ℕ} (h : M.HaltsWithin input t) (cost : σ → ℕ) : ∃ (bound : ℕ), ∀ (s : σ), M.Reachable input s → cost s ≤ bound

Any total local runtime has a common finite bound on all reachable states of an abstract machine with an all-branches clock. This maximum is proof-level data: it need not be computed by the simulator, encoded in a state, or stored on a tape.

def Turing.NondeterministicQueryMachine.HaltsFrom {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) (s : σ) (t : ℕ) : Prop

Every branch of t steps from the supplied abstract state has halted.

theorem Turing.NondeterministicQueryMachine.haltsFrom_of_reachable {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) {t : ℕ} (h : M.HaltsWithin input t) {s : σ} (hs : M.Reachable input s) : M.HaltsFrom input s t

A clock for the initial state is also a clock from every reachable state. The extra history only makes the complete branch longer than the original clock.

noncomputable def Turing.NondeterministicQueryMachine.remainingSteps {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) (s : σ) : ℕ

The least all-branches halting clock from a state, or zero when no such clock exists. This is a ghost ranking function, not a counter stored by the native simulator.

theorem Turing.NondeterministicQueryMachine.remainingSteps_spec {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) {s : σ} (h : ∃ (t : ℕ), M.HaltsFrom input s t) : M.HaltsFrom input s (M.remainingSteps input s)

theorem Turing.NondeterministicQueryMachine.remainingSteps_le {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) {s : σ} {t : ℕ} (h : M.HaltsFrom input s t) : M.remainingSteps input s ≤ t

theorem Turing.NondeterministicQueryMachine.remainingSteps_pos {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) {s : σ} (h : ∃ (t : ℕ), M.HaltsFrom input s t) (hs : M.halted s = false) : 0 < M.remainingSteps input s

theorem Turing.NondeterministicQueryMachine.remainingSteps_step_lt {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) {s : σ} (h : ∃ (t : ℕ), M.HaltsFrom input s t) (hs : M.halted s = false) (choice : Bool) : M.remainingSteps input (M.step input s choice) < M.remainingSteps input s

The ghost clock strictly decreases on every branch from a running state. The native machine can therefore be proved terminating without computing or storing any runtime maximum.

Reusing the deterministic input pass

def Turing.NondeterministicQueryMachine.withChoice {σ : Type u_1} (M : NondeterministicQueryMachine σ) (choice : Bool) : QueryMachine σ

Fixing the choice gives a deterministic query machine. This does not enumerate choices or store a witness: it supplies either of the two local transition routines.

theorem Turing.NondeterministicQueryMachine.step_withChoice {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) (choice : Bool) (s : σ) : (M.withChoice choice).step input s = M.step input s choice

theorem Turing.NondeterministicQueryMachine.streamState_passNext {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) (choice : Bool) (s : σ) : MultiTapeTM.streamState (s, 0, none) (QueryMachine.Simulation.passNext (M.withChoice choice)) input input.length = (s, input.length, M.read input s)

The deterministic input scan fetches exactly the abstract query answer.

theorem Turing.NondeterministicQueryMachine.passEnd_streamState {σ : Type u_1} (M : NondeterministicQueryMachine σ) (input : List Bool) (choice : Bool) (s : σ) : QueryMachine.Simulation.passEnd (M.withChoice choice) (MultiTapeTM.streamState (s, 0, none) (QueryMachine.Simulation.passNext (M.withChoice choice)) input input.length) = (M.step input s choice, 0, none)

The end of a deterministic pass performs the selected nondeterministic abstract step and resets the position counter and fetched answer.

Local computation and space bounds

theorem Turing.NondeterministicQueryMachine.next_withChoice_inSpace {σ : Type} {encS : σ ↪ List Bool} {M : NondeterministicQueryMachine σ} (hnext : MultiTapeTM.ComputableInSpace M.next (MultiTapeTM.encPair encS (MultiTapeTM.encPair (MultiTapeTM.encOption MultiTapeTM.encBool) MultiTapeTM.encBool)) encS fun (p : σ × Option Bool × Bool) => ((MultiTapeTM.encPair encS (MultiTapeTM.encPair (MultiTapeTM.encOption MultiTapeTM.encBool) MultiTapeTM.encBool)) p).length) (choice : Bool) : MultiTapeTM.ComputableInSpace (M.withChoice choice).next (MultiTapeTM.encPair encS (MultiTapeTM.encOption MultiTapeTM.encBool)) encS fun (p : σ × Option Bool) => ((MultiTapeTM.encPair encS (MultiTapeTM.encOption MultiTapeTM.encBool)) p).length

Fixing the native choice preserves linear-space computability of the transition routine.

theorem Turing.NondeterministicQueryMachine.passNext_inSpace {σ : Type} {encS : σ ↪ List Bool} {M : NondeterministicQueryMachine σ} (hquery : MultiTapeTM.ComputableInSpace M.query encS MultiTapeTM.encNat fun (s : σ) => (encS s).length) (choice : Bool) : MultiTapeTM.ComputableInSpace (QueryMachine.Simulation.passNext (M.withChoice choice)) (MultiTapeTM.encPair (QueryMachine.Simulation.encPass encS) MultiTapeTM.encBool) (QueryMachine.Simulation.encPass encS) fun (p : QueryMachine.Simulation.PassState σ × Bool) => ((MultiTapeTM.encPair (QueryMachine.Simulation.encPass encS) MultiTapeTM.encBool) p).length

The input-scan callback is the deterministic one and does not depend on the choice.

theorem Turing.NondeterministicQueryMachine.passEnd_inSpace {σ : Type} {encS : σ ↪ List Bool} {M : NondeterministicQueryMachine σ} (hnext : MultiTapeTM.ComputableInSpace M.next (MultiTapeTM.encPair encS (MultiTapeTM.encPair (MultiTapeTM.encOption MultiTapeTM.encBool) MultiTapeTM.encBool)) encS fun (p : σ × Option Bool × Bool) => ((MultiTapeTM.encPair encS (MultiTapeTM.encPair (MultiTapeTM.encOption MultiTapeTM.encBool) MultiTapeTM.encBool)) p).length) (hhalted : MultiTapeTM.ComputableInSpace M.halted encS MultiTapeTM.encBool fun (s : σ) => (encS s).length) (choice : Bool) : MultiTapeTM.ComputableInSpace (QueryMachine.Simulation.passEnd (M.withChoice choice)) (QueryMachine.Simulation.encPass encS) (QueryMachine.Simulation.encPass encS) fun (p : QueryMachine.Simulation.PassState σ) => ((QueryMachine.Simulation.encPass encS) p).length

Either end-of-pass routine is computable in space linear in the encoded pass state.

theorem Turing.NondeterministicQueryMachine.passCont_inSpace {σ : Type} {encS : σ ↪ List Bool} {M : NondeterministicQueryMachine σ} (hhalted : MultiTapeTM.ComputableInSpace M.halted encS MultiTapeTM.encBool fun (s : σ) => (encS s).length) (choice : Bool) : MultiTapeTM.ComputableInSpace (QueryMachine.Simulation.passCont (M.withChoice choice)) (QueryMachine.Simulation.encPass encS) MultiTapeTM.encBool fun (p : QueryMachine.Simulation.PassState σ) => ((QueryMachine.Simulation.encPass encS) p).length

The pass continuation test is computable in linear space.

theorem Turing.NondeterministicQueryMachine.passFinish_inSpace {σ : Type} {encS : σ ↪ List Bool} {M : NondeterministicQueryMachine σ} (haccept : MultiTapeTM.ComputableInSpace M.accept encS MultiTapeTM.encBool fun (s : σ) => (encS s).length) (choice : Bool) : MultiTapeTM.ComputableInSpace (QueryMachine.Simulation.passFinish (M.withChoice choice)) (QueryMachine.Simulation.encPass encS) MultiTapeTM.encBits fun (p : QueryMachine.Simulation.PassState σ) => ((QueryMachine.Simulation.encPass encS) p).length

The finalizer emits exactly the acceptance bit, with linear-space computation.

theorem Turing.NondeterministicQueryMachine.length_passState_le (input : List Bool) {σ : Type} {encS : σ ↪ List Bool} {s : σ} {j S c : ℕ} (hstate : (encS s).length ≤ c * S) (hlog : input.length.log2 + 1 ≤ S) (hj : j ≤ input.length) (answer : Option Bool) : ((QueryMachine.Simulation.encPass encS) (s, j, answer)).length ≤ (2 * c + 6) * S

The encoded scan state fits in the abstract-state budget plus the binary input counter. This estimate is independent of the number of passes and of all earlier choices.

theorem Turing.NondeterministicQueryMachine.length_scanState_le (input : List Bool) {σ : Type} {encS : σ ↪ List Bool} {M : NondeterministicQueryMachine σ} {S c : ℕ} (hstate : ∀ (s : σ), M.Reachable input s → (encS s).length ≤ c * S) (hlog : input.length.log2 + 1 ≤ S) (choices : List Bool) {j : ℕ} (hj : j ≤ input.length) (answer : Option Bool) : ((QueryMachine.Simulation.encPass encS) (M.run input choices, j, answer)).length ≤ (2 * c + 6) * S

Every abstract prefix state has the same space bound when the bound holds on reachable states. No choice history is included in the encoded state.