Nondeterministic Turing machines

11 fully proved

Single Tape NTM

TheoremAcceptance as a label list#✓fully proved

A single-tape nondeterministic Turing machine \(m\) accepts a word \(x\) if and only if there is a list \(\mu\) of transition labels (read a symbol, write a symbol, move, skip) such that applying the labels of \(\mu\) in order to the input tape of \(x\) (the tape holding \(x\) from the head cell rightward, every other cell blank) never fails, that is, every read label finds its symbol in the cell under the head, and \(\mu\) leads the automaton of \(m\) from some start state to some accepting state.

theorem accepts_iff_exists_labels {xs : List Symbol} :
    Acceptor.Accepts m xs ↔ ∃ μs : List (TrLabel Symbol),
      (μs.foldl applyToTape (some (BiTape.mk₁ xs))).isSome ∧
        ∃ s ∈ m.start, ∃ s' ∈ m.accept, m.MTr s μs s'

Used by 2

Used byAcceptance is closed under extension on the right · Acceptance by an NTM with finite state and tape alphabets is r.e

TheoremAcceptance is closed under extension on the right#✓fully proved

If a single-tape nondeterministic Turing machine \(m\) accepts a word \(x\) over its tape alphabet, then \(m\) accepts \(xy\) for every word \(y\) over that alphabet.

This is a defect of CSLib's definition of these machines: a transition can only test the cell under the head for a symbol, never for a blank, so every cell that an accepting run on \(x\) reads holds a letter of \(x\) or one the run wrote, and the same run accepts \(xy\).

theorem accepts_append {xs : List Symbol} (ys : List Symbol) (h : Acceptor.Accepts m xs) :
    Acceptor.Accepts m (xs ++ ys)

Sources

• defect of the pinned CSLib definition, fixed upstream by leanprover/cslib#1039.

Uses 1 · Used by 1

Proof usesAcceptance as a label list

Used byAn NTM that accepts the empty word accepts every word

TheoremAn NTM that accepts the empty word accepts every word#✓fully proved

If a single-tape nondeterministic Turing machine \(m\) accepts the empty word, then \(m\) accepts every word over its tape alphabet.

This is a special case of acceptance being closed under extension on the right, a defect of CSLib's definition of these machines.

theorem accepts_of_accepts_nil (xs : List Symbol) (h : Acceptor.Accepts m []) :
    Acceptor.Accepts m xs

Uses 1 · Used by 1

Proof usesAcceptance is closed under extension on the right

Used byNo NTM accepts exactly the binary code of \(0\)

TheoremNo NTM accepts exactly the binary code of \(0\)#✓fully proved

Let \(m\) be a single-tape nondeterministic Turing machine with tape alphabet \(\Sigma\), and let \(\iota\) be any map from the bits to \(\Sigma\). For a natural number \(n\), write \(w_n\) for the word over \(\Sigma\) obtained by applying \(\iota\) letter by letter to the little-endian binary code of \(n\), in which \(0\) is coded by the empty word. Then it is not the case that, for every natural number \(n\), \(m\) accepts \(w_n\) if and only if \(n = 0\).

The word \(w_0\) is empty, and a machine that accepts the empty word accepts every word, in particular \(w_1\).

theorem not_forall_accepts_encodeNat_iff_eq_zero (ι : Bool → Symbol) :
    ¬∀ n : ℕ, Acceptor.Accepts m ((encodeNat n).map ι) ↔ n = 0

Uses 1 · Used by 1

Proof usesAn NTM that accepts the empty word accepts every word

Used byNo single-tape NTM recognizes \(n = 0\)

TheoremAcceptance by an NTM with finite state and tape alphabets is r.e#✓fully proved

Acceptance by an NTM with finite state and tape alphabets is r.e. in the input word (Sipser, Theorem 3.16, through recursion theory): search for a label list that applies to the input tape, checked on coded tapes, and along which the image of the start states, a finite set, meets the accepting states.

theorem rePred_accepts [Finite State] [Finite Symbol] [Primcodable Symbol] :
    REPred fun xs : List Symbol ↦ Acceptor.Accepts m xs

Uses 8 · Used by 3

Proof usesAcceptance as a label list · Pushing a cell onto a coded tape · Pushing a cell onto a coded tape is primitive recursive · The head of a stack tape is the first entry of its list · Pushing onto a stack tape, on cell lists · Tail of a stack tape, on cell lists · Existential projection preserves recursive enumerability · Joint primitive recursion over a finite first argument

Used byA predicate recognized by a single-tape NTM is recognized by a deterministic single-tape machine · Deterministic machines recognize NTM acceptance · Deterministic machines recognize NTM acceptance along a computable map

Decidability

TheoremDeterministic machines recognize NTM acceptance#✓fully proved

Let \(m\) be a single-tape nondeterministic Turing machine with a finite set of states and a finite tape alphabet \(\Sigma\) that has decidable equality and a primitive recursive encoding. Then the predicate on words over \(\Sigma\) that holds at a word exactly when \(m\) accepts it is recognizable by a single-tape deterministic Turing machine.

theorem singleTapeRecognizable_accepts :
    SingleTapeRecognizable fun xs : List Symbol ↦ Acceptor.Accepts m xs

Sources

• Sipser, Theorem 3.16.

Uses 3

Statement usesPredicates recognizable by a single-tape Turing machine

Proof usesAcceptance by an NTM with finite state and tape alphabets is r.e · Single-tape recognizable predicates are exactly the r.e. predicates

TheoremDeterministic machines recognize NTM acceptance along a computable map#✓fully proved

