# One can write arbitrary comments in this file after hashes,
# but keep in mind that students will be able to see such comments.

# The first non-comment line of the file is the title of the
# assignment.

Homework 3: Generalized Quantifiers

# Next, typing conventions are entered. If no typing conventions
# are given, some defaults are used.

constants of type e : alice betty connor mary john bill
constants of type i : k
constants of type <e,t> : book smokes boy girl
constants of type <e, <e, t>> : hits with has using 
constants of type <e, <e, <e, t>>> : give 
variables of type <<e, t>, t> : XX NP2 NP3 YY ZZ A B C
variables of type <<<e, t>, t>, <<e, t>, t>> : D YYY
variables of type <<<<e, t>, t> , <e,t>>,t> : NP1
variables of type e : x-z
variables of type <e,t> : P-Q X-Z 
variables of type <e,et> : R-W 


# The following directive instructs the program to
# interpret multiple-letter constants and variables
# properly.

multiple letter identifiers

# "use rule" directives are for tree evaluation exercises.
# They indicate which composition rules are available
# at nonterminals.

use rule function application
use rule non-branching nodes
use rule predicate modification
use rule lambda abstraction

# Next, lexical entries provided to the student are given.
# A word (i.e. "sleep") can be given any number of lexical
# entry choices by repeating the "define" directive multiple
# times. Students are able to add their own lexical entries
# as well.

define happy : Lx.happy(x)
define boy,boys : boy
define girl,girls : girl
define love, loves : LyLx.love(x,y)
define someone, somebody : LP.Ex[P(x)]
define everyone, everybody : LP.Ax[P(x)]
define no-one, nobody : LP.~Ex[P(x)]
define some,a : LP.LQ.Ex[P(x) & Q(x)]
define every : LP.LQ.Ax[P(x) -> Q(x)]
define most : LP.LQ.|P ^^ Q| >= k*|P|
define most : LP.LQ.|{x | P(x)} ^^ {x | Q(x)}| >= k*|{x|P(x)}|
define no : LP.LQ.~Ex[P(x) & Q(x)]
define no : LP.LQ.P ^^ Q = \emptyset
define no : LP.LQ.|P ^^ Q| = 0

define Alice : alice
define Betty : betty
define Connor : connor

define Mary: LP.P(mary)
define John: LP.P(john)
define Bill: LP.P(bill)
define book: book
#define gives: LYY.YY(Ly(LXX.Lx.(XX(Lz.give(z)(y)(x)))))
define gives: LYY.LZZ.LXX(ZZ(Lx.XX(Lz.YY(Ly.(give(x)(y)(z))))))
define gives: LYY.LXX(YY(Lx.XX(Lz.Ly.(give(x)(y)(z)))))
define with : LXX.LP.LYY.(XX(Ly(YY(Lx.using(y)(x) & P(x)))))
define with : LXX.LYY.LP(XX(Ly(YY(Lx.(has(y)(x) & P(x))))))
define hits : LXX.Ly(XX(Lx.(hits(y)(x))))
define smokes : smokes
define and : LP.LXX.Ly.XX(Lx(P(x) & P(y)))
define does : LXX.XX
define too : LYYY.YYY
# Finally, the exercises themselves are entered.

exercise tree
title Formulating NatLg denotations as lambda-expressions
directions Do the derivation.

[.S [.NP every girl] [.VP [.VP gives [.NP Mary ] ] [.NP a book ] ] ]

[.S [.NP every girl] [.VP [.VP gives [.NP Mary ] ] [.NP a book ] ] ]

[.S [.NP John ] [.VP [.VP hits [.NP a boy ]] [.PP with [.NP a book ] ] ] ]

[.S [.NP John ] [.VP hits [.NP [.NP a boy ] [.PP with [.NP a book ] ] ] ] ]

[.S [.VP [.NP John ] [.VP smokes [.CON and ] ] ] [.S [.NP Bill ] [.VP [does] [too]]]]

#[.S [.S [.NP John ] [.VP smokes ] ] [.SCON [.CON and ] [.S [.NP Bill ] [.VP does too ] ] ] ]