This paper is part of a broader project whose aim is to present a coherent uniﬁed approach to natural language dialogue semantics using tools from type theory. Here we explore aspects of our approach which relate to situation theory and situation semantics. We ﬁrst point out a relationship between type theory and the Austinian notion of truth. We then consider how records in type theory might be used to represent situations and how dependent record types can be used to model (...) constraints on situations. We then sketch treatments of attitude phenomena for which Barwise and Perry proposed situation semantic analyses (perception complements, belief, the Pierre puzzle) as well as two other intensional phenomena (intensional verbs and intentional identity). Finally we give a characterisation of the type theory used and a small illustrative fragment of English. (shrink)
A statement is said to be true when the historic state of affairs to which it is correlated by the demonstrative conventions (the ones to which it ‘refers’) is of a type with which the sentence used in making it is correlated by the descriptive conventions.
For several years the research group at our Dialogue Systems Lab has been involved in the development of the information state update approach to the building of dialogue systems and in particular Issue based dialogue management developed in Staffan Larsson's PhD thesis and based on Jonathan Ginzburg's gameboard approach to dialogue, focussing on the notion of questions (or issues) under discussion. Larsson's computational approach to information state updates involves a large collection of update rules which fire when certain conditions in (...) the information state are met in a regime determined by a general control algorithm. An utterance by a dialogue participant will in general unleash a whole chain of such updates and part of the power of the approach lies in the fact that we can define very general update rules which have small effects on the information state and which are not necessarily linked to any particular form of utterance. It gives us a much finer grain on update rules than thinking in terms of single monolithic updates associated with speaker utterances. (shrink)
We propose a record type theoretical account of cases of copredication which have motivated the introduction of dot types in the Generative Lexicon (Asher and Pustejovsky, 2005). We will suggest that using record types gives us a simple and intuitive account of dot types and also makes a connection between copredication and the use of hypothetical contexts in a record type theoretic analysis of dynamic generalized quantiﬁers. We propose a view of lexical innovation which draws both on Pustejovsky’s original (...) work on the Generative Lexicon (Pustejovsky, 1995) and the notion of resource present in the Grammatical Framework (Ranta, forthcoming). (shrink)
In most language technology applications that include a lexicon, this lexicon is a collection of static accounts of the properties of words, such as their meaning. However, in human conversations it is often the case that word-meaning is adjusted to ﬁt the context. Pustejovsky’s  theory of the Generative Lexicon explores some regular ways in which word meanings shift in context and thus represents an important step towards the implementation of systems which can assign meanings to words dynamically depending on (...) the context in which they occur. (shrink)
We shall consider a formulation of generalised quantiﬁers using type theory with records (TTR). TTR follows closely the development of record types in Martin-L¨of or constructive type theory but differs in that the type theory is deﬁned on a classical set theoretic basis. This means that the classical set-theoretic approach to generalised quantiﬁers can be imported into the type theoretic framework. The result is, I believe, equivalent to the proposal for dynamic generalised quantiﬁers in Chierchia (1995). The use of dependent (...) types provides us with an elegant approach to the formulation of dynamic quantiﬁers. We use a notion of hypothetical context which we have used elsewhere to give accounts of intentional identity, answers to questions and information state updates in dialogue management. We suggest that this points towards a general theory of hypothetical context in natural language. We suspect also that our analysis using records will support analyses of common noun phrase and verb-phrase anaphora and also facilitate representations which are underspeciﬁed with respect to quantiﬁer scope, though we leave the investigation of this to future research. (shrink)
• languages as sets of strings and early transformational grammar • interpreted languages as sets of string-meaning pairs • Montague in ‘Universal Grammar’: There is in my opinion no important theoretical diﬀerence between natural languages and the artiﬁcial languages of logicians; indeed I consider it possible to comprehend the syntax and semantics of both kinds of languages within a single natural and mathematically precise theory.
Within the community of researchers applying type theory to natural language there have been proposals to use contexts from type theory to model information states and to use context extension to model information updates. Examples of this are Ranta (1994) and research conducted in the DenK project (e.g. Ahn, 1995, Ahn and Borghuis, 1998).
In a recent paper Asher and Pustejovsky propose a type theoretical approach to account for cases of copredication which had motivated Pustejovsky to introduce dot types in the Generative Lexicon. In this paper I will propose an alternative treatment to that given by Asher and Pustejovsky using type theory with records. I will suggest that using record types not only gives us a simple and intuitive account of dot types but also makes an important connection between copredication and (...) the use of hypothetical contexts in dynamic generalized quantiﬁers I have proposed in earlier work. More generally it allows us to preserve the intuitive feature structure based accounts of lexical analysis proposed in Pustejovsky’s original work on the Generative Lexicon while at the same time introducing functions and binding in the way that is necessary for giving formal accounts of compositional semantics. (shrink)
I will explore possibilities for formulating linguistic semantics in terms of records and record types of the kind used in recent developments of Martin-L¨of type theory (Betarte, 1998, Betarte and Tasistro, 1998, Coquand, Pollock and Takeyama, 2003, Tasistro, 1997). I will suggest that they give us the tools to develop a theory which includes aspects of Montague semantics, using the lambda calculus1, Discourse Representation Theory (DRT)2, situation semantics3 and Head-Driven Phrase Structure Grammar (HPSG)4 in a single theory. I will also (...) argue that formulating these theories in terms of record types may provide us not only with a uniﬁed approach but also with certain improvements over the individual theories. (shrink)
The work reported here is of two sorts. One the one hand, we attempt to consolidate a lot of recent work on situation theory into a workable version, one that researchers can use and add to in ways that might be suitable for various applications. On the other, we attempt to solve a representational problem with situation theory: how can we represent complicated situation-theoretic objects in a way that is perspicuous. Our way in to the latter problem comes from (...) an on-going project aimed at bringing insights from Discourse Representation Theory and Situation Theory to bear on one another. In terms of this project, this paper represents a rather modest contribution. Our goal is to design a language for representing situationtheoretic objects that is based on Kamp's discourse representation structures (drss). This was where we started but we found that working on the notation and its semantics led us to clari cations of various aspects of situation theory. A major part of the clari cation in the theory comes from our use of the work on parameters and abstraError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapError: Illegal entry in bfrange block in ToUnicode CMapction by Aczel and Lunnon AL].. (shrink)
We suggest a way of bringing together type theory and uniﬁcation-based grammar formalisms by using records in type theory. The work is part of a broader project whose aim is to present a coherent uniﬁed approach to natural language dialogue semantics using tools from type theory.
We propose a shift in perspective from the view of natural languages as formal languages to natural languages as a collection of resources for constructing local languages for use in particular situations. This is suggested by our experience constructing natural language grammars for particular applications using the Grammatical Framework. It points to a research programme investigating how such resources play a role in linguistic innovation by agents constructing situation-speciﬁc local languages and how they can be made dynamic, modiﬁed by the (...) linguistic agent’s exposure to innovative linguistic data. (shrink)
This paper introduces a formal view of the semantics and pragmatics of corrective feedback in dialogues between adults and children. The goal of this research is to give a formal account of language coordination in dialogue, and semantic coordination in particular. Accounting for semantic coordination requires (1) a semantics, i.e. an architecture allowing for dynamic meanings and meaning updates as results of dialogue moves, and (2) a pragmatics, describing the dialogue moves involved in semantic coordination. We illustrate the general approach (...) by applying it to some examples from the literature on corrective feedback, and provide a fairly detailed discussion of one example using TTR (Type Theory with Records) to formalize concepts. TTR provides an analysis of linguistic content which is structured in order to allow modiﬁcation and similarity metrics, and a framework for describing dialogue moves and resulting updates to linguistic resources. (shrink)
Intuitively Austinian propositions are propositions that tell us something about a situation In this paper we will consider Austinian propositions and the associated notion that situations support infons which are to be found in situation theory and situation semantics We will try to tease out the consequences of taking the Austinian approach advocated in situation semantics as opposed to a very similar approach originally proposed by Davidson That is that event predicates where events are to be generally conceived so as (...) to be more like the notion of sit uation i e including states and processes are taken to have an argument position for an event We will do this comparison with respect to an area of data that was part of the original motivation for situation semantics naked in nitive perception complements see Barwise and Perry We will see that negative descriptions of events are one area where the Austinian and Davidsonian approaches make dif ferent predictions and at the end of the paper we will brie y consider negative event descriptions more generally with particular reference to the DRT analysis based on a Davidsonian approach as exempli ed by Amsili and Le Draoulec this volume.. (shrink)
We present a sketch of a formulation of an analysis of clarification ellipsis using dependent record types as they have been developed in Martin-Lof type theory. Record types provide a semantic formalism which at the same time..
1This work was supported in part by the projects TRINDI (Task Oriented Instructional Dialogue), EC Project LE4-8314, SDS (Swedish Dialogue Systems), NUTEK/HSFR Language Technology Project F1472/1997, INDI (Information Exchange in Dialogue), Riksbankens Jubileumsfond 1997-0134, and SIRIDUS (Specification, Interaction, Reconfiguration in Dialogue Understanding Systems), EC Project IST-1999-10516, and ILT (Interactive Language Technology), Vinnova Project 2001-6340. To appear in Presuppositions and Discourse ed. by Rainer Bäuerle, Uwe Reyle and Thomas Ede Zimmermann, Elsevier, Amsterdam.
We offer a computational analysis of the resolution of ellipsis in certain cases of dialogue clarification. We show that this goes beyond standard techniques used in anaphora and ellipsis resolution and requires operations on highly structured, linguistically heterogeneous representations. We characterize these operations and the representations on which they operate. We offer an analysis couched in a version of Head-Driven Phrase Structure Grammar combined with a theory of information states (IS).
The paper investigates an elliptical construction, Clarification Ellipsis, that occurs in dialogue. We suggest that this provides data that demonstrates that updates resulting from utterances cannot be defined in purely semantic terms, contrary to the prevailing assumptions of existing approaches to dynamic semantics. We offer a computationally oriented analysis of the resolution of ellipsis in certain cases of dialogue clarification. We show that this goes beyond standard techniques used in anaphora and ellipsis resolution and requires operations on highly structured, linguistically (...) heterogeneous representations. We characterize these operations and the representations on which they operate. We offer an analysis couched in a version of Head-Driven Phrase Structure Grammar combined with a theory of information states (IS) in dialogue. We sketch an algorithm for the process of utterance integration in IS which leads to grounding or clarification. The account proposed here has direct applications to the theory of attitude reports, an issue which is explored briefly in the concluding remarks of the paper. (shrink)
This paper shows how a dialogue system for information-seekingdialogues can be implemented in a type-theory-based syntax editor,originally developed for editing mathematical proofs.The implementation gives a simple logical metatheory tosuch dialogue systems and also suggests new functions forthem, e.g., a local undo operation. The method developed provides alogically based declarative way of implementing simple dialoguesystems that is easy to port to new domains.