Multi-tape machines decide only recursive predicates

DefinitionDecidability by multi-tape machines#✓fully proved

Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). A predicate \(p\) on \(\alpha\) is decidable by a multi-tape machine when there are a number \(k\) and a deterministic Turing machine \(M\) with finitely many states, a read-only input tape, \(k\) work tapes and a write-only output tape, all over the Boolean alphabet, such that for every \(a \in \alpha\) there is a Boolean \(b\) for which \(M\) computes the one-letter word \(b\) on the binary word of \(\mathrm{encode}(a)\) (least significant bit first), and \(b\) is true exactly when \(p(a)\) holds. Here \(M\) computes a word \(v\) on an input word \(w\) when its run started on \(w\) halts with \(v\) on its output tape.

def MultiTapeDecidable (p : α → Prop) : Prop :=
  ∃ (k : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State),
    ∀ a, ∃ b : Bool, tm.Computes (encodeNat (encode a)) [b] ∧ (b = true ↔ p a)

Used by 4

Used byA predicate decided by a multi-tape machine is computable · Multi-tape machines decide no more than multi-stack machines · A predicate decided by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine has a recursively enumerable complement

DefinitionRecognizability by multi-tape machines#✓fully proved

Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). A predicate \(p\) on \(\alpha\) is recognizable by a multi-tape machine when there are a number \(k\) and a deterministic Turing machine \(M\) with finitely many states, a read-only input tape, \(k\) work tapes and a write-only output tape, all over the Boolean alphabet, such that for every \(a \in \alpha\), the run of \(M\) started on the binary word of \(\mathrm{encode}(a)\) (least significant bit first) halts if and only if \(p(a)\) holds.

def MultiTapeRecognizable (p : α → Prop) : Prop :=
  ∃ (k : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State),
    ∀ a, (∃ o, tm.Computes (encodeNat (encode a)) o) ↔ p a

Used by 3

Used byCo-recognizability by multi-tape machines · Multi-tape machines recognize no more than multi-stack machines · A predicate recognizable by a multi-tape machine is recursively enumerable

DefinitionCo-recognizability by multi-tape machines#✓fully proved

Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). A predicate \(p\) on \(\alpha\) is co-recognizable by a multi-tape machine when its complement \(\neg p\) is recognizable by a multi-tape machine.

def MultiTapeCoRecognizable (p : α → Prop) : Prop :=
  MultiTapeRecognizable fun a ↦ ¬p a

Uses 1

Statement usesRecognizability by multi-tape machines

TheoremA predicate recognizable by a multi-tape machine is recursively enumerable#✓fully proved

Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). If a predicate \(p\) on \(\alpha\) is recognizable by a multi-tape machine, then \(p\) is recursively enumerable, that is, the partial function on \(\alpha\) that is defined, with a trivial value, exactly where \(p\) holds is partial recursive.

theorem MultiTapeRecognizable.rePred (h : MultiTapeRecognizable p) : REPred p

Uses 15 · Used by 1

Statement usesRecognizability by multi-tape machines

Proof usesCodes for multi-tape machines · A code computes exactly what its clocked evaluator returns · Multi-tape codes as tables · Clocked evaluator · Every finite-state machine has a code · The evaluator is primitive recursive · The multi-tape machine of a code · Coded actions · Coded actions as tuples · Keys of a code's table · Simulation up to a state relabelling · Relabelling preserves what a machine computes · Existential projection preserves recursive enumerability · Binary encoding, least significant bit first

Used byMulti-tape machines recognize no more than multi-stack machines

TheoremA predicate decided by a multi-tape machine is recursively enumerable#✓fully proved

Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). If a predicate \(p\) on \(\alpha\) is decidable by a multi-tape machine, then \(p\) is recursively enumerable, that is, the partial function on \(\alpha\) that is defined, with a trivial value, exactly where \(p\) holds is partial recursive.

theorem MultiTapeDecidable.rePred (h : MultiTapeDecidable p) : REPred p

Uses 16 · Used by 1

Statement usesDecidability by multi-tape machines

Proof usesCodes for multi-tape machines · A code computes exactly what its clocked evaluator returns · Multi-tape codes as tables · Clocked evaluator · Every finite-state machine has a code · The evaluator is primitive recursive · The multi-tape machine of a code · Coded actions · Coded actions as tuples · Keys of a code's table · Simulation up to a state relabelling · Relabelling preserves what a machine computes · Output determinism · Existential projection preserves recursive enumerability · Binary encoding, least significant bit first

Used byA predicate decided by a multi-tape machine is computable

TheoremA predicate decided by a multi-tape machine has a recursively enumerable complement#✓fully proved

Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). If a predicate \(p\) on \(\alpha\) is decidable by a multi-tape machine, then its complement \(\neg p\) is recursively enumerable, that is, the partial function on \(\alpha\) that is defined, with a trivial value, exactly where \(\neg p\) holds is partial recursive.

theorem MultiTapeDecidable.rePred_not (h : MultiTapeDecidable p) :
    REPred fun a ↦ ¬p a

Uses 16 · Used by 1

Statement usesDecidability by multi-tape machines

Proof usesCodes for multi-tape machines · A code computes exactly what its clocked evaluator returns · Multi-tape codes as tables · Clocked evaluator · Every finite-state machine has a code · The evaluator is primitive recursive · The multi-tape machine of a code · Coded actions · Coded actions as tuples · Keys of a code's table · Simulation up to a state relabelling · Relabelling preserves what a machine computes · Output determinism · Existential projection preserves recursive enumerability · Binary encoding, least significant bit first

Used byA predicate decided by a multi-tape machine is computable

TheoremA predicate decided by a multi-tape machine is computable#✓fully proved

Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). If a predicate \(p\) on \(\alpha\) is decidable by a multi-tape machine, then \(p\) is computable, that is, \(p\) is decidable and its Boolean characteristic function \(\alpha \to \mathrm{Bool}\) is computable.

This is Post's theorem applied to \(p\) and its complement, both recursively enumerable.

theorem MultiTapeDecidable.computablePred (h : MultiTapeDecidable p) : ComputablePred p

Uses 3 · Used by 1

Statement usesDecidability by multi-tape machines

Proof usesA predicate decided by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine has a recursively enumerable complement

Used byMulti-tape machines decide no more than multi-stack machines

TheoremMulti-tape machines decide no more than multi-stack machines#✓fully proved

Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). Every predicate on \(\alpha\) that is decidable by a multi-tape machine is decidable by a multi-stack machine.

theorem multiTapeDecidable_implies_tm2Decidable (h : MultiTapeDecidable p) :
    TM2Decidable p

Uses 4

Statement usesDecidability by multi-tape machines · Decidability by multi-stack machines

Proof usesA predicate decided by a multi-tape machine is computable · Multi-stack decidable predicates are exactly the computable predicates

TheoremMulti-tape machines recognize no more than multi-stack machines#✓fully proved

Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). Every predicate on \(\alpha\) that is recognizable by a multi-tape machine is recognizable by a multi-stack machine.

theorem multiTapeRecognizable_implies_tm2Recognizable (h : MultiTapeRecognizable p) :
    TM2Recognizable p

Uses 4

Statement usesRecognizability by multi-tape machines · Recognizability by multi-stack machines

Proof usesA predicate recognizable by a multi-tape machine is recursively enumerable · Multi-stack recognizable predicates are exactly the r.e. predicates

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.