define equality predicate Lambda-Calculus nltk

I am trying to define a Lambda-Calculus representation of the word 'are', which is an equality predicate for this ccg:

ccg = '''
# CCG grammar
# complete the lexical entries with their categories and semantics

:- S, NP, N

logicians => NP { \\x. LOGICIANS(x) }
logicians => N { \\x. LOGICIANS(x) }
linguists => NP { \\x. LINGUISTS(x) }
linguists => N { \\x. LINGUISTS(x) }
engineers => NP { \\x. ENGINEERS(x) }
engineers => N { \\x. ENGINEERS(x) }

non => NP/N { \\N x. ~N(x) }

are => (S\\NP)/NP  {\\x y.are(x,y)}

all => NP/N { \\P Q. all x. (P(x) -> Q(x)) }
no => NP/N { \\P Q. all x. (P(x) -> ~Q(x)) }
some => NP/N { \\N V. exists x. (N(x) & V(x)) }
'''

With this ccg, I want to parse sentences like 'all logicians are linguists'. However, I find it hard to find the correct representation of the word 'are'. For example, I tried to define 'are' as:

are => (S\\NP)/NP {\\X x.X(\y.are(x,y))}

Unfortunately, this resulted in a faulty semantic interpretation:

S {are(\x.LINGUISTS(x),\Q.all x.(LOGICIANS(x) -> Q(x)))}

Next, I tried to define it as:

are => (S\\NP)/NP { \\X Y. all y. (X(y) <-> Y(y)) }

But then I ended up with the following error because y gets interpreted as a variable

LogicalExpressionException                Traceback (most recent call last)

/usr/local/lib/python3.10/dist-packages/nltk/sem/logic.py in parse(self, data, signature)
    153         try:
--> 154             result = self.process_next_expression(None)
    155             if self.inRange(0):

24 frames

LogicalExpressionException: 'y' is an illegal predicate name.  Individual variables may not be used as predicates.


The above exception was the direct cause of the following exception:

LogicalExpressionException                Traceback (most recent call last)

/usr/local/lib/python3.10/dist-packages/nltk/sem/logic.py in parse(self, data, signature)
    157         except LogicalExpressionException as e:
    158             msg = "{}\n{}\n{}^".format(e, data, " " * mapping[e.index - 1])
--> 159             raise LogicalExpressionException(None, msg) from e
    160 
    161         if self.type_check:

LogicalExpressionException: 'y' is an illegal predicate name.  Individual variables may not be used as predicates.
all y.(LINGUISTS(y) <-> all x.(LOGICIANS(x) -> y(x)))

I can't change the grammar itself (the S,NP,N rules) so I feel like I'm stuck. Is there any way to define the equality relation in Lambda-Calculus for ccg's?

Solution

By its syntactic definition, are is applied first to the object NP linguists and then to the subject NP all logicians to yield a sentence.

So we need something that abstracts over two NPs:

\\P R. ...

The quantified NP all linguists in subject position will reduce to

\\Q. all x. (Logician(x) -> Q(x))

We then want this quantified subject NP to be applied to the object NP, so that Linguists can fill in for Q.

So what are needs to do after taking an object NP P and a quantified subject NP R is to apply the latter to the former:

R(P)

Thus we get

are => (S\NP)/NP  {\\P R. R(P)}

We can see that this matches the given category as taking an NP and another NP to yield a sentence.

With this we get the reduction behavior as desired:

  (     are    (     linguists   ))(           all                (     logicians    ))
= ((\\P R.R(P))(\\x. Linguists(x)))((\\P Q. all x. (P(x) -> Q(x)))(\\x. Logicians(x))))
= ((\\P R.R(P))(\\x. Linguists(x)))(\\Q. all x. ((\\x. Logicians(x)))(x) -> Q(x)))
= ((\\P R.R(P))(\\x. Linguists(x)))(\\Q. all x. (Logicians(x) -> Q(x)))
= (\\R.R (\\x. Linguists(x)))(\\Q. all x. (Logicians(x) -> Q(x)))
= (\\Q. all x. (Logicians(x) -> Q(x)))(\\x. Linguists(x))
= all x. (Logicians(x) -> (\\x. Linguists(x)))(x))
= all x. (Logicians(x) -> Linguists(x))

Old answer preserved as an alternative (and arguably better, bot not allowed by the assignment) approach:

~~The problem with your grammar starts at an earlier point.~~

You should not need two different definitions for each predicate "logician", "linguists", ... to make them work in different syntactic positions of the sentence. They are NPs - functions which abstract over individuals and return true or false. The category N does not match this behavior. It is meant for names or pronouns referring directly to a single individual. So these definitions should go, and only the ones with NP remain.

The quantifiers are, as you correctly lambda-defined them, functions which successively combine with two predicates (NPs) on their right to form a sentence (S). So their category must be (S/NP)/NP.

Since "non-" takes an NP to become another NP, its category must be NP/NP.

Now what we want for the behavior of are is

all(logicians)(are(linguists)) = all(logicians)(linguists)

i.e. that when applied with a predicate, it reduces to just that predicate itself. So are is the identify function on predicates: \\P.P.

Syntactically, it combines with an NP to yield another NP, so its category is NP/NP.

are => NP/NP {\\P.P}

Now we get the reduction behavior as desired:

(all(logicians))(are(linguists)) (( (S/NP)/NP )( NP ))(NP/NP( NP )) = ((\\P Q. all x. (P(x) -> Q(x)))(\\x. Logician(x)))(\\P.P(\\x. Linguist(x))) (( (S/NP)/NP )( NP ))( NP ) = (\\P Q. all x. (P(x) -> Q(x)))(\\x. Logician(x)))(\\x. Linguist(x)) ( S/NP )( NP ) = (\\ Q. all x. ((\\x. Logician(x))(x) -> Q(x)))(\\x. Linguist(x)) ( S/NP )( NP ) = (\\ Q. all x. (Logician(x) -> Q(x)))(\\x. Linguist(x)) S = all x. (Logician(x) -> (\\x. Linguist(x))(x)) S = all x. (Logician(x) -> Linguist(x))