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ℕ.
• Integer square root : a term Sqrt so that (sqrt_correct) IsChurch n a → IsChurch n.sqrt (Sqrt ⬝ a).
• Nat pairing : a term NatPair so that (natPair_correct) IsChurch a x → IsChurch b y → IsChurch (Nat.pair a b) (NatPair ⬝ x ⬝ y).
• Nat unpairing : terms NatUnpairLeft and NatUnpairRight so that (natUnpairLeft_correct) IsChurch n a → IsChurch n.unpair.1 (NatUnpairLeft ⬝ a) and (natUnpairRight_correct) IsChurch n a → IsChurch n.unpair.2 (NatUnpairRight ⬝ a).

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 < 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 < 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)

Integer square root

def Cslib.SKI.SqrtCondPoly : SKI.Polynomial 2

Inner condition for Sqrt: with &0 = n, &1 = k, computes if n < (k+1)² then 0 else 1.

Equations

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

def Cslib.SKI.SqrtCond : SKI

SKI term for the inner condition of Sqrt

Equations

• Cslib.SKI.SqrtCond = Cslib.SKI.SqrtCondPoly.toSKI

theorem Cslib.SKI.sqrtCond_def (cn ck : SKI) : Relation.ReflTransGen Red ((SqrtCond.app cn).app ck) (((SKI.Cond.app SKI.Zero).app SKI.One).app (SKI.Neg.app ((SKI.LE.app ((SKI.Mul.app (SKI.Succ.app ck)).app (SKI.Succ.app ck))).app cn)))

SqrtCond ⬝ n ⬝ k reduces to: return 0 if (k+1)² > n, else 1. Used by RFind to locate the smallest such k, which is √n.

def Cslib.SKI.SqrtPoly : SKI.Polynomial 1

Sqrt n = smallest k such that (k+1)² > n, i.e., the integer square root. Defined as λ n. RFind (SqrtCond n).

Equations

• Cslib.SKI.SqrtPoly = (Cslib.SKI.Polynomial.term Cslib.SKI.RFind).app ((Cslib.SKI.Polynomial.term Cslib.SKI.SqrtCond).app (Cslib.SKI.Polynomial.var 0))

def Cslib.SKI.Sqrt : SKI

SKI term for integer square root

Equations

• Cslib.SKI.Sqrt = Cslib.SKI.SqrtPoly.toSKI

theorem Cslib.SKI.sqrt_def (cn : SKI) : Relation.ReflTransGen Red (Sqrt.app cn) (RFind.app (SqrtCond.app cn))

Sqrt ⬝ n reduces to an RFind search for the smallest k with (k+1)² > n.

theorem Cslib.SKI.sqrt_correct (n : ℕ) (cn : SKI) (hcn : IsChurch n cn) : IsChurch n.sqrt (Sqrt.app cn)

Sqrt correctly computes Nat.sqrt.

Nat pairing (matching Mathlib's Nat.pair)

def Cslib.SKI.NatPairPoly : SKI.Polynomial 2

NatPair a b = if a < b then bb + a else aa + a + b. With &0 = a, &1 = b. The condition a < b is ¬(b ≤ a).

Equations

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

def Cslib.SKI.NatPair : SKI

SKI term for Nat pairing

Equations

• Cslib.SKI.NatPair = Cslib.SKI.NatPairPoly.toSKI

theorem Cslib.SKI.natPair_def (ca cb : SKI) : Relation.ReflTransGen Red ((NatPair.app ca).app cb) (((SKI.Cond.app ((SKI.Add.app ((SKI.Mul.app cb).app cb)).app ca)).app ((SKI.Add.app ((SKI.Add.app ((SKI.Mul.app ca).app ca)).app ca)).app cb)).app (SKI.Neg.app ((SKI.LE.app cb).app ca)))

NatPair ⬝ a ⬝ b reduces to: if a < b then b² + a, else a² + a + b.

theorem Cslib.SKI.natPair_correct (a b : ℕ) (ca cb : SKI) (ha : IsChurch a ca) (hb : IsChurch b cb) : IsChurch (Nat.pair a b) ((NatPair.app ca).app cb)

NatPair correctly computes Nat.pair.

Nat unpairing (matching Mathlib's Nat.unpair)

def Cslib.SKI.NatUnpairLeftPoly : SKI.Polynomial 1

NatUnpairLeft n = if n - s² < s then n - s² else s where s = Nat.sqrt n.

Equations

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

def Cslib.SKI.NatUnpairLeft : SKI

SKI term for left projection of Nat.unpair

Equations

• Cslib.SKI.NatUnpairLeft = Cslib.SKI.NatUnpairLeftPoly.toSKI

theorem Cslib.SKI.natUnpairLeft_def (cn : SKI) : Relation.ReflTransGen Red (NatUnpairLeft.app cn) (((SKI.Cond.app ((SKI.Sub.app cn).app ((SKI.Mul.app (Sqrt.app cn)).app (Sqrt.app cn)))).app (Sqrt.app cn)).app (SKI.Neg.app ((SKI.LE.app (Sqrt.app cn)).app ((SKI.Sub.app cn).app ((SKI.Mul.app (Sqrt.app cn)).app (Sqrt.app cn))))))

NatUnpairLeft ⬝ n reduces to: let s = √n and d = n - s²; return d if d < s, else s.

theorem Cslib.SKI.natUnpairLeft_correct (n : ℕ) (cn : SKI) (hcn : IsChurch n cn) : IsChurch (Nat.unpair n).1 (NatUnpairLeft.app cn)

NatUnpairLeft correctly computes the first component of Nat.unpair.

def Cslib.SKI.NatUnpairRightPoly : SKI.Polynomial 1

NatUnpairRight n = let s = sqrt n in if n - s² < s then s else n - s² - s.

Equations

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

def Cslib.SKI.NatUnpairRight : SKI

SKI term for right projection of Nat.unpair

Equations

• Cslib.SKI.NatUnpairRight = Cslib.SKI.NatUnpairRightPoly.toSKI

theorem Cslib.SKI.natUnpairRight_def (cn : SKI) : Relation.ReflTransGen Red (NatUnpairRight.app cn) (((SKI.Cond.app (Sqrt.app cn)).app ((SKI.Sub.app ((SKI.Sub.app cn).app ((SKI.Mul.app (Sqrt.app cn)).app (Sqrt.app cn)))).app (Sqrt.app cn))).app (SKI.Neg.app ((SKI.LE.app (Sqrt.app cn)).app ((SKI.Sub.app cn).app ((SKI.Mul.app (Sqrt.app cn)).app (Sqrt.app cn))))))

NatUnpairRight ⬝ n reduces to: let s = √n and d = n - s²; return s if d < s, else d - s.

theorem Cslib.SKI.natUnpairRight_correct (n : ℕ) (cn : SKI) (hcn : IsChurch n cn) : IsChurch (Nat.unpair n).2 (NatUnpairRight.app cn)

NatUnpairRight correctly computes the second component of Nat.unpair.