Let \(m\) be a single-tape nondeterministic Turing machine with a finite set of states and a finite tape alphabet \(\Sigma\) that has decidable equality and a primitive recursive encoding. Let \(\alpha\) be a primitively encodable type and \(f\) a computable map from \(\alpha\) to words over \(\Sigma\). Then the predicate on \(\alpha\) that holds at \(a\) exactly when \(m\) accepts \(f(a)\) is recognizable by a single-tape deterministic Turing machine.

theorem singleTapeRecognizable_accepts_comp {α : Type*} [Primcodable α] {f : α → List Symbol}
    (hf : Computable f) : SingleTapeRecognizable fun a ↦ Acceptor.Accepts m (f a)

Sources

• Sipser, Theorem 3.16.

Uses 3

Statement usesPredicates recognizable by a single-tape Turing machine

Proof usesAcceptance by an NTM with finite state and tape alphabets is r.e · Single-tape recognizable predicates are exactly the r.e. predicates

DefinitionPredicates recognizable by a single-tape nondeterministic machine#✓fully proved

Let \(\alpha\) be a type with a primitive recursive encoding into \(\mathbb{N}\). A predicate \(p\) on \(\alpha\) is recognizable by a single-tape nondeterministic machine when there are a finite set of states, a finite tape alphabet \(\Sigma\) with decidable equality, an injective map \(\iota\) from the bits \(\{0, 1\}\) to \(\Sigma\) and a single-tape nondeterministic Turing machine \(M\) with these states over \(\Sigma\) such that for every \(a \in \alpha\), \(M\) accepts the input word obtained by writing the binary encoding of the code of \(a\) in \(\mathbb{N}\) letter by letter through \(\iota\) if and only if \(p(a)\) holds. Here \(M\) accepts a word when some run of \(M\) from one of its start states on the tape holding the word, with the head on its first symbol, reaches an accepting state.

In this model a machine cannot test whether a cell is blank, so a machine that accepts a word accepts every extension of the word on the right. Every such predicate is recognizable by a single-tape deterministic machine, but not conversely: the predicate \(n = 0\) on \(\mathbb{N}\) is decidable by a single-tape deterministic machine and is not recognizable by a single-tape nondeterministic machine.

def SingleTapeNTMRecognizable (p : α → Prop) : Prop :=
  ∃ (State Symbol : Type) (_ : Fintype State) (_ : Fintype Symbol) (_ : DecidableEq Symbol)
    (ι : Bool → Symbol), Function.Injective ι ∧ ∃ m : SingleTapeNTM State Symbol,
      ∀ a, Acceptor.Accepts m ((encodeNat (encode a)).map ι) ↔ p a

Sources

• the pinned CSLib definition of nondeterministic machines; the upstream PR leanprover/cslib#1039 lets machines read and write blank cells.

Used by 3

Used byA decidable predicate that no single-tape NTM recognizes · No single-tape NTM recognizes \(n = 0\) · A predicate recognized by a single-tape NTM is recognized by a deterministic single-tape machine

TheoremA predicate recognized by a single-tape NTM is recognized by a deterministic single-tape machine#✓fully proved

A predicate recognized by a single-tape NTM is recognized by a deterministic single-tape machine (Sipser, Theorem 3.16, through recursion theory).

theorem SingleTapeNTMRecognizable.singleTapeRecognizable (h : SingleTapeNTMRecognizable p) :
    SingleTapeRecognizable p

Uses 5

Statement usesPredicates recognizable by a single-tape nondeterministic machine · Predicates recognizable by a single-tape Turing machine

Proof usesAcceptance by an NTM with finite state and tape alphabets is r.e · Single-tape recognizable predicates are exactly the r.e. predicates · Binary codes of natural numbers in a tape alphabet are primitive recursive

TheoremNo single-tape NTM recognizes \(n = 0\)#✓fully proved

The predicate \(n = 0\) on the natural numbers is not recognizable by any single-tape nondeterministic Turing machine.

The binary code of \(0\) is the empty word, and a single-tape nondeterministic machine that accepts the empty word accepts every word.

theorem not_singleTapeNTMRecognizable_eq_zero :
    ¬SingleTapeNTMRecognizable fun n : ℕ ↦ n = 0

Sources

• defect of the pinned CSLib definition, fixed upstream by leanprover/cslib#1039.

Uses 2 · Used by 1

Statement usesPredicates recognizable by a single-tape nondeterministic machine

Proof usesNo NTM accepts exactly the binary code of \(0\)

Used byA decidable predicate that no single-tape NTM recognizes

TheoremA decidable predicate that no single-tape NTM recognizes#✓fully proved

There is a predicate \(p\) on the natural numbers that is decidable by a single-tape deterministic Turing machine but is not recognizable by any single-tape nondeterministic Turing machine.

The predicate \(n = 0\) is such a predicate.

theorem exists_singleTapeDecidable_not_singleTapeNTMRecognizable :
    ∃ p : ℕ → Prop, SingleTapeDecidable p ∧ ¬SingleTapeNTMRecognizable p

Sources

• Sipser, Corollary 3.18, whose half "every Turing-recognizable language is recognized by a nondeterministic machine" fails on the pinned CSLib definition; fixed upstream by leanprover/cslib#1039.

Uses 4

Statement usesPredicates decidable by a single-tape Turing machine · Predicates recognizable by a single-tape nondeterministic machine

Proof usesNo single-tape NTM recognizes \(n = 0\) · Single-tape decidable predicates are exactly the computable predicates

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.