%%% computation semantics of the untyped lambda calculus (call-by-name)
%%%
%%% To force normal-order evaluation, the [app-operand] rule
%%% is only allowed to be used if the operator is in normal form
%%% and not a beta-redex.
%%%
%%% AUTHOR: Gary T. Leavens

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