An Analysis of Selectional Restrictions in Dependent Type Semantics- Logical polysemies, Coercion and Metaphor Department of Computer Science Eriko Kinoshita (Supervisor : Daisuke Bekki)type), written (x : A) → B, and Σ-type (dependent] product type), written (x : A) × B or[x:A(see [10] for details). A term having a deB
pendent type is called a proof term. For instance,p : man(x) expresses that a proof term p has thetype man(x), in other words, p is a proof for theproposition that x is a man.
In contrast to model-theoretic semantics, thesemantics of natural language based on dependent types can be called proof-theoretic semantics, where the meaning of a sentence is regarded as a proof-condition (verification condition), rather than as a truth-condition. By taking
proof-conditions as a central aspect of meaning,
semantic theories based on dependent types areparticularly suitable for capturing inferential aspects of interpretation.
DTS [3, 4] differs from the previous studies inthat it has underspecified term @ to handle phenomena that depend on the preceding contexts
such as presupposition and anaphora. For example, the sentence in (2) is given the semantic representation (SR) containing the term @ having theΣ-type for the proposition that there is an entity xsuch that x is a man. A term having the Σ-type isa pair of objects, from which the projection function π1 takes the first element.
(2) He whistled.
( (]))[x : entitywhistle π1 @ :man(x)Such an underspecified SR is compositionally derived from a parse tree for a sentence. Then thewell-formedness of an SR is proved via typechecking. This process of type-checking involves
a process of constructing a proof term for @. By
replacing @ with the constructed term, we can resolve presupposition and anaphora and thus obtain a fully specified SR for the sentence. The
overall process is shown in (3). See [3, 4] formore details.
3. An Analysis in DTS. Selectional restrictions
show the behavior of presupposition [1, 8, 9].

1. Introduction. Recently, various extended typesystems have been developed to explain phenomena related to coercion [1, 2, 13]. These systems
are enriched with more fine-grained types than iscommonly assumed in formal semantics, whichenables us to analyze selectional restrictions ofpredicates as type matching. In such systems, anoperation for dealing with coercion is triggered
when a predicate and its argument cause a typemismatch. However, there is a problem with thenaive assumption that coercion is only triggeredby type mismatch: coercion can be contextuallytriggered without any type mismatch. For example, (1a) has the reading in (1b), even though theliteral reading does not produce a type mismatch.
(1) a. The lion escaped.
b. The actor who plays the lion
at The Lion King escaped(from the theater).
Moreover, type inference with selectional restriction is context-sensitive in a way that is analogous to presupposition (see §3). These phenomena suggest that coercion is not only driven bytype matching in semantic composition but also
by inference with contextual information.
This paper proposes a formal analysis of coercion in the framework of Dependent Type Semantics (DTS) [3, 4], a framework of proof-theoretic
semantics that combines dependent types withunderspecification. Coercion is treated at thestage of type checking implemented as proof
search, rather than at the stage of semantic composition. We show that this analysis captures theinferential aspect of coercion as shown by phenomena like (1).
2. DTS. Dependent types have been used to analyze various aspects of natural languages [6, 12].
Compared with simple types, dependent types can
express types depending on terms. For instance,man(x) is a type depending on a term x that corresponds to the proposition that x is a man. Dependent types include Π-type (dependent function(3)

semantic compositiontype-checking

parse trees −−−−−−−−−−→ underspecified SRs −−−−−−→ well-formed SRs(proof search)

1..
..

[escape :x : entityanimate(x)](CON )→ type..
..

T F lanimate : type ? : T F lanimate@(@ : T F lanimate ) : T F lanimate[] (ΣE)x : entityl
π1 (@ : T F animate ) :animate(x)escape(π1 (@ : T F lanimate )) : type

(ΠE)

Figure 1: Type checking for the SR of “The lion escaped.”
ment of the relation R has F target as a selectional restriction. In this case, we can choose thepredicate “y plays w at the Lion King” for R andanimate for F target. By replacing @ with theconstructed term and taking its first projection interms of π1 , we can obtain an SR escape(a, t),which captures the intended reading of (1b). In
the case of the literal reading of (1a), we can use
the equality relation to fill in R, which leads tothe desired interpretation. Using the mechanismof presupposition projection in DTS, we can also
account for the inference patterns in (4).
Although details are omitted here due to space
limitations, the present theory can naturally extend to other phenomena discussed in the literature [11], in particular, to logical polysemies (copredication) [1], metaphor and aspectual verbs[7]. In our proof-theoretic account, an effort toobtain an interpretation by coercion can be measured by the complexity of a proof search. Thisaccounts for an aspect of interpretation involved
in metaphor, coercion and aspectual verbs called
complicity [5]. In the full version of the paper, a more detailed comparison with other typetheoretic approaches where coercion is treated at
the stage of semantic composition [1, 2] will beaddressed too.

For instance, the predicate marry presupposesthat its arguments are human; this presupposition
projects out of constructions such as negation:(4) Bob didn’t marry Mary.
⇒ Bob and Mary are human.
To capture these presuppositional inferences,
we analyze selectional restrictions as presuppositions in DTS (cf. [8]). For example, we define alexical entry for escape as follows.
xescape : λx.escape(π1 (@ : T F animate))
xwhere T F[ animate≡ ]y : entity t pair : animate(y) F source : entity → type
 p : F source(x)][][
w:entityy:entity R:→ type →F source(w)animate(y)R(x, p)t pair

In simple type theory, the type of a one-placepredicate is usually defined as entity → prop.
In DTS, by] contrast, the type of escape is[x : entity→ type, where animate(x) specianimate(x)fies the selectional restriction of the predicate.
Note that selectional restrictions are represented
as predicates, not as types. In the case of (1b),we have an SR escape(π1 (@ : T F lanimate )),where l is the term of the lion. The typechecking for this SR goes as shown in Fig. 1.
Here the term @ launches a proof search forthe missing information: it searches a 5-tuple(t pair, F source, p, R, q) that satisfies the condition T F lanimate from the context, where q is a
proof term for R(l, p)t pair. In short, @ acts tolocate an object of type entity that satisfies theproperty animate, which is the selectional restriction of predicate escape, associated with thelion from the context. More specifically, t pairis a pair (a, t) of an actor a (of type entity) anda proof t that the actor is animate; F source isa property of the lion l such that the first argu-References. [1] Asher, N. (2011) Lexical Meaning inContext.[2] Asher, N. and Luo, Z (2012) Formalisationof coercions in lexical semantics.[3] Bekki, D. (2014)
Representing anaphora with dependent types. [4]Bekki, D. & Mineshima, K. (2017) Context-passing
and underspecification in Dependent Type Semantics.
[5] Camp, E. (2017) Why metaphors make good insults. [6] Cooper, R. (2012) Type theory and semantics in flux. [7] Egg, M. (2003) Beginning novels andfinishing hamburgers. [8] Kinoshita, E., Mineshima,
K. & Bekki, D. (2016) An analysis of selectional restrictions with Dependent Type Semantics. [9] Magidor, O. (2013) Category mistakes. [10] Martin-Löf,P. (1984) Intuitionistic Type Theory. [11] Pustejovsky,
J:1995, The Generative Lexicon.[12] Ranta, A. (1994)
Type Theoretical Grammar.[13] Retoré, C. (2014) TheMontagovian Generative Lexicon ΛT yn .

2