# Confluence: Confluence of untyped lambda calculus π§

module plfa.part2.Confluence where

## Introduction

In this chapter we prove that beta reduction is *confluent*, a property also known as *Church-Rosser*. That is, if there are reduction sequences from any term `L`

to two different terms `Mβ`

and `Mβ`

, then there exist reduction sequences from those two terms to some common term `N`

. In pictures:

```
L
/ \
/ \
/ \
Mβ Mβ
\ /
\ /
\ /
N
```

where downward lines are instances of `ββ `

.

Confluence is studied in many other kinds of rewrite systems besides the lambda calculus, and it is well known how to prove confluence in rewrite systems that enjoy the *diamond property*, a single-step version of confluence. Let `β`

be a relation. Then `β`

has the diamond property if whenever `L β Mβ`

and `L β Mβ`

, then there exists an `N`

such that `Mβ β N`

and `Mβ β N`

. This is just an instance of the same picture above, where downward lines are now instance of `β`

. If we write `β*`

for the reflexive and transitive closure of `β`

, then confluence of `β*`

follows immediately from the diamond property.

Unfortunately, reduction in the lambda calculus does not satisfy the diamond property. Here is a counter example.

```
(Ξ» x. x x)((Ξ» x. x) a) ββ (Ξ» x. x x) a
(Ξ» x. x x)((Ξ» x. x) a) ββ ((Ξ» x. x) a) ((Ξ» x. x) a)
```

Both terms can reduce to `a a`

, but the second term requires two steps to get there, not one.

To side-step this problem, weβll define an auxilliary reduction relation, called *parallel reduction*, that can perform many reductions simultaneously and thereby satisfy the diamond property. Furthermore, we show that a parallel reduction sequence exists between any two terms if and only if a beta reduction sequence exists between them. Thus, we can reduce the proof of confluence for beta reduction to confluence for parallel reduction.

## Imports

open import Relation.Binary.PropositionalEquality using (_β‘_; refl) open import Function using (_β_) open import Data.Product using (_Γ_; Ξ£; Ξ£-syntax; β; β-syntax; projβ; projβ) renaming (_,_ to β¨_,_β©) open import plfa.part2.Substitution using (Rename; Subst) open import plfa.part2.Untyped using (_ββ_; Ξ²; ΞΎβ; ΞΎβ; ΞΆ; _ββ _; begin_; _βββ¨_β©_; _ββ β¨_β©_; _β; abs-cong; appL-cong; appR-cong; ββ -trans; _β’_; _β_; `_; #_; _,_; β ; Ζ_; _Β·_; _[_]; rename; ext; exts; Z; S_; subst; subst-zero)

## Parallel Reduction

The parallel reduction relation is defined as follows.

infix 2 _β_ data _β_ : β {Ξ A} β (Ξ β’ A) β (Ξ β’ A) β Set where pvar : β{Ξ A}{x : Ξ β A} --------- β (` x) β (` x) pabs : β{Ξ}{N Nβ² : Ξ , β β’ β } β N β Nβ² ---------- β Ζ N β Ζ Nβ² papp : β{Ξ}{L Lβ² M Mβ² : Ξ β’ β } β L β Lβ² β M β Mβ² ----------------- β L Β· M β Lβ² Β· Mβ² pbeta : β{Ξ}{N Nβ² : Ξ , β β’ β }{M Mβ² : Ξ β’ β } β N β Nβ² β M β Mβ² ----------------------- β (Ζ N) Β· M β Nβ² [ Mβ² ]

The first three rules are congruences that reduce each of their parts simultaneously. The last rule reduces a lambda term and term in parallel followed by a beta step.

We remark that the `pabs`

, `papp`

, and `pbeta`

rules perform reduction on all their subexpressions simultaneously. Also, the `pabs`

rule is akin to the `ΞΆ`

rule and `pbeta`

is akin to `Ξ²`

.

Parallel reduction is reflexive.

par-refl : β{Ξ A}{M : Ξ β’ A} β M β M par-refl {Ξ} {A} {` x} = pvar par-refl {Ξ} {β } {Ζ N} = pabs par-refl par-refl {Ξ} {β } {L Β· M} = papp par-refl par-refl

