Skip to main content

Context-Passing and Underspecification in Dependent Type Semantics

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

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

Abstract

Dependent type semantics (DTS) is a framework of discourse semantics based on dependent type theory, following the line of Sundholm (Handbook of Philosophical Logic, 1986) and Ranta (Type-Theoretical Grammar, 1994). DTS attains compositionality as required to serve as a semantic component of modern formal grammars including variations of categorial grammars, which is achieved by adopting mechanisms for local contexts, context-passing, and underspecified terms. In DTS, the calculation of presupposition projection reduces to type checking, and the calculation of anaphora resolution and presupposition binding both reduce to proof search in dependent type theory, inheriting the paradigm of anaphora resolution as proof construction.

Our sincere thanks to Kenichi Asai, Nicholas Asher, Kentaro Inui, Yusuke Kubota, Sadao Kurohashi, Robert Levine, Zhaohui Luo, Ribeka Tanaka and Ayumi Ueyama for many insightful comments. We also thank to Youyou Cong, Yuri Ishishita, Ayako Nakamura, Yuki Nakano, Miho Sato and Maika Utsugi for helpful discussions. This research is partially supported by JST, CREST.

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

Access this chapter

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.

    The representative version of dependent type theory is Martin-Löf Type Theory (MLTT) (Martin-Löf 1984), which is also known as Constructive Type Theory or Intensional Type Theory. In this article, we use the term “dependent type theory” as a term to refer to any type theory with dependent types, including MLTT, \(\lambda P\) (Barendregt 1992), Calculus of Construction (CoC) (Coquand and Huet 1988), and Unified Type Theory (UTT) (Luo 2012b).

  2. 2.

    The subscripts i and j signify that we focus on judgments under a specified reading in which the antecedent of it is a donkey in (1), and the antecedent of He is A man in (2).

  3. 3.

    Francez and Dyckhoff (2010) and Francez et al. (2010) also pursued a proof-theoretic semantics of natural language. The difference in their approach is that the meaning of a word itself is defined via its verification conditions, whereas in our approach the meaning of a word is represented by a term in dependent type theory, as a contribution to the meaning of a sentence it may participate in. Luo (2014) provides a comparison between Francez’s approach and dependent-theoretic approaches, together with an interesting discussion on the proof-theoretic and model-theoretic status of natural language semantics via dependent type theory.

  4. 4.

    DTS also employs a two-dimensional notation for \(\varSigma \)-types as shown in Definition 2, which is reminiscent of the notation for record types in Cooper (2005).

  5. 5.

    We denote the set of free variables in B by \(fv(B)\).

  6. 6.

    DTS employs two sorts: \( \textsf {type}\) and \( \textsf {kind}\), and its terms are stratified into three levels: terms of type A where A is a type, types of sort \( \textsf {type}\), kinds of sort \( \textsf {kind}\). The only axiom is (\( \textsf {type}F\)) in Definition 3. The (\(\varPi F\)) rule allows the four patterns (\( \textsf {type}\), \( \textsf {type}\)), (\( \textsf {type}\), \( \textsf {kind}\)), (\( \textsf {kind}\), \( \textsf {type}\)) and (\( \textsf {kind}\), \( \textsf {kind}\)) as in Definition 1, and the (\(\varSigma F\)) rule allows the three patterns (\( \textsf {type}\), \( \textsf {type}\)), (\( \textsf {type}\), \( \textsf {kind}\)) and (\( \textsf {kind}\), \( \textsf {kind}\)) as in Definition 2. Thus, in this article, DTS employs dependent type theory in which \( \textsf {type}\) is an impredicative universe with respect to \(\varPi \). This setting is stronger than the predicative dependent type theory that Bekki (2014) is founded on, but not too strong to construct a proof of Girard’s paradox (Girard 1972; Coquand 1986; Hook and Howe 1986). We are grateful to Zhaohui Luo (personal communication) for discussions and comments on this issue.

  7. 7.

    Following the notation in logic, we write \( \mathbf{farmer }(x)\) for \(( \mathbf{farmer }\, x)\) and \( \mathbf{own } (x,y)\) for \(( \mathbf{own }\, y)\, x\), and so on. More generally, for an n-place predicate \( \mathbf{f }\), we often write \( \mathbf{f }(x_1, \ldots , x_n)\) for \((\ldots ( \mathbf{f }\, x_n) \ldots x_1)\).

  8. 8.

    Here we use the notation in DTS.

  9. 9.

    Note that the notion of predicate in a dependently typed setting is different from that used in a simply typed setting—the type theory that underlies Montague semantics (Montague 1974) and the standard framework of formal semantics (Heim and Kratzer 1998). In the simply typed setting, we usually use base type e for the type of entities and t for the type of truth-values, that is, we have \(e: \textsf {type}\) and \(t: \textsf {type}\); given these base types, a one-place predicate is assigned type \(e\!\rightarrow \!t\) and a two-place predicate type \(e\!\rightarrow \!e\!\rightarrow \!t\), and so on. In our dependently typed setting, by contrast, we have \( \mathbf{entity }: \textsf {type}\) and assign type \( \mathbf{entity }\rightarrow \textsf {type}\) to one-place predicates and type \( \mathbf{entity }\rightarrow \mathbf{entity }\rightarrow \textsf {type}\) to two-place predicates. In this sense, a predicate in our setting is not a function from entities to truth-values (or, equivalently, a set of entities) but a function from entities to types (that is, propositions); note also that the meanings of types are specified in terms of inference rules, not in terms of their denotation.

  10. 10.

    The problem of negated and conditional forms of predicational sentences is discussed in Tanaka et al. (2015). See also Chatzikyriakidis and Luo (2016) and footnote 1 of that paper for more information.

  11. 11.

    For a recent survey on the interpretation of predicational sentences and predicate nominals, see Mikkelsen (2011).

  12. 12.

    See Sect. 4.2 for more discussion on the formation rule of negation.

  13. 13.

    We will give a more detailed discussion of the notion of presupposition in the context of dependent type theory in Sect. 4.

  14. 14.

    Sundholm (1989) gives an analysis of generalized quantifiers in the framework of dependent type theory in which common nouns are treated as types. Tanaka (2014) points out that Sundholm’s approach faces an “over-counting” problem in the interpretation of the proportional quantifier most, and provides a refined analysis by interpreting common nouns as predicates in the framework of DTS. Also, Tanaka et al. (2014) combines the framework of DTS with the semantics of modals that allows explicit quantification over possible worlds and applies it to the analysis of modal subordination phenomena.

  15. 15.

    The analysis of negation goes back to Chatzikyriakidis and Luo (2014).

  16. 16.

    The definition of the judgment of the form \(\varGamma \vdash M:A\) is that there exists a proof diagram from the assumptions \(\varGamma \) to the consequence M : A. The judgment of the form \(\varGamma \vdash A\ true \) holds if and only if there exists a proof term M such that \(\varGamma \vdash M:A\).

  17. 17.

    In DTS, we assume that the global context \(\mathcal {K}\) at least includes:

    • The basic ontological commitment (e.g. \( \mathbf{entity }: \textsf {type}\))

    • The arities of predicates (e.g. \( \mathbf{whitsle }: \mathbf{entity }\rightarrow \textsf {type}\))

    • Ontological knowledge (e.g. ).

  18. 18.

    The use of the (\( CONV \)) rule in (22) depends on the \(\beta \)-equivalence \( \mathbf{whistle }(\pi _1\pi _1t) =_{\beta } \mathbf{whistle }(\pi _1\pi _1(\pi _1t,\pi _1\pi _2t))\), which is omitted for the sake of space.

  19. 19.

    The dynamic conjunction rule is an extension of the progressive conjunction rule in Ranta (1994) with a context-passing mechanism.

  20. 20.

    The types of the context c and the pair of contexts (cu) are different. Thus, the two dynamic propositions M and N should be assigned different types. However, this does not require a polymorphic setting at the object-language level since M and N are preterms, and polymorphism is handled at the metalanguage level when type inference takes place.

  21. 21.

    Examples taken from “The Winograd Schema Challenge” (Levesque 2011), slightly adapted.

  22. 22.

    Bekki and Sato (2015) defined a fragment of dependent type theory with underspecified terms which has a decidable type-checking and inference algorithms.

  23. 23.

    See Soames (1989) and Beaver (2001) for useful surveys on the topic.

  24. 24.

    We abbreviate \(\lambda x_1 \ldots \lambda x_n.\, M\) as \(\lambda x_1 \ldots x_n.\, M\).

  25. 25.

    The treatment of gender information of pronoun as presuppositions goes back at least to Cooper (1983). See Sudo (2012) for a recent discussion.

  26. 26.

    See Tanaka et al. (2015) for more details. Earlier work using dependent type theory to analyze factivity includes Fox (1994b), Ranta (1994), and Krahmer and Piwek (1999).

