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 SKI.Church (n : ℕ) (f x : SKI) : SKI

Function form of the church numerals.

Equations

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

theorem SKI.church_red (n : ℕ) (f f' x x' : SKI) (hf : f.MRed f') (hx : x.MRed x') : (Church n f x).MRed (Church n f' x')

church commutes with reduction.

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

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

Equations

• SKI.IsChurch n a = ∀ (f x : SKI), ((a.app f).app x).MRed (SKI.Church n f x)

theorem SKI.isChurch_trans (n : ℕ) {a a' : SKI} (h : a.MRed 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 SKI.Zero : SKI

Church zero := λ f x. x

Equations

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

theorem SKI.zero_correct : IsChurch 0 SKI.Zero

def SKI.One : SKI

Church one := λ f x. f x

Equations

• SKI.One = SKI.I

theorem SKI.one_correct : IsChurch 1 SKI.One

def 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

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

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

def 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 SKI.PredAux : SKI

A term representing PredAux

Equations

• SKI.PredAux = SKI.PredAuxPoly.toSKI

theorem SKI.predAux_def (p : SKI) : (PredAux.app p).MRed ((MkPair.app (Snd.app p)).app (SKI.Succ.app (Snd.app p)))

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

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

Equations

• SKI.IsChurchPair ns x = (SKI.IsChurch ns.fst (SKI.Fst.app x) ∧ SKI.IsChurch ns.snd (SKI.Snd.app x))

theorem SKI.isChurchPair_trans (ns : ℕ × ℕ) (a a' : SKI) (h : a.MRed a') : IsChurchPair ns a' → IsChurchPair ns a

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

theorem 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 SKI.PredPoly : SKI.Polynomial 1

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

Equations

• SKI.PredPoly = (SKI.Polynomial.term SKI.Fst).app (((SKI.Polynomial.var 0).app (SKI.Polynomial.term SKI.PredAux)).app (SKI.Polynomial.term ((SKI.MkPair.app SKI.Zero).app SKI.Zero)))

def SKI.Pred : SKI

A term representing Pred

Equations

• SKI.Pred = SKI.PredPoly.toSKI

theorem SKI.pred_def (a : SKI) : (Pred.app a).MRed (Fst.app ((a.app PredAux).app ((MkPair.app SKI.Zero).app SKI.Zero)))

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

Primitive recursion

def SKI.IsZeroPoly : SKI.Polynomial 1

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

Equations

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

def SKI.IsZero : SKI

A term representing IsZero

Equations

• SKI.IsZero = SKI.IsZeroPoly.toSKI

theorem SKI.isZero_def (a : SKI) : (IsZero.app a).MRed ((a.app (K.app FF)).app TT)

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

def 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 SKI.RecAux : SKI

A term representing RecAux

Equations

• SKI.RecAux = SKI.RecAuxPoly.toSKI

theorem SKI.recAux_def (R₀ x g a : SKI) : ((((RecAux.app R₀).app x).app g).app a).MRed (((SKI.Cond.app x).app ((g.app a).app (((R₀.app x).app g).app (Pred.app a)))).app (IsZero.app a))

def 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

• SKI.Rec = SKI.RecAux.fixedPoint

theorem SKI.rec_def (x g a : SKI) : (((Rec.app x).app g).app a).MRed (((SKI.Cond.app x).app ((g.app a).app (((Rec.app x).app g).app (Pred.app a)))).app (IsZero.app a))

theorem SKI.rec_zero (x g a : SKI) (ha : IsChurch 0 a) : (((Rec.app x).app g).app a).MRed x

theorem SKI.rec_succ (n : ℕ) (x g a : SKI) (ha : IsChurch (n + 1) a) : (((Rec.app x).app g).app a).MRed ((g.app a).app (((Rec.app x).app g).app (Pred.app a)))

Root-finding (μ-recursion)

def 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 SKI.RFindAboveAux : SKI

A term representing RFindAboveAux

Equations

• SKI.RFindAboveAux = SKI.RFindAboveAuxPoly.toSKI

theorem SKI.rfindAboveAux_def (R₀ f a : SKI) : (((RFindAboveAux.app R₀).app a).app f).MRed (((SKI.Cond.app a).app ((R₀.app (SKI.Succ.app a)).app f)).app (IsZero.app (f.app a)))

theorem SKI.rfindAboveAux_base (R₀ f a : SKI) (hfa : IsChurch 0 (f.app a)) : (((RFindAboveAux.app R₀).app a).app f).MRed a

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

def SKI.RFindAbove : SKI

Find the minimal root of fNat above a number n

Equations

• SKI.RFindAbove = SKI.RFindAboveAux.fixedPoint

theorem 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 SKI.RFind : SKI

Ordinary root finding is root finding above zero

Equations

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

theorem 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 SKI.AddPoly : SKI.Polynomial 2

Addition: λ n m. n Succ m

Equations

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

def SKI.Add : SKI

A term representing addition on church numerals

Equations

• SKI.Add = SKI.AddPoly.toSKI

theorem SKI.add_def (a b : SKI) : ((SKI.Add.app a).app b).MRed ((a.app SKI.Succ).app b)

theorem 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 SKI.MulPoly : SKI.Polynomial 2

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

Equations

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

def SKI.Mul : SKI

A term representing multiplication on church numerals

Equations

• SKI.Mul = SKI.MulPoly.toSKI

theorem SKI.mul_def (a b : SKI) : ((SKI.Mul.app a).app b).MRed ((a.app (SKI.Add.app b)).app SKI.Zero)

theorem 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 SKI.SubPoly : SKI.Polynomial 2

Subtraction: λ n m. n Pred m

Equations

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

def SKI.Sub : SKI

A term representing subtraction on church numerals

Equations

• SKI.Sub = SKI.SubPoly.toSKI

theorem SKI.sub_def (a b : SKI) : ((SKI.Sub.app a).app b).MRed ((b.app Pred).app a)

theorem 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 SKI.LEPoly : SKI.Polynomial 2

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

Equations

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

def SKI.LE : SKI

A term representing comparison on church numerals

Equations

• SKI.LE = SKI.LEPoly.toSKI

theorem SKI.le_def (a b : SKI) : ((SKI.LE.app a).app b).MRed (IsZero.app ((SKI.Sub.app a).app b))

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