Closure properties of oracle-relative computability

Mathlib's Nat.RecursiveIn O is the inductive closure of the basic functions and the oracles in O under pairing, composition, primitive recursion and unbounded search starting at zero. This file derives further closure properties from those constructors:

• Nat.RecursiveIn.comp_primrec, Nat.RecursiveIn.map_primrec: composition with a primitive recursive function on either side;
• Nat.RecursiveIn.rfind': unbounded search starting at a given value, the oracle-relative form of Nat.Partrec.rfind';
• Nat.RecursiveIn.cond: a conditional with a guard computable in O, which evaluates only the selected branch.

The search rfind' is the closure property needed to evaluate the search instruction of a code, whose search starts at the second component of its input rather than at zero. The conditional is needed to combine two reductions according to a decidable property of the input, as in the Turing join of two oracles.

Mathlib's ComputableIn₂ expresses computability of binary total functions in terms of encodings; ComputableIn₂.iff_nat restates it for functions on ℕ as a Nat.RecursiveIn statement on codes Nat.pair a b of pairs. Total oracle-computable functions are closed under composition, pairing, primitive recursion, and forming finite initial segments of a sequence. These closure proofs adapt Mathlib's Computable.comp, Computable.pair, and Computable.nat_rec in Mathlib.Computability.Partrec to Nat.RecursiveIn.

theorem Nat.RecursiveIn.comp_primrec {O : Set (ℕ →. ℕ)} {f : ℕ →. ℕ} {g : ℕ → ℕ} (hf : Nat.RecursiveIn O f) (hg : Nat.Primrec g) : Nat.RecursiveIn O fun (n : ℕ) => f (g n)

Precomposition with a primitive recursive function preserves recursiveness in O.

theorem Nat.RecursiveIn.map_primrec {O : Set (ℕ →. ℕ)} {f : ℕ →. ℕ} {g : ℕ → ℕ} (hf : Nat.RecursiveIn O f) (hg : Nat.Primrec g) : Nat.RecursiveIn O fun (n : ℕ) => Part.map g (f n)

Postcomposition with a primitive recursive function preserves recursiveness in O.

theorem Nat.RecursiveIn.rfind' {O : Set (ℕ →. ℕ)} {f : ℕ →. ℕ} (hf : Nat.RecursiveIn O f) : Nat.RecursiveIn O (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))))

Search from a given start. If f is recursive in O, so is the function sending Nat.pair a m to the least n ≥ m with f (Nat.pair a n) = 0, provided f (Nat.pair a k) is defined for every k from m to n. This is the oracle-relative form of Nat.Partrec.rfind'.

theorem Nat.RecursiveIn.cond {O : Set (ℕ →. ℕ)} {f : ℕ →. ℕ} {c : ℕ → Bool} (hc : ComputableIn O c) (hf : Nat.RecursiveIn O f) {g : ℕ →. ℕ} (hg : Nat.RecursiveIn O g) : Nat.RecursiveIn O fun (n : ℕ) => bif c n then f n else g n

Conditionals. If the guard c is computable in O and f and g are recursive in O, then so is the function which agrees with f where c holds and with g elsewhere. Only the selected branch is evaluated, so the conditional is defined at n exactly when the selected branch is.

theorem ComputableIn₂.iff_nat {O : Set (ℕ →. ℕ)} {f : ℕ → ℕ → ℕ} : ComputableIn₂ O f ↔ Nat.RecursiveIn O fun (n : ℕ) => Part.some (f (Nat.unpair n).1 (Nat.unpair n).2)

A binary total function on ℕ is computable in O exactly when it is recursive in O as a function of the code Nat.pair a b of its arguments.

theorem ComputableIn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {O : Set (ℕ →. ℕ)} {f : β → γ} {g : α → β} (hf : ComputableIn O f) (hg : ComputableIn O g) : ComputableIn O fun (a : α) => f (g a)

Composition of total oracle-computable functions.

theorem ComputableIn.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {O : Set (ℕ →. ℕ)} {f : α → β} {g : α → γ} (hf : ComputableIn O f) (hg : ComputableIn O g) : ComputableIn O fun (a : α) => (f a, g a)

Pairing total oracle-computable functions.

theorem ComputableIn.nat_rec {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {O : Set (ℕ →. ℕ)} {f : α → ℕ} {g : α → β} {h : α → ℕ × β → β} (hf : ComputableIn O f) (hg : ComputableIn O g) (hh : ComputableIn₂ O h) : ComputableIn O fun (a : α) => Nat.rec (g a) (fun (n : ℕ) (b : β) => h a (n, b)) (f a)

Primitive recursion of total oracle-computable functions. The recursion counter is allowed to depend on the parameter.

theorem ComputableIn₂.list_range_map {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {O : Set (ℕ →. ℕ)} {f : α → ℕ → β} (hf : ComputableIn₂ O f) : ComputableIn₂ O fun (a : α) (n : ℕ) => List.map (f a) (List.range n)

A finite initial segment of an oracle-computable sequence can be computed uniformly in its length and in the sequence parameter.