Computability

DefinitionPrimitive recursive function#

Primrec f means f is primitive recursive (after encoding its input and output as natural numbers).

Primrec.{u_1, u_2} {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] (f : α → β) : Prop
Sources
MathlibPrimrec
Uses 1 · Used by 2
Statement usesNatural number
Used bySmn theorem · Kleene's recursion theorem

DefinitionAckermann function#

The two-argument Ackermann function, defined so that

  • ack 0 n = n + 1
  • ack (m + 1) 0 = ack m 1
  • ack (m + 1) (n + 1) = ack m (ack (m + 1) n).

This is of interest as both a fast-growing function, and as an example of a recursive function that isn't primitive recursive.

ack : ℕ → ℕ → ℕ
Sources
Mathliback
Uses 1
Statement usesNatural number

DefinitionTuring machine#

A Post-Turing machine with symbol type Γ and label type Λ is a function which, given the current state q : Λ and the tape head a : Γ, either halts (returns none) or returns a new state q' : Λ and a Stmt describing what to do, either a move left or right, or a write command.

Both Λ and Γ are required to be inhabited; the default value for Γ is the "blank" tape value, and the default value of Λ is the initial state.

Turing.TM0.Machine.{u_1, u_2} (Γ : Type u_1) (Λ : Type u_2) [Inhabited Λ] :
  Type (max (max u_1 u_2) u_1 u_2)
Sources
MathlibTuring.TM0.Machine

TheoremHalting problem#

The Halting problem is not computable

ComputablePred.halting_problem (n : ℕ) : ¬ComputablePred fun c => (c.eval n).Dom
Sources
MathlibComputablePred.halting_problem
Uses 2
Statement usesIn terms of general recursive functions
Proof usesRice theorem

TheoremRice theorem#

Rice's Theorem

ComputablePred.rice (C : Set (ℕ →. ℕ)) (h : ComputablePred fun c => c.eval ∈ C) {f g : ℕ →. ℕ}
  (hf : Nat.Partrec f) (hg : Nat.Partrec g) (fC : f ∈ C) : g ∈ C
Sources
MathlibComputablePred.rice
Uses 2 · Used by 1
Statement usesIn terms of general recursive functions
Proof usesKleene's recursion theorem
Used byHalting problem

AbbreviationTuring degrees#

Turing degrees are the equivalence classes of partial functions under Turing equivalence.

TuringDegree : Type
Sources
MathlibTuringDegree
Uses 1
Statement usesNatural number

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.