POPL Tutorial/Typed bracket abstraction with equivalence

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.

This is a case study translating the simply lambda calculus into S, K, and I combinatory logic. The correctness of the translation is proven in the following sense: if a two terms are beta-eta equal, then their translations are beta-eta equal.

William Lovas

Syntax and static semantics

First we define the syntax of the two languages. term A is the type of simply-typed lambda-calculus terms of type A; comb A is the type of simply-typed combinator terms of type A. Combinators are of interest primarily because they have no binding structure; despite this apparent limitation, we can translate any lambda-calculus term to an operationally and logically related combinator term.

Note that since we're using an intrinsic encoding, these syntax definitions double as definitions of the languages' static semantics.

tp : type.              %name tp A a.

o : tp.
=> : tp -> tp -> tp.    %infix right 10 =>.


term : tp -> type.      %name term M x.

%% tm : type.              %name tm M x.
%% %abbrev term : tp -> type = [x] tm.

app : term (A => B) -> term A -> term B.
lam : (term A -> term B) -> term (A => B).


comb : tp -> type.     %name comb N y.

%% cm : type.              %name cm N y.
%% %abbrev comb : tp -> type = [x] cm.

s : comb ((A => B => C) => (A => B) => A => C).
k : comb (A => B => A).
i : comb (A => A).

capp : comb (A => B) -> comb A -> comb B.

We can use Twelf's abbreviation mechanism and fixity declarations to obtain some cute syntax.

%abbrev @ = app.
%infix left 10 @.

%abbrev @@ = capp.
%infix left 10 @@.

Equational theory

Then we define equality relations on both languages. teq is definitional equality for lambda terms; ceq is definitional equality for combinator terms. In both cases, the equality relation amounts to beta-eta equivalence. (We use extensionality instead of a rule based on eta-expansion.)

% definitional equality on terms (better name?)
teq : term A -> term A -> type.
%mode teq *M1 *M2.  % spurious mode declaration necessary?  see unique-block..

% beta
eq/beta : teq (app (lam [x] M1 x) M2) (M1 M2).

% eta
eq/eta : teq M1 M2
          <- ({x} teq (app M1 x) (app M2 x)).

% XXX interesting note: beta + ext ⊦ lam.  lam + beta + eta ⊦ ext.
% others?  cut out some cases?

