TimeBounded

def

A language L over an alphabet Γ is decidable in time T (T : ℕ → ℕ) if there is a total decider f : List Γ → Bool together with a Turing machine M computing f, such that M runs for at most T n steps on every input of length n, and f agrees with the characteristic function of L: for every word w, w ∈ L iff f w = true.

Statement

def TimeBounded (Γ : Type) (T : ℕ → ℕ) (L : Language Γ) : Prop

Source

Sipser, Def. 7.1 (time complexity / decider running in time T); Arora & Barak Def. 1.1-1.2; formalised over Mathlib's bundled model Turing.TM2ComputableInTime (Mathlib/Computability/TuringMachine/Computable.lean)

Verified

10 Sep 2026

Axioms

none listed

Used by 6

PolyTimeBoundedThe class P over alphabet Γ consists of all languages L for which there is a polynomial p : Polynomial ℕ such that L is decidable in time…
time_bounded_monoIf T and T' are time bounds with T n ≤ T' n for every n, then every language decidable in time T is decidable in time T'.
time_bounded_eq_co_of_decider_negation_closedLet T be a time bound and suppose the family of deciders computable within T steps is closed under Boolean negation, i.e. for every f :…
NondeterministicPolyTimeBoundedA language L over Γ is in NP in verifier form if there are a polynomial p and a language V of words over Γ ⊕ Unit such that V is decidable…
ExpTimeBoundedThe 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 ^…
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

TimeBounded Γ T L is a proposition parameterized by a type Γ, a function T : ℕ → ℕ, and a language L : Language Γ (i.e., a set of lists over Γ). It asserts the following, in order: There exists a Boolean-valued function f : List Γ → Bool such that both of the following hold: 1. There exists a Turing machine M of type Turing.TM2ComputableInTime (id : List Γ → List Γ) (Computability.encodeBool f) — that is, a TM2 machine that computes the encoded Boolean function Computability.encodeBool f from an identity-encoded input list — such that for every natural number n, the machine's time function satisfies M.time n ≤ T n. 2. For every list w : List Γ, w belongs to L if and only if f w = true. Thus the definition says that the language L is decided by some Boolean function f on lists, and that this f is computable by a TM2 machine whose runtime function M.time is pointwise bounded above by the given function T.

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

/-- A language is decidable in time T if some Turing machine decider runs within T n steps on inputs of length n and decides it. -/
def TimeBounded (Γ : Type) (T : ℕ → ℕ) (L : Language Γ) : Prop := ∃ (f : List Γ → Bool),
    (∃ M : Turing.TM2ComputableInTime (id : List Γ → List Γ) Computability.encodeBool f,
      ∀ n, M.time n ≤ T n) ∧
    ∀ w, w ∈ L ↔ f w = true

Discuss this result Challenge it