Lax51.TuringRamPolytimeEquivalence
Polynomial-time equivalence of Turing machines and word RAMs
concepts/Lax51/TuringRamPolytimeEquivalence.lean · lax-51
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Evidence
Each proof establishes this claim relative to its assumptions.
Theorem
Finite multi-tape Turing machines and uniform word random access machines compute exactly the same total functions in polynomial time, when both use the length of the canonical binary encoding as input size and the word RAM is required to have a polynomially bounded sufficient word length.
Concretely, a Turing machine must transform the binary encoding of an input word into the binary encoding of its output in polynomially many Turing steps. A word RAM receives the same semantic input as a native list of numbers, physically prefixed by its length so that the input tape is self-delimiting; one program must return the exact output in polynomially many RAM instructions at every sufficiently large word length, and a polynomial in the encoded input length must suffice to represent the length prefix, all input and output entries, and to make the computation correct.
The claim concerns polynomial-time function computation, commonly called . The usual machine-independence statement for the decision class is its specialization to functions with Boolean-valued output. No fixed polynomial simulation overhead is claimed, only preservation of the class of polynomial-time computable functions.
Lean source view on GitHub
| 1 | import Lax51.RamPolytime |
| 2 | import Lax51.TuringPolytime |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Polynomial-time equivalence of Turing machines and word RAMs |
| 7 | type: theorem |
| 8 | --- |
| 9 | Finite multi-tape Turing machines and uniform word random access machines |
| 10 | compute exactly the same total functions in polynomial time, when both use |
| 11 | the length of the canonical binary encoding as input size and the word RAM |
| 12 | is required to have a polynomially bounded sufficient word length. |
| 13 | |
| 14 | Concretely, a Turing machine must transform the binary encoding of an input |
| 15 | word into the binary encoding of its output in polynomially many Turing |
| 16 | steps. A word RAM receives the same semantic input as a native list of |
| 17 | numbers, physically prefixed by its length so that the input tape is |
| 18 | self-delimiting; one program must return the exact output in polynomially |
| 19 | many RAM instructions at every sufficiently large word length, and a |
| 20 | polynomial in the encoded input length must suffice to represent the length |
| 21 | prefix, all input and output entries, and to make the computation correct. |
| 22 | |
| 23 | The claim concerns polynomial-time function computation, commonly called |
| 24 | `FP`. The usual machine-independence statement for the decision class `P` |
| 25 | is its specialization to functions with Boolean-valued output. No fixed |
| 26 | polynomial simulation overhead is claimed, only preservation of the class |
| 27 | of polynomial-time computable functions. |
| 28 | -/ |
| 29 | |
| 30 | namespace Lax51.TuringRamPolytimeEquivalence |
| 31 | |
| 32 | open Lax51.RamPolytime Lax51.TuringPolytime |
| 33 | |
| 34 | /-- **Polynomial-time machine invariance.** A total function on finite words |
| 35 | is computable in polynomial time by a uniform word RAM with a polynomially |
| 36 | bounded sufficient word length if and only if it is computable in polynomial |
| 37 | time by a finite multi-tape Turing machine. -/ |
| 38 | axiom ramPolytime_iff_turingPolytime (f : List ℕ → List ℕ) : |
| 39 | RamPolytime f ↔ TuringPolytime f |
| 40 | |
| 41 | end Lax51.TuringRamPolytimeEquivalence |
| 42 |
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments