feat(CombinatoryLogic): Partrec → SKI computability

Cslib.lean

@@ -110,10 +110,12 @@ public import Cslib.Languages.CCS.Basic
 public import Cslib.Languages.CCS.BehaviouralTheory
 public import Cslib.Languages.CCS.Semantics
 public import Cslib.Languages.CombinatoryLogic.Basic
+public import Cslib.Languages.CombinatoryLogic.Computable
 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.PartrecToSKI
 public import Cslib.Languages.CombinatoryLogic.Recursion
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic

Cslib/Languages/CombinatoryLogic/Computable.lean

@@ -0,0 +1,83 @@
+/-
+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.Data.PFun
+
+/-!
+# SKI-computable functions
+
+This file defines the notion of SKI-computability for partial functions on natural
+numbers, via Church numerals: a term computes `f : ℕ →. ℕ` if it maps Church numeral
+inputs to Church numeral outputs wherever `f` is defined.
+
+## Main definitions
+
+- `SKI.Computes`: an SKI term computes a given partial function.
+- `SKI.Computable`: a partial function is SKI-computable if some SKI term computes it.
+
+## Implementation notes
+
+Unlike `Cslib.URM.Computes`, which is a two-sided equality of `Part` values, this
+predicate is one-sided: it constrains the term's behavior only where the function is
+defined, and says nothing about inputs outside the domain.
+-/
+
+@[expose] public section
+
+namespace Cslib
+
+namespace SKI
+
+open Red MRed
+
+/-- An SKI term `t` computes a partial function `f : ℕ →. ℕ` if,
+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 : ℕ, m ∈ f n →
+      IsChurch m (t ⬝ cn)
+
+/-- A partial function `f : ℕ →. ℕ` is SKI-computable if there exists an SKI term that
+computes it. -/
+def Computable (f : ℕ →. ℕ) : Prop :=
+  ∃ t : SKI, Computes t f
+
+/-- To show that a term computes a total function, it suffices to produce a Church
+numeral for the output on every input. -/
+theorem computes_of_total {t : SKI} {f : ℕ →. ℕ} (g : ℕ → ℕ)
+    (heval : ∀ n, f n = Part.some (g n))
+    (hcorrect : ∀ n cn, IsChurch n cn → IsChurch (g n) (t ⬝ cn)) :
+    Computes t f := by
+  intro n cn hcn m hm; rw [heval] at hm; obtain rfl := Part.mem_some_iff.mp hm
+  exact hcorrect n cn hcn
+
+/-- 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
+  obtain ⟨intermediate, hint_mem, hm_mem⟩ := Part.mem_bind_iff.mp hm
+  exact isChurch_trans _ (B_def tf tg cn)
+    (hf intermediate (tg ⬝ cn) (hg n cn hcn intermediate hint_mem) m hm_mem)
+
+/-- 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 [Seq.seq, Functor.map, Part.mem_bind_iff, Part.mem_map_iff] at hm
+  obtain ⟨_, ⟨a, ha, rfl⟩, b, hb, rfl⟩ := hm
+  exact isChurch_trans _ ((MRed.S _ _ _).trans (MRed.head _ (B_def _ _ _)))
+    (natPair_correct a b _ _ (hf n cn hcn a ha) (hg n cn hcn b hb))
+
+end SKI
+
+end Cslib

Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean

@@ -0,0 +1,255 @@
+/-
+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.Computable
+public import Mathlib.Computability.PartrecCode
+
+/-!
+# Partial Recursive → SKI-computable (Nat.Partrec)
+
+This file translates `Nat.Partrec.Code` to SKI terms and proves the translation
+correct, showing that every partial recursive function is SKI-computable in the
+sense of `SKI.Computes` (from `Cslib.Languages.CombinatoryLogic.Computable`).
+
+## Main definitions
+
+- `codeToSKINat`: translates `Nat.Partrec.Code` constructors to SKI terms.
+
+## Main results
+
+- `codeToSKINat_correct`: each translated code computes the corresponding `Code.eval`.
+- `natPartrec_skiComputable`: every `Nat.Partrec` function is SKI-computable.
+
+-/
+
+@[expose] public section
+
+namespace Cslib
+
+namespace SKI
+
+open Red MRed
+open Nat.Partrec
+
+/-! ### Helper terms for `Code.prec` and `Code.rfind'` -/
+
+/-- 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 via `Rec` with pair/unpair plumbing. -/
+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. -/
+private theorem zero_computes : Computes (K ⬝ SKI.Zero) (Code.eval .zero) :=
+  computes_of_total (fun _ => 0) (fun _ => rfl)
+    (fun _ _ _ => isChurch_trans 0 (MRed.K SKI.Zero _) zero_correct)
+
+/-- `Code.succ` computes the successor function. -/
+private theorem succ_computes : Computes SKI.Succ (Code.eval .succ) :=
+  computes_of_total (· + 1) (fun _ => rfl) succ_correct
+
+/-- `Code.left` computes the left projection of `Nat.unpair`. -/
+private theorem left_computes : Computes NatUnpairLeft (Code.eval .left) :=
+  computes_of_total (fun n => (Nat.unpair n).1) (fun _ => rfl) natUnpairLeft_correct
+
+/-- `Code.right` computes the right projection of `Nat.unpair`. -/
+private theorem right_computes : Computes NatUnpairRight (Code.eval .right) :=
+  computes_of_total (fun n => (Nat.unpair n).2) (fun _ => rfl) natUnpairRight_correct
+
+/-- 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 : ℕ,
+    m ∈ Code.eval (f.prec g) (Nat.pair a₀ b₀) →
+    ∀ cb : SKI, IsChurch b₀ cb →
+    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
+    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
+    obtain ⟨ih_val, hih_eq, hm_eq⟩ := Part.mem_bind_iff.mp 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
+    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)
+      (Rec ⬝ base ⬝ step ⬝ (Pred ⬝ cb)) hpred hcih
+    have hpair_full := natPair_correct a₀ (Nat.pair k ih_val) ca
+      (NatPair ⬝ (Pred ⬝ cb) ⬝ (Rec ⬝ base ⬝ step ⬝ (Pred ⬝ cb))) hca hpair_inner
+    -- By ihg, tg computes the result
+    have hcm := ihg _ _ hpair_full m hm_eq
+    -- Chain the reductions
+    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
+
+/-- Shared extraction step for the `rfind` predicate: from membership of a boolean `b` in
+`decide (· = 0) <$> f.eval (a₀, j + m₀)` recover the underlying value `v`, together with the
+fact that `decide (v = 0) = b`. Used by both the root and below-root analyses. -/
+private theorem rfind_eval_aux {f : Code} {a₀ m₀ j : ℕ} {b : Bool}
+    (h : b ∈ (fun m => decide (m = 0)) <$> f.eval (Nat.pair a₀ (j + m₀))) :
+    ∃ v, decide (v = 0) = b ∧ v ∈ f.eval (Nat.pair a₀ (m₀ + j)) := by
+  obtain ⟨v, hv_mem, hv_eq⟩ := (Part.mem_map_iff _).mp h
+  rw [Nat.add_comm] at hv_mem
+  exact ⟨v, hv_eq, hv_mem⟩
+
+/-- 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₀)))) :
+    (0 : ℕ) ∈ f.eval (Nat.pair a₀ (m₀ + k)) := by
+  obtain ⟨v, hv_eq, hv_mem⟩ := rfind_eval_aux (Nat.rfind_spec hk)
+  obtain rfl : v = 0 := by simpa using hv_eq
+  exact hv_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₀)))) :
+    ∀ i < k, ∃ vi, vi ≠ 0 ∧ vi ∈ f.eval (Nat.pair a₀ (m₀ + i)) := by
+  intro i hi
+  obtain ⟨v, hv_eq, hv_mem⟩ := rfind_eval_aux (Nat.rfind_min hk hi)
+  exact ⟨v, by simpa using hv_eq, hv_mem⟩
+
+/-- 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
+  rw [← Nat.pair_unpair n] at hm
+  exact isChurch_trans _ (precTrans_def tf tg cn) (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
+  have hca := natUnpairLeft_correct n cn hcn
+  have hcm₀ := natUnpairRight_correct n cn hcn
+  -- Extract k from the rfind result
+  simp only [Code.eval, Nat.unpaired] at hresult
+  set a₀ := (Nat.unpair n).1
+  set m₀ := (Nat.unpair n).2
+  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, v ∈ f.eval (Nat.pair a₀ i) →
+      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_mem⟩ := rfind_eval_pos_below hk_mem i hi
+      exact ⟨vi - 1, Nat.succ_pred_eq_of_ne_zero hvi_ne ▸ hg (m₀ + i) y hy vi hvi_mem⟩)
+  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
+  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]; exact prec_computes ihf ihg
+  | rfind' f ihf =>
+    simp only [codeToSKINat]; exact rfind_computes ihf
+
+/-! ### Main result -/
+
+/-- Every partial recursive function on `ℕ` is SKI-computable. -/
+theorem natPartrec_skiComputable (f : ℕ →. ℕ) (hf : Nat.Partrec f) :
+    SKI.Computable f := by
+  obtain ⟨c, hc⟩ := Code.exists_code.mp hf
+  exact ⟨codeToSKINat c, hc ▸ codeToSKINat_correct c⟩
+
+end SKI
+
+end Cslib