Encoding of Oracle Programs and Universality

This file provides an encoding for oracle partial recursive functions and a definition of the universal partial recursive function relative to an oracle, along with a proof that it is universal.

theorem Computability.RecursiveIn_id {O : Set (ℕ →. ℕ)} : RecursiveIn O fun (n : ℕ) => Part.some n

The identity function is recursive in any oracle O.

theorem Computability.RecursiveIn_comp_total {O : Set (ℕ →. ℕ)} {f g : ℕ → ℕ} (hf : RecursiveIn O fun (n : ℕ) => Part.some (f n)) (hg : RecursiveIn O fun (n : ℕ) => Part.some (g n)) : RecursiveIn O fun (n : ℕ) => Part.some (f (g n))

The composition of two total recursive functions is recursive.

theorem Computability.RecursiveIn_pair_total {O : Set (ℕ →. ℕ)} {f g : ℕ → ℕ} (hf : RecursiveIn O fun (n : ℕ) => Part.some (f n)) (hg : RecursiveIn O fun (n : ℕ) => Part.some (g n)) : RecursiveIn O fun (n : ℕ) => Part.some (Nat.pair (f n) (g n))

theorem Computability.RecursiveIn_prec_total {O : Set (ℕ →. ℕ)} {f h : ℕ → ℕ} (hf : RecursiveIn O fun (n : ℕ) => Part.some (f n)) (hh : RecursiveIn O fun (n : ℕ) => Part.some (h n)) : RecursiveIn O fun (p : ℕ) => Part.some (Nat.rec (f (Nat.unpair p).1) (fun (y IH : ℕ) => h (Nat.pair (Nat.unpair p).1 (Nat.pair y IH))) (Nat.unpair p).2)

theorem Computability.RecursiveIn_add {O : Set (ℕ →. ℕ)} : RecursiveIn O fun (p : ℕ) => Part.some ((Nat.unpair p).1 + (Nat.unpair p).2)

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

Every primitive recursive function is recursive.

theorem Computability.RecursiveIn.rfind' {O : Set (ℕ →. ℕ)} {f : ℕ →. ℕ} (hf : RecursiveIn O f) : RecursiveIn O (Nat.unpaired fun (a m : ℕ) => Part.map (fun (x : ℕ) => x + m) (Nat.rfind fun (n : ℕ) => (fun (m : ℕ) => decide (m = 0)) <$> f (Nat.pair a (n + m))))

def Computability.oracleCode {α : Type} [Denumerable α] (f : α → ℕ →. ℕ) : ℕ → ℕ →. ℕ

Reindexes an oracle family f : α → ℕ →. ℕ to a family indexed by ℕ via the denumerable encoding of α; out-of-range indices map to the nowhere-defined function.

Equations

• Computability.oracleCode f i n = match Encodable.decode i with | some a => f a n | none => ⊥

inductive Computability.codeo : Type

Codes (Gödel numberings) for oracle partial recursive functions.

• zero : codeo
• succ : codeo
• left : codeo
• right : codeo
• oracle : ℕ → codeo
• pair : codeo → codeo → codeo
• comp : codeo → codeo → codeo
• prec : codeo → codeo → codeo
• rfind' : codeo → codeo

def Computability.evalo {α : Type} [Primcodable α] (f : α → ℕ →. ℕ) : codeo → ℕ →. ℕ

Semantics of codeo, relative to an indexed oracle family.

Equations

• One or more equations did not get rendered due to their size.
• Computability.evalo f Computability.codeo.zero = pure 0
• Computability.evalo f Computability.codeo.succ = fun (n : ℕ) => ↑(some (n + 1))
• Computability.evalo f Computability.codeo.left = fun (n : ℕ) => ↑(some (Nat.unpair n).1)
• Computability.evalo f Computability.codeo.right = fun (n : ℕ) => ↑(some (Nat.unpair n).2)
• Computability.evalo f (Computability.codeo.oracle i) = match Encodable.decode i with | some a => f a | none => fun (x : ℕ) => ⊥
• Computability.evalo f (cf.pair cg) = fun (n : ℕ) => Nat.pair <$> Computability.evalo f cf n <*> Computability.evalo f cg n
• Computability.evalo f (cf.comp cg) = fun (n : ℕ) => Computability.evalo f cg n >>= Computability.evalo f cf

def Computability.encodeCodeo : codeo → ℕ

Encodes a code as a natural number.

Equations

