Lax Lean Archive

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

Lax51.TuringToRamGenericTime

Generic-time simulation of Turing machines by word RAMs

concepts/Lax51/TuringToRamGenericTime.lean · lax-51

proven

Loading review…

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

    Evidence

    Each proof establishes this claim relative to its assumptions.

    Theorem

    A finite multi-tape Turing-machine computation with an arbitrary numerical per-input running-time bound can be simulated by one uniform word-RAM program. Both the sufficient word length and the RAM running time have fixed polynomial overhead in the encoded input size plus the supplied Turing running time.

    No regularity assumption is made on the running-time function: it need not be polynomial, monotone, or computable. The result is therefore a generic quantitative simulation theorem. Computability and polynomial-time preservation follow by separately imposing the corresponding regularity on the supplied bound.

    Lean source view on GitHub

    1import Lax13.Ram
    2import Lax51.BinaryWordEncoding
    3import Mathlib.Algebra.Polynomial.Eval.Defs
    4import Mathlib.Computability.TuringMachine.Computable
    5
    6/-!
    7---
    8title: Generic-time simulation of Turing machines by word RAMs
    9type: theorem
    10---
    11A finite multi-tape Turing-machine computation with an arbitrary numerical
    12per-input running-time bound can be simulated by one uniform word-RAM
    13program. Both the sufficient word length and the RAM running time have
    14fixed polynomial overhead in the encoded input size plus the supplied
    15Turing running time.
    16
    17No regularity assumption is made on the running-time function: it need not
    18be polynomial, monotone, or computable. The result is therefore a generic
    19quantitative simulation theorem. Computability and polynomial-time
    20preservation follow by separately imposing the corresponding regularity on
    21the supplied bound.
    22-/
    23
    24namespace Lax51.TuringToRamGenericTime
    25
    26open Lax13.Ram
    27open Lax51.BinaryWordEncoding
    28open Polynomial Turing
    29
    30/-- A finite Turing machine with an arbitrary per-input numerical
    31running-time bound compiles to one uniform word-RAM program. The sufficient
    32word length and RAM running time are fixed polynomials in the input bit-size
    33plus that bound. -/
    34axiom turingWithInputTime_to_ramInPolynomialOverhead
    35 {f : List ℕ → List ℕ}
    36 (H : TM2ComputableAux Symbol Symbol) (time : List ℕ → ℕ)
    37 (hrun : ∀ x, TM2OutputsInTime H.tm
    38 (List.map H.inputAlphabet.invFun (encode x))
    39 (some (List.map H.outputAlphabet.invFun (encode (f x)))) (time x)) :
    40 ∃ (p : Program) (wordOverhead timeOverhead : Polynomial ℕ),
    41 ∀ (x : List ℕ) (w : ℕ),
    42 wordOverhead.eval (bitSize x + time x) ≤ w →
    43 ∃ t ≤ timeOverhead.eval (bitSize x + time x),
    44 RunsTo w p (x.length :: x) (f x) t
    45
    46end Lax51.TuringToRamGenericTime
    47
    Show Proof

    Builds on

    Used by

    none

    From Mathlib

    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…