Oracle computability #
This file defines oracle computability using partial recursive functions.
Main definitions #
RecursiveIn O f: An inductive definition representing that a partial functionfis partial recursive given access to a set of oracles O.
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.
Tags #
Computability, Oracle, Turing Degrees, Reducibility, Equivalence Relation
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)