Church-Rosser (w/ catch-all case)

Syntax

%sort exp %.
%name exp %.
%term lam %pi (%pi exp %-> exp) %-> exp %.
%term app %pi exp %-> exp %-> exp %.

When we use this %block, it expresses that we can be working in a context with arbitrary expression variables.

%block exps {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.

%sort reduce {_ exp} {_ exp} %.
%mode reduce %in %out %.
%term reduce/lam
  %pi (reduce (lam E) (lam E'))
  %<- ({x exp} %pi (reduce x x) %-> (reduce (E x) (E' x))) %.
%term reduce/app %pi (reduce (app E1 E2) (app E1' E2')) %<- (reduce E1 E1') %<- (reduce E2 E2') %.
%term reduce/beta
  %pi (reduce (app (lam E1) E2) (E1' E2'))
  %<- ({x exp} %pi (reduce x x) %-> (reduce (E1 x) (E1' x)))
  %<- (reduce E2 E2') %.
%block exps_red {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.

%sort identity {E} {_ reduce E E} %.
%mode identity %in %out %.
%term _
  %pi (identity (lam ([x] E x)) (reduce/lam D))
  %<- ({x} {idx reduce x x} %pi (identity x idx) %-> (identity (E x) (%the (reduce (E x) (E x)) (D x idx)))) %.
%term _
  %pi (identity (app E1 E2) (reduce/app D2 D1))
  %<- (identity E1 (%the (reduce E1 E1) D1))
  %<- (identity E2 (%the (reduce E2 E2) D2)) %.
%block exps_id {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 $e_{arg}$ reduces to $e'_{arg}$, then $[e_{arg}$/x]e reduces to $[e'_{arg}$/x]e'.

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

%sort substitute {_ {x exp} %pi (reduce x x) %-> (reduce (E x) (E' x))} {_ reduce Earg Earg'} {_ reduce (E Earg) (E' Earg')} %.
%mode substitute %in %in %out %.

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 STELF 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.

%term _ substitute ([x] [redx reduce x x] redx) Darg Darg %.
%term _ substitute ([x] [redx reduce x x] D) Darg D %.
%term _
  %pi (substitute ([x] [redx reduce x x] reduce/lam (%the ({y} %pi (reduce y y) %-> (reduce (E x y) (E' x y))) (D x redx))) (%the (reduce Earg Earg') Darg) (%the (reduce (lam ([y] E Earg y)) (lam ([y] E' Earg' y))) (reduce/lam D')))
  %<- ({y} {redy reduce y y} substitute ([x] [redx reduce x x] D x redx y redy) Darg (%the (reduce (E Earg y) (E' Earg' y)) (D' y redy))) %.
%term _
  %pi (substitute ([x] [redx reduce x x] reduce/app (%the (reduce (Eb x) (Eb' x)) (Db x redx)) (%the (reduce (Ea x) (Ea' x)) (Da x redx))) (%the (reduce Earg Earg') Darg) (%the (reduce (app (Ea Earg) (Eb Earg)) (app (Ea' Earg') (Eb' Earg'))) (reduce/app Db' Da')))
  %<- (substitute Da Darg (%the (reduce (Ea Earg) (Ea' Earg')) Da'))
  %<- (substitute Db Darg (%the (reduce (Eb Earg) (Eb' Earg')) Db')) %.
%term _
  %pi (substitute ([x] [redx reduce x x] reduce/beta (%the (reduce (Eb x) (Eb' x)) (Db x redx)) (%the ({y} %pi (reduce y y) %-> (reduce (Ea x y) (Ea' x y))) (Da x redx))) (%the (reduce Earg Earg') Darg) (%the (reduce (app (lam (Ea Earg)) (Eb Earg)) (Ea' Earg' (Eb' Earg'))) (reduce/beta Db' Da')))
  %<- ({y} {redy reduce y y} substitute ([x] [redx reduce x x] Da x redx y redy) Darg (%the (reduce (Ea Earg y) (Ea' Earg' y)) (Da' y redy)))
  %<- (substitute Db Darg (%the (reduce (Eb Earg) (Eb' Earg')) Db')) %.
%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.

%sort diamond {_ reduce E E1} {_ reduce E E2} {_ reduce E1 E'} {_ reduce E2 E'} %.
%mode diamond %in %in %out %out %.

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

%term _
  %pi (diamond (%the (reduce E E) ID) (%the (reduce E E2) D) D ID')
  %<- (identity E2 ID') %.
%term _
  %pi (diamond (%the (reduce E E1) D) (%the (reduce E E) ID) (%the (reduce E1 E1) ID') 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. STELF will, of course, not allow this sloppiness.

%term _
  %pi (diamond (%the (reduce (lam E) (lam E1)) (reduce/lam (%the ({x exp} {redx reduce x x} reduce (E x) (E1 x)) D1))) (%the (reduce (lam E) (lam E2)) (reduce/lam (%the ({x exp} {redx reduce x x} reduce (E x) (E2 x)) D2))) (reduce/lam D1') (reduce/lam D2'))
  %<- ({x exp} {redx reduce x x} {idx identity x redx} diamond (D1 x redx) (D2 x redx) (%the (reduce (E1 x) (E' x)) (D1' x redx)) (%the (reduce (E2 x) (E' x)) (D2' x redx))) %.

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’

%term _
  %pi (diamond (%the (reduce (app Ea Eb) (app E1a E1b)) (reduce/app (%the (reduce Eb E1b) D1b) (%the (reduce Ea E1a) D1a))) (%the (reduce (app Ea Eb) (app E2a E2b)) (reduce/app (%the (reduce Eb E2b) D2b) (%the (reduce Ea E2a) D2a))) (reduce/app D1b' D1a') (reduce/app D2b' D2a'))
  %<- (diamond D1a D2a (%the (reduce E1a Ea') D1a') (%the (reduce E2a Ea') D2a'))
  %<- (diamond D1b D2b (%the (reduce E1b Eb') D1b') (%the (reduce E2b Eb') D2b')) %.

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

%term _
  %pi (diamond (%the (reduce (app (lam Ea) Eb) (E1a E1b)) (reduce/beta (%the (reduce Eb E1b) D1b) (%the ({x} %pi (reduce x x) %-> (reduce (Ea x) (E1a x))) D1a))) (%the (reduce (app (lam Ea) Eb) (E2a E2b)) (reduce/beta (%the (reduce Eb E2b) D2b) (%the ({x} %pi (reduce x x) %-> (reduce (Ea x) (E2a x))) D2a))) D1 D2)
  %<- ({x} {redx reduce x x}
  %pi (identity x redx)
  %-> (diamond (D1a x redx) (D2a x redx) (%the (reduce (E1a x) (Ea' x)) (D1a' x redx)) (%the (reduce (E2a x) (Ea' x)) (D2a' x redx))))
  %<- (diamond D1b D2b (%the (reduce E1b Eb') D1b') (%the (reduce E2b Eb') D2b'))
  %<- (substitute D1a' D1b' (%the (reduce (E1a E1b) (Ea' Eb')) D1))
  %<- (substitute D2a' D2b' (%the (reduce (E2a E2b) (Ea' Eb')) D2)) %.

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’

%term _
  %pi (diamond (%the (reduce (app (lam Ea) Eb) (E1a E1b)) (reduce/beta (%the (reduce Eb E1b) D1b) (%the ({x exp} %pi (reduce x x) %-> (reduce (Ea x) (E1a x))) D1a))) (%the (reduce (app (lam Ea) Eb) (app (lam E2a) E2b)) (reduce/app (%the (reduce Eb E2b) D2b) (reduce/lam (%the ({x exp} %pi (reduce x x) %-> (reduce (Ea x) (E2a x))) D2a)))) D1 (reduce/beta D2b' D2a'))
  %<- ({x exp} {redx reduce x x}
  %pi (identity x redx)
  %-> (diamond (D1a x redx) (D2a x redx) (%the (reduce (E1a x) (Ea' x)) (D1a' x redx)) (%the (reduce (E2a x) (Ea' x)) (D2a' x redx))))
  %<- (diamond D1b D2b (%the (reduce E1b Eb') D1b') (%the (reduce E2b Eb') D2b'))
  %<- (substitute D1a' D1b' (%the (reduce (E1a E1b) (Ea' Eb')) D1)) %.

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.

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

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

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