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 MJoin Red is symmetric (trivially) and reflexive (since ↠ is), so we in fact show that MJoin 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.
• mJoin_red_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.mRed_of_parallelReduction {a a' : SKI} (h : a.ParallelReduction a') : Relation.ReflTransGen Red a a'

The inclusion ⭢ₚ ⊆ ↠

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

The inclusion ⭢ ⊆ ⭢ₚ

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

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 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.MJoin ParallelReduction)

theorem Cslib.SKI.mJoin_red_equivalence : Equivalence (Relation.MJoin 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.