CADE Tutorial/Combinators Support

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
% XXX fill in
% translation
% XXX fill in

Equational theory

% lambda term equality
% (elided)
% combinator equality
%sort ceq {_ comb} {_ comb} %.
% betas
%term ceq/i ceq (capp i A) A %.
%term ceq/k ceq (capp (capp k A) B) 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
% XXX fill in