Documentation out of dateLearn more

POPL Tutorial/Typed bracket abstraction with equivalence

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.

%sort tp %.
%name tp %.
%term o tp %.
%term => %pi tp %-> tp %-> tp %.
%prec %right 10 => %.
%sort term {_ tp} %.
%name term %.
%% tm : type.              %name tm M x.
%% %abbrev term : tp -> type = [x] tm.
%term app %pi (term (A => B)) %-> (term A) %-> (term B) %.
%term lam %pi (%pi (term A) %-> (term B)) %-> (term (A => B)) %.
%sort comb {_ tp} %.
%name comb %.
%% cm : type.              %name cm N y.
%% %abbrev comb : tp -> type = [x] cm.
%term s comb (A => B => C => (A => B) => A => C) %.
%term k comb (A => B => A) %.
%term i comb (A => A) %.
%term capp %pi (comb (A => B)) %-> (comb A) %-> (comb B) %.

We can use STELF’s abbreviation mechanism and fixity declarations to obtain some cute syntax.

%inline @ app %.
%prec %left 10 @ %.
%inline @@ capp %.
%prec %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?)
%sort teq {_ term A} {_ term A} %.
%mode teq %star %star %.
% spurious mode declaration necessary?  see unique-block..
% beta
%term eq/beta teq (app (lam ([x] M1 x)) M2) (M1 M2) %.
% eta
%term eq/eta %pi (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
%term eq/lam %pi (teq (lam ([x] M x)) (lam ([x] M' x))) %<- ({x} teq (M x) (M' x)) %.
%term eq/app %pi (teq (app M1 M2) (app M1' M2')) %<- (teq M1 M1') %<- (teq M2 M2') %.
% equivalence
%term eq/refl teq M M %.
%term eq/symm %pi (teq M M') %<- (teq M' M) %.
%term eq/trans %pi (teq M M'') %<- (teq M' M'') %<- (teq M M') %.
%block teq-block [A tp] {x term A}%.
%worlds (teq-block) (teq _ _) %.
% definitional equality on combs
%sort ceq {_ comb A} {_ comb A} %.
% betas
%term ceq/i ceq (capp i N) N %.
%term ceq/k ceq (capp (capp k N1) N2) N1 %.
%term ceq/s ceq (capp (capp (capp s N1) N2) N3) (capp (capp N1 N3) (capp N2 N3)) %.
% eta
%term ceq/eta %pi (ceq N1 N2) %<- ({y} ceq (capp N1 y) (capp N2 y)) %.
% compatibility
%term ceq/app %pi (ceq (capp N1 N2) (capp N1' N2')) %<- (ceq N1 N1') %<- (ceq N2 N2') %.
% equivalence
%term ceq/refl ceq N N %.
%term ceq/symm %pi (ceq N N') %<- (ceq N' N) %.
%term ceq/trans %pi (ceq N N'') %<- (ceq N' N'') %<- (ceq N N') %.
%inline ; (%pi (ceq N N') %-> (ceq N' N'') %-> (ceq N N'')) [d1] [d2] ceq/trans d1 d2 %.
%prec %right 5 ; %.
%block ceq-block [A tp] {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 $[x] N$ where $N$ is a combinator term, and $x$ is a variable potentially free in $N$ . (Be careful not to confuse these brackets with STELF’s syntax for lambda abstraction.) It is defined inductively over the term $N$ :

$[x]$ $x = I$
$[x]$ $N = K$ $N$ (where $x$ not free in $N$ )
$[x]$ $N_1$ $N_2 = S$ $([x]$ $N_1)$ $([x]$ $N_2)$

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

$x^* = x$
$(M_1$ $M_2)^*$ = $M_1^*$ $M_2^*$
$(\lambda x.$ $M)^* = [x]$ $M^*$

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.

%sort translate {_ term A} {_ comb A} %.
%mode translate %in %out %.
%name translate %.
%sort bracket {_ %pi (comb A) %-> (comb B)} {_ comb (A => B)} %.
%mode bracket %in %out %.
%name bracket %.
%term t/app
  %pi (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.

%term t/lam
  %pi (translate (lam ([x] M x)) N*)
  %<- ({x term A} {y comb A} %pi (translate x y) %-> (translate (M x) (N y)))
  %<- (bracket ([y] N y) N*) %.
%term b/i bracket ([x] x) i %.
%term b/k bracket ([x] Y) (capp k Y) %.
%term b/s
  %pi (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 [A tp] {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…

%sort can-bracket {N %pi (comb A) %-> (comb B)} {_ bracket N N*} %.
%mode can-bracket %in %out %.
%sort can-translate {M term A} {_ translate M N} %.
%mode can-translate %in %out %.
%term _ can-bracket ([x] x) b/i %.
%term _ can-bracket ([x] N) b/k %.
%term _
  %pi (can-bracket ([x] capp (N1 x) (N2 x)) (b/s Dbrack2 Dbrack1))
  %<- (can-bracket ([x] N1 x) Dbrack1)
  %<- (can-bracket ([x] N2 x) Dbrack2) %.
%term _
  %pi (can-translate (app M1 M2) (t/app Dtrans2 Dtrans1))
  %<- (can-translate M1 (%the (translate M1 N1) Dtrans1))
  %<- (can-translate M2 (%the (translate M2 N2) Dtrans2)) %.
%term _
  %pi (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) (%the (translate (M x) (N y)) (Dtrans x y dtrans)))
  %<- (can-bracket ([y] N y) (%the (bracket ([y] N y) N*) Dbrack)) %.
%block can-block [A tp] {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.

%sort subst {_ bracket ([x] N x) N*} {N0} {_ ceq (capp N* N0) (N N0)} %.
%mode subst %in %in %out %.
%term _ subst (%the (bracket ([x] x) i) b/i) N0 (%the (ceq (i @@ N0) N0) ceq/i) %.
%term _ subst (%the (bracket ([x] Y) (k @@ Y)) b/k) N0 (%the (ceq (k @@ Y @@ N0) Y) ceq/k) %.
% developing incrementally, it's useful to write down the type of each output
%term _
  %pi (subst (%the (bracket ([x] N1 x @@ N2 x) (s @@ N1' @@ N2')) (b/s (%the (bracket ([x] N2 x) N2') B2) (%the (bracket ([x] N1 x) N1') B1))) N0 (ceq/trans (%the (ceq (s @@ N1' @@ N2' @@ N0) (N1' @@ N0 @@ (N2' @@ N0))) ceq/s) (%the (ceq (N1' @@ N0 @@ (N2' @@ N0)) (N1 N0 @@ N2 N0)) (ceq/app Dceq2 Dceq1))))
  %<- (subst B1 N0 (%the (ceq (N1' @@ N0) (N1 N0)) Dceq1))
  %<- (subst B2 N0 (%the (ceq (N2' @@ N0) (N2 N0)) Dceq2)) %.
%worlds (ceq-block) (subst _ _ _) %.
%total {B} (subst B _ _) %.

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

%sort translate-unique {_ translate M N} {_ translate M N'} {_ ceq N N'} %.
%mode translate-unique %in %in %out %.
%term _
  %pi (translate-unique (%the (translate (M1 @ M2) (N1 @@ N2)) (t/app (%the (translate M2 N2) Dtrans2) (%the (translate M1 N1) Dtrans1))) (%the (translate (M1 @ M2) (N1' @@ N2')) (t/app (%the (translate M2 N2') Dtrans2') (%the (translate M1 N1') Dtrans1'))) (ceq/app Dceq2 Dceq1))
  %<- (translate-unique Dtrans1 Dtrans1' (%the (ceq N1 N1') Dceq1))
  %<- (translate-unique Dtrans2 Dtrans2' (%the (ceq N2 N2') Dceq2)) %.
%term _
  %pi (translate-unique (%the (translate (lam ([x] M x)) N*) (t/lam (%the (bracket ([y] N y) N*) Dbrack) ([x] [y] [dt] %the (translate (M x) (N y)) (Dtrans x y dt)))) (%the (translate (lam ([x] M x)) N'*) (t/lam (%the (bracket ([y] N' y) N'*) Dbrack') ([x] [y] [dt] %the (translate (M x) (N' y)) (Dtrans' x y dt)))) (%the (ceq N* N'*) (ceq/eta ([y] %the (ceq (N* @@ y) (N'* @@ y)) ((%the (ceq (N* @@ y) (N y)) (Dceq y)) ; (%the (ceq (N y) (N' y)) (Dceqtrans y)) ; (%the (ceq (N' y) (N'* @@ y)) (ceq/symm (Dceq' y))))))))
  %<- ({x} {y} {dtrans translate x y} {thm-unique translate-unique dtrans dtrans ceq/refl} translate-unique (Dtrans x y dtrans) (Dtrans' x y dtrans) (%the (ceq (N y) (N' y)) (Dceqtrans y)))
  %<- ({z} subst Dbrack z (%the (ceq (N* @@ z) (N z)) (Dceq z)))
  %<- ({z} subst Dbrack' z (%the (ceq (N'* @@ z) (N' z)) (Dceq' z))) %.
%block unique-block [A tp] {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.

%sort simulate' {_ translate M N} {_ translate M' N'} {_ teq M M'} {_ ceq N N'} %.
%mode simulate' %in %in %in %out %.
%inline simulate (%pi (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.
%term _
  %pi (simulate (%the (teq (app (lam ([x] M1 x)) M2) (M1 M2)) eq/beta) (%the (translate (app (lam ([x] M1 x)) M2) (capp N1* N2)) (t/app (%the (translate M2 N2) Dtrans2) (t/lam (%the (bracket ([y] N1 y) N1*) Dbrack) ([x term A2] [y comb A2] [dtrans translate x y] %the (translate (M1 x) (N1 y)) (Dtrans1 x y dtrans))))) (%the (translate (M1 M2) N3) Dtrans3) (%the (ceq (capp N1* N2) N3) (Dceq ; Dceq3)))
  %<- (subst Dbrack N2 (%the (ceq (capp N1* N2) (N1 N2)) Dceq))
  %<- (translate-unique (Dtrans1 M2 N2 Dtrans2) Dtrans3 (%the (ceq (N1 N2) N3) Dceq3)) %.
%term _
  %pi (simulate (%the (teq M1 M2) (eq/eta ([x] %the (teq (app M1 x) (app M2 x)) (Deq x)))) (%the (translate M1 N1) Dtrans1) (%the (translate M2 N2) Dtrans2) (%the (ceq N1 N2) (ceq/eta ([y] Dceq y))))
  %<- ({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 (%the (teq (app M1 x) (app M2 x)) (Deq x)) (%the (translate (app M1 x) (capp N1 y)) (t/app dtrans Dtrans1)) (%the (translate (app M2 x) (capp N2 y)) (t/app dtrans Dtrans2)) (%the (ceq (capp N1 y) (capp N2 y)) (Dceq y))) %.
%term _
  %pi (simulate (%the (teq (lam ([x] M x)) (lam ([x] M' x))) (eq/lam ([x] %the (teq (M x) (M' x)) (Deq x)))) (%the (translate (lam ([x] M x)) N*) (t/lam (%the (bracket ([y] N y) N*) Dbrack) ([x] [y] [dtrans translate x y] %the (translate (M x) (N y)) (Dtrans x y dtrans)))) (%the (translate (lam ([x] M' x)) N*') (t/lam (%the (bracket ([y] N' y) N*') Dbrack') ([x] [y] [dtrans translate x y] %the (translate (M' x) (N' y)) (Dtrans' x y dtrans)))) (%the (ceq N* N*') (ceq/eta ([y] (%the (ceq (N* @@ y) (N y)) (Dceq* y)) ; (%the (ceq (N y) (N' y)) (Dceq y)) ; (%the (ceq (N' y) (N*' @@ y)) (ceq/symm (Dceq*' y)))))))
  %<- ({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 (%the (teq (M x) (M' x)) (Deq x)) (%the (translate (M x) (N y)) (Dtrans x y dtrans)) (%the (translate (M' x) (N' y)) (Dtrans' x y dtrans)) (%the (ceq (N y) (N' y)) (Dceq y)))
  %<- ({y} subst Dbrack y (%the (ceq (N* @@ y) (N y)) (Dceq* y)))
  %<- ({y} subst Dbrack' y (%the (ceq (N*' @@ y) (N' y)) (Dceq*' y))) %.
%term _
  %pi (simulate (%the (teq (M1 @ M2) (M1' @ M2')) (eq/app (%the (teq M2 M2') Deq2) (%the (teq M1 M1') Deq1))) (%the (translate (M1 @ M2) (N1 @@ N2)) (t/app (%the (translate M2 N2) Dtrans2) (%the (translate M1 N1) Dtrans1))) (%the (translate (M1' @ M2') (N1' @@ N2')) (t/app (%the (translate M2' N2') Dtrans2') (%the (translate M1' N1') Dtrans1'))) (%the (ceq (N1 @@ N2) (N1' @@ N2')) (ceq/app Dceq2 Dceq1)))
  %<- (simulate Deq1 Dtrans1 Dtrans1' (%the (ceq N1 N1') Dceq1))
  %<- (simulate Deq2 Dtrans2 Dtrans2' (%the (ceq N2 N2') Dceq2)) %.
%term _
  %pi (simulate (%the (teq M M) eq/refl) (%the (translate M N) Dtrans) (%the (translate M N') Dtrans') Dceq)
  %<- (translate-unique Dtrans Dtrans' (%the (ceq N N') Dceq)) %.
%term _
  %pi (simulate (%the (teq M M') (eq/symm (%the (teq M' M) Deq))) (%the (translate M N) Dtrans) (%the (translate M' N') Dtrans') (%the (ceq N N') (ceq/symm Dceq)))
  %<- (simulate Deq Dtrans' Dtrans (%the (ceq N' N) Dceq)) %.
%term _
  %pi (simulate (%the (teq M M'') (eq/trans (%the (teq M M') Deq1) (%the (teq M' M'') Deq2))) (%the (translate M N) Dtrans) (%the (translate M'' N'') Dtrans'') (%the (ceq N N'') (ceq/trans Dceq1 Dceq2)))
  %<- (can-translate M' (%the (translate M' N') Dtrans'))
  %<- (simulate Deq1 Dtrans Dtrans' (%the (ceq N N') Dceq1))
  %<- (simulate Deq2 Dtrans' Dtrans'' (%the (ceq N' N'') Dceq2)) %.
%block simulate-block [A tp] {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 _) %.