Deciding problems with nondeterministic machines

A nondeterministic machine accepts an input when some computation path ends halted with output [true], the encoding Turing.MultiTapeTM.encBool true used by verifiers and deterministic deciders. Paths that halt with another output, and paths ending in a stuck configuration, do not accept. A machine decides A in time t Arora and Barak, Definition 2.5 when on every encoded instance enc a, every computation path of at least t a steps ends halted, and a ∈ A exactly when some computation path on enc a accepts. The time bound applies to every branch, including rejecting ones.

A transition relation may be empty at a running configuration. Upstream's Turing.MultiTapeNTM.RunsInTime therefore permits a computation path that ends stuck before the time bound; such a path neither halts nor accepts. When no configuration is stuck, every computation path within the bound extends to a halted one of exactly the bound (Turing.MultiTapeNTM.ComputationPath.exists_halted_extension).

A machine recognizes A within space s (Turing.MultiTapeNTM.RecognizesInSpace) when on every encoded instance every computation prefix visits at most s a work-tape cells (upstream Turing.MultiTapeNTM.RunsInSpace), and a ∈ A exactly when some computation path accepts. No time bound is imposed: a branch may run forever or end stuck, and neither accepts. It decides A within space s (Turing.MultiTapeNTM.DecidesInSpace) when moreover every branch halts Sipser, Definition 8.1: on every encoded instance some number of steps t bounds every computation path (upstream Turing.MultiTapeNTM.RunsInTime). A path may still end stuck before t steps; it does not accept, as a branch of a textbook machine that has no move rejects. The bound t may depend arbitrarily on the instance. For machines with finitely many states, as in NL and NPSPACE, there are finitely many actions, so the machine branches finitely and by König's lemma this is equivalent to every branch halting; with infinitely many states it can be strictly stronger. The terminology follows Sipser's for deterministic machines, which recognize a language when they may loop and decide it when they halt on every input.

Turing.MultiTapeNTM.DecidableInPolyTime asks for one machine with a binary alphabet and finitely many states, and one polynomially bounded time bound, for all instances. Like Turing.MultiTapeTM.ComputableTidilyInPolyTime, it is relative to the encoding of instances.

Main definitions

• Turing.MultiTapeNTM.Accepts: some computation path halts with output [true].
• Turing.MultiTapeNTM.DecidesInTime: a machine decides a problem within a time bound.
• Turing.MultiTapeNTM.RecognizesInSpace: a machine recognizes a problem within a space bound, with no halting requirement.
• Turing.MultiTapeNTM.DecidesInSpace: a machine decides a problem within a space bound, every branch halting.
• Turing.MultiTapeNTM.DecidableInTime, Turing.MultiTapeNTM.DecidableInPolyTime: some finite binary machine decides a problem within a time bound, or within a polynomial time bound.

Main results

• Turing.MultiTapeNTM.RunPath.exists_extend_of_halted: a halted path extends to any length.
• Turing.MultiTapeNTM.RunsInTime.exists_time_eq: under a time bound, a halted computation path has the last configuration of one of exactly the bound.
• Turing.MultiTapeNTM.accepts_iff_exists_time_eq: under a time bound t, acceptance is witnessed by a computation path of exactly t steps.
• Turing.MultiTapeNTM.ComputationPath.exists_halted_extension: without stuck configurations, every computation path within a time bound is a prefix of a halted one.
• Turing.MultiTapeNTM.runsInTime_one_of_forall_step_initCfg: a machine whose first steps all halt runs within one step.
• Turing.MultiTapeNTM.DecidesInSpace.recognizesInSpace: a decider is a recognizer.
• Turing.MultiTapeNTM.DecidesInSpace.exists_runsInTime: every branch of a decider halts.
• Turing.MultiTapeNTM.RunsInTime.runsInSpace: space is at most time.
• Turing.MultiTapeNTM.DecidesInTime.decidesInSpace: a time-bounded decider is a space-bounded one.
• Turing.MultiTapeTM.ComputesFunInTimeAndSpace.decidesInSpace, Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_decidesInSpace: a deterministic decider within space s is a nondeterministic one with one computation path.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• M. Sipser, Introduction to the Theory of Computation

theorem Turing.MultiTapeNTM.RunPath.exists_extend_of_halted {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) (h : (RelSeries.last p).Halted) {n : ℕ} (hn : p.length ≤ n) : ∃ (q : ntm.RunPath input), RelSeries.head q = RelSeries.head p ∧ q.length = n ∧ RelSeries.last q = RelSeries.last p

A run path that ends halted extends to any longer length, by steps of its halted last configuration to itself.

