% Beta-reduction for  higher order logic
% beta_red.pl
% Based on code by Patrick Blackburn & Johan Bos

% Operator for functional application
:- op(400, yfx, *).

beta_reduce(Expression, Result):-
	beta_reduce(Expression, Result, []).

beta_reduce(Expr1, Expr2, []):-
    var(Expr1),
   Expr1=Expr2.

beta_reduce(Expression, Result, Stack):-
	nonvar(Expression),
	Expression = Functor*Argument,
	beta_reduce(Functor, Result,  [Argument|Stack]),!.

beta_reduce(Expression, Result, [Var|Stack]):-
	nonvar(Expression),
	Expression = Var^Body,!,
	beta_reduce(Body, Result, Stack).

beta_reduce(Expression, Result, []):-
	nonvar(Expression),
	\+ (Expression = X^_, nonvar(X)), %!,
	compose(Expression, Functor, Expressions),
	beta_reduce_all(Expressions, Results),
	compose(Result, Functor, Results).

compose(Term,Symbol,ArgList):-
    Term =.. [Symbol|ArgList].


beta_reduce_all([], []).
beta_reduce_all([First|Rest], [NewFirst|NewRest]):-
	beta_reduce(First, NewFirst),
	beta_reduce_all(Rest, NewRest).