The
pioneering work of Ranta (1994) on using Type Theory for NL
semantics has initiated a strong interest in the use of Type
Theories for representing formal semantics. And even though
Type Theory was initially mainly concerned
with compositional and formal semantics, a number of
linguists, logicians and computer scientists noticed the
relevance of type theory for lexical semantics as
well. Around 2000 the paper “the metaphysics of words in
context” by Asher & Pustejovsky (2001) initiated Type
Theoretic approaches to lexical coercions and meaning
transfers by investigating extension and refinement of the type
system used by Montague. Accounts for this type of phenomena
need to capture ordinary selectional restriction phenomena
(e.g. a “chair” may not “bark”, in an ordinary context), while
at the some time they have to ensure some flexibility for
adapting meanings to contexts in case of meaning transfers,
co-predication etc. The study of this kind of phenomena is of
course not new. Their study goes back at least till the 80’s
(Bierwisch, Nunberg, Cruse among others). What is
relatively new is the study of these phenomena from the
perspective of Type Theory and this approach is by now quite
successful as valuable type theoretical contributions on
incorporating lexical considerations into compositional
semantics show (Asher, Bassac, Chatzikyriakidis, Cooper, Luo,
Melloni, Mery, Moot, Prévot, Pustejovsky, Ranta, Real, Retoré)
Authors
are invited to submit 4-page abstracts before March 31 on any
subject related to the workshop, including:
Papers
on this page should be referred to as follows: Author, Title in
ESSLLI proceedings of the TYTLES workshop on Type Theory and
Lexical Semantics (Cooper, Retoré, eds) ESSLLI 2015,
Barcelona.
Monday14:00-15:30
14:00 Christian
Retoré (and Robin Cooper), Introduction
14:30 Justyna Grudzinska and
Marek Zawadowski. A Puzzle about Long-distance Indefinites
and Dependent Type Semantics
Dependently Typed Semantics with Generalized Quantifiers (DTSGQ)
combines two semantic approaches to account for natural language
quantification: Generalized Quantifier Theory familiar from
Montague-style semantics (Mostowski, A. 1957, Lindstrˆm, P.
1966, Barwise, J., Cooper, R. 1981) and type-theoretic approach
(Martin-Löf, P. 1972, Ranta, A. 1994, Makkai, M. 1995, Luo, Z.
2012). Like in the classical Montague-style analysis, DTSGQ
makes essential use of generalized quantifiers (GQs). But in the
spirit of the type-theoretic framework we adopt a many-typed
analysis (in place of a standard single-sorted analysis). Like
in the standard type-theoretic approaches, we have type
dependency in our system. But our semantics is
model-theoretic (with truth and reference being basic concepts),
and not proof-theoretic (where proof is a central semantic
concept). Combining GQs with dependent types allows us to
handle in a uniform manner a number of semantic puzzles
concerning natural language quantifiers. In our previous work we
have defined a new interpretational algorithm to account for a
wide range of anaphoric (dynamic) effects associated with
natural language quantification (Grudzinska, J., Zawadowski, M.
2014). In this paper we will tackle the phenomenon of
exceptional scopes of one class of quantifiers (indefinites) and
the so-called puzzle about long-distance indefinites that seems
to be unsettled in the literature (see Chierchia, G. 2001,
Schwarz, B. 2001, Szabolcsi, A. 2010). Our solution to the
puzzle about long-distance indefinites makes crucial use of
dependent types, i.e. we propose to credit the problematic
long-distance readings to the presence of possibly hidden)
dependencies.
15:00 Stergios
Chatzikyriakidis, Mathieu Lafourcade, Lionel Ramadier and
Manel Zarrouk. Type Theories and Lexical Networks: Using
Serious Games as the Basis for Multi-Sorted Typed Systems
In this paper, we show how a rich lexico-semantic network which
has been built using serious games, JeuxDeMots, can help us in
grounding our semantic ontologies as well as different sorts of
information in doing formal semantics using modern type theories
(type theories within the tradition of Martin L¨of). We discuss
the domain of base types, adjectival and verbal types,
hyperonymy/hyponymy relations as well as more advanced issues
like homophony and polysemy.
Tuesday 14:00 - 15:30
14:00 Staffan Larsson.
Perceptual Meaning in TTR Judgement-based Semantics and
Conceptual Spaces
We are developing a type-theoretical judgement-based semantics
where notions such as perception, classification, judgement,
learning and dialogue coordination play a central role. By
bringing perception and semantic coordination into formal
semantics, this theory can be seen as an attempt at unifying
cognitive and formal approaches to meaning. The purpouse of this
paper is to briefly compare judgement-based semantics to the
theory of conceptual spaces. We conclude that there are
important similarities but also some differences. One aim of
judgement-based semantics is to formalise semantic
classification and learning in detail, to enable
integration of these aspects of meaning with those traditionally
studied in formal semantics, and to enable computational
modeling and implementation of these aspects of meaning. By
using statistical classifiers, we connect to machine learning
theory, giving access to a host of classification methods and
associated learning algorithms.
14:30 Simon Dobnik.
Interfacing Language, Spatial Perception and Cognition in
Type Theory with Records
In the proposed presentation we overview and connect two lines
of our work related to Type Theory with Records (TTR): modelling
of spatial language and cognition and modelling of
attention-driven judgement. We argue that computational
modelling of perception, action, language, and cognition
introduces several requirements on a formal semantic theory and
its practical implementations: (i) interfacing discrete
conceptual knowledge and continuous real-valued sensory
readings; (ii) information fusion of knowledge from several
modalities; (iii) dynamic adaptation of semantic
representations/knowledge as agents experience new situations
through linguistic interaction and perception. Using examples of
semantic representations of spatial descriptions we show how
Type Theory with Records satisfies these requirements. The
advantage of truth being based on agent-relative judgements in
TTR is crucial in this but practically it comes with a
computational cost. However, this challenge is not unique to
TTR. An agent would have to check whether a situation s is of
every type in its inventory. In the second part of the talk we
argue that the number of type judgements an agent has to make
can be minimised by incorporating a cognitive notion of
judgement that is driven by perceptual attention.
15:00 Peter Sutton and Hana
Filip. Probabilistic Mereological TTR and the Mass/Count
Distinction
The goals of this paper are threefold. (1) We argue that four
semantic classes can be used to predict cross and
intralinguistic variation in whether nouns are encoded as count
or mass. These semantic classes are defined in terms of two
kinds of sources: vagueness (Chierchia 2010) and (non-)overlap
of individuated entities (Landman 2011). (2) We enrich prob-TTR
(Cooper et al. 2014, a probabilistic variant of TTR, Cooper
2012) with mereological relations to give probM-TTR. We adopt
prob-TTR since its probabilistic basis is perfectly suited to
the representation of vagueness. We enrich it with mereology so
as to be able to express when two (mereological) entities
overlap. (3) We derive our four classes by defining vagueness
and non-overlap in probabilistic terms, and showing how
vagueness and (non-)overlap interact. The presence of neither
vagueness nor overlap is characteristic of prototypical count
nouns (cat, book). The presence of vagueness and overlap is
characteristic of “substance” mass nouns (mud, blood). Both
these noun classes display little or no cross and
intralinguistic variation in MASS/COUNT encoding. “Aggregate”
nouns (furniture, kitchenware) are not vague, but do overlap (a
pestle and mortar can count as both one and two items of
kitchenware). “Granular” nouns (lentils, rice) are vague (it is
vague how much rice counts as enough rice for dinner). Both of
these noun classes display cross- and intralinguistic
variation in MASS/COUNT encoding. Countability requires
determining a clear counting base of discrete entities.
Vagueness or overlap can interfere with counting, vagueness and
overlap always do.
Wednesday14:00 - 15:30
14:00 Ellen Breitholtz.
Are Widows Always Wicked? Learning concepts through
enthymematic reasoning
In this paper we suggest that enthymematic reasoning may play a
role in the acquisition of new concepts by a language learner.
On our account, a learner, for example a young child, forms
hypotheses about acceptable ways of reasoning – so called topoi
– based on observations and interaction with dialogue partners.
These topoi are then used to underpin the child’s reasoning in
other situations. To illustrate this point we analyse an example
of natural dialogue using an information state update approach
cast in Type Theory with Records. This approach allows us to
represent misunderstanding and misinterpretation of meaning,
since it is based on the conceptualisation of entities in
individuals rather than on a God's eye view of meaning. Also,
the record types of TTR offer a convenient way to represent
subtype relations, which seems to be an important aspect of our
evaluation of in which situations specific topoi are applicable
Our account fits well with an approach to word meaning where
speakers are constantly adjusting meanings on the basis of
experience, and where meaning may be negotiated in
interaction. Also, our account of word acquisition relates to
Pustejovsky’s (1998) suggestion that enthymemes, or enthymematic
reasoning, may be a means for lexical interpretation.
14:30 Bruno
Mery. The Relative Complexity of Constraints in
Co-Predicative Utterances
In
examining “The Relative Complexity of Constraints in
Co-Predicative Utterances”, we want to explore one among many
phenomena of lexical semantics that are at once hard to
characterise and prone to many exceptions and idiosyncrasies,
and nevertheless can be formally treated in compositional
semantics, thus illustrating the expressive power of
adaptative logical frameworks for semantics and the specific
challenges in gathering adequate data to evaluate their
validity. We detail the particular variations of semantic
felicity in co-predicative utterances the constraints on the
combination of facets of polysemous words, and the possible
adaptations that can be proposed to existing formal frameworks
that support lexical semantics. As the linguistic data is
incomplete and disputed, we also include a proposal for a
linguistic survey aimed at clearing up many outstanding
issues.This communication is intended as a discussion
material, detailing a specific issue in order to foster
collaborations around the subject. Having been prepared by the
author in his spare time, it is, by necessity, incomplete. The
work presented here is closely related to /\TYn, a formal
framework for lexical semantics developed since 2006 with
Christian Bassac, Richard Moot, Christian Retoré and many
other researchers at LaBRI and LIRMM. We will also present a
recently developed extension of that framework in Linear
Intuitionistic Logic that can be used to integrate many of the
discussed phenomena.
15:00 Daisuke Bekki and
Miho Satoh. Calculating Projections via Type Checking
Dependent type semantics (DTS) is a proof-theoretic,
compositional framework of discourse semantics based on
dependent type theory, extended with underspecified terms.
In DTS, anaphora and presupposition triggers are represented by
using underspecified terms, which are to be replaced by proof
terms inhabiting the same type. This process corresponds to
anaphora resolution and presupposition binding, and it has been
predicted in previous literature that the type of each
underspecified term can be calculated via type
inference/checking of dependent type theory, which amounts to
the calculation of presupposition projection. However, the
formulation of type inference/checking for DTS has been left as
an open issue, which is not an obvious task, since type
inference/checking in dependent type theory is known to be
undecidable. In this paper, we formalized a set of rules for a
type inference/checking algorithm for a decidable fragment of
dependent type theory, which is an extension of the type
inference/checking algorithm for Agda by Loh et al. We
claim that this fragment is sufficient for representing
(proof-theoretic) meaning of a broad range of natural language
sentences. Moreover, we have implemented the proposed
algorithm in Haskell programming language and demonstrate that
it correctly calculates the projective contents of sentences
involving presupposition filtering and global/local
accommodations.
Thursday 14:00 - 15:30
14:00 Laura Kallmeyer,
Timm Lichte, Rainer Osswald, Sylvain Pogodalla and Christian
Wurm. Quantification in Frame Semantics with Hybrid Logic
We present an approach that aims at integrating logical
operators into semantic frames by employing hybrid logic. Frames
have been developed as a format for the representation of
conceptual and lexical knowledge. They are commonly presented as
graphs, where nodes correspond to entities (individuals, events,
etc.) and edges represent (functional or non-functional)
relations between these entities. Semantic structures of this
type allow one to capture lexical meaning in a fine-grained way
but lack a natural way to integrate logical operators such as
quantifiers. Our approach starts from the observation that modal
logic is a powerful tool for describing relational structures
and is hence suitable for characterizing frames. We use a hybrid
logic extension of modal logic. In particular, we make use of
the following elements that can occur in logical formulas:
nominals, which allow the reference to specific nodes of the
frame, and state variables with their associated quantifiers,
which can express general properties of the models. Lexical
items are then provided with logical expressions which specify
the semantic properties that should hold for the corresponding
frames. This grounds our approach to quantification in frame
semantics. Finally, we devise a compositional syntax-semantics
interface in a type-theoretic setting and give an illustration
of how classical examples of quantifier scope can interact with
path equalities introduced by the lexical frames.
14:30 Livy Real and Alexandre
Rademaker. An Overview on Portuguese Nominalisation
We discuss nominalizations in Portuguese formed by the suffix
-ura, as pintura (painting), magistratura (magistracy) and
gordura (fat). We have done a corpus-based description of the
behavior of these nominal forms and proposed a type ontology to
categorize them. We have parted from all the nouns formed by
-ura which are present in OpenWordNet-PT and checked them in
three famous Portuguese dictionaries (Porto Dictionary, Caldas
Aulete Dictionary and Houaiss Dictionary). Then we analyzed
their use in context in Corpus Brasileiro, a corpus which has
more than 1 billion words extracted from various textual
genders. In order to offer a rich description, we also tested
all words formed by -ura in co-predication contexts with at
least three native speakers of Brazilian Portuguese with no
knowledge of linguistic study theories to check if their types
could be co-predicated. Although our main goal was to produce a
corpus-based description on those nouns, we have found few
possible generalizations considering the type-structure of -ura
forms. More than that, our tests on co-predication show that may
be the frequency of use of a given word has a special role on
the acceptability of co-predication between different senses of
a nominalization.
15:00 Pepijn Kokke. Formalising
type-logical grammars in Agda
This is a talk about the proof assistant Agda. More
specifically, about using Agda to prove things and all the
advantages of doing so. Those advantages, as we shall
explain, are that you: a) have a machine-checked
implementation of your theory; b) can compute with your proofs;
and c) can typeset Agda proofs so that the proofs you write are
the proofs you publish. The first half of this talk is going to
be spent introducing the Agda language, programming in Agda and
writing papers in literate Agda. The second half is going to be
spend giving an example of this process,
by
formalising the Lambek-Grishin calculus (LG) in Agda, discussing
a proof for cut-elimination in LG, and outlining a CPS
translation from LG into Agda. We will finish up by providing
several example analyses of sentences. [SLIDES]
Friday14:00 - 15:30
14:00 Seohyun Im and Chungmin Lee. A
Developed Analysis of Type Coercion Using Asher's TCL
and Conventionality
This
paper aims to propose a developed analysis of type coercion
phenomena such as "begin the book" based on Type Theory and
Conventional Non-linguistic Context, making a distinction
between linguistic and non-linguistic context. We argue that
linguistic and non-linguistic context as well as the lexical
meaning of the words are deeply involved in the interpretation
of a type-coerced construction. In the lexical semantic level,
the type-coerced construction is ambiguous. Although its
linguistic context can decrease the number of possible
interpretations of the construction in the process of
composition, it is still ambiguous until its non-linguistic
context disambiguates the meaning of the construction. More
importantly, we propose that the lexical meaning (type) of a
word is a conventionalized meaning under the assumption of a
conventional non-linguistic context linked to the word. The
context holds in the compositional process. Therefore, a
type-coerced construction has a preferred interpretation
derived from its conventional non-linguistic context, if no
specific non-linguistic context (the situation of utterance)
is provided and its linguistic context is neutral. For
instance, the preferred interpretation of "begin the book" is
to begin reading the book, because the conventional
non-linguistic context of "book" is the situation of reading
the book. However, the preference is just a probability and
the construction is still ambiguous. To sum up, the ambiguity
of a type-coerced construction is resolved through the three
levels: from lexical semantics (conventional non-linguistic
context), to compositional semantics (linguistic context) and
to pragmatics (non-linguistic context).
14:30 Ribeka Tanaka, Koji
Mineshima and Daisuke Bekki. Factivity and Presupposition in
Dependent Type Semantics
Dependent Type Semantics (DTS) is a framework of natural
language semantics based on dependent type theory. In
contrast to traditional model-theoretic semantics, DTS is a
proof-theoretic semantics where entailment relations are
characterized as provability relations between semantic
representations. Two distinctive features of DTS, as
compared to other type-theoretical frameworks, are that (i) it
is augmented with underspecified terms so as to provide a
unified analysis of entailment, anaphora and presupposition from
an inferential/computational perspective; and (ii) it gives a
fully compositional account of inferences involving anaphora. In
this paper, we present an analysis of entailment and
presupposition associated with factive verbs within the
framework of DTS. Factive attitude verbs such as "know"
are distinguished from non-factive attitude verbs such as
"believe" in that they introduce presuppositional
inferences. We propose different forms of semantic
representations for factive verbs and non-factive verbs: we
analyze factive verbs as predicates taking a proof term as
argument, and non-factive verbs as predicates taking a
proposition in the sense of dependent type theory. Our
theory also accounts for inferential properties of factive and
non-factive verbs taking NP-complements: for example, "S
believes the hypothesis that P" implies "S believes that P",
whereas "S knows the hypothesis that P" does not imply "S knows
that P".
15:00 Robin
Cooper (and Christian Retoré). Final summary and
discussion: emerging themes in type theory and lexical
semantics (from the above articles)
Robin
Cooper (University of Gothenburg, CoChair),
Christian
Retoré (Université de Montpellier, &
LIRMM CoChair)
Alexandra
Arapinis (CNR, Trento)
Nicholas
Asher (CNRS, Toulouse)
Christian
Bassac (Université Lyon II)
Stergios
Chatzikyriakidis (CNRS et LRIMM,
Montpellier)
Shalom
Lappin (King’s College, London)
Zhaohui
Luo (Royal Holloway, University of London)
Chiara Melloni
(CNR, Verona)
Bruno
Mery (Université de Bordeaux)
Richard
Moot (CNRS, Bordeaux)
Glyn
Morrill (Universitat Polytècnica de
Catalunya, Barcelona)
Larry
Moss (Indiana University, Bloomington)
Reinhard
Muskens (Universiteit Tilburg)
Livy Real (IBM
Research, Saõ Paolo)