English
If f: β → σ and there exist data m, l, g with m, l, g primitive recursive, together with an order condition m(b′) < m(b) for all b′ ∈ l(b), and a halting condition H(b) = some(f(b)) for all b, then f is primitive recursive.
Русский
Если функция f: β → σ и существуют данные m, l, g, которые являются примитивно рекурсивными, удовлетворяющие условию порядка m(b′) < m(b) для всех b′ ∈ l(b) и условию завершения H(b) = some(f(b)) для всех b, тогда f примитивно-рекурсивна.
LaTeX
$$$\text{If } m,l,g \text{ are primitive recursive with } \forall b, \forall b' \in l(b),\ m(b') < m(b) \text{ and } g(b, (l(b))\mapsto f(b)) = \text{Some}(f(b)), \text{ then } f \text{ is primitive recursive.}$$$
Lean4
theorem nat_omega_rec' (f : β → σ) {m : β → ℕ} {l : β → List β} {g : β → List σ → Option σ} (hm : Primrec m)
(hl : Primrec l) (hg : Primrec₂ g) (Ord : ∀ b, ∀ b' ∈ l b, m b' < m b) (H : ∀ b, g b ((l b).map f) = some (f b)) :
Primrec f := by
haveI : DecidableEq β := Encodable.decidableEqOfEncodable β
let mapGraph (M : List (β × σ)) (bs : List β) : List σ := bs.flatMap (Option.toList <| M.lookup ·)
let bindList (b : β) : ℕ → List β := fun n ↦ n.rec [b] fun _ bs ↦ bs.flatMap l
let graph (b : β) : ℕ → List (β × σ) := fun i ↦
i.rec [] fun i ih ↦ (bindList b (m b - i)).filterMap fun b' ↦ (g b' <| mapGraph ih (l b')).map (b', ·)
have mapGraph_primrec : Primrec₂ mapGraph :=
to₂ <| list_flatMap snd <| optionToList.comp₂ <| listLookup.comp₂ .right (fst.comp₂ .left)
have bindList_primrec : Primrec₂ (bindList) :=
nat_rec' snd (list_cons.comp fst (const [])) (to₂ <| list_flatMap (snd.comp snd) (hl.comp₂ .right))
have graph_primrec : Primrec₂ (graph) :=
to₂ <|
nat_rec' snd (const []) <|
to₂ <|
listFilterMap
(bindList_primrec.comp (fst.comp fst) (nat_sub.comp (hm.comp <| fst.comp fst) (fst.comp snd))) <|
to₂ <|
option_map (hg.comp snd (mapGraph_primrec.comp (snd.comp <| snd.comp fst) (hl.comp snd)))
(Primrec₂.pair.comp₂ (snd.comp₂ .left) .right)
have : Primrec (fun b => (graph b (m b + 1))[0]?.map Prod.snd) :=
option_map (list_getElem?.comp (graph_primrec.comp Primrec.id (succ.comp hm)) (const 0)) (snd.comp₂ Primrec₂.right)
exact
option_some_iff.mp <|
this.of_eq <| fun b ↦
by
have graph_eq_map_bindList (i : ℕ) (hi : i ≤ m b + 1) :
graph b i = (bindList b (m b + 1 - i)).map fun x ↦ (x, f x) :=
by
have bindList_eq_nil : bindList b (m b + 1) = [] :=
have bindList_m_lt (k : ℕ) : ∀ b' ∈ bindList b k, m b' < m b + 1 - k := by
induction k with simp [bindList]
| succ k ih => grind
List.eq_nil_iff_forall_not_mem.mpr (by intro b' ha'; by_contra; simpa using bindList_m_lt (m b + 1) b' ha')
have mapGraph_graph {bs bs' : List β} (has : bs' ⊆ bs) :
mapGraph (bs.map <| fun x => (x, f x)) bs' = bs'.map f := by
induction bs' with simp [mapGraph]
| cons b bs' ih =>
have : b ∈ bs ∧ bs' ⊆ bs := by simpa using has
rcases this with ⟨ha, has'⟩
simpa [List.lookup_graph f ha] using ih has'
have graph_succ :
∀ i,
graph b (i + 1) =
(bindList b (m b - i)).filterMap fun b' => (g b' <| mapGraph (graph b i) (l b')).map (b', ·) :=
fun _ => rfl
have bindList_succ : ∀ i, bindList b (i + 1) = (bindList b i).flatMap l := fun _ => rfl
induction i with
| zero => symm; simpa [graph] using bindList_eq_nil
| succ i
ih =>
simp only [graph_succ, ih (Nat.le_of_lt hi), Nat.succ_sub (Nat.lt_succ.mp hi), Nat.succ_eq_add_one,
bindList_succ, Nat.reduceSubDiff]
apply List.filterMap_eq_map_iff_forall_eq_some.mpr
intro b' ha'; simp; rw [mapGraph_graph]
· exact H b'
· exact (List.infix_flatMap_of_mem ha' l).subset
simp [graph_eq_map_bindList (m b + 1) (Nat.le_refl _), bindList]
