# Church-Rosser (w/ catch-all case)

 This is Literate TwelfCode: hereStatus: %% OK %% Output: 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.

```%block exps : block {x: exp}.
%worlds (exps) (exp).```

## Reduction

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'. When we introduce a new variable, we always add in the fact that it can evaluate to itself.

The %block exps_red explicitly states that we will be reducing in a setting with free variables, with the invariant that every variable is added with the invariant that it can evaluate to itself.

```reduce : exp -> exp -> type.
%mode reduce +E -E'.

reduce/lam : reduce (lam E) (lam E')
<- ({x:exp} reduce x x -> 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 x x -> reduce (E1 x) (E1' x))
<- reduce E2 E2'.

%block exps_red : block {x: exp}{d: reduce x x}.
%worlds (exps_red) (reduce _ _).
%total E (reduce E _).```

### Reduction is reflexive

We will need to know later that reduction is reflexive. It is an easy proof by induction on the first argument, but we cannot get away with using a catch-all case, so when we go under a binder. This forces us to describe a new world, exps_id, that captures the variable case of this theorem.

```identity : {E} reduce E E -> type.
%mode identity +A -B.

- : identity (lam ([x] E x)) (reduce/lam D)
<- ({x}{idx : reduce x x}
identity x idx
-> identity (E x) (D x idx : reduce (E x) (E x))).

- : identity (app E1 E2) (reduce/app D2 D1)
<- identity E1 (D1 : reduce E1 E1)
<- identity E2 (D2 : reduce E2 E2).

%block exps_id : block {x: exp}{redx: reduce x x}{idx: identity x redx}.
%worlds (exps_id) (identity _ _).
%total T (identity T _).```

## Substitution

