Computation and Deduction 2009/20090304-support

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% ABORT %%
Output: here.

Support code for March 4 guest lecture on worlds-checking and combinators.

% combinator equality

ceq : comb -> comb -> type.

% betas
ceq/i : ceq (capp i A) A.
ceq/k : ceq (capp (capp k A) B) 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'.

%worlds (comb-block) (ceq _ _).