%%% 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
%%%
%%% #load "abstract_syntax.mod", "substitution.mod", "normal_form.mod", "reductions.mod".
%%% #query abstract_syntax, substitution, normal_form, reductions.

module reductions.

import abstract_syntax, substitution, normal_form.

type	reducesto	term -> term -> o.

(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 M')
=> % ------------------------------             [app-operator]
     (reducesto (ap M N) (ap M' N)).

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

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