# POPL Tutorial/Church Rosser (Problem)

 This is Literate TwelfCode: hereStatus: %% OK %% Output: here.

In this exercise, we will prove the Church-Rosser theorem. You are provided with a syntax and two substitution lemmas, and your task will be to implement two cases of the diamond lemma - the Application-Application case, and the Beta-Application case.

You will be able to uncomment the %total at the end when you are done.

The solution is here.

## Syntax

```exp : type.  %name exp E.
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.```

When we use this %block, it expresses that we can be working in a context with arbitrary expression variables. This will be the only world we will need for this exercise.

`%block exps : block {x: exp}.`

## Reduction

We can always reduce an expression to itself (which means that we don't explicitly need a case to handle variables). We can reduce under binders and reduce both sides of an application "in parallel." If we have a β-redex (λx.ea) eb, then after reducing ea (with x free) to ea' (with x free) and reducing eb to eb', we can return [eb'/x]ea', the substitution of eb' into ea'.

The %worlds explicitly states that we will be reducing in a setting with free variables.

```reduce : exp -> exp -> type.

reduce/id : reduce E E.

reduce/lam : reduce (lam E) (lam E')
<- ({x:exp} reduce (E x) (E' x)).

reduce/app : reduce (app E1 E2) (app E1' E2')
<- reduce E1 E1'
<- reduce E2 E2'.

reduce/beta : reduce (app (lam E1) E2) (E1' E2')
<- ({x:exp} reduce (E1 x) (E1' x))
<- reduce E2 E2'.

%worlds (exps) (reduce _ _).```

## Substitution

The first substitution theorem says that if we have a term e1 with x free and a term e2 that reduces to term e2', then [e2/x]e1 reduces to [e2'/x]e1.

The interesting cases are really the first two - if the term is just the free variable being substituted for, the result follows from the hypothesis. In the case that the free variable is not free (i.e. the term has no hole), then the result follows from the reflexivity of reduction. This is more than sufficient to handle the case of a variable that is not the distinguished free variable, and all other cases are covered.

The proof is by induction on the structure of the term with the free variable.

```substitute1 : {E1:exp -> exp} reduce E2 E2' -> reduce (E1 E2) (E1 E2') -> type.
%mode substitute1 +X1 +X2 -X3.

- : substitute1 ([x] x) D D.

- : substitute1 ([x] E) _ reduce/id.

- : substitute1 ([x] lam ([y] E x y)) D (reduce/lam D')
<- ({y} substitute1 ([x] E x y) D (D' y)).

- : substitute1 ([x] app (E1 x) (E2 x)) D (reduce/app D2 D1)
<- substitute1 E1 D D1
<- substitute1 E2 D D2.

%worlds (exps) (substitute1 _ _ _).
%total E (substitute1 E _ _).```