theorem Turing.MultiTapeNTM.RunsInTime.exists_time_eq {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} {t : ℕ} (ht : ntm.RunsInTime input t) (p : ntm.ComputationPath input) (hp : p.last.Halted) : ∃ (q : ntm.ComputationPath input), q.time = t ∧ q.last = p.last

Under a time bound t, every computation path that ends halted has the same last configuration as a computation path of exactly t steps.

theorem Turing.MultiTapeNTM.RunPath.exists_extend {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (htotal : ∀ (c : Cfg k Symbol State input), ∃ (c' : Cfg k Symbol State input), ntm.Step c c') (p : ntm.RunPath input) {n : ℕ} (hn : p.length ≤ n) : ∃ (q : ntm.RunPath input) (hq : q.length = n), ∀ (i : ℕ) (hi : i < p.length + 1), q.toFun ⟨i, ⋯⟩ = p.toFun ⟨i, hi⟩

Without stuck configurations, every run path extends to any longer length, as a prefix.

theorem Turing.MultiTapeNTM.ComputationPath.exists_halted_extension {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (htotal : ∀ (c : Cfg k Symbol State input), ∃ (c' : Cfg k Symbol State input), ntm.Step c c') {t : ℕ} (ht : ntm.RunsInTime input t) (p : ntm.ComputationPath input) (hp : p.time ≤ t) : ∃ (q : ntm.ComputationPath input) (hq : q.time = t), q.last.Halted ∧ ∀ (i : ℕ) (hi : i < p.length + 1), q.toFun ⟨i, ⋯⟩ = p.toFun ⟨i, hi⟩

Actual halting. Without stuck configurations, every computation path within a time bound t is a prefix of a computation path of exactly t steps, which has halted.

theorem Turing.MultiTapeNTM.runsInTime_one_of_forall_step_initCfg {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (h : ∀ (c : Cfg k Symbol State input), ntm.Step (ntm.initCfg input) c → c.Halted) : ntm.RunsInTime input 1

If every step from the initial configuration reaches a halted configuration, every computation path halts within one step.

theorem Turing.MultiTapeNTM.ComputationPath.exists_snoc {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.ComputationPath input) {c : Cfg k Symbol State input} (h : ntm.Step p.last c) : ∃ (q : ntm.ComputationPath input), q.time = p.time + 1 ∧ q.last = c

A computation path extends by any step from its last configuration.

def Turing.MultiTapeNTM.Accepts {k : ℕ} {State : Type u_1} (ntm : MultiTapeNTM k Bool State) (input : List Bool) : Prop

The machine accepts input when some computation path ends halted with output [true].

theorem Turing.MultiTapeNTM.accepts_iff_exists_time_eq {k : ℕ} {State : Type u_1} {ntm : MultiTapeNTM k Bool State} {input : List Bool} {t : ℕ} (ht : ntm.RunsInTime input t) : ntm.Accepts input ↔ ∃ (p : ntm.ComputationPath input), p.time = t ∧ p.last.output = [true]

Under a time bound t, a machine accepts exactly when some computation path of exactly t steps ends with output [true]; such a path has halted.

def Turing.MultiTapeNTM.DecidesInTime {k : ℕ} {State : Type u_1} {α : Type u_3} (ntm : MultiTapeNTM k Bool State) (enc : α ↪ List Bool) (A : Set α) (t : α → ℕ) : Prop

ntm decides A within t relative to the encoding enc: on every encoded instance enc a, every computation path of at least t a steps ends halted, and a ∈ A exactly when some computation path accepts. A computation path may also end stuck before t a steps; it does not accept.

def Turing.MultiTapeNTM.DecidableInTime {α : Type u_3} (A : Set α) (enc : α ↪ List Bool) (t : α → ℕ) : Prop

Some nondeterministic machine with a binary alphabet and finitely many states decides A within t.

def Turing.MultiTapeNTM.DecidableInPolyTime {α : Type u_3} (A : Set α) (enc : α ↪ List Bool) : Prop

Some nondeterministic machine with a binary alphabet and finitely many states decides A within a time bound polynomial in the length of the encoded instance.

theorem Turing.MultiTapeNTM.DecidesInTime.mono {k : ℕ} {State : Type u_1} {α : Type u_3} {ntm : MultiTapeNTM k Bool State} {enc : α ↪ List Bool} {A : Set α} {t t' : α → ℕ} (h : ntm.DecidesInTime enc A t) (ht : ∀ (a : α), t a ≤ t' a) : ntm.DecidesInTime enc A t'

Time bounds can be increased.

def Turing.MultiTapeNTM.RecognizesInSpace {k : ℕ} {State : Type u_1} {α : Type u_3} (ntm : MultiTapeNTM k Bool State) (enc : α ↪ List Bool) (A : Set α) (s : α → ℕ) : Prop

ntm recognizes A within space s relative to the encoding enc: on every encoded instance enc a, every computation prefix visits at most s a work-tape cells, and a ∈ A exactly when some computation path accepts. No time bound is imposed: a branch may run forever or end stuck, and neither accepts.

theorem Turing.MultiTapeNTM.RecognizesInSpace.mono {k : ℕ} {State : Type u_1} {α : Type u_3} {ntm : MultiTapeNTM k Bool State} {enc : α ↪ List Bool} {A : Set α} {s s' : α → ℕ} (h : ntm.RecognizesInSpace enc A s) (hs : ∀ (a : α), s a ≤ s' a) : ntm.RecognizesInSpace enc A s'

Space bounds can be increased.

def Turing.MultiTapeNTM.DecidesInSpace {k : ℕ} {State : Type u_1} {α : Type u_3} (ntm : MultiTapeNTM k Bool State) (enc : α ↪ List Bool) (A : Set α) (s : α → ℕ) : Prop

ntm decides A within space s relative to the encoding enc: it recognizes A within space s, and every branch halts Sipser, Definition 8.1: on every encoded instance some number of steps bounds every computation path. A path may end stuck before the bound; it does not accept.

theorem Turing.MultiTapeNTM.DecidesInSpace.recognizesInSpace {k : ℕ} {State : Type u_1} {α : Type u_3} {ntm : MultiTapeNTM k Bool State} {enc : α ↪ List Bool} {A : Set α} {s : α → ℕ} (h : ntm.DecidesInSpace enc A s) : ntm.RecognizesInSpace enc A s

A decider within space s recognizes its problem within space s.

theorem Turing.MultiTapeNTM.DecidesInSpace.exists_runsInTime {k : ℕ} {State : Type u_1} {α : Type u_3} {ntm : MultiTapeNTM k Bool State} {enc : α ↪ List Bool} {A : Set α} {s : α → ℕ} (h : ntm.DecidesInSpace enc A s) (a : α) : ∃ (t : ℕ), ntm.RunsInTime (enc a) t

Every branch of a decider halts: on every encoded instance some number of steps bounds every computation path.

theorem Turing.MultiTapeNTM.DecidesInSpace.mono {k : ℕ} {State : Type u_1} {α : Type u_3} {ntm : MultiTapeNTM k Bool State} {enc : α ↪ List Bool} {A : Set α} {s s' : α → ℕ} (h : ntm.DecidesInSpace enc A s) (hs : ∀ (a : α), s a ≤ s' a) : ntm.DecidesInSpace enc A s'

Space bounds can be increased.

theorem Turing.MultiTapeNTM.RunsInTime.runsInSpace {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} {t : ℕ} (h : ntm.RunsInTime input t) : ntm.RunsInSpace input (k * (t + 1))

Space is at most time. Under a time bound t, every computation path visits at most k * (t + 1) work-tape cells: within t steps each head visits at most t + 1 cells, and from step t on the path stays at a halted configuration.

theorem Turing.MultiTapeNTM.DecidesInTime.decidesInSpace {k : ℕ} {State : Type u_1} {α : Type u_3} {ntm : MultiTapeNTM k Bool State} {enc : α ↪ List Bool} {A : Set α} {t : α → ℕ} (h : ntm.DecidesInTime enc A t) : ntm.DecidesInSpace enc A fun (a : α) => k * (t a + 1)

A decider within time t decides within the space it visits in that time, k * (t a + 1), and every branch halts within t a steps.

theorem Turing.MultiTapeTM.ComputesFunInTimeAndSpace.decidesInSpace {k : ℕ} {State : Type u_1} {α : Type u_3} {tm : MultiTapeTM k Bool State} {enc : α ↪ List Bool} {f : α → Bool} {t s : α → ℕ} {A : Set α} (htm : tm.ComputesFunInTimeAndSpace enc encBool f t s) (hA : ∀ (a : α), a ∈ A ↔ f a = true) : tm.DecidesInSpace enc A s

A deterministic decider is a nondeterministic decider with one computation path: a machine computing a Boolean function f within time t and space s decides, as a nondeterministic machine, the problem where f is true within space s. Its only path halts within t a steps, its prefixes and its halted extensions visit no more cells than the run, and it accepts exactly when it halts with output [true].

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_decidesInSpace {α : Type u_3} {enc : α ↪ List Bool} {f : α → Bool} {t s : α → ℕ} {A : Set α} (h : ComputableInTimeAndSpace f enc encBool t s) (hA : ∀ (a : α), a ∈ A ↔ f a = true) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (ntm : MultiTapeNTM k Bool State), ntm.DecidesInSpace enc A s

A Boolean function computable within time t and space s decides the problem where it is true by some nondeterministic machine with a binary alphabet and finitely many states, within space s.