An Introduction to Dependent Type Semantics

Daisuke Bekki and Koji Mineshima

  • Area: LaLo
  • Level: A
  • Week: 1
  • Time: 14:00 – 15:30
  • Room: D1.03

Abstract

This course is intended to provide an introduction to natural language semantics based on dependent type theory (Martin-Löf 1984; Coquand and Huet 1988).  This discipline, which originated in Sundholm (1986) and Ranta (1994), has been paid much attention recently and extended in various ways (see Cooper 2005 and Luo 2012). From among these extensions, we plan to introduce the compositional framework Dependent Type Semantics (DTS; Bekki 2014), together with its empirical predictions on linguistic phenomena and its conceptual implications for the theory of meaning.

History and Motivation

This course introduces Dependent Type Semantics (DTS), a framework of natural language semantics via dependent type theory.

In the late 1980s, against the backdrop of the rapid development of mainstream discourse semantics such as Discourse Representation Theory (DRT), File Change Semantics, and Dynamic Predicate Logic, Martin-Löf and Sundholm noticed that dependent type theory, which is an extension of simply typed lambda calculus, may provide a solution to the discrepancy between syntactic structures and semantic representations (SRs) of donkey sentences (or, more generally, discourse anaphora). (1b) is an SR of the sentence (1a) given in Sundholm(1986), while (1c) is a first-order translation of (1a).

(1)
a. Every farmer who owns a donkey beats it.
b. (Πu: (Σx:farmer(x))(Σy: donkey(y))own(x,y)) beat(π1(u),π1(π2(u)))
c. ∀x(farmer(x) → ∀y(donkey(y) ∧ own(x,y)) → beat(x,y))

In dependent type theory, an SR of a declarative sentence is a type, which is a collection of proofs. A type (Πx:A)B (dependent function type) is a generalization of implication/function types A → B and universal types (∀x:A)B, while a type (Σx:A)B (dependent product type) is a generalization of conjunction/product types A ⨉ B and existential types (∃x:A)B. We observe that the structure of the SR (1b) parallels that of (1a), in the sense that the universal and the existential quantifications are respectively translated to Π and Σ, unlike (1c) where an indefinite a donkey is translated to the universal quantifier and the syntactic structure of (1a) is lost.

While the accessible anaphoric links are well represented, the inaccessible anaphora such as (2), listed in Karttunen (1976), are simply not representable with dependent types as Ranta (1994) argued. This is because universal quantification, implication, and negation are represented by Π-types that are data types of functions, from which the intended antecedents cannot be picked up. This is an explanation purely based on the structures of proofs, which is fundamentally different from that of DRT and other dynamic semantics.

(2)
a. Everybody bought a cari. *Iti stinks.
b. If John bought a cari, iti must be a Porsche. *Iti stinks.
c. John didn’t buy a cari. *Iti stinks.

This explanatory advantage launched a discipline of discourse semantics based on the dependent type theory: Ahn and Kolb (1990) proposed a translation algorithm from discourse representation structures to SRs in terms of dependent type theory. Perez (1995) proposed an integration of dependent type theory and Montagovian categorial grammar, and tried to provide a compositional setting (which has not been entirely successful, as discussed in Bekki (2014)). Then, the seminal work of Ranta (1994)—a compilation of this discipline in the mid-1990s—covers a broad range of linguistic phenomena including the anaphora inaccessibility mentioned above, descriptions, tense, and modality.

However, Ranta’s work is formulated as a theory of sentence generation, which needs to be reformulated if one is to adopt it as a semantic component of a modern formal syntactic theory. This problem further involves how to formulate a problem of anaphora resolution and presupposition binding/accommodation as achieved in van der Sandt (1992), Geurts (1999), and Bos (2003) within the DRT framework.

Interestingly, the pursuit of this problem led to works such as Krause (1995), Krahmer and Piwek (1999), Mineshima (2008) and Bekki (2014) attaining a paradigm called “anaphora resolution as proof construction,” which unified analyses of anaphora resolution and presupposition binding/accommodation, and analyses of sentential entailments. Moreover, within the framework of DTS in Bekki (2014), presupposition projections are simply calculated by type checking/inference algorithm of dependent type theory (Bekki and Sato 2015).

Course Plan

The content of this course is highly relevant to the ESSLLI2014 course by Chatzikyriakidis and Luo, titled “Formal Semantics in Modern Type Theories: Theory and Implementation.” However, our course may be of interest to both those who attended it and those who did not, for the following two reasons.

First, our course will focus more on the aspect of DTS as a semantic component of formal grammars. We will present a fully compositional version of DTS, which will meet the demands of researchers studying formal syntax who are looking for a discourse semantics that is a purely type-theoretical.

Second, we will start our course with an introduction to dependent type theory. There seems to be a relatively high barrier to entry for formal linguists seeking to learn semantic theories based on dependent type theory, since one is required to be familiar with proof theory and type theory, especially Martin-Löf type theory, which has a proof-theoretic semantics (see Dummett 1975, Dummett 1976, Prawitz 1980). The notion of proof-theoretic semantics is fundamentally different from that of model-theoretic semantics in which every representation is understood in terms of its semantic value (e.g., dependent type theory does not make use of concepts such as an assignment function, on which the analysis of accessibility in DRT is based). Our aim is to remove any such barrier, by introducing the fundamental notions of proof-theoretic semantics, comparing them with the corresponding notions in model-theoretic semantics.

