## The ACalculus

In Section 1.3, we pointed out that mathematical set notation was a helpful method of specifying properties P of words that we wanted to select from a document. We illustrated this with (31), which we glossed as "the set of all w such that w is an element of V (the vocabulary) and w has property P".

It turns out to be extremely useful to add something to first-order logic that will achieve the same effect. We do this with the A-operator (pronounced "lambda"). The A counterpart to (31) is (32). (Since we are not trying to do set theory here, we just treat V as a unary predicate.)

A expressions were originally designed by Alonzo Church to represent computable functions and to provide a foundation for mathematics and logic. The theory in which A expressions are studied is known as the A-calculus. Note that the A-calculus is not part of first-order logic—both can be used independently of the other.

A is a binding operator, just as the first-order logic quantifiers are. If we have an open formula, such as (33a), then we can bind the variable x with the A operator, as shown in (33b). The corresponding NLTK representation is given in (33c).

Remember that \ is a special character in Python strings. We must either escape it (with another \), or else use "raw strings" (Section 3.4) as shown here:

>>> e = lp.parse(r'\x.(walk(x) & chew_gum(x))')

<LambdaExpression \x.(walk(x) & chew_gum(x))>

>>> print lp.parse(r'\x.(walk(x) & chew_gum(y))') \x.(walk(x) & chew_gum(y))

We have a special name for the result of binding the variables in an expression: A-abstraction. When you first encounter A-abstracts, it can be hard to get an intuitive sense of their meaning. A couple of English glosses for (33b) are: "be an x such that x walks and x chews gum" or "have the property of walking and chewing gum." It has often been suggested that A-abstracts are good representations for verb phrases (or subjectless clauses), particularly when these occur as arguments in their own right. This is illustrated in (34a) and its translation, (34b).

(34) a. To walk and chew gum is hard b. hard(\x.(walk(x) & chew_gum(x))

So the general picture is this: given an open formula 9 with free variable x, abstracting over x yields a property expression Ax.9—the property of being an x such that 9. Here's a more official version of how abstracts are built:

(35) If a is of type T, and x is a variable of type e, then \x.a is of type (e, T).

(34b) illustrated a case where we say something about a property, namely that it is hard. But what we usually do with properties is attribute them to individuals. And in fact, if 9 is an open formula, then the abstract Ax.9 can be used as a unary predicate. In (36), (33b) is predicated of the term gerald.

Now (36) says that Gerald has the property of walking and chewing gum, which has the same meaning as (37).

What we have done here is remove the \x from the beginning of \x.(walk(x) & chew_gum(x)) and replaced all occurrences of x in (walk(x) & chew_gum(x)) by gerald. We'll use a[p/x] as notation for the operation of replacing all free occurrences of x in a by the expression P. So

represents the same expression as (37). The "reduction" of (36) to (37) is an extremely useful operation in simplifying semantic representations, and we shall use it a lot in the rest of this chapter. The operation is often called P-reduction. In order for it to be semantically justified, we want it to hold that Ax. a(P) has the same semantic value as a[ p/x]. This is indeed true, subject to a slight complication that we will come to shortly. In order to carry out P-reduction of expressions in NLTK, we can call the simplify() method O.

>>> e = lp.parse(r'\x.(walk(x) & chew_gum(x))(gerald)') >>> print e

\x.(walk(x) & chew_gum(x))(gerald) >>> print e.simplify() O (walk(gerald) & chew_gum(gerald))

Although we have so far only considered cases where the body of the A-abstract is an open formula, i.e., of type t, this is not a necessary restriction; the body can be any well-formed expression. Here's an example with two As:

Just as (33b) plays the role of a unary predicate, (38) works like a binary predicate: it can be applied directly to two arguments . The LogicParser allows nested As such as \x.\y. to be written in the abbreviated form \x y. O.

>>> print lp.parse(r'\x.\y.(dog(x) & own(y, x))(cyril)').simplify() \y.(dog(cyril) & own(y,cyril))

>>> print lp.parse(r'\x y.(dog(x) & own(y, x))(cyril, angus)').simplify() O (dog(cyril) & own(angus,cyril))

All our A-abstracts so far have involved the familiar first-order variables: x, y, and so on —variables of type e. But suppose we want to treat one abstract, say, \x.walk(x), as the argument of another A-abstract? We might try this: \y.y(angus)(\x.walk(x))

But since the variable y is stipulated to be of type e, \y.y(angus) only applies to arguments of type e while \x.walk(x) is of type (e, t)! Instead, we need to allow abstraction over variables of higher type. Let's use P and Q as variables of type (e, t), and then we can have an abstract such as \P.P(angus). Since P is of type (e, t), the whole abstract is of type ((e, t), t). Then \P.P(angus)(\x.walk(x)) is legal, and can be simplified via P-reduction to \x.walk(x)(angus) and then again to walk(angus).

When carrying out ^-reduction, some care has to be taken with variables. Consider, for example, the A-terms (39a) and (39b), which differ only in the identity of a free variable.

Suppose now that we apply the A-term \P.exists x.P(x) to each of these terms:

(40) a. \P.exists x.P(x)(\y.see(y, x)) b. \P.exists x.P(x)(\y.see(y, z))

We pointed out earlier that the results of the application should be semantically equivalent. But if we let the free variable x in (39a) fall inside the scope of the existential quantifier in (40a), then after reduction, the results will be different:

(41a) means there is some x that sees him/herself, whereas (41b) means that there is some x that sees an unspecified individual z. What has gone wrong here? Clearly, we want to forbid the kind of variable "capture" shown in (41a).

In order to deal with this problem, let's step back a moment. Does it matter what particular name we use for the variable bound by the existential quantifier in the function expression of (40a)? The answer is no. In fact, given any variable-binding expression (involving V, 3, or A), the name chosen for the bound variable is completely arbitrary. For example, exists x.P(x) and exists y.P(y) are equivalent; they are called a-equivalents, or alphabetic variants. The process of relabeling bound variables is known as a-conversion. When we test for equality of VariableBinderExpressions in the logic module (i.e., using ==), we are in fact testing for a-equivalence:

>>> e1 = lp.parse('exists x.P(x)') >>> print e1 exists x.P(x)

>>> e2 = e1.alpha_convert(nltk.Variable('z'))

True

When ^-reduction is carried out on an application f(a), we check whether there are free variables in a that also occur as bound variables in any subterms of f. Suppose, as in the example just discussed, that x is free in a, and that f contains the subterm exists x.P(x). In this case, we produce an alphabetic variant of exists x.P(x), say, exists z1.P(z1) , and then carry on with the reduction. This relabeling is carried out automatically by the ^-reduction code in logic, and the results can be seen in the following example:

>>> e3 = lp.parse('\P.exists x.P(x)(\y.see(y, x))') >>> print e3

(\P.exists x.P(x))(\y.see(y,x)) >>> print e3.simplify() exists z1.see(z1,x)

* > As you work through examples like these in the following sections, you may find that the logical expressions which are returned have different ' " f Jtf variable names; for example, you might see z14 in place of z1 in the preceding formula. This change in labeling is innocuous—in fact, it is just an illustration of alphabetic variants.