Lean4
/-- 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.
-/
inductive RecursiveIn (O : Set (ℕ →. ℕ)) : (ℕ →. ℕ) → Prop
| zero : RecursiveIn O fun _ => 0
| succ : RecursiveIn O Nat.succ
| left : RecursiveIn O fun n => (Nat.unpair n).1
| right : RecursiveIn O fun n => (Nat.unpair n).2
| oracle : ∀ g ∈ O, RecursiveIn O g
|
pair {f h : ℕ →. ℕ} (hf : RecursiveIn O f) (hh : RecursiveIn O h) : RecursiveIn O fun n => (Nat.pair <$> f n <*> h n)
| comp {f h : ℕ →. ℕ} (hf : RecursiveIn O f) (hh : RecursiveIn O h) : RecursiveIn O fun n => h n >>= f
|
prec {f h : ℕ →. ℕ} (hf : RecursiveIn O f) (hh : RecursiveIn O h) :
RecursiveIn O fun p =>
let (a, n) := Nat.unpair p
n.rec (f a) fun y IH => do
let i ← IH
h (Nat.pair a (Nat.pair y i))
|
rfind {f : ℕ →. ℕ} (hf : RecursiveIn O f) :
RecursiveIn O fun a => Nat.rfind fun n => (fun m => m = 0) <$> f (Nat.pair a n)
