Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Logic, Language, Information, and Computation

WoLLIC 2017: Logic, Language, Information, and Computation pp 216–228Cite as

Dependent Event Types

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10388))

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.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 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. 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. 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. 4.

    It may be worth mentioning that, in the setting of MTT-semantics, coercive subtyping [12, 14] is used and, for uniformity, we may adopt coercive subtyping rather than subsumptive subtyping, although in general subsumptive subtyping is simpler.

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

  1. Asher, N., Luo, Z.: Formalisation of coercions in lexical semantics. In: Sinn und Bedeutung, vol. 17, Paris (2012)

    Google Scholar 

  2. Champollion, L.: The interaction of compositional semantics and event semantics. Linguist. Philos. 38, 31–66 (2015)

    Article  Google Scholar 

  3. Chatzikyriakidis, S., Luo, Z. (eds.): Modern Perspectives in Type-Theoretical Semantics. Springer, Heidelberg (2017)

    Google Scholar 

  4. Chatzikyriakidis, S., Luo, Z.: Formal Semantics in Modern Type Theories. ISTE/Wiley (2018, to appear)

    Google Scholar 

  5. Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(1), 56–68 (1940)

    Article  MathSciNet  MATH  Google Scholar 

  6. Davidson, D.: The logical form of action sentences. In: Rothstein, S. (ed.) The Logic of Decision and Action. University of Pittsburgh Press, Pittsburgh (1967)

    Google Scholar 

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

    Google Scholar 

  8. Goguen, H.: A typed operational semantics for type theory. Ph.D. thesis, University of Edinburgh (1994)

    Google Scholar 

  9. Landman, F.: Plurality. In: Lappin, S. (ed.) The Handbook of Contemporary Semantic Theory (1996)

    Google Scholar 

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

    Google Scholar 

  11. Luo, Z.: Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, Oxford (1994)

    MATH  Google Scholar 

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

    Chapter  Google Scholar 

  13. Luo, Z.: Formal semantics in modern type theories with coercive subtyping. Linguist. Philos. 35(6), 491–513 (2012)

    Article  Google Scholar 

  14. Luo, Z., Soloviev, S., Xue, T.: Coercive subtyping: theory and implementation. Inf. Comput. 223, 18–42 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  15. Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis, Berkeley (1984)

    MATH  Google Scholar 

  16. Montague, R.: Formal Philosophy. Yale University Press, New Haven (1974). Collected papers Ed. by R. Thomason

    Google Scholar 

  17. Parsons, T.: Events in the Semantics of English. MIT Press, Cambridge (1990)

    Google Scholar 

  18. Ranta, A.: Type-Theoretical Grammar. Oxford University Press, Oxford (1994)

    MATH  Google Scholar 

  19. Williams, A.: Arguments in Syntax and Semantics. Cambridge University Press, Cambridge (2015)

    Book  Google Scholar 

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

    Chapter  Google Scholar 

  21. Xue, T.: Theory and implementation of coercive subtyping. Ph.D. thesis, Royal Holloway, University of London (2013)

    Google Scholar 

Download references

Acknowledgement

Thanks go to Stergios Chatzikyriakidis, David Corfield, Koji Mineshima and Christian Retoré for helpful comments on this work.

Author information

Authors and Affiliations

  1. Royal Holloway, University of London, Egham, Surrey, UK

    Zhaohui Luo

  2. IRIT, Toulouse, France

    Sergei Soloviev

Authors
  1. Zhaohui Luo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sergei Soloviev
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zhaohui Luo .

Editor information

Editors and Affiliations

  1. Department of Mathematics and Statistics, University of Helsinki, Helsinki, Finland

    Juliette Kennedy

  2. Centro de Informática, Recife, Pernambuco, Brazil

    Ruy J.G.B. de Queiroz

Rights and permissions

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

Publish with us

Policies and ethics

Search

Navigation