Abstract
This paper studies how dependent types can be employed for a refined treatment of event types, offering a nice improvement to Davidson’s event semantics. We consider dependent event types indexed by thematic roles and illustrate how, in the presence of refined event types, subtyping plays an essential role in semantic interpretations. We consider two extensions with dependent event types: first, the extension of Church’s simple type theory as employed in Montague semantics that is familiar with many linguistic semanticists and, secondly, the extension of a modern type theory as employed in MTT-semantics. The former uses subsumptive subtyping, while the latter uses coercive subtyping, to capture the subtyping relationships between dependent event types. Both of these extensions have nice meta-theoretic properties such as normalisation and logical consistency; in particular, we shall show that the former can be faithfully embedded into the latter and hence has expected meta-theoretic properties. As an example of applications, it is shown that dependent event types give a natural solution to the incompatibility problem (sometimes called the event quantification problem) in combining event semantics with the traditional compositional semantics, both in the Montagovian setting with the simple type theory and in the setting of MTT-semantics.
Z. Luo—Partially supported by EU COST Action CA15123 and CAS/SAFEA International Partnership Program.
S. Soloviev—Also an associated researcher at ITMO Univ, St. Petersburg, Russia. Partially supported by EU COST Action CA15123 and Russian Federation Grant 074-U01.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
In logical formulas or lambda-expressions, people often omit the type labels of events and entities: for example, (2) would just be written as \( \exists e.\ kiss(e)\ \& \ agent(e,j)\ \& \ patient(e,m)\ \& \ passionate(e)\), since traditionally there are only one type of events and one type of entities; we shall put in the type labels explicitly. Another note on notations is: e and t in boldface stand for the type of entities and the type of truth values, respectively, as in MG, while e and t not in boldface stand for different things (for example, e would usually be used as a variable of an event type).
- 2.
Please note here that, for kiss(e) and passionate(e) to be well-typed, the type of event e must be the same as the domain of kiss and passionate – see the next section about subtyping, which allows them to be well-typed.
- 3.
Formally, we have \(\textsc {agent}_{AP}[a,p] = \lambda e : Evt_{AP}(a,p).a\), of type \(Evt_{AP}(a,p) \rightarrow Agent\). Usually we simply write, for example, \(\textsc {agent}_{AP}(e)\) for \(\textsc {agent}_{AP}[a,p](e)\).
- 4.
- 5.
A notational remark: in \(C_e\), C stands for ‘Church’ and e for ‘event’. The notation UTT[E] comes from the work of coercive subtyping (see, for example, [14]) where T[C] denotes type theory T extended by coercive subtyping whose basic subtyping are given as the set C of subtyping judgements.
- 6.
This section is rather formal and, for a reader less interested in formal matters, its details might be safely skipped if one wishes so.
- 7.
We only consider the intuitionistic \(\supset \) and \(\forall \) here, omitting other operators including, in particular, those about, e.g. negation/classical logic in [5]. Also, we shall not assume extensionality.
- 8.
Formally, this is a partial function – it is only defined when certain conditions hold. The embedding theorem shows that the embedding is total for well-typed terms. Also, a notional note: we shall use S and T to stand for types in UTT[E] where function types are special cases of \(\Pi \)-types: for any types S and T, \(S\rightarrow T = \Pi (S,[\_:S]T)\).
- 9.
Of course, one can argue that this is not intended since the agent is known, but formally, nothing prevents one from doing it.
References
Asher, N., Luo, Z.: Formalisation of coercions in lexical semantics. In: Sinn und Bedeutung, vol. 17, Paris (2012)
Champollion, L.: The interaction of compositional semantics and event semantics. Linguist. Philos. 38, 31–66 (2015)
Chatzikyriakidis, S., Luo, Z. (eds.): Modern Perspectives in Type-Theoretical Semantics. Springer, Heidelberg (2017)
Chatzikyriakidis, S., Luo, Z.: Formal Semantics in Modern Type Theories. ISTE/Wiley (2018, to appear)
Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(1), 56–68 (1940)
Davidson, D.: The logical form of action sentences. In: Rothstein, S. (ed.) The Logic of Decision and Action. University of Pittsburgh Press, Pittsburgh (1967)
de Groote, P., Winter, Y.: A type-logical account of quantification in event semantics. In: Logic and Engineering of Natural Language Semantics, vol. 11 (2014)
Goguen, H.: A typed operational semantics for type theory. Ph.D. thesis, University of Edinburgh (1994)
Landman, F.: Plurality. In: Lappin, S. (ed.) The Handbook of Contemporary Semantic Theory (1996)
Luo, Z.: A problem of adequacy: conservativity of calculus of constructions over higher-order logic. Technical report, LFCS report series ECS-LFCS-90-121, Department of Computer Science, University of Edinburgh (1990)
Luo, Z.: Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, Oxford (1994)
Luo, Z.: Coercive subtyping in type theory. In: Dalen, D., Bezem, M. (eds.) CSL 1996. LNCS, vol. 1258, pp. 275–296. Springer, Heidelberg (1997). doi:10.1007/3-540-63172-0_45
Luo, Z.: Formal semantics in modern type theories with coercive subtyping. Linguist. Philos. 35(6), 491–513 (2012)
Luo, Z., Soloviev, S., Xue, T.: Coercive subtyping: theory and implementation. Inf. Comput. 223, 18–42 (2012)
Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis, Berkeley (1984)
Montague, R.: Formal Philosophy. Yale University Press, New Haven (1974). Collected papers Ed. by R. Thomason
Parsons, T.: Events in the Semantics of English. MIT Press, Cambridge (1990)
Ranta, A.: Type-Theoretical Grammar. Oxford University Press, Oxford (1994)
Williams, A.: Arguments in Syntax and Semantics. Cambridge University Press, Cambridge (2015)
Winter, Y., Zwarts, J.: Event semantics and abstract categorial grammar. In: Kanazawa, M., Kornai, A., Kracht, M., Seki, H. (eds.) MOL 2011. LNCS (LNAI), vol. 6878, pp. 174–191. Springer, Heidelberg (2011). doi:10.1007/978-3-642-23211-4_11
Xue, T.: Theory and implementation of coercive subtyping. Ph.D. thesis, Royal Holloway, University of London (2013)
Acknowledgement
Thanks go to Stergios Chatzikyriakidis, David Corfield, Koji Mineshima and Christian Retoré for helpful comments on this work.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer-Verlag GmbH Germany
About this paper
Cite this paper
Luo, Z., Soloviev, S. (2017). Dependent Event Types. In: Kennedy, J., de Queiroz, R. (eds) Logic, Language, Information, and Computation. WoLLIC 2017. Lecture Notes in Computer Science(), vol 10388. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-55386-2_15
Download citation
DOI: https://doi.org/10.1007/978-3-662-55386-2_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-55385-5
Online ISBN: 978-3-662-55386-2
eBook Packages: Computer ScienceComputer Science (R0)