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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 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.
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.
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.
- 5.
We denote the set of free variables in B by \(fv(B)\).
- 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.
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.
Here we use the notation in DTS.
- 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.
- 11.
For a recent survey on the interpretation of predicational sentences and predicate nominals, see Mikkelsen (2011).
- 12.
See Sect. 4.2 for more discussion on the formation rule of negation.
- 13.
We will give a more detailed discussion of the notion of presupposition in the context of dependent type theory in Sect. 4.
- 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.
The analysis of negation goes back to Chatzikyriakidis and Luo (2014).
- 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.
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.
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.
The dynamic conjunction rule is an extension of the progressive conjunction rule in Ranta (1994) with a context-passing mechanism.
- 20.
The types of the context c and the pair of contexts (c, u) 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.
Examples taken from “The Winograd Schema Challenge” (Levesque 2011), slightly adapted.
- 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.
- 24.
We abbreviate \(\lambda x_1 \ldots \lambda x_n.\, M\) as \(\lambda x_1 \ldots x_n.\, M\).
- 25.
- 26.
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.
Asher, N. (2011). Lexical Meaning in Context: A Web of Words. Cambridge: Cambridge University Press.
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.
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.
Beaver, D. I. (2001). Presupposition and Assertion in Dynamic Semantics. Studies in Logic, Language and Information. Stanford: CSLI Publications & FoLLI.
Bekki, D. (2013). Dependent type semantics: an introduction. In the 2012 Edition of the LIRa Yearbook: A Selection of Papers. Amsterdam: University of Amsterdam.
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.
Bekki, D., & McCready, E. (2014). CI via DTS. In Proceedings of LENLS11 (pp. 110–123). Tokyo.
Bekki, D., & Sato, M. (2015). Calculating projections via type checking. In The Proceedings of TYpe Theory and LExical Semantics (TYTLES), ESSLLI2015 Workshop. Barcelona, Spain.
Bos, J. (2003). Implementing the binding and accommodation theory for anaphora resolution and presupposition projection. Computational Linguistics, 29(2), 179–210.
Chatzikyriakidis, S., & Luo, Z. (2014). Natural language inference in Coq. Journal of Logic, Language and Information, 23(4), 441–480.
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.
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).
Cooper, R. (1983). Quantification and Syntactic Theory. Dordrecht: Reidel.
Cooper, R. (2005). Austinian truth, attitudes and type theory. Research on Language and Computation, 3, 333–362.
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.
Coquand, T., & Huet, G. (1988). The calculus of constructions. Information and Computation, 76(2–3), 95–120.
Dávila-Pérez, R. (1994). Translating English into Martin-Löf’s Theory of Types: A Compositional Approach, Technical report, University of Essex.
Dávila-Pérez, R. (1995). Semantics and Parsing in Intuitionistic Categorial Grammar”, Ph.d. thesis, University of Essex.
Dummett, M. (1975). What is a theory of meaning? In S. Guttenplan (Ed.), Mind and Language (pp. 97–138). Oxford: Oxford University Press.
Dummett, M. (1976). What is a theory of meaning? (II). In Evans & McDowell (Eds.), Truth and Meaning (pp. 67–137). Oxford: Oxford University Press.
Evans, G. (1980). Pronouns. Linguistic Inquiry, 11, 337–362.
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).
Fox, C. (1994b). Existence presuppositions and category mistakes. Acta Linguistica Hungarica, 42(3/4), 325–339. (Published 1996).
Francez, N., & Dyckhoff, R. (2010). Proof-theoretic semantics for a natural language fragment. Linguistics and Philosophy, 33(6), 447–477.
Francez, N., Dyckhoff, R., & Ben-Avi, G. (2010). Proof-theoretic semantics for subsentential phrases. Studia Logica, 94(3), 381–401.
Geach, P. (1962). Reference and Generality: An Examination of Some Medieval and Modern Theories. Ithaca, New York: Cornell University Press.
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).
Geurts, B. (1999). Presuppositions and Pronouns. Oxford: Elsevier.
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.
Groenendijk, J., & Stokhof, M. (1991). Dynamic predicate logic. Linguistics and Philosophy, 14, 39–100.
Heim, I. (1982). The Semantics of Definite and Indefinite Noun Phrases, Ph.d dissertation, University of Massachusetts. Published 1989 by Garland Press, New York.
Heim, I., & Kratzer, A. (1998). Semantics in Generative Grammar. Malden: Blackwell Publishers.
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.
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.
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.
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.
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.
Kripke, S. (2009). Presupposition and anaphora: remarks on the formulation of the projection problem. Linguistic Inquiry, 40(3), 367–386.
Levesque, H. J. (2011). The winograd schema challenge. In The Proceedings of AAAI Spring Symposium: Logical Formalization of Commonsense Reasoning.
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.
Luo, Z. (2012b). Formal semantics in modern type theories with coercive subtyping. Linguistics and Philosophy, 35(6), 491–513.
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.
Magidor, O. (2013). Category Mistakes. Oxford: Oxford University Press.
Martin-Löf, P. (1984). Intuitionistic Type Theory, G. Sambin (Ed.). Naples, Italy: Bibliopolis.
Mikkelsen, L. (2011). Copular clauses. In Semantics: An International Handbook of Natural Language Meaning, HSK 33.2 (pp. 1805–1829). Berlin: de Gruyter.
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.
Mineshima, K. (2013). Aspects of Inference in Natural Language, Ph.d. thesis, Keio University.
Montague, R. (1974). Formal Philosophy. New Haven: Yale University Press.
Nordström, B., Petersson, K., & Smith, J. (1990). Programming in Martin-Löf’s Type Theory. Oxford: Oxford University Press.
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.
Prawitz, D. (1980). Intuitionistic Logic: A Philosophical Challenge. In G. von Wright (Ed.), Logics and Philosophy. The Hague: Martinus Nijhoff.
Ranta, A. (1994). Type-Theoretical Grammar. Oxford: Oxford University Press.
Russell, B. (1919). Introduction to Mathematical Philosophy. Crows Nest: George Allen & Unwin.
Soames, S. (1989). Presupposition. In D. Gabbay & F. Guenthner (Eds.), Handbook of Philosophical Logic (Vol. 4, pp. 553–616). Dordrecht: Reidel.
Steedman, M. J. (1996). Surface Structure and Interpretation. Cambridge: The MIT Press.
Sudo, Y. (2012). On the semantics of Phi features on pronouns, Doctoral dissertation, MIT.
Sundholm, G. (1986). Proof theory and meaning. In D. Gabbay & F. Guenthner (Eds.), Handbook of Philosophical Logic (Vol. III, pp. 471–506). Reidel: Kluwer.
Sundholm, G. (1989). Constructive generalized quantifiers. Synthese, 79, 1–12.
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.
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.
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.
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.
van der Sandt, R. (1992). Presupposition projection as anaphora resolution. Journal of Semantics, 9, 333–377.
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.
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.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)