Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax51.RamPolytime

Polynomial-time computation by a word RAM

concepts/Lax51/RamPolytime.lean · lax-51

definition

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    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 x.length::xx.length :: x. 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

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

    Loading discussion…