The second substitution theorem is similar, except that we are reducing e1 with x free to e1' as well as by reducing e2 to e2', showing that [e2/x]e1 reduces to [e2'/x]e1'.

Proof is by induction on the structure of the reduction of e1 to e1'. We call to the substitute1 lemma when we "bottom out" at the reflexive case reduce/id.

```substitute2
: ({x:exp} reduce (E1 x) (E1' x))
-> reduce E2 E2'
-> reduce (E1 E2) (E1' E2')
-> type.
%mode substitute2 +X1 +X2 -X3.

- : substitute2 ([x] reduce/id : reduce (E x) (E x)) D D'
<- substitute1 E D D'.

- : substitute2 ([x] reduce/lam ([y] D1 x y)) D2 (reduce/lam D)
<- ({y} substitute2 ([x] D1 x y) D2 (D y)).

- : substitute2 ([x] reduce/app (D2 x) (D1 x)) D (reduce/app D2' D1')
<- substitute2 D1 D D1'
<- substitute2 D2 D D2'.

- : substitute2 ([x] reduce/beta (D2 x) ([y] D1 x y)) D (reduce/beta D2' D1')
<- ({y} substitute2 ([x] D1 x y) D (D1' y))
<- substitute2 D2 D D2'.

%worlds (exps) (substitute2 _ _ _).
%total D (substitute2 D _ _).```

## The Diamond Property

Now we come to the interesting part: the diamond property.

```   E
/ \
/   \
E1   E2
\   /
\ /
E'
```

If E reduces to both E1, and E2, then there is a common E' such that E1 and E2 both reduce to it.

```diamond : reduce E E1 -> reduce E E2 -> reduce E1 E' -> reduce E2 E' -> type.
%mode diamond +X1 +X2 -X3 -X4.```

### Identity

If either case is the identity, then we are done.

```id:    E  D:       D:     E  id:
e=>e  / \ e=>e2    e=>e1 / \ e=>e
/   \              /   \
E    E2            E1    E
D:   \   /id:      id:  \   /D:
e=>e2 \ / e2=>e2   e1=>e1\ / e=>e1
e2                 E1
```
```- : diamond reduce/id D D reduce/id.
- : diamond D reduce/id reduce/id D.```

### Lambda-Lambda

If both cases are reductions under a binder, we pull the result straight from the induction hypothesis.

```            λx.e              by induction:
reduce/lam   / \  reduce/lam    D1, D2 ---> D1': e1'=>e'
(D1: e=>e1) /   \ (D2: e=>e2)               D2': e2'=>e'
/     \
λx.e1   λx.e2
\     /
reduce/lam  \   / reduce/lam
D1'          \ /  D2'
λx.e'
```

Note the oversimplification being made in the graphical presentation, in that the subterms and sub-derivations are not clearly shown to have a free variable. Twelf will, of course, not allow this sloppiness.

```- : diamond
(reduce/lam (D1 : {x: exp} reduce (E x) (E1 x))
: reduce (lam E) (lam E1))
(reduce/lam (D2 : {x: exp} reduce (E x) (E2 x))
: reduce (lam E) (lam E2))
(reduce/lam D1') (reduce/lam D2')
<- ({x: exp} diamond (D1 x) (D2 x)
(D1' x : reduce (E1 x) (E' x))
(D2' x : reduce (E2 x) (E' x))).```

### Application-Application

If both cases are applications, we pull the result straight from the induction hypothesis.

```                 ea eb                by induction
reduce/app       /   \   reduce/app     D1a, D2a ---> D1a': e1a=>ea'
(D1b: eb=>e1b)  /     \  (D2b: eb=>e2b)               D2a': e2a=>ea'
(D1a: ea=>e1a) /       \ (D2a: ea=>e2a) D1b, D2b ---> D1b': e1b=>eb'
e1a e1b   e2a e2b                          D2b': e2b=>eb'
\       /
reduce/app      \     /  reduce/app
D1b' D1a'        \   /   D2b' D2a'
ea' eb'
```
`%% WRITE THIS CASE`

### Beta-Beta

If both cases are beta reductions, we get the result from performing two substitutions.

```              (λx.ea) eb            by induction
reduce/beta      / \   reduce/beta    D1a, D2a ---> D1a': e1a=>ea'
(D1b: eb=>e1b)  /   \  (D2b: eb=>e2b)               D2a': e2a=>ea'
(D1a: ea=>e1a) /     \ (D2a: ea=>e1a) D1b, D2b ---> D1b': e1b=>eb'
[e1b/x]e1a  [e2b/x]e2a                      D2b': e2b=>eb'
\     /
substitute      \   /  substitute
D1b' into D1a'   \ /   D2b' into D2a'
[eb'/x]ea
```
```- : diamond
(reduce/beta
(D1b : reduce Eb E1b)
(D1a : {x} reduce (Ea x) (E1a x))
: reduce (app (lam Ea) Eb) (E1a E1b))
(reduce/beta
(D2b : reduce Eb E2b)
(D2a : {x} reduce (Ea x) (E2a x))
: reduce (app (lam Ea) Eb) (E2a E2b))
D1 D2
<- ({x} diamond (D1a x) (D2a x)
(D1a' x : reduce (E1a x) (Ea' x))
(D2a' x : reduce (E2a x) (Ea' x)))
<- diamond D1b D2b
(D1b'   : reduce E1b Eb')
(D2b'   : reduce E2b Eb')
<- substitute2 D1a' D1b'
(D1     : reduce (E1a E1b) (Ea' Eb'))
<- substitute2 D2a' D2b'
(D2     : reduce (E2a E2b) (Ea' Eb')).```

### Beta-Application

If the left-hand side is a β-reduction (λx.ea) eb => [e1b/x] e1a but the right-hand side is not, then we know that the right-hand side reduction must be (λx.ea) eb => (λx.e2a) e2b.

Unfortunately, then we have two options - either λx.ea => λx.e2a by reduce/refl and reduce/lam. The reduce/refl case is essentially just an inconvenience caused by allowing identity reductions anywhere (not just at variables).

The first subcase:

```             (λx.ea) eb              by induction
reduce/beta      / \   reduce/app      D1a, D2a ---> D1a': e1a=>ea'
(D1b: eb=>e1b)  /   \  (D2b: eb=>e2b)                D2a': e2a=>ea'
(D1a: ea=>e1a) /     \ (reduce/lam     D1b, D2b ---> D1b': e1b=>eb'
/       \  (D2a: ea=>e2a))             D2b': e1b=>eb'
[e1b/x]e1a  (λx.e2a) e2b
\       /
substitute     \     / reduce/beta
D1b' into D2a'  \   /  D2b' D2a'
\ /
[eb'/x]ea'
```
`%% WRITE THIS CASE`

The second subcase:

```             (λx.ea) eb              by induction
reduce/beta      / \   reduce/app      D1b, D2b ---> D1b': e1b=>eb'
(D1b: eb=>e1b)  /   \  (D2b: eb=>e2b)                D2b': e1b=>eb'
(D1a: ea=>e1a) /     \ (reduce/id
/       \   ea=>ea))
[e1b/x]e1a   (λx.ea) e2b
\       /
substitute     \     / reduce/beta
D1b' into e1a   \   /  D2b' D1a
\ /
[eb'/x]e1a
```
```- : diamond
(reduce/beta
(D1b : reduce Eb E1b)
(D1a : {x} reduce (Ea x) (E1a x))
: reduce (app (lam Ea) Eb) (E1a E1b))
(reduce/app
(D2b : reduce Eb E2b)
(reduce/id : reduce (lam Ea) (lam Ea))
: reduce (app (lam Ea) Eb) (app (lam Ea) E2b))
D1 (reduce/beta D2b' D1a)
<- diamond D1b D2b
(D1b'   : reduce E1b Eb')
(D2b'   : reduce E2b Eb')
<- substitute1 E1a D1b'
(D1     : reduce (E1a E1b) (E1a Eb')).```

### Application-Beta

If the right-hand hand side is a β-reduction but the left-hand side is not, we have to do the same two cases in reverse; we omit the graphics for those two cases as they are symmetric.

```- : diamond
(reduce/app
(D1b : reduce Eb E1b)
(reduce/id : reduce (lam Ea) (lam Ea))
: reduce (app (lam Ea) Eb) (app (lam Ea) E1b))
(reduce/beta
(D2b : reduce Eb E2b)
(D2a : {x} reduce (Ea x) (E2a x))
: reduce (app (lam Ea) Eb) (E2a E2b))
(reduce/beta D1b' D2a) D2
<- diamond D1b D2b
(D1b'   : reduce E1b Eb')
(D2b'   : reduce E2b Eb')
<- substitute1 E2a D2b'
(D2     : reduce (E2a E2b) (E2a Eb')).

- : diamond
(reduce/app
(D1b : reduce Eb E1b)
(reduce/lam (D1a : {x} reduce (Ea x) (E1a x)))
: reduce (app (lam Ea) Eb) (app (lam E1a) E1b))
(reduce/beta
(D2b : reduce Eb E2b)
(D2a : {x} reduce (Ea x) (E2a x))
: reduce (app (lam Ea) Eb) (E2a E2b))
(reduce/beta D1b' D1a') D2
<- ({x} diamond (D1a x) (D2a x)
(D1a' x : reduce (E1a x) (Ea' x))
(D2a' x : reduce (E2a x) (Ea' x)))
<- diamond D1b D2b
(D1b'   : reduce E1b Eb')
(D2b'   : reduce E2b Eb')
<- substitute2 D2a' D2b'
(D2     : reduce (E2a E2b) (Ea' Eb')).```

Now we are done! We check in the exps world with free variables.

```%worlds (exps) (diamond _ _ _ _).
%% %total D1 (diamond D1 D2 _ _).```