The Church–Rosser Property

Definition of the Church Rosser property

[Church--Rosser property, CR] A relation $\xredone$source on terms is said to satisfy the Church--Rosser property iff, whenever $M \xredone P$source and $M \xredone Q$source, then there exists some $N$source such that $P \xredone N$source and $Q \xredone N$source.

Church Rosser property passes to transitive closure

If a relation $\xredone$source satisfies the Church--Rosser property, and $\xred$source is the smallest transitive relation containing $\xredone$source, then $\xred$source satisfies the Church--Rosser property too.

Proof

Suppose

We will prove the theorem by constructing a grid $N$source of terms of height is $m + 1$source and width $n + 1$source. We use $N_{i,j}$source to denote the term in the $i$source-th row and $j$source-th column.

We construct $N$source in such a way that $N_{i,j} \xredone N_{i+1,j}$source and $N_{i,j} \xredone N_{i,j+1}$source. It is defined as follows:

where $R$source is a term such that $N_{i-1,j} \xredone R$source and $N_{i,j-1} \xredone R$source. By the Church--Rosser property of $\xredone$source, such a term always exists.

Now we have $N_{m,0} \xredone \dots \xredone N_{m,n}$source and $N_{0,n} \xredone \dots \xredone N_{m,n}$source. Note $N_{m,0}$source is $P$source and $N_{0,n}$source is $Q$source. By definition of $\xred$source the theorem follows.

Four source rules for parallel beta reduction

[parallel $\beta$source-reduction, $\bredpar$source] Parallel reduction ($\bredpar$source) of terms is inductively defined as follows:

1. $x \bredpar x$source.

2. If $N \xrightarrow{\beta} N'$source then $\lambd[x][N] \bredpar \lambd[x][N']$source.

3. If $P \bredpar P'$source and $Q \bredpar Q'$source then $PQ \bredpar P'Q'$source.

4. If $N \bredpar N'$source and $Q \bredpar Q'$source then $(\lambd[x][N])Q \bredpar \Subst{N'}{Q'}{x}$source.

Reflexivity of parallel beta reduction

$M \bredpar M$source.

Proof

Exercise.

Exercise proving parallel beta reflexivity

Prove the theorem on reflexivity of parallel beta reduction.

Definition of beta complete development

[$\beta$source-complete development] The $\beta$source-complete development $\bcd{M}$source of $M$source is defined inductively as follows:

Editorial

This definition has the problem that we haven't introduced how to define functions on ($\lambd$source-)terms recursively. Will fix in future.

Parallel beta reduction and substitution

If $M \bredpar M'$source and $R \bredpar R'$source, then $\Subst{M}{R}{y} \bredpar \Subst{M'}{R'}{y}$source.

Proof

By induction on the derivation of $M \bredpar M'$source.

1. The last step is the variable rule for parallel beta reduction: Exercise.

2. The last step is the abstraction rule for parallel beta reduction: Then $M$source is $\lambd[x][N]$source and $M'$source is $\lambd[x][N']$source, where $N \bredpar N'$source. We want to prove that $\Subst{(\lambd[x][N])}{R}{y} \bredpar \Subst{(\lambd[x][N'])}{R'}{y}$source, i.e., $\lambd[x][\Subst{N}{R}{y}] \bredpar \lambd[x][\Subst{N'}{R}{y}]$source. This follows immediately by the abstraction rule for parallel beta reduction and the induction hypothesis.

3. The last step is the application rule for parallel beta reduction: Exercise.

4. The last step is the contraction rule for parallel beta reduction: $M$source is $(\lambd[x][N])Q$source and $M'$source is $\Subst{N'}{Q'}{x}$source. We want to prove that $\Subst{((\lambd[x][N])Q)}{R}{y} \bredpar \Subst{\Subst{N'}{Q'}{x}}{R'}{y}$source, i.e., $(\lambd[x][\Subst{N}{R}{y}])\Subst{Q}{R}{y} \bredpar \Subst{\Subst{N'}{R'}{y}}{\Subst{Q'}{R'}{y}}{x}$source. This follows by the contraction rule for parallel beta reduction and the induction hypothesis.

Exercise completing the parallel beta substitution proof

Complete the proof of the substitution compatibility lemma for parallel beta reduction.

Every parallel beta reduct reaches the complete development

If $M \bredpar M'$source then $M' \bredpar \bcd{M}$source.

Proof

By induction on the derivation of $M \bredpar M'$source.

1. The last rule is the variable rule for parallel beta reduction: Exercise.

2. The last rule is the abstraction rule for parallel beta reduction: $M$source is $\lambd[x][N]$source and $M'$source is $\lambd[x][N']$source with $N \bredpar N'$source. We want to show that $\lambd[x][N'] \bredpar \bcd{(\lambd[x][N])}$source, i.e., $\lambd[x][N'] \bredpar \lambd[x][\bcd{N}]$source by the abstraction equation for beta complete development. It follows by the abstraction rule for parallel beta reduction and the induction hypothesis.

3. The last rule is the application rule for parallel beta reduction:$M$source is $PQ$source and $M'$source is $P'Q'$source for some $P$source, $Q$source, $P'$source and $Q'$source, with $P \bredpar P'$source and $Q \bredpar Q'$source. By induction hypothesis, we have $P' \bredpar \bcd{P}$source and $Q' \bredpar \bcd{Q}$source.

   1. If $P$source is $\lambd[x][N]$source for some $x$source and $N$source, then $P'$source must be $\lambd[x][N']$source for some $N'$source with $N \bredpar N'$source. By induction hypothesis we have $N' \bredpar \bcd{N}$source and $Q' \bredpar \bcd{Q}$source. Then $(\lambd[x][N'])Q' \bredpar \Subst{\bcd{N}}{\bcd{Q}}{x}$source by the contraction rule for parallel beta reduction.

   2. If $P$source is not a $\lambd$source-abstract, then $P'Q' \bredpar \bcd{P}\bcd{Q}$source by the application rule for parallel beta reduction, and the right-hand side is $\bcd{PQ}$source by the non-redex application equation for beta complete development.

4. The last rule is the contraction rule for parallel beta reduction: $M$source is $(\lambd[x][N])Q$source and $M'$source is $\Subst{N'}{Q'}{x}$source for some $x$source, $N$source, $Q$source, $N'$source, and $Q'$source, with $N \bredpar N'$source and $Q \bredpar Q'$source. By induction hypothesis we know $N' \bredpar \bcd{N}$source and $Q' \bredpar \bcd{Q}$source. By the substitution compatibility lemma for parallel beta reduction we have $\Subst{N'}{Q'}{x} \bredpar \Subst{\bcd{N}}{\bcd{Q}}{x}$source, the right-hand side of which is exactly $\bcd{((\lambd[x][N])Q)}$source.

Exercise completing the beta complete development lemma

Complete the proof of the lemma that every parallel beta reduct reaches the complete development.

Church Rosser property for parallel beta reduction

$\bredpar$source has the Church--Rosser property.

Proof

Immediate from the lemma that every parallel beta reduct reaches the complete development.

One beta contraction is a parallel beta reduction

If $M \bredone M'$source, then $M \bredpar M'$source.

Proof

If $M \bredone M'$source, then $M$source is $(\lambd[x][N])Q$source, $M'$source is $\Subst{N}{Q}{x}$source, for some $x$source, $N$source, and $Q$source. Since $N \bredpar N$source and $Q \bredpar Q$source by the theorem on reflexivity of parallel beta reduction, we immediately have $(\lambd[x][N])Q \bredpar \Subst{N}{Q}{x}$source by the definition of parallel beta reductionthe contraction rule for parallel beta reduction.

A parallel beta step can be serialized

If $M \bredpar M'$source, then $M \bred M'$source.

Proof

By induction on the derivation of $M \bredpar M'$source.

1. The last rule is the variable rule for parallel beta reduction: Then $M$source and $M'$source are just $x$source, and $x \bred x$source.

2. The last rule is the abstraction rule for parallel beta reduction: $M$source is $\lambd[x][N]$source and $M'$source is $\lambd[x][N']$source for some $x$source, $N$source, $N'$source, where $N \bredpar N'$source. By induction hypothesis we have $N \bred N'$source. Then $\lambd[x][N] \bred \lambd[x][N']$source (by the same series of $\bredone$source contractions as $N \bred N'$source).

3. The last rule is the application rule for parallel beta reduction: $M$source is $PQ$source and $M'$source is $P'Q'$source for some $P$source, $Q$source, $P'$source, $Q'$source, where $P \bredpar P'$source and $Q \bredpar Q'$source. By induction hypothesis we have $P \bred P'$source and $Q \bred Q'$source. So $PQ \bred P'Q'$source by the reduction sequence $P \bred P'$source followed by the reduction $Q \bred Q'$source.

4. The last rule is the contraction rule for parallel beta reduction: $M$source is $(\lambd[x][N])Q$source and $M'$source is $\Subst{N'}{Q'}{x}$source for some $x$source, $N$source, $M'$source, $Q$source, $Q'$source, where $N \bredpar N'$source and $Q \bredpar Q'$source. By induction hypothesis we get $Q \bred Q'$source and $N \bred N'$source. So $(\lambd[x][N])Q \bred \Subst{N'}{Q'}{x}$source by $N \bred N'$source followed by $Q \bred Q'$source and finally contraction of $(\lambd[x][N'])Q'$source to $\Subst{N'}{Q'}{x}$source.

Beta reduction is the transitive closure of parallel beta reduction

$\bred$source is the smallest transitive relation containing $\bredpar$source.

Proof

Let $\xred$source be the smallest transitive relation containing $\bredpar$source.

$\bred \subseteq \xred$source: Suppose $M \bred M'$source, i.e., $M \ident M_1 \bredone \dots \bredone M_k \ident M'$source. By the lemma that one beta contraction is a parallel beta reduction, $M \ident M_1 \bredpar \dots \bredpar M_k \ident M'$source. Since is $\xred$source contains $\bredpar$source and is transitive, $M \xred M'$source.

$\xred \subseteq \bred$source: Suppose $M \xred M'$source, i.e., $M \ident M_1 \bredpar \dots \bredpar M_k \ident M'$source. By the lemma serializing parallel beta reduction, $M \ident M_1 \bred \dots \bred M_k \ident M'$source. Since $\bred$source is transitive, $M \bred M'$source.

Church Rosser property for beta reduction

$\bred$source satisfies the Church--Rosser property.

Proof

Immediate from the theorem that transitive closure preserves the Church Rosser property, the Church Rosser theorem for parallel beta reduction, and the lemma identifying beta reduction as the transitive closure of parallel beta reduction.

Five source rules for parallel beta eta reduction

[Parallel $\beta\eta$source-reduction, $\beredpar$source] Parallel $\beta\eta$source-reduction ($\beredpar$source) on terms is inductively defined as follows:

1. $x \beredpar x$source.

2. If $N \xrightarrow{\beta} N'$source then $\lambd[x][N] \beredpar \lambd[x][N']$source.

