Skip to main content
SpringerLink
Log in

Adapting Type Theory with Records for Natural Language Semantics

  • Chapter
  • First Online:
Modern Perspectives in Type-Theoretical Semantics

Part of the book series: Studies in Linguistics and Philosophy ((SLAP,volume 98))

Abstract

In this paper we will go through the version of type theory TTR (Type Theory with Records) that we have proposed in a number of publications (including, Cooper, Res Lang Comput, 3:333–362, 2005a, J Log Comput, 15(2):99–112, 2005b, Handbook of the philosophy of science, volume 14: Philosophy of linguistics, 2012) and discuss the motivation for some choices that we have made which make it differ from other more standard modern type theories. We will relate TTR to the kind of type theory used in traditional formal semantics, characterizing more modern type theories as rich type theories with a greater variety of types. TTR, unlike many rich type theories, allows objects to be of several types and introduces both a kind of intensionality and modality. While TTR uses the idea that propositions should be modelled by types, it does not complete follow the Curry-Howard Correspondence introducing intersection and union types for a more classical treatment of conjunction and disjunction. It uses record types in place of \(\varSigma \)-types and uses dependent types for several aspects of linguistic analysis.

An earlier version of this paper was presented as an invited talk at the workshop on Natural Language and Computer Science, in association with the conference Logic in Computer Science, 2013, New Orleans, USA. I am grateful to the participants of this workshop for comments and in particular for clarifying discussion with Valeria de Paiva both during and after the workshop. This research was supported in part by VR project 2009–1569, Semantic analysis of interaction and coordination in dialogue (SAICD) and by VR project VR 2013–4873, Networks and Types (NetTypes).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

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 89.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 119.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 119.99
Price excludes VAT (USA)
  • Durable hardcover 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

Institutional subscriptions

Notes

  1. 1.

    This definition was not present in Cooper (2012).

  2. 2.

    This clause has been modified since (Cooper 2012) where it was a conditional rather than a biconditional.

  3. 3.

    This definition has been modified since (Cooper 2012) to make PType and Type be relativized to the model M.

