Lax Lean Archive

Composition of polynomial-time algorithms

Lax218471.Combinators · concepts/Lax218471/Combinators.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

    Encoded polynomial-time functions can be used through their existential machine witnesses. Their outputs have polynomially bounded encoded size, and composition preserves polynomial time. All size measures refer to the specified encodings; the intermediate encoding is shared by both algorithms.

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

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

    1 comp proven

    2 graph_realizable proven

    3 output_size proven

    Lean source view on GitHub

    1import Lax218471.PolynomialTime
    2
    3/-!
    4---
    5title: Composition of polynomial-time algorithms
    6type: theorem
    7---
    8Encoded polynomial-time functions can be used through their existential
    9machine witnesses. Their outputs have polynomially bounded encoded size,
    10and composition preserves polynomial time. All size measures refer to the
    11specified encodings; the intermediate encoding is shared by both algorithms.
    12-/
    13
    14namespace Lax218471.Combinators
    15
    16open PolynomialTime
    17
    18/-- Every polynomial-time function has polynomially bounded output size. -/
    19axiom output_size {α β A B : Type} {ea : α → List A} {eb : β → List B} {f : α → β}
    20 (h : Polytime ea eb f) :
    21 ∃ p : Polynomial ℕ, ∀ a, (eb (f a)).length ≤ p.eval (ea a).length
    22
    23/-- An existential polynomial-time algorithm realizes its encoded contract. -/
    24axiom graph_realizable {α β A : Type} {ea : α → List A} {eb : β → List A} {f : α → β}
    25 (h : Polytime ea eb f) : Nonempty (Implementation (Graph ea eb f))
    26
    27/-- Sequential composition of algorithms supplied only by existence statements. -/
    28axiom comp {α β γ A : Type} [Fintype A] [Inhabited A]
    29 {ea : α → List A} {eb : β → List A} {ec : γ → List A}
    30 {f : α → β} {g : β → γ} (hf : Polytime ea eb f) (hg : Polytime eb ec g) :
    31 Polytime ea ec (g ∘ f)
    32
    33end Lax218471.Combinators
    34
    Show ProofShow 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…