How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
A fixed effective binary encoding of deterministic one-tape Turing machines
Definition
For this page, a coded deterministic one-tape Turing machine is presented in the normalized numeric form where:
- , and the state set is with start state , accept state , and reject state ;
- , and the tape alphabet is with blank symbol ;
- , and the input alphabet is ;
- is a total function where the last coordinate encodes the move direction by
By Deterministic one-tape Turing machines with designated accept and reject states, each such tuple determines a deterministic one-tape Turing machine, and on this page we use this numeric presentation as the machine description to be encoded.
Let denote the usual binary numeral for a natural number , with . List the source pairs in lexicographic order, and for each such pair write The description tuple of is the finite tuple of binary words where and the triples are listed in the same lexicographic source order.
For a binary word , put . For every finite nonempty tuple of binary words define one variable-arity encoder by The first recovers the arity , and the self-delimiting blocks then recover the entries. Different arities have different unary headers, so this single encoder is injective and prefix-free across all finite positive arities; for each fixed arity it is the construction from Finite tuples admit effective prefix-free binary encodings.
The chosen code of , written , is
Its total decoder first parses the unary arity and the indicated self-delimiting blocks. It then checks that every entry is a canonical binary numeral, that the first three entries give , , and , that the arity is , and that every transition triple lies in . If every check succeeds, it returns the unique coded machine determined by those data; otherwise it returns a fixed malformed-code symbol. Thus the chosen machine coding is effective in the sense of Effective binary encodings and total decoders.
Remarks
-
This coding fixes one concrete syntax for machine descriptions. Universality on this page is always relative to that syntax.
-
The coding describes machines, not the partial functions or languages they induce. Different coded machines may still compute the same mathematical function.
Depends on
Used by
- Turing machines admit an effective enumeration Corollary
- Overhead breaks an unrestricted diagonalization claim Counterexample
- A universal Turing machine relative to a fixed machine encoding Definition
- An efficient universal simulation with a clock Definition
- Index sets and extensional properties of Turing-machine languages Definition
- Kleene computation predicate and output map Definition
- Kleene's T-predicate and output function Definition
- The halting problem HALT_TM Definition
- The step-count busy beaver function relative to the chosen machine coding Definition
- The Turing-machine acceptance problem A_TM Definition
- Testing a few short binary strings for machine-code well-formedness Example
- FALSE: diagonalization requires a machine to read its physical source text False statement
- FALSE: every countable language is decidable False statement
- False: unrestricted diagonalization respects any resource bound False statement
- A constructible time bound yields a uniformly clocked simulator Lemma
- A fixed interpreter can execute one encoded machine step Lemma
- A hypothetical decider for A_TM yields a diagonal self-application machine Lemma
- A nontrivial extensional property admits a uniform witness machine construction Lemma
- Accepting computation histories can be encoded by modified-PCP domino matches Lemma
- Effective enumeration of clocked machines Lemma
- Prefix program codes admit linear nondeterministic universal simulation Lemma
- Space-bounded universal simulation Lemma
- The chosen machine coding is injective and has a total decoder Lemma
- The one-step update on coded Turing configurations is primitive recursive Lemma
- The fixed machine coding gives an acceptable numbering Proposition
- Well-formed deterministic one-tape Turing machine descriptions form a decidable language Proposition
- A universal simulator can realize T steps with machine-dependent O(T log T) overhead Theorem
- Clocked universal simulation with time and space bounds Theorem
- Halting on every input is not recognizable Theorem
- Language equivalence of Turing machines is undecidable Theorem
- Recognizable extensional properties are positively witnessed by finite information Theorem
- The busy beaver function eventually dominates every total computable function Theorem
- The halting problem is recognizable and undecidable Theorem
- The nonhalting set is productive and the halting set is creative Theorem
- The Turing-machine acceptance problem is computably enumerable complete Theorem
- The Turing-machine acceptance problem is recognizable Theorem
- The Turing-machine acceptance problem is undecidable Theorem
Dependency tree · two levels
7 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Richard Zach, Sets, Logic, Computation: An Open Introduction to Metalogic (standard reference, not scraped)
- Michael Sipser, MIT 18.404J Theory of Computation, Lecture 6: TM Variants, Church-Turing Thesis (standard reference, not scraped)