References

  • Aristotle. (2007). On rhetoric: A theory of civic discourse (2nd ed.). Oxford: Oxford University Press (translated with Introduction, Notes, and Appendices by George A. Kennedy).

    Google Scholar 

  • Austin, J. L. (1961). Truth. In J. O. Urmson & G. J. Warnock (Eds.), J. L. Austin: Philosophical Papers. Oxford: Oxford University Press.

    Google Scholar 

  • Barsalou, L. W. (1992). Frames, concepts, and conceptual fields. In A. Lehrer & E. F. Kittay (Eds.), Frames, fields, and contrasts: New essays in semantic and lexical organization (pp. 21–74). Hillsdale, NJ: Lawrence Erlbaum Associates.

    Google Scholar 

  • Barwise, J., & Cooper, R. (1981). Generalized quantifiers and natural language. Linguistics and Philosophy, 4(2), 159–219.

    Article  Google Scholar 

  • Barwise, J., & Perry, J. (1983). Situations and attitudes. Cambridge, Mass: Bradford Books, MIT Press.

    Google Scholar 

  • Bellin, G., de Paiva, V., & Ritter, E. (2001). Extended Curry-Howard correspondence for a basic constructive modal logic. In Proceedings of Methods for Modalities.

    Google Scholar 

  • Betarte, G. (1998). Dependent record types and algebraic structures in type theory. Ph.D. thesis, Department of Computing Science, University of Gothenburg and Chalmers University of Technology.

    Google Scholar 

  • Betarte. G., & Tasistro, A. (1998). Extension of Martin-Löf’s type theory with record types and subtyping. In G. Sambin & J. Smith (Eds.), Twenty-five years of constructive type theory. Oxford Logic Guides (Vol. 36). Oxford: Oxford University Press.

    Google Scholar 

  • Bierman, G. M., & de Paiva, V. C. (2000). On an intuitionistic modal logic. Studia Logica, 65(3), 383–416.

    Article  Google Scholar 

  • Breitholtz, E. (2010). Clarification requests as enthymeme elicitors. In Aspects of Semantics and Pragmatics of Dialogue. SemDial 2010, 14th Workshop on the Semantics and Pragmatics of Dialogue. http://www.semdial2010.amu.edu.pl/separate_papers/19.pdf.

  • Breitholtz, E. (2011). Enthymemes under discussion: Towards a micro-rhetorical approach to dialogue modelling. In Proceedings of SPR-11 ILCLI International Workshop on Semantics, Pragmatics, and Rhetoric Donostia. Retrieved November 9–11, 2011.

    Google Scholar 

  • Breitholtz, E. (2014a). Enthymemes in Dialogue: A mico-rhetorical approach. Ph.D. thesis, University of Gothenburg.

    Google Scholar 

  • Breitholtz, E. (2014b). Reasoning with topoi – towards a rhetorical approach to non-monotonicity. In Proceedings of AISB Symposium on “Questions, Discourse and Dialogue: 20 Years After Making it Explicit”.

    Google Scholar 

  • Breitholtz, E., & Cooper, R. (2011). Enthymemes as rhetorical resources. In R. Artstein, M. Core, D. DeVault, K. Georgila, E. Kaiser & A. Stent (Eds.), SemDial 2011 (Los Angelogue): Proceedings of the 15th Workshop on the Semantics and Pragmatics of Dialogue. http://projects.ict.usc.edu/nld/semdial2011/semdial2011-proce edings.pdf.

  • Chierchia, G. (1995). Dynamics of meaning: Anaphora, presupposition, and the theory of grammar. Chicago: University of Chicago Press.

    Book  Google Scholar 

  • Chierchia, G., & Turner, R. (1988). Semantics and property theory. Linguistics and Philosophy, 11(3), 261–302.

    Article  Google Scholar 

  • Chomsky, N. (1965). Aspects of the theory of syntax. Cambridge: MIT Press.

    Google Scholar 

  • Cooper, R. (2005a). Austinian truth, attitudes and type theory. Research on Language and Computation, 3, 333–362.

    Article  Google Scholar 

  • Cooper, R. (2005b). Records and record types in semantic theory. Journal of Logic and Computation, 15(2), 99–112.

    Article  Google Scholar 

  • Cooper, R. (2008). Type theory with records and unification-based grammar. In F. Hamm & S. Kepser (Eds.), Logics for linguistic structures (pp. 9–34). Berlin: Mouton de Gruyter.

    Google Scholar 

  • Cooper, R. (2010). Frames in formal semantics. In H. Loftsson, E. Rögnvaldsson & S. Helgadóttir (Eds.), IceTAL 2010. Berlin: Springer.

    Google Scholar 

  • Cooper, R. (2011). Copredication, quantification and frames. In S. Pogodalla & J.-P. Prost (Eds.), LACL 2011. LNCS (LNAI), (Vol. 6736, pp. 64–79). Berlin: Springer.

    Google Scholar 

  • Cooper, R. (2012). Type theory and semantics in flux. In R. Kempson, N. Asher & T. Fernando (Eds.), Handbook of the philosophy of science, volume 14: Philosophy of linguistics (pp. 271–323). Elsevier BV. General editors: Dov M. Gabbay, Paul Thagard and John Woods.

    Google Scholar 

  • Cooper, R. (2014). How to do things with types. In V. de Paiva, W. Neuper, P. Quaresma, C. Retoré, L. S. Moss, & J. Saludes (Eds.), Joint Proceedings of the Second Workshop on Natural Language and Computer Science (NLCS 2014) & 1st International Workshop on Natural Language Services for Reasoners (NLSR 2014) July 17–18, 2014 Vienna (pp. 149–158). Austria: Center for Informatics and Systems of the University of Coimbra.

    Google Scholar 

  • Cooper, R. (2015). Frames as records. In A. Foret, G. Morrill, R. Muskens, & R. Osswald (Eds.), Preproceedings of the 20th Conference on Formal Grammar. http://fg.phil.hhu.de/2015/Preproceedings-FG-2015.pdf.

  • Cooper, R. (2016, in prep). Type theory and language: From perception to linguistic communication, draft of book chapters. https://sites.google.com/site/typetheorywithrecords/drafts.

  • Cooper, R., & Ginzburg, J. (2015). Type theory with records for natural language semantics. In Lappin and Fox (pp. 375–407).

    Google Scholar 

  • Coquand, T., Pollack, R., & Takeyama, M. (2004). A logical framework with dependently typed records. Fundamenta Informaticae XX:1–22

    Google Scholar 

  • Davidson, D. (1980). Essays on actions and events. Oxford: Oxford University Press (new edition 2001).

    Google Scholar 

  • de Paiva, V. (2003) Natural deduction and context as (constructive) modality. In Modeling and Using Context, Proceedings of the 4th International and Interdisciplinary Conference CONTEXT 2003. Springer Lecture Notes in Artificial Intelligence, (Vol. 2680). Stanford, CA, USA: Springer.

    Google Scholar 

  • Fernando, T. (2004). A finite-state approach to events in natural language semantics. Journal of Logic and Computation, 14(1), 79–92.

    Article  Google Scholar 

  • Fernando, T. (2015). The semantics of tense and aspect: A finite-state perspective. In Lappin and Fox.

    Google Scholar 

  • Fillmore, C. J. (1982). Frame semantics. Linguistics in the morning calm (pp. 111–137). Seoul: Hanshin Publishing Co.

    Google Scholar 

  • Fillmore, C. J. (1985). Frames and the semantics of understanding. Quaderni di Semantica, 6(2), 222–254.

    Google Scholar 

  • Fox, C., & Lappin, S. (2005). Foundations of intensional semantics. Oxford: Blackwell Publishing.

    Google Scholar 

  • Gibson, J. J. (1986). The ecological approach to visual perception. Hillsdale: Lawrence Erlbaum Associates.

    Google Scholar 

  • Ginzburg, J. (1994). An update semantics for dialogue. In H. Bunt (Ed.), Proceedings of the 1st International Workshop on Computational Semantics. Tilburg: ITK, Tilburg University.

    Google Scholar 

  • Ginzburg, J. (2012). The interactive stance: Meaning for conversation. Oxford: Oxford University Press.

    Book  Google Scholar 

  • Ginzburg, J., & Sag, I. A. (2000). Interrogative investigations: The form, meaning, and use of English interrogatives. No. 123 in CSLI Lecture Notes. Stanford, California: CSLI Publications.

    Google Scholar 

  • Ginzburg, J., Cooper, R., & Fernando, T. (2014). Propositions, questions, and adjectives: A rich type theoretic approach. In R. Cooper, S. Dobnik, S. Lappin, & S. Larsson (Eds.), Proceedings of the EACL 2014 Workshop on Type Theory and Natural Language Semantics (TTNLS) (pp. 89–96) Gothenburg, Sweden: Association for Computational Linguistics. http://www.aclweb.org/anthology/W14-14.

  • Grice, H. (1975). Logic and conversation. In P. Cole & J. Morgan (Eds.), Speech acts, syntax and semantics (Vol. 3, pp. 41–58). New York: Academic Press.

    Google Scholar 

  • Grice, H. P. (1989). Studies in the way of words. Cambridge: Harvard University Press.

    Google Scholar 

  • Kallmeyer, L., & Osswald, R. (2013). Syntax-driven semantic frame composition in Lexicalized Tree Adjoining Grammars. Journal of Language Modelling, 1(2), 267–330.

    Article  Google Scholar 

  • Kamp, H. (1981). A theory of truth and discourse representation. In J. Groenendijk, T. Janssen & M. Stokhof (Eds.), Formal methods in the study of language. Mathematical Centre Tracts (Vol. 135). Amsterdam: Mathematisch Centrum.

    Google Scholar 

  • Kamp, H., & Reyle, U. (1993). From discourse to logic. Dordrecht: Kluwer.

    Google Scholar 

  • Kaplan, D. (1978). On the logic of demonstratives. Journal of Philosophical Logic, 8, 81–98.

    Google Scholar 

  • Lappin, S. (2012). An operational approach to fine-grained intensionality. In T. Graf, D. Paperno, A. Szabolcsi & J. Tellings (Eds.), Theories of everything: In honor of Ed Keenan (Vol. 17). UCLA Working Papers in Linguistics. Department of Linguistics, UCLA.

    Google Scholar 

  • Lappin, S. (2015). Curry typing, polymorphism, and fine-grained intensionality. In Lappin and Fox.

    Google Scholar 

  • Lappin, S., & Fox, C. (Eds.). (2015). The handbook of contemporary semantic theory (2nd ed.). Berlin: Wiley-Blackwell.

    Google Scholar 

  • Larsson, S. (2002). Issue-based dialogue management. Ph.D. thesis, University of Gothenburg.

    Google Scholar 

  • Larsson, S., & Traum, D. R. (2001). Information state and dialogue management in the TRINDI dialogue move engine toolkit. Natural Language Engineering, 6(3&4), 323–340.

    Article  Google Scholar 

  • Löbner, S. (2014). Evidence for frames from human language. In T. Gamerschlag, D. Gerland, W. Petersen, & R. Osswald (Eds.), Frames and concept types. Studies in Linguistics and Philosophy (Vol. 94, pp. 23–68). New York: Springer.

    Google Scholar 

  • Löbner, S. (2016, in prep). Functional concepts and frames. http://semanticsarchive.net/Archive/jI1NGEwO/Loebner_Function al_Concepts_and_Frames.pdf.

  • Luo, Z. (2010). Type-theoretical semantics with coercive subtyping. Proceedings of SALT, 20, 38–56.

    Article  Google Scholar 

  • Luo, Z. (2011). Contextual analysis of word meanings in type-theoretical semantics. In S. Pogodalla, & J.-P. Prost (Eds.), LACL 2011. LNCS (Vol. 6736, pp. 159–174). Berlin: Springer.

    Google Scholar 

  • Martin-Löf, P. (1984). Intuitionistic type theory. Naples: Bibliopolis.

    Google Scholar 

  • Montague, R. (1970). Universal grammar. Theoria, 36, 373–398.

    Article  Google Scholar 

  • Montague, R. (1973). The proper treatment of quantification in ordinary English. In J. Hintikka, J. Moravcsik, & P. Suppes (Eds.), Approaches to Natural Language: Proceedings of the 1970 Stanford Workshop on Grammar and Semantics (pp. 247–270). Dordrecht: Reidel Publishing Company.

    Google Scholar 

  • Montague, R. (1974). Formal philosophy: Selected papers of Richard Montague. New Haven: Yale University Press. (ed. and with an introduction by Richmond H. Thomason).

    Google Scholar 

  • Muskens, R. (2005). Sense and the computation of reference. Linguistics and Philosophy, 28(4), 473–504.

    Article  Google Scholar 

  • Muskens, R. (2013). Data semantics and linguistic semantics. In M. Aloni, M. Franke & F. Roelofsen (Eds.), The dynamic, inquistive, and visionary life of  \(\phi , ? \phi ,\,{and}\,\Diamond \phi \) : A festschrift for Jeroen Groenendijk, Martin Stokhof, and Frank Veltman (pp. 175–183). http://www.illc.uva.nl/Festschrift-JMF/.

  • Pogodalla, S., Prost, J. P. (Eds.). (2011). Logical Aspects of Computational Linguistics: 6th International Conference, LACL 2011 (Vol. 6736). Berlin: Springer.

    Google Scholar 

  • Ranta, A. (1994). Type-theoretical grammar. Oxford: Clarendon Press.

    Google Scholar 

  • Ranta, A. (2011). Grammatical framework: Programming with multilingual grammars. Stanford: CSLI Publications.

    Google Scholar 

  • Sag, I. A., Wasow, T., & Bender, E. M. (2003). Syntactic Theory: A Formal Introduction, (2\(^{\rm nd}\) ed.). Stanford: CSLI Publications. http://cslipublications.stanford.edu/site/1575864002.html.

  • Sundholm, G. (1986). Proof theory and meaning. In D. Gabbay & F. Guenthner (Eds.), Handbook of philosophical logic (Vol. III). Dordrecht: Reidel.

    Google Scholar 

  • Tasistro, A. (1997). Substitution, record types and subtyping in type theory, with applications to the theory of programming. Ph.D. thesis, Department of Computing Science, University of Gothenburg and Chalmers University of Technology.

    Google Scholar 

  • Thomason, R. H. (1980). A model theory for propositional attitudes. Linguistics and Philosophy, 4, 47–70.

    Article  Google Scholar 

  • Thomason, R. H. (1988). Motivating ramified type theory. In G. Chierchia, B. H. Partee, & R. Turner (Eds.), Properties, types and meanings, volume I: Foundational issues. Dordrecht: Kluwer.

    Google Scholar 

  • Turner, R. (2005). Semantics and stratification. Journal of Logic and Computation, 15(2), 145–158.

    Article  Google Scholar 

  • Univalent Foundations Program T. (2013). Homotopy type theory: Univalent foundations of mathematics. https://homotopytypetheory.org.

Download references

Author information

Authors and Affiliations

  1. University of Gothenburg, Gothenburg, Sweden

    Robin Cooper

Authors
  1. Robin Cooper
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Robin Cooper .

Editor information

Editors and Affiliations

  1. University of Gothenburg, Sweden & Open University Cyprus, Gothenburg, Sweden

    Stergios Chatzikyriakidis

  2. Dept. of Computer Science, University of London Royal Holloway, London, United Kingdom

    Zhaohui Luo

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Cooper, R. (2017). Adapting Type Theory with Records for Natural Language Semantics. In: Chatzikyriakidis, S., Luo, Z. (eds) Modern Perspectives in Type-Theoretical Semantics. Studies in Linguistics and Philosophy, vol 98. Springer, Cham. https://doi.org/10.1007/978-3-319-50422-3_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-50422-3_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-50420-9

  • Online ISBN: 978-3-319-50422-3

  • eBook Packages: Social SciencesSocial Sciences (R0)

Publish with us

Policies and ethics

Search

Navigation