Skip to content
STELF
Documentation out of dateLearn more

Bracket abstraction

This is a case study translating the untyped lambda calculus into S, K, and I combinators. 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

First we define the syntax of the two languages. term is the type of untyped lambda-calculus terms; cterm is the type of untyped combinator terms.

%sort term %.
%name term %.
%term app %pi term %-> term %-> term %.
%term lam %pi (%pi term %-> term) %-> term %.
%sort cterm %.
%name cterm %.
%term s cterm %.
%term k cterm %.
%term i cterm %.
%term capp %pi cterm %-> cterm %-> cterm %.

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

%inline @ app %.
%prec %left 10 @ %.
%inline @@ capp %.
%prec %left 10 @@ %.

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.

%sort step {_ term} {_ term} %.
%term s-β 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} {_ cterm} %.
%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} {_ cterm} %.
%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 N1 cterm} {%in N1' cterm} {%in N2 cterm} {%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 N1 cterm} {%in N2 cterm} {%in N2' cterm} {%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 _ _) %.

We can now define our translation in the standard way. Bracket abstraction is represented by a judgement relating LF-level abstractions in the combinator language to closed combinator terms. This is essentially higher-order abstract syntax.

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

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') %.
% turns out that once the case is done, the types are unnecessary!
%%     <- subst B1 N0 CS1
%%     <- subst B2 N0 CS2
%%     <- cs-1* CS1 CS1'
%%     <- cs-2* CS2 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-β (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 _ _ _) %.