Given that the empirical coverage of DTS is getting broader, we will discuss, among other things, representations of generalized quantifiers in Sundholm (1989), Fox and Lappin (2005), Tanaka et al. (2013), and Tanaka (2014); modality and factivity discussed in Ranta (1994), Tanaka (2014), and Tanaka et al. (2015); the phenomena of coercion discussed in Luo (2010,2011,2012a,2012b) and Asher and Luo (2012); a unified analysis of conventional implicatures and presuppositions in Bekki and McCready(2014).

We also plan to compare DTS with other proof-theoretic semantics of natural language, such as the ones proposed in Francez (2010a,2010b) and Luo (2012). The relation between DTS and theories of tropes such as in Moltmann (2007) may interest philosophers.

Course Outline

Day 1 : From Natural Deduction to Dependent Type Theory
  • Proof-theoretic semantics and model-theoretic semantics
  • Natural deduction
  • Curry-Howard Correspondence
  • Dependent types (Π-type and Σ-type)

Slide: Course outline
Slide: From natural deduction to dependent type theory

Day 2 : Dependent Type Semantics (Part I): Anaphora
  • Introducing the basic framework of DTS
  • Anaphora resolution in DTS
  • Bound variable anaphora, Donkey anaphora, E-type anaphora, Syllogistic anaphora, Accessibility

Slide: Dependent Type Semantics (DTS)

Day 3 : Dependent Type Semantics (Part II): Presupposition
  • Presupposition resolution via type-checking
  • A proof-theoretic account of presupposition projection
  • Applications: bridging, factive presupposition, Binding problem

Slide: Presuppositions

Day 4 : Dependent Type Semantics (Part III): More types
  • The interpretation of common nouns: types or predicates?
  • Natural number and finite types
  • Guest Lecture 1 (Ribeka Tanaka): Generalized quantifiers in Dependent Type Semantics

Slide: Common Nouns: types or predicates?
Slide: More dependent types
Slide: Generalized Quantifier in Dependent Type Semantics (by Ribeka Tanaka)

Day 5 : Computational and philosophical aspects of Dependent Type Semantics
  • Guest Lecture 2 (Pascual Martínez-Goméz): Computational semantics and recognizing textual entailment
  • Presupposition accommodation
  • A proof-theoretic turn in natural language semantics: Beyond context change potential

Slide: Introduction
Slide: Computational semantics and recognizing textual entailment
Slide: Proof-theoretic turn

Appendix

A formal presentation of dependent type theory

Selected References

Theoretical Background

Coquand, T. and G. Huet. (1988) “The Calculus of Constructions”, Information and Computation 76(2-3), pp.95–120.

Martin-Löf, P. (1984) Intuitionistic Type Theory, Vol. 17. Naples, Italy: Bibliopolis. Sambin, Giovanni (ed.).

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

Dependent Type Semantics

Bekki, D. (2014) “Representing Anaphora with Dependent Types”, In the Proceedings of N. Asher and S. V. Soloviev (eds.): Logical Aspects of Computational Linguistics (8th international conference, LACL2014, Toulouse, France, June 2014 Proceedings), LNCS 8535. Toulouse, pp.14–29, Springer, Heiderburg.

Bekki, D. and E. McCready. (2014) “CI via DTS”, In the Proceedings of LENLS11. Tokyo, pp.110–123.

Bekki, D. and M. Sato. (2015) “Calculating Projections via Type Checking”, In the Proceedings of TYpe Theory and LExical Semantics (TYTLES), ESSLLI2015 workshop. Barcelona, Spain.

Tanaka, R. (2014) “A Proof-Theoretic Approach to Generalized Quantifiers in Dependent Type Semantics”, In the Proceedings of R. de Haan (ed.): the ESSLLI 2014 Student Session, 26th European Summer School in Logic, Language and Information. Tübingen, Germany, pp.140–151.

Tanaka, R., K. Mineshima, and D. Bekki. (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. Tokyo, pp.43–56.

Tanaka, R., K. Mineshima, and D. Bekki. (2015) “Factivity and Presupposition in Dependent Type Semantics”, In the Proceedings of TYpe Theory and LExical Semantics (TYTLES), ESSLLI2015 workshop.

Anaphora and Presupposition

Bos, J. (2003) “Implementing the Binding and Accommodation Theory for Anaphora Resolution and Presupposition Projection”, Computational Linguistics 29(2), pp.179– 210.

Geurts, B. (1999) Presuppositions and pronouns. Elsevier, Oxford.

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

Dependent Types and Proof-Theoretic Semantics of Natural Language

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

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

Luo, Z. (2012a) “Common Nouns as Types”, In: D. B ́echet and A. Dikovsky (eds.): Logical Aspects of Computational Linguistics, 7th International Conference, LACL2012, Nantes, France, July 2012 Proceedings. Springer, pp.173–185.

Luo, Z. (2012b) “Formal Semantics in Modern Type Theories with Coercive Subtyping”, Linguistics and Philosophy 35(6).

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

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