From 7ae0c59569396856dcbf320577529e42c35edb2b Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Fri, 6 Mar 2026 10:20:50 +0100 Subject: [PATCH 01/13] =?UTF-8?q?feat(CombinatoryLogic):=20Partrec=20?= =?UTF-8?q?=E2=86=92=20SKI=20computability?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Prove that every Nat.Partrec function on ℕ is SKI-computable (nat_partrec_ski_computable). Translates all eight Nat.Partrec.Code constructors to SKI terms and proves correctness, exercising the Recursion.lean infrastructure: primitive recursion (Rec), μ-recursion (RFind/RFindAbove), Nat pairing/unpairing, and integer square root. --- Cslib.lean | 1 + Cslib/Languages/CombinatoryLogic/Basic.lean | 1 + Cslib/Languages/CombinatoryLogic/List.lean | 1 + .../CombinatoryLogic/PartrecEquivalence.lean | 379 ++++++++++++++++++ .../Languages/CombinatoryLogic/Recursion.lean | 8 +- 5 files changed, 389 insertions(+), 1 deletion(-) create mode 100644 Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean diff --git a/Cslib.lean b/Cslib.lean index 4d3aa37f9..5a97679e6 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -78,6 +78,7 @@ public import Cslib.Languages.CombinatoryLogic.Confluence public import Cslib.Languages.CombinatoryLogic.Defs public import Cslib.Languages.CombinatoryLogic.Evaluation public import Cslib.Languages.CombinatoryLogic.List +public import Cslib.Languages.CombinatoryLogic.PartrecEquivalence public import Cslib.Languages.CombinatoryLogic.Recursion public import Cslib.Languages.LambdaCalculus.LocallyNameless.Context public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic diff --git a/Cslib/Languages/CombinatoryLogic/Basic.lean b/Cslib/Languages/CombinatoryLogic/Basic.lean index e8743062a..0bf5d2aca 100644 --- a/Cslib/Languages/CombinatoryLogic/Basic.lean +++ b/Cslib/Languages/CombinatoryLogic/Basic.lean @@ -288,6 +288,7 @@ theorem cond_correct (a x y : SKI) (u : Bool) (h : IsBool u a) : /-- Neg := λ a. Cond FF TT a -/ protected def Neg : SKI := SKI.Cond ⬝ FF ⬝ TT +@[scoped grind →] theorem neg_correct (a : SKI) (ua : Bool) (h : IsBool ua a) : IsBool (¬ ua) (SKI.Neg ⬝ a) := by apply isBool_trans (a' := if ua then FF else TT) · apply cond_correct (h := h) diff --git a/Cslib/Languages/CombinatoryLogic/List.lean b/Cslib/Languages/CombinatoryLogic/List.lean index c71721da9..3645cfe62 100644 --- a/Cslib/Languages/CombinatoryLogic/List.lean +++ b/Cslib/Languages/CombinatoryLogic/List.lean @@ -74,6 +74,7 @@ theorem nil_def (c n : SKI) : (Nil ⬝ c ⬝ n) ↠ n := NilPoly.toSKI_correct [c, n] (by simp) /-- The empty list term correctly represents `[]`. -/ +@[scoped grind .] theorem nil_correct : IsChurchList [] Nil := nil_def /-! ### Cons: Consing an element onto a list -/ diff --git a/Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean b/Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean new file mode 100644 index 000000000..75fb9ce74 --- /dev/null +++ b/Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean @@ -0,0 +1,379 @@ +/- +Copyright (c) 2026 Jesse Alama. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jesse Alama +-/ + +module + +public import Cslib.Languages.CombinatoryLogic.Recursion +public import Mathlib.Computability.PartrecCode + +@[expose] public section + +/-! +# Partial Recursive → SKI-computable (Nat.Partrec) + +This file defines a notion of computability for SKI terms on natural numbers +(using Church numerals) and translates `Nat.Partrec.Code` to SKI terms. + +## Main definitions + +- `Computes t f`: SKI term `t` computes a partial function `f : ℕ →. ℕ` on Church numerals. +- `codeToSKINat`: translates `Nat.Partrec.Code` constructors to SKI terms. + +## Main results + +- `codeToSKINat_correct`: each translated code computes the corresponding `Code.eval`. +- `nat_partrec_ski_computable`: every `Nat.Partrec` function is SKI-computable. + +-/ + +namespace Cslib + +namespace SKI + +open Red MRed +open Nat.Partrec + +/-! ### Computability predicate for functions on ℕ -/ + +/-- An SKI term `t` computes a partial function `f : ℕ →. ℕ` if, +for every Church numeral input, `t` reduces to a Church numeral output +whenever `f` is defined. -/ +def Computes (t : SKI) (f : ℕ →. ℕ) : Prop := + ∀ n : ℕ, ∀ cn : SKI, IsChurch n cn → + ∀ m : ℕ, f n = Part.some m → + ∃ cm : SKI, IsChurch m cm ∧ (t ⬝ cn) ↠ cm + +/-! ### Helper terms for prec and rfind' translations -/ + +/-- Step function for primitive recursion: + `λ a cn prev. tg ⬝ (NatPair ⬝ a ⬝ (NatPair ⬝ (Pred ⬝ cn) ⬝ prev))` + Variables: &0 = a, &1 = cn, &2 = prev -/ +def PrecStepPoly (tg : SKI) : SKI.Polynomial 3 := + tg ⬝' (NatPair ⬝' &0 ⬝' (NatPair ⬝' (Pred ⬝' &1) ⬝' &2)) +/-- SKI term for the primitive recursion step function. -/ +def PrecStep (tg : SKI) : SKI := (PrecStepPoly tg).toSKI +theorem precStep_def (tg a cn prev : SKI) : + (PrecStep tg ⬝ a ⬝ cn ⬝ prev) ↠ + tg ⬝ (NatPair ⬝ a ⬝ (NatPair ⬝ (Pred ⬝ cn) ⬝ prev)) := + (PrecStepPoly tg).toSKI_correct [a, cn, prev] (by simp) + +/-- Full primitive recursion translation: + `λ n. Rec (tf (left n)) (PrecStep tg (left n)) (right n)` -/ +def PrecTransPoly (tf tg : SKI) : SKI.Polynomial 1 := + Rec ⬝' (tf ⬝' (NatUnpairLeft ⬝' &0)) + ⬝' (PrecStep tg ⬝' (NatUnpairLeft ⬝' &0)) + ⬝' (NatUnpairRight ⬝' &0) +/-- SKI term for primitive recursion. -/ +def PrecTrans (tf tg : SKI) : SKI := (PrecTransPoly tf tg).toSKI +theorem precTrans_def (tf tg cn : SKI) : + (PrecTrans tf tg ⬝ cn) ↠ + Rec ⬝ (tf ⬝ (NatUnpairLeft ⬝ cn)) + ⬝ (PrecStep tg ⬝ (NatUnpairLeft ⬝ cn)) + ⬝ (NatUnpairRight ⬝ cn) := + (PrecTransPoly tf tg).toSKI_correct [cn] (by simp) + +/-- Unbounded search translation: + `λ n. RFindAbove ⬝ (NatUnpairRight ⬝ n) ⬝ (B ⬝ tf ⬝ (NatPair ⬝ (NatUnpairLeft ⬝ n)))` -/ +def RFindTransPoly (tf : SKI) : SKI.Polynomial 1 := + RFindAbove ⬝' (NatUnpairRight ⬝' &0) + ⬝' (B ⬝' tf ⬝' (NatPair ⬝' (NatUnpairLeft ⬝' &0))) +/-- SKI term for unbounded search (μ-recursion). -/ +def RFindTrans (tf : SKI) : SKI := (RFindTransPoly tf).toSKI +theorem rfindTrans_def (tf cn : SKI) : + (RFindTrans tf ⬝ cn) ↠ + RFindAbove ⬝ (NatUnpairRight ⬝ cn) + ⬝ (B ⬝ tf ⬝ (NatPair ⬝ (NatUnpairLeft ⬝ cn))) := + (RFindTransPoly tf).toSKI_correct [cn] (by simp) + +/-! ### Translation from Nat.Partrec.Code to SKI -/ + +/-- Translate `Nat.Partrec.Code` to SKI terms operating on Church numerals. -/ +def codeToSKINat : Code → SKI + | .zero => K ⬝ SKI.Zero + | .succ => SKI.Succ + | .left => NatUnpairLeft + | .right => NatUnpairRight + | .pair f g => + let tf := codeToSKINat f + let tg := codeToSKINat g + S ⬝ (B ⬝ NatPair ⬝ tf) ⬝ tg + | .comp f g => + B ⬝ (codeToSKINat f) ⬝ (codeToSKINat g) + | .prec f g => + PrecTrans (codeToSKINat f) (codeToSKINat g) + | .rfind' f => + RFindTrans (codeToSKINat f) + +/-! ### Correctness proofs -/ + +/-- `Code.zero` computes the constant zero function. -/ +theorem zero_computes : Computes (K ⬝ SKI.Zero) (Code.eval .zero) := by + intro n cn hcn m hm + have h0 : Code.eval .zero n = Part.some 0 := by + rw [show Code.zero = Code.const 0 from rfl, Code.eval_const] + rw [h0] at hm + have heq : (0 : ℕ) = m := Part.some_injective hm + subst heq + exact ⟨SKI.Zero, zero_correct, MRed.K SKI.Zero cn⟩ + +/-- `Code.succ` computes the successor function. -/ +theorem succ_computes : Computes SKI.Succ (Code.eval .succ) := by + intro n cn hcn m hm + have h0 : Code.eval .succ n = Part.some (n + 1) := by + simp only [Code.eval, PFun.coe_val] + rw [h0] at hm + have heq : n + 1 = m := Part.some_injective hm + subst heq + exact ⟨SKI.Succ ⬝ cn, succ_correct n cn hcn, .refl⟩ + +/-- `Code.left` computes the left projection of `Nat.unpair`. -/ +theorem left_computes : Computes NatUnpairLeft (Code.eval .left) := by + intro n cn hcn m hm + have h0 : Code.eval .left n = Part.some (Nat.unpair n).1 := by + simp only [Code.eval, PFun.coe_val] + rw [h0] at hm + have heq := Part.some_injective hm + subst heq + exact ⟨NatUnpairLeft ⬝ cn, natUnpairLeft_correct n cn hcn, .refl⟩ + +/-- `Code.right` computes the right projection of `Nat.unpair`. -/ +theorem right_computes : Computes NatUnpairRight (Code.eval .right) := by + intro n cn hcn m hm + have h0 : Code.eval .right n = Part.some (Nat.unpair n).2 := by + simp only [Code.eval, PFun.coe_val] + rw [h0] at hm + have heq := Part.some_injective hm + subst heq + exact ⟨NatUnpairRight ⬝ cn, natUnpairRight_correct n cn hcn, .refl⟩ + +/-- Composition of computable functions is computable. -/ +theorem comp_computes {f g : ℕ →. ℕ} {tf tg : SKI} + (hf : Computes tf f) (hg : Computes tg g) : + Computes (B ⬝ tf ⬝ tg) (fun n => g n >>= f) := by + intro n cn hcn m hm + simp only at hm + have hm' : m ∈ (g n >>= f) := by rw [hm]; exact Part.mem_some m + obtain ⟨intermediate, hint_mem, hm_mem⟩ := Part.mem_bind_iff.mp hm' + have hgn : g n = Part.some intermediate := Part.eq_some_iff.mpr hint_mem + have hfint : f intermediate = Part.some m := Part.eq_some_iff.mpr hm_mem + obtain ⟨cint, hcint, hcint_red⟩ := hg n cn hcn intermediate hgn + obtain ⟨cm, hcm, hcm_red⟩ := hf intermediate cint hcint m hfint + exact ⟨cm, hcm, Trans.trans (B_tail_mred tf tg cn _ hcint_red) hcm_red⟩ + +/-- Pairing of computable functions is computable. -/ +theorem pair_computes {f g : ℕ →. ℕ} {tf tg : SKI} + (hf : Computes tf f) (hg : Computes tg g) : + Computes (S ⬝ (B ⬝ NatPair ⬝ tf) ⬝ tg) + (fun n => Nat.pair <$> f n <*> g n) := by + intro n cn hcn m hm + simp only at hm + -- hm : Nat.pair <$> f n <*> g n = Part.some m + have hm' : m ∈ (Nat.pair <$> f n <*> g n) := by rw [hm]; exact Part.mem_some m + -- Unfold <*> into bind: pf <*> pa = pf >>= fun h => h <$> pa + have hm_bind : m ∈ Part.bind (Part.map Nat.pair (f n)) (fun h => Part.map h (g n)) := hm' + obtain ⟨h, hh_mem, hm_in_h⟩ := Part.mem_bind_iff.mp hm_bind + obtain ⟨a, ha_mem, hh_eq⟩ := (Part.mem_map_iff _).mp hh_mem + subst hh_eq + obtain ⟨b, hb_mem, hm_eq⟩ := (Part.mem_map_iff _).mp hm_in_h + have hfn : f n = Part.some a := Part.eq_some_iff.mpr ha_mem + have hgn : g n = Part.some b := Part.eq_some_iff.mpr hb_mem + obtain ⟨ca, hca, hca_red⟩ := hf n cn hcn a hfn + obtain ⟨cb, hcb, hcb_red⟩ := hg n cn hcn b hgn + refine ⟨NatPair ⬝ ca ⬝ cb, ?_, ?_⟩ + · subst hm_eq + exact natPair_correct a b ca cb hca hcb + · calc (S ⬝ (B ⬝ NatPair ⬝ tf) ⬝ tg ⬝ cn) + ↠ ((B ⬝ NatPair ⬝ tf) ⬝ cn ⬝ (tg ⬝ cn)) := MRed.S _ _ _ + _ ↠ ((NatPair ⬝ (tf ⬝ cn)) ⬝ (tg ⬝ cn)) := MRed.head _ (B_def _ _ _) + _ ↠ ((NatPair ⬝ ca) ⬝ (tg ⬝ cn)) := MRed.head _ (MRed.tail _ hca_red) + _ ↠ (NatPair ⬝ ca ⬝ cb) := MRed.tail _ hcb_red + +/-- Helper: `Rec` correctly implements primitive recursion from `Code.prec`. -/ +private theorem prec_rec_correct (f g : Code) (tf tg : SKI) + (ihf : Computes tf f.eval) (ihg : Computes tg g.eval) + (a₀ : ℕ) (ca : SKI) (hca : IsChurch a₀ ca) : + ∀ b₀ : ℕ, ∀ m : ℕ, + Code.eval (f.prec g) (Nat.pair a₀ b₀) = Part.some m → + ∀ cb : SKI, IsChurch b₀ cb → + ∃ cm, IsChurch m cm ∧ + (Rec ⬝ (tf ⬝ ca) ⬝ (PrecStep tg ⬝ ca) ⬝ cb) ↠ cm := by + intro b₀ + induction b₀ with + | zero => + intro m hm cb hcb + rw [Code.eval_prec_zero] at hm + obtain ⟨cm, hcm, hred⟩ := ihf a₀ ca hca m hm + exact ⟨cm, hcm, Trans.trans (rec_zero _ _ cb hcb) hred⟩ + | succ k ih => + intro m hm cb hcb + rw [Code.eval_prec_succ] at hm + -- Extract the intermediate value from the bind + have hm' : m ∈ (Code.eval (f.prec g) (Nat.pair a₀ k) >>= + fun i => g.eval (Nat.pair a₀ (Nat.pair k i))) := by + rw [hm]; exact Part.mem_some m + obtain ⟨ih_val, hih_mem, hm_mem⟩ := Part.mem_bind_iff.mp hm' + have hih_eq := Part.eq_some_iff.mpr hih_mem + have hm_eq := Part.eq_some_iff.mpr hm_mem + -- By IH, Rec computes the intermediate value on Pred ⬝ cb + have hpred : IsChurch k (Pred ⬝ cb) := pred_correct (k + 1) cb hcb + obtain ⟨cih, hcih, hcih_red⟩ := ih ih_val hih_eq (Pred ⬝ cb) hpred + -- Build Church numeral for the argument to g + have hpair_inner := natPair_correct k ih_val (Pred ⬝ cb) cih hpred hcih + have hpair_full := natPair_correct a₀ (Nat.pair k ih_val) ca + (NatPair ⬝ (Pred ⬝ cb) ⬝ cih) hca hpair_inner + -- By ihg, tg computes the result + obtain ⟨cm, hcm, hcm_red⟩ := ihg _ _ hpair_full m hm_eq + -- Chain the reductions + set step := PrecStep tg ⬝ ca + set base := tf ⬝ ca + refine ⟨cm, hcm, ?_⟩ + calc + _ ↠ step ⬝ cb ⬝ (Rec ⬝ base ⬝ step ⬝ (Pred ⬝ cb)) := + rec_succ k base step cb hcb + _ ↠ step ⬝ cb ⬝ cih := MRed.tail _ hcih_red + _ ↠ tg ⬝ (NatPair ⬝ ca ⬝ (NatPair ⬝ (Pred ⬝ cb) ⬝ cih)) := + precStep_def tg ca cb cih + _ ↠ cm := hcm_red + +/-- Helper: extract eval facts from rfind membership, with `m₀ +` order + matching `rfind_above_induction`. -/ +private theorem rfind_eval_facts {f : Code} {a₀ m₀ k : ℕ} + (hk : k ∈ Nat.rfind (fun n => + (fun m => decide (m = 0)) <$> f.eval (Nat.pair a₀ (n + m₀)))) : + f.eval (Nat.pair a₀ (m₀ + k)) = Part.some 0 ∧ + ∀ i < k, ∃ vi, vi ≠ 0 ∧ f.eval (Nat.pair a₀ (m₀ + i)) = Part.some vi := by + constructor + · have hspec := Nat.rfind_spec hk + obtain ⟨val, hval_mem, hval_eq⟩ := (Part.mem_map_iff _).mp hspec + have : val = 0 := by simpa using hval_eq + subst this; rw [Nat.add_comm] at hval_mem + exact Part.eq_some_iff.mpr hval_mem + · intro i hi + have hmin := Nat.rfind_min hk hi + obtain ⟨val, hval_mem, hval_eq⟩ := (Part.mem_map_iff _).mp hmin + have hval_ne : val ≠ 0 := by simpa using hval_eq + rw [Nat.add_comm] at hval_mem + exact ⟨val, hval_ne, Part.eq_some_iff.mpr hval_mem⟩ + +/-- Helper: `RFindAbove` correctly implements `Code.rfind'` by induction on + the number of steps until the root. -/ +private theorem rfind_above_induction (f : Code) (tf : SKI) + (ihf : Computes tf f.eval) (a₀ : ℕ) (ca : SKI) (hca : IsChurch a₀ ca) + (g : SKI) (hg : g = B ⬝ tf ⬝ (NatPair ⬝ ca)) : + ∀ n m : ℕ, ∀ x : SKI, IsChurch m x → + f.eval (Nat.pair a₀ (m + n)) = Part.some 0 → + (∀ i < n, ∃ vi, vi ≠ 0 ∧ + f.eval (Nat.pair a₀ (m + i)) = Part.some vi) → + IsChurch (m + n) (RFindAbove ⬝ x ⬝ g) := by + intro n + induction n with + | zero => + intro m x hx hroot _ + simp only [Nat.add_zero] at hroot ⊢ + apply isChurch_trans (a' := RFindAboveAux ⬝ RFindAbove ⬝ x ⬝ g) + · apply MRed.head; apply MRed.head; exact fixedPoint_correct _ + apply isChurch_trans (a' := x) + · apply rfindAboveAux_base + -- Need: IsChurch 0 (g ⬝ x) + subst hg + apply isChurch_trans _ (B_def tf (NatPair ⬝ ca) x) + have hpair := natPair_correct a₀ m ca x hca hx + obtain ⟨cm, hcm, hred⟩ := ihf _ _ hpair 0 hroot + exact isChurch_trans 0 hred hcm + · exact hx + | succ n ih => + intro m x hx hroot hbelow + apply isChurch_trans (a' := RFindAboveAux ⬝ RFindAbove ⬝ x ⬝ g) + · apply MRed.head; apply MRed.head; exact fixedPoint_correct _ + -- f at m is nonzero, so step + obtain ⟨v₀, hv₀_ne, hv₀_eval⟩ := hbelow 0 (by omega) + simp only [Nat.add_zero] at hv₀_eval + apply isChurch_trans (a' := RFindAbove ⬝ (SKI.Succ ⬝ x) ⬝ g) + · apply rfindAboveAux_step (m := v₀ - 1) + subst hg + apply isChurch_trans _ (B_def tf (NatPair ⬝ ca) x) + have hpair := natPair_correct a₀ m ca x hca hx + obtain ⟨cm, hcm, hred⟩ := ihf _ _ hpair v₀ hv₀_eval + have hv₀_pos : v₀ - 1 + 1 = v₀ := Nat.succ_pred_eq_of_ne_zero hv₀_ne + rw [hv₀_pos] + exact isChurch_trans _ hred hcm + · have h := ih (m + 1) (SKI.Succ ⬝ x) (succ_correct m x hx) + (by rw [show m + 1 + n = m + (n + 1) from by omega]; exact hroot) + (by + intro i hi + obtain ⟨vi, hvi_ne, hvi_eval⟩ := hbelow (i + 1) (by omega) + exact ⟨vi, hvi_ne, by + rw [show m + 1 + i = m + (i + 1) from by omega]; exact hvi_eval⟩) + rw [show m + (n + 1) = m + 1 + n from by omega] + exact h + +/-- Main correctness theorem: `codeToSKINat` correctly computes `Code.eval`. -/ +theorem codeToSKINat_correct (c : Code) : Computes (codeToSKINat c) c.eval := by + induction c with + | zero => exact zero_computes + | succ => exact succ_computes + | left => exact left_computes + | right => exact right_computes + | pair f g ihf ihg => + simp only [codeToSKINat, Code.eval] + exact pair_computes ihf ihg + | comp f g ihf ihg => + simp only [codeToSKINat, Code.eval] + exact comp_computes ihf ihg + | prec f g ihf ihg => + simp only [codeToSKINat] + intro n cn hcn m hm + have hca := natUnpairLeft_correct n cn hcn + have hcb := natUnpairRight_correct n cn hcn + have hred := precTrans_def (codeToSKINat f) (codeToSKINat g) cn + -- Rewrite eval in terms of unpair components + have hpair : n = Nat.pair (Nat.unpair n).1 (Nat.unpair n).2 := + (Nat.pair_unpair n).symm + rw [hpair] at hm + obtain ⟨cm, hcm, hcm_red⟩ := prec_rec_correct f g _ _ ihf ihg + (Nat.unpair n).1 (NatUnpairLeft ⬝ cn) hca + (Nat.unpair n).2 m hm (NatUnpairRight ⬝ cn) hcb + exact ⟨cm, hcm, Trans.trans hred hcm_red⟩ + | rfind' f ihf => + simp only [codeToSKINat] + intro n cn hcn result hresult + set tf := codeToSKINat f + set a₀ := (Nat.unpair n).1 + set m₀ := (Nat.unpair n).2 + have hca := natUnpairLeft_correct n cn hcn + have hcm₀ := natUnpairRight_correct n cn hcn + have hred := rfindTrans_def tf cn + -- Extract k from the rfind result + have hresult' : result ∈ Code.eval (Code.rfind' f) n := by + rw [hresult]; exact Part.mem_some _ + simp only [Code.eval, Nat.unpaired, + show (Nat.unpair n).1 = a₀ from rfl, + show (Nat.unpair n).2 = m₀ from rfl] at hresult' + obtain ⟨k, hk_mem, hresult_eq⟩ := (Part.mem_map_iff _).mp hresult' + subst hresult_eq + obtain ⟨heval_root, heval_below⟩ := rfind_eval_facts hk_mem + set g := B ⬝ tf ⬝ (NatPair ⬝ (NatUnpairLeft ⬝ cn)) + have hind := rfind_above_induction f tf ihf a₀ + (NatUnpairLeft ⬝ cn) hca g rfl k m₀ + (NatUnpairRight ⬝ cn) hcm₀ heval_root heval_below + rw [Nat.add_comm] at hind + exact ⟨RFindAbove ⬝ (NatUnpairRight ⬝ cn) ⬝ g, hind, hred⟩ + +/-! ### Main equivalence theorem -/ + +/-- Every partial recursive function `f : ℕ →. ℕ` is SKI-computable. + +This establishes that SKI combinatory logic can compute all partial recursive +functions on ℕ. +-/ +theorem nat_partrec_ski_computable (f : ℕ →. ℕ) (hf : Nat.Partrec f) : + ∃ t : SKI, Computes t f := by + obtain ⟨c, hc⟩ := Code.exists_code.mp hf + exact ⟨codeToSKINat c, hc ▸ codeToSKINat_correct c⟩ + +end SKI + +end Cslib diff --git a/Cslib/Languages/CombinatoryLogic/Recursion.lean b/Cslib/Languages/CombinatoryLogic/Recursion.lean index 5885b0d74..dce848cf9 100644 --- a/Cslib/Languages/CombinatoryLogic/Recursion.lean +++ b/Cslib/Languages/CombinatoryLogic/Recursion.lean @@ -253,7 +253,7 @@ We define Rec so that -/ def Rec : SKI := fixedPoint RecAux theorem rec_def (x g a : SKI) : - (Rec ⬝ x ⬝ g ⬝ a) ↠ SKI.Cond ⬝ x ⬝ (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) ⬝ (IsZero ⬝ a) := calc + (Rec ⬝ x ⬝ g ⬝ a) ↠ SKI.Cond ⬝ x ⬝ (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) ⬝ (IsZero ⬝ a) := calc _ ↠ RecAux ⬝ Rec ⬝ x ⬝ g ⬝ a := by apply MRed.head; apply MRed.head; apply MRed.head apply fixedPoint_correct @@ -305,6 +305,12 @@ theorem rfindAboveAux_step (R₀ f a : SKI) {m : Nat} (hfa : IsChurch (m + 1) (f /-- Find the minimal root of `fNat` above a number n -/ def RFindAbove : SKI := RFindAboveAux.fixedPoint + +/-- One unfolding of `RFindAbove`: apply the fixed-point combinator once. -/ +theorem RFindAbove_unfold (x g : SKI) : + (RFindAbove ⬝ x ⬝ g) ↠ RFindAboveAux ⬝ RFindAbove ⬝ x ⬝ g := by + apply MRed.head; apply MRed.head; exact fixedPoint_correct _ + theorem RFindAbove_correct (fNat : Nat → Nat) (f x : SKI) (hf : ∀ i : Nat, ∀ y : SKI, IsChurch i y → IsChurch (fNat i) (f ⬝ y)) (n m : Nat) (hx : IsChurch m x) (hroot : fNat (m+n) = 0) (hpos : ∀ i < n, fNat (m+i) ≠ 0) : From 8337461ca93c20566c1f1787c513f0ef673e765f Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Sat, 7 Mar 2026 14:44:12 +0100 Subject: [PATCH 02/13] refactor(CombinatoryLogic): simplify Computes using isChurch_trans --- .../CombinatoryLogic/PartrecEquivalence.lean | 79 ++++++++----------- 1 file changed, 33 insertions(+), 46 deletions(-) diff --git a/Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean b/Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean index 75fb9ce74..d49681cc4 100644 --- a/Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean +++ b/Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean @@ -39,12 +39,12 @@ open Nat.Partrec /-! ### Computability predicate for functions on ℕ -/ /-- An SKI term `t` computes a partial function `f : ℕ →. ℕ` if, -for every Church numeral input, `t` reduces to a Church numeral output -whenever `f` is defined. -/ +for every Church numeral input, `t` applied to the input is a Church numeral +for the output whenever `f` is defined. -/ def Computes (t : SKI) (f : ℕ →. ℕ) : Prop := ∀ n : ℕ, ∀ cn : SKI, IsChurch n cn → ∀ m : ℕ, f n = Part.some m → - ∃ cm : SKI, IsChurch m cm ∧ (t ⬝ cn) ↠ cm + IsChurch m (t ⬝ cn) /-! ### Helper terms for prec and rfind' translations -/ @@ -117,7 +117,7 @@ theorem zero_computes : Computes (K ⬝ SKI.Zero) (Code.eval .zero) := by rw [h0] at hm have heq : (0 : ℕ) = m := Part.some_injective hm subst heq - exact ⟨SKI.Zero, zero_correct, MRed.K SKI.Zero cn⟩ + exact isChurch_trans 0 (MRed.K SKI.Zero cn) zero_correct /-- `Code.succ` computes the successor function. -/ theorem succ_computes : Computes SKI.Succ (Code.eval .succ) := by @@ -127,7 +127,7 @@ theorem succ_computes : Computes SKI.Succ (Code.eval .succ) := by rw [h0] at hm have heq : n + 1 = m := Part.some_injective hm subst heq - exact ⟨SKI.Succ ⬝ cn, succ_correct n cn hcn, .refl⟩ + exact succ_correct n cn hcn /-- `Code.left` computes the left projection of `Nat.unpair`. -/ theorem left_computes : Computes NatUnpairLeft (Code.eval .left) := by @@ -137,7 +137,7 @@ theorem left_computes : Computes NatUnpairLeft (Code.eval .left) := by rw [h0] at hm have heq := Part.some_injective hm subst heq - exact ⟨NatUnpairLeft ⬝ cn, natUnpairLeft_correct n cn hcn, .refl⟩ + exact natUnpairLeft_correct n cn hcn /-- `Code.right` computes the right projection of `Nat.unpair`. -/ theorem right_computes : Computes NatUnpairRight (Code.eval .right) := by @@ -147,7 +147,7 @@ theorem right_computes : Computes NatUnpairRight (Code.eval .right) := by rw [h0] at hm have heq := Part.some_injective hm subst heq - exact ⟨NatUnpairRight ⬝ cn, natUnpairRight_correct n cn hcn, .refl⟩ + exact natUnpairRight_correct n cn hcn /-- Composition of computable functions is computable. -/ theorem comp_computes {f g : ℕ →. ℕ} {tf tg : SKI} @@ -159,9 +159,9 @@ theorem comp_computes {f g : ℕ →. ℕ} {tf tg : SKI} obtain ⟨intermediate, hint_mem, hm_mem⟩ := Part.mem_bind_iff.mp hm' have hgn : g n = Part.some intermediate := Part.eq_some_iff.mpr hint_mem have hfint : f intermediate = Part.some m := Part.eq_some_iff.mpr hm_mem - obtain ⟨cint, hcint, hcint_red⟩ := hg n cn hcn intermediate hgn - obtain ⟨cm, hcm, hcm_red⟩ := hf intermediate cint hcint m hfint - exact ⟨cm, hcm, Trans.trans (B_tail_mred tf tg cn _ hcint_red) hcm_red⟩ + have hcint := hg n cn hcn intermediate hgn + have hcm := hf intermediate (tg ⬝ cn) hcint m hfint + exact isChurch_trans _ (B_def tf tg cn) hcm /-- Pairing of computable functions is computable. -/ theorem pair_computes {f g : ℕ →. ℕ} {tf tg : SKI} @@ -180,16 +180,13 @@ theorem pair_computes {f g : ℕ →. ℕ} {tf tg : SKI} obtain ⟨b, hb_mem, hm_eq⟩ := (Part.mem_map_iff _).mp hm_in_h have hfn : f n = Part.some a := Part.eq_some_iff.mpr ha_mem have hgn : g n = Part.some b := Part.eq_some_iff.mpr hb_mem - obtain ⟨ca, hca, hca_red⟩ := hf n cn hcn a hfn - obtain ⟨cb, hcb, hcb_red⟩ := hg n cn hcn b hgn - refine ⟨NatPair ⬝ ca ⬝ cb, ?_, ?_⟩ - · subst hm_eq - exact natPair_correct a b ca cb hca hcb - · calc (S ⬝ (B ⬝ NatPair ⬝ tf) ⬝ tg ⬝ cn) - ↠ ((B ⬝ NatPair ⬝ tf) ⬝ cn ⬝ (tg ⬝ cn)) := MRed.S _ _ _ - _ ↠ ((NatPair ⬝ (tf ⬝ cn)) ⬝ (tg ⬝ cn)) := MRed.head _ (B_def _ _ _) - _ ↠ ((NatPair ⬝ ca) ⬝ (tg ⬝ cn)) := MRed.head _ (MRed.tail _ hca_red) - _ ↠ (NatPair ⬝ ca ⬝ cb) := MRed.tail _ hcb_red + have hca := hf n cn hcn a hfn + have hcb := hg n cn hcn b hgn + subst hm_eq + exact isChurch_trans _ (calc (S ⬝ (B ⬝ NatPair ⬝ tf) ⬝ tg ⬝ cn) + ↠ ((B ⬝ NatPair ⬝ tf) ⬝ cn ⬝ (tg ⬝ cn)) := MRed.S _ _ _ + _ ↠ (NatPair ⬝ (tf ⬝ cn) ⬝ (tg ⬝ cn)) := MRed.head _ (B_def _ _ _)) + (natPair_correct a b (tf ⬝ cn) (tg ⬝ cn) hca hcb) /-- Helper: `Rec` correctly implements primitive recursion from `Code.prec`. -/ private theorem prec_rec_correct (f g : Code) (tf tg : SKI) @@ -198,15 +195,13 @@ private theorem prec_rec_correct (f g : Code) (tf tg : SKI) ∀ b₀ : ℕ, ∀ m : ℕ, Code.eval (f.prec g) (Nat.pair a₀ b₀) = Part.some m → ∀ cb : SKI, IsChurch b₀ cb → - ∃ cm, IsChurch m cm ∧ - (Rec ⬝ (tf ⬝ ca) ⬝ (PrecStep tg ⬝ ca) ⬝ cb) ↠ cm := by + IsChurch m (Rec ⬝ (tf ⬝ ca) ⬝ (PrecStep tg ⬝ ca) ⬝ cb) := by intro b₀ induction b₀ with | zero => intro m hm cb hcb rw [Code.eval_prec_zero] at hm - obtain ⟨cm, hcm, hred⟩ := ihf a₀ ca hca m hm - exact ⟨cm, hcm, Trans.trans (rec_zero _ _ cb hcb) hred⟩ + exact isChurch_trans _ (rec_zero _ _ cb hcb) (ihf a₀ ca hca m hm) | succ k ih => intro m hm cb hcb rw [Code.eval_prec_succ] at hm @@ -219,24 +214,19 @@ private theorem prec_rec_correct (f g : Code) (tf tg : SKI) have hm_eq := Part.eq_some_iff.mpr hm_mem -- By IH, Rec computes the intermediate value on Pred ⬝ cb have hpred : IsChurch k (Pred ⬝ cb) := pred_correct (k + 1) cb hcb - obtain ⟨cih, hcih, hcih_red⟩ := ih ih_val hih_eq (Pred ⬝ cb) hpred + set step := PrecStep tg ⬝ ca + set base := tf ⬝ ca + have hcih := ih ih_val hih_eq (Pred ⬝ cb) hpred -- Build Church numeral for the argument to g - have hpair_inner := natPair_correct k ih_val (Pred ⬝ cb) cih hpred hcih + have hpair_inner := natPair_correct k ih_val (Pred ⬝ cb) + (Rec ⬝ base ⬝ step ⬝ (Pred ⬝ cb)) hpred hcih have hpair_full := natPair_correct a₀ (Nat.pair k ih_val) ca - (NatPair ⬝ (Pred ⬝ cb) ⬝ cih) hca hpair_inner + (NatPair ⬝ (Pred ⬝ cb) ⬝ (Rec ⬝ base ⬝ step ⬝ (Pred ⬝ cb))) hca hpair_inner -- By ihg, tg computes the result - obtain ⟨cm, hcm, hcm_red⟩ := ihg _ _ hpair_full m hm_eq + have hcm := ihg _ _ hpair_full m hm_eq -- Chain the reductions - set step := PrecStep tg ⬝ ca - set base := tf ⬝ ca - refine ⟨cm, hcm, ?_⟩ - calc - _ ↠ step ⬝ cb ⬝ (Rec ⬝ base ⬝ step ⬝ (Pred ⬝ cb)) := - rec_succ k base step cb hcb - _ ↠ step ⬝ cb ⬝ cih := MRed.tail _ hcih_red - _ ↠ tg ⬝ (NatPair ⬝ ca ⬝ (NatPair ⬝ (Pred ⬝ cb) ⬝ cih)) := - precStep_def tg ca cb cih - _ ↠ cm := hcm_red + exact isChurch_trans _ (Trans.trans (rec_succ k base step cb hcb) + (precStep_def tg ca cb (Rec ⬝ base ⬝ step ⬝ (Pred ⬝ cb)))) hcm /-- Helper: extract eval facts from rfind membership, with `m₀ +` order matching `rfind_above_induction`. -/ @@ -281,8 +271,7 @@ private theorem rfind_above_induction (f : Code) (tf : SKI) subst hg apply isChurch_trans _ (B_def tf (NatPair ⬝ ca) x) have hpair := natPair_correct a₀ m ca x hca hx - obtain ⟨cm, hcm, hred⟩ := ihf _ _ hpair 0 hroot - exact isChurch_trans 0 hred hcm + exact ihf _ _ hpair 0 hroot · exact hx | succ n ih => intro m x hx hroot hbelow @@ -296,10 +285,9 @@ private theorem rfind_above_induction (f : Code) (tf : SKI) subst hg apply isChurch_trans _ (B_def tf (NatPair ⬝ ca) x) have hpair := natPair_correct a₀ m ca x hca hx - obtain ⟨cm, hcm, hred⟩ := ihf _ _ hpair v₀ hv₀_eval have hv₀_pos : v₀ - 1 + 1 = v₀ := Nat.succ_pred_eq_of_ne_zero hv₀_ne rw [hv₀_pos] - exact isChurch_trans _ hred hcm + exact ihf _ _ hpair v₀ hv₀_eval · have h := ih (m + 1) (SKI.Succ ⬝ x) (succ_correct m x hx) (by rw [show m + 1 + n = m + (n + 1) from by omega]; exact hroot) (by @@ -333,10 +321,9 @@ theorem codeToSKINat_correct (c : Code) : Computes (codeToSKINat c) c.eval := by have hpair : n = Nat.pair (Nat.unpair n).1 (Nat.unpair n).2 := (Nat.pair_unpair n).symm rw [hpair] at hm - obtain ⟨cm, hcm, hcm_red⟩ := prec_rec_correct f g _ _ ihf ihg + exact isChurch_trans _ hred (prec_rec_correct f g _ _ ihf ihg (Nat.unpair n).1 (NatUnpairLeft ⬝ cn) hca - (Nat.unpair n).2 m hm (NatUnpairRight ⬝ cn) hcb - exact ⟨cm, hcm, Trans.trans hred hcm_red⟩ + (Nat.unpair n).2 m hm (NatUnpairRight ⬝ cn) hcb) | rfind' f ihf => simp only [codeToSKINat] intro n cn hcn result hresult @@ -360,7 +347,7 @@ theorem codeToSKINat_correct (c : Code) : Computes (codeToSKINat c) c.eval := by (NatUnpairLeft ⬝ cn) hca g rfl k m₀ (NatUnpairRight ⬝ cn) hcm₀ heval_root heval_below rw [Nat.add_comm] at hind - exact ⟨RFindAbove ⬝ (NatUnpairRight ⬝ cn) ⬝ g, hind, hred⟩ + exact isChurch_trans _ hred hind /-! ### Main equivalence theorem -/ From ee6cb30a4234bd18a77b1ee099559694a62ca18c Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Sat, 7 Mar 2026 15:02:07 +0100 Subject: [PATCH 03/13] style(PartrecEquivalence): add blank lines after defs and clarify docstrings --- .../CombinatoryLogic/PartrecEquivalence.lean | 20 ++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean b/Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean index d49681cc4..575ac8b7c 100644 --- a/Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean +++ b/Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean @@ -46,15 +46,23 @@ def Computes (t : SKI) (f : ℕ →. ℕ) : Prop := ∀ m : ℕ, f n = Part.some m → IsChurch m (t ⬝ cn) -/-! ### Helper terms for prec and rfind' translations -/ +/-! ### Helper terms for prec and rfind' translations + +These helpers adapt the `Rec` combinator from `Recursion.lean` for the paired encoding +used by `Nat.Partrec.Code.prec`, which passes arguments as `Nat.pair a (Nat.pair counter prev)`. +-/ /-- Step function for primitive recursion: `λ a cn prev. tg ⬝ (NatPair ⬝ a ⬝ (NatPair ⬝ (Pred ⬝ cn) ⬝ prev))` Variables: &0 = a, &1 = cn, &2 = prev -/ def PrecStepPoly (tg : SKI) : SKI.Polynomial 3 := tg ⬝' (NatPair ⬝' &0 ⬝' (NatPair ⬝' (Pred ⬝' &1) ⬝' &2)) -/-- SKI term for the primitive recursion step function. -/ + +/-- SKI term for the primitive recursion step function. Adapts `Rec`'s step argument +to `Code.prec`'s calling convention by repacking `(a, counter, prev_result)` into the +`Nat.pair a (Nat.pair (counter - 1) prev_result)` format expected by `tg`. -/ def PrecStep (tg : SKI) : SKI := (PrecStepPoly tg).toSKI + theorem precStep_def (tg a cn prev : SKI) : (PrecStep tg ⬝ a ⬝ cn ⬝ prev) ↠ tg ⬝ (NatPair ⬝ a ⬝ (NatPair ⬝ (Pred ⬝ cn) ⬝ prev)) := @@ -66,8 +74,12 @@ def PrecTransPoly (tf tg : SKI) : SKI.Polynomial 1 := Rec ⬝' (tf ⬝' (NatUnpairLeft ⬝' &0)) ⬝' (PrecStep tg ⬝' (NatUnpairLeft ⬝' &0)) ⬝' (NatUnpairRight ⬝' &0) -/-- SKI term for primitive recursion. -/ + +/-- SKI term for primitive recursion. Delegates to the `Rec` combinator from `Recursion.lean`, +using pair/unpair plumbing to translate between `Nat.Partrec.Code.prec`'s paired input +convention (`Nat.pair a n`) and `Rec`'s direct arguments `(base, step, n)`. -/ def PrecTrans (tf tg : SKI) : SKI := (PrecTransPoly tf tg).toSKI + theorem precTrans_def (tf tg cn : SKI) : (PrecTrans tf tg ⬝ cn) ↠ Rec ⬝ (tf ⬝ (NatUnpairLeft ⬝ cn)) @@ -80,8 +92,10 @@ theorem precTrans_def (tf tg cn : SKI) : def RFindTransPoly (tf : SKI) : SKI.Polynomial 1 := RFindAbove ⬝' (NatUnpairRight ⬝' &0) ⬝' (B ⬝' tf ⬝' (NatPair ⬝' (NatUnpairLeft ⬝' &0))) + /-- SKI term for unbounded search (μ-recursion). -/ def RFindTrans (tf : SKI) : SKI := (RFindTransPoly tf).toSKI + theorem rfindTrans_def (tf cn : SKI) : (RFindTrans tf ⬝ cn) ↠ RFindAbove ⬝ (NatUnpairRight ⬝ cn) From 2c9b49cf77973227a74e6630b159d683664674c3 Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Thu, 19 Mar 2026 10:19:50 +0100 Subject: [PATCH 04/13] style(CombinatoryLogic): trim docs, simplify proofs, fix naming conventions Shorten verbose docstrings, collapse rw/have/subst patterns to obtain rfl, extract inline calc blocks, and rename to camelCase (natPartrec_skiComputable, rfindAbove_induction). --- .../CombinatoryLogic/PartrecEquivalence.lean | 61 +-- .../CombinatoryLogic/SKIPartrec.lean | 455 ++++++++++++++++++ 2 files changed, 476 insertions(+), 40 deletions(-) create mode 100644 Cslib/Languages/CombinatoryLogic/SKIPartrec.lean diff --git a/Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean b/Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean index 575ac8b7c..e7fb6ebda 100644 --- a/Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean +++ b/Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean @@ -25,7 +25,7 @@ This file defines a notion of computability for SKI terms on natural numbers ## Main results - `codeToSKINat_correct`: each translated code computes the corresponding `Code.eval`. -- `nat_partrec_ski_computable`: every `Nat.Partrec` function is SKI-computable. +- `natPartrec_skiComputable`: every `Nat.Partrec` function is SKI-computable. -/ @@ -46,11 +46,7 @@ def Computes (t : SKI) (f : ℕ →. ℕ) : Prop := ∀ m : ℕ, f n = Part.some m → IsChurch m (t ⬝ cn) -/-! ### Helper terms for prec and rfind' translations - -These helpers adapt the `Rec` combinator from `Recursion.lean` for the paired encoding -used by `Nat.Partrec.Code.prec`, which passes arguments as `Nat.pair a (Nat.pair counter prev)`. --/ +/-! ### Helper terms for `Code.prec` and `Code.rfind'` -/ /-- Step function for primitive recursion: `λ a cn prev. tg ⬝ (NatPair ⬝ a ⬝ (NatPair ⬝ (Pred ⬝ cn) ⬝ prev))` @@ -58,9 +54,7 @@ used by `Nat.Partrec.Code.prec`, which passes arguments as `Nat.pair a (Nat.pair def PrecStepPoly (tg : SKI) : SKI.Polynomial 3 := tg ⬝' (NatPair ⬝' &0 ⬝' (NatPair ⬝' (Pred ⬝' &1) ⬝' &2)) -/-- SKI term for the primitive recursion step function. Adapts `Rec`'s step argument -to `Code.prec`'s calling convention by repacking `(a, counter, prev_result)` into the -`Nat.pair a (Nat.pair (counter - 1) prev_result)` format expected by `tg`. -/ +/-- SKI term for the primitive recursion step function. -/ def PrecStep (tg : SKI) : SKI := (PrecStepPoly tg).toSKI theorem precStep_def (tg a cn prev : SKI) : @@ -75,9 +69,7 @@ def PrecTransPoly (tf tg : SKI) : SKI.Polynomial 1 := ⬝' (PrecStep tg ⬝' (NatUnpairLeft ⬝' &0)) ⬝' (NatUnpairRight ⬝' &0) -/-- SKI term for primitive recursion. Delegates to the `Rec` combinator from `Recursion.lean`, -using pair/unpair plumbing to translate between `Nat.Partrec.Code.prec`'s paired input -convention (`Nat.pair a n`) and `Rec`'s direct arguments `(base, step, n)`. -/ +/-- SKI term for primitive recursion via `Rec` with pair/unpair plumbing. -/ def PrecTrans (tf tg : SKI) : SKI := (PrecTransPoly tf tg).toSKI theorem precTrans_def (tf tg cn : SKI) : @@ -128,9 +120,7 @@ theorem zero_computes : Computes (K ⬝ SKI.Zero) (Code.eval .zero) := by intro n cn hcn m hm have h0 : Code.eval .zero n = Part.some 0 := by rw [show Code.zero = Code.const 0 from rfl, Code.eval_const] - rw [h0] at hm - have heq : (0 : ℕ) = m := Part.some_injective hm - subst heq + rw [h0] at hm; obtain rfl := Part.some_injective hm exact isChurch_trans 0 (MRed.K SKI.Zero cn) zero_correct /-- `Code.succ` computes the successor function. -/ @@ -138,9 +128,7 @@ theorem succ_computes : Computes SKI.Succ (Code.eval .succ) := by intro n cn hcn m hm have h0 : Code.eval .succ n = Part.some (n + 1) := by simp only [Code.eval, PFun.coe_val] - rw [h0] at hm - have heq : n + 1 = m := Part.some_injective hm - subst heq + rw [h0] at hm; obtain rfl := Part.some_injective hm exact succ_correct n cn hcn /-- `Code.left` computes the left projection of `Nat.unpair`. -/ @@ -148,9 +136,7 @@ theorem left_computes : Computes NatUnpairLeft (Code.eval .left) := by intro n cn hcn m hm have h0 : Code.eval .left n = Part.some (Nat.unpair n).1 := by simp only [Code.eval, PFun.coe_val] - rw [h0] at hm - have heq := Part.some_injective hm - subst heq + rw [h0] at hm; obtain rfl := Part.some_injective hm exact natUnpairLeft_correct n cn hcn /-- `Code.right` computes the right projection of `Nat.unpair`. -/ @@ -158,9 +144,7 @@ theorem right_computes : Computes NatUnpairRight (Code.eval .right) := by intro n cn hcn m hm have h0 : Code.eval .right n = Part.some (Nat.unpair n).2 := by simp only [Code.eval, PFun.coe_val] - rw [h0] at hm - have heq := Part.some_injective hm - subst heq + rw [h0] at hm; obtain rfl := Part.some_injective hm exact natUnpairRight_correct n cn hcn /-- Composition of computable functions is computable. -/ @@ -197,10 +181,11 @@ theorem pair_computes {f g : ℕ →. ℕ} {tf tg : SKI} have hca := hf n cn hcn a hfn have hcb := hg n cn hcn b hgn subst hm_eq - exact isChurch_trans _ (calc (S ⬝ (B ⬝ NatPair ⬝ tf) ⬝ tg ⬝ cn) - ↠ ((B ⬝ NatPair ⬝ tf) ⬝ cn ⬝ (tg ⬝ cn)) := MRed.S _ _ _ - _ ↠ (NatPair ⬝ (tf ⬝ cn) ⬝ (tg ⬝ cn)) := MRed.head _ (B_def _ _ _)) - (natPair_correct a b (tf ⬝ cn) (tg ⬝ cn) hca hcb) + have hred : (S ⬝ (B ⬝ NatPair ⬝ tf) ⬝ tg ⬝ cn) ↠ + (NatPair ⬝ (tf ⬝ cn) ⬝ (tg ⬝ cn)) := calc + _ ↠ (B ⬝ NatPair ⬝ tf) ⬝ cn ⬝ (tg ⬝ cn) := MRed.S _ _ _ + _ ↠ NatPair ⬝ (tf ⬝ cn) ⬝ (tg ⬝ cn) := MRed.head _ (B_def _ _ _) + exact isChurch_trans _ hred (natPair_correct a b _ _ hca hcb) /-- Helper: `Rec` correctly implements primitive recursion from `Code.prec`. -/ private theorem prec_rec_correct (f g : Code) (tf tg : SKI) @@ -239,11 +224,11 @@ private theorem prec_rec_correct (f g : Code) (tf tg : SKI) -- By ihg, tg computes the result have hcm := ihg _ _ hpair_full m hm_eq -- Chain the reductions - exact isChurch_trans _ (Trans.trans (rec_succ k base step cb hcb) - (precStep_def tg ca cb (Rec ⬝ base ⬝ step ⬝ (Pred ⬝ cb)))) hcm + have hred := (rec_succ k base step cb hcb).trans + (precStep_def tg ca cb (Rec ⬝ base ⬝ step ⬝ (Pred ⬝ cb))) + exact isChurch_trans _ hred hcm -/-- Helper: extract eval facts from rfind membership, with `m₀ +` order - matching `rfind_above_induction`. -/ +/-- Extract eval facts from `Nat.rfind` membership. -/ private theorem rfind_eval_facts {f : Code} {a₀ m₀ k : ℕ} (hk : k ∈ Nat.rfind (fun n => (fun m => decide (m = 0)) <$> f.eval (Nat.pair a₀ (n + m₀)))) : @@ -264,7 +249,7 @@ private theorem rfind_eval_facts {f : Code} {a₀ m₀ k : ℕ} /-- Helper: `RFindAbove` correctly implements `Code.rfind'` by induction on the number of steps until the root. -/ -private theorem rfind_above_induction (f : Code) (tf : SKI) +private theorem rfindAbove_induction (f : Code) (tf : SKI) (ihf : Computes tf f.eval) (a₀ : ℕ) (ca : SKI) (hca : IsChurch a₀ ca) (g : SKI) (hg : g = B ⬝ tf ⬝ (NatPair ⬝ ca)) : ∀ n m : ℕ, ∀ x : SKI, IsChurch m x → @@ -357,7 +342,7 @@ theorem codeToSKINat_correct (c : Code) : Computes (codeToSKINat c) c.eval := by subst hresult_eq obtain ⟨heval_root, heval_below⟩ := rfind_eval_facts hk_mem set g := B ⬝ tf ⬝ (NatPair ⬝ (NatUnpairLeft ⬝ cn)) - have hind := rfind_above_induction f tf ihf a₀ + have hind := rfindAbove_induction f tf ihf a₀ (NatUnpairLeft ⬝ cn) hca g rfl k m₀ (NatUnpairRight ⬝ cn) hcm₀ heval_root heval_below rw [Nat.add_comm] at hind @@ -365,12 +350,8 @@ theorem codeToSKINat_correct (c : Code) : Computes (codeToSKINat c) c.eval := by /-! ### Main equivalence theorem -/ -/-- Every partial recursive function `f : ℕ →. ℕ` is SKI-computable. - -This establishes that SKI combinatory logic can compute all partial recursive -functions on ℕ. --/ -theorem nat_partrec_ski_computable (f : ℕ →. ℕ) (hf : Nat.Partrec f) : +/-- Every partial recursive function on `ℕ` is SKI-computable. -/ +theorem natPartrec_skiComputable (f : ℕ →. ℕ) (hf : Nat.Partrec f) : ∃ t : SKI, Computes t f := by obtain ⟨c, hc⟩ := Code.exists_code.mp hf exact ⟨codeToSKINat c, hc ▸ codeToSKINat_correct c⟩ diff --git a/Cslib/Languages/CombinatoryLogic/SKIPartrec.lean b/Cslib/Languages/CombinatoryLogic/SKIPartrec.lean new file mode 100644 index 000000000..c88c86eab --- /dev/null +++ b/Cslib/Languages/CombinatoryLogic/SKIPartrec.lean @@ -0,0 +1,455 @@ +/- +Copyright (c) 2026 Jesse Alama. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jesse Alama +-/ + +module + +public import Cslib.Languages.CombinatoryLogic.Evaluation +public import Cslib.Languages.CombinatoryLogic.PartrecEquivalence +public import Mathlib.Computability.PartrecCode + +@[expose] public section + +/-! +# SKI-computable → Nat.Partrec (reverse direction) + +This file proves the reverse direction of the SKI ↔ Partrec equivalence: +every function computed by an SKI term is partial recursive. + +## Main definitions + +- `SKI.encodeSKI` / `SKI.ofNatSKI`: encoding/decoding of SKI terms as natural numbers. +- `SKI.extractChurchK`: extract the natural number from a `churchK` normal form. +- `SKI.evalStepFn`: one step of evaluation as a total function (identity on normal forms). +- `SKI.evalNat`: the partial function `ℕ →. ℕ` computed by an SKI term. + +## Main results + +- `SKI.ski_eval_partrec`: the function computed by any SKI term is `Nat.Partrec`. +- `SKI.Computes.le_evalNat`: compatibility of `Computes` with `evalNat`. +- `SKI.partrec_iff_ski_evalNat`: equivalence of `Nat.Partrec` and SKI-computability. +-/ + +namespace Cslib + +namespace SKI + +open Red MRed Relation +open Nat.Partrec + +/-! ### Encoding SKI terms as natural numbers -/ + +/-- Encode an SKI term as a natural number. +- `S → 0`, `K → 1`, `I → 2` +- `app a b → Nat.pair (encodeSKI a) (encodeSKI b) + 3` -/ +def encodeSKI : SKI → ℕ + | S => 0 + | K => 1 + | I => 2 + | a ⬝ b => Nat.pair (encodeSKI a) (encodeSKI b) + 3 + +/-- Decode a natural number to an SKI term. Total function (every `ℕ` maps to some SKI term). +Follows Mathlib's pattern for `ofNatCode` with inline termination proofs. -/ +def ofNatSKI : ℕ → SKI + | 0 => S + | 1 => K + | 2 => I + | n + 3 => + have : n.unpair.1 < n + 3 := + Nat.lt_of_le_of_lt (Nat.unpair_left_le n) (by omega) + have : n.unpair.2 < n + 3 := + Nat.lt_of_le_of_lt (Nat.unpair_right_le n) (by omega) + ofNatSKI n.unpair.1 ⬝ ofNatSKI n.unpair.2 + +@[simp] +theorem ofNatSKI_encodeSKI (t : SKI) : ofNatSKI (encodeSKI t) = t := by + induction t with + | S => simp [encodeSKI, ofNatSKI] + | K => simp [encodeSKI, ofNatSKI] + | I => simp [encodeSKI, ofNatSKI] + | app a b iha ihb => unfold encodeSKI ofNatSKI; simp [iha, ihb] + +@[simp] +theorem encodeSKI_ofNatSKI (n : ℕ) : encodeSKI (ofNatSKI n) = n := by + induction n using Nat.strongRecOn with + | _ n ih => + match n with + | 0 => simp [ofNatSKI, encodeSKI] + | 1 => simp [ofNatSKI, encodeSKI] + | 2 => simp [ofNatSKI, encodeSKI] + | n + 3 => + unfold ofNatSKI + simp only [encodeSKI] + have h1 : n.unpair.1 ≤ n := Nat.unpair_left_le n + have h2 : n.unpair.2 ≤ n := Nat.unpair_right_le n + rw [ih n.unpair.1 (by omega), ih n.unpair.2 (by omega), Nat.pair_unpair] + +/-- The encoding/decoding defines an equivalence `SKI ≃ ℕ`. -/ +def equivNat : SKI ≃ ℕ where + toFun := encodeSKI + invFun := ofNatSKI + left_inv := ofNatSKI_encodeSKI + right_inv := encodeSKI_ofNatSKI + +instance : Denumerable SKI := Denumerable.mk' equivNat + +@[simp] +theorem encode_eq_encodeSKI (t : SKI) : Encodable.encode t = encodeSKI t := rfl + +@[simp] +theorem ofNat_eq_ofNatSKI (n : ℕ) : Denumerable.ofNat SKI n = ofNatSKI n := rfl + +/-! ### Extracting values from churchK normal forms -/ + +/-- Extract the natural number from a `churchK` normal form. +`churchK 0 = K`, `churchK (n+1) = K ⬝ churchK n`. -/ +def extractChurchK : SKI → Option ℕ + | K => some 0 + | K ⬝ x => (extractChurchK x).map (· + 1) + | _ => none + +@[simp] +theorem extractChurchK_churchK (n : ℕ) : extractChurchK (churchK n) = some n := by + induction n with + | zero => rfl + | succ n ih => simp [churchK, extractChurchK, ih] + +theorem extractChurchK_some {t : SKI} {m : ℕ} (h : extractChurchK t = some m) : + t = churchK m := by + induction t generalizing m with + | S => simp [extractChurchK] at h + | K => + simp only [extractChurchK] at h + cases h; rfl + | I => simp [extractChurchK] at h + | app a b _ ih_b => + match a with + | K => + simp only [extractChurchK, Option.map_eq_some_iff] at h + obtain ⟨m', hm', rfl⟩ := h + have hb := ih_b hm' + subst hb + simp [churchK] + | S => simp [extractChurchK] at h + | I => simp [extractChurchK] at h + | _ ⬝ _ => simp [extractChurchK] at h + +/-! ### One-step evaluation as a total function -/ + +/-- One step of evaluation, returning the same term if already in normal form. -/ +def evalStepFn (t : SKI) : SKI := + match t.evalStep with + | .inl _ => t + | .inr t' => t' + +theorem evalStepFn_of_redexFree {t : SKI} (h : t.RedexFree) : + evalStepFn t = t := by + simp only [evalStepFn] + have : (t.evalStep).isLeft = true := redexFree_iff_evalStep.mp h + match ht : t.evalStep with + | .inl _ => rfl + | .inr _ => rw [ht] at this; cases this + +theorem evalStepFn_red {t : SKI} (h : ¬t.RedexFree) : + t ⭢ evalStepFn t := by + simp only [evalStepFn] + have : ¬(t.evalStep).isLeft = true := fun h' => h (redexFree_iff_evalStep.mpr h') + match ht : t.evalStep with + | .inl _ => rw [ht] at this; exact absurd rfl this + | .inr t' => exact evalStep_right_correct t t' ht + +/-- Iterating `evalStepFn` k times gives a multi-step reduction. -/ +theorem iterate_evalStepFn_mred (t : SKI) (k : ℕ) : + t ↠ evalStepFn^[k] t := by + induction k with + | zero => exact .refl + | succ k ih => + rw [Function.iterate_succ_apply'] + set t' := evalStepFn^[k] t with ht' + by_cases hrf : t'.RedexFree + · rw [evalStepFn_of_redexFree hrf]; exact ih + · exact Trans.trans ih (ReflTransGen.single (evalStepFn_red hrf)) + +/-- Once a term reaches a normal form, further iterations don't change it. -/ +theorem iterate_evalStepFn_stable {t : SKI} (h : t.RedexFree) (k : ℕ) : + evalStepFn^[k] t = t := by + induction k with + | zero => rfl + | succ k ih => + rw [Function.iterate_succ_apply', ih] + exact evalStepFn_of_redexFree h + +/-! ### The partial function computed by an SKI term -/ + +/-- The partial function `ℕ →. ℕ` computed by an SKI term `t`. + +Given input `n`, we: +1. Build `t ⬝ toChurch(n) ⬝ K ⬝ K` +2. Iterate `evalStepFn` to search for a normal form +3. If the normal form matches `churchK m`, return `m` -/ +noncomputable def evalNat (t : SKI) : ℕ →. ℕ := fun n => + Nat.rfindOpt (fun k => + extractChurchK (evalStepFn^[k] (t ⬝ toChurch n ⬝ K ⬝ K))) + +/-! ### Key lemma: normal-order reduction reaches normal forms -/ + +/-- If `t ↠ nf` and `nf` is redex-free, then iterating `evalStepFn` eventually reaches `nf`. + +This is the **standardization theorem** for SKI combinatory logic: normal-order +reduction (as implemented by `evalStep`) is normalizing — if a term has a normal form, +normal-order reduction finds it. + +The proof requires showing that the specific evaluation strategy in `evalStep` +(leftmost-outermost / head reduction) avoids infinite loops when a normal form exists. +This is a deep result; see e.g. Curry & Feys (1958) or Hindley & Seldin (2008). -/ +theorem exists_iterate_of_mred_redexFree {t nf : SKI} + (hred : t ↠ nf) (hnf : nf.RedexFree) : + ∃ k, evalStepFn^[k] t = nf := by + sorry + +/-! ### Monotonicity of the evaluation sequence -/ + +/-- Once `extractChurchK` succeeds at step `k`, it also succeeds at step `k'` for `k ≤ k'` +with the same result, because churchK values are redex-free and stable under iteration. -/ +theorem extractChurchK_iterate_mono {t : SKI} {m k : ℕ} + (hk : extractChurchK (evalStepFn^[k] t) = some m) + {k' : ℕ} (hle : k ≤ k') : + extractChurchK (evalStepFn^[k'] t) = some m := by + have heq := extractChurchK_some hk + rw [show k' = (k' - k) + k from by omega, Function.iterate_add_apply, heq, + iterate_evalStepFn_stable (churchK_redexFree m), extractChurchK_churchK] + +/-! ### Correctness: Computes t f → f ≤ evalNat t -/ + +/-- If `Computes t f`, then wherever `f` is defined, `evalNat t` agrees. -/ +theorem Computes.le_evalNat {t : SKI} {f : ℕ →. ℕ} (hc : Computes t f) : + ∀ n m, f n = Part.some m → evalNat t n = Part.some m := by + intro n m hfn + -- From Computes, get cm with IsChurch m cm and (t ⬝ toChurch n) ↠ cm + obtain ⟨cm, hcm, hred⟩ := hc n (toChurch n) (toChurch_correct n) m hfn + -- t ⬝ toChurch n ⬝ K ⬝ K ↠ cm ⬝ K ⬝ K ↠ Church m K K = churchK m + have h_full : (t ⬝ toChurch n ⬝ K ⬝ K) ↠ churchK m := + Trans.trans (parallel_mRed (MRed.head K hred) .refl) + (churchK_church m ▸ hcm K K) + -- Find k such that iteration reaches churchK m + obtain ⟨k, hk⟩ := exists_iterate_of_mred_redexFree h_full (churchK_redexFree m) + -- evalNat uses rfindOpt; at step k, extractChurchK succeeds + simp only [evalNat] + rw [Part.eq_some_iff] + apply (Nat.rfindOpt_mono + (fun {_ _ _} hle hm => extractChurchK_iterate_mono hm hle)).mpr + exact ⟨k, by rw [hk, extractChurchK_churchK]; rfl⟩ + +/-! ### Computability: evalNat t is Nat.Partrec -/ + +section Computability + +/-- Encoding of `evalStepFn` operating directly on natural numbers. -/ +def evalStepNat : ℕ → ℕ := fun n => encodeSKI (evalStepFn (ofNatSKI n)) + +/-- The encoding of `toChurch n` as a natural number. -/ +def toChurchNat : ℕ → ℕ := fun n => encodeSKI (toChurch n) + +/-- The encoding of `extractChurchK` operating on encoded terms. -/ +def extractChurchKNat : ℕ → Option ℕ := fun n => extractChurchK (ofNatSKI n) + +/-- `evalStepNat` correctly encodes `evalStepFn`. -/ +theorem evalStepNat_correct (t : SKI) : + evalStepNat (encodeSKI t) = encodeSKI (evalStepFn t) := by + simp [evalStepNat] + +/-- `extractChurchKNat` correctly encodes `extractChurchK`. -/ +theorem extractChurchKNat_correct (t : SKI) : + extractChurchKNat (encodeSKI t) = extractChurchK t := by + simp [extractChurchKNat] + +/-- The iterate of `evalStepNat` correctly encodes the iterate of `evalStepFn`. -/ +theorem iterate_evalStepNat_correct (t : SKI) (k : ℕ) : + evalStepNat^[k] (encodeSKI t) = + encodeSKI (evalStepFn^[k] t) := by + induction k with + | zero => rfl + | succ k ih => + rw [Function.iterate_succ_apply', Function.iterate_succ_apply', ih, + evalStepNat_correct] + +/-! #### Primrec helpers (no sorry dependencies) -/ + +/-- Application on SKI terms is primitive recursive. -/ +private theorem primrec_app : Primrec₂ (· ⬝ · : SKI → SKI → SKI) := + ((Primrec.ofNat SKI).comp + (Primrec.nat_add.comp + (Primrec₂.natPair.comp + (Primrec.encode.comp .fst) (Primrec.encode.comp .snd)) + (Primrec.const 3))).of_eq + fun ⟨a, b⟩ => by + simp only [ofNat_eq_ofNatSKI, encode_eq_encodeSKI] + change ofNatSKI (encodeSKI (a ⬝ b)) = _ + simp + +/-- `toChurch` is primitive recursive. -/ +private theorem primrec_toChurch : Primrec toChurch := + (Primrec.nat_iterate .id (.const (K ⬝ I)) + ((primrec_app.comp (.const SKI.Succ) .snd).to₂)).of_eq + fun n => by + change (fun x => SKI.Succ ⬝ x)^[n] (K ⬝ I) = toChurch n + induction n with + | zero => rfl + | succ n ih => rw [Function.iterate_succ_apply', ih, toChurch] + +/-! #### Helper lemmas for computability proofs -/ + +/-- Encoding of `Option.map (· + 1)` in terms of the encoded option. -/ +private theorem encode_option_map_succ (o : Option ℕ) : + Encodable.encode (o.map (· + 1)) = + if Encodable.encode o = 0 then 0 else Encodable.encode o + 1 := by + cases o <;> simp + +/-- `extractChurchK` returns `none` for applications whose left child is not `K`. -/ +private theorem extractChurchK_app_neK {a b : SKI} (h : a ≠ K) : + extractChurchK (a ⬝ b) = Option.none := by + cases a with + | K => exact absurd rfl h + | S => rfl + | I => rfl + | app c d => rfl + +/-! #### Nat.Primrec theorems -/ + +/-- Encoding of Church numerals is primitive recursive. -/ +theorem nat_primrec_toChurchNat : Nat.Primrec toChurchNat := + Primrec.nat_iff.mp (Primrec.encode.comp primrec_toChurch) + +/-- One step of SKI evaluation on encoded terms is primitive recursive. + +This requires showing that the pattern matching in `evalStep` — which dispatches on the +top-level structure of the SKI term (S/K/I/app) and performs the appropriate reduction — +can be expressed as a primitive recursive function on the natural number encoding. +The proof would involve ~150-250 lines of careful case analysis on the encoding. -/ +theorem nat_primrec_evalStepNat : Nat.Primrec evalStepNat := by + sorry + +/-- Extraction from churchK on encoded terms is primitive recursive. + +Uses course-of-values recursion (`Primrec.nat_strong_rec`): the value at `n ≥ 3` +depends on the value at `(n - 3).unpair.2 < n`. -/ +theorem nat_primrec_extractChurchKNat : + Nat.Primrec fun n => Encodable.encode (extractChurchKNat n) := by + rw [← Primrec.nat_iff] + -- Define the body for course-of-values recursion + let body : List ℕ → ℕ := fun hist => + if hist.length = 1 then 1 + else if 3 ≤ hist.length ∧ (hist.length - 3).unpair.1 = 1 then + if (hist[(hist.length - 3).unpair.2]?).getD 0 = 0 then 0 + else (hist[(hist.length - 3).unpair.2]?).getD 0 + 1 + else 0 + -- Show body is Primrec + have h_body : Primrec body := by + have len : Primrec (List.length : List ℕ → ℕ) := Primrec.list_length + have sub3 := Primrec.nat_sub.comp len (Primrec.const 3) + have unp := Primrec.unpair.comp sub3 + have unp1 := Primrec.fst.comp unp + have unp2 := Primrec.snd.comp unp + have lkup : Primrec (fun hist : List ℕ => (hist[(hist.length - 3).unpair.2]?).getD 0) := + Primrec.option_getD.comp (Primrec.list_getElem?.comp Primrec.id unp2) (Primrec.const 0) + exact Primrec.ite (Primrec.eq.comp len (Primrec.const 1)) (Primrec.const 1) + (Primrec.ite + (PrimrecPred.and (Primrec.nat_le.comp (Primrec.const 3) len) + (Primrec.eq.comp unp1 (Primrec.const 1))) + (Primrec.ite (Primrec.eq.comp lkup (Primrec.const 0)) + (Primrec.const 0) (Primrec.succ.comp lkup)) + (Primrec.const 0)) + -- Apply course-of-values recursion + exact (Primrec.nat_strong_rec + (fun (_ : PUnit) n => Encodable.encode (extractChurchKNat n)) + (g := fun _ hist => some (body hist)) + (Primrec.option_some.comp (h_body.comp Primrec.snd)) + (by + intro () n + simp only [body, List.length_map, List.length_range] + congr 1 + rcases n with _ | _ | _ | n + · simp [extractChurchKNat, ofNatSKI, extractChurchK] + · simp [extractChurchKNat, ofNatSKI, extractChurchK] + · simp [extractChurchKNat, ofNatSKI, extractChurchK] + · simp only [show ¬(n + 3 = 1) from by omega, ite_false, + show 3 ≤ n + 3 from by omega, true_and, show n + 3 - 3 = n from by omega, + extractChurchKNat, ofNatSKI] + by_cases h : n.unpair.1 = 1 + · have hK : ofNatSKI 1 = K := by unfold ofNatSKI; rfl + simp only [h, ite_true, hK, extractChurchK] + have h_lt : n.unpair.2 < n + 3 := + Nat.lt_of_le_of_lt (Nat.unpair_right_le n) (by omega) + simp only [List.getElem?_map, List.getElem?_range h_lt, Option.map_some, + Option.getD_some] + exact (encode_option_map_succ (extractChurchKNat n.unpair.2)).symm + · simp only [h, ite_false] + have : ofNatSKI n.unpair.1 ≠ K := by + intro heq + exact h ((encodeSKI_ofNatSKI _).symm.trans (congrArg encodeSKI heq)) + simp [extractChurchK_app_neK this])).comp (Primrec.const ()) Primrec.id + +/-! #### Converting Nat.Primrec to Primrec on SKI -/ + +/-- `evalStepFn` is primitive recursive. -/ +private theorem primrec_evalStepFn : Primrec evalStepFn := + ((Primrec.ofNat SKI).comp + ((Primrec.nat_iff.mpr nat_primrec_evalStepNat).comp Primrec.encode)).of_eq + fun t => by simp [evalStepNat] + +/-- `extractChurchK` is primitive recursive. -/ +private theorem primrec_extractChurchK : Primrec extractChurchK := + (Primrec.encode_iff.mp <| + (Primrec.nat_iff.mpr nat_primrec_extractChurchKNat).comp Primrec.encode).of_eq + fun t => by simp [extractChurchKNat] + +/-- The function computed by any SKI term is partial recursive. -/ +theorem ski_eval_partrec (t : SKI) : Nat.Partrec (evalNat t) := by + rw [← Partrec.nat_iff] + change Partrec fun n => Nat.rfindOpt fun k => + extractChurchK (evalStepFn^[k] (t ⬝ toChurch n ⬝ K ⬝ K)) + apply Partrec.rfindOpt + -- Need: Computable₂ (fun n k => extractChurchK (evalStepFn^[k] (t ⬝ toChurch n ⬝ K ⬝ K))) + apply Primrec₂.to_comp + exact primrec_extractChurchK.comp + (Primrec.nat_iterate .snd + (primrec_app.comp (primrec_app.comp (primrec_app.comp + (Primrec.const t) (primrec_toChurch.comp .fst)) + (Primrec.const K)) (Primrec.const K)) + (primrec_evalStepFn.comp₂ Primrec₂.right)) + +end Computability + +/-! ### Combined equivalence -/ + +/-- Every partial recursive function has an SKI term whose `evalNat` agrees wherever `f` +is defined. This is weaker than full equality `evalNat t = f` but follows directly from +`Computes.le_evalNat` and `natPartrec_skiComputable`. -/ +theorem nat_partrec_le_ski_evalNat {f : ℕ →. ℕ} (hf : Nat.Partrec f) : + ∃ t : SKI, ∀ n m, f n = Part.some m → evalNat t n = Part.some m := + let ⟨t, ht⟩ := natPartrec_skiComputable f hf + ⟨t, ht.le_evalNat⟩ + +/-- Full equivalence: a function is `Nat.Partrec` iff it is the function computed +by some SKI term. + +The forward direction requires showing that the SKI term produced by `codeToSKINat` +computes *exactly* `f` (not just agreeing where `f` is defined). This needs a stronger +`ComputesExact` property of the construction: the term does not reduce to a Church +numeral on inputs where `f` is undefined. -/ +theorem partrec_iff_ski_evalNat {f : ℕ →. ℕ} : + Nat.Partrec f ↔ ∃ t : SKI, evalNat t = f := by + constructor + · intro hf + obtain ⟨t, ht⟩ := natPartrec_skiComputable f hf + -- ht.le_evalNat gives: wherever f is defined, evalNat t agrees. + -- The missing piece: evalNat t is undefined wherever f is. + exact ⟨t, sorry⟩ + · rintro ⟨t, rfl⟩ + exact ski_eval_partrec t + +end SKI + +end Cslib From 1af3c6172fca68fadff43dca268cccdc7692e728 Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Thu, 19 Mar 2026 16:11:02 +0100 Subject: [PATCH 05/13] =?UTF-8?q?refactor(CombinatoryLogic):=20rename=20Pa?= =?UTF-8?q?rtrecEquivalence=20=E2=86=92=20PartrecToSKI?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Only one direction (Partrec → SKI) is proven; rename file and section header to avoid overclaiming equivalence. Remove unrelated SKIPartrec stub (converse direction) to a separate branch. --- Cslib.lean | 2 +- ...trecEquivalence.lean => PartrecToSKI.lean} | 2 +- .../CombinatoryLogic/SKIPartrec.lean | 455 ------------------ 3 files changed, 2 insertions(+), 457 deletions(-) rename Cslib/Languages/CombinatoryLogic/{PartrecEquivalence.lean => PartrecToSKI.lean} (99%) delete mode 100644 Cslib/Languages/CombinatoryLogic/SKIPartrec.lean diff --git a/Cslib.lean b/Cslib.lean index 5a97679e6..94e683ade 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -78,7 +78,7 @@ public import Cslib.Languages.CombinatoryLogic.Confluence public import Cslib.Languages.CombinatoryLogic.Defs public import Cslib.Languages.CombinatoryLogic.Evaluation public import Cslib.Languages.CombinatoryLogic.List -public import Cslib.Languages.CombinatoryLogic.PartrecEquivalence +public import Cslib.Languages.CombinatoryLogic.PartrecToSKI public import Cslib.Languages.CombinatoryLogic.Recursion public import Cslib.Languages.LambdaCalculus.LocallyNameless.Context public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic diff --git a/Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean b/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean similarity index 99% rename from Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean rename to Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean index e7fb6ebda..12df72b60 100644 --- a/Cslib/Languages/CombinatoryLogic/PartrecEquivalence.lean +++ b/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean @@ -348,7 +348,7 @@ theorem codeToSKINat_correct (c : Code) : Computes (codeToSKINat c) c.eval := by rw [Nat.add_comm] at hind exact isChurch_trans _ hred hind -/-! ### Main equivalence theorem -/ +/-! ### Main result -/ /-- Every partial recursive function on `ℕ` is SKI-computable. -/ theorem natPartrec_skiComputable (f : ℕ →. ℕ) (hf : Nat.Partrec f) : diff --git a/Cslib/Languages/CombinatoryLogic/SKIPartrec.lean b/Cslib/Languages/CombinatoryLogic/SKIPartrec.lean deleted file mode 100644 index c88c86eab..000000000 --- a/Cslib/Languages/CombinatoryLogic/SKIPartrec.lean +++ /dev/null @@ -1,455 +0,0 @@ -/- -Copyright (c) 2026 Jesse Alama. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jesse Alama --/ - -module - -public import Cslib.Languages.CombinatoryLogic.Evaluation -public import Cslib.Languages.CombinatoryLogic.PartrecEquivalence -public import Mathlib.Computability.PartrecCode - -@[expose] public section - -/-! -# SKI-computable → Nat.Partrec (reverse direction) - -This file proves the reverse direction of the SKI ↔ Partrec equivalence: -every function computed by an SKI term is partial recursive. - -## Main definitions - -- `SKI.encodeSKI` / `SKI.ofNatSKI`: encoding/decoding of SKI terms as natural numbers. -- `SKI.extractChurchK`: extract the natural number from a `churchK` normal form. -- `SKI.evalStepFn`: one step of evaluation as a total function (identity on normal forms). -- `SKI.evalNat`: the partial function `ℕ →. ℕ` computed by an SKI term. - -## Main results - -- `SKI.ski_eval_partrec`: the function computed by any SKI term is `Nat.Partrec`. -- `SKI.Computes.le_evalNat`: compatibility of `Computes` with `evalNat`. -- `SKI.partrec_iff_ski_evalNat`: equivalence of `Nat.Partrec` and SKI-computability. --/ - -namespace Cslib - -namespace SKI - -open Red MRed Relation -open Nat.Partrec - -/-! ### Encoding SKI terms as natural numbers -/ - -/-- Encode an SKI term as a natural number. -- `S → 0`, `K → 1`, `I → 2` -- `app a b → Nat.pair (encodeSKI a) (encodeSKI b) + 3` -/ -def encodeSKI : SKI → ℕ - | S => 0 - | K => 1 - | I => 2 - | a ⬝ b => Nat.pair (encodeSKI a) (encodeSKI b) + 3 - -/-- Decode a natural number to an SKI term. Total function (every `ℕ` maps to some SKI term). -Follows Mathlib's pattern for `ofNatCode` with inline termination proofs. -/ -def ofNatSKI : ℕ → SKI - | 0 => S - | 1 => K - | 2 => I - | n + 3 => - have : n.unpair.1 < n + 3 := - Nat.lt_of_le_of_lt (Nat.unpair_left_le n) (by omega) - have : n.unpair.2 < n + 3 := - Nat.lt_of_le_of_lt (Nat.unpair_right_le n) (by omega) - ofNatSKI n.unpair.1 ⬝ ofNatSKI n.unpair.2 - -@[simp] -theorem ofNatSKI_encodeSKI (t : SKI) : ofNatSKI (encodeSKI t) = t := by - induction t with - | S => simp [encodeSKI, ofNatSKI] - | K => simp [encodeSKI, ofNatSKI] - | I => simp [encodeSKI, ofNatSKI] - | app a b iha ihb => unfold encodeSKI ofNatSKI; simp [iha, ihb] - -@[simp] -theorem encodeSKI_ofNatSKI (n : ℕ) : encodeSKI (ofNatSKI n) = n := by - induction n using Nat.strongRecOn with - | _ n ih => - match n with - | 0 => simp [ofNatSKI, encodeSKI] - | 1 => simp [ofNatSKI, encodeSKI] - | 2 => simp [ofNatSKI, encodeSKI] - | n + 3 => - unfold ofNatSKI - simp only [encodeSKI] - have h1 : n.unpair.1 ≤ n := Nat.unpair_left_le n - have h2 : n.unpair.2 ≤ n := Nat.unpair_right_le n - rw [ih n.unpair.1 (by omega), ih n.unpair.2 (by omega), Nat.pair_unpair] - -/-- The encoding/decoding defines an equivalence `SKI ≃ ℕ`. -/ -def equivNat : SKI ≃ ℕ where - toFun := encodeSKI - invFun := ofNatSKI - left_inv := ofNatSKI_encodeSKI - right_inv := encodeSKI_ofNatSKI - -instance : Denumerable SKI := Denumerable.mk' equivNat - -@[simp] -theorem encode_eq_encodeSKI (t : SKI) : Encodable.encode t = encodeSKI t := rfl - -@[simp] -theorem ofNat_eq_ofNatSKI (n : ℕ) : Denumerable.ofNat SKI n = ofNatSKI n := rfl - -/-! ### Extracting values from churchK normal forms -/ - -/-- Extract the natural number from a `churchK` normal form. -`churchK 0 = K`, `churchK (n+1) = K ⬝ churchK n`. -/ -def extractChurchK : SKI → Option ℕ - | K => some 0 - | K ⬝ x => (extractChurchK x).map (· + 1) - | _ => none - -@[simp] -theorem extractChurchK_churchK (n : ℕ) : extractChurchK (churchK n) = some n := by - induction n with - | zero => rfl - | succ n ih => simp [churchK, extractChurchK, ih] - -theorem extractChurchK_some {t : SKI} {m : ℕ} (h : extractChurchK t = some m) : - t = churchK m := by - induction t generalizing m with - | S => simp [extractChurchK] at h - | K => - simp only [extractChurchK] at h - cases h; rfl - | I => simp [extractChurchK] at h - | app a b _ ih_b => - match a with - | K => - simp only [extractChurchK, Option.map_eq_some_iff] at h - obtain ⟨m', hm', rfl⟩ := h - have hb := ih_b hm' - subst hb - simp [churchK] - | S => simp [extractChurchK] at h - | I => simp [extractChurchK] at h - | _ ⬝ _ => simp [extractChurchK] at h - -/-! ### One-step evaluation as a total function -/ - -/-- One step of evaluation, returning the same term if already in normal form. -/ -def evalStepFn (t : SKI) : SKI := - match t.evalStep with - | .inl _ => t - | .inr t' => t' - -theorem evalStepFn_of_redexFree {t : SKI} (h : t.RedexFree) : - evalStepFn t = t := by - simp only [evalStepFn] - have : (t.evalStep).isLeft = true := redexFree_iff_evalStep.mp h - match ht : t.evalStep with - | .inl _ => rfl - | .inr _ => rw [ht] at this; cases this - -theorem evalStepFn_red {t : SKI} (h : ¬t.RedexFree) : - t ⭢ evalStepFn t := by - simp only [evalStepFn] - have : ¬(t.evalStep).isLeft = true := fun h' => h (redexFree_iff_evalStep.mpr h') - match ht : t.evalStep with - | .inl _ => rw [ht] at this; exact absurd rfl this - | .inr t' => exact evalStep_right_correct t t' ht - -/-- Iterating `evalStepFn` k times gives a multi-step reduction. -/ -theorem iterate_evalStepFn_mred (t : SKI) (k : ℕ) : - t ↠ evalStepFn^[k] t := by - induction k with - | zero => exact .refl - | succ k ih => - rw [Function.iterate_succ_apply'] - set t' := evalStepFn^[k] t with ht' - by_cases hrf : t'.RedexFree - · rw [evalStepFn_of_redexFree hrf]; exact ih - · exact Trans.trans ih (ReflTransGen.single (evalStepFn_red hrf)) - -/-- Once a term reaches a normal form, further iterations don't change it. -/ -theorem iterate_evalStepFn_stable {t : SKI} (h : t.RedexFree) (k : ℕ) : - evalStepFn^[k] t = t := by - induction k with - | zero => rfl - | succ k ih => - rw [Function.iterate_succ_apply', ih] - exact evalStepFn_of_redexFree h - -/-! ### The partial function computed by an SKI term -/ - -/-- The partial function `ℕ →. ℕ` computed by an SKI term `t`. - -Given input `n`, we: -1. Build `t ⬝ toChurch(n) ⬝ K ⬝ K` -2. Iterate `evalStepFn` to search for a normal form -3. If the normal form matches `churchK m`, return `m` -/ -noncomputable def evalNat (t : SKI) : ℕ →. ℕ := fun n => - Nat.rfindOpt (fun k => - extractChurchK (evalStepFn^[k] (t ⬝ toChurch n ⬝ K ⬝ K))) - -/-! ### Key lemma: normal-order reduction reaches normal forms -/ - -/-- If `t ↠ nf` and `nf` is redex-free, then iterating `evalStepFn` eventually reaches `nf`. - -This is the **standardization theorem** for SKI combinatory logic: normal-order -reduction (as implemented by `evalStep`) is normalizing — if a term has a normal form, -normal-order reduction finds it. - -The proof requires showing that the specific evaluation strategy in `evalStep` -(leftmost-outermost / head reduction) avoids infinite loops when a normal form exists. -This is a deep result; see e.g. Curry & Feys (1958) or Hindley & Seldin (2008). -/ -theorem exists_iterate_of_mred_redexFree {t nf : SKI} - (hred : t ↠ nf) (hnf : nf.RedexFree) : - ∃ k, evalStepFn^[k] t = nf := by - sorry - -/-! ### Monotonicity of the evaluation sequence -/ - -/-- Once `extractChurchK` succeeds at step `k`, it also succeeds at step `k'` for `k ≤ k'` -with the same result, because churchK values are redex-free and stable under iteration. -/ -theorem extractChurchK_iterate_mono {t : SKI} {m k : ℕ} - (hk : extractChurchK (evalStepFn^[k] t) = some m) - {k' : ℕ} (hle : k ≤ k') : - extractChurchK (evalStepFn^[k'] t) = some m := by - have heq := extractChurchK_some hk - rw [show k' = (k' - k) + k from by omega, Function.iterate_add_apply, heq, - iterate_evalStepFn_stable (churchK_redexFree m), extractChurchK_churchK] - -/-! ### Correctness: Computes t f → f ≤ evalNat t -/ - -/-- If `Computes t f`, then wherever `f` is defined, `evalNat t` agrees. -/ -theorem Computes.le_evalNat {t : SKI} {f : ℕ →. ℕ} (hc : Computes t f) : - ∀ n m, f n = Part.some m → evalNat t n = Part.some m := by - intro n m hfn - -- From Computes, get cm with IsChurch m cm and (t ⬝ toChurch n) ↠ cm - obtain ⟨cm, hcm, hred⟩ := hc n (toChurch n) (toChurch_correct n) m hfn - -- t ⬝ toChurch n ⬝ K ⬝ K ↠ cm ⬝ K ⬝ K ↠ Church m K K = churchK m - have h_full : (t ⬝ toChurch n ⬝ K ⬝ K) ↠ churchK m := - Trans.trans (parallel_mRed (MRed.head K hred) .refl) - (churchK_church m ▸ hcm K K) - -- Find k such that iteration reaches churchK m - obtain ⟨k, hk⟩ := exists_iterate_of_mred_redexFree h_full (churchK_redexFree m) - -- evalNat uses rfindOpt; at step k, extractChurchK succeeds - simp only [evalNat] - rw [Part.eq_some_iff] - apply (Nat.rfindOpt_mono - (fun {_ _ _} hle hm => extractChurchK_iterate_mono hm hle)).mpr - exact ⟨k, by rw [hk, extractChurchK_churchK]; rfl⟩ - -/-! ### Computability: evalNat t is Nat.Partrec -/ - -section Computability - -/-- Encoding of `evalStepFn` operating directly on natural numbers. -/ -def evalStepNat : ℕ → ℕ := fun n => encodeSKI (evalStepFn (ofNatSKI n)) - -/-- The encoding of `toChurch n` as a natural number. -/ -def toChurchNat : ℕ → ℕ := fun n => encodeSKI (toChurch n) - -/-- The encoding of `extractChurchK` operating on encoded terms. -/ -def extractChurchKNat : ℕ → Option ℕ := fun n => extractChurchK (ofNatSKI n) - -/-- `evalStepNat` correctly encodes `evalStepFn`. -/ -theorem evalStepNat_correct (t : SKI) : - evalStepNat (encodeSKI t) = encodeSKI (evalStepFn t) := by - simp [evalStepNat] - -/-- `extractChurchKNat` correctly encodes `extractChurchK`. -/ -theorem extractChurchKNat_correct (t : SKI) : - extractChurchKNat (encodeSKI t) = extractChurchK t := by - simp [extractChurchKNat] - -/-- The iterate of `evalStepNat` correctly encodes the iterate of `evalStepFn`. -/ -theorem iterate_evalStepNat_correct (t : SKI) (k : ℕ) : - evalStepNat^[k] (encodeSKI t) = - encodeSKI (evalStepFn^[k] t) := by - induction k with - | zero => rfl - | succ k ih => - rw [Function.iterate_succ_apply', Function.iterate_succ_apply', ih, - evalStepNat_correct] - -/-! #### Primrec helpers (no sorry dependencies) -/ - -/-- Application on SKI terms is primitive recursive. -/ -private theorem primrec_app : Primrec₂ (· ⬝ · : SKI → SKI → SKI) := - ((Primrec.ofNat SKI).comp - (Primrec.nat_add.comp - (Primrec₂.natPair.comp - (Primrec.encode.comp .fst) (Primrec.encode.comp .snd)) - (Primrec.const 3))).of_eq - fun ⟨a, b⟩ => by - simp only [ofNat_eq_ofNatSKI, encode_eq_encodeSKI] - change ofNatSKI (encodeSKI (a ⬝ b)) = _ - simp - -/-- `toChurch` is primitive recursive. -/ -private theorem primrec_toChurch : Primrec toChurch := - (Primrec.nat_iterate .id (.const (K ⬝ I)) - ((primrec_app.comp (.const SKI.Succ) .snd).to₂)).of_eq - fun n => by - change (fun x => SKI.Succ ⬝ x)^[n] (K ⬝ I) = toChurch n - induction n with - | zero => rfl - | succ n ih => rw [Function.iterate_succ_apply', ih, toChurch] - -/-! #### Helper lemmas for computability proofs -/ - -/-- Encoding of `Option.map (· + 1)` in terms of the encoded option. -/ -private theorem encode_option_map_succ (o : Option ℕ) : - Encodable.encode (o.map (· + 1)) = - if Encodable.encode o = 0 then 0 else Encodable.encode o + 1 := by - cases o <;> simp - -/-- `extractChurchK` returns `none` for applications whose left child is not `K`. -/ -private theorem extractChurchK_app_neK {a b : SKI} (h : a ≠ K) : - extractChurchK (a ⬝ b) = Option.none := by - cases a with - | K => exact absurd rfl h - | S => rfl - | I => rfl - | app c d => rfl - -/-! #### Nat.Primrec theorems -/ - -/-- Encoding of Church numerals is primitive recursive. -/ -theorem nat_primrec_toChurchNat : Nat.Primrec toChurchNat := - Primrec.nat_iff.mp (Primrec.encode.comp primrec_toChurch) - -/-- One step of SKI evaluation on encoded terms is primitive recursive. - -This requires showing that the pattern matching in `evalStep` — which dispatches on the -top-level structure of the SKI term (S/K/I/app) and performs the appropriate reduction — -can be expressed as a primitive recursive function on the natural number encoding. -The proof would involve ~150-250 lines of careful case analysis on the encoding. -/ -theorem nat_primrec_evalStepNat : Nat.Primrec evalStepNat := by - sorry - -/-- Extraction from churchK on encoded terms is primitive recursive. - -Uses course-of-values recursion (`Primrec.nat_strong_rec`): the value at `n ≥ 3` -depends on the value at `(n - 3).unpair.2 < n`. -/ -theorem nat_primrec_extractChurchKNat : - Nat.Primrec fun n => Encodable.encode (extractChurchKNat n) := by - rw [← Primrec.nat_iff] - -- Define the body for course-of-values recursion - let body : List ℕ → ℕ := fun hist => - if hist.length = 1 then 1 - else if 3 ≤ hist.length ∧ (hist.length - 3).unpair.1 = 1 then - if (hist[(hist.length - 3).unpair.2]?).getD 0 = 0 then 0 - else (hist[(hist.length - 3).unpair.2]?).getD 0 + 1 - else 0 - -- Show body is Primrec - have h_body : Primrec body := by - have len : Primrec (List.length : List ℕ → ℕ) := Primrec.list_length - have sub3 := Primrec.nat_sub.comp len (Primrec.const 3) - have unp := Primrec.unpair.comp sub3 - have unp1 := Primrec.fst.comp unp - have unp2 := Primrec.snd.comp unp - have lkup : Primrec (fun hist : List ℕ => (hist[(hist.length - 3).unpair.2]?).getD 0) := - Primrec.option_getD.comp (Primrec.list_getElem?.comp Primrec.id unp2) (Primrec.const 0) - exact Primrec.ite (Primrec.eq.comp len (Primrec.const 1)) (Primrec.const 1) - (Primrec.ite - (PrimrecPred.and (Primrec.nat_le.comp (Primrec.const 3) len) - (Primrec.eq.comp unp1 (Primrec.const 1))) - (Primrec.ite (Primrec.eq.comp lkup (Primrec.const 0)) - (Primrec.const 0) (Primrec.succ.comp lkup)) - (Primrec.const 0)) - -- Apply course-of-values recursion - exact (Primrec.nat_strong_rec - (fun (_ : PUnit) n => Encodable.encode (extractChurchKNat n)) - (g := fun _ hist => some (body hist)) - (Primrec.option_some.comp (h_body.comp Primrec.snd)) - (by - intro () n - simp only [body, List.length_map, List.length_range] - congr 1 - rcases n with _ | _ | _ | n - · simp [extractChurchKNat, ofNatSKI, extractChurchK] - · simp [extractChurchKNat, ofNatSKI, extractChurchK] - · simp [extractChurchKNat, ofNatSKI, extractChurchK] - · simp only [show ¬(n + 3 = 1) from by omega, ite_false, - show 3 ≤ n + 3 from by omega, true_and, show n + 3 - 3 = n from by omega, - extractChurchKNat, ofNatSKI] - by_cases h : n.unpair.1 = 1 - · have hK : ofNatSKI 1 = K := by unfold ofNatSKI; rfl - simp only [h, ite_true, hK, extractChurchK] - have h_lt : n.unpair.2 < n + 3 := - Nat.lt_of_le_of_lt (Nat.unpair_right_le n) (by omega) - simp only [List.getElem?_map, List.getElem?_range h_lt, Option.map_some, - Option.getD_some] - exact (encode_option_map_succ (extractChurchKNat n.unpair.2)).symm - · simp only [h, ite_false] - have : ofNatSKI n.unpair.1 ≠ K := by - intro heq - exact h ((encodeSKI_ofNatSKI _).symm.trans (congrArg encodeSKI heq)) - simp [extractChurchK_app_neK this])).comp (Primrec.const ()) Primrec.id - -/-! #### Converting Nat.Primrec to Primrec on SKI -/ - -/-- `evalStepFn` is primitive recursive. -/ -private theorem primrec_evalStepFn : Primrec evalStepFn := - ((Primrec.ofNat SKI).comp - ((Primrec.nat_iff.mpr nat_primrec_evalStepNat).comp Primrec.encode)).of_eq - fun t => by simp [evalStepNat] - -/-- `extractChurchK` is primitive recursive. -/ -private theorem primrec_extractChurchK : Primrec extractChurchK := - (Primrec.encode_iff.mp <| - (Primrec.nat_iff.mpr nat_primrec_extractChurchKNat).comp Primrec.encode).of_eq - fun t => by simp [extractChurchKNat] - -/-- The function computed by any SKI term is partial recursive. -/ -theorem ski_eval_partrec (t : SKI) : Nat.Partrec (evalNat t) := by - rw [← Partrec.nat_iff] - change Partrec fun n => Nat.rfindOpt fun k => - extractChurchK (evalStepFn^[k] (t ⬝ toChurch n ⬝ K ⬝ K)) - apply Partrec.rfindOpt - -- Need: Computable₂ (fun n k => extractChurchK (evalStepFn^[k] (t ⬝ toChurch n ⬝ K ⬝ K))) - apply Primrec₂.to_comp - exact primrec_extractChurchK.comp - (Primrec.nat_iterate .snd - (primrec_app.comp (primrec_app.comp (primrec_app.comp - (Primrec.const t) (primrec_toChurch.comp .fst)) - (Primrec.const K)) (Primrec.const K)) - (primrec_evalStepFn.comp₂ Primrec₂.right)) - -end Computability - -/-! ### Combined equivalence -/ - -/-- Every partial recursive function has an SKI term whose `evalNat` agrees wherever `f` -is defined. This is weaker than full equality `evalNat t = f` but follows directly from -`Computes.le_evalNat` and `natPartrec_skiComputable`. -/ -theorem nat_partrec_le_ski_evalNat {f : ℕ →. ℕ} (hf : Nat.Partrec f) : - ∃ t : SKI, ∀ n m, f n = Part.some m → evalNat t n = Part.some m := - let ⟨t, ht⟩ := natPartrec_skiComputable f hf - ⟨t, ht.le_evalNat⟩ - -/-- Full equivalence: a function is `Nat.Partrec` iff it is the function computed -by some SKI term. - -The forward direction requires showing that the SKI term produced by `codeToSKINat` -computes *exactly* `f` (not just agreeing where `f` is defined). This needs a stronger -`ComputesExact` property of the construction: the term does not reduce to a Church -numeral on inputs where `f` is undefined. -/ -theorem partrec_iff_ski_evalNat {f : ℕ →. ℕ} : - Nat.Partrec f ↔ ∃ t : SKI, evalNat t = f := by - constructor - · intro hf - obtain ⟨t, ht⟩ := natPartrec_skiComputable f hf - -- ht.le_evalNat gives: wherever f is defined, evalNat t agrees. - -- The missing piece: evalNat t is undefined wherever f is. - exact ⟨t, sorry⟩ - · rintro ⟨t, rfl⟩ - exact ski_eval_partrec t - -end SKI - -end Cslib From 6d3692c9992e62dcc031b925b6ad24fd2463bf48 Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Thu, 19 Mar 2026 17:49:56 +0100 Subject: [PATCH 06/13] refactor(CombinatoryLogic): extract helpers, simplify proofs Add computes_of_total and RFindAbove_unfold helpers to eliminate repeated proof patterns. Simplify comp/pair_computes Part.mem chains and rfindAbove_induction via early subst + local helper. Remove dormant @[scoped grind] attributes from nil_correct and neg_correct. --- Cslib/Languages/CombinatoryLogic/Basic.lean | 1 - Cslib/Languages/CombinatoryLogic/List.lean | 1 - .../CombinatoryLogic/PartrecToSKI.lean | 115 ++++++++---------- .../Languages/CombinatoryLogic/Recursion.lean | 8 +- 4 files changed, 51 insertions(+), 74 deletions(-) diff --git a/Cslib/Languages/CombinatoryLogic/Basic.lean b/Cslib/Languages/CombinatoryLogic/Basic.lean index 0bf5d2aca..e8743062a 100644 --- a/Cslib/Languages/CombinatoryLogic/Basic.lean +++ b/Cslib/Languages/CombinatoryLogic/Basic.lean @@ -288,7 +288,6 @@ theorem cond_correct (a x y : SKI) (u : Bool) (h : IsBool u a) : /-- Neg := λ a. Cond FF TT a -/ protected def Neg : SKI := SKI.Cond ⬝ FF ⬝ TT -@[scoped grind →] theorem neg_correct (a : SKI) (ua : Bool) (h : IsBool ua a) : IsBool (¬ ua) (SKI.Neg ⬝ a) := by apply isBool_trans (a' := if ua then FF else TT) · apply cond_correct (h := h) diff --git a/Cslib/Languages/CombinatoryLogic/List.lean b/Cslib/Languages/CombinatoryLogic/List.lean index 3645cfe62..c71721da9 100644 --- a/Cslib/Languages/CombinatoryLogic/List.lean +++ b/Cslib/Languages/CombinatoryLogic/List.lean @@ -74,7 +74,6 @@ theorem nil_def (c n : SKI) : (Nil ⬝ c ⬝ n) ↠ n := NilPoly.toSKI_correct [c, n] (by simp) /-- The empty list term correctly represents `[]`. -/ -@[scoped grind .] theorem nil_correct : IsChurchList [] Nil := nil_def /-! ### Cons: Consing an element onto a list -/ diff --git a/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean b/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean index 12df72b60..65488e6c6 100644 --- a/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean +++ b/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean @@ -115,37 +115,38 @@ def codeToSKINat : Code → SKI /-! ### Correctness proofs -/ +/-- Helper for total functions: if `c.eval` is total with output `g n`, and `t` reduces + to a Church numeral for `g n`, then `t` computes `c.eval`. -/ +private theorem computes_of_total (t : SKI) (c : Code) (g : ℕ → ℕ) + (heval : ∀ n, c.eval n = Part.some (g n)) + (hcorrect : ∀ n cn, IsChurch n cn → IsChurch (g n) (t ⬝ cn)) : + Computes t c.eval := by + intro n cn hcn m hm; rw [heval] at hm; obtain rfl := Part.some_injective hm + exact hcorrect n cn hcn + /-- `Code.zero` computes the constant zero function. -/ -theorem zero_computes : Computes (K ⬝ SKI.Zero) (Code.eval .zero) := by - intro n cn hcn m hm - have h0 : Code.eval .zero n = Part.some 0 := by - rw [show Code.zero = Code.const 0 from rfl, Code.eval_const] - rw [h0] at hm; obtain rfl := Part.some_injective hm - exact isChurch_trans 0 (MRed.K SKI.Zero cn) zero_correct +theorem zero_computes : Computes (K ⬝ SKI.Zero) (Code.eval .zero) := + computes_of_total _ .zero (fun _ => 0) + (fun n => by rw [show Code.zero = Code.const 0 from rfl, Code.eval_const]) + (fun _ _ _ => isChurch_trans 0 (MRed.K SKI.Zero _) zero_correct) /-- `Code.succ` computes the successor function. -/ -theorem succ_computes : Computes SKI.Succ (Code.eval .succ) := by - intro n cn hcn m hm - have h0 : Code.eval .succ n = Part.some (n + 1) := by - simp only [Code.eval, PFun.coe_val] - rw [h0] at hm; obtain rfl := Part.some_injective hm - exact succ_correct n cn hcn +theorem succ_computes : Computes SKI.Succ (Code.eval .succ) := + computes_of_total _ .succ (· + 1) + (fun _ => by simp only [Code.eval, PFun.coe_val]) + (fun n cn hcn => succ_correct n cn hcn) /-- `Code.left` computes the left projection of `Nat.unpair`. -/ -theorem left_computes : Computes NatUnpairLeft (Code.eval .left) := by - intro n cn hcn m hm - have h0 : Code.eval .left n = Part.some (Nat.unpair n).1 := by - simp only [Code.eval, PFun.coe_val] - rw [h0] at hm; obtain rfl := Part.some_injective hm - exact natUnpairLeft_correct n cn hcn +theorem left_computes : Computes NatUnpairLeft (Code.eval .left) := + computes_of_total _ .left (fun n => (Nat.unpair n).1) + (fun _ => by simp only [Code.eval, PFun.coe_val]) + (fun n cn hcn => natUnpairLeft_correct n cn hcn) /-- `Code.right` computes the right projection of `Nat.unpair`. -/ -theorem right_computes : Computes NatUnpairRight (Code.eval .right) := by - intro n cn hcn m hm - have h0 : Code.eval .right n = Part.some (Nat.unpair n).2 := by - simp only [Code.eval, PFun.coe_val] - rw [h0] at hm; obtain rfl := Part.some_injective hm - exact natUnpairRight_correct n cn hcn +theorem right_computes : Computes NatUnpairRight (Code.eval .right) := + computes_of_total _ .right (fun n => (Nat.unpair n).2) + (fun _ => by simp only [Code.eval, PFun.coe_val]) + (fun n cn hcn => natUnpairRight_correct n cn hcn) /-- Composition of computable functions is computable. -/ theorem comp_computes {f g : ℕ →. ℕ} {tf tg : SKI} @@ -153,13 +154,10 @@ theorem comp_computes {f g : ℕ →. ℕ} {tf tg : SKI} Computes (B ⬝ tf ⬝ tg) (fun n => g n >>= f) := by intro n cn hcn m hm simp only at hm - have hm' : m ∈ (g n >>= f) := by rw [hm]; exact Part.mem_some m - obtain ⟨intermediate, hint_mem, hm_mem⟩ := Part.mem_bind_iff.mp hm' - have hgn : g n = Part.some intermediate := Part.eq_some_iff.mpr hint_mem - have hfint : f intermediate = Part.some m := Part.eq_some_iff.mpr hm_mem - have hcint := hg n cn hcn intermediate hgn - have hcm := hf intermediate (tg ⬝ cn) hcint m hfint - exact isChurch_trans _ (B_def tf tg cn) hcm + obtain ⟨intermediate, hint_mem, hm_mem⟩ := Part.mem_bind_iff.mp (hm ▸ Part.mem_some m) + have hcint := hg n cn hcn intermediate (Part.eq_some_iff.mpr hint_mem) + exact isChurch_trans _ (B_def tf tg cn) + (hf intermediate (tg ⬝ cn) hcint m (Part.eq_some_iff.mpr hm_mem)) /-- Pairing of computable functions is computable. -/ theorem pair_computes {f g : ℕ →. ℕ} {tf tg : SKI} @@ -168,24 +166,13 @@ theorem pair_computes {f g : ℕ →. ℕ} {tf tg : SKI} (fun n => Nat.pair <$> f n <*> g n) := by intro n cn hcn m hm simp only at hm - -- hm : Nat.pair <$> f n <*> g n = Part.some m - have hm' : m ∈ (Nat.pair <$> f n <*> g n) := by rw [hm]; exact Part.mem_some m - -- Unfold <*> into bind: pf <*> pa = pf >>= fun h => h <$> pa - have hm_bind : m ∈ Part.bind (Part.map Nat.pair (f n)) (fun h => Part.map h (g n)) := hm' - obtain ⟨h, hh_mem, hm_in_h⟩ := Part.mem_bind_iff.mp hm_bind - obtain ⟨a, ha_mem, hh_eq⟩ := (Part.mem_map_iff _).mp hh_mem - subst hh_eq - obtain ⟨b, hb_mem, hm_eq⟩ := (Part.mem_map_iff _).mp hm_in_h - have hfn : f n = Part.some a := Part.eq_some_iff.mpr ha_mem - have hgn : g n = Part.some b := Part.eq_some_iff.mpr hb_mem - have hca := hf n cn hcn a hfn - have hcb := hg n cn hcn b hgn - subst hm_eq - have hred : (S ⬝ (B ⬝ NatPair ⬝ tf) ⬝ tg ⬝ cn) ↠ - (NatPair ⬝ (tf ⬝ cn) ⬝ (tg ⬝ cn)) := calc - _ ↠ (B ⬝ NatPair ⬝ tf) ⬝ cn ⬝ (tg ⬝ cn) := MRed.S _ _ _ - _ ↠ NatPair ⬝ (tf ⬝ cn) ⬝ (tg ⬝ cn) := MRed.head _ (B_def _ _ _) - exact isChurch_trans _ hred (natPair_correct a b _ _ hca hcb) + obtain ⟨h, hh_mem, hm_in_h⟩ := Part.mem_bind_iff.mp (hm ▸ Part.mem_some m) + obtain ⟨a, ha_mem, rfl⟩ := (Part.mem_map_iff _).mp hh_mem + obtain ⟨b, hb_mem, rfl⟩ := (Part.mem_map_iff _).mp hm_in_h + have hca := hf n cn hcn a (Part.eq_some_iff.mpr ha_mem) + have hcb := hg n cn hcn b (Part.eq_some_iff.mpr hb_mem) + exact isChurch_trans _ ((MRed.S _ _ _).trans (MRed.head _ (B_def _ _ _))) + (natPair_correct a b _ _ hca hcb) /-- Helper: `Rec` correctly implements primitive recursion from `Code.prec`. -/ private theorem prec_rec_correct (f g : Code) (tf tg : SKI) @@ -257,36 +244,30 @@ private theorem rfindAbove_induction (f : Code) (tf : SKI) (∀ i < n, ∃ vi, vi ≠ 0 ∧ f.eval (Nat.pair a₀ (m + i)) = Part.some vi) → IsChurch (m + n) (RFindAbove ⬝ x ⬝ g) := by + subst hg + -- Helper: `B ⬝ tf ⬝ (NatPair ⬝ ca) ⬝ x` computes `f.eval (Nat.pair a₀ m)`. + have hgx : ∀ m x, IsChurch m x → ∀ v, f.eval (Nat.pair a₀ m) = Part.some v → + IsChurch v (B ⬝ tf ⬝ (NatPair ⬝ ca) ⬝ x) := fun m x hx v hv => + isChurch_trans _ (B_def tf (NatPair ⬝ ca) x) + (ihf _ _ (natPair_correct a₀ m ca x hca hx) v hv) intro n induction n with | zero => intro m x hx hroot _ simp only [Nat.add_zero] at hroot ⊢ - apply isChurch_trans (a' := RFindAboveAux ⬝ RFindAbove ⬝ x ⬝ g) - · apply MRed.head; apply MRed.head; exact fixedPoint_correct _ + apply isChurch_trans _ (RFindAbove_unfold x _) apply isChurch_trans (a' := x) - · apply rfindAboveAux_base - -- Need: IsChurch 0 (g ⬝ x) - subst hg - apply isChurch_trans _ (B_def tf (NatPair ⬝ ca) x) - have hpair := natPair_correct a₀ m ca x hca hx - exact ihf _ _ hpair 0 hroot + · exact rfindAboveAux_base _ _ _ (hgx m x hx 0 hroot) · exact hx | succ n ih => intro m x hx hroot hbelow - apply isChurch_trans (a' := RFindAboveAux ⬝ RFindAbove ⬝ x ⬝ g) - · apply MRed.head; apply MRed.head; exact fixedPoint_correct _ - -- f at m is nonzero, so step + apply isChurch_trans _ (RFindAbove_unfold x _) obtain ⟨v₀, hv₀_ne, hv₀_eval⟩ := hbelow 0 (by omega) simp only [Nat.add_zero] at hv₀_eval - apply isChurch_trans (a' := RFindAbove ⬝ (SKI.Succ ⬝ x) ⬝ g) + apply isChurch_trans (a' := RFindAbove ⬝ (SKI.Succ ⬝ x) ⬝ _) · apply rfindAboveAux_step (m := v₀ - 1) - subst hg - apply isChurch_trans _ (B_def tf (NatPair ⬝ ca) x) - have hpair := natPair_correct a₀ m ca x hca hx - have hv₀_pos : v₀ - 1 + 1 = v₀ := Nat.succ_pred_eq_of_ne_zero hv₀_ne - rw [hv₀_pos] - exact ihf _ _ hpair v₀ hv₀_eval + have : v₀ - 1 + 1 = v₀ := Nat.succ_pred_eq_of_ne_zero hv₀_ne + rw [this]; exact hgx m x hx v₀ hv₀_eval · have h := ih (m + 1) (SKI.Succ ⬝ x) (succ_correct m x hx) (by rw [show m + 1 + n = m + (n + 1) from by omega]; exact hroot) (by diff --git a/Cslib/Languages/CombinatoryLogic/Recursion.lean b/Cslib/Languages/CombinatoryLogic/Recursion.lean index dce848cf9..5518289e8 100644 --- a/Cslib/Languages/CombinatoryLogic/Recursion.lean +++ b/Cslib/Languages/CombinatoryLogic/Recursion.lean @@ -316,11 +316,11 @@ theorem RFindAbove_correct (fNat : Nat → Nat) (f x : SKI) (n m : Nat) (hx : IsChurch m x) (hroot : fNat (m+n) = 0) (hpos : ∀ i < n, fNat (m+i) ≠ 0) : IsChurch (m+n) (RFindAbove ⬝ x ⬝ f) := by induction n generalizing m x - all_goals apply isChurch_trans (a' := RFindAboveAux ⬝ RFindAbove ⬝ x ⬝ f) - case zero.a => + all_goals apply isChurch_trans _ (RFindAbove_unfold x f) + case zero => apply isChurch_trans (a' := x) <;> grind [rfindAboveAux_base] - case succ.a n ih => + case succ n ih => apply isChurch_trans (a' := RFindAbove ⬝ (SKI.Succ ⬝ x) ⬝ f) · let y := (fNat m).pred have : IsChurch (y + 1) (f ⬝ x) := by @@ -330,8 +330,6 @@ theorem RFindAbove_correct (fNat : Nat → Nat) (f x : SKI) assumption · replace ih := ih (SKI.Succ ⬝ x) (m + 1) (succ_correct _ x hx) grind - -- close the `h` goals of the above `apply isChurch_trans` - all_goals {apply MRed.head; apply MRed.head; exact fixedPoint_correct _} /-- Ordinary root finding is root finding above zero -/ From 9c3b13c514a6116fdf7fc1e762fbde820e3d2d47 Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Sat, 21 Mar 2026 08:16:07 +0100 Subject: [PATCH 07/13] refactor(PartrecToSKI): split rfind_eval_facts into two lemmas Split the conjunction into `rfind_eval_root` (f evaluates to 0 at the root) and `rfind_eval_pos_below` (f evaluates to nonzero below k). --- .../CombinatoryLogic/PartrecToSKI.lean | 37 +++++++++++-------- 1 file changed, 21 insertions(+), 16 deletions(-) diff --git a/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean b/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean index 65488e6c6..d1a52ca50 100644 --- a/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean +++ b/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean @@ -215,24 +215,28 @@ private theorem prec_rec_correct (f g : Code) (tf tg : SKI) (precStep_def tg ca cb (Rec ⬝ base ⬝ step ⬝ (Pred ⬝ cb))) exact isChurch_trans _ hred hcm -/-- Extract eval facts from `Nat.rfind` membership. -/ -private theorem rfind_eval_facts {f : Code} {a₀ m₀ k : ℕ} +/-- If `k ∈ Nat.rfind …`, then `f` evaluates to 0 at the root. -/ +private theorem rfind_eval_root {f : Code} {a₀ m₀ k : ℕ} + (hk : k ∈ Nat.rfind (fun n => + (fun m => decide (m = 0)) <$> f.eval (Nat.pair a₀ (n + m₀)))) : + f.eval (Nat.pair a₀ (m₀ + k)) = Part.some 0 := by + have hspec := Nat.rfind_spec hk + obtain ⟨val, hval_mem, hval_eq⟩ := (Part.mem_map_iff _).mp hspec + have : val = 0 := by simpa using hval_eq + subst this; rw [Nat.add_comm] at hval_mem + exact Part.eq_some_iff.mpr hval_mem + +/-- If `k ∈ Nat.rfind …`, then `f` evaluates to a nonzero value below `k`. -/ +private theorem rfind_eval_pos_below {f : Code} {a₀ m₀ k : ℕ} (hk : k ∈ Nat.rfind (fun n => (fun m => decide (m = 0)) <$> f.eval (Nat.pair a₀ (n + m₀)))) : - f.eval (Nat.pair a₀ (m₀ + k)) = Part.some 0 ∧ ∀ i < k, ∃ vi, vi ≠ 0 ∧ f.eval (Nat.pair a₀ (m₀ + i)) = Part.some vi := by - constructor - · have hspec := Nat.rfind_spec hk - obtain ⟨val, hval_mem, hval_eq⟩ := (Part.mem_map_iff _).mp hspec - have : val = 0 := by simpa using hval_eq - subst this; rw [Nat.add_comm] at hval_mem - exact Part.eq_some_iff.mpr hval_mem - · intro i hi - have hmin := Nat.rfind_min hk hi - obtain ⟨val, hval_mem, hval_eq⟩ := (Part.mem_map_iff _).mp hmin - have hval_ne : val ≠ 0 := by simpa using hval_eq - rw [Nat.add_comm] at hval_mem - exact ⟨val, hval_ne, Part.eq_some_iff.mpr hval_mem⟩ + intro i hi + have hmin := Nat.rfind_min hk hi + obtain ⟨val, hval_mem, hval_eq⟩ := (Part.mem_map_iff _).mp hmin + have hval_ne : val ≠ 0 := by simpa using hval_eq + rw [Nat.add_comm] at hval_mem + exact ⟨val, hval_ne, Part.eq_some_iff.mpr hval_mem⟩ /-- Helper: `RFindAbove` correctly implements `Code.rfind'` by induction on the number of steps until the root. -/ @@ -321,7 +325,8 @@ theorem codeToSKINat_correct (c : Code) : Computes (codeToSKINat c) c.eval := by show (Nat.unpair n).2 = m₀ from rfl] at hresult' obtain ⟨k, hk_mem, hresult_eq⟩ := (Part.mem_map_iff _).mp hresult' subst hresult_eq - obtain ⟨heval_root, heval_below⟩ := rfind_eval_facts hk_mem + have heval_root := rfind_eval_root hk_mem + have heval_below := rfind_eval_pos_below hk_mem set g := B ⬝ tf ⬝ (NatPair ⬝ (NatUnpairLeft ⬝ cn)) have hind := rfindAbove_induction f tf ihf a₀ (NatUnpairLeft ⬝ cn) hca g rfl k m₀ From cc3fb50d31e1348b42d434916aa1af8ebf1fac80 Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Tue, 31 Mar 2026 12:12:35 +0200 Subject: [PATCH 08/13] refactor(Recursion): generalize RFindAbove_correct to partial functions Add RFindAbove_correct' which works with pointwise Church encoding properties rather than requiring a total function. Restate the original RFindAbove_correct as a corollary. --- .../Languages/CombinatoryLogic/Recursion.lean | 44 +++++++++++++------ 1 file changed, 30 insertions(+), 14 deletions(-) diff --git a/Cslib/Languages/CombinatoryLogic/Recursion.lean b/Cslib/Languages/CombinatoryLogic/Recursion.lean index 5518289e8..d021ac3a0 100644 --- a/Cslib/Languages/CombinatoryLogic/Recursion.lean +++ b/Cslib/Languages/CombinatoryLogic/Recursion.lean @@ -311,25 +311,41 @@ theorem RFindAbove_unfold (x g : SKI) : (RFindAbove ⬝ x ⬝ g) ↠ RFindAboveAux ⬝ RFindAbove ⬝ x ⬝ g := by apply MRed.head; apply MRed.head; exact fixedPoint_correct _ -theorem RFindAbove_correct (fNat : Nat → Nat) (f x : SKI) - (hf : ∀ i : Nat, ∀ y : SKI, IsChurch i y → IsChurch (fNat i) (f ⬝ y)) - (n m : Nat) (hx : IsChurch m x) (hroot : fNat (m+n) = 0) (hpos : ∀ i < n, fNat (m+i) ≠ 0) : - IsChurch (m+n) (RFindAbove ⬝ x ⬝ f) := by +/-- Generalized root-finding that works with pointwise properties rather than a total + function. At the root `m + n`, `f` yields Church 0; below, a nonzero Church numeral. -/ +theorem RFindAbove_correct' (f x : SKI) (n m : Nat) (hx : IsChurch m x) + (hf_root : ∀ y, IsChurch (m + n) y → IsChurch 0 (f ⬝ y)) + (hf_below : ∀ i < n, ∀ y, IsChurch (m + i) y → + ∃ k, IsChurch (k + 1) (f ⬝ y)) : + IsChurch (m + n) (RFindAbove ⬝ x ⬝ f) := by induction n generalizing m x all_goals apply isChurch_trans _ (RFindAbove_unfold x f) case zero => - apply isChurch_trans (a' := x) <;> - grind [rfindAboveAux_base] + simp only [Nat.add_zero] at * + apply isChurch_trans (a' := x) + · exact rfindAboveAux_base _ _ _ (hf_root x hx) + · exact hx case succ n ih => apply isChurch_trans (a' := RFindAbove ⬝ (SKI.Succ ⬝ x) ⬝ f) - · let y := (fNat m).pred - have : IsChurch (y + 1) (f ⬝ x) := by - subst y - exact Nat.succ_pred_eq_of_ne_zero (hpos 0 (by simp)) ▸ hf m x hx - apply rfindAboveAux_step - assumption - · replace ih := ih (SKI.Succ ⬝ x) (m + 1) (succ_correct _ x hx) - grind + · obtain ⟨k, hk⟩ := hf_below 0 (by omega) x (by simpa using hx) + exact rfindAboveAux_step _ _ _ hk + · rw [show m + (n + 1) = (m + 1) + n from by omega] + exact ih (SKI.Succ ⬝ x) (m + 1) (succ_correct _ x hx) + (fun y hy => hf_root y (by rw [show m + 1 + n = m + (n + 1) from by omega] at hy; exact hy)) + (fun i hi y hy => hf_below (i + 1) (by omega) y (by + rw [show m + 1 + i = m + (i + 1) from by omega] at hy; exact hy)) + +theorem RFindAbove_correct (fNat : Nat → Nat) (f x : SKI) + (hf : ∀ i : Nat, ∀ y : SKI, IsChurch i y → IsChurch (fNat i) (f ⬝ y)) + (n m : Nat) (hx : IsChurch m x) (hroot : fNat (m+n) = 0) (hpos : ∀ i < n, fNat (m+i) ≠ 0) : + IsChurch (m+n) (RFindAbove ⬝ x ⬝ f) := by + apply RFindAbove_correct' f x n m hx + · intro y hy; exact hroot ▸ hf (m + n) y hy + · intro i hi y hy + have hne := hpos i hi + refine ⟨(fNat (m + i)) - 1, ?_⟩ + have : fNat (m + i) - 1 + 1 = fNat (m + i) := by omega + rw [this]; exact hf (m + i) y hy /-- Ordinary root finding is root finding above zero -/ From 8262b9770ef8c3858bf6f320094407329c57389c Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Tue, 31 Mar 2026 12:12:42 +0200 Subject: [PATCH 09/13] refactor(PartrecToSKI): extract Computes combinators, add bind_eq_some - Extract prec_computes and rfind_computes as standalone lemmas, making codeToSKINat_correct a uniform 1-2 line per case induction. - Delete rfindAbove_induction (40 lines) by using the generalized RFindAbove_correct' from Recursion.lean. - Add bind_eq_some helper to simplify Part.mem_bind_iff extraction boilerplate in comp_computes and prec_rec_correct. --- .../CombinatoryLogic/PartrecToSKI.lean | 155 +++++++----------- 1 file changed, 61 insertions(+), 94 deletions(-) diff --git a/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean b/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean index d1a52ca50..b29ee265a 100644 --- a/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean +++ b/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean @@ -115,6 +115,13 @@ def codeToSKINat : Code → SKI /-! ### Correctness proofs -/ +/-- Extract witnesses from a bind that equals `Part.some`. -/ +private theorem bind_eq_some {a : Part α} {g : α → Part β} {m : β} + (h : (a >>= g) = Part.some m) : + ∃ x, a = Part.some x ∧ g x = Part.some m := by + have hm := Part.mem_bind_iff.mp (h ▸ Part.mem_some m) + exact hm.imp fun x ⟨hx, hm⟩ => ⟨Part.eq_some_iff.mpr hx, Part.eq_some_iff.mpr hm⟩ + /-- Helper for total functions: if `c.eval` is total with output `g n`, and `t` reduces to a Church numeral for `g n`, then `t` computes `c.eval`. -/ private theorem computes_of_total (t : SKI) (c : Code) (g : ℕ → ℕ) @@ -153,11 +160,9 @@ theorem comp_computes {f g : ℕ →. ℕ} {tf tg : SKI} (hf : Computes tf f) (hg : Computes tg g) : Computes (B ⬝ tf ⬝ tg) (fun n => g n >>= f) := by intro n cn hcn m hm - simp only at hm - obtain ⟨intermediate, hint_mem, hm_mem⟩ := Part.mem_bind_iff.mp (hm ▸ Part.mem_some m) - have hcint := hg n cn hcn intermediate (Part.eq_some_iff.mpr hint_mem) + obtain ⟨intermediate, hint_eq, hm_eq⟩ := bind_eq_some hm exact isChurch_trans _ (B_def tf tg cn) - (hf intermediate (tg ⬝ cn) hcint m (Part.eq_some_iff.mpr hm_mem)) + (hf intermediate (tg ⬝ cn) (hg n cn hcn intermediate hint_eq) m hm_eq) /-- Pairing of computable functions is computable. -/ theorem pair_computes {f g : ℕ →. ℕ} {tf tg : SKI} @@ -191,13 +196,7 @@ private theorem prec_rec_correct (f g : Code) (tf tg : SKI) | succ k ih => intro m hm cb hcb rw [Code.eval_prec_succ] at hm - -- Extract the intermediate value from the bind - have hm' : m ∈ (Code.eval (f.prec g) (Nat.pair a₀ k) >>= - fun i => g.eval (Nat.pair a₀ (Nat.pair k i))) := by - rw [hm]; exact Part.mem_some m - obtain ⟨ih_val, hih_mem, hm_mem⟩ := Part.mem_bind_iff.mp hm' - have hih_eq := Part.eq_some_iff.mpr hih_mem - have hm_eq := Part.eq_some_iff.mpr hm_mem + obtain ⟨ih_val, hih_eq, hm_eq⟩ := bind_eq_some hm -- By IH, Rec computes the intermediate value on Pred ⬝ cb have hpred : IsChurch k (Pred ⬝ cb) := pred_correct (k + 1) cb hcb set step := PrecStep tg ⬝ ca @@ -238,49 +237,53 @@ private theorem rfind_eval_pos_below {f : Code} {a₀ m₀ k : ℕ} rw [Nat.add_comm] at hval_mem exact ⟨val, hval_ne, Part.eq_some_iff.mpr hval_mem⟩ -/-- Helper: `RFindAbove` correctly implements `Code.rfind'` by induction on - the number of steps until the root. -/ -private theorem rfindAbove_induction (f : Code) (tf : SKI) - (ihf : Computes tf f.eval) (a₀ : ℕ) (ca : SKI) (hca : IsChurch a₀ ca) - (g : SKI) (hg : g = B ⬝ tf ⬝ (NatPair ⬝ ca)) : - ∀ n m : ℕ, ∀ x : SKI, IsChurch m x → - f.eval (Nat.pair a₀ (m + n)) = Part.some 0 → - (∀ i < n, ∃ vi, vi ≠ 0 ∧ - f.eval (Nat.pair a₀ (m + i)) = Part.some vi) → - IsChurch (m + n) (RFindAbove ⬝ x ⬝ g) := by - subst hg - -- Helper: `B ⬝ tf ⬝ (NatPair ⬝ ca) ⬝ x` computes `f.eval (Nat.pair a₀ m)`. - have hgx : ∀ m x, IsChurch m x → ∀ v, f.eval (Nat.pair a₀ m) = Part.some v → - IsChurch v (B ⬝ tf ⬝ (NatPair ⬝ ca) ⬝ x) := fun m x hx v hv => - isChurch_trans _ (B_def tf (NatPair ⬝ ca) x) - (ihf _ _ (natPair_correct a₀ m ca x hca hx) v hv) - intro n - induction n with - | zero => - intro m x hx hroot _ - simp only [Nat.add_zero] at hroot ⊢ - apply isChurch_trans _ (RFindAbove_unfold x _) - apply isChurch_trans (a' := x) - · exact rfindAboveAux_base _ _ _ (hgx m x hx 0 hroot) - · exact hx - | succ n ih => - intro m x hx hroot hbelow - apply isChurch_trans _ (RFindAbove_unfold x _) - obtain ⟨v₀, hv₀_ne, hv₀_eval⟩ := hbelow 0 (by omega) - simp only [Nat.add_zero] at hv₀_eval - apply isChurch_trans (a' := RFindAbove ⬝ (SKI.Succ ⬝ x) ⬝ _) - · apply rfindAboveAux_step (m := v₀ - 1) - have : v₀ - 1 + 1 = v₀ := Nat.succ_pred_eq_of_ne_zero hv₀_ne - rw [this]; exact hgx m x hx v₀ hv₀_eval - · have h := ih (m + 1) (SKI.Succ ⬝ x) (succ_correct m x hx) - (by rw [show m + 1 + n = m + (n + 1) from by omega]; exact hroot) - (by - intro i hi - obtain ⟨vi, hvi_ne, hvi_eval⟩ := hbelow (i + 1) (by omega) - exact ⟨vi, hvi_ne, by - rw [show m + 1 + i = m + (i + 1) from by omega]; exact hvi_eval⟩) - rw [show m + (n + 1) = m + 1 + n from by omega] - exact h +/-- Primitive recursion of computable functions is computable. -/ +private theorem prec_computes {f g : Code} {tf tg : SKI} + (ihf : Computes tf f.eval) (ihg : Computes tg g.eval) : + Computes (PrecTrans tf tg) (f.prec g).eval := by + intro n cn hcn m hm + have hca := natUnpairLeft_correct n cn hcn + have hcb := natUnpairRight_correct n cn hcn + have hred := precTrans_def tf tg cn + have hpair : n = Nat.pair (Nat.unpair n).1 (Nat.unpair n).2 := + (Nat.pair_unpair n).symm + rw [hpair] at hm + exact isChurch_trans _ hred (prec_rec_correct f g _ _ ihf ihg + (Nat.unpair n).1 (NatUnpairLeft ⬝ cn) hca + (Nat.unpair n).2 m hm (NatUnpairRight ⬝ cn) hcb) + +/-- Unbounded search of a computable function is computable. -/ +private theorem rfind_computes {f : Code} {tf : SKI} + (ihf : Computes tf f.eval) : + Computes (RFindTrans tf) (Code.rfind' f).eval := by + intro n cn hcn result hresult + set a₀ := (Nat.unpair n).1 + set m₀ := (Nat.unpair n).2 + have hca := natUnpairLeft_correct n cn hcn + have hcm₀ := natUnpairRight_correct n cn hcn + -- Extract k from the rfind result + have hresult' : result ∈ Code.eval (Code.rfind' f) n := by + rw [hresult]; exact Part.mem_some _ + simp only [Code.eval, Nat.unpaired, + show (Nat.unpair n).1 = a₀ from rfl, + show (Nat.unpair n).2 = m₀ from rfl] at hresult' + obtain ⟨k, hk_mem, hresult_eq⟩ := (Part.mem_map_iff _).mp hresult' + subst hresult_eq + -- Build the callback: the composed SKI term computes f on paired arguments + set g := B ⬝ tf ⬝ (NatPair ⬝ (NatUnpairLeft ⬝ cn)) + have hg : ∀ i y, IsChurch i y → ∀ v, f.eval (Nat.pair a₀ i) = Part.some v → + IsChurch v (g ⬝ y) := fun i y hy v hv => + isChurch_trans _ (B_def tf (NatPair ⬝ (NatUnpairLeft ⬝ cn)) y) + (ihf _ _ (natPair_correct a₀ i (NatUnpairLeft ⬝ cn) y hca hy) v hv) + -- Apply generalized RFindAbove_correct' + have hind := RFindAbove_correct' g (NatUnpairRight ⬝ cn) k m₀ hcm₀ + (fun y hy => hg (m₀ + k) y hy 0 (rfind_eval_root hk_mem)) + (fun i hi y hy => by + obtain ⟨vi, hvi_ne, hvi_eq⟩ := rfind_eval_pos_below hk_mem i hi + exact ⟨vi - 1, by have : vi - 1 + 1 = vi := by omega + rw [this]; exact hg (m₀ + i) y hy vi hvi_eq⟩) + rw [Nat.add_comm] at hind + exact isChurch_trans _ (rfindTrans_def tf cn) hind /-- Main correctness theorem: `codeToSKINat` correctly computes `Code.eval`. -/ theorem codeToSKINat_correct (c : Code) : Computes (codeToSKINat c) c.eval := by @@ -290,49 +293,13 @@ theorem codeToSKINat_correct (c : Code) : Computes (codeToSKINat c) c.eval := by | left => exact left_computes | right => exact right_computes | pair f g ihf ihg => - simp only [codeToSKINat, Code.eval] - exact pair_computes ihf ihg + simp only [codeToSKINat, Code.eval]; exact pair_computes ihf ihg | comp f g ihf ihg => - simp only [codeToSKINat, Code.eval] - exact comp_computes ihf ihg + simp only [codeToSKINat, Code.eval]; exact comp_computes ihf ihg | prec f g ihf ihg => - simp only [codeToSKINat] - intro n cn hcn m hm - have hca := natUnpairLeft_correct n cn hcn - have hcb := natUnpairRight_correct n cn hcn - have hred := precTrans_def (codeToSKINat f) (codeToSKINat g) cn - -- Rewrite eval in terms of unpair components - have hpair : n = Nat.pair (Nat.unpair n).1 (Nat.unpair n).2 := - (Nat.pair_unpair n).symm - rw [hpair] at hm - exact isChurch_trans _ hred (prec_rec_correct f g _ _ ihf ihg - (Nat.unpair n).1 (NatUnpairLeft ⬝ cn) hca - (Nat.unpair n).2 m hm (NatUnpairRight ⬝ cn) hcb) + simp only [codeToSKINat]; exact prec_computes ihf ihg | rfind' f ihf => - simp only [codeToSKINat] - intro n cn hcn result hresult - set tf := codeToSKINat f - set a₀ := (Nat.unpair n).1 - set m₀ := (Nat.unpair n).2 - have hca := natUnpairLeft_correct n cn hcn - have hcm₀ := natUnpairRight_correct n cn hcn - have hred := rfindTrans_def tf cn - -- Extract k from the rfind result - have hresult' : result ∈ Code.eval (Code.rfind' f) n := by - rw [hresult]; exact Part.mem_some _ - simp only [Code.eval, Nat.unpaired, - show (Nat.unpair n).1 = a₀ from rfl, - show (Nat.unpair n).2 = m₀ from rfl] at hresult' - obtain ⟨k, hk_mem, hresult_eq⟩ := (Part.mem_map_iff _).mp hresult' - subst hresult_eq - have heval_root := rfind_eval_root hk_mem - have heval_below := rfind_eval_pos_below hk_mem - set g := B ⬝ tf ⬝ (NatPair ⬝ (NatUnpairLeft ⬝ cn)) - have hind := rfindAbove_induction f tf ihf a₀ - (NatUnpairLeft ⬝ cn) hca g rfl k m₀ - (NatUnpairRight ⬝ cn) hcm₀ heval_root heval_below - rw [Nat.add_comm] at hind - exact isChurch_trans _ hred hind + simp only [codeToSKINat]; exact rfind_computes ihf /-! ### Main result -/ From a4fc0224f9277aec1e8e801d80dd5222f73ea54c Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Tue, 31 Mar 2026 16:33:12 +0200 Subject: [PATCH 10/13] refactor: move bind_eq_some to Cslib.Foundations.Data.Part Promote the private helper to Part.eq_some_of_bind_eq_some in a new shared foundations file, making it available to other modules. --- Cslib.lean | 1 + Cslib/Foundations/Data/Part.lean | 28 +++++++++++++++++++ .../CombinatoryLogic/PartrecToSKI.lean | 12 ++------ 3 files changed, 32 insertions(+), 9 deletions(-) create mode 100644 Cslib/Foundations/Data/Part.lean diff --git a/Cslib.lean b/Cslib.lean index 94e683ade..f0ec03ec1 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -44,6 +44,7 @@ public import Cslib.Foundations.Data.BiTape public import Cslib.Foundations.Data.FinFun public import Cslib.Foundations.Data.HasFresh public import Cslib.Foundations.Data.Nat.Segment +public import Cslib.Foundations.Data.Part public import Cslib.Foundations.Data.OmegaSequence.Defs public import Cslib.Foundations.Data.OmegaSequence.Flatten public import Cslib.Foundations.Data.OmegaSequence.InfOcc diff --git a/Cslib/Foundations/Data/Part.lean b/Cslib/Foundations/Data/Part.lean new file mode 100644 index 000000000..343b3c529 --- /dev/null +++ b/Cslib/Foundations/Data/Part.lean @@ -0,0 +1,28 @@ +/- +Copyright (c) 2026 Jesse Alama. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jesse Alama +-/ + +module + +public import Mathlib.Data.Part + +@[expose] public section + +/-! +# Auxiliary lemmas for `Part` + +Convenience lemmas for working with partial values from `Mathlib.Data.Part`. +-/ + +namespace Part + +/-- Extract witnesses from a bind that equals `Part.some`. -/ +theorem eq_some_of_bind_eq_some {a : Part α} {g : α → Part β} {m : β} + (h : (a >>= g) = Part.some m) : + ∃ x, a = Part.some x ∧ g x = Part.some m := by + have hm := Part.mem_bind_iff.mp (h ▸ Part.mem_some m) + exact hm.imp fun x ⟨hx, hm⟩ => ⟨Part.eq_some_iff.mpr hx, Part.eq_some_iff.mpr hm⟩ + +end Part diff --git a/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean b/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean index b29ee265a..3e4b89894 100644 --- a/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean +++ b/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean @@ -6,6 +6,7 @@ Authors: Jesse Alama module +public import Cslib.Foundations.Data.Part public import Cslib.Languages.CombinatoryLogic.Recursion public import Mathlib.Computability.PartrecCode @@ -115,13 +116,6 @@ def codeToSKINat : Code → SKI /-! ### Correctness proofs -/ -/-- Extract witnesses from a bind that equals `Part.some`. -/ -private theorem bind_eq_some {a : Part α} {g : α → Part β} {m : β} - (h : (a >>= g) = Part.some m) : - ∃ x, a = Part.some x ∧ g x = Part.some m := by - have hm := Part.mem_bind_iff.mp (h ▸ Part.mem_some m) - exact hm.imp fun x ⟨hx, hm⟩ => ⟨Part.eq_some_iff.mpr hx, Part.eq_some_iff.mpr hm⟩ - /-- Helper for total functions: if `c.eval` is total with output `g n`, and `t` reduces to a Church numeral for `g n`, then `t` computes `c.eval`. -/ private theorem computes_of_total (t : SKI) (c : Code) (g : ℕ → ℕ) @@ -160,7 +154,7 @@ theorem comp_computes {f g : ℕ →. ℕ} {tf tg : SKI} (hf : Computes tf f) (hg : Computes tg g) : Computes (B ⬝ tf ⬝ tg) (fun n => g n >>= f) := by intro n cn hcn m hm - obtain ⟨intermediate, hint_eq, hm_eq⟩ := bind_eq_some hm + obtain ⟨intermediate, hint_eq, hm_eq⟩ := Part.eq_some_of_bind_eq_some hm exact isChurch_trans _ (B_def tf tg cn) (hf intermediate (tg ⬝ cn) (hg n cn hcn intermediate hint_eq) m hm_eq) @@ -196,7 +190,7 @@ private theorem prec_rec_correct (f g : Code) (tf tg : SKI) | succ k ih => intro m hm cb hcb rw [Code.eval_prec_succ] at hm - obtain ⟨ih_val, hih_eq, hm_eq⟩ := bind_eq_some hm + obtain ⟨ih_val, hih_eq, hm_eq⟩ := Part.eq_some_of_bind_eq_some hm -- By IH, Rec computes the intermediate value on Pred ⬝ cb have hpred : IsChurch k (Pred ⬝ cb) := pred_correct (k + 1) cb hcb set step := PrecStep tg ⬝ ca From fe9a8029d747235435f308dbe57ee9f2e2d2ee85 Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Wed, 1 Apr 2026 22:23:27 +0200 Subject: [PATCH 11/13] chore: regenerate Cslib.lean import file --- Cslib.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib.lean b/Cslib.lean index f0ec03ec1..fc9515419 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -44,12 +44,12 @@ public import Cslib.Foundations.Data.BiTape public import Cslib.Foundations.Data.FinFun public import Cslib.Foundations.Data.HasFresh public import Cslib.Foundations.Data.Nat.Segment -public import Cslib.Foundations.Data.Part public import Cslib.Foundations.Data.OmegaSequence.Defs public import Cslib.Foundations.Data.OmegaSequence.Flatten public import Cslib.Foundations.Data.OmegaSequence.InfOcc public import Cslib.Foundations.Data.OmegaSequence.Init public import Cslib.Foundations.Data.OmegaSequence.Temporal +public import Cslib.Foundations.Data.Part public import Cslib.Foundations.Data.RelatesInSteps public import Cslib.Foundations.Data.Relation public import Cslib.Foundations.Data.Set.Saturation From c9de35eacab917890880d3c9a3673b82cdfdae72 Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Wed, 1 Apr 2026 22:53:15 +0200 Subject: [PATCH 12/13] fix: add missing Cslib.Init import to Part.lean CI checkInitImports requires all Cslib modules to import Cslib.Init. --- Cslib/Foundations/Data/Part.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Cslib/Foundations/Data/Part.lean b/Cslib/Foundations/Data/Part.lean index 343b3c529..de6d2b212 100644 --- a/Cslib/Foundations/Data/Part.lean +++ b/Cslib/Foundations/Data/Part.lean @@ -6,6 +6,7 @@ Authors: Jesse Alama module +public import Cslib.Init public import Mathlib.Data.Part @[expose] public section From 4efedc096d0a73e9ab5a1ae28e4c91cfc3d07a33 Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Wed, 1 Apr 2026 22:54:46 +0200 Subject: [PATCH 13/13] docs(Part): note dependency on mathlib4#37521 --- Cslib/Foundations/Data/Part.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Cslib/Foundations/Data/Part.lean b/Cslib/Foundations/Data/Part.lean index de6d2b212..97da80f6d 100644 --- a/Cslib/Foundations/Data/Part.lean +++ b/Cslib/Foundations/Data/Part.lean @@ -15,6 +15,8 @@ public import Mathlib.Data.Part # Auxiliary lemmas for `Part` Convenience lemmas for working with partial values from `Mathlib.Data.Part`. + +Note: this file may go away entirely if leanprover-community/mathlib4#37521 gets merged. -/ namespace Part