Converting types into lambda notation and set notation

I am looking into different phrases and their semantic derivation. For example, the verb sneeze:

Type (e,t)

λx[SNEEZE]x

In a sentence like: Michael and Jamie sneeze, I would like to know how to get to to RUN(m)^RUN(j).

I know that Michale and Jamie are of type (e) and that two DPs conjoined together mean that the type of 'and' in this case is (e,ee)

The lambda notation of 'and' I have found to be λP[λx[λy[P(x)^Q(y).

However I am unsure when applying each lambda how to get the end result.

Similarly, in the case of quantified DP expressions.

I have found that in a statement like two cookies λx[2x^COOKIE (et,t)

OR

less than four girls λx[#x<4^GIRL(x)] (et,t)

that they difficult to combine with other elements.

For example, Daniel and Nina ate two cookies. Here, a type mismatch occurs quantifier raising and lambda extraction are needed. But it is hard to do these processes if it is hard to combine with the elements. Daniel (e), Nina (e), and (e,ee) λP[λxλy[P(x)^Q(y), ate (e,et) λxλy[EAT(y,x)].

Similarly, Less than four girls smile and laugh. Smile (et), laugh (et), and (e,t) (e,t) (e,t) λP[λQ[λx[P(x) ∧ Q(x)]]]. I am struggling particularly because 'less than' seems hard to put in lambda notation. I was wondering whether set notation would be better for this semantic derivation?

So for all three sentences, I have looked over them for a number of days now and I am struggling to find any sort of conclusion for them. Particularly Dan and Nina ate two cookies, as the examples I have searched for quantifier raising all seem to not have any conjoined NPs in. Most examples are of the type of 'John bought every dog' and not 'Bill and Ben bought two pots' etc.

• What is your question? What exactly would you like to do? Find a beta-reduction series that starts with an application of the lambda expressions for the individual expressions and ends with the reduced term? Then again: Where is the point where you got stuck? Apr 11 '19 at 15:14
• @lemontree Essentially how to convert quantifed DPs into lambda/set notation, and if there is a type mismatch at the VP stage, specifically at Dan and Nina ate 2 cookies, then how would the tree be like by doing quantifier raising and lambda extration. Also to check if my types are correct because I am unsure about the lambda notation of the numeral expressions. I am not a seasoned linguist by any means but I have struggled for many days and I haven't found any good information relating to this area so I just want to find out how to do complete semantic derivations of those sentences. Apr 11 '19 at 17:39
• @Lyhbm It's really interesting. In which domain do you use lambda calculus, type theory, adn semantics at the same time ? I see you reconstruct the semantics of the sentence with mathematical terms, but ignore in which field one usually does this. Any reference so I can educate myself a little on this ? Are you doing some NLP Machine Learning stuffs, or is it much more fundamental research in semantics ? In your other question, linguistics.stackexchange.com/a/31124/1172 is pointing to Formal Semantics. Is it the good start point ? Apr 13 '19 at 10:50
• @StephaneRolland I am currently an undergraduate linguistics student studying intermediate semantics. For complete semantic derivation, we are required to notate lambda calculus, type theory and sets and predicates. Also looking into areas of formal semantics. Apr 14 '19 at 16:51

As for and:

You got your lambda term for and wrong. Either you mean coordination between subject DPs ("Mary and John sneeze") then your lambda term is λP[λx[λy[P(x)^P(y)]]], with just one predicate P (not Q). Or you mean a coordination between VPs ("Mary sneezes and coughs"), then your lambda term is λPλQ[λx[P(x)^Q(y)]]] (with an abstraction for a second predicate Q but just one abstraction for an individual variable x). I assume you meant λP[λx[λy[P(x)^P(y)]]], which is of type ((e,t),(e,(e,t))): Put in a one-place predicate, then an individual, then another individual, get out a truth value.

Also, you got the sneezing wrong: The term is λx[sneeze(x)], not λx[sneeze](x); the application to x is part of the scope of the lambda abstraction, not outside of it.
To avoid confusion with the variable x, we can (but don't have to) rename the bound variable x to, say, u, and get λu[sneeze(u)] with the exact same meaning.

So for the sentence "John and Mary run", you simply apply your and term to each of the terms you abstract for:

and                    sneeze         mary john
≡ (λP[λx[λy[P(x)^P(y)]]])(λu[sneeze(u)])(m)  (j)
((e,t),(e,(e,t)))      (e,t)          (e)  (e)
> (λx[λy[(λu[sneeze(u)])(x)^(λu[sneeze(u)])(y)]])(m)(j)
(e,(e,t))                                      (e)(e)
> (λx[λy[sneeze(x)^sneeze(y)]])(m)(j)
(e,(e,t))                    (e)(e)
> (λy[sneeze(m)^sneeze(y)])(j)
(e,t)                    (e)
> sneeze(m)^sneeze(j)
(t)

Here I chose to first simplify the two redexes (λu[sneeze(u)])(x) and (λu[sneeze(u)])(y) to sneeze(x) and sneeze(y) before continuing with the applications to m and j, but one could do it the other way round as well and get the same result (In lambda calculus, the order in which you choose to perform your reductions never matters, eventually any two computation paths will yield the same end result):

and                    sneeze         mary john
≡ (λP[λx[λy[P(x)^P(y)]]])(λu[sneeze(u)])(m)  (j)
((e,t),(e,(e,t)))      (e,t)          (e)  (e)
> (λx[λy[(λu[sneeze(u)])(x)^(λu[sneeze(u)])(y)]])(m)(j)
(e,(e,t))                                      (e)(e)
> (λy[(λu[sneeze(u)])(m)^(λu[sneeze(u)])(y)])(j)
(e,t)                                      (e)
> (λu[sneeze(u)])(m)^(λu[sneeze(u)])(j)
(t)
> sneeze(m)^sneeze(j)
(t)

The lambda reduction for and between VPs works quite similarly:

and                   sneeze         cough         mary
≡ (λP[λQ[λx[P(x)^Q(x)]]])(λu[sneeze(u)])(λv[cough(v)])(m)
((e,t),((e,t),(e,t)))  (e,t)          (e,t)         (e)
> ... (absorb sneeze for P)
> ... (absorb cough for Q)
> ... (absorb mary for x)
> ... (simplify)
> sneeze(m)^cough(m)
(t)

As for your proposal for the quantified DPs, I don't quite understand your notation λx[2x^COOKIE (et,t) - how is 2x^something defined? I assume you mean something like "Tgere are two x'es and these x'es are cookies", but this is not very nice: For your individual variable x one individual goes in, and that's what your term will be applied to - one individual. By just prepending a "2" in front of the variable you don't magically duplicate the amount of entities involved - it's still just one individual that goes in, syntacically and semantically.
Furthermore, you missed the application to the variable x in your predication: cookie(x) - not just cookie.

In general, quantifiers are always a bit difficult to formalize, so don't worry if you're struggling.

"All", "some", "no" etc., can be modeled via ∃ and ∀, but for absolute numbers it gets difficult.
"Exactly one" can be formalized as follows:

exactly one: λP[λQ[∃x[∀y[P(y) <-> y=x] ^ Q(x)]]]

For a quantifier like "at least two", you can simply do three existential quantifications, have a conjunction of predicates applying to all the elements separately and then making sure that the variables stand for distinct entities:

at least two: λP[λQ[∃x1∃x2[P(x1)^P(x2)^x1≠x2^Q(x1)^Q(x2)]]]

You already see that this can get quite annoying if you have higher numbers or something more complex like a combination with a VP.
You can then combine the two tricks to get something like "exactly two" - again, the formula blows up even more:

exactly two: λP[λQ[∃x1∃x2∀y1∀y2[P(y1)<->x1=y1 ^ P(y2)<->y2=x2 ^ x1≠x2 ^ Q(x1) ^ Q(x2)]]]

"At most" can be achieved by adding negated existential statements ("there are no 3 distinct entities such that P applies to all of them").
Anything else is even more difficult. In particular, quantifiers like more than or most can not be defined with a first-order formula at all. So you'd probably want a different mechanism anyway.
A possibility is to model generalized-quantifiers via comparison between sets: no is a relation between to sets X and Y such that they have no elements in commen (their intersection is empty). at least one is a relation between to sets X and Y such that they have at least one element in common (their intersection is non-empty, or has cardinality (= size) >=1). all is a relation between to sets X and Y such that all elements which are in X are also in Y, i.e., X is a subset of Y (X ⊆ Y). two is a relation between two sets X and Y such that their intersection is of size 2. So two could be defined as

two: λP[λQ[|P∩Q| = 2]].

It's now debatable whether sets (which is what goes in here) is the same as predicates (which is what you'd normally want for VPs and NPs). When taking P for "cookie" and Q for the predication about these cookies, what the quantifier expresses is "The intersection between the things that are cookies and the things that Daniel and Nina ate is two", i.o.w., "There are exactly two entities which were eaten by Daniel and Nina and are coookies". (You actually have a semantic ambiguity here - did Daniel and Nina eat two cookies each, or two in total? Each of the two readings would have a different representation.)

In any case, a quantifier will be of type ((e,t),((e,t),t)):First a one-place predicates (or sets) go in; this will yield a quantified DP like "two cookies" of type ((e,t),t) as desired, because this is the usual type for quantified DPs. When we then put in another predicate, we get out a sentence with a truth value.
The way this notation of "two" works means that you effecively quantifier-raise, because your topmost operation will be the quantification, which comes from the DP in object position.

The other proposal would be to type-shift the verb, which expects two inputs of type e, to a different type such that it can absorb a quantified DP of type ((e,t),t):

eat: (e,(e,t)) --> (((e,t),t),(e,t))

This works well from a type-theoretic perspective, and can be represented in set notation, for example as outlined e.g. here and here. However, it is not clear what the resulting lambda term would look like, because you would have to allow the predicate eat two take an argument which is not an indidual but some complex lambda term that represents a quantified DP, and this would simply be no longer predicate logic.

In conclusion: Quantifiers are difficult. Representing them as generalized quantifiers by set-theoretic means is the easiest; in this case, they will be relatiions between sets, i.e. lambda terms of the form λP[λQ[some relation between P and Q]] and type ((e,t),((e,t),t)).