%%% computation semantics of the untyped lambda calculus.
%%%
%%% The rules are ordered to favor normal-order evaluation,
%%% but this is not forced by the rules, and so on backtracking
%%% other orders are possible.  But this corresponds to the usual
%%% presentation of a reduction system for the lambda calculus.
%%%
%%% AUTHOR: Gary T. Leavens

module reductions.
  
  accumulate normal_form, rtc.
  
  (reducesto (ap (lambda I M) N) NforIinM) :- (substitute N I M NforIinM).
                                                % [beta]
  
  (reducesto (lambda I (ap M (var I))) M) :- (not (free_in I M)).
                                                % [eta]
  
             (reducesto M M2)
  => % ------------------------------             [app-operator]
       (reducesto (ap M N) (ap M2 N)).
  
           (reducesto N N2)
  => % ------------------------------             [app-operand]
       (reducesto (ap M N) (ap M N2)).
  
                (reducesto M M2)
  => % --------------------------------------     [reduce-body]
       (reducesto (lambda I M) (lambda I M2)).