Oracle Computability

This file defines a model of oracle computability using partial recursive functions. It extends the notion of Nat.Partrec by allowing access to a set of oracle functions.

Main Definitions

• RecursiveIn O f: A partial function f : ℕ →. ℕ is recursive in a set of oracles O ⊆ ℕ →. ℕ if it can be constructed from constants, basic operations, and functions in O using pairing, composition, primitive recursion, and μ-recursion.
• liftPrim: Encodes a function α →. σ as a function ℕ →. ℕ using Primcodable.
• RecursiveIn', RecursiveIn₂, ComputableIn, ComputableIn₂: Versions of RecursiveIn for functions between Primcodable types.

Implementation Notes

The encoding/decoding mechanism relies on Primcodable. The definition of RecursiveIn mimics the inductive structure of Nat.Partrec.

References

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

Tags

Computability, Oracle, Recursion, Primitive Recursion

inductive Computability.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)

inductive Computability.PrimrecIn (O : Set (ℕ → ℕ)) : (ℕ → ℕ) → Prop

The primitive recursive functions ℕ → ℕ relative to a set of oracles O.

• zero {O : Set (ℕ → ℕ)} : PrimrecIn O fun (x : ℕ) => 0
• succ {O : Set (ℕ → ℕ)} : PrimrecIn O Nat.succ
• left {O : Set (ℕ → ℕ)} : PrimrecIn O fun (n : ℕ) => (Nat.unpair n).1
• right {O : Set (ℕ → ℕ)} : PrimrecIn O fun (n : ℕ) => (Nat.unpair n).2
• oracle {O : Set (ℕ → ℕ)} (g : ℕ → ℕ) : g ∈ O → PrimrecIn O g
• pair {O : Set (ℕ → ℕ)} {f g : ℕ → ℕ} : PrimrecIn O f → PrimrecIn O g → PrimrecIn O fun (n : ℕ) => Nat.pair (f n) (g n)
• comp {O : Set (ℕ → ℕ)} {f g : ℕ → ℕ} : PrimrecIn O f → PrimrecIn O g → PrimrecIn O fun (n : ℕ) => f (g n)
• prec {O : Set (ℕ → ℕ)} {f g : ℕ → ℕ} : PrimrecIn O f → PrimrecIn O g → PrimrecIn O (Nat.unpaired fun (z n : ℕ) => Nat.rec (f z) (fun (y IH : ℕ) => g (Nat.pair z (Nat.pair y IH))) n)

def Computability.liftPrim {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] (f : α →. σ) : ℕ →. ℕ

Encodes a partial function α →. σ as a partial function ℕ →. ℕ using Primcodable.

Equations

• Computability.liftPrim f n = (↑(Encodable.decode n)).bind fun (a : α) => Part.map Encodable.encode (f a)

def Computability.liftPrimrec {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] (f : α → σ) : ℕ → ℕ

Encodes a total function α → σ as a function ℕ → ℕ using Primcodable.

Equations

• Computability.liftPrimrec f n = (Option.map (fun (a : α) => Encodable.encode (f a)) (Encodable.decode n)).getD 0

def Computability.RecursiveIn' {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] (O : Set (ℕ →. ℕ)) (f : α →. σ) : Prop

A partial function between Primcodable types is recursive in O if its lift is.

Equations

• Computability.RecursiveIn' O f = Computability.RecursiveIn O (Computability.liftPrim f)

def Computability.PrimrecIn' {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] (O : Set (ℕ → ℕ)) (f : α → σ) : Prop

Relative primitive recursion between primcodable types

Equations

• Computability.PrimrecIn' O f = Computability.PrimrecIn O (Computability.liftPrimrec f)

def Computability.RecursiveIn₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] (O : Set (ℕ →. ℕ)) (f : α → β →. σ) : Prop

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

Equations

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

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

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

Equations

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

def Computability.ComputableIn₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] (O : Set (ℕ →. ℕ)) (f : α → β → σ) : Prop

A binary total function is computable in O.

Equations

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

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

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

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

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

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

If a function is computable, then it is computable in every oracle.

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

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

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

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

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

theorem Computability.RecursiveIn.some {O : Set (ℕ →. ℕ)} : RecursiveIn O Part.some

theorem Computability.RecursiveIn.none {O : Set (ℕ →. ℕ)} : RecursiveIn O fun (x : ℕ) => Part.none

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

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

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

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

theorem Computability.unpair_in (O : Set (ℕ →. ℕ)) : ComputableIn O Nat.unpair

theorem Computability.succ_in (O : Set (ℕ →. ℕ)) : ComputableIn O Nat.succ

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

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

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

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

theorem Computability.RecursiveIn.partrec_of_none {f : ℕ →. ℕ} (fRecInNone : RecursiveIn {fun (x : ℕ) => Part.none} f) : Nat.Partrec f

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

theorem Computability.partrec_iff_forall_recursiveIn {f : ℕ →. ℕ} : Nat.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.

@[simp]

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

theorem Computability.recursiveIn_mono {O₁ O₂ : Set (ℕ →. ℕ)} (hsub : O₁ ⊆ O₂) {g : ℕ →. ℕ} : RecursiveIn O₁ g → RecursiveIn O₂ g

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