Typed combinators soundness and completeness

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-typed lambda calculus into the SKI combinator calculus. 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, and vice versa.

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.

By working over intrinsically typed terms, we can regard our theorems as theorems comparing a natural deduction presentation of propositional logic with a Hilbert-style axiomatic presentation, but none of the theorems depend on types, and would hold equally well of untyped terms.

tp : type.              %name tp A a.

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


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

%%% uncomment for untyped version:
%% 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.

%%% uncomment for untyped version:
%% 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 specify convenient infix syntax for application.

%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
teq : term A -> term A -> type.

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

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

% 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'.

Infix syntax for transitivity is convenient when building derivations.

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

%block term-block : some {A:tp} block {x:term A}.
%worlds (term-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/ext : 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 comb-block : some {A:tp} block {y:comb A}.
%worlds (comb-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. (The block trans-block will form the basis of later blocks.)

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 ([y] y) i.

b/k : bracket ([y] N) (capp k N).

b/s : bracket ([y] capp (N1 y) (N2 y)) (capp (capp s N1*) N2*)
       <- bracket ([y] N1 y) N1*
       <- bracket ([y] N2 y) 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 explicitly prove effectiveness lemmas.

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 is equivalent 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 (comb-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] [dtrans] 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] Dtrans' x y dtrans : translate (M x) (N' y))
          : translate (lam [x] M x) N'*)
        (ceq/ext ([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.

- : simulate (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)
             (eq/beta
               : teq (app (lam [x] M1 x) M2) (M1 M2))
             (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 (Dtrans1 : translate M1 N1)
             (Dtrans2 : translate M2 N2)
             (eq/ext ([x] Deq x : teq (app M1 x) (app M2 x))
               : teq M1 M2)
             (ceq/ext ([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}
            simulate (t/app dtrans Dtrans1 : translate (app M1 x) (capp N1 y))
                     (t/app dtrans Dtrans2 : translate (app M2 x) (capp N2 y))
                     (Deq x : teq (app M1 x) (app M2 x))
                     (Dceq y : ceq (capp N1 y) (capp N2 y))).

- : simulate (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*')
             (eq/lam ([x] Deq x : teq (M x) (M' x))
               : teq (lam [x] M x) (lam [x] M' x))
             (ceq/ext ([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}
            simulate (Dtrans x y dtrans : translate (M x) (N y))
                     (Dtrans' x y dtrans : translate (M' x) (N' y))
                     (Deq x : teq (M x) (M' x))
                     (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 (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'))
             (eq/app (Deq2 : teq M2 M2')
                     (Deq1 : teq M1 M1')
               : teq (M1 @ M2) (M1' @ M2'))
             (ceq/app Dceq2 Dceq1
               : ceq (N1 @@ N2) (N1' @@ N2'))
     <- simulate Dtrans1 Dtrans1' Deq1 (Dceq1 : ceq N1 N1')
     <- simulate Dtrans2 Dtrans2' Deq2 (Dceq2 : ceq N2 N2').

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

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

- : simulate (Dtrans : translate M N)
             (Dtrans'' : translate M'' N'')
             (eq/trans (Deq1 : teq M M') (Deq2 : teq M' M'') : teq M M'')
             (ceq/trans Dceq1 Dceq2 : ceq N N'')
     <- can-translate M' (Dtrans' : translate M' N')
     <- simulate Dtrans Dtrans' Deq1 (Dceq1 : ceq N N')
     <- simulate Dtrans' Dtrans'' Deq2 (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}.

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

Backward translation

To show completeness we exhibit a backward translation---called "reification"---taking combinators to lambda terms, and show that for every translation, there is a reification to a term equivalent to the original input term.

Reification just replaces combinators with their definitions as lambda terms.

reify : comb A -> term A -> type.       %name reify Dreify dreify.
%mode reify +N -M.

r/s : reify s (lam [x] lam [y] lam [z] x @ z @ (y @ z)).
r/k : reify k (lam [x] lam [y] x).
r/i : reify i (lam [x] x).

r/capp : reify (N1 @@ N2) (M1 @ M2)
          <- reify N1 M1
          <- reify N2 M2.

We consider reification in any world with free variables as long as there's a combinator variable for each lambda-term variable and an appropriate correspondence between them.

%block reify-block
            : some {A:tp}
              block {x:term A} {y:comb A} {dreify: reify y x}.

%worlds (reify-block) (reify _ _).

Twelf can verify that reification is total and that the result is unique up to identity,

%total N (reify N _).
%unique reify +N -M.

but in order to use these facts in other metatheorems, we must prove them ourselves.

The theorem can-reify shows the effectiveness of reification by constructing a reify derivation for any given combinator N.

can-reify : {N : comb A} reify N M -> type.
%mode can-reify +N -Dreify.

- : can-reify s r/s.
- : can-reify k r/k.
- : can-reify i r/i.
- : can-reify (capp N1 N2) (r/capp Dreify2 Dreify1)
     <- can-reify N1 Dreify1
     <- can-reify N2 Dreify2.

Note the use of a theorem case in the block for can-reify: since we prove reification with respect to an open world, we have to include proofs for the free variable cases.

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

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

The theorem reify-unique shows the uniqueness of reification. For convenience, we demonstrate only that reifications are unique up to term equivalence.

reify-unique : reify N M -> reify N M' -> teq M M' -> type.
%mode reify-unique +Dreify1 +Dreify2 -Deq.

- : reify-unique r/i r/i eq/refl.
- : reify-unique r/k r/k eq/refl.
- : reify-unique r/s r/s eq/refl.
- : reify-unique (r/capp Dreify2 Dreify1)
                 (r/capp Dreify2' Dreify1')
                 (eq/app Deq2 Deq1)
     <- reify-unique Dreify1 Dreify1' Deq1
     <- reify-unique Dreify2 Dreify2' Deq2.

%block reify-unique-block
            : some {A:tp}
              block {x:term A} {y:comb A} {dreify: reify y x}
                    {thm: reify-unique dreify dreify eq/refl}.

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

The reification of a closed combinator term is a closed lambda-term, but we require the following strengthening lemma to show that this is the case.

strengthen-reify : ({x} {y} reify y x -> reify N (M! x))
                    %%
                    -> reify N M
                    -> ({x} teq M (M! x))
                    -> type.
%mode strengthen-reify +Dreify! -Dreify -Deq.

- : strengthen-reify ([x] [y] [dreify: reify y x] r/s) r/s ([x] eq/refl).
- : strengthen-reify ([x] [y] [dreify: reify y x] r/k) r/k ([x] eq/refl).
- : strengthen-reify ([x] [y] [dreify: reify y x] r/i) r/i ([x] eq/refl).

- : strengthen-reify ([x] [y] [dreify: reify y x]
                         r/capp (Dreify2! x y dreify : reify N2 (M2! x))
                                (Dreify1! x y dreify : reify N1 (M1! x))
                       : reify (N1 @@ N2) ((M1! x) @ (M2! x)))
                     (r/capp Dreify2 Dreify1)
                     ([x] eq/app (Deq2 x) (Deq1 x))
     <- strengthen-reify ([x] [y] [dreify] Dreify1! x y dreify)
                         (Dreify1 : reify N1 M1)
                         ([x] Deq1 x : teq M1 (M1! x))
     <- strengthen-reify ([x] [y] [dreify] Dreify2! x y dreify)
                         (Dreify2 : reify N2 M2)
                         ([x] Deq2 x : teq M2 (M2! x)).

%block strengthen-reify-block
            : some {A:tp}
              block {x:term A} {y:comb A} {dreify: reify y x}
                    {thm: {B:tp} strengthen-reify
                                   ([x1:term B] [y1:comb B] [dreify1] dreify)
                                   dreify
                                   ([x1] eq/refl)}.

%worlds (strengthen-reify-block) (strengthen-reify _ _ _).
%total D (strengthen-reify D _ _).

Correctness of the backward translation

Our main technique for showing completeness is to show that every translation of M has a reification to an equivalent M'. First, we show the following lemma, which says that bracket abstractions reify to lambda abstractions.

bracket-reify : bracket ([y] N y) N*
                 -> ({x} {y} reify y x -> reify (N y) (M x))
                 %%
                 -> reify N* M*
                 -> teq M* (lam [x] M x)
                 -> type.
%mode bracket-reify +Dbrack +Dreify -Dreify* -Deq*.

- : bracket-reify (b/i : bracket ([y] y) i)
                  ([x] [y] [dreify: reify y x] dreify)
                  (r/i : reify i (lam [x] x))
                  (eq/refl : teq (lam [x] x) (lam [x] x)).

In the case where bracket abstraction returns an application of the K combinator to a closed term, we require our strengthening lemma to show that the result of reification is also closed.

- : bracket-reify (b/k : bracket ([y] N) (k @@ N))
                  ([x] [y] [dreify: reify y x]
                      Dreify! x y dreify : reify N (M! x))
                  (r/capp Dreify r/k
                    : reify (k @@ N) ((lam [x] lam [y] x) @ M))
                  (eq/beta ; eq/lam ([x] Deq x)
                    : teq ((lam [x] lam [y] x) @ M) (lam [y] M! y))
     <- strengthen-reify
            ([x] [y] [dreify: reify y x] Dreify! x y dreify)
            (Dreify : reify N M)
            ([x] Deq x : teq M (M! x)).

The case for reifying an application of the S combinator is tedious, but straightforward.

- : bracket-reify (b/s (Dbrack2 : bracket ([y] N2 y) N2*)
                       (Dbrack1 : bracket ([y] N1 y) N1*)
                    : bracket ([y] (N1 y) @@ (N2 y)) (s @@ N1* @@ N2*))
                  ([x] [y] [dreify: reify y x]
                      r/capp (Dreify2 x y dreify : reify (N2 y) (M2 x))
                             (Dreify1 x y dreify : reify (N1 y) (M1 x))
                       : reify ((N1 y) @@ (N2 y)) ((M1 x) @ (M2 x)))
                  (r/capp (Dreify2* : reify N2* M2*)
                    (r/capp (Dreify1* : reify N1* M1*)
                            (r/s))
                    : reify (s @@ N1* @@ N2*)
                            ( (lam [x] lam [y] lam [z] x @ z @ (y @ z))
                              @ M1* @ M2*) )
                  (% reduce first redex
                   eq/app
                      (eq/refl : teq M2* M2*)
                      eq/beta
                    ;
                   % reduce second redex
                   eq/beta
                    ;
                   % descend under lambda
                   eq/lam ([x] eq/app
                                (eq/app (eq/refl : teq x x) Deq2* ; eq/beta
                                  : teq (M2* @ x) (M2 x))
                                (eq/app (eq/refl : teq x x) Deq1* ; eq/beta
                                  : teq (M1* @ x) (M1 x)))
                    : teq ( (lam[x] lam[y] lam[z] x @ z @ (y @ z)) @ M1* @ M2* )
                          (lam [z] (M1 z) @ (M2 z)))
     <- bracket-reify Dbrack1 ([x] [y] [dreify: reify y x] Dreify1 x y dreify)
            (Dreify1* : reify N1* M1*)
            (Deq1* : teq M1* (lam [z] M1 z))
     <- bracket-reify Dbrack2 ([x] [y] [dreify: reify y x] Dreify2 x y dreify)
            (Dreify2* : reify N2* M2*)
            (Deq2* : teq M2* (lam [z] M2 z)).

%worlds (strengthen-reify-block) (bracket-reify _ _ _ _).
%total D (bracket-reify D _ _ _).

Now we can prove that every translation reifies to an equivalent term, appealing to the above bracket abstraction lemma in the lam case.

translate-reify : translate M N -> reify N M' -> teq M M' -> type.
%mode translate-reify +Dt -Dr -Deq.

- : translate-reify
        (t/app (Dtrans2 : translate M2 N2)
               (Dtrans1 : translate M1 N1)
          : translate (M1 @ M2) (N1 @@ N2))
        (r/capp (Dreify2 : reify N2 M2')
                (Dreify1 : reify N1 M1')
          : reify (N1 @@ N2) (M1' @ M2'))
        (eq/app Deq2 Deq1
          : teq (M1 @ M2) (M1' @ M2'))
     <- translate-reify Dtrans1 Dreify1 (Deq1 : teq M1 M1')
     <- translate-reify Dtrans2 Dreify2 (Deq2 : teq M2 M2').

- : translate-reify
        (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*)
        (Dreify* : reify N* M*)
        (eq/lam ([x] Deq x) ; eq/symm Deq*
          : teq (lam [x] M x) M*)
     <- ({x} {y} {dtrans: translate x y} {dreify: reify y x}
         {thm-closed: {B} strengthen-reify
                            ([x1:term B] [y1:comb B] [dreify1] dreify)
                            dreify
                            ([x1] eq/refl)}
         {thm-translate: translate-reify dtrans dreify eq/refl}
            translate-reify
            (Dtrans x y dtrans)
            (Dreify x y dreify : reify (N y) (M0 x))
            (Deq x : teq (M x) (M0 x)))
     <- bracket-reify
            Dbrack
            ([x] [y] [dreify] Dreify x y dreify)
            (Dreify* : reify N* M*)
            (Deq* : teq M* (lam [x] M0 x)).

%block translate-reify-block
            : some {A:tp}
              block {x:term A} {y:comb A}
                    {dtrans: translate x y} {dreify: reify y x}
                    {thm-closed: {B:tp}
                                 strengthen-reify
                                   ([x1:term B] [y1:comb B] [dreify1] dreify)
                                   dreify
                                   ([x1] eq/refl)}
                    {thm-translate: translate-reify dtrans dreify eq/refl}.

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

Next, we prove a theorem similar to our earlier simulate theorem, but for reification: given two reification derivations from equivalent inputs, their outputs are equivalent.

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

- : reify-simulate (r/capp (Dreify : reify N M) r/i
                     : reify (i @@ N) ((lam [x] x) @ M))
                   (Dreify' : reify N M')
                   (ceq/i : ceq (i @@ N) N)
                   (eq/beta ; Deq : teq ((lam [x] x) @ M) M')
     <- reify-unique Dreify Dreify' (Deq : teq M M').

- : reify-simulate (r/capp (Dreify2 : reify N2 M2)
                      (r/capp (Dreify1 : reify N1 M1)
                               r/k)
                     : reify (k @@ N1 @@ N2) ((lam [x] lam [y] x) @ M1 @ M2))
                   (Dreify' : reify N1 M')
                   (ceq/k : ceq (k @@ N1 @@ N2) N1)
                   (eq/app eq/refl eq/beta ; eq/beta ; Deq
                     : teq ((lam [x] lam [y] x) @ M1 @ M2) M')
     <- reify-unique Dreify1 Dreify' (Deq : teq M1 M').

- : reify-simulate (r/capp (Dreify3 : reify N3 M3)
                      (r/capp (Dreify2 : reify N2 M2)
                      (r/capp (Dreify1 : reify N1 M1)
                      r/s))
                     : reify (s @@ N1 @@ N2 @@ N3)
                             ( (lam [x] lam [y] lam [z] x @ z @ (y @ z))
                               @ M1 @ M2 @ M3 ))
                   (r/capp
                       (r/capp (Dreify3' : reify N3 M3')
                               (Dreify2' : reify N2 M2'))
                       (r/capp (Dreify3'' : reify N3 M3'')
                               (Dreify1' : reify N1 M1'))
                     : reify (N1 @@ N3 @@ (N2 @@ N3)) (M1' @ M3'' @ (M2' @ M3')))
                   (ceq/s : ceq (s @@ N1 @@ N2 @@ N3) (N1 @@ N3 @@ (N2 @@ N3)))
                   (eq/app eq/refl (eq/app eq/refl eq/beta) ;
                    eq/app eq/refl eq/beta ;
                    eq/beta ;
                    eq/app (eq/app Deq3 Deq2)
                           (eq/app Deq3' Deq1)
                     : teq ( (lam [x] lam [y] lam [z] x @ z @ (y @ z))
                             @ M1 @ M2 @ M3 )
                           (M1' @ M3'' @ (M2' @ M3')))
     <- reify-unique Dreify1 Dreify1' (Deq1 : teq M1 M1')
     <- reify-unique Dreify2 Dreify2' (Deq2 : teq M2 M2')
     <- reify-unique Dreify3 Dreify3' (Deq3 : teq M3 M3')
     <- reify-unique Dreify3 Dreify3'' (Deq3' : teq M3 M3'').

- : reify-simulate (Dreify1 : reify N1 M1)
                   (Dreify2 : reify N2 M2)
                   (ceq/ext ([y] Dceq y : ceq (N1 @@ y) (N2 @@ y))
                     : ceq N1 N2)
                   (eq/ext ([x] Deq x : teq (M1 @ x) (M2 @ x))
                     : teq M1 M2)
     <- ({x} {y} {dreify: reify y x}
         {thm-can: can-reify y dreify}
         {thm-unique: reify-unique dreify dreify eq/refl}
            reify-simulate
                (r/capp dreify Dreify1 : reify (N1 @@ y) (M1 @ x))
                (r/capp dreify Dreify2 : reify (N2 @@ y) (M2 @ x))
                (Dceq y)
                (Deq x : teq (M1 @ x) (M2 @ x))).

- : reify-simulate (r/capp (Dreify2 : reify N2 M2)
                           (Dreify1 : reify N1 M1)
                     : reify (N1 @@ N2) (M1 @ M2))
                   (r/capp (Dreify2' : reify N2' M2')
                           (Dreify1' : reify N1' M1')
                     : reify (N1' @@ N2') (M1' @ M2'))
                   (ceq/app (Dceq2 : ceq N2 N2')
                            (Dceq1 : ceq N1 N1')
                     : ceq (N1 @@ N2) (N1' @@ N2'))
                   (eq/app Deq2 Deq1
                     : teq (M1 @ M2) (M1' @ M2'))
     <- reify-simulate Dreify1 Dreify1' Dceq1 (Deq1 : teq M1 M1')
     <- reify-simulate Dreify2 Dreify2' Dceq2 (Deq2 : teq M2 M2').

- : reify-simulate (Dreify : reify N M)
                   (Dreify' : reify N M')
                   (ceq/refl : ceq N N)
                   (Deq : teq M M')
     <- reify-unique Dreify Dreify' (Deq : teq M M').

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

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

%block reify-simulate-block
            : some {A:tp}
              block {x:term A} {y:comb A} {dreify: reify y x}
                    {thm-can: can-reify y dreify}
                    {thm-unique: reify-unique dreify dreify eq/refl}.

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

Finally, we can now prove the translation complete: every combinator equivalence hit by the translation comes from a lambda-calculus equivalence.

Given two translations, we get reifications for both. By the above simulation theorem, we show that the reifications must be equal. Then the desired result follows by transitivity.

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

- : complete (Dtrans : translate M N)
             (Dtrans' : translate M' N')
             (Dceq : ceq N N')
             (Deq ; Deq0 ; eq/symm Deq' : teq M M')
     <- translate-reify Dtrans (Dreify : reify N M0) (Deq : teq M M0)
     <- translate-reify Dtrans' (Dreify' : reify N' M0') (Deq' : teq M' M0')
     <- reify-simulate Dreify Dreify' Dceq (Deq0 : teq M0 M0').

We can also make a copy of simulate called sound, in order to be able check it in the same world as complete.

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

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

We can make a master-block in which each of soundness and completeness hold. Terms under translation can have any free variables x, as long as they are matched by free combinator variables y such that x translates to y and y reifies to x. The other variables in the block are theorem cases relating to these new translation and reification assumptions.

Note that for world subsumption to work correctly, it was necessary to always state x and y in the same order, even in the reification theorems.

%block master-block
            : some {A:tp}
              block {x:term A} {y:comb A}
                    {dtrans: translate x y}
                      {thm-can-tr: can-translate x dtrans}
                      {thm-tr-unique: translate-unique dtrans dtrans ceq/refl}
                    {dreify: reify y x}
                      {thm-can-re: can-reify y dreify}
                      {thm-re-unique: reify-unique dreify dreify eq/refl}
                      {thm-re-closed: {B:tp}
                                 strengthen-reify
                                   ([x1:term B] [y1:comb B] [dreify1] dreify)
                                   dreify
                                   ([x1] eq/refl)}
                      {thm-tr-re: translate-reify dtrans dreify eq/refl}.

%worlds (master-block) (complete _ _ _ _).
%total {} (complete _ _ _ _).

%worlds (master-block) (sound _ _ _ _).
%total {} (sound _ _ _ _).