%%% Parallel reduction in the untyped lambda calculus
%%% Author: Frank Pfenning

=> : term -> term -> type.  %infix none 10 =>.
                            %name => R.

beta : ({x:term} x => x -> M1 x => M1' x)
     ->                      M2 => M2'
     ->       (app (lam M1) M2) => M1' M2'.

ap   :            M1 => M1'
     ->           M2 => M2'
     ->  (app M1 M2) => (app M1' M2').

lm   : ({x:term} x => x -> M x => M' x)
     ->                  lam M => lam M'.

% Parallel, multi-step reduction

=>* : term -> term -> type.  %infix none 10 =>*.
                             %name =>* R*.

%tabled =>*.

id   :          M  =>* M.

;    :          M  =>* M''  
     <-         M  => M'
     <-         M' =>* M''.   %infix right 10 ;.


% Parallel conversion

<=> : term -> term -> type.  %infix none 10 <=>.
                             %name <=> C.

%tabled <=>.
reduce :  M  =>* M'
       -> M  <=> M'.

expand :  M  =>* M'
       -> M' <=> M.

;;     :  M  <=> M'
       -> M' <=> M''
       -> M  <=> M''.  %infix none 8 ;;.