Nondeterministic counter programs

A counter program (Turing.CounterProgram) runs nondeterministically when register 0 receives a fresh nondeterministic bit after every step (Turing.CounterProgram.toNondeterministicQueryMachine): an instruction branches on the bit by comparing register 0 with 1. The rest of a step is the deterministic one; in particular the first instruction sees register 0 at 0. A branch accepts when it halts with the final word [true].

A program that halts on every branch of every encoded input enc a within time a steps, whose registers stay at most (n + 1) ^ d on every branch, where n is the length of the input, decides in logarithmic space the problem of the inputs it accepts (Turing.CounterProgram.exists_decidesInLogSpace): one finite-state nondeterministic machine decides it within space c * (Nat.log2 n + 1), every branch halting (Turing.MultiTapeNTM.DecidesInSpace). This is the classical description of nondeterministic logarithmic-space algorithms, a constant number of polynomially bounded counters and random read-only access to the input Sipser, Section 8.4. The machine is compiled through Turing.NondeterministicQueryMachine.exists_decidesInSpace.

Halting on every branch and the register bounds are established together from an invariant and a rank that every step from a running configuration satisfying the invariant decreases, whatever the choice (Turing.CounterProgram.haltsWithin_of_rank, Turing.CounterProgram.forall_run_of_rank). Accepting branches are built step by step (Turing.CounterProgram.Branches).

Main definitions

• Turing.CounterProgram.withChoice: overwrite register 0 by a choice bit.
• Turing.CounterProgram.toNondeterministicQueryMachine: a counter program as a nondeterministic query machine.
• Turing.CounterProgram.Branches: some branch leads from one configuration to another.

Main results

• Turing.CounterProgram.step_toNondeterministicQueryMachine: a nondeterministic step is a deterministic step followed by a choice.
• Turing.CounterProgram.haltsWithin_of_rank, Turing.CounterProgram.forall_run_of_rank: halting on every branch and invariants of every branch, from a decreasing rank.
• Turing.CounterProgram.accepts_of_branches: a branch to the accepting halt accepts.
• Turing.CounterProgram.exists_decidesInLogSpace: nondeterministic counter programs with polynomially bounded registers decide in logarithmic space.

References

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

def Turing.CounterProgram.withChoice (s : Config) (choice : Bool) : Config

Overwrite register 0 by the choice bit, 1 for true and 0 for false.

def Turing.CounterProgram.toNondeterministicQueryMachine (P : CounterProgram) : NondeterministicQueryMachine Config

A counter program as a nondeterministic query machine: a step is a deterministic step, after which register 0 receives the choice. A halted branch accepts when its final word is [true].

theorem Turing.CounterProgram.step_toNondeterministicQueryMachine (P : CounterProgram) (w : List Bool) (s : Config) (choice : Bool) : P.toNondeterministicQueryMachine.step w s choice = if P.halted s = true then s else withChoice (P.step w s) choice

A nondeterministic step is a deterministic step followed by a choice; halted configurations stay put.

@[simp]

theorem Turing.CounterProgram.withChoice_fst (s : Config) (choice : Bool) : (withChoice s choice).1 = s.1

@[simp]

theorem Turing.CounterProgram.withChoice_snd (s : Config) (choice : Bool) : (withChoice s choice).2 = s.2.set 0 choice.toNat

Every branch

theorem Turing.CounterProgram.forall_replay_of_inv {P : CounterProgram} {w : List Bool} (Inv : Config → Prop) (hstep : ∀ (s : Config), Inv s → P.halted s = false → ∀ (choice : Bool), Inv (withChoice (P.step w s) choice)) (choices : List Bool) {s : Config} (hs : Inv s) : Inv (P.toNondeterministicQueryMachine.replay w choices s)

An invariant preserved by every step from a running configuration holds of every configuration on every branch, halted configurations staying put.

