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 CommonReduct is symmetric (trivially) and reflexive (since ⇒* is), so we in fact show that CommonReduct 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.
• commonReduct_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 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 SKI.«term_⇒ₚ_» : Lean.TrailingParserDescr

Notation for parallel reduction

Equations

• SKI.«term_⇒ₚ_» = Lean.ParserDescr.trailingNode `SKI.«term_⇒ₚ_» 90 91 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇒ₚ ") (Lean.ParserDescr.cat `term 91))

theorem SKI.mRed_of_parallelReduction {a a' : SKI} (h : a.ParallelReduction a') : a.MRed a'

The inclusion ⇒ₚ ⊆ ⇒*

theorem SKI.parallelReduction_of_red {a a' : SKI} (h : a.Red a') : a.ParallelReduction a'

The inclusion ⇒ ⊆ ⇒ₚ

theorem SKI.reflTransGen_parallelReduction_mRed : Relation.ReflTransGen ParallelReduction = MRed

The inclusions of mRed_of_parallelReduction and parallelReduction_of_red imply that ⇒ 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 SKI.I_irreducible (a : SKI) (h : I.ParallelReduction a) : a = I

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

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

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

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

theorem 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 SKI.parallelReduction_diamond (a a₁ a₂ : SKI) (h₁ : a.ParallelReduction a₁) (h₂ : a.ParallelReduction a₂) : Relation.Join ParallelReduction a₁ a₂

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 SKI.join_parallelReduction_equivalence : Equivalence (Relation.Join (Relation.ReflTransGen ParallelReduction))

theorem SKI.commonReduct_equivalence : Equivalence CommonReduct

The Church-Rosser theorem in its general form.

theorem SKI.MRed.diamond (a b c : SKI) (hab : a.MRed b) (hac : a.MRed c) : b.CommonReduct c

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