Turing degrees

This file defines Turing reducibility and equivalence, proves that Turing equivalence is an equivalence relation, and defines Turing degrees as the quotient under this relation.

Main definitions

• TuringReducible: A relation defining Turing reducibility between partial functions.
• TuringEquivalent: An equivalence relation defining Turing equivalence between partial functions.
• TuringDegree: The type of Turing degrees, defined as the quotient of partial functions under TuringEquivalent.

Notation

• f ≤ᵀ g : f is Turing reducible to g.
• f ≡ᵀ g : f is Turing equivalent to g.

References

• [Odifreddi1989] Odifreddi, Piergiorgio. Classical Recursion Theory: The Theory of Functions and Sets of Natural Numbers, Vol. I. Springer-Verlag, 1989.

Tags

Computability, Oracle, Turing Degrees, Reducibility, Equivalence Relation

@[reducible, inline]

abbrev TuringReducible (f g : ℕ →. ℕ) : Prop

f is Turing reducible to g if f is partial recursive given access to the oracle g

Equations

• TuringReducible f g = RecursiveIn {g} f

@[reducible, inline]

abbrev TuringEquivalent (f g : ℕ →. ℕ) : Prop

f is Turing equivalent to g if f is reducible to g and g is reducible to f.

Equations

• TuringEquivalent f g = AntisymmRel TuringReducible f g

def Computability.«term_≤ᵀ_» : Lean.TrailingParserDescr

f is Turing reducible to g if f is partial recursive given access to the oracle g

Equations

• Computability.«term_≤ᵀ_» = Lean.ParserDescr.trailingNode `Computability.«term_≤ᵀ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ᵀ ") (Lean.ParserDescr.cat `term 51))

def Computability.«term_≡ᵀ_» : Lean.TrailingParserDescr

f is Turing equivalent to g if f is reducible to g and g is reducible to f.

Equations

• Computability.«term_≡ᵀ_» = Lean.ParserDescr.trailingNode `Computability.«term_≡ᵀ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≡ᵀ ") (Lean.ParserDescr.cat `term 51))

theorem Nat.Partrec.turingReducible {f g : ℕ →. ℕ} (pF : Nat.Partrec f) : TuringReducible f g

If a function is partial recursive, then it is recursive in every partial function.

theorem TuringReducible.partrec_of_zero {f : ℕ →. ℕ} (fRecInZero : TuringReducible f fun (x : ℕ) => Part.some 0) : Nat.Partrec f

If a function is recursive in the constant zero function, then it is partial recursive.

theorem partrec_iff_forall_turingReducible {f : ℕ →. ℕ} : Nat.Partrec f ↔ ∀ (g : ℕ →. ℕ), TuringReducible f g

A partial function f is partial recursive if and only if it is recursive in every partial function g.

theorem TuringReducible.refl (f : ℕ →. ℕ) : TuringReducible f f

theorem TuringReducible.rfl {f : ℕ →. ℕ} : TuringReducible f f

theorem TuringReducible.trans {f g h : ℕ →. ℕ} (hg : TuringReducible f g) (hh : TuringReducible g h) : TuringReducible f h

instance instIsPreorderPFunNatTuringReducible : IsPreorder (ℕ →. ℕ) TuringReducible

theorem TuringEquivalent.equivalence : Equivalence TuringEquivalent

theorem TuringEquivalent.refl (f : ℕ →. ℕ) : TuringEquivalent f f

theorem TuringEquivalent.symm {f g : ℕ →. ℕ} (h : TuringEquivalent f g) : TuringEquivalent g f

theorem TuringEquivalent.trans (f g h : ℕ →. ℕ) (h₁ : TuringEquivalent f g) (h₂ : TuringEquivalent g h) : TuringEquivalent f h

@[reducible, inline]

abbrev TuringDegree : Type

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

Equations

• TuringDegree = Antisymmetrization (ℕ →. ℕ) TuringReducible

@[instance_reducible]

instance TuringDegree.instPartialOrder : PartialOrder TuringDegree

Equations

• TuringDegree.instPartialOrder = instPartialOrderAntisymmetrization