Lax51.RamPolytime
Polynomial-time computation by a word RAM
concepts/Lax51/RamPolytime.lean · lax-51
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
A total function from finite lists of natural numbers to finite lists of natural numbers is computable in polynomial time by a word RAM when there are one uniform program, a polynomial word-length bound, and a polynomial running-time bound with the following property.
For an input whose canonical binary encoding has length n, the RAM receives the physical tape . Every tape and output entry fits in a word of the bounded length, and at every word length at least that bound the program returns the exact output within the bounded number of RAM instructions. Both polynomials are evaluated at n.
Measuring input size in bits, rather than in the number of entries, puts the RAM and Turing machine on the same input-size scale. Requiring correctness at every sufficiently large word length makes the program uniform in the word length. Requiring a polynomial sufficient word length is what permits a Turing machine to simulate each operation on a word in polynomial time. No lower bound such as logarithmic word length is separately necessary: the explicit fitting condition says directly that the length prefix, all native input entries, and all exact output entries are representable.
Lean source view on GitHub
| 1 | import Lax13.Ram |
| 2 | import Lax51.BinaryWordEncoding |
| 3 | import Mathlib.Algebra.Polynomial.Eval.Defs |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Polynomial-time computation by a word RAM |
| 8 | type: definition |
| 9 | --- |
| 10 | A total function from finite lists of natural numbers to finite lists of |
| 11 | natural numbers is computable in polynomial time by a word RAM when there |
| 12 | are one uniform program, a polynomial word-length bound, and a polynomial |
| 13 | running-time bound with the following property. |
| 14 | |
| 15 | For an input whose canonical binary encoding has length *n*, the RAM receives |
| 16 | the physical tape `x.length :: x`. Every tape and output entry fits in a word |
| 17 | of the bounded length, and at every word length at least that bound the program |
| 18 | returns the exact output within the bounded number of RAM instructions. Both |
| 19 | polynomials are evaluated at *n*. |
| 20 | |
| 21 | Measuring input size in bits, rather than in the number of entries, puts the |
| 22 | RAM and Turing machine on the same input-size scale. Requiring correctness |
| 23 | at every sufficiently large word length makes the program uniform in the |
| 24 | word length. Requiring a polynomial sufficient word length is what permits |
| 25 | a Turing machine to simulate each operation on a word in polynomial time. |
| 26 | No lower bound such as logarithmic word length is separately necessary: |
| 27 | the explicit fitting condition says directly that the length prefix, all |
| 28 | native input entries, and all exact output entries are representable. |
| 29 | -/ |
| 30 | |
| 31 | namespace Lax51.RamPolytime |
| 32 | |
| 33 | open Lax13.Ram |
| 34 | open Lax51.BinaryWordEncoding |
| 35 | |
| 36 | /-- Every entry of `x` is representable by a word of `w` bits. -/ |
| 37 | def FitsInWords (w : ℕ) (x : List ℕ) : Prop := |
| 38 | ∀ a ∈ x, a < 2 ^ w |
| 39 | |
| 40 | /-- Polynomial-time computation by one uniform word-RAM program, measured |
| 41 | in the bit-size of the logical word-list input. The physical input tape is |
| 42 | length-prefixed, so a program can consume exactly the logical input and then |
| 43 | continue computing even though the underlying RAM's exhausted-input behavior |
| 44 | is an unconditional halt. -/ |
| 45 | def RamPolytime (f : List ℕ → List ℕ) : Prop := |
| 46 | ∃ (p : Program) (wordBound timeBound : Polynomial ℕ), |
| 47 | ∀ x : List ℕ, |
| 48 | FitsInWords (wordBound.eval (bitSize x)) ((x.length :: x) ++ f x) ∧ |
| 49 | ∀ w : ℕ, wordBound.eval (bitSize x) ≤ w → |
| 50 | ∃ t ≤ timeBound.eval (bitSize x), |
| 51 | RunsTo w p (x.length :: x) (f x) t |
| 52 | |
| 53 | end Lax51.RamPolytime |
| 54 |
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