General recursion in the SKI calculus

In this file we implement general recursion functions (on the natural numbers), inspired by the formalisation of Mathlib.Computability.Partrec. Since composition (B-combinator) and pairs (MkPair, Fst, Snd) have been implemented in Cslib.Computability.CombinatoryLogic.Basic, what remains are the following definitions and proofs of their correctness.

• Church numerals : a predicate IsChurch n a expressing that the term a is βη-equivalent to the standard church numeral n — that is, a ⬝ f ⬝ x ↠ f ⬝ (f ⬝ ... ⬝ (f ⬝ x))).
• SKI numerals : Zero and Succ, corresponding to Partrec.zero and Partrec.succ, and correctness proofs zero_correct and succ_correct.
• Predecessor : a term Pred so that (pred_correct) IsChurch n a → IsChurch n.pred (Pred ⬝ a).
• Primitive recursion : a term Rec so that (rec_correct_succ) IsChurch (n+1) a implies Rec ⬝ x ⬝ g ⬝ a ↠ g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a)) and (rec_correct_zero) IsChurch 0 a implies Rec ⬝ x ⬝ g ⬝ a ↠ x.
• Unbounded root finding (μ-recursion) : given a term f representing a function fℕ: Nat → Nat, which takes on the value 0 a term RFind such that (rFind_correct) RFind ⬝ f ↠ a such that IsChurch n a for n the smallest root of fℕ.

References

• For church numerals and recursion via the fixed-point combinator, see sections 3.2 and 3.3 of Selinger's notes https://www.mscs.dal.ca/~selinger/papers/papers/lambdanotes.pdf

TODO

