Complexity

StructurePolynomial-time computation#

A Turing machine + a polynomial time function + a proof it outputs f in at most time(input.length) steps.

Turing.TM2ComputableInPolyTime {α β αΓ βΓ : Type} (ea : α → List αΓ) (eb : β → List βΓ)
  (f : α → β) : Type 1

Sources

• Mathlib documentation: Turing.TM2ComputableInPolyTime
• Source of Turing.TM2ComputableInPolyTime in Mathlib/Computability/TuringMachine/Computable.lean
• Mathlib overview: Logic and computation › Complexity

MathlibTuring.TM2ComputableInPolyTime

Uses 1

Statement usesPolynomial functions

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.