1.5.5 Beta-Conversion

The first argument of betaConvert/2 is the expression to be reduced and the second argument will be the result after reduction. Let's look at the two clauses of the predicate in detail. You find them in the file betaConversion.pl .

betaConvert(Functor@Arg,Result):-
        betaConvert(Functor,lambda(X,Formula)),
        !,
        substitute(Arg,X,Formula,BetaConverted),
        betaConvert(BetaConverted,Result).

The first clause of betaConvert/2 is for the cases where ``real'' -conversion is done, i.e. where a is thrown away and all occurences of the respective variable are replaced by the given argument. In such cases

1. The input expression must be of the form Functor@Arg,

2. The functor must be (recursively!) reducible to the form lambda(X,Formula) (and is indeed reduced to that form before going on).

If these three conditions are met, the required substitution is made and the result can be further -converted recursively.

This clause of betaConvert/2 makes use of a predicate substitute/4 (originally implemented by Sterling and Shapiro) that we won't look at in any more detail. It is called like this:

substitute(Substitute,For,In, Result).

Substitute is substituted for For in In. The result is returned in Result.