POPL Tutorial/Combinators session

This is Literate Twelf Code: here Status: %% OK %% Output: here.

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

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