Turing Reducibility and Turing Degrees

This file defines Turing reducibility and Turing equivalence in terms of oracle computability, as well as the notion of Turing degrees as equivalence classes under mutual reducibility.

Main Definitions

• TuringReducible f g: The function f is Turing reducible to g if f is recursive in the singleton set {g}.
• TuringEquivalent f g: Functions f and g are Turing equivalent if they are mutually Turing reducible.
• TuringDegree: The type of Turing degrees, given by the quotient of ℕ →. ℕ under TuringEquivalent.

Notation

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

Implementation Notes

We define TuringDegree as the Antisymmetrization of the preorder of partial functions under Turing reducibility. This gives a concrete representation of degrees as equivalence classes.

References

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

Tags

Computability, Turing Degrees, Reducibility, Equivalence Relation

@[reducible, inline]

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

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

Equations

• Computability.TuringReducible f g = Computability.RecursiveIn {g} f

@[reducible, inline]

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

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

Equations

• Computability.TuringEquivalent f g = AntisymmRel Computability.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 Computability.TuringReducible.refl (f : ℕ →. ℕ) : TuringReducible f f

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

instance Computability.instReflPFunNatTuringReducible : Std.Refl TuringReducible

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

instance Computability.instIsTransPFunNatTuringReducible : IsTrans (ℕ →. ℕ) TuringReducible

instance Computability.instIsPreorderPFunNatTuringReducible : IsPreorder (ℕ →. ℕ) TuringReducible

theorem Computability.TuringEquivalent.equivalence : Equivalence TuringEquivalent

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

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

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

instance Computability.instIsPreorderPFunNatTuringReducible_1 : IsPreorder (ℕ →. ℕ) TuringReducible

Instance declaring that RecursiveIn is a preorder.

@[reducible, inline]

abbrev Computability.TuringDegree : Type

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

Equations

• Computability.TuringDegree = Antisymmetrization (ℕ →. ℕ) Computability.TuringReducible

@[implicit_reducible]

instance Computability.TuringDegree.instPartialOrder : PartialOrder TuringDegree

Equations

• Computability.TuringDegree.instPartialOrder = instPartialOrderAntisymmetrization

Turing join on partial functions

We define the join (f ⊕ g) by coding answers from f as even numbers and answers from g as odd numbers:

• on even inputs 2*n, query f n and return 2 * y
• on odd inputs 2*n+1, query g n and return 2 * y + 1

def Computability.turingJoin (f g : ℕ →. ℕ) : ℕ →. ℕ

The Turing join f ⊕ g: answers from f are coded as even numbers and answers from g as odd numbers.

Equations

• (f ⊕ g) n = bif n.bodd then Part.map (fun (y : ℕ) => 2 * y + 1) (g n.div2) else Part.map (fun (y : ℕ) => 2 * y) (f n.div2)

def Computability.«term_⊕_» : Lean.TrailingParserDescr

The Turing join f ⊕ g: answers from f are coded as even numbers and answers from g as odd numbers.

Equations

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

@[simp]

theorem Computability.turingJoin_even (f g : ℕ →. ℕ) (n : ℕ) : (f ⊕ g) (2 * n) = Part.map (fun (y : ℕ) => 2 * y) (f n)

@[simp]

theorem Computability.turingJoin_odd (f g : ℕ →. ℕ) (n : ℕ) : (f ⊕ g) (2 * n + 1) = Part.map (fun (y : ℕ) => 2 * y + 1) (g n)

theorem Computability.left_le_join (f g : ℕ →. ℕ) : TuringReducible f (f ⊕ g)

theorem Computability.right_le_join (f g : ℕ →. ℕ) : TuringReducible g (f ⊕ g)

theorem Computability.RecursiveIn_cond_const {O : Set (ℕ →. ℕ)} {c : ℕ → Bool} {f : ℕ →. ℕ} (hc : Computable c) (hf : RecursiveIn O f) (k : ℕ) : RecursiveIn O fun (n : ℕ) => bif c n then f n else Part.some k

def Computability.eq01 : ℕ →. ℕ

The equality test on pairs: returns 0 if the two components are equal and 1 otherwise.

Equations

• Computability.eq01 p = Part.some (if (Nat.unpair p).1 = (Nat.unpair p).2 then 0 else 1)

theorem Computability.eq01_natPartrec : Nat.Partrec eq01