3. If $P \beredpar P'$source and $Q \beredpar Q'$source then $PQ \beredpar P'Q'$source.

4. If $N \beredpar N'$source and $Q \beredpar Q'$source then $(\lambd[x][N])Q \beredpar \Subst{N'}{Q'}{x}$source.

5. If $N \beredpar N'$source then $\lambd[x][Nx] \beredpar N'$source, provided $x \notin FV(N)$source.

Reflexivity of parallel beta eta reduction

$M \beredpar M$source.

Proof

Exercise.

Exercise proving parallel beta eta reflexivity

Prove the theorem on reflexivity of parallel beta eta reduction.

Source definition of beta eta complete development

[$\beta\eta$source-complete development] The $\beta\eta$source-complete development $\becd{M}$source of $M$source is defined as follows:

Parallel beta eta reduction and substitution

If $M \beredpar M'$source and $R \beredpar R'$source, then $\Subst{M}{R}{y} \beredpar \Subst{M'}{R'}{y}$source.

Proof

By induction on the derivation of $M \beredpar M'$source.

The first four cases are exactly like those in the substitution compatibility lemma for parallel beta reduction. If the last rule is the eta rule for parallel beta eta reduction, then $M$source is $\lambd[x][Nx]$source, $M'$source is $N'$source for some $x$source and $N'$source where $x \notin FV(N)$source, and $N \beredpar N'$source. We want to show that $\Subst{(\lambd[x][Nx])}{R}{y} \beredpar \Subst{N'}{R'}{y}$source, i.e., $\lambd[x][\Subst{N}{R}{y} x] \beredpar \Subst{N'}{R'}{y}$source. It follows by the definition of parallel beta eta reductionthe eta rule for parallel beta eta reduction and the induction hypothesis.

Source beta eta complete development lemma

If $M \beredpar M'$source then $M' \beredpar \becd{M}$source.

Proof

By induction on the derivation of $M \beredpar M'$source.

The first four cases are like those in the lemma that every parallel beta reduct reaches the complete development. If the last rule is the eta rule for parallel beta eta reduction, then $M$source is $\lambd[x][Nx]$source and $M'$source is $N'$source for some $x$source, $N$source, $N'$source where $x \notin FV(N)$source and $N \beredpar N'$source. We want to show that $N' \beredpar \becd{(\lambd[x][Nx])}$source, i.e., $N' \beredpar \becd{N}$source, which is immediate by induction hypothesis.

Source Church Rosser theorem for parallel beta eta reduction

$\beredpar$source has the Church-Rosser property.

Proof

Immediate from the source lemma that every parallel beta eta reduct reaches the complete development.

One beta eta contraction is a parallel beta eta reduction

If $M \beredone M'$source, then $M \beredpar M'$source.

Proof

By induction on the derivation of $M \beredone M'$source. If $M \bredone M'$source by $\eta$source-conversion (i.e., the earlier definition of eta contraction), we use the theorem on reflexivity of parallel beta eta reduction. The other cases are as in the lemma that one beta contraction is a parallel beta reduction.

A parallel beta eta step can be serialized

If $M \beredpar M'$source, then $M \bered M'$source.

Proof

Induction on the derivation of $M \beredpar M'$source.

If the last rule is the eta rule for parallel beta eta reduction, then $M$source is $\lambd[x][Nx]$source and $M'$source is $N'$source for some $x$source, $N$source, $N'$source where $x \notin FV(N)$source and $N \beredpar N'$source. Thus we can first reduce $\lambd[x][Nx]$source to $N$source by $\eta$source-conversion, followed by the series of $\beredone$source steps that show that $N \bered N'$source, which holds by induction hypothesis.

Beta eta reduction is the transitive closure of parallel beta eta reduction

$\bered$source is the smallest transitive relation containing $\beredpar$source.

Proof

As in the lemma identifying beta reduction as the transitive closure of parallel beta reduction

Church Rosser property for beta eta reduction

$\bered$source satisfies Church--Rosser property.

Proof

By the theorem that transitive closure preserves the Church Rosser property, the Church Rosser theorem for parallel beta eta reduction and the lemma identifying beta eta reduction as the transitive closure of parallel beta eta reduction.