As can be seen in the O'Reilly NLTK book, Chapter 10, when I want to model the syntax tree of sentence “Bob loves Alice,” namely
into first-order logic lambda-expressions, I get the following:
where on the left I have the tree of types and on the right the tree of λ-expressions. I have chosen to type-raise both Bob and Alice.
My question is the following: from the tree of types I can easily calculate that the type of "loves" must be <<<e,t>,t>,<e,t>> but how can I deduce from this that the corresponding λ-expression must be
λR.λx.R(λy.loves(x,y))
Is there some method to obtain the λ-expression of a leave of the syntax tree from its type and from the surrounding λ-expressions?