% compatibilities
eq/lam : teq (lam [x] M x) (lam [x] M' x)
          <- ({x} teq (M x) (M' x)).

eq/app : teq (app M1 M2) (app M1' M2')
          <- teq M1 M1'
          <- teq M2 M2'.

% equivalence
eq/refl : teq M M.

eq/symm : teq M M'
           <- teq M' M.

eq/trans : teq M M''
            <- teq M' M''
            <- teq M M'.

%block teq-block : some {A:tp} block {x:term A}.
%worlds (teq-block) (teq _ _).

% definitional equality on combs
ceq : comb A -> comb A -> type.

% betas
ceq/i : ceq (capp i N) N.
ceq/k : ceq (capp (capp k N1) N2) N1.
ceq/s : ceq (capp (capp (capp s N1) N2) N3) (capp (capp N1 N3) (capp N2 N3)).

% eta
ceq/eta : ceq N1 N2
           <- ({y} ceq (capp N1 y) (capp N2 y)).

% compatibility
ceq/app : ceq (capp N1 N2) (capp N1' N2')
           <- ceq N1 N1'
           <- ceq N2 N2'.

% equivalence
ceq/refl : ceq N N.

ceq/symm : ceq N N'
            <- ceq N' N.

ceq/trans : ceq N N''
             <- ceq N' N''
             <- ceq N N'.

%abbrev ; : ceq N N' -> ceq N' N'' -> ceq N N'' = [d1] [d2] ceq/trans d1 d2.
%infix right 5 ;.

%block ceq-block : some {A:tp} block {y:comb A}.
%worlds (ceq-block) (ceq _ _).

Translation

We can now define a compositional translation from lambda terms to combinator terms in the standard way. The translation appeals to a function called bracket abstraction which simulates binding in the combinator calculus.

Bracket abstraction is usually written where is a combinator term, and is a variable potentially free in . (Be careful not to confuse these brackets with Twelf's syntax for lambda abstraction.) It is defined inductively over the term :


(where not free in )

Using it, we can define a translation on lambda-terms, , where is a lambda-term, as follows:


=

Note that in the definition of bracket abstraction, we need not consider a case for lambda-abstraction since bracket abstraction works over combinator terms, in which lambda-abstraction has already been eliminated.

The main translation is represented in LF by a judgement (an LF type family) translate M N. Bracket abstraction is represented by a judgement relating LF-level abstractions in the combinator language to closed combinator terms, bracket ([x] N x) N. This definition is essentially an instance of higher-order abstract syntax.

translate : term A -> comb A -> type.
%mode translate +M -N.
%name translate Dtrans dtrans.

bracket : (comb A -> comb B) -> comb (A => B) -> type.
%mode bracket +N -N*.
%name bracket Dbrack dbrack.


t/app : translate (app M1 M2) (capp N1 N2)
         <- translate M1 N1
         <- translate M2 N2.

The translation on lambda-abstractions has to work under an extended context with a lambda-term variable, a combinator-term variable, and an assumption that the one translates to the other. See the %worlds declaration below.

t/lam : translate (lam [x] M x) N*
         <- ({x:term A} {y:comb A} translate x y -> translate (M x) (N y))
         <- bracket ([y] N y) N*.


b/i : bracket ([x] x) i.

b/k : bracket ([x] Y) (capp k Y).

b/s : bracket ([x] capp (N1 x) (N2 x)) (capp (capp s N1') N2')
       <- bracket ([x] N1 x) N1'
       <- bracket ([x] N2 x) N2'.


%block trans-block : some {A:tp}
                     block {x:term A} {y:comb A} {dtrans:translate x y}.

%worlds (trans-block) (bracket _ _).
%worlds (trans-block) (translate _ _).

Both relations are effective (though we cannot use this fact in proofs).

%total N (bracket N _).
%total M (translate M _).

Instead, we need effectiveness lemmas. XXX explain this better...

can-bracket : {N : comb A -> comb B} bracket N N* -> type.
%mode can-bracket +N -Dbrack.

can-translate : {M : term A} translate M N -> type.
%mode can-translate +M -Dtrans.

- : can-bracket ([x] x) b/i.
- : can-bracket ([x] N) b/k.
- : can-bracket ([x] capp (N1 x) (N2 x)) (b/s Dbrack2 Dbrack1)
     <- can-bracket ([x] N1 x) Dbrack1
     <- can-bracket ([x] N2 x) Dbrack2.

- : can-translate (app M1 M2) (t/app Dtrans2 Dtrans1)
     <- can-translate M1 (Dtrans1 : translate M1 N1)
     <- can-translate M2 (Dtrans2 : translate M2 N2).

- : can-translate (lam [x] M x) (t/lam Dbrack Dtrans)
     <- ({x} {y} {dtrans: translate x y} {thm: can-translate x dtrans}
            can-translate (M x) (Dtrans x y dtrans : translate (M x) (N y)))
     <- can-bracket ([y] N y) (Dbrack : bracket ([y] N y) N*).

%block can-block
            : some {A:tp}
              block {x:term A} {y:comb A}
                    {dtrans: translate x y}
                    {thm: can-translate x dtrans}.

%worlds (can-block) (can-bracket _ _).
%total N (can-bracket N _).

%worlds (can-block) (can-translate _ _).
%total M (can-translate M _).

Correctness of the translation

First, we prove the correctness of bracket abstraction itself: the application of a bracket abstraction reduces to a substitution.

subst : bracket ([x] N x) N* -> {N0} ceq (capp N* N0) (N N0) -> type.
%mode subst +B +X -CS.

- : subst (b/i : bracket ([x] x) i)
          N0
          (ceq/i : ceq (i @@ N0) N0).

- : subst (b/k : bracket ([x] Y) (k @@ Y))
          N0
          (ceq/k : ceq (k @@ Y @@ N0) Y).

% developing incrementally, it's useful to write down the type of each output
- : subst (b/s (B2 : bracket ([x] N2 x) N2')
               (B1 : bracket ([x] N1 x) N1')
            : bracket ([x] N1 x @@ N2 x) (s @@ N1' @@ N2'))
          N0
          (ceq/trans
              (ceq/s
                : ceq (s @@ N1' @@ N2' @@ N0) ((N1' @@ N0) @@ (N2' @@ N0)))
              (ceq/app Dceq2 Dceq1
                : ceq ((N1' @@ N0) @@ (N2' @@ N0)) (N1 N0 @@ N2 N0)))
     <- subst B1 N0 (Dceq1 : ceq (N1' @@ N0) (N1 N0))
     <- subst B2 N0 (Dceq2 : ceq (N2' @@ N0) (N2 N0)).

%worlds (ceq-block) (subst _ _ _).
%total {B} (subst B _ _).

Next, we need to know that the translation of a term is unique up to equivalence.

translate-unique : translate M N -> translate M N' -> ceq N N' -> type.
%mode translate-unique +Dt1 +Dt2 -Deq.

- : translate-unique
        (t/app (Dtrans2 : translate M2 N2)
               (Dtrans1 : translate M1 N1)
          : translate (M1 @ M2) (N1 @@ N2))
        (t/app (Dtrans2' : translate M2 N2')
               (Dtrans1' : translate M1 N1')
          : translate (M1 @ M2) (N1' @@ N2'))
        (ceq/app Dceq2 Dceq1)
     <- translate-unique Dtrans1 Dtrans1' (Dceq1 : ceq N1 N1')
     <- translate-unique Dtrans2 Dtrans2' (Dceq2 : ceq N2 N2').

- : translate-unique
        (t/lam (Dbrack : bracket ([y] N y) N*)
               ([x] [y] [dt] Dtrans x y dt : translate (M x) (N y))
          : translate (lam [x] M x) N*)
        (t/lam (Dbrack' : bracket ([y] N' y) N'*)
               ([x] [y] [dt] Dtrans' x y dt : translate (M x) (N' y))
          : translate (lam [x] M x) N'*)
        (ceq/eta ([y] (Dceq y : ceq (N* @@ y) (N y)) ;
                      (Dceqtrans y : ceq (N y) (N' y)) ;
                      (ceq/symm (Dceq' y) : ceq (N' y) (N'* @@ y))
                   : ceq (N* @@ y) (N'* @@ y))
          : ceq N* N'*)
     <- ({x} {y} {dtrans: translate x y}
         {thm-unique: translate-unique dtrans dtrans ceq/refl}
            translate-unique (Dtrans x y dtrans) (Dtrans' x y dtrans)
            (Dceqtrans y : ceq (N y) (N' y)))
     <- ({z} subst Dbrack z (Dceq z : ceq (N* @@ z) (N z)))
     <- ({z} subst Dbrack' z (Dceq' z : ceq (N'* @@ z) (N' z))).

%block unique-block
            : some {A:tp}
              block {x:term A} {y:comb A}
                    {dtrans: translate x y}
                    {thm: translate-unique dtrans dtrans ceq/refl}.

%worlds (unique-block) (translate-unique _ _ _).
%total D (translate-unique D _ _).

Then, we can prove simulation, the correctness of translation, by a straightforward induction on equality derivations in the lambda-calculus, using the correctness of bracket abstraction as a lemma in the case of a beta-reduction.

simulate' : translate M N -> translate M' N' -> teq M M' -> ceq N N' -> type.
%mode simulate' +Dt +Dt' +Deq -Dceq.

%abbrev simulate
            : teq M M' -> translate M N -> translate M' N' -> ceq N N' -> type
            = [deq] [dt] [dt'] [ceq] simulate' dt dt' deq ceq.
%%mode simulate +Deq +Dt +Dt' -Dceq.

- : simulate (eq/beta
               : teq (app (lam [x] M1 x) M2) (M1 M2))
             (t/app (Dtrans2 : translate M2 N2)
                    (t/lam
                        (Dbrack : bracket ([y] N1 y) N1*)
                        % XXX mysteriously necessary type annotations
                        ([x:term A2] [y:comb A2] [dtrans:translate x y]
                            Dtrans1 x y dtrans
                          : translate (M1 x) (N1 y)))
               : translate (app (lam [x] M1 x) M2) (capp N1* N2))
             (Dtrans3
               : translate (M1 M2) N3)
             (Dceq ; Dceq3
               : ceq (capp N1* N2) N3)
     <- subst Dbrack N2 (Dceq : ceq (capp N1* N2) (N1 N2))
     <- translate-unique (Dtrans1 M2 N2 Dtrans2) Dtrans3
                         (Dceq3 : ceq (N1 N2) N3).

- : simulate (eq/eta ([x] Deq x : teq (app M1 x) (app M2 x))
               : teq M1 M2)
             (Dtrans1 : translate M1 N1)
             (Dtrans2 : translate M2 N2)
             (ceq/eta ([y] Dceq y) : ceq N1 N2)
     <- ({x} {y} {dtrans: translate x y}
         {thm-can: can-translate x dtrans}
         {thm-unique: translate-unique dtrans dtrans ceq/refl}
         {thm-simulate: simulate eq/refl dtrans dtrans ceq/refl}
            simulate (Deq x : teq (app M1 x) (app M2 x))
                     (t/app dtrans Dtrans1 : translate (app M1 x) (capp N1 y))
                     (t/app dtrans Dtrans2 : translate (app M2 x) (capp N2 y))
                     (Dceq y : ceq (capp N1 y) (capp N2 y))).

- : simulate (eq/lam ([x] Deq x : teq (M x) (M' x))
               : teq (lam [x] M x) (lam [x] M' x))
             (t/lam (Dbrack : bracket ([y] N y) N*)
                    ([x] [y] [dtrans: translate x y] Dtrans x y dtrans
                      : translate (M x) (N y))
               : translate (lam [x] M x) N*)
             (t/lam (Dbrack' : bracket ([y] N' y) N*')
                    ([x] [y] [dtrans: translate x y] Dtrans' x y dtrans
                      : translate (M' x) (N' y))
               : translate (lam [x] M' x) N*')
             (ceq/eta ([y] (Dceq* y : ceq (N* @@ y) (N y)) ;
                           (Dceq y : ceq (N y) (N' y)) ;
                           (ceq/symm (Dceq*' y) : ceq (N' y) (N*' @@ y)))
               : ceq N* N*')
     <- ({x} {y} {dtrans: translate x y}
         {thm-can: can-translate x dtrans}
         {thm-unique: translate-unique dtrans dtrans ceq/refl}
         {thm-simulate: simulate eq/refl dtrans dtrans ceq/refl}
            simulate (Deq x : teq (M x) (M' x))
                     (Dtrans x y dtrans : translate (M x) (N y))
                     (Dtrans' x y dtrans : translate (M' x) (N' y))
                     (Dceq y : ceq (N y) (N' y)))
     <- ({y} subst Dbrack y (Dceq* y : ceq (N* @@ y) (N y)))
     <- ({y} subst Dbrack' y (Dceq*' y : ceq (N*' @@ y) (N' y))).

- : simulate (eq/app (Deq2 : teq M2 M2')
                     (Deq1 : teq M1 M1')
               : teq (M1 @ M2) (M1' @ M2'))
             (t/app (Dtrans2 : translate M2 N2)
                    (Dtrans1 : translate M1 N1)
               : translate (M1 @ M2) (N1 @@ N2))
             (t/app (Dtrans2' : translate M2' N2')
                    (Dtrans1' : translate M1' N1')
               : translate (M1' @ M2') (N1' @@ N2'))
             (ceq/app Dceq2 Dceq1
               : ceq (N1 @@ N2) (N1' @@ N2'))
     <- simulate Deq1 Dtrans1 Dtrans1' (Dceq1 : ceq N1 N1')
     <- simulate Deq2 Dtrans2 Dtrans2' (Dceq2 : ceq N2 N2').

- : simulate (eq/refl : teq M M)
             (Dtrans : translate M N)
             (Dtrans' : translate M N')
             Dceq
     <- translate-unique Dtrans Dtrans' (Dceq : ceq N N').

- : simulate (eq/symm (Deq : teq M' M) : teq M M')
             (Dtrans : translate M N)
             (Dtrans' : translate M' N')
             (ceq/symm Dceq : ceq N N')
     <- simulate Deq Dtrans' Dtrans (Dceq : ceq N' N).

- : simulate (eq/trans (Deq1 : teq M M') (Deq2 : teq M' M'') : teq M M'')
             (Dtrans : translate M N)
             (Dtrans'' : translate M'' N'')
             (ceq/trans Dceq1 Dceq2 : ceq N N'')
     <- can-translate M' (Dtrans' : translate M' N')
     <- simulate Deq1 Dtrans Dtrans' (Dceq1 : ceq N N')
     <- simulate Deq2 Dtrans' Dtrans'' (Dceq2 : ceq N' N'').

%block simulate-block
            : some {A:tp}
              block {x:term A} {y:comb A}
                    {dtrans: translate x y}
                    {thm-can: can-translate x dtrans}
                    {thm-unique: translate-unique dtrans dtrans ceq/refl}
                    {thm-simulate: simulate' dtrans dtrans eq/refl ceq/refl}.

%worlds (simulate-block) (simulate' _ _ _ _).
%total D (simulate' _ _ D _).