We define the sequences of parallel reduction as follows.

infix 2 _β*_ infixr 2 _ββ¨_β©_ infix 3 _β data _β*_ : β {Ξ A} β (Ξ β’ A) β (Ξ β’ A) β Set where _β : β {Ξ A} (M : Ξ β’ A) -------- β M β* M _ββ¨_β©_ : β {Ξ A} (L : Ξ β’ A) {M N : Ξ β’ A} β L β M β M β* N --------- β L β* N

#### Exercise `par-diamond-eg`

(practice)

Revisit the counter example to the diamond property for reduction by showing that the diamond property holds for parallel reduction in that case.

-- Your code goes here

## Equivalence between parallel reduction and reduction

Here we prove that for any `M`

and `N`

, `M β* N`

if and only if `M ββ N`

. The only-if direction is particularly easy. We start by showing that if `M ββ N`

, then `M β N`

. The proof is by induction on the reduction `M ββ N`

.

beta-par : β{Ξ A}{M N : Ξ β’ A} β M ββ N ------ β M β N beta-par {Ξ} {β } {L Β· M} (ΞΎβ r) = papp (beta-par {M = L} r) par-refl beta-par {Ξ} {β } {L Β· M} (ΞΎβ r) = papp par-refl (beta-par {M = M} r) beta-par {Ξ} {β } {(Ζ N) Β· M} Ξ² = pbeta par-refl par-refl beta-par {Ξ} {β } {Ζ N} (ΞΆ r) = pabs (beta-par r)

With this lemma in hand we complete the only-if direction, that `M ββ N`

implies `M β* N`

. The proof is a straightforward induction on the reduction sequence `M ββ N`

.

betas-pars : β{Ξ A} {M N : Ξ β’ A} β M ββ N ------ β M β* N betas-pars {Ξ} {A} {Mβ} {.Mβ} (Mβ β) = Mβ β betas-pars {Ξ} {A} {.L} {N} (L βββ¨ b β© bs) = L ββ¨ beta-par b β© betas-pars bs

Now for the other direction, that `M β* N`

implies `M ββ N`

. The proof of this direction is a bit different because itβs not the case that `M β N`

implies `M ββ N`

. After all, `M β N`

performs many reductions. So instead we shall prove that `M β N`

implies `M ββ N`

.

