[TYPES/announce] workshop TYTLES TYpe Theory and LExical Semantics (August 3-7 ESSLLI , Barcelone)

[Christian RETORE]

call for participation /  program with abstracts 
TYTLES TYpe Theory and LExical Semantics (Cooper, Retoré) 
for registration and practical information see: http://www.esslli2015.org

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. Using Type Theory to deal with lexical phenomena is an active research theme, with an increasing presence in various formal/computational semantic journals and conferences and valuable type theoretical contributions on incorporating lexical considerations into compositional semantics.

The topics to be addressed include:
	• Linguistically motivated extensions of current type theories
	• Lexical semantics in type theory
	• Interaction between lexical semantics and type theoretical semantics
	• Classical semantic questions in richly typed frameworks:
	• Modelling specific questions in type theory:
	• Lexical semantics, type theoretical semantics and computational implementation 


PROGRAM 

Monday14:00-15:30

14:00 Christian Retoré (and Robin Cooper), Introduction cf. workshop presentation 

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 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).

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. 

Friday14:00 - 15:30

14:00 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.

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)

Program committee 

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)
--
Christian RETORE 
Université de Montpellier  & LIRMM 
http://www.lirmm.fr/~retore