%%% 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

%%% #load "abstract_syntax.mod", "substitution.mod", "normal_form.mod", "computation_call_by_name.mod".
%%% #query abstract_syntax, substitution, normal_form, computation_call_by_name.

module computation_call_by_name.

import abstract_syntax, substitution, normal_form.

type	reducesto	term -> term -> o.

            (substitute N I M NforIinM)
=> % ----------------------------------------   [beta]
     (reducesto (ap (lambda I M) N) NforIinM).

           (reducesto M M')
=> % ------------------------------             [app-operator]
     (reducesto (ap M N) (ap M' N)).

        ((not (M = (lambda I M'))),
         (normal_form M),
         (reducesto N N'))
=> % ------------------------------             [app-operand]
     (reducesto (ap M N) (ap M N')).

            (not (free_in I M))
=> % ---------------------------------------    [eta]
     (reducesto (lambda I (ap M (var I))) M).

              (reducesto M M')
=> % --------------------------------------     [reduce-body]
     (reducesto (lambda I M) (lambda I M')).