Lax Lean Archive

Polynomial-time substitution of black-box subroutines

Lax218471.Substitution · concepts/Lax218471/Substitution.lean · lax-218471

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.

    Natural Language Statement

    Theorem

    A structured program with a fixed library of polynomial-time subroutines compiles to an ordinary finite stack Turing machine. Every call includes argument transfer, execution of the supplied machine, output transfer, and cleanup of private storage. A bound on source instructions and on every argument and reply yields a polynomial bound on actual machine execution.

    The library is chosen before the input. Its implementations may be supplied existentially by other theorems. Calls may be adaptive and may occur inside loops, provided the execution proof supplies the stated uniform size bound.

    Concept map
    4 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 compile proven

    2 polytime proven

    Lean source view on GitHub

    1import Lax218471.Programs
    2
    3/-!
    4---
    5title: Polynomial-time substitution of black-box subroutines
    6type: theorem
    7---
    8A structured program with a fixed library of polynomial-time subroutines
    9compiles to an ordinary finite stack Turing machine. Every call includes
    10argument transfer, execution of the supplied machine, output transfer, and
    11cleanup of private storage. A bound on source instructions and on every
    12argument and reply yields a polynomial bound on actual machine execution.
    13
    14The library is chosen before the input. Its implementations may be supplied
    15existentially by other theorems. Calls may be adaptive and may occur inside
    16loops, provided the execution proof supplies the stated uniform size bound.
    17-/
    18
    19namespace Lax218471.Substitution
    20
    21open Subroutine Programs PolynomialTime
    22
    23/-- Compilation to a concrete subroutine, with polynomial overhead per source
    24instruction in the maximum call argument and reply length. -/
    25axiom compile {K A σ I : Type} [DecidableEq K] [Fintype A] [Inhabited A]
    26 (R : I → List A → List A → Prop)
    27 (library : ∀ i, Nonempty (Implementation (R i))) (p : Program K A σ I) :
    28 ∃ (r : Routine (fun _ : K => A) σ) (overhead : Polynomial ℕ),
    29 ∀ size s t n, Executes R size p s t n →
    30 ∃ m ≤ n * overhead.eval size, r.Executes s t m
    31
    32/-- The caller's initial or final store, with a single designated data stack. -/
    33def ioStore {K A σ : Type} [DecidableEq K]
    34 (port : K) (initial : σ) (xs : List A) : Store (fun _ : K => A) σ :=
    35 ⟨initial, Function.update (fun _ => []) port xs⟩
    36
    37/-- Polynomially many source instructions and polynomially bounded calls
    38suffice for polynomial-time computation by an actual finite TM2. -/
    39axiom polytime {K A σ I : Type} [DecidableEq K] [Fintype A] [Inhabited A]
    40 [Fintype K] [Fintype σ] {α β : Type}
    41 (R : I → List A → List A → Prop)
    42 (library : ∀ i, Nonempty (Implementation (R i))) (p : Program K A σ I)
    43 (input output : K) (initial : σ) (ea : α → List A) (eb : β → List A) (f : α → β)
    44 (steps size : Polynomial ℕ)
    45 (h : ∀ a, ∃ n ≤ steps.eval (ea a).length,
    46 Executes R (size.eval (ea a).length) p
    47 (ioStore input initial (ea a)) (ioStore output initial (eb (f a))) n) :
    48 Polytime ea eb f
    49
    50end Lax218471.Substitution
    51
    Show ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…