The substitution theorem says that if we have a term e with x free that reduces to e' (with x still free) and earg reduces to e'arg, then [earg/x]e reduces to [e'arg/x]e'.

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

```substitute
: ({x: exp} reduce x x -> reduce (E x) (E' x))
-> reduce Earg Earg'
-> reduce (E Earg) (E' Earg') -> type.
%mode substitute +D +Darg -D'.```

We actually need to think about what block this theorem will take place in, because there are at least two options. In this variant, we utilize the technique of using a catch-all case in order to avoid putting a fact about variable substitution cases in the context. This latter style is used in the Twelf examples directory and is explored on the wiki in the page Church-Rosser (alternate substitution theorem).

The interesting cases are really the first two - if we reach a reduction for the variable we are substituing for, then our second argument is the answer (the rest of the time that variable just gets passed around). If we reach a point where the variable we are substuiting for doesn't even appear in the term (this is the catch-all case), then that first argument is the answer.

```- : substitute ([x] [redx: reduce x x] redx) Darg Darg.

- : substitute ([x] [redx: reduce x x] D) Darg D.

- : substitute
([x] [redx: reduce x x]
reduce/lam
(D x redx : {y} reduce y y -> reduce (E x y) (E' x y)))
(Darg: reduce Earg Earg')
(reduce/lam D'
: reduce (lam ([y] (E Earg) y)) (lam ([y] (E' Earg') y)))
<- ({y} {redy: reduce y y}
substitute ([x] [redx: reduce x x] D x redx y redy) Darg
(D' y redy : reduce (E Earg y) (E' Earg' y))).

- : substitute
([x] [redx: reduce x x]
reduce/app
(Db x redx : reduce (Eb x) (Eb' x))
(Da x redx : reduce (Ea x) (Ea' x)))
(Darg: reduce Earg Earg')
(reduce/app Db' Da'
: reduce (app (Ea Earg) (Eb Earg)) (app (Ea' Earg') (Eb' Earg')))
<- substitute Da Darg (Da': reduce (Ea Earg) (Ea' Earg'))
<- substitute Db Darg (Db': reduce (Eb Earg) (Eb' Earg')).

- : substitute
([x] [redx: reduce x x]
reduce/beta
(Db x redx : reduce (Eb x) (Eb' x))
(Da x redx : {y} reduce y y -> reduce (Ea x y) (Ea' x y)))
(Darg: reduce Earg Earg')
(reduce/beta Db' Da'
: reduce (app (lam (Ea Earg)) (Eb Earg)) ((Ea' Earg') (Eb' Earg')))
<- ({y} {redy: reduce y y}
substitute ([x] [redx: reduce x x] Da x redx y redy) Darg
(Da' y redy : reduce (Ea Earg y) (Ea' Earg' y)))
<- substitute Db Darg (Db': reduce (Eb Earg) (Eb' Earg')).

%worlds (exps_red) (substitute _ _ _).
%total D (substitute 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 (ID : reduce E E) (D : reduce E E2)
D ID'
<- identity E2 ID'.
- : diamond (D : reduce E E1) (ID : reduce E E)
(ID' : reduce E1 E1) D
<- identity E1 ID'.```

### 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}{redx: reduce x x} reduce (E x) (E1 x))
: reduce (lam E) (lam E1))
(reduce/lam (D2 : {x: exp}{redx: reduce x x} reduce (E x) (E2 x))
: reduce (lam E) (lam E2))
(reduce/lam D1') (reduce/lam D2')
<- ({x: exp}{redx: reduce x x}{idx: identity x redx}
diamond (D1 x redx) (D2 x redx)
(D1' x redx : reduce (E1 x) (E' x))
(D2' x redx : 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'
```
```- : diamond
(reduce/app (D1b : reduce Eb E1b) (D1a : reduce Ea E1a)
: reduce (app Ea Eb) (app E1a E1b))
(reduce/app (D2b : reduce Eb E2b) (D2a : reduce Ea E2a)
: reduce (app Ea Eb) (app E2a E2b))
(reduce/app D1b' D1a') (reduce/app D2b' D2a')
<- diamond D1a D2a
(D1a' : reduce E1a Ea')
(D2a' : reduce E2a Ea')
<- diamond D1b D2b
(D1b' : reduce E1b Eb')
(D2b' : reduce E2b Eb').```

### 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 x x -> reduce (Ea x) (E1a x))
: reduce (app (lam Ea) Eb) (E1a E1b))
(reduce/beta
(D2b : reduce Eb E2b)
(D2a : {x} reduce x x -> reduce (Ea x) (E2a x))
: reduce (app (lam Ea) Eb) (E2a E2b))
D1 D2
<- ({x}{redx : reduce x x}
identity x redx -> diamond (D1a x redx) (D2a x redx)
(D1a' x redx : reduce (E1a x) (Ea' x))
(D2a' x redx : reduce (E2a x) (Ea' x)))
<- diamond D1b D2b
(D1b' : reduce E1b Eb')
(D2b' : reduce E2b Eb')
<- substitute D1a' D1b'
(D1   : reduce (E1a E1b) (Ea' Eb'))
<- substitute 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, which means it is a reduce/lam hiding inside a reduce/app.

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'
```
```- : diamond
(reduce/beta
(D1b : reduce Eb E1b)
(D1a : {x: exp} reduce x x -> reduce (Ea x) (E1a x))
: reduce (app (lam Ea) Eb) (E1a E1b))
(reduce/app
(D2b : reduce Eb E2b)
(reduce/lam (D2a : {x: exp} reduce x x -> reduce (Ea x) (E2a x)))
: reduce (app (lam Ea) Eb) (app (lam E2a) E2b))
D1 (reduce/beta D2b' D2a')
<- ({x: exp}{redx: reduce x x}
identity x redx -> diamond (D1a x redx) (D2a x redx)
(D1a' x redx : reduce (E1a x) (Ea' x))
(D2a' x redx : reduce (E2a x) (Ea' x)))
<- diamond D1b D2b
(D1b' : reduce E1b Eb')
(D2b' : reduce E2b Eb')
<- substitute D1a' D1b'
(D1   : reduce (E1a E1b) (Ea' 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 case in reverse; we omit the graphic.

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

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

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