POPL Tutorial/Typed bracket abstraction (solution)

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 term steps to a reduct, its translation multi-steps to its reduct’s translation.

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; cterm 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 %.
%term i tp %.
%term => %pi tp %-> tp %-> tp %.
%prec %right 10 => %.
%sort term {_ tp} %.
%name term %.
%term app %pi (term (A => B)) %-> (term A) %-> (term B) %.
%term lam %pi (%pi (term A) %-> (term B)) %-> (term (A => B)) %.
%sort cterm {_ tp} %.
%name cterm %.
%term s cterm (A => B => C => (A => B) => A => C) %.
%term k cterm (A => B => A) %.
%term i cterm (A => A) %.
%term capp %pi (cterm (A => B)) %-> (cterm A) %-> (cterm 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 @@ %.

Dynamic semantics

Then we define reduction relations on both languages. step is the single-step reduction relation on lambda terms; cstep is the single-step reduction relation on combinator terms. For lambda-calculus terms, we do not reduce under binders.

%sort step {_ term A} {_ term A} %.
%term s-beta step (app (lam ([x] M1 x)) M2) (M1 M2) %.
%term s-1 %pi (step (app M1 M2) (app M1' M2)) %<- (step M1 M1') %.
%term s-2 %pi (step (app M1 M2) (app M1 M2')) %<- (step M2 M2') %.
%sort cstep {_ cterm A} {_ cterm A} %.
%term cs-i cstep (capp i X) X %.
%term cs-k cstep (capp (capp k X) Y) X %.
%term cs-s cstep (capp (capp (capp s X) Y) Z) (capp (capp X Z) (capp Y Z)) %.
%term cs-1 %pi (cstep (capp X Y) (capp X' Y)) %<- (cstep X X') %.
%term cs-2 %pi (cstep (capp X Y) (capp X Y')) %<- (cstep Y Y') %.

We also define multi-step reduction on combinator terms.

Our simulation will relate single-step derivations in the lambda-calculus to multi-step derivations on the translated terms.

%sort cstep* {_ cterm A} {_ cterm A} %.
%term cs-cons %pi (cstep* N N'') %<- (cstep N N') %<- (cstep* N' N'') %.
%term cs-nil cstep* N N %.

We can pre-emptively prove some compatibility lemmas about multi-step reduction.

%sort cs-1* {_ cstep* N1 N1'} {_ cstep* (capp N1 N2) (capp N1' N2)} %.
%mode {%in A tp} {%in B tp} {%in N1 cterm (A => B)} {%in N1' cterm (A => B)} {%in N2 cterm A} {%in CS1 cstep* N1 N1'} {%out CS2 cstep* (capp N1 N2) (capp N1' N2)} cs-1* CS1 CS2 %.
%term _ cs-1* cs-nil cs-nil %.
%term _ %pi (cs-1* (cs-cons CS C) (cs-cons CS' (cs-1 C))) %<- (cs-1* CS CS') %.
%worlds () (cs-1* _ _) %.
%total {CS} (cs-1* CS _) %.
%sort cs-2* {_ cstep* N2 N2'} {_ cstep* (capp N1 N2) (capp N1 N2')} %.
%mode {%in A tp} {%in B tp} {%in N1 cterm (A => B)} {%in N2 cterm A} {%in N2' cterm A} {%in CS1 cstep* N2 N2'} {%out CS2 cstep* (capp N1 N2) (capp N1 N2')} cs-2* CS1 CS2 %.
%term _ cs-2* cs-nil cs-nil %.
%term _ %pi (cs-2* (cs-cons CS C) (cs-cons CS' (cs-2 C))) %<- (cs-2* CS CS') %.
%worlds () (cs-2* _ _) %.
%total {CS} (cs-2* CS _) %.
%sort cs-trans {_ cstep* N1 N2} {_ cstep* N2 N3} {_ cstep* N1 N3} %.
%mode cs-trans %in %in %out %.
%term _ cs-trans cs-nil Cs2 Cs2 %.
%term _ %pi (cs-trans (cs-cons Cs1 C) Cs2 (cs-cons Cs12 C)) %<- (cs-trans Cs1 Cs2 Cs12) %.
%worlds () (cs-trans _ _ _) %.
%total {Cs} (cs-trans Cs _ _) %.

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) trans 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 trans {_ term A} {_ cterm A} %.
%sort bracket {_ %pi (cterm A) %-> (cterm B)} {_ cterm (A => B)} %.
%term t-app %pi (trans (app M1 M2) (capp N1 N2)) %<- (trans M1 N1) %<- (trans 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 (trans (lam ([x] M x)) N')
  %<- ({x term A} {y cterm A} %pi (trans x y) %-> (trans (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 tbind [A tp] {x term A} {y cterm A} {dtrans trans x y}%.
%worlds (tbind) (bracket _ _) %.
%worlds (tbind) (trans _ _) %.

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} {_ cstep* (capp N' N0) (N N0)} %.
%mode subst %in %in %out %.
%term _ subst b-i N0 (cs-cons cs-nil cs-i) %.
%term _ subst b-k N0 (cs-cons cs-nil cs-k) %.
% developing incrementally, it's useful to write down the type of each output
%term _
  %pi (subst (b-s (%the (bracket ([x] N2 x) N2') B2) (%the (bracket ([x] N1 x) N1') B1)) N0 (cs-cons CS12' cs-s))
  %<- (subst B1 N0 (%the (cstep* (N1' @@ N0) (N1 N0)) CS1))
  %<- (subst B2 N0 (%the (cstep* (N2' @@ N0) (N2 N0)) CS2))
  %<- (cs-1* CS1 (%the (cstep* (N1' @@ N0 @@ (N2' @@ N0)) (N1 N0 @@ (N2' @@ N0))) CS1'))
  %<- (cs-2* CS2 (%the (cstep* (N1 N0 @@ (N2' @@ N0)) (N1 N0 @@ N2 N0)) CS2'))
  %<- (cs-trans CS1' CS2' CS12') %.
%worlds () (subst _ _ _) %.
%total {B} (subst B _ _) %.

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

%sort simulate {_ step M M'} {_ trans M N} {_ trans M' N'} {_ cstep* N N'} %.
%mode simulate %in %in %out %out %.

NB: in this step, on paper, you have to prove two compositionality lemmas. in STELF, using higher-order abstract syntax, we get them for free — see (T1 _ _ T2) output.

%term _
  %pi (simulate s-beta (t-app T2 (t-lam B1 T1)) (T1 _ _ T2) CS)
  %<- (subst B1 N2 CS) %.
%term _
  %pi (simulate (s-1 S1) (t-app T2 T1) (t-app T2 T1') CSapp)
  %<- (simulate S1 T1 T1' CS1)
  %<- (cs-1* CS1 CSapp) %.
%term _
  %pi (simulate (s-2 S2) (t-app T2 T1) (t-app T2' T1) CSapp)
  %<- (simulate S2 T2 T2' CS2)
  %<- (cs-2* CS2 CSapp) %.
%worlds () (simulate _ _ _ _) %.
%total D (simulate D _ _ _) %.