POPL Tutorial/Combinators session (answers)

Adapted from the case study on Typed combinators soundness and completeness.

Syntax

% lambda calculus
%sort term %.
%name term %.
%term app %pi term %-> term %-> term %.
%term lam %pi (%pi term %-> term) %-> term %.
% combinator calculus
%sort comb %.
%name comb %.
%term s comb %.
%term k comb %.
%term i comb %.
%term capp %pi comb %-> comb %-> comb %.

Translation

% bracket abstraction
%sort bracket {_ %pi comb %-> comb} {_ comb} %.
%mode bracket %in %out %.
%term bracket/var bracket ([y] y) i %.
%term bracket/i bracket ([y] i) (capp k i) %.
%term bracket/k bracket ([y] k) (capp k k) %.
%term bracket/s bracket ([y] s) (capp k s) %.
%term bracket/app
  %pi (bracket ([y] capp (A y) (B y)) (capp (capp s A') B'))
  %<- (bracket ([y] A y) A')
  %<- (bracket ([y] B y) B') %.
%block bracket-block {y comb} {bracket/y bracket ([z] y) (capp k y)}%.
%worlds (bracket-block) (bracket _ _) %.
%total A (bracket A _) %.
% translation
%sort translate {_ term} {_ comb} %.
%mode translate %in %out %.
%term translate/app %pi (translate (app M N) (capp A B)) %<- (translate M A) %<- (translate N B) %.
%term translate/lam
  %pi (translate (lam ([x] M x)) A')
  %<- ({x} {y} %pi (bracket ([z] y) (capp k y)) %-> (translate x y) %-> (translate (M x) (A y)))
  %<- (bracket ([y] A y) A') %.
%block translate-block {x term} {y comb} {bracket/y bracket ([z] y) (capp k y)} {translate/x translate x y}%.
%worlds (translate-block) (translate _ _) %.
%total M (translate M _) %.

Equational theory

% lambda term equality
%sort teq {_ term} {_ term} %.
% beta
%term teq/beta teq (app (lam ([x] M x)) N) (M N) %.
% extensionality (eta)
%term teq/ext %pi (teq M M') %<- ({x term} teq (app M x) (app M' x)) %.
% compatibilities
%term teq/app %pi (teq (app M N) (app M' N')) %<- (teq M M') %<- (teq N N') %.
%term teq/lam %pi (teq (lam ([x] M x)) (lam ([x] M' x))) %<- ({x term} teq (M x) (M' x)) %.
% equivalence
%term teq/refl teq M M %.
%term teq/symm %pi (teq M M') %<- (teq M' M) %.
%term teq/trans %pi (teq M M') %<- (teq M N) %<- (teq N M') %.
%block term-block {x term}%.
%worlds (term-block) (teq _ _) %.
% combinator equality
%sort ceq {_ comb} {_ comb} %.
% betas
%term ceq/i ceq (capp i A) A %.
%term ceq/k ceq (capp (capp k A) _) A %.
%term ceq/s ceq (capp (capp (capp s A) B) C) (capp (capp A C) (capp B C)) %.
% extensionality
%term ceq/ext %pi (ceq A A') %<- ({y comb} ceq (capp A y) (capp A' y)) %.
% compatibility
%term ceq/app %pi (ceq (capp A B) (capp A' B')) %<- (ceq A A') %<- (ceq B B') %.
% equivalence
%term ceq/refl ceq A A %.
%term ceq/symm %pi (ceq A A') %<- (ceq A' A) %.
%term ceq/trans %pi (ceq A A') %<- (ceq A B) %<- (ceq B A') %.
%block comb-block {y comb}%.
%worlds (comb-block) (ceq _ _) %.

Correctness of the translation

% substitution lemma
%sort subst {_ bracket ([y] A y) A'} {C comb} {_ ceq (capp A' C) (A C)} %.
%mode subst %in %in %out %.
%term _ subst (%the (bracket ([y] y) i) bracket/var) C (%the (ceq (capp i C) C) ceq/i) %.
%term _ subst (%the (bracket ([y] i) (capp k i)) bracket/i) C (%the (ceq (capp (capp k i) C) i) ceq/k) %.
%term _ subst (%the (bracket ([y] k) (capp k k)) bracket/k) C (%the (ceq (capp (capp k k) C) k) ceq/k) %.
%term _ subst (%the (bracket ([y] s) (capp k s)) bracket/s) C (%the (ceq (capp (capp k s) C) s) ceq/k) %.
%term _
  %pi (subst (bracket/app (%the (bracket ([y] B y) B') Dbrack2) (%the (bracket ([y] A y) A') Dbrack1)) C (ceq/trans (ceq/app Dceq2 Dceq1) ceq/s))
  %<- (subst Dbrack1 C (%the (ceq (capp A' C) (A C)) Dceq1))
  %<- (subst Dbrack2 C (%the (ceq (capp B' C) (B C)) Dceq2)) %.
%block subst-block {y comb} {dbrack bracket ([z] y) (capp k y)} {thm-subst {C comb} subst dbrack C ceq/k}%.
%worlds (subst-block) (subst _ _ _) %.
%total D (subst D _ _) %.