OraclePartialRecursionTraces.lean

1 import RealizationBoundaries.ComputablePresentations
2 
3 /-! # Finite semantic traces of relative partial primitive recursion -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace RealizationBoundaries
7 
8 /-- The literal partial primitive recursion appearing in native `RecursiveIn.prec`. -/
9 def oraclePartialRec (f h : ℕ →. ℕ) (a : ℕ) : ℕ → Part ℕ :=
10   Nat.rec (f a) (fun n r => r.bind (fun z => h (Nat.pair a (Nat.pair n z))))
11 
12 /-- A terminating primitive-recursion evaluation is exactly a finite sequence
13 of terminating child evaluations. Values after the final stage carry no data. -/
14 theorem oraclePartialRec_mem_iff_trace (f h : ℕ →. ℕ) (a n y : ℕ) :
15     y ∈ oraclePartialRec f h a n ↔
16       ∃ s : ℕ → ℕ, s n = y ∧ s 0 ∈ f a ∧
17         ∀ i < n, s (i+1) ∈ h (Nat.pair a (Nat.pair i (s i))) := by
18   induction n generalizing y with
19   | zero =>
20     constructor
21     · intro hy
22       exact ⟨fun _ => y, rfl, hy, fun _ hi => (Nat.not_lt_zero _ hi).elim⟩
23     · rintro ⟨s, hsy, hs, _⟩
24       exact hsy ▸ hs
25   | succ n ih =>
26     change y ∈ (oraclePartialRec f h a n).bind
27       (fun z => h (Nat.pair a (Nat.pair n z))) ↔ _
28     rw [Part.mem_bind_iff]
29     constructor
30     · rintro ⟨z, hz, hy⟩
31       obtain ⟨s, hsn, hs0, hs⟩ := (ih z).mp hz
32       let t := Function.update s (n+1) y
33       refine ⟨t, by simp [t], ?_, ?_⟩
34       · simpa [t, Nat.succ_ne_zero] using hs0
35       · intro i hi
36         rcases Nat.lt_succ_iff_lt_or_eq.mp hi with hin | rfl
37         · have hi1 : i+1 ≠ n+1 := by omega
38           have hi0 : i ≠ n+1 := by omega
39           simpa [t, Function.update_of_ne hi1, Function.update_of_ne hi0] using hs i hin
40         · simpa [t, hsn] using hy
41     · rintro ⟨s, hsn, hs0, hs⟩
42       refine ⟨s n, (ih (s n)).mpr ⟨s, rfl, hs0, ?_⟩, ?_⟩
43       · exact fun i hi => hs i (Nat.lt_succ_of_lt hi)
44       · exact hsn ▸ hs n (Nat.lt_succ_self n)
45 
46 /-- The native primitive-recursion constructor uses exactly this semantic
47 recursor after decoding its parameter/count pair. -/
48 theorem recursiveIn_prec_uses_oraclePartialRec {O : Set (ℕ →. ℕ)}
49     {f h : ℕ →. ℕ} (hf : Nat.RecursiveIn O f) (hh : Nat.RecursiveIn O h) :
50     Nat.RecursiveIn O (fun k => oraclePartialRec f h k.unpair.1 k.unpair.2) :=
51   Nat.RecursiveIn.prec hf hh
52 
53 end RealizationBoundaries

Back to source controls