ExpTimeBounded
The class EXP over alphabet Γ consists of all languages L for which there is a polynomial p such that L is decidable in time n ↦ 2 ^ (p.eval n), i.e. by a Turing machine whose running time on inputs of length n is bounded by 2^(p(n)).
Statement
def ExpTimeBounded (Γ : Type) (L : Language Γ) : Prop
- Source
- Arora & Barak, Def. 1.5 (EXP = ∪_c DTIME(2^(n^c))); Papadimitriou, Def. 2.1
- Verified
- 10 Sep 2026
- Axioms
- none listed
- Built on 1
- TimeBoundedA language L over an alphabet Γ is decidable in time T (T : ℕ → ℕ) if there is a total decider f : List Γ → Bool together with a Turing…
- Used by 1
- poly_time_subset_exp_timeEvery language in P is in EXP: if L is decidable in time p(n) for a polynomial p, then L is decidable in time 2^(p(n)).
Read back from the Lean
For any type Γ and any language L over Γ, the definition equates ExpTimeBounded Γ L with the following proposition: there exists a polynomial p : Polynomial ℕ, then there exists a Boolean-valued function f : List Γ → Bool, such that (1) there exists a Turing machine M witnessing that f is computable in time under input encoding id : List Γ → List Γ and output encoding Computability.encodeBool, and for every natural number n, M.time n ≤ 2 ^ (p.eval n); this bound is required for all n, not merely eventually or infinitely often; and (2) for every word w, w ∈ L if and only if f w = true. Thus L is exactly the set decided by f, and f is computable by a Turing machine whose time at length n is bounded by 2 raised to the value at n of a natural polynomial.
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- The complexity class EXP over the alphabet Γ: languages decidable in exponential time. -/ def ExpTimeBounded (Γ : Type) (L : Language Γ) : Prop := ∃ p : Polynomial ℕ, TimeBounded Γ (fun n => 2 ^ p.eval n) L