References

  • Ahn, R., & Kolb, H.-P. (1990). Discourse representation meets constructive mathematics. In L. Kalman & L. Polos (Eds.), Papers from the Second Symposium on Logic and Language. Akademiai Kiado.

    Google Scholar 

  • Asher, N. (2011). Lexical Meaning in Context: A Web of Words. Cambridge: Cambridge University Press.

    Google Scholar 

  • Atlas, J., & Levinson, S. (1981). It-clefts, informativeness and logical form: Radical pragmatics. In P. Cole (Ed.), Radical Pragmatics (pp. 1–61). Cambridge: Academic Press.

    Google Scholar 

  • Barendregt, H. P. (1992). Lambda calculi with types. In S. Abramsky, D. M. Gabbay, & T. Maibaum (Eds.), Handbook of Logic in Computer Science (Vol. 2, pp. 117–309). Oxford: Oxford Science Publications.

    Google Scholar 

  • Beaver, D. I. (2001). Presupposition and Assertion in Dynamic Semantics. Studies in Logic, Language and Information. Stanford: CSLI Publications & FoLLI.

    Google Scholar 

  • Bekki, D. (2013). Dependent type semantics: an introduction. In the 2012 Edition of the LIRa Yearbook: A Selection of Papers. Amsterdam: University of Amsterdam.

    Google Scholar 

  • Bekki, D. (2014). Representing anaphora with dependent types. In N. Asher & S. V. Soloviev (Eds.), Proceedings of the Logical Aspects of Computational Linguistics (8th International Conference, LACL2014, Toulouse, France, June 2014), LNCS (Vol. 8535, pp. 14–29). Springer, Heiderburg.

    Google Scholar 

  • Bekki, D., & McCready, E. (2014). CI via DTS. In Proceedings of LENLS11 (pp. 110–123). Tokyo.

    Google Scholar 

  • Bekki, D., & Sato, M. (2015). Calculating projections via type checking. In The Proceedings of TYpe Theory and LExical Semantics (TYTLES), ESSLLI2015 Workshop. Barcelona, Spain.

    Google Scholar 

  • Bos, J. (2003). Implementing the binding and accommodation theory for anaphora resolution and presupposition projection. Computational Linguistics, 29(2), 179–210.

    Article  Google Scholar 

  • Chatzikyriakidis, S., & Luo, Z. (2014). Natural language inference in Coq. Journal of Logic, Language and Information, 23(4), 441–480.

    Article  Google Scholar 

  • Chatzikyriakidis, S., & Luo, Z. (2016). On the Interpretation of Common Nouns: Types v.s. Predicates. In Modern Perspectives in Type Theoretical Semantics, Studies of Linguistics and Philosophy. Heidelberg: Springer.

    Google Scholar 

  • Clark, H. H. (1975). Bridging. In S. Roger, & B. L. Nash-Webber (Eds.), In the Proceedings of TINLAP’75: Proceedings of the 1975 Workshop on Theoretical Issues in Natural Language Processing (pp. 169–174). Cambridge, Massachusetts. (Association for Computational Linguistics, Stroudsburg, PA, USA).

    Google Scholar 

  • Cooper, R. (1983). Quantification and Syntactic Theory. Dordrecht: Reidel.

    Book  Google Scholar 

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

    Article  Google Scholar 

  • Coquand, T. (1986). An analysis of Girard’s paradox. In The Proceedings of the First Symposium on Logic in Computer Science (pp. 227–236). IEEE Computer Society: Washington, D.C.

    Google Scholar 

  • Coquand, T., & Huet, G. (1988). The calculus of constructions. Information and Computation, 76(2–3), 95–120.

    Article  Google Scholar 

  • Dávila-Pérez, R. (1994). Translating English into Martin-Löf’s Theory of Types: A Compositional Approach, Technical report, University of Essex.

    Google Scholar 

  • Dávila-Pérez, R. (1995). Semantics and Parsing in Intuitionistic Categorial Grammar”, Ph.d. thesis, University of Essex.

    Google Scholar 

  • Dummett, M. (1975). What is a theory of meaning? In S. Guttenplan (Ed.), Mind and Language (pp. 97–138). Oxford: Oxford University Press.

    Google Scholar 

  • Dummett, M. (1976). What is a theory of meaning? (II). In Evans & McDowell (Eds.), Truth and Meaning (pp. 67–137). Oxford: Oxford University Press.

    Google Scholar 

  • Evans, G. (1980). Pronouns. Linguistic Inquiry, 11, 337–362.

    Google Scholar 

  • Fox, C. (1994a). Discourse representation, type theory and property theory. In H. Bunt, R. Muskens & G. Rentier (Eds.), The Proceedings of the International Workshop on Computational Semantics (pp. 71–80). Tilburg: Institute for Language Technology and Artificial Intelligence (ITK).

    Google Scholar 

  • Fox, C. (1994b). Existence presuppositions and category mistakes. Acta Linguistica Hungarica, 42(3/4), 325–339. (Published 1996).

    Google Scholar 

  • Francez, N., & Dyckhoff, R. (2010). Proof-theoretic semantics for a natural language fragment. Linguistics and Philosophy, 33(6), 447–477.

    Article  Google Scholar 

  • Francez, N., Dyckhoff, R., & Ben-Avi, G. (2010). Proof-theoretic semantics for subsentential phrases. Studia Logica, 94(3), 381–401.

    Article  Google Scholar 

  • Geach, P. (1962). Reference and Generality: An Examination of Some Medieval and Modern Theories. Ithaca, New York: Cornell University Press.

    Google Scholar 

  • Gentzen, G. (1935). Untersuchungen über das logische Schliessen I,II. Mathematische Zeitschrift 39, pp. 176–210, 405–431. (Translated as ‘Investigations into Logical Deduction’, and printed in M.E. Szabo, The Collected Works of Gerhard Gentzen, Amsterdam: North-Holland, 1969, pp. 68–131).

    Google Scholar 

  • Geurts, B. (1999). Presuppositions and Pronouns. Oxford: Elsevier.

    Google Scholar 

  • Girard, J.-Y. (1972). Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Thése de doctorat d’état: Université Paris VII.

    Google Scholar 

  • Groenendijk, J., & Stokhof, M. (1991). Dynamic predicate logic. Linguistics and Philosophy, 14, 39–100.

    Article  Google Scholar 

  • Heim, I. (1982). The Semantics of Definite and Indefinite Noun Phrases, Ph.d dissertation, University of Massachusetts. Published 1989 by Garland Press, New York.

    Google Scholar 

  • Heim, I., & Kratzer, A. (1998). Semantics in Generative Grammar. Malden: Blackwell Publishers.

    Google Scholar 

  • Hook, J. G., & Howe, D. J. (1986). Impredicative Strong Existential Equivalent to Type:Type, Technical Report TR 86–760. Department of Computer Science, Cornell University.

    Google Scholar 

  • Kamp, H. (1981). A theory of truth and semantic representation. In J. Groenendijk, T. M. Janssen & M. Stokhof (eds.), Formal Methods in the Study of Language. Amsterdam: Mathematical Centre Tract 135.

    Google Scholar 

  • Kamp, H., J. van Genabith, & U. Reyle. (2011). Discourse representation theory. In D. M. Gabbay & F. Gunthner (Eds.), Handbook of Philosophical Logic (Vol. 15, pp.125–394). Doredrecht, Springer.

    Google Scholar 

  • Karttunen, L. (1976). Discourse referents. In J. D. McCawley (Ed.), Syntax and Semantics 7: Notes from the Linguistic Underground (Vol. 7, pp. 363–385). New York: Academic Press.

    Google Scholar 

  • Krahmer, E., & Piwek, P. (1999). Presupposition projection as proof construction. In H. Bunt & R. Muskens (Eds.), Computing Meanings: Current Issues in Computational Semantics, Studies in Linguistics Philosophy Series. Dordrecht: Kluwer Academic Publishers.

    Google Scholar 

  • Kripke, S. (2009). Presupposition and anaphora: remarks on the formulation of the projection problem. Linguistic Inquiry, 40(3), 367–386.

    Article  Google Scholar 

  • Levesque, H. J. (2011). The winograd schema challenge. In The Proceedings of AAAI Spring Symposium: Logical Formalization of Commonsense Reasoning.

    Google Scholar 

  • Luo, Z. (2012a). Common nouns as types. In D. Béchet & A. Dikovsky (Eds.), Proceedings of the Logical Aspects of Computational Linguistics, 7th International Conference, LACL2012, Nantes, France, July 2012 (pp. 173–185). Heidelberg: Springer.

    Google Scholar 

  • Luo, Z. (2012b). Formal semantics in modern type theories with coercive subtyping. Linguistics and Philosophy, 35(6), 491–513.

    Google Scholar 

  • Luo, Z. (2014). Formal semantics in modern type theories: is it model-theoretic, proof-theoretic, or both? In N. Asher & S. V. Soloviev (Eds.), Logical Aspects of Computational Linguistics (8th International Conference, LACL2014, Toulouse, France, June 2014 Proceedings), LNCS 8535 (pp. 177–188). Toulouse: Springer.

    Google Scholar 

  • Magidor, O. (2013). Category Mistakes. Oxford: Oxford University Press.

    Google Scholar 

  • Martin-Löf, P. (1984). Intuitionistic Type Theory, G. Sambin (Ed.). Naples, Italy: Bibliopolis.

    Google Scholar 

  • Mikkelsen, L. (2011). Copular clauses. In Semantics: An International Handbook of Natural Language Meaning, HSK 33.2 (pp. 1805–1829). Berlin: de Gruyter.

    Google Scholar 

  • Mineshima, K. (2008). A presuppositional analysis of definite descriptions in proof theory. In: K. Satoh, A. Inokuchi, K. Nagao & T. Kawamura (Eds.), New Frontiers in Artificial Intelligence: JSAI 2007 Conference and Workshops, Revised Selected Papers, Lecture Notes in Computer Science (Vol. 4914, pp. 214–227). Heidelberg: Springer.

    Google Scholar 

  • Mineshima, K. (2013). Aspects of Inference in Natural Language, Ph.d. thesis, Keio University.

    Google Scholar 

  • Montague, R. (1974). Formal Philosophy. New Haven: Yale University Press.

    Google Scholar 

  • Nordström, B., Petersson, K., & Smith, J. (1990). Programming in Martin-Löf’s Type Theory. Oxford: Oxford University Press.

    Google Scholar 

  • Piwek, P., & Krahmer, E. (2000). Presuppositions in context: constructing bridges. In P. Bonzon, M. Cavalcanti, & R. Nossum (Eds.), Formal Aspects of Context, Applied Logic Series. Dordrecht: Kluwer Academic Publishers.

    Google Scholar 

  • Prawitz, D. (1980). Intuitionistic Logic: A Philosophical Challenge. In G. von Wright (Ed.), Logics and Philosophy. The Hague: Martinus Nijhoff.

    Google Scholar 

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

    Google Scholar 

  • Russell, B. (1919). Introduction to Mathematical Philosophy. Crows Nest: George Allen & Unwin.

    Google Scholar 

  • Soames, S. (1989). Presupposition. In D. Gabbay & F. Guenthner (Eds.), Handbook of Philosophical Logic (Vol. 4, pp. 553–616). Dordrecht: Reidel.

    Chapter  Google Scholar 

  • Steedman, M. J. (1996). Surface Structure and Interpretation. Cambridge: The MIT Press.

    Google Scholar 

  • Sudo, Y. (2012). On the semantics of Phi features on pronouns, Doctoral dissertation, MIT.

    Google Scholar 

  • Sundholm, G. (1986). Proof theory and meaning. In D. Gabbay & F. Guenthner (Eds.), Handbook of Philosophical Logic (Vol. III, pp. 471–506). Reidel: Kluwer.

    Google Scholar 

  • Sundholm, G. (1989). Constructive generalized quantifiers. Synthese, 79, 1–12.

    Article  Google Scholar 

  • Tanaka, R. (2014). A proof-theoretic approach to generalized quantifiers in dependent type semantics. In R. de Haan (Ed.), The Proceedings of the ESSLLI 2014 Student Session, 26th European Summer School in Logic, Language and Information (pp. 140–151). Tübingen, Germany.

    Google Scholar 

  • Tanaka, R., Mineshima, K., & Bekki, D. (2014). Resolving modal anaphora in dependent type semantics. In The Proceedings of the Eleventh International Workshop on Logic and Engineering of Natural Language Semantics (LENLS11), JSAI International Symposia on AI 2014 (pp. 43–56). Tokyo.

    Google Scholar 

  • Tanaka, R., Mineshima, K., Bekki, D. (2015). Factivity and presupposition in dependent type semantics. In The Proceedings of Type Theory and Lexical Semantics (TYTLES), ESSLLI2015 Workshop.

    Google Scholar 

  • Tanaka, R., Nakano, Y., & Bekki, D. (2013). Constructive generalized quantifiers revisited. In The Proceedings of Logic and Engineering of Natural Language Semantics 10 (LENLS 10) (pp. 69–78). Tokyo.

    Google Scholar 

  • van der Sandt, R. (1992). Presupposition projection as anaphora resolution. Journal of Semantics, 9, 333–377.

    Article  Google Scholar 

  • van der Sandt, R., & Geurts, B. (1991). Presupposition, anaphora, and lexical content. In O. Herzog & C.-R. Rollinger (Eds.), Text Understanding in LILOG (pp. 259–296). Berlin: Springer.

    Chapter  Google Scholar 

  • Watanabe, N., McCready, E., & Bekki, D. (2014). Japanese honorification: compositionality and expressivity. In S. Kawahara & M. Igarashi (Eds.), The Proceedings of FAJL 7: Formal Approaches to Japanese Linguistics, the MIT Working Papers in Linguistics 73 (pp. 265–276). International Christian University, Japan.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Daisuke Bekki .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Bekki, D., Mineshima, K. (2017). Context-Passing and Underspecification in Dependent Type 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_2

Download citation

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

  • 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