theorem Computability.eq01_recursiveIn (O : Set (ℕ →. ℕ)) : RecursiveIn O eq01

theorem Computability.eq01_rfind_none : (Nat.rfind fun (k : ℕ) => (fun (m : ℕ) => decide (m = 0)) <$> (Nat.pair <$> Part.none <*> Part.some k >>= eq01)) = Part.none

theorem Computability.eq01_rfind_some (n : ℕ) : (Nat.rfind fun (k : ℕ) => (fun (m : ℕ) => decide (m = 0)) <$> (Nat.pair <$> Part.some n <*> Part.some k >>= eq01)) = Part.some n

theorem Computability.eq01_rfind (v : Part ℕ) : (Nat.rfind fun (k : ℕ) => (fun (m : ℕ) => decide (m = 0)) <$> (Nat.pair <$> v <*> Part.some k >>= eq01)) = v

theorem Computability.RecursiveIn_cond_core_rfind {O : Set (ℕ →. ℕ)} {c : ℕ → Bool} {f g : ℕ →. ℕ} (hc : Computable c) (hf : RecursiveIn O f) (hg : RecursiveIn O g) : ∃ (cmp : ℕ →. ℕ), RecursiveIn O cmp ∧ (fun (n : ℕ) => Nat.rfind fun (k : ℕ) => (fun (m : ℕ) => decide (m = 0)) <$> cmp (Nat.pair n k)) = fun (n : ℕ) => bif c n then f n else g n

theorem Computability.RecursiveIn_cond {O : Set (ℕ →. ℕ)} {c : ℕ → Bool} {f g : ℕ →. ℕ} (hc : Computable c) (hf : RecursiveIn O f) (hg : RecursiveIn O g) : RecursiveIn O fun (n : ℕ) => bif c n then f n else g n

theorem Computability.turingJoin_recursiveIn_pair (f g : ℕ →. ℕ) : RecursiveIn {f, g} (f ⊕ g)

theorem Computability.join_le (f g h : ℕ →. ℕ) (hf : TuringReducible f h) (hg : TuringReducible g h) : TuringReducible (f ⊕ g) h

Semilattice Structure on Turing Degrees

We show that turingJoin respects Turing equivalence and lifts to a supremum operation on TuringDegree, making it a SemilatticeSup.

theorem Computability.TuringDegree.join_mono {f f' g g' : ℕ →. ℕ} (hf : TuringReducible f f') (hg : TuringReducible g g') : TuringReducible (f ⊕ g) (f' ⊕ g')

The Turing join respects Turing reducibility: if f ≤ᵀ f' and g ≤ᵀ g', then f ⊕ g ≤ᵀ f' ⊕ g'.

theorem Computability.TuringDegree.join_congr {f f' g g' : ℕ →. ℕ} (hf : TuringEquivalent f f') (hg : TuringEquivalent g g') : TuringEquivalent (f ⊕ g) (f' ⊕ g')

The Turing join respects Turing equivalence.

def Computability.TuringDegree.sup : TuringDegree → TuringDegree → TuringDegree

The supremum operation on Turing degrees, induced by the Turing join.

Equations

• Computability.TuringDegree.sup = Quotient.lift₂ (fun (f g : ℕ →. ℕ) => toAntisymmetrization Computability.TuringReducible (f ⊕ g)) Computability.TuringDegree.sup._proof_1

theorem Computability.TuringDegree.sup_mk (f g : ℕ →. ℕ) : sup (toAntisymmetrization TuringReducible f) (toAntisymmetrization TuringReducible g) = toAntisymmetrization TuringReducible (f ⊕ g)

theorem Computability.TuringDegree.le_sup_left (a b : TuringDegree) : a ≤ a.sup b

theorem Computability.TuringDegree.le_sup_right (a b : TuringDegree) : b ≤ a.sup b

theorem Computability.TuringDegree.sup_le {a b c : TuringDegree} (ha : a ≤ c) (hb : b ≤ c) : a.sup b ≤ c

@[implicit_reducible]

instance Computability.TuringDegree.instSemilatticeSup : SemilatticeSup TuringDegree

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Computability.TuringDegree.sup_def (f g : ℕ →. ℕ) : toAntisymmetrization TuringReducible f ⊔ toAntisymmetrization TuringReducible g = toAntisymmetrization TuringReducible (f ⊕ g)

The sup on Turing degrees agrees with the Turing join on representatives.