Lax Lean Archive

Running time

Lax213208.RunningTime · concepts/Lax213208/RunningTime.lean · lax-213208

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

    RunsInTimealginputsTRunsInTime alg inputs T asserts termination within T(n)T(n) instructions, where nn is the binary size of the instance. The bound also supplies a sufficient word width in bits. It says nothing about solution quality.

    Polynomial, quasipolynomial, and subexponential time are independent of approximation ratios. Subexponential time means 2o(n)2^{o(n)}: for every δ>0\delta>0, a bound c 2⌈δn⌉c\,2^{\lceil\delta n\rceil} holds.

    Concept map
    11 concepts; 5 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax213208.AlgorithmInput
    2import Lax213208.Programs
    3import Mathlib.Data.Nat.Log
    4import Mathlib.Data.Real.Archimedean
    5
    6/-!
    7---
    8title: Running time
    9type: definition
    10---
    11`RunsInTime alg inputs T` asserts termination within T(n)T(n) instructions,
    12where nn is the binary size of the instance. The bound also supplies a
    13sufficient word width in bits. It says nothing about solution quality.
    14
    15Polynomial, quasipolynomial, and subexponential time are independent of
    16approximation ratios. Subexponential time means 2o(n)2^{o(n)}: for every
    17δ>0\delta>0, a bound c 2⌈δn⌉c\,2^{\lceil\delta n\rceil} holds.
    18-/
    19
    20namespace Lax213208.RunningTime
    21
    22open OptimizationProblem AlgorithmInput Programs
    23
    24variable {Instance Solution : Type*} {problem : Problem Instance Solution}
    25
    26def RunsInTime (alg : Program) (inputs : Set Instance) (time : ℕ → ℕ)
    27 (precision : Option ℕ := none) : Prop :=
    28 ∀ x ∈ inputs, ∃ output,
    29 RunsWithin alg (inputTape problem precision x) output (time (inputSize problem x))
    30
    31def PolynomialTime (alg : Program) (inputs : Set Instance)
    32 (precision : Option ℕ := none) : Prop :=
    33 ∃ c d : ℕ, 0 < c ∧ 0 < d ∧
    34 RunsInTime (problem := problem) alg inputs (fun n => c * (n + 2) ^ d) precision
    35
    36def QuasipolynomialTime (alg : Program) (inputs : Set Instance)
    37 (precision : Option ℕ := none) : Prop :=
    38 ∃ c d : ℕ, 0 < c ∧ 0 < d ∧
    39 RunsInTime (problem := problem) alg inputs
    40 (fun n => 2 ^ (c * (Nat.log2 (n + 2) + 1) ^ d)) precision
    41
    42def SubexponentialTime (alg : Program) (inputs : Set Instance)
    43 (precision : Option ℕ := none) : Prop :=
    44 ∀ δ : ℝ, 0 < δ → ∃ c : ℕ, 0 < c ∧
    45 RunsInTime (problem := problem) alg inputs (fun n => c * 2 ^ ⌈δ * n⌉₊) precision
    46
    47end Lax213208.RunningTime
    48
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…