Nondeterministic Multi-Tape Turing Machines

Defines nondeterministic Turing machines with a read-only input tape, k work tapes and one write-only output tape, and what it means for one to compute an output within a time and space bound.

Design

Following [Pap94], chapter 2.7, a nondeterministic machine is a Turing machine whose transition function is replaced by a transition relation: Tr q input work action holds when action is one of the actions permitted in that situation.

A halted configuration steps to itself, so once a machine has halted it has a run of every length. A time bound is therefore an upper bound, with no separate account of the step at which it halted.

The transition relation may be empty at a running configuration, so a machine can get stuck. Every notion below asks for a computation ending in a halted configuration, so a stuck one is not a witness.

Important Declarations

• MultiTapeNTM: the machine, an initial state and a transition relation
• Step: the one-step relation on configurations
• ComputationPath: a run of the machine: a series of configurations from the initial one, each reached from the previous by a step
• ComputesSuchThat: some computation halts, emits a given output and meets a given constraint
• Computes, ComputesInExactTime, ComputesInExactSpace, ComputesInExactTimeAndSpace: its instances, whose bounds all refer to a single computation

References

• C. Papadimitriou, Computational Complexity
• M. Sipser, Introduction to the Theory of Computation

structure Turing.MultiTapeNTM (k : ℕ) (Symbol : Type u_3) (State : Type u_4) : Type (max u_3 u_4)

A nondeterministic multi-tape Turing machine with k work tapes over the alphabet of Option Symbol (where none is the blank symbol). Neither Symbol nor State is required to be finite.

• q₀ : State

  initial state

• Tr (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) (action : Action k Symbol State) : Prop

  transition relation: which combinations of state, current input symbol, tuple of work head symbols and resulting actions are valid transitions

def Turing.MultiTapeNTM.Step {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (ntm : MultiTapeNTM k Symbol State) (c₁ c₂ : Cfg k Symbol State input) : Prop

The one-step relation on configurations. A halted configuration steps to itself; a running one steps by any permitted transition.

Equations

• ntm.Step c₁ c₂ = match c₁.state with | none => c₂ = c₁ | some q => ∃ (action : Turing.Action k Symbol State), ntm.Tr q c₁.inputSymbol c₁.workTapeSymbols action ∧ c₂ = action.apply c₁

theorem Turing.MultiTapeNTM.step_of_halt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} {c c' : Cfg k Symbol State input} (h : c.Halted) : ntm.Step c c' ↔ c' = c

A halted configuration steps only to itself.

def Turing.MultiTapeNTM.initCfg {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) : Cfg k Symbol State input

The initial configuration corresponding to an input string.

Equations

• ntm.initCfg input = Turing.Cfg.init ntm.q₀ input

structure Turing.MultiTapeNTM.ComputationPath {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) : Type (max u_1 u_2)

A computation path of ntm on input: the configurations it passes through, forming a chain of steps from the initial configuration to the one it ends at.

• cfgs : List (Cfg k Symbol State input)

  the configurations passed through, starting with the initial one

• last : Cfg k Symbol State input

  the configuration the path ends at

• isChainFromTo : List.IsChainFromTo ntm.Step self.cfgs (ntm.initCfg input) self.last

  consecutive configurations are joined by a step, from the initial configuration to last

def Turing.MultiTapeNTM.ComputationPath.time {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {ntm : MultiTapeNTM k Symbol State} {input : List Symbol} (p : ntm.ComputationPath input) : ℕ

The number of steps taken, the time the computation takes.

Equations

• p.time = p.cfgs.length - 1

def Turing.MultiTapeNTM.ComputationPath.space {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {ntm : MultiTapeNTM k Symbol State} {input : List Symbol} (p : ntm.ComputationPath input) : ℕ

The number of work tape cells touched.

Equations

• p.space = Turing.spaceUsedOfCfgs p.cfgs

def Turing.MultiTapeNTM.ComputesSuchThat {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) (P : ntm.ComputationPath input → Prop) : Prop

ntm has a computation on input that starts at the initial configuration, halts, emits output and satisfies P. The notions below are its instances, so their constraints all refer to a single computation.

Equations

• ntm.ComputesSuchThat input output P = ∃ (p : ntm.ComputationPath input), p.last.Halted ∧ p.last.output = output ∧ P p

def Turing.MultiTapeNTM.Computes {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) : Prop

ntm computes output from input, with no bound on resources.

Equations

• ntm.Computes input output = ntm.ComputesSuchThat input output fun (x : ntm.ComputationPath input) => True

def Turing.MultiTapeNTM.ComputesInExactTime {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) (t : ℕ) : Prop

ntm computes output from input in exactly t steps.

Equations

• ntm.ComputesInExactTime input output t = ntm.ComputesSuchThat input output fun (p : ntm.ComputationPath input) => p.time = t

def Turing.MultiTapeNTM.ComputesInExactSpace {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) (s : ℕ) : Prop

ntm computes output from input touching exactly s work tape cells.

Equations

• ntm.ComputesInExactSpace input output s = ntm.ComputesSuchThat input output fun (p : ntm.ComputationPath input) => p.space = s

def Turing.MultiTapeNTM.ComputesInExactTimeAndSpace {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) (t s : ℕ) : Prop

ntm computes output from input in t steps and s work tape cells, by a single computation. Nondeterministic analogue of MultiTapeTM.ComputesInTimeAndSpace.

Equations

• ntm.ComputesInExactTimeAndSpace input output t s = ntm.ComputesSuchThat input output fun (p : ntm.ComputationPath input) => p.time = t ∧ p.space = s