1.5.6 Beta-Conversion Continued

Second, there is a clause of betaConvert/2 that deals with those expressions that do not match the first clause. Note that the first clause contains a cut. So, the second clause will deal with all and only those expressions whose functor is not (reducible to) a -abstraction. The only well-formed expressions of that kind are formulas like walk(john) & (lambda(X,talk(X))@john) and atomic formulas with arguments that are possibly still reducible. Apart from that, this clause also applies to predicate symbols, constants and variables (remember that they are all represented as Prolog atoms). It simply returns them unchanged.

betaConvert(Formula,Result):-
        compose(Formula,Functor,Formulas),
        betaConvertList(Formulas,ResultFormulas),
        compose(Result,Functor,ResultFormulas).

The clause breaks down Formula using the predicate compose/3. This predicate decomposes complex Prolog terms into the functor and a list of its arguments (thus in our case, either the subformulas of a complex formula or the arguments of a predication). For atoms (thus in particular for our representations of predicate symbols, constants and variables), the atom is returned as Functor and the list of arguments is empty.

If the input is not an atom, the arguments or subformulas on the list are recursively reduced themselves. This is done with the help of:

betaConvertList([],[]).
betaConvertList([Formula|Others],[Result|ResultOthers]):-
        betaConvert(Formula,Result),
        betaConvertList(Others,ResultOthers).

After that, the functor and the reduced arguments/subformulas are put together again using compose/3 the other way round. Finally, the fully reduced formula is returned as Result.

If the input is an atom, the calls to betaConvertList/2 and compose/3 trivially succeed and the atom is returned as Result.

Here is an example query with -conversion:

?- s(Sem,[harry,flies],[]), betaConvert(Sem,Reduced).
 
Sem = lambda(A,A@mary)@lambda(B,walk(B)), Reduced = fly(harry) 

Try it for ``Harry curses a witch.'': s(Sem,[harry,curses,a,witch],[]), betaConvert(Sem,Res).

?- Question!

Above, we said that complex formulas like fly(harry) & (lambda(x,fly(x))@harry) are split up into their subformulas (which are then in turn -converted) by the last clause of betaConvert/2. Explain how this is achieved at the example of this particular formula!