• One could unify is_bool, IsChurch and IsChurchPair into a predicate represents : α → SKI → Prop, for any type α "built from pieces that we understand" — something along the lines of "pure finite types" (see eg https://en.wikipedia.org/wiki/Primitive_recursive_functional). This would also clean up the statement of rfind_correct.
• The predicate ∃ n : Nat, IsChurch n : SKI → Prop is semidecidable: by confluence, it suffices to normal-order reduce a ⬝ f ⬝ x for any "atomic" terms f and x. This could be implemented by defining reduction on polynomials.
• With such a decision procedure, every SKI-term defines a partial function Nat →. Nat, in the sense of Mathlib.Data.Part (as used in Mathlib.Computability.Partrec).
• The results of this file should define a surjection SKI → Nat.Partrec.

def Cslib.SKI.Church (n : ℕ) (f x : SKI) : SKI

Function form of the church numerals.

Equations

• Cslib.SKI.Church 0 f x = x
• Cslib.SKI.Church n_2.succ f x = f.app (Cslib.SKI.Church n_2 f x)

@[simp]

theorem Cslib.SKI.Church_zero (f x : SKI) : Church 0 f x = x

@[simp]

theorem Cslib.SKI.Church_succ (n : ℕ) (f x : SKI) : Church (n + 1) f x = f.app (Church n f x)

theorem Cslib.SKI.church_red (n : ℕ) (f f' x x' : SKI) (hf : Relation.ReflTransGen Red f f') (hx : Relation.ReflTransGen Red x x') : Relation.ReflTransGen Red (Church n f x) (Church n f' x')

church commutes with reduction.

def Cslib.SKI.IsChurch (n : ℕ) (a : SKI) : Prop

The term a is βη-equivalent to a standard church numeral.

Equations

• Cslib.SKI.IsChurch n a = ∀ (f x : Cslib.SKI), Relation.ReflTransGen Cslib.SKI.Red ((a.app f).app x) (Cslib.SKI.Church n f x)

theorem Cslib.SKI.isChurch_trans (n : ℕ) {a a' : SKI} (h : Relation.ReflTransGen Red a a') : IsChurch n a' → IsChurch n a

To show IsChurch n a it suffices to show the same for a reduct of a.

Church numeral basics

def Cslib.SKI.Zero : SKI

Church zero := λ f x. x

Equations

• Cslib.SKI.Zero = Cslib.SKI.K.app Cslib.SKI.I

theorem Cslib.SKI.zero_correct : IsChurch 0 SKI.Zero

def Cslib.SKI.One : SKI

Church one := λ f x. f x

Equations

• Cslib.SKI.One = Cslib.SKI.I

theorem Cslib.SKI.one_correct : IsChurch 1 SKI.One

def Cslib.SKI.Succ : SKI

Church succ := λ a f x. f (a f x) λ a f. B f (a f) λ a. S B a ~ S B

Equations

• Cslib.SKI.Succ = Cslib.SKI.S.app Cslib.SKI.B

theorem Cslib.SKI.succ_correct (n : ℕ) (a : SKI) (h : IsChurch n a) : IsChurch (n + 1) (SKI.Succ.app a)

def Cslib.SKI.toChurch : ℕ → SKI

Build the canonical SKI Church numeral for n.

Equations

• Cslib.SKI.toChurch 0 = Cslib.SKI.Zero
• Cslib.SKI.toChurch n_1.succ = Cslib.SKI.Succ.app (Cslib.SKI.toChurch n_1)

@[simp]

theorem Cslib.SKI.toChurch_zero : toChurch 0 = SKI.Zero

toChurch 0 = Zero.

@[simp]

theorem Cslib.SKI.toChurch_succ (n : ℕ) : toChurch (n + 1) = SKI.Succ.app (toChurch n)

toChurch (n + 1) = Succ ⬝ toChurch n.

theorem Cslib.SKI.toChurch_correct (n : ℕ) : IsChurch n (toChurch n)

toChurch n correctly represents n.

def Cslib.SKI.PredAuxPoly : SKI.Polynomial 1

To define the predecessor, iterate the function PredAux ⟨i, j⟩ ↦ ⟨j, j+1⟩ on ⟨0,0⟩, then take the first component.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.SKI.PredAux : SKI

A term representing PredAux

Equations

• Cslib.SKI.PredAux = Cslib.SKI.PredAuxPoly.toSKI

theorem Cslib.SKI.predAux_def (p : SKI) : Relation.ReflTransGen Red (PredAux.app p) ((MkPair.app (Snd.app p)).app (SKI.Succ.app (Snd.app p)))

def Cslib.SKI.IsChurchPair (ns : ℕ × ℕ) (x : SKI) : Prop

Useful auxiliary definition expressing that p represents ns ∈ Nat × Nat.

Equations

• Cslib.SKI.IsChurchPair ns x = (Cslib.SKI.IsChurch ns.1 (Cslib.SKI.Fst.app x) ∧ Cslib.SKI.IsChurch ns.2 (Cslib.SKI.Snd.app x))

theorem Cslib.SKI.isChurchPair_trans (ns : ℕ × ℕ) (a a' : SKI) (h : Relation.ReflTransGen Red a a') : IsChurchPair ns a' → IsChurchPair ns a

theorem Cslib.SKI.predAux_correct (p : SKI) (ns : ℕ × ℕ) (h : IsChurchPair ns p) : IsChurchPair (ns.2, ns.2 + 1) (PredAux.app p)

theorem Cslib.SKI.predAux_correct' (n : ℕ) : IsChurchPair (n.pred, n) (Church n PredAux ((MkPair.app SKI.Zero).app SKI.Zero))

The stronger induction hypothesis necessary for the proof of pred_correct.

def Cslib.SKI.PredPoly : SKI.Polynomial 1

Predecessor := λ n. Fst ⬝ (n ⬝ PredAux ⬝ (MkPair ⬝ Zero ⬝ Zero))

Equations

• One or more equations did not get rendered due to their size.

def Cslib.SKI.Pred : SKI

A term representing Pred

Equations

• Cslib.SKI.Pred = Cslib.SKI.PredPoly.toSKI

theorem Cslib.SKI.pred_def (a : SKI) : Relation.ReflTransGen Red (Pred.app a) (Fst.app ((a.app PredAux).app ((MkPair.app SKI.Zero).app SKI.Zero)))

theorem Cslib.SKI.pred_correct (n : ℕ) (a : SKI) (h : IsChurch n a) : IsChurch n.pred (Pred.app a)

Primitive recursion

def Cslib.SKI.IsZeroPoly : SKI.Polynomial 1

IsZero := λ n. n (K FF) TT

Equations

• Cslib.SKI.IsZeroPoly = ((Cslib.SKI.Polynomial.var 0).app (Cslib.SKI.Polynomial.term (Cslib.SKI.K.app Cslib.SKI.FF))).app (Cslib.SKI.Polynomial.term Cslib.SKI.TT)

def Cslib.SKI.IsZero : SKI

A term representing IsZero

Equations

• Cslib.SKI.IsZero = Cslib.SKI.IsZeroPoly.toSKI

theorem Cslib.SKI.isZero_def (a : SKI) : Relation.ReflTransGen Red (IsZero.app a) ((a.app (K.app FF)).app TT)

theorem Cslib.SKI.isZero_correct (n : ℕ) (a : SKI) (h : IsChurch n a) : IsBool (decide (n = 0)) (IsZero.app a)

def Cslib.SKI.RecAuxPoly : SKI.Polynomial 4

To define Rec x g n := if n==0 then x else (Rec x g (Pred n)), we obtain a fixed point of R ↦ λ x g n. Cond ⬝ (IsZero ⬝ n) ⬝ x ⬝ (g ⬝ a ⬝ (R ⬝ x ⬝ g ⬝ (Pred ⬝ n)))

Equations

• One or more equations did not get rendered due to their size.

def Cslib.SKI.RecAux : SKI

A term representing RecAux

Equations

• Cslib.SKI.RecAux = Cslib.SKI.RecAuxPoly.toSKI

theorem Cslib.SKI.recAux_def (R₀ x g a : SKI) : Relation.ReflTransGen Red ((((RecAux.app R₀).app x).app g).app a) (((SKI.Cond.app x).app ((g.app a).app (((R₀.app x).app g).app (Pred.app a)))).app (IsZero.app a))

def Cslib.SKI.Rec : SKI

We define Rec so that Rec ⬝ x ⬝ g ⬝ a ↠ SKI.Cond ⬝ x ⬝ (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) ⬝ (IsZero ⬝ a)

Equations

• Cslib.SKI.Rec = Cslib.SKI.RecAux.fixedPoint

theorem Cslib.SKI.rec_def (x g a : SKI) : Relation.ReflTransGen Red (((Rec.app x).app g).app a) (((SKI.Cond.app x).app ((g.app a).app (((Rec.app x).app g).app (Pred.app a)))).app (IsZero.app a))

theorem Cslib.SKI.rec_zero (x g a : SKI) (ha : IsChurch 0 a) : Relation.ReflTransGen Red (((Rec.app x).app g).app a) x

theorem Cslib.SKI.rec_succ (n : ℕ) (x g a : SKI) (ha : IsChurch (n + 1) a) : Relation.ReflTransGen Red (((Rec.app x).app g).app a) ((g.app a).app (((Rec.app x).app g).app (Pred.app a)))

Root-finding (μ-recursion)

def Cslib.SKI.RFindAboveAuxPoly : SKI.Polynomial 3

First define an auxiliary function RFindAbove that looks for roots above a fixed number n, as a fixed point of R ↦ λ n f. if f n = 0 then n else R f (n+1) ~ λ n f. Cond ⬝ n (R f (Succ n)) (IsZero (f n))

Equations

• One or more equations did not get rendered due to their size.

def Cslib.SKI.RFindAboveAux : SKI

A term representing RFindAboveAux

Equations

• Cslib.SKI.RFindAboveAux = Cslib.SKI.RFindAboveAuxPoly.toSKI

theorem Cslib.SKI.rfindAboveAux_def (R₀ f a : SKI) : Relation.ReflTransGen Red (((RFindAboveAux.app R₀).app a).app f) (((SKI.Cond.app a).app ((R₀.app (SKI.Succ.app a)).app f)).app (IsZero.app (f.app a)))

theorem Cslib.SKI.rfindAboveAux_base (R₀ f a : SKI) (hfa : IsChurch 0 (f.app a)) : Relation.ReflTransGen Red (((RFindAboveAux.app R₀).app a).app f) a

theorem Cslib.SKI.rfindAboveAux_step (R₀ f a : SKI) {m : ℕ} (hfa : IsChurch (m + 1) (f.app a)) : Relation.ReflTransGen Red (((RFindAboveAux.app R₀).app a).app f) ((R₀.app (SKI.Succ.app a)).app f)

def Cslib.SKI.RFindAbove : SKI

Find the minimal root of fNat above a number n

Equations

• Cslib.SKI.RFindAbove = Cslib.SKI.RFindAboveAux.fixedPoint

theorem Cslib.SKI.RFindAbove_correct (fNat : ℕ → ℕ) (f x : SKI) (hf : ∀ (i : ℕ) (y : SKI), IsChurch i y → IsChurch (fNat i) (f.app y)) (n m : ℕ) (hx : IsChurch m x) (hroot : fNat (m + n) = 0) (hpos : ∀ (i : ℕ), i < n → fNat (m + i) ≠ 0) : IsChurch (m + n) ((RFindAbove.app x).app f)

def Cslib.SKI.RFind : SKI

Ordinary root finding is root finding above zero

Equations

• Cslib.SKI.RFind = Cslib.SKI.RFindAbove.app Cslib.SKI.Zero

theorem Cslib.SKI.RFind_correct (fNat : ℕ → ℕ) (f : SKI) (hf : ∀ (i : ℕ) (y : SKI), IsChurch i y → IsChurch (fNat i) (f.app y)) (n : ℕ) (hroot : fNat n = 0) (hpos : ∀ (i : ℕ), i < n → fNat i ≠ 0) : IsChurch n (RFind.app f)

Further numeric operations

def Cslib.SKI.AddPoly : SKI.Polynomial 2

Addition: λ n m. n Succ m

Equations

• Cslib.SKI.AddPoly = ((Cslib.SKI.Polynomial.var 0).app (Cslib.SKI.Polynomial.term Cslib.SKI.Succ)).app (Cslib.SKI.Polynomial.var 1)

def Cslib.SKI.Add : SKI

A term representing addition on church numerals

Equations

• Cslib.SKI.Add = Cslib.SKI.AddPoly.toSKI

theorem Cslib.SKI.add_def (a b : SKI) : Relation.ReflTransGen Red ((SKI.Add.app a).app b) ((a.app SKI.Succ).app b)

theorem Cslib.SKI.add_correct (n m : ℕ) (a b : SKI) (ha : IsChurch n a) (hb : IsChurch m b) : IsChurch (n + m) ((SKI.Add.app a).app b)

def Cslib.SKI.MulPoly : SKI.Polynomial 2

Multiplication: λ n m. n (Add m) Zero

Equations

• Cslib.SKI.MulPoly = ((Cslib.SKI.Polynomial.var 0).app ((Cslib.SKI.Polynomial.term Cslib.SKI.Add).app (Cslib.SKI.Polynomial.var 1))).app (Cslib.SKI.Polynomial.term Cslib.SKI.Zero)

def Cslib.SKI.Mul : SKI

A term representing multiplication on church numerals

Equations

• Cslib.SKI.Mul = Cslib.SKI.MulPoly.toSKI

theorem Cslib.SKI.mul_def (a b : SKI) : Relation.ReflTransGen Red ((SKI.Mul.app a).app b) ((a.app (SKI.Add.app b)).app SKI.Zero)

theorem Cslib.SKI.mul_correct {n m : ℕ} {a b : SKI} (ha : IsChurch n a) (hb : IsChurch m b) : IsChurch (n * m) ((SKI.Mul.app a).app b)

def Cslib.SKI.SubPoly : SKI.Polynomial 2

Subtraction: λ n m. n Pred m

Equations

• Cslib.SKI.SubPoly = ((Cslib.SKI.Polynomial.var 1).app (Cslib.SKI.Polynomial.term Cslib.SKI.Pred)).app (Cslib.SKI.Polynomial.var 0)

def Cslib.SKI.Sub : SKI

A term representing subtraction on church numerals

Equations

• Cslib.SKI.Sub = Cslib.SKI.SubPoly.toSKI

theorem Cslib.SKI.sub_def (a b : SKI) : Relation.ReflTransGen Red ((SKI.Sub.app a).app b) ((b.app Pred).app a)

theorem Cslib.SKI.sub_correct (n m : ℕ) (a b : SKI) (ha : IsChurch n a) (hb : IsChurch m b) : IsChurch (n - m) ((SKI.Sub.app a).app b)

def Cslib.SKI.LEPoly : SKI.Polynomial 2

Comparison: (. ≤ .) := λ n m. IsZero ⬝ (Sub ⬝ n ⬝ m)

Equations

• Cslib.SKI.LEPoly = (Cslib.SKI.Polynomial.term Cslib.SKI.IsZero).app (((Cslib.SKI.Polynomial.term Cslib.SKI.Sub).app (Cslib.SKI.Polynomial.var 0)).app (Cslib.SKI.Polynomial.var 1))

def Cslib.SKI.LE : SKI

A term representing comparison on church numerals

Equations

• Cslib.SKI.LE = Cslib.SKI.LEPoly.toSKI

theorem Cslib.SKI.le_def (a b : SKI) : Relation.ReflTransGen Red ((SKI.LE.app a).app b) (IsZero.app ((SKI.Sub.app a).app b))

theorem Cslib.SKI.le_correct (n m : ℕ) (a b : SKI) (ha : IsChurch n a) (hb : IsChurch m b) : IsBool (decide (n ≤ m)) ((SKI.LE.app a).app b)