• Computability.encodeCodeo Computability.codeo.zero = 0
• Computability.encodeCodeo Computability.codeo.succ = 1
• Computability.encodeCodeo Computability.codeo.left = 2
• Computability.encodeCodeo Computability.codeo.right = 3
• Computability.encodeCodeo (Computability.codeo.oracle i) = 4 + 5 * i
• Computability.encodeCodeo (cf.pair cg) = 4 + (5 * Nat.pair (Computability.encodeCodeo cf) (Computability.encodeCodeo cg) + 1)
• Computability.encodeCodeo (cf.comp cg) = 4 + (5 * Nat.pair (Computability.encodeCodeo cf) (Computability.encodeCodeo cg) + 2)
• Computability.encodeCodeo (cf.prec cg) = 4 + (5 * Nat.pair (Computability.encodeCodeo cf) (Computability.encodeCodeo cg) + 3)
• Computability.encodeCodeo cf.rfind' = 4 + (5 * Computability.encodeCodeo cf + 4)

@[irreducible]

def Computability.decodeCodeo : ℕ → codeo

Decodes a natural number into a code; the inverse of encodeCodeo.

Equations

• One or more equations did not get rendered due to their size.
• Computability.decodeCodeo 0 = Computability.codeo.zero
• Computability.decodeCodeo 1 = Computability.codeo.succ
• Computability.decodeCodeo 2 = Computability.codeo.left
• Computability.decodeCodeo 3 = Computability.codeo.right

theorem Computability.encodeCodeo_decodeCodeo' (c : ℕ) : encodeCodeo (decodeCodeo c) = c

theorem Computability.decodeCodeo_encodeCodeo (c : codeo) : decodeCodeo (encodeCodeo c) = c

def Computability.const : ℕ → codeo

Returns a code for the constant function outputting a particular natural.

Equations

• Computability.const 0 = Computability.codeo.zero
• Computability.const n.succ = Computability.codeo.succ.comp (Computability.const n)

theorem Computability.const_inj {n₁ n₂ : ℕ} : const n₁ = const n₂ → n₁ = n₂

def Computability.idCode : codeo

A code for the identity function.

Equations

• Computability.idCode = Computability.codeo.left.pair Computability.codeo.right

def Computability.curry (c : codeo) (n : ℕ) : codeo

Given a code c taking a pair as input, returns a code using n as the first argument to c.

Equations

• Computability.curry c n = c.comp ((Computability.const n).pair Computability.idCode)

theorem Computability.rfind'o {α : Type} [Primcodable α] {g : α → ℕ →. ℕ} {cf : codeo} (hf : RecursiveIn (Set.range g) (evalo g cf)) : RecursiveIn (Set.range g) (Nat.unpaired fun (a m : ℕ) => Part.map (fun (x : ℕ) => x + m) (Nat.rfind fun (n : ℕ) => (fun (m : ℕ) => decide (m = 0)) <$> evalo g cf (Nat.pair a (n + m))))

def Computability.encodeConst (n : ℕ) : ℕ

The encoding of the code for the constant function with value n.

Equations

• Computability.encodeConst n = Computability.encodeCodeo (Computability.const n)

def Computability.encodeConstStepFun (p : ℕ) : ℕ

One primitive-recursion step used to show encodeConst is primitive recursive.

Equations

• Computability.encodeConstStepFun p = 4 + (5 * Nat.pair 1 (Nat.unpair (Nat.unpair p).2).2 + 2)

theorem Computability.encode_const_step_primrec : Nat.Primrec encodeConstStepFun

theorem Computability.encode_const_succ (n : ℕ) : encodeConst (n + 1) = 4 + (5 * Nat.pair 1 (encodeConst n) + 2)

theorem Computability.encode_const_primrec : Nat.Primrec encodeConst

def Computability.sInner (n : ℕ) : ℕ

The encoding of the code pairing the constant n with the identity code.

Equations

• Computability.sInner n = Computability.encodeCodeo ((Computability.const n).pair Computability.idCode)

@[simp]

theorem Computability.s_inner_eq (n : ℕ) : sInner n = 4 + (5 * Nat.pair (encodeConst n) (encodeCodeo idCode) + 1)

theorem Computability.s_inner_primrec : Nat.Primrec sInner

def Computability.s (n : ℕ) : ℕ

The encoding of the code applying oracle 0 to the constant n (an s-m-n index).

Equations

• Computability.s n = Computability.encodeCodeo ((Computability.codeo.oracle 0).comp (Computability.const n))

theorem Computability.s_eq (n : ℕ) : s n = 4 + (5 * Nat.pair 4 (encodeConst n) + 2)

theorem Computability.s_primrec : Nat.Primrec s

theorem Computability.exists_code_rel {α : Type} [Primcodable α] (g : α → ℕ →. ℕ) (f : ℕ →. ℕ) : RecursiveIn (Set.range g) f ↔ ∃ (c : codeo), evalo g c = f

A function is partial recursive relative to an indexed set of oracles O if and only if there is a code implementing it. Therefore, evalo is a universal partial recursive function relative to g.