[ formulas
| nd
| and
| lv
| nd -> and
| and -> lv
| lv -> and
| and -> nd
| reductions
|| minimal linear logic
|| LLF
]
Some Reductions for Annotated Natural Deductions
%%% Reduction of annotated minimal linear natural deductions
%%% Author: Frank Pfenning
%%%
%%% This incorporates no strategy, just gives the rules
%%% Also, this includes no commutative reductions.
rede : elim A & elim A -> type.
redi : intro A & intro A -> type.
%% Coercion
rede_coerce : rede (i2e (e2i E) , E). % needed? --- seems eta-like.
redi_coerce : redi (e2i (i2e I) , I).
%% Multiplicative Connectives
rede_imp : rede (impe' I2 (i2e (impi' I1)) , i2e (I1 (i2e I2))).
redi_times : redi (timese' I3 (i2e (timesi' I1 I2)) , I3 (i2e I1) (i2e I2)).
redi_one : redi (onee' I1 (i2e (onei')) , I1).
rede_with1 : rede (withe1' (i2e (withi' (I1 , I2))) , i2e I1).
rede_with2 : rede (withe2' (i2e (withi' (I1 , I2))) , i2e I2).
% no rede_top
redi_plus1 : redi (pluse' (I2 , I3) (i2e (plusi1' I1)) , I2 (i2e I1)).
redi_plus2 : redi (pluse' (I2 , I3) (i2e (plusi2' I1)) , I3 (i2e I1)).
% no redi_zero
rede_forall : rede (foralle' T (i2e (foralli' I1)) , i2e (I1 T)).
redi_exists : redi (existse' I2 (i2e (existsi' T I1)) , I2 T (i2e I1)).
redi_! : redi (!e' I2 (i2e (!i' I1)) , I2 (i2e I1)).
[ formulas
| nd
| and
| lv
| nd -> and
| and -> lv
| lv -> and
| and -> nd
| reductions
|| minimal linear logic
|| LLF
]
Frank Pfenning