Computable function

DefinitionIn terms of general recursive functions#

Computable functions α → σ between Primcodable types: a function is computable if and only if it is partially recursive (as a partial function)

Computable.{u_1, u_2} {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] (f : α → σ) :
  Prop

Sources

• Mathlib documentation: Computable
• Source of Computable in Mathlib/Computability/Partrec.lean
• Mathlib overview: Logic and computation › Computability › computable function

MathlibComputable

Uses 1 · Used by 4

Statement usesNatural number

Used byHalting problem · Rice theorem · Smn theorem · Kleene's recursion theorem

StructureIn terms of Turing machines#

A Turing machine + a proof it outputs f.

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

Sources

• Mathlib documentation: Turing.TM2Computable
• Source of Turing.TM2Computable in Mathlib/Computability/TuringMachine/Computable.lean
• Mathlib overview: Logic and computation › Computability › computable function

MathlibTuring.TM2Computable

Uses 2

Statement usesFinite set · Natural number

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.