Oracle Computability and Turing Degrees

This file defines a model of oracle computability using partial recursive functions. This file introduces Turing reducibility and equivalence, prove that Turing equivalence is an equivalence relation, and define Turing degrees as the quotient under this relation.

Main Definitions

• RecursiveIn O f: An inductive definition representing that a partial function f is partial recursive given access to a set of oracles O.
• 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.

Implementation Notes

The type of partial functions recursive in a set of oracle O is the smallest type containing the constant zero, the successor, left and right projections, each oracle g ∈ O, and is closed under pairing, composition, primitive recursion, and μ-recursion.

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

inductive RecursiveIn (O : Set (ℕ →. ℕ)) : (ℕ →. ℕ) → Prop

The type of partial functions recursive in a set of oracles O is the smallest type containing the constant zero, the successor, left and right projections, each oracle g ∈ O, and is closed under pairing, composition, primitive recursion, and μ-recursion.

• zero {O : Set (ℕ →. ℕ)} : RecursiveIn O fun (x : ℕ) => 0
• succ {O : Set (ℕ →. ℕ)} : RecursiveIn O ↑Nat.succ
• left {O : Set (ℕ →. ℕ)} : RecursiveIn O fun (n : ℕ) => ↑(some (Nat.unpair n).1)
• right {O : Set (ℕ →. ℕ)} : RecursiveIn O fun (n : ℕ) => ↑(some (Nat.unpair n).2)
• oracle {O : Set (ℕ →. ℕ)} (g : ℕ →. ℕ) : g ∈ O → RecursiveIn O g
• pair {O : Set (ℕ →. ℕ)} {f h : ℕ →. ℕ} (hf : RecursiveIn O f) (hh : RecursiveIn O h) : RecursiveIn O fun (n : ℕ) => Nat.pair <$> f n <*> h n
• comp {O : Set (ℕ →. ℕ)} {f h : ℕ →. ℕ} (hf : RecursiveIn O f) (hh : RecursiveIn O h) : RecursiveIn O fun (n : ℕ) => h n >>= f
• prec {O : Set (ℕ →. ℕ)} {f h : ℕ →. ℕ} (hf : RecursiveIn O f) (hh : RecursiveIn O h) : RecursiveIn O fun (p : ℕ) => match Nat.unpair p with | (a, n) => Nat.rec (f a) (fun (y : ℕ) (IH : Part ℕ) => do let i ← IH h (Nat.pair a (Nat.pair y i))) n
• rfind {O : Set (ℕ →. ℕ)} {f : ℕ →. ℕ} (hf : RecursiveIn O f) : RecursiveIn O fun (a : ℕ) => Nat.rfind fun (n : ℕ) => (fun (m : ℕ) => decide (m = 0)) <$> f (Nat.pair a n)

@[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 : 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

instance instIsReflPFunNatTuringReducible : IsRefl (ℕ →. ℕ) TuringReducible

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

instance instIsTransPFunNatTuringReducible : IsTrans (ℕ →. ℕ) TuringReducible

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

instance instIsPreorderPFunNatTuringReducible_1 : IsPreorder (ℕ →. ℕ) TuringReducible

Instance declaring that RecursiveIn is a preorder.

@[reducible, inline]

abbrev TuringDegree : Type

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

Equations

• TuringDegree = Antisymmetrization (ℕ →. ℕ) TuringReducible

instance TuringDegree.instPartialOrder : PartialOrder TuringDegree

Equations

• TuringDegree.instPartialOrder = instPartialOrderAntisymmetrization

@[simp]

theorem recursiveIn_empty_iff_partrec {f : ℕ →. ℕ} : RecursiveIn ∅ f ↔ Nat.Partrec f