SKI reduction is confluent

This file proves the Church-Rosser theorem for the SKI calculus, that is, if a ↠ b and a ↠ c, b ↠ d and c ↠ d for some term d. More strongly (though equivalently), we show that the relation of having a common reduct is transitive — in the above situation, a and b, and a and c have common reducts, so the result implies the same of b and c. Note that Join (ReflTransGen Red) is symmetric (trivially) and reflexive (since ↠ is), so we in fact show that Join (ReflTransGen Red) is an equivalence.

Our proof follows the method of Tait and Martin-Löf for the lambda calculus, as presented for instance in Chapter 4 of Peter Selinger's notes: https://www.mscs.dal.ca/~selinger/papers/papers/lambdanotes.pdf.

Main definitions

• ParallelReduction : a relation ⭢ₚ on terms such that ⭢ ⊆ ⭢ₚ ⊆ ↠, allowing simultaneous reduction on the head and tail of a term.

Main results

• parallelReduction_diamond : parallel reduction satisfies the diamond property, that is, it is confluent in a single step.
• join_mRed_equivalence : by a general result, the diamond property for ⭢ₚ implies the same for its reflexive-transitive closure. This closure is exactly ↠, which implies the Church-Rosser theorem as sketched above.

inductive Cslib.SKI.ParallelReduction : SKI → SKI → Prop

A reduction step allowing simultaneous reduction of disjoint redexes

• refl (a : SKI) : a.ParallelReduction a

  Parallel reduction is reflexive,

• red_I (a : SKI) : (I.app a).ParallelReduction a

  Contains Red,

• red_K (a b : SKI) : ((K.app a).app b).ParallelReduction a
• red_S (a b c : SKI) : (((S.app a).app b).app c).ParallelReduction ((a.app c).app (b.app c))
• par ⦃a a' b b' : SKI⦄ : a.ParallelReduction a' → b.ParallelReduction b' → (a.app b).ParallelReduction (a'.app b')

  and allows simultaneous reduction of disjoint redexes.

def Cslib.SKI.«term_⭢ₚ_» : Lean.TrailingParserDescr

Equations

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

def Cslib.SKI.«term_↠ₚ_» : Lean.TrailingParserDescr

Equations

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

theorem Cslib.SKI.ParallelReduction.le_reflTransGen_red : (fun (x1 x2 : SKI) => x1.ParallelReduction x2) ≤ fun (x1 x2 : SKI) => Relation.ReflTransGen Red x1 x2

The inclusion (· ⭢ₚ ·) ≤ (· ↠ ·).

theorem Cslib.SKI.Red.le_parallelReduction : (fun (x1 x2 : SKI) => x1.Red x2) ≤ fun (x1 x2 : SKI) => x1.ParallelReduction x2

The inclusion (· ⭢ ·) ≤ (· ⭢ₚ ·).

theorem Cslib.SKI.reflTransGen_parallelReduction_mRed : Relation.ReflTransGen ParallelReduction = Relation.ReflTransGen Red

The relations ⭢ and ⭢ₚ have the same reflexive-transitive closure.

Irreducibility for the (partially applied) primitive combinators.

TODO: possibly these should be proven more generally (in another file) for ↠.

theorem Cslib.SKI.I_irreducible (a : SKI) (h : I.ParallelReduction a) : a = I

theorem Cslib.SKI.K_irreducible (a : SKI) (h : K.ParallelReduction a) : a = K

theorem Cslib.SKI.Ka_irreducible (a c : SKI) (h : (K.app a).ParallelReduction c) : ∃ (a' : SKI), a.ParallelReduction a' ∧ c = K.app a'

theorem Cslib.SKI.S_irreducible (a : SKI) (h : S.ParallelReduction a) : a = S

theorem Cslib.SKI.Sa_irreducible (a c : SKI) (h : (S.app a).ParallelReduction c) : ∃ (a' : SKI), a.ParallelReduction a' ∧ c = S.app a'

theorem Cslib.SKI.Sab_irreducible (a b c : SKI) (h : ((S.app a).app b).ParallelReduction c) : ∃ (a' : SKI), ∃ (b' : SKI), a.ParallelReduction a' ∧ b.ParallelReduction b' ∧ c = (S.app a').app b'

theorem Cslib.SKI.parallelReduction_diamond : Relation.Diamond ParallelReduction

The key result: the Church-Rosser property holds for ⭢ₚ. The proof is a lengthy case analysis on the reductions a ⭢ₚ a₁ and a ⭢ₚ a₂, but is entirely mechanical.

theorem Cslib.SKI.join_parallelReduction_equivalence : Equivalence (Relation.Join (Relation.ReflTransGen ParallelReduction))

theorem Cslib.SKI.join_mRed_equivalence : Equivalence (Relation.Join (Relation.ReflTransGen Red))

The Church-Rosser theorem in its general form.

theorem Cslib.SKI.MRed.diamond : Relation.Confluent Red

The Church-Rosser theorem in the form it is usually stated.