theorem Turing.CounterProgram.forall_run_of_rank {P : CounterProgram} {w : List Bool} (Inv : Config → Prop) (hinit : Inv P.init) (hstep : ∀ (s : Config), Inv s → P.halted s = false → ∀ (choice : Bool), Inv (withChoice (P.step w s) choice)) (choices : List Bool) : Inv (P.toNondeterministicQueryMachine.run w choices)

An invariant of every branch, from an invariant of the initial configuration preserved by every step from a running configuration.

theorem Turing.CounterProgram.haltsWithin_of_rank {P : CounterProgram} {w : List Bool} (Inv : Config → Prop) (rank : Config → ℕ) (hinit : Inv P.init) (hstep : ∀ (s : Config), Inv s → P.halted s = false → ∀ (choice : Bool), Inv (withChoice (P.step w s) choice) ∧ rank (withChoice (P.step w s) choice) < rank s) : P.toNondeterministicQueryMachine.HaltsWithin w (rank P.init)

Every branch halts within the rank of the initial configuration, when every step from a running configuration satisfying an invariant preserves it and decreases the rank, whatever the choice.

Some branch

def Turing.CounterProgram.Branches {P : CounterProgram} {w : List Bool} (s s' : Config) : Prop

Some branch leads from s to s'.

theorem Turing.CounterProgram.Branches.refl {P : CounterProgram} {w : List Bool} (s : Config) : Branches s s

theorem Turing.CounterProgram.Branches.trans {P : CounterProgram} {w : List Bool} {s s' s'' : Config} (h : Branches s s') (h' : Branches s' s'') : Branches s s''

theorem Turing.CounterProgram.Branches.single {P : CounterProgram} {w : List Bool} {s : Config} (hs : P.halted s = false) (choice : Bool) : Branches s (withChoice (P.step w s) choice)

One step from a running configuration, with either choice.

theorem Turing.CounterProgram.Branches.head {P : CounterProgram} {w : List Bool} {s s' : Config} (hs : P.halted s = false) (choice : Bool) (h : Branches (withChoice (P.step w s) choice) s') : Branches s s'

theorem Turing.CounterProgram.accepts_of_branches {P : CounterProgram} {w : List Bool} {s : Config} (h : Branches P.init s) (hs : P.instr s.1 = Instr.accept) : P.toNondeterministicQueryMachine.Accepts w

A branch to the accepting halt accepts.

theorem Turing.CounterProgram.instr_of_accepts {P : CounterProgram} {w choices : List Bool} (hhalt : P.toNondeterministicQueryMachine.halted (P.toNondeterministicQueryMachine.run w choices) = true) (hacc : P.toNondeterministicQueryMachine.accept (P.toNondeterministicQueryMachine.run w choices) = true) : P.instr (P.toNondeterministicQueryMachine.run w choices).1 = Instr.accept

An accepting branch ends at a halt with the final word [true].

Logarithmic space

theorem Turing.CounterProgram.exists_decidesInLogSpace (P : CounterProgram) {α : Type} {enc : α ↪ List Bool} {A : Set α} (time : α → ℕ) (d : ℕ) (hhalt : ∀ (a : α), P.toNondeterministicQueryMachine.HaltsWithin (enc a) (time a)) (hbound : ∀ (a : α) (choices : List Bool), ∀ r ∈ (P.toNondeterministicQueryMachine.run (enc a) choices).2, r ≤ ((enc a).length + 1) ^ d) (hA : ∀ (a : α), a ∈ A ↔ P.toNondeterministicQueryMachine.Accepts (enc a)) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (ntm : MultiTapeNTM k Bool State) (c : ℕ), ntm.DecidesInSpace enc A fun (a : α) => c * ((enc a).length.log2 + 1)

Nondeterministic counter programs decide in logarithmic space. Let a counter program, run nondeterministically, halt on every branch on every encoded input enc a within time a steps, let its registers stay at most (n + 1) ^ d on every branch, where n is the length of the input, and let it accept exactly the inputs of the instances in A. Then one finite-state nondeterministic machine decides A within space c * (Nat.log2 n + 1), halting on every branch.