Oracle computability

This file defines oracle computability using partial recursive functions.

Main definitions

• Nat.RecursiveIn O f: A partial function f : ℕ →. ℕ is partial recursive given access to oracles in the set O.
• RecursiveIn O f: Lifts Nat.RecursiveIn to partial functions between Primcodable types.
• ComputableIn O f: A total function f : α → σ is computable given access to oracles in O.

Main results

• Nat.Partrec.recursiveIn: Every partial recursive function is recursive in any oracle set.
• partrec_iff_forall_recursiveIn_singleton: A function is partial recursive iff it is recursive in every singleton oracle set.
• recursiveIn_empty_iff: Being recursive in the empty set is equivalent to being partial recursive.
• RecursiveIn.mono: Monotonicity of RecursiveIn with respect to oracle sets.

Implementation notes

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.

References

• Piergiorgio Odifreddi, Classical Recursion Theory: The Theory of Functions and Sets of Natural Numbers

Tags

Computability, Oracle, Turing Degrees, Reducibility, Equivalence Relation

inductive Nat.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 (ℕ →. ℕ)} : Nat.RecursiveIn O fun (x : ℕ) => 0
• succ {O : Set (ℕ →. ℕ)} : Nat.RecursiveIn O ↑Nat.succ
• left {O : Set (ℕ →. ℕ)} : Nat.RecursiveIn O fun (n : ℕ) => ↑(some (unpair n).1)
• right {O : Set (ℕ →. ℕ)} : Nat.RecursiveIn O fun (n : ℕ) => ↑(some (unpair n).2)
• oracle {O : Set (ℕ →. ℕ)} (g : ℕ →. ℕ) : g ∈ O → Nat.RecursiveIn O g
• pair {O : Set (ℕ →. ℕ)} {f h : ℕ →. ℕ} (hf : Nat.RecursiveIn O f) (hh : Nat.RecursiveIn O h) : Nat.RecursiveIn O fun (n : ℕ) => Nat.pair <$> f n <*> h n
• comp {O : Set (ℕ →. ℕ)} {f h : ℕ →. ℕ} (hf : Nat.RecursiveIn O f) (hh : Nat.RecursiveIn O h) : Nat.RecursiveIn O fun (n : ℕ) => h n >>= f
• prec {O : Set (ℕ →. ℕ)} {f h : ℕ →. ℕ} (hf : Nat.RecursiveIn O f) (hh : Nat.RecursiveIn O h) : Nat.RecursiveIn O fun (p : ℕ) => match 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 : Nat.RecursiveIn O f) : Nat.RecursiveIn O fun (a : ℕ) => Nat.rfind fun (n : ℕ) => (fun (m : ℕ) => decide (m = 0)) <$> f (Nat.pair a n)

def RecursiveIn {α : Type u_5} {σ : Type u_6} [Primcodable α] [Primcodable σ] (O : Set (ℕ →. ℕ)) (f : α →. σ) : Prop

A partial function f : α →. σ between Primcodable types is recursive in a set of oracles O if its encoding as a function ℕ →. ℕ is Nat.RecursiveIn O.

Equations

• RecursiveIn O f = Nat.RecursiveIn O fun (n : ℕ) => (↑(Encodable.decode n)).bind fun (a : α) => Part.map Encodable.encode (f a)

theorem RecursiveIn.iff_nat {f : ℕ →. ℕ} {O : Set (ℕ →. ℕ)} : RecursiveIn O f ↔ Nat.RecursiveIn O f

def RecursiveIn₂ {α : Type u_5} {β : Type u_6} {σ : Type u_7} [Primcodable α] [Primcodable β] [Primcodable σ] (O : Set (ℕ →. ℕ)) (f : α → β →. σ) : Prop

A binary partial function is recursive in O if the curried form is.

Equations

• RecursiveIn₂ O f = RecursiveIn O fun (p : α × β) => f p.1 p.2

def ComputableIn {α : Type u_5} {σ : Type u_6} [Primcodable α] [Primcodable σ] (O : Set (ℕ →. ℕ)) (f : α → σ) : Prop

A total function is computable in O if its constant lift is recursive in O.

Equations

• ComputableIn O f = RecursiveIn O fun (a : α) => Part.some (f a)

def ComputableIn₂ {α : Type u_5} {β : Type u_6} {σ : Type u_7} [Primcodable α] [Primcodable β] [Primcodable σ] (O : Set (ℕ →. ℕ)) (f : α → β → σ) : Prop

A binary total function is computable in O.

Equations

• ComputableIn₂ O f = ComputableIn O fun (p : α × β) => f p.1 p.2

theorem Nat.RecursiveIn.of_eq {f g : ℕ →. ℕ} {O : Set (ℕ →. ℕ)} (hf : Nat.RecursiveIn O f) (H : ∀ (n : ℕ), f n = g n) : Nat.RecursiveIn O g

theorem Nat.RecursiveIn.of_eq_tot {f : ℕ →. ℕ} {g : ℕ → ℕ} {O : Set (ℕ →. ℕ)} (hf : Nat.RecursiveIn O f) (H : ∀ (n : ℕ), g n ∈ f n) : Nat.RecursiveIn O ↑g

theorem Nat.RecursiveIn.subst {O O' : Set (ℕ →. ℕ)} {f : ℕ →. ℕ} (hf : Nat.RecursiveIn O f) (hO : ∀ g ∈ O, Nat.RecursiveIn O' g) : Nat.RecursiveIn O' f

If every element of O is Nat.RecursiveIn O', then any function which is Nat.RecursiveIn O is also Nat.RecursiveIn O'.

theorem Nat.RecursiveIn.partrec_of_oracle {f : ℕ →. ℕ} {O : Set (ℕ →. ℕ)} (hO : ∀ g ∈ O, Nat.Partrec g) (hf : Nat.RecursiveIn O f) : Nat.Partrec f

If every function in O is partial recursive, then a function which is Nat.RecursiveIn O is also partial recursive.

theorem Nat.Partrec.recursiveIn {f : ℕ →. ℕ} {O : Set (ℕ →. ℕ)} (pF : Nat.Partrec f) : Nat.RecursiveIn O f

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

theorem Partrec.recursiveIn {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} {O : Set (ℕ →. ℕ)} (hf : Partrec f) : RecursiveIn O f

If a partial function is partial recursive, then it is RecursiveIn any oracle set.

theorem Nat.Primrec.recursiveIn {O : Set (ℕ →. ℕ)} {f : ℕ → ℕ} (hf : Nat.Primrec f) : Nat.RecursiveIn O fun (n : ℕ) => ↑(some (f n))

theorem Computable.computableIn {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α → β} {O : Set (ℕ →. ℕ)} (hf : Computable f) : ComputableIn O f

theorem Primrec.computableIn {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α → σ} {O : Set (ℕ →. ℕ)} (hf : Primrec f) : ComputableIn O f

theorem Primrec₂.computableIn₂ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} {O : Set (ℕ →. ℕ)} (hf : Primrec₂ f) : ComputableIn₂ O f

theorem ComputableIn.recursiveIn {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α → σ} {O : Set (ℕ →. ℕ)} (hf : ComputableIn O f) : RecursiveIn O fun (a : α) => Part.some (f a)

theorem ComputableIn₂.recursiveIn₂ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} {O : Set (ℕ →. ℕ)} (hf : ComputableIn₂ O f) : RecursiveIn₂ O fun (a : α) => ↑(f a)

theorem RecursiveIn.of_eq {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {O : Set (ℕ →. ℕ)} {f g : α →. σ} (hf : RecursiveIn O f) (H : ∀ (x : α), f x = g x) : RecursiveIn O g

theorem RecursiveIn.of_eq_tot {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {O : Set (ℕ →. ℕ)} {f : α →. σ} {g : α → σ} (hf : RecursiveIn O f) (H : ∀ (n : α), g n ∈ f n) : RecursiveIn O ↑g

theorem RecursiveIn.oracle {O : Set (ℕ →. ℕ)} (g : ℕ →. ℕ) : g ∈ O → RecursiveIn O g

theorem RecursiveIn.some {α : Type u_1} [Primcodable α] {O : Set (ℕ →. ℕ)} : RecursiveIn O Part.some

theorem RecursiveIn.none {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {O : Set (ℕ →. ℕ)} : RecursiveIn O fun (x : α) => Part.none

theorem RecursiveIn.subst {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {O O' : Set (ℕ →. ℕ)} {f : α →. σ} (hf : RecursiveIn O f) (hO : ∀ g ∈ O, RecursiveIn O' g) : RecursiveIn O' f

If every element of O is RecursiveIn O', then any function which is RecursiveIn O is also RecursiveIn O'.

theorem RecursiveIn.mono {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} {O₁ O₂ : Set (ℕ →. ℕ)} (hsub : O₁ ⊆ O₂) (hf : RecursiveIn O₁ f) : RecursiveIn O₂ f

Monotonicity of RecursiveIn with respect to oracle sets.

theorem RecursiveIn.partrec_of_oracle {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} {O : Set (ℕ →. ℕ)} (hO : ∀ g ∈ O, Partrec g) (hf : RecursiveIn O f) : Partrec f

If every function in O is partial recursive, then a function which is RecursiveIn O is also partial recursive.

theorem RecursiveIn.partrec_of_const {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} {s : Part ℕ} (hf : RecursiveIn {fun (x : ℕ) => s} f) : Partrec f

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

@[simp]

theorem recursiveIn_empty_iff {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} : RecursiveIn ∅ f ↔ Partrec f

theorem partrec_iff_forall_recursiveIn_singleton {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} : Partrec f ↔ ∀ (g : ℕ →. ℕ), RecursiveIn {g} f

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

theorem ComputableIn.const {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {O : Set (ℕ →. ℕ)} (s : σ) : ComputableIn O fun (x : α) => s

theorem ComputableIn.id {α : Type u_1} [Primcodable α] {O : Set (ℕ →. ℕ)} : ComputableIn O id

theorem ComputableIn.fst {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {O : Set (ℕ →. ℕ)} : ComputableIn O Prod.fst

theorem ComputableIn.snd {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {O : Set (ℕ →. ℕ)} : ComputableIn O Prod.snd

theorem ComputableIn.unpair {O : Set (ℕ →. ℕ)} : ComputableIn O Nat.unpair

theorem ComputableIn.succ {O : Set (ℕ →. ℕ)} : ComputableIn O Nat.succ

theorem ComputableIn.sumInl {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {O : Set (ℕ →. ℕ)} : ComputableIn O Sum.inl

theorem ComputableIn.sumInr {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {O : Set (ℕ →. ℕ)} : ComputableIn O Sum.inr