Church-Rosser via complete development

In this case study, we give a simple proof of the diamond property of untyped parallel reduction. The proof, due to Masako Takahashi (Parallel Reductions in $\lambda$-Calculus, Information and Computation 118(1), 1995) makes use of a auxilary relation called complete developement. This case study is a good example of proving metatheorems in regular worlds: we use several different worlds, and transport theorems between them.

Syntax and judgements

First, we define the syntax of the language, along with parallel reduction and complete development.
See Reformulating languages to use hypothetical judgements for a discussion of these judgements and their encodings. The only difference between the two relations is the side condition on the complete development application rule, which forces the beta-reduction rule to take precedence over it.
Thus, a single step of complete development contracts all beta-redices in the left-hand term one step. Consequently, all beta-redices must be reduced away before a term can take a reflexivity step.

%sort trm %.
%term lam %pi (%pi trm %-> trm) %-> trm %.
%term app %pi trm %-> trm %-> trm %.
%block trmb {x trm}%.
%worlds (trmb) (trm) %.

Parallel reduction

%sort => {_ trm} {_ trm} %.
%prec %none 10 => %.
%mode => %in %out %.
%term =>/beta
  %pi (app (lam M) N => M' N')
  %<- ({x trm} %pi (x => x) %-> (M x => M' x))
  %<- (N => N') %.
%term =>/app %pi (app M N => (app M' N')) %<- (M => M') %<- (N => N') %.
%term =>/lam %pi (lam M => lam M') %<- ({x trm} %pi (x => x) %-> (M x => M' x)) %.
%block =>b {x trm} {prx x => x}%.
%worlds (=>b) (=> _ _) %.
%total E (=> E _) %.

Note that STELF can prove that parallel reduction is total automatically!

Complete development

%sort notlam {_ trm} %.
%mode notlam %in %.
%term notlam/app notlam (app _ _) %.
%block nlb {x trm} {nlx notlam x}%.
%worlds (nlb) (notlam _) %.
%sort ==> {_ trm} {_ trm} %.
%prec %none 10 ==> %.
%mode ==> %in %out %.
%term ==>/beta
  %pi (app (lam M) N ==> M' N')
  %<- ({x trm} %pi (notlam x) %-> (x ==> x) %-> (M x ==> M' x))
  %<- (N ==> N') %.
%term ==>/app %pi (app M N ==> (app M' N')) %<- (M ==> M') %<- (N ==> N') %<- (notlam M) %.
%term ==>/lam
  %pi (lam M ==> lam M')
  %<- ({x trm} %pi (notlam x) %-> (x ==> x) %-> (M x ==> M' x)) %.
%block ==>b {x trm} {nlx notlam x} {cdx x ==> x}%.
%worlds (==>b) (==> _ _) %.

STELF cannot prove that complete development is total automatically, but we will prove this fact ourselves below.

Below, we will want to work in a world where both parallel reduction and complete development exist.
Thus, we define a block that includes all the assumptions in both =>b and ==>b:

%block =>&==>b {x trm} {prx x => x} {nlx notlam x} {cdx x ==> x}%.

Diamond property of parallel reduction

Every term either is or isn’t a lambda

As a lemma, we need to prove that every term either is or is not a lambda.

%sort lam-or-not {_ trm} %.
%term lam-or-not/lam lam-or-not (lam _) %.
%term lam-or-not/not %pi (lam-or-not E) %<- (notlam E) %.
%sort decide {E} {_ lam-or-not E} %.
%mode decide %in %out %.
%term _ decide (lam _) lam-or-not/lam %.
%term _ decide (app _ _) (lam-or-not/not notlam/app) %.

What world should this lemma be stated in?
It talks about trms, so we definitely need term assumptions, and notlam only makes sense with its assumptions. But neither of the reduction relations are relevant, so we should leave off their hypotheses. However, to prove the theorem, we need to cover the case of decide for variables x, which we do by putting a case in the LF context.
(See Proving metatheorems: Proving metatheorems in non-empty contexts for a discussion of this technique.) Thus, we arrive at:

%block decideb {x trm} {nlx notlam x} {decx decide x (lam-or-not/not nlx)}%.
%worlds (decideb) (decide _ _) %.
%total E (decide E _) %.

Complete development is total

To prove the diamond property, we need to know that every term is reducible under complete-development.
First, we prove a lemma showing that an application reduces if its components do:

%sort ==>-tot/app {_ lam-or-not E1} {_ E1 ==> E1'} {_ E2 ==> E2'} {_ app E1 E2 ==> E''} %.
%mode ==>-tot/app %in %in %in %out %.
%term _ ==>-tot/app lam-or-not/lam (==>/lam D1) D2 (==>/beta D2 D1) %.
%term _ ==>-tot/app (lam-or-not/not Nl) D1 D2 (==>/app Nl D2 D1) %.
%worlds (==>b) (==>-tot/app _ _ _ _) %.
%total {} (==>-tot/app _ _ _ _) %.

Note that the world ==>b is the minimal one in which both ==> and lam-or-not make sense, so it is the most appropriate world to use here.

%sort ==>-tot {E trm} {_ E ==> E'} %.
%mode ==>-tot %in %out %.
%term _
  %pi (==>-tot (lam E) (==>/lam D))
  %<- ({x trm} {nlx notlam x} {cdx x ==> x} {_ decide x (lam-or-not/not nlx)} {_ ==>-tot x cdx} ==>-tot (E x) (D x nlx cdx)) %.
%term _
  %pi (==>-tot (app E E') D)
  %<- (==>-tot E De)
  %<- (==>-tot E' De')
  %<- (decide E Dlon)
  %<- (==>-tot/app Dlon De De' D) %.

This lemma at least needs the assumptions in ==>b for complete development to be adequately represented. Additionally, because the above case uses decide as a lemma, we need to ensure that its assumptions are in the world we choose here. Additionally, to show that variables reduce, we need a theorem case in the context. Thus, we arrive at the following block:

%block ==>totb {x trm} {nlx notlam x} {cdx x ==> x} {_ decide x (lam-or-not/not nlx)} {_ ==>-tot x cdx}%.
%worlds (==>totb) (==>-tot _ _) %.
%total D (==>-tot D _) %.

Why may we call decide from contexts made up of ==>totb blocks when decide was only stated for contexts made up of decideb blocks? In general, extending the context could create new cases that decide would be unable to handle. However, in this instance, both of the new assumptions, which have types ==> and ==>-tot, are irrelevant (insubordinate) to decide, so STELF permits this world subsumption. That is, decide is only concerned with trms and derivations of notlam and derivations of decide itself, and neither ==> nor ==>-tot assumptions influence those types.

Substituting reductions into parallel reduction

We also need to show that the substitution of a reduction is the reduction of the substitution. To prove this lemma, we distinguish cases on an LF function representing the hypothetical derivation:

%sort subst {_ {x trm} %pi (x => x) %-> (M x => M' x)} {_ N => N'} {_ M N => M' N'} %.
%mode subst %in %in %out %.

(M x) is x:

%term _ subst ([x] [prx] prx) Dn Dn %.

(M x) doesn’t mention x at all (this covers all other variables in the context, as well any other x-closed term):

%term _ subst ([x] [prx] D) _ D %.

The remaining cases proceed compositionally:

%term _
  %pi (subst ([x] [prx] =>/app (Dm2 x prx) (Dm1 x prx)) Dn (=>/app Dm2' Dm1'))
  %<- (subst Dm2 Dn Dm2')
  %<- (subst Dm1 Dn Dm1') %.
%term _
  %pi (subst ([x] [prx] =>/beta (Dm2 x prx) ([y] [pry] Dm1 y pry x prx)) Dn (=>/beta Dm2' Dm1'))
  %<- (subst Dm2 Dn Dm2')
  %<- ({y trm} {pry y => y} subst ([x] [prx] Dm1 y pry x prx) Dn (Dm1' y pry)) %.
%term _
  %pi (subst ([x] [prx] =>/lam ([y] [pry] Dm y pry x prx)) Dn (=>/lam Dm'))
  %<- ({y trm} {pry y => y} subst ([x] [prx] Dm y pry x prx) Dn (Dm' y pry)) %.

Because this theorem is property only of parallel reduction, we use the block containing only parallel reduction assumptions:

%worlds (=>b) (subst _ _ _) %.
%total D (subst D _ _) %.

The triangle property

The key lemma in this proof is that given a split of parallel reduction on one side and complete development on the other, there is a parallel reduction on the other side of the triangle:

%sort tri {_ M ==> M'} {_ M => M''} {_ M'' => M'} %.
%mode tri %in %in %out %.
%term _ tri D1 D2 D2 %.
%term _
  %pi (tri (==>/app Dnl (%the (N ==> N') Dn') (%the (M ==> M') Dm')) (=>/app (%the (N => N'') Dn'') (%the (M => M'') Dm'')) (=>/app Dn Dm))
  %<- (tri Dn' Dn'' Dn)
  %<- (tri Dm' Dm'' Dm) %.
%term _
  %pi (tri (==>/lam Dn') (=>/lam Dn'') (=>/lam Dn))
  %<- ({x trm} {prx x => x} {nlx notlam x} {cdx x ==> x} tri (Dn' x nlx cdx) (Dn'' x prx) (Dn x prx)) %.
%term _
  %pi (tri (==>/beta (%the (N ==> N') Dn') (%the ({x} {nlx} {cdx} M x ==> (M' x)) Dm')) (=>/app (%the (N => N'') Dn'') (=>/lam (%the ({x} {prx} M x => (M'' x)) Dm''))) (=>/beta Dn Dm))
  %<- (tri Dn' Dn'' Dn)
  %<- ({x trm} {prx x => x} {nlx notlam x} {cdx x ==> x} tri (Dm' x nlx cdx) (Dm'' x prx) (Dm x prx)) %.
%term _
  %pi (tri (==>/beta (%the (N ==> N') Dn') (%the ({x} {nlx} {cdx} M x ==> (M' x)) Dm')) (=>/beta (%the (N => N'') Dn'') (%the ({x} {prx} M x => (M'' x)) Dm'')) D)
  %<- (tri Dn' Dn'' Dn)
  %<- ({x trm} {prx x => x} {nlx notlam x} {cdx x ==> x} tri (Dm' x nlx cdx) (Dm'' x prx) (Dm x prx))
  %<- (subst Dm Dn D) %.

The best world for this proof is the one where both parallel reduction and complete development exist, and we don’t need any additional assumptions for the proof, so this is the world we use:

%worlds (=>&==>b) (tri _ _ _) %.
%total D (tri D _ _) %.

Let’s investigate why complete development is necessary for this proof to go through. Without the side condition on application, we’d have an additional case to consider, where the complete development was by the application rule, and the parallel reduction was by the beta rule. We’d set up this case as follows:

%term _
  %pi (tri (==>/app IMPOSSIBLE (%the (N ==> N') Dn') (==>/lam (%the (\ ({x\} \ ({nlx\} \ ({cdx\} M x ==> (M' x))))) Dm'))) (=>/beta (%the (N => N_) Dn_) (%the (\ ({x\} \ ({prx\} M x => (M_ x)))) Dm_)) (%the (M_ N_ => app (lam M') N') XXX))
  %<- (tri Dn' Dn_ (%the (N_ => N') Dn))
  %<- (\ ({x trm\} \ ({prx x => x\} \ ({nlx notlam x\} \ ({cdx x ==> x\} tri (Dm' x nlx cdx) (Dm_ x prx) ((%the (\ ({x\} %pi (x => x) %-> (M_ x => (M' x)))) Dm) x prx)))))) %.

From the inductive hypotheses, we know that M_ x => M' x for all x and that N_ => N'. However, we need to prove that M_ N_ => app (lam M') N'. By subst, we can get that the left-hand side reduces to the beta-reduction of the right-hand side, but there the proof breaks down.

The diamond property

We prove the diamond property by first generating a parallel reduction for M and then making two triangles, which complete the square.

%sort dia {_ M => M'} {_ M => M''} {_ M' => N} {_ M'' => N} %.
%mode dia %in %in %out %out %.
%term _
  %pi (dia (%the (M => Mleft) Dleft) (%the (M => Mright) Dright) Dleftmiddle Drightmiddle)
  %<- (==>-tot M D==>middle)
  %<- (tri D==>middle Dleft Dleftmiddle)
  %<- (tri D==>middle Dright Drightmiddle) %.

Because we call both ==>-tot and tri, we need to maintain all the assumptions of both of them.
This is the block =>&==>b extended with the theorem cases for decide and ==>-tot (a.k.a. ==>-totb extended with a parallel reduction assumption). STELF verifies the world subsumption showing that ==>-tot and tri remain true under such extensions of the context.

%block diab {x trm} {prx x => x} {nlx notlam x} {cdx x ==> x} {_ decide x (lam-or-not/not nlx)} {_ ==>-tot x cdx}%.
%worlds (diab) (dia _ _ _ _) %.
%total {} (dia _ _ _ _) %.

Other properties of complete development

To complete the development of complete development, we can prove two other simple lemmas.

Soundness of complete development wrt parallel reduction

First, every complete development reduction is a parallel reduction: we simply forget the proof of the side condition on the application rule.

%sort sound {_ E ==> E'} {_ E => E'} %.
%mode sound %in %out %.
%term _
  %pi (sound (==>/beta Dn Dm) (=>/beta Dn' Dm'))
  %<- (sound Dn Dn')
  %<- ({x} {nlx notlam x} {cdx x ==> x} {prx x => x} {_ sound cdx prx} sound (Dm x nlx cdx) (Dm' x prx)) %.
%term _
  %pi (sound (==>/app _ Dn Dm) (=>/app Dn' Dm'))
  %<- (sound Dm Dm')
  %<- (sound Dn Dn') %.
%term _
  %pi (sound (==>/lam Dm) (=>/lam Dm'))
  %<- ({x} {nlx notlam x} {cdx x ==> x} {prx x => x} {_ sound cdx prx} sound (Dm x nlx cdx) (Dm' x prx)) %.

For this theorem, we need both complete development and parallel reduction, as well as a theorem case, so we extend =>&==>b as follows:

%block soundb {x trm} {nlx notlam x} {cdx x ==> x} {prx x => x} {_ sound cdx prx}%.
%worlds (soundb) (sound _ _) %.
%total D (sound D _) %.

Complete development is deterministic

Finally, we can show that complete development is derministic.

%sort id {_ trm} {_ trm} %.
%term refl id E E %.
%sort id-app-cong {_ id E1 E1'} {_ id E2 E2'} {_ id (app E1 E2) (app E1' E2')} %.
%mode id-app-cong %in %in %out %.
%term _ id-app-cong refl refl refl %.
%worlds (trmb) (id-app-cong _ _ _) %.
%total {} (id-app-cong _ _ _) %.
%sort id-lam-cong {_ {x trm} id (E x) (E' x)} {_ id (lam E) (lam E')} %.
%mode id-lam-cong %in %out %.
%term _ id-lam-cong _ refl %.
%worlds (trmb) (id-lam-cong _ _) %.
%total {} (id-lam-cong _ _) %.
%sort id-func {_ {x trm} id (E x) (E' x)} {_ id E1 E1'} {_ id (E E1) (E' E1')} %.
%mode id-func %in %in %out %.
%term _ id-func ([_] refl) refl refl %.
%worlds (trmb) (id-func _ _ _) %.
%total {} (id-func _ _ _) %.
%sort ==>-det {_ E ==> E'} {_ E ==> E''} {_ id E' E''} %.
%mode ==>-det %in %in %out %.
%term _ ==>-det D D refl %.
%term _
  %pi (==>-det (==>/beta D1 D2) (==>/beta D1' D2') Id)
  %<- (==>-det D1 D1' Id1)
  %<- ({x} {nlx} {cdx} ==>-det (D2 x nlx cdx) (D2' x nlx cdx) (Id2 x))
  %<- (id-func Id2 Id1 Id) %.
%term _
  %pi (==>-det (==>/lam D) (==>/lam D') Id')
  %<- ({x} {nlx} {cdx} ==>-det (D x nlx cdx) (D' x nlx cdx) (Id x))
  %<- (id-lam-cong Id Id') %.
%term _
  %pi (==>-det (==>/app Dnl D2 D1) (==>/app Dnl' D2' D1') Id)
  %<- (==>-det D1 D1' Id1)
  %<- (==>-det D2 D2' Id2)
  %<- (id-app-cong Id1 Id2 Id) %.

STELF rules out the off-diagonal cases for us. For example, an app vs. beta case would have a contradictory derivation of notlam (lam _) as an argument to ==>/app.

%worlds (==>b) (==>-det _ _ _) %.
%total D (==>-det D _ _) %.