3.5.5 Beta-Conversion

Implementation of 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 three clauses of the predicate in detail.

betaConversion.pl: View Download

betaConvert(Var,Result):-
        var(Var),
        !,
        Result=Var.

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

The first clause of betaConvert/2 simply records the fact that variables cannot be further reduced.

The second clause 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 compound,

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

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