Lax Lean Archive

Polynomial-time implementations of encoded functions and contracts

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

definition

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

    Definition

    Polynomial time is measured in the length of the specified input encoding. An implementation contains an actual finite TM2 and a polynomial time bound. A contract may restrict the valid inputs: callers must establish the contract at every call. This permits direct use of algorithms whose correctness is known only on well-formed encodings.

    Concept map
    1 concept; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Computability.TuringMachine.Computable
    2
    3/-!
    4---
    5title: Polynomial-time implementations of encoded functions and contracts
    6type: definition
    7---
    8Polynomial time is measured in the length of the specified input encoding.
    9An implementation contains an actual finite TM2 and a polynomial time bound.
    10A contract may restrict the valid inputs: callers must establish the contract
    11at every call. This permits direct use of algorithms whose correctness is
    12known only on well-formed encodings.
    13-/
    14
    15namespace Lax218471.PolynomialTime
    16
    17open Turing
    18
    19/-- Existence of a finite machine computing an encoded function in polynomial time. -/
    20def Polytime {α β A B : Type} (ea : α → List A) (eb : β → List B) (f : α → β) : Prop :=
    21 Nonempty (TM2ComputableInPolyTime ea eb f)
    22
    23/-- A finite machine and a time bound realizing every input/output pair of a contract. -/
    24structure Implementation {A : Type} (R : List A → List A → Prop) extends
    25 TM2ComputableAux A A where
    26 time : Polynomial ℕ
    27 correct : ∀ x y, R x y →
    28 Nonempty (TM2OutputsInTime tm (x.map inputAlphabet.symm)
    29 (some (y.map outputAlphabet.symm)) (time.eval x.length))
    30
    31/-- The input/output relation of an encoded function. -/
    32def Graph {α β A : Type} (ea : α → List A) (eb : β → List A) (f : α → β)
    33 (x y : List A) : Prop := ∃ a, ea a = x ∧ eb (f a) = y
    34
    35end Lax218471.PolynomialTime
    36
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…