Dependent event types

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.