par-betas : β{Ξ A}{M N : Ξ β’ A} β M β N ------ β M ββ N par-betas {Ξ} {A} {.(` _)} (pvar{x = x}) = (` x) β par-betas {Ξ} {β } {Ζ N} (pabs p) = abs-cong (par-betas p) par-betas {Ξ} {β } {L Β· M} (papp {L = L}{Lβ²}{M}{Mβ²} pβ pβ) = begin L Β· M ββ β¨ appL-cong{M = M} (par-betas pβ) β© Lβ² Β· M ββ β¨ appR-cong (par-betas pβ) β© Lβ² Β· Mβ² β par-betas {Ξ} {β } {(Ζ N) Β· M} (pbeta{Nβ² = Nβ²}{Mβ² = Mβ²} pβ pβ) = begin (Ζ N) Β· M ββ β¨ appL-cong{M = M} (abs-cong (par-betas pβ)) β© (Ζ Nβ²) Β· M ββ β¨ appR-cong{L = Ζ Nβ²} (par-betas pβ) β© (Ζ Nβ²) Β· Mβ² βββ¨ Ξ² β© Nβ² [ Mβ² ] β

The proof is by induction on `M β N`

.

Suppose

`x β x`

. We immediately have`x ββ x`

.Suppose

`Ζ N β Ζ Nβ²`

because`N β Nβ²`

. By the induction hypothesis we have`N ββ Nβ²`

. We conclude that`Ζ N ββ Ζ Nβ²`

because`ββ`

is a congruence.Suppose

`L Β· M β Lβ² Β· Mβ²`

because`L β Lβ²`

and`M β Mβ²`

. By the induction hypothesis, we have`L ββ Lβ²`

and`M ββ Mβ²`

. So`L Β· M ββ Lβ² Β· M`

and then`Lβ² Β· M ββ Lβ² Β· Mβ²`

because`ββ`

is a congruence.Suppose

`(Ζ N) Β· M β Nβ² [ Mβ² ]`

because`N β Nβ²`

and`M β Mβ²`

. By similar reasoning, we have`(Ζ N) Β· M ββ (Ζ Nβ²) Β· Mβ²`

which we can following with the Ξ² reduction`(Ζ Nβ²) Β· Mβ² ββ Nβ² [ Mβ² ]`

.

With this lemma in hand, we complete the proof that `M β* N`

implies `M ββ N`

with a simple induction on `M β* N`

.

pars-betas : β{Ξ A} {M N : Ξ β’ A} β M β* N ------ β M ββ N pars-betas (Mβ β) = Mβ β pars-betas (L ββ¨ p β© ps) = ββ -trans (par-betas p) (pars-betas ps)

## Substitution lemma for parallel reduction

Our next goal is the prove the diamond property for parallel reduction. But to do that, we need to prove that substitution respects parallel reduction. That is, if `N β Nβ²`

and `M β Mβ²`

, then `N [ M ] β Nβ² [ Mβ² ]`

. We cannot prove this directly by induction, so we generalize it to: if `N β Nβ²`

and the substitution `Ο`

pointwise parallel reduces to `Ο`

, then `subst Ο N β subst Ο Nβ²`

. We define the notion of pointwise parallel reduction as follows.

par-subst : β{Ξ Ξ} β Subst Ξ Ξ β Subst Ξ Ξ β Set par-subst {Ξ}{Ξ} Ο Οβ² = β{A}{x : Ξ β A} β Ο x β Οβ² x

Because substitution depends on the extension function `exts`

, which in turn relies on `rename`

, we start with a version of the substitution lemma, called `par-rename`

, that is specialized to renamings. The proof of `par-rename`

relies on the fact that renaming and substitution commute with one another, which is a lemma that we import from Chapter Substitution and restate here.

rename-subst-commute : β{Ξ Ξ}{N : Ξ , β β’ β }{M : Ξ β’ β }{Ο : Rename Ξ Ξ } β (rename (ext Ο) N) [ rename Ο M ] β‘ rename Ο (N [ M ]) rename-subst-commute {N = N} = plfa.part2.Substitution.rename-subst-commute {N = N}

Now for the `par-rename`

lemma.

par-rename : β{Ξ Ξ A} {Ο : Rename Ξ Ξ} {M Mβ² : Ξ β’ A} β M β Mβ² ------------------------ β rename Ο M β rename Ο Mβ² par-rename pvar = pvar par-rename (pabs p) = pabs (par-rename p) par-rename (papp pβ pβ) = papp (par-rename pβ) (par-rename pβ) par-rename {Ξ}{Ξ}{A}{Ο} (pbeta{Ξ}{N}{Nβ²}{M}{Mβ²} pβ pβ) with pbeta (par-rename{Ο = ext Ο} pβ) (par-rename{Ο = Ο} pβ) ... | G rewrite rename-subst-commute{Ξ}{Ξ}{Nβ²}{Mβ²}{Ο} = G

The proof is by induction on `M β Mβ²`

. The first four cases are straightforward so we just consider the last one for `pbeta`

.

- Suppose
`(Ζ N) Β· M β Nβ² [ Mβ² ]`

because`N β Nβ²`

and`M β Mβ²`

. By the induction hypothesis, we have`rename (ext Ο) N β rename (ext Ο) Nβ²`

and`rename Ο M β rename Ο Mβ²`

. So by`pbeta`

we have`(Ζ rename (ext Ο) N) Β· (rename Ο M) β (rename (ext Ο) N) [ rename Ο M ]`

. However, to conclude we instead need parallel reduction to`rename Ο (N [ M ])`

. But thankfully, renaming and substitution commute with one another.

With the `par-rename`

lemma in hand, it is straightforward to show that extending substitutions preserves the pointwise parallel reduction relation.

par-subst-exts : β{Ξ Ξ} {Ο Ο : Subst Ξ Ξ} β par-subst Ο Ο ------------------------------------------ β β{B} β par-subst (exts Ο {B = B}) (exts Ο) par-subst-exts s {x = Z} = pvar par-subst-exts s {x = S x} = par-rename s

The next lemma that we need for proving that substitution respects parallel reduction is the following which states that simultaneoous substitution commutes with single substitution. We import this lemma from Chapter Substitution and restate it below.

subst-commute : β{Ξ Ξ}{N : Ξ , β β’ β }{M : Ξ β’ β }{Ο : Subst Ξ Ξ } β subst (exts Ο) N [ subst Ο M ] β‘ subst Ο (N [ M ]) subst-commute {N = N} = plfa.part2.Substitution.subst-commute {N = N}

We are ready to prove that substitution respects parallel reduction.

subst-par : β{Ξ Ξ A} {Ο Ο : Subst Ξ Ξ} {M Mβ² : Ξ β’ A} β par-subst Ο Ο β M β Mβ² -------------------------- β subst Ο M β subst Ο Mβ² subst-par {Ξ} {Ξ} {A} {Ο} {Ο} {` x} s pvar = s subst-par {Ξ} {Ξ} {A} {Ο} {Ο} {Ζ N} s (pabs p) = pabs (subst-par {Ο = exts Ο} {Ο = exts Ο} (Ξ» {A}{x} β par-subst-exts s {x = x}) p) subst-par {Ξ} {Ξ} {β } {Ο} {Ο} {L Β· M} s (papp pβ pβ) = papp (subst-par s pβ) (subst-par s pβ) subst-par {Ξ} {Ξ} {β } {Ο} {Ο} {(Ζ N) Β· M} s (pbeta{Nβ² = Nβ²}{Mβ² = Mβ²} pβ pβ) with pbeta (subst-par{Ο = exts Ο}{Ο = exts Ο}{M = N} (Ξ»{A}{x} β par-subst-exts s {x = x}) pβ) (subst-par {Ο = Ο} s pβ) ... | G rewrite subst-commute{N = Nβ²}{M = Mβ²}{Ο = Ο} = G

We proceed by induction on `M β Mβ²`

.

Suppose

`x β x`

. We conclude that`Ο x β Ο x`

using the premise`par-subst Ο Ο`

.Suppose

`Ζ N β Ζ Nβ²`

because`N β Nβ²`

. To use the induction hypothesis, we need`par-subst (exts Ο) (exts Ο)`

, which we obtain by`par-subst-exts`

. So we have`subst (exts Ο) N β subst (exts Ο) Nβ²`

and conclude by rule`pabs`

.Suppose

`L Β· M β Lβ² Β· Mβ²`

because`L β Lβ²`

and`M β Mβ²`

. By the induction hypothesis we have`subst Ο L β subst Ο Lβ²`

and`subst Ο M β subst Ο Mβ²`

, so we conclude by rule`papp`

.Suppose

`(Ζ N) Β· M β Nβ² [ Mβ² ]`

because`N β Nβ²`

and`M β Mβ²`

. Again we obtain`par-subst (exts Ο) (exts Ο)`

by`par-subst-exts`

. So by the induction hypothesis, we have`subst (exts Ο) N β subst (exts Ο) Nβ²`

and`subst Ο M β subst Ο Mβ²`

. Then by rule`pbeta`

, we have parallel reduction to`subst (exts Ο) Nβ² [ subst Ο Mβ² ]`

. Substitution commutes with itself in the following sense. For any Ο, N, and M, we have`(subst (exts Ο) N) [ subst Ο M ] β‘ subst Ο (N [ M ])`

So we have parallel reduction to

`subst Ο (Nβ² [ Mβ² ])`

.

Of course, if `M β Mβ²`

, then `subst-zero M`

pointwise parallel reduces to `subst-zero Mβ²`

.

par-subst-zero : β{Ξ}{A}{M Mβ² : Ξ β’ A} β M β Mβ² β par-subst (subst-zero M) (subst-zero Mβ²) par-subst-zero {M} {Mβ²} p {A} {Z} = p par-subst-zero {M} {Mβ²} p {A} {S x} = pvar

We conclude this section with the desired corollary, that substitution respects parallel reduction.

sub-par : β{Ξ A B} {N Nβ² : Ξ , A β’ B} {M Mβ² : Ξ β’ A} β N β Nβ² β M β Mβ² -------------------------- β N [ M ] β Nβ² [ Mβ² ] sub-par pn pm = subst-par (par-subst-zero pm) pn

## Parallel reduction satisfies the diamond property

The heart of the confluence proof is made of stone, or rather, of diamond! We show that parallel reduction satisfies the diamond property: that if `M β N`

and `M β Nβ²`

, then `N β L`

and `Nβ² β L`

for some `L`

. The proof is relatively easy; it is parallel reductionβs *raison dβetre*.

par-diamond : β{Ξ A} {M N Nβ² : Ξ β’ A} β M β N β M β Nβ² --------------------------------- β Ξ£[ L β Ξ β’ A ] (N β L) Γ (Nβ² β L) par-diamond (pvar{x = x}) pvar = β¨ ` x , β¨ pvar , pvar β© β© par-diamond (pabs p1) (pabs p2) with par-diamond p1 p2 ... | β¨ Lβ² , β¨ p3 , p4 β© β© = β¨ Ζ Lβ² , β¨ pabs p3 , pabs p4 β© β© par-diamond{Ξ}{A}{L Β· M}{N}{Nβ²} (papp{Ξ}{L}{Lβ}{M}{Mβ} p1 p3) (papp{Ξ}{L}{Lβ}{M}{Mβ} p2 p4) with par-diamond p1 p2 ... | β¨ Lβ , β¨ p5 , p6 β© β© with par-diamond p3 p4 ... | β¨ Mβ , β¨ p7 , p8 β© β© = β¨ (Lβ Β· Mβ) , β¨ (papp p5 p7) , (papp p6 p8) β© β© par-diamond (papp (pabs p1) p3) (pbeta p2 p4) with par-diamond p1 p2 ... | β¨ Nβ , β¨ p5 , p6 β© β© with par-diamond p3 p4 ... | β¨ Mβ , β¨ p7 , p8 β© β© = β¨ Nβ [ Mβ ] , β¨ pbeta p5 p7 , sub-par p6 p8 β© β© par-diamond (pbeta p1 p3) (papp (pabs p2) p4) with par-diamond p1 p2 ... | β¨ Nβ , β¨ p5 , p6 β© β© with par-diamond p3 p4 ... | β¨ Mβ , β¨ p7 , p8 β© β© = β¨ (Nβ [ Mβ ]) , β¨ sub-par p5 p7 , pbeta p6 p8 β© β© par-diamond {Ξ}{A} (pbeta p1 p3) (pbeta p2 p4) with par-diamond p1 p2 ... | β¨ Nβ , β¨ p5 , p6 β© β© with par-diamond p3 p4 ... | β¨ Mβ , β¨ p7 , p8 β© β© = β¨ Nβ [ Mβ ] , β¨ sub-par p5 p7 , sub-par p6 p8 β© β©

The proof is by induction on both premises.

Suppose

`x β x`

and`x β x`

. We choose`L = x`

and immediately have`x β x`

and`x β x`

.Suppose

`Ζ N β Ζ Nβ`

and`Ζ N β Ζ Nβ`

. By the induction hypothesis, there exists`Lβ²`

such that`Nβ β Lβ²`

and`Nβ β Lβ²`

. We choose`L = Ζ Lβ²`

and by`pabs`

conclude that`Ζ Nβ β Ζ Lβ²`

and `Ζ Nβ β Ζ Lβ².Suppose that

`L Β· M β Lβ Β· Mβ`

and`L Β· M β Lβ Β· Mβ`

. By the induction hypothesis we have`Lβ β Lβ`

and`Lβ β Lβ`

for some`Lβ`

. Likewise, we have`Mβ β Mβ`

and`Mβ β Mβ`

for some`Mβ`

. We choose`L = Lβ Β· Mβ`

and conclude with two uses of`papp`

.Suppose that

`(Ζ N) Β· M β (Ζ Nβ) Β· Mβ`

and`(Ζ N) Β· M β Nβ [ Mβ ]`

By the induction hypothesis we have`Nβ β Nβ`

and`Nβ β Nβ`

for some`Nβ`

. Likewise, we have`Mβ β Mβ`

and`Mβ β Mβ`

for some`Mβ`

. We choose`L = Nβ [ Mβ ]`

. We have`(Ζ Nβ) Β· Mβ β Nβ [ Mβ ]`

by rule`pbeta`

and conclude that`Nβ [ Mβ ] β Nβ [ Mβ ]`

because substitution respects parallel reduction.Suppose that

`(Ζ N) Β· M β Nβ [ Mβ ]`

and`(Ζ N) Β· M β (Ζ Nβ) Β· Mβ`

. The proof of this case is the mirror image of the last one.Suppose that

`(Ζ N) Β· M β Nβ [ Mβ ]`

and`(Ζ N) Β· M β Nβ [ Mβ ]`

. By the induction hypothesis we have`Nβ β Nβ`

and`Nβ β Nβ`

for some`Nβ`

. Likewise, we have`Mβ β Mβ`

and`Mβ β Mβ`

for some`Mβ`

. We choose`L = Nβ [ Mβ ]`

. We have both`(Ζ Nβ) Β· Mβ β Nβ [ Mβ ]`

and`(Ζ Nβ) Β· Mβ β Nβ [ Mβ ]`

by rule`pbeta`

#### Exercise (practice)

Draw pictures that represent the proofs of each of the six cases in the above proof of `par-diamond`

. The pictures should consist of nodes and directed edges, where each node is labeled with a term and each edge represents parallel reduction.

## Proof of confluence for parallel reduction

As promised at the beginning, the proof that parallel reduction is confluent is easy now that we know it satisfies the diamond property. We just need to prove the strip lemma, which states that if `M β N`

and `M β* Nβ²`

, then `N β* L`

and `Nβ² β L`

for some `L`

. The following diagram illustrates the strip lemma

```
M
/ \
1 *
/ \
N Nβ²
\ /
* 1
\ /
L
```

where downward lines are instances of `β`

or `β*`

, depending on how they are marked.

The proof of the strip lemma is a straightforward induction on `M β* Nβ²`

, using the diamond property in the induction step.

strip : β{Ξ A} {M N Nβ² : Ξ β’ A} β M β N β M β* Nβ² ------------------------------------ β Ξ£[ L β Ξ β’ A ] (N β* L) Γ (Nβ² β L) strip{Ξ}{A}{M}{N}{Nβ²} mn (M β) = β¨ N , β¨ N β , mn β© β© strip{Ξ}{A}{M}{N}{Nβ²} mn (M ββ¨ mm' β© m'n') with par-diamond mn mm' ... | β¨ L , β¨ nl , m'l β© β© with strip m'l m'n' ... | β¨ Lβ² , β¨ ll' , n'l' β© β© = β¨ Lβ² , β¨ (N ββ¨ nl β© ll') , n'l' β© β©

The proof of confluence for parallel reduction is now proved by induction on the sequence `M β* N`

, using the above lemma in the induction step.

par-confluence : β{Ξ A} {L Mβ Mβ : Ξ β’ A} β L β* Mβ β L β* Mβ ------------------------------------ β Ξ£[ N β Ξ β’ A ] (Mβ β* N) Γ (Mβ β* N) par-confluence {Ξ}{A}{L}{.L}{N} (L β) Lβ*N = β¨ N , β¨ Lβ*N , N β β© β© par-confluence {Ξ}{A}{L}{Mββ²}{Mβ} (L ββ¨ LβMβ β© Mββ*Mββ²) Lβ*Mβ with strip LβMβ Lβ*Mβ ... | β¨ N , β¨ Mββ*N , MββN β© β© with par-confluence Mββ*Mββ² Mββ*N ... | β¨ Nβ² , β¨ Mββ²β*Nβ² , Nβ*Nβ² β© β© = β¨ Nβ² , β¨ Mββ²β*Nβ² , (Mβ ββ¨ MββN β© Nβ*Nβ²) β© β©

The step case may be illustrated as follows:

```
L
/ \
1 *
/ \
Mβ (a) Mβ
/ \ /
* * 1
/ \ /
Mββ²(b) N
\ /
* *
\ /
Nβ²
```

where downward lines are instances of `β`

or `β*`

, depending on how they are marked. Here `(a)`

holds by `strip`

and `(b)`

holds by induction.

## Proof of confluence for reduction

Confluence of reduction is a corollary of confluence for parallel reduction. From `L ββ Mβ`

and `L ββ Mβ`

we have `L β* Mβ`

and `L β* Mβ`

by `betas-pars`

. Then by confluence we obtain some `L`

such that `Mβ β* N`

and `Mβ β* N`

, from which we conclude that `Mβ ββ N`

and `Mβ ββ N`

by `pars-betas`

.

confluence : β{Ξ A} {L Mβ Mβ : Ξ β’ A} β L ββ Mβ β L ββ Mβ ----------------------------------- β Ξ£[ N β Ξ β’ A ] (Mβ ββ N) Γ (Mβ ββ N) confluence Lβ Mβ Lβ Mβ with par-confluence (betas-pars Lβ Mβ) (betas-pars Lβ Mβ) ... | β¨ N , β¨ MββN , MββN β© β© = β¨ N , β¨ pars-betas MββN , pars-betas MββN β© β©

## Notes

Broadly speaking, this proof of confluence, based on parallel reduction, is due to W. Tait and P. Martin-Lof (see Barendredgt 1984, Section 3.2). Details of the mechanization come from several sources. The `subst-par`

lemma is the βstrong substitutivityβ lemma of Shafer, Tebbi, and Smolka (ITP 2015). The proofs of `par-diamond`

, `strip`

, and `par-confluence`

are based on Pfenningβs 1992 technical report about the Church-Rosser theorem. In addition, we consulted Nipkow and Berghoferβs mechanization in Isabelle, which is based on an earlier article by Nipkow (JAR 1996). We opted not to use the βcomplete developmentsβ approach of Takahashi (1995) because we felt that the proof was simple enough based solely on parallel reduction. There are many more mechanizations of the Church-Rosser theorem that we have not yet had the time to read, including Shankarβs (J. ACM 1988) and Homeierβs (TPHOLs 2001).

## Unicode

This chapter uses the following unicode:

```
β U+3015 RIGHTWARDS TRIPLE ARROW (\r== or \Rrightarrow)
```