Single-Tape Nondeterministic Turing Machines (NTMs)

Nondeterministic Turing Machines (NTMs), defined as nondeterministic automata (NA) that act on a bidirectional tape (BiTape).

References

• M. Sipser, Introduction to Theory of Computation

structure Cslib.Computability.Turing.SingleTape.SingleTapeNTM (State : Type u_1) (Symbol : Type u_2) extends Cslib.Automata.NA State (Cslib.Computability.Turing.SingleTape.TrLabel Symbol) : Type (max u_1 u_2)

A (single-tape) Nondeterministic Turing Machine (NTM) is a nondeterministic automaton equipped with a set of accepting halting states.

• Tr : State → Computability.Turing.SingleTape.TrLabel Symbol → State → Prop
• start : Set State
• accept : Set State

  The set of accepting states.

• accept_halting {s : State} (hmem : s ∈ self.accept) : ¬∃ (μ : TrLabel Symbol) (s' : State), self.Tr s μ s'

  Proof that all accepting states are halting states.

def Cslib.Computability.Turing.SingleTape.SingleTapeNTM.Yields {State : Type u_1} {Symbol : Type u_2} [DecidableEq Symbol] (m : SingleTapeNTM State Symbol) (c c' : Cfg State Symbol) : Prop

An NTM yields a small-step operational semantics on configurations, which codifies an execution step. This formalises the 'yields' relation from [Sip13].

Equations

• m.Yields c c' = ∃ (μ : Cslib.Computability.Turing.SingleTape.TrLabel Symbol), m.Tr c.state μ c'.state ∧ Cslib.Computability.Turing.SingleTape.TrLabel.applyToTape (some c.tape) μ = some c'.tape

theorem Cslib.Computability.Turing.SingleTape.SingleTapeNTM.yields_tr {State : Type u_1} {Symbol : Type u_2} [DecidableEq Symbol] {c c' : Cfg State Symbol} {m : SingleTapeNTM State Symbol} : m.Yields c c' ↔ ∃ (μ : TrLabel Symbol), m.Tr c.state μ c'.state ∧ TrLabel.applyToTape (some c.tape) μ = some c'.tape

def Cslib.Computability.Turing.SingleTape.SingleTapeNTM.MYields {State : Type u_1} {Symbol : Type u_2} [DecidableEq Symbol] (m : SingleTapeNTM State Symbol) (a : Cfg State Symbol) : Cfg State Symbol → Prop

Multistep execution of an NTM, defined as the reflexive and transitive closure of one-step execution.

Equations

• m.MYields = Relation.ReflTransGen m.Yields

theorem Cslib.Computability.Turing.SingleTape.SingleTapeNTM.mYields_mTr {State : Type u_1} {Symbol : Type u_2} [DecidableEq Symbol] {c c' : Cfg State Symbol} {m : SingleTapeNTM State Symbol} : m.MYields c c' ↔ ∃ (μs : List (TrLabel Symbol)), m.MTr c.state μs c'.state ∧ List.foldl TrLabel.applyToTape (some c.tape) μs = some c'.tape

Characterisation of executions in terms of multistep transitions.

@[implicit_reducible]

instance Cslib.Computability.Turing.SingleTape.SingleTapeNTM.instAcceptor {State : Type u_1} {Symbol : Type u_2} [DecidableEq Symbol] : Automata.Acceptor (SingleTapeNTM State Symbol) Symbol

An NTM is an acceptor of finite lists of symbols.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.Computability.Turing.SingleTape.SingleTapeNTM.AcceptsInSteps {State : Type u_1} {Symbol : Type u_2} [DecidableEq Symbol] (m : SingleTapeNTM State Symbol) (xs : List Symbol) (n : ℕ) : Prop

The NTM m accepts xs in n execution steps.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.Computability.Turing.SingleTape.SingleTapeNTM.AcceptsInAtMostSteps {State : Type u_1} {Symbol : Type u_2} [DecidableEq Symbol] (m : SingleTapeNTM State Symbol) (xs : List Symbol) (n : ℕ) : Prop

The NTM m accepts xs in at most n execution steps.

Equations

• m.AcceptsInAtMostSteps xs n = ∃ k ≤ n, m.AcceptsInSteps xs k

@[implicit_reducible]

instance Cslib.Computability.Turing.SingleTape.SingleTapeNTM.instTransducer {State : Type u_1} {Symbol : Type u_2} [DecidableEq Symbol] : Automata.Transducer (SingleTapeNTM State Symbol) Symbol Symbol

An NTM is a transducer of finite lists of symbols.

Equations

• One or more equations did not get rendered due to their size.