3.5.6 Beta-Conversion Continued

Implementation of Beta-Conversion continued.

Finally, there is a clause of betaConvert/2 that deals with those expressions that do not match the first two clauses. Note that the first two clauses both contain cuts. So, this last clause will deal with all (and only) the non-variable 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.

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

This clause breaks down such expressions and recursively reduces their arguments or subformulas. This is done with the help of:

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

?- Question!

We said that the last clause handles atomic formulas with arguments that are still reducible. Given our grammar and lexicon, can we ever get this kind of expressions?

Here is an example query with -conversion:

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

Try it for ``John loves Mary'': s(Sem,[john,loves,mary],[]), betaConvert(Sem,Res).

?- Question!

Above, we said that complex formulas like walk(john) & (lambda(X,talk(X))@john) are reduced to 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.

?- Question!

In Chapter 6, we will learn about a way of semantics construction that differs in some respects from what we are doing now with the -calculus. Without going into detail, (sub-)formulas might be of the form walk@john there. Nevertheless, we will use the predicate betaConversion/2 given above to reduce formulas containing . Now, the question is: Which of the clauses of betaConvert/2 handles queries like betaConvert(walk@john,Res)? What is the result?

Our implementation of betaConvert/2 uses a version of the Sterling and Shapiro substitute/4 predicate. Because this is an important predicate, we recommend that you look at its definition in Section ``substitute/4''.