POPL Tutorial/Combinators session

From The Twelf Project

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

Contents 1 Syntax 2 Translation 3 Equational theory 4 Correctness of the translation

Syntax

 lambda calculus

term : type.                    %name term M x.

app : term -> term -> term.
lam : (term -> term) -> term.


 combinator calculus

comb : type.                    %name comb A y.

s : comb.
k : comb.
i : comb.
capp : comb -> comb -> comb.

Translation

 bracket abstraction
 XXX fill in

 translation
 XXX fill in

Equational theory

 lambda term equality

 (elided)

 combinator equality

ceq : comb -> comb -> type.

 betas
ceq/i : ceq (capp i A) A.
ceq/k : ceq (capp (capp k A) _) A.
ceq/s : ceq (capp (capp (capp s A) B) C) (capp (capp A C) (capp B C)).

 extensionality
ceq/ext : ceq A A'
           <- ({y:comb} ceq (capp A y) (capp A' y)).

 compatibility
ceq/app : ceq (capp A B) (capp A' B')
           <- ceq A A'
           <- ceq B B'.

 equivalence
ceq/refl : ceq A A.

ceq/symm : ceq A A'
            <- ceq A' A.

ceq/trans : ceq A A'
             <- ceq A B
             <- ceq B A'.

%block comb-block : block {y:comb}.
%worlds (comb-block) (ceq _ _).

Correctness of the translation

 substitution lemma
 XXX fill in

Solution