by Daisuke Bekki (Ochanomizu University)
This course provides a comprehensive overview of Dependent Type Semantics (DTS), a proof-theoretic semantics of natural language based on dependent type theory. DTS marks a departure from the traditional model-theoretic semantic frameworks, with its uniform analysis of projective contents such as anaphora, presupposition, and conventional implicatures through the process of proof construction. I will also reflect on the extensive research and developments of DTS over the past decade, from empirical linguistic research to computational research. The latter includes discussion on the integration of DTS and neural networks, which will shed light on our future prospects and provide insights into DTS's potential applications in computational linguistics.
This lecture will provide a comprehensive overview of Dependent Type Semantics (DTS: Bekki (2014), Bekki and Mineshima (2017), Bekki (2023)), a proof-theoretic semantics of natural language based on dependent type theory. DTS marks a departure from the traditional model-theoretic semantics in that the meaning of a sentence is given by its verification condition, which is represented by a type interpreted via Curry-Howard isomorphism where propositions are types and proofs are terms. In particular, DTS employs a type theory called \textit{underspecified dependent type theory} (UDTT), that is an extention of Martin-L\"of type theory (Martin L\”of 1984) with underspecified types (Bekki 2023). An underspecified type corresponds to an open proof in type theory, and to a semantic representation of anaphora and presupposition triggers in linguistics. This establishes a new correspondence between the meaning of natural language and type theory, shedding new light on both fields.
An underspecified type requres a proof of a given type (corresponding to the presupposition content) in its formation rule, and it substitutes a variable with the proof found in the proof search. This mechanism of DTS serves as an uniform analysis of anaphora and presupposition through the process of underspecification, inheriting the ‘presupposition is anaphora’ paradigm (van der Sandt and Geurts 1991, van der Sandt 1992) and the anaphora resolusion is proof construction'' paradigm (Krahmer and Piwek1999, Piwek and Krahmer 2000).
This DTS setting not only provides a compositional semantic theory with descriptive power enough to cover a wide variety of linguistic phenomena but also gives novel explanations for classical puzzles such as anaphora accessibility and anaphoric potentials. For example, the E-type anaphoric link in \refex{1} is predicted to be accessible since a proof from \textit{someone bought a car} to the existence of a non-human entity is constructable in UDTT.
(1) Someone bought [a car]. It stinks.
Meanwhile, anaphoric links, as listed in \refex{2}, are predicted to be inaccessible because the required proofs are not constructable: This is because universal quantification, implication, and negation are represented by $\Pi$-types, data types of functions from which the intended antecedents cannot be picked up. This is an explanation purely based on the structures of proofs, fundamentally different from dynamic semantics.
(2) a. Everyone bought [a car]$^i$. *It$_i$ stinks. b. If John bought [a car]$^i$, it$_i$ must be a Porsche. *It$_i$ stinks. c. John didn't buy [a car]$^i$. *It$_i$ stinks.
Moreover, discourse theories such as DRT need to introduce an extra representational layer such as DRSs to distinguish the anaphoric potentials of \refex{ALwnPatC} and \refex{NELwpatC}, since the first sentences of \refex{ALwnPatC} and \refex{NELwpatC} are truth-conditionally equivalent in model-theoretic semantics.
(3) a. A linguist was not present at the class. He/she must be overslept.\label{ex:ALwnPatC} b. Not every linguist was present at the class. *He/she must be overslept.\label{ex:NELwpatC}
In DTS, \refex{ALwnPatC} and \refex{NELwpatC} have different proof-theoretic statuses: The proof construction in \refex{ALwnPatC} is intuitionistic while that in \refex{NELwpatC} is classical, the latter of which is not allowed in the intuitionistic setting of UDTT. In other words, DTS explains the different anaphoric potentials of \refex{ALwnPatC} and \refex{NELwpatC} by means of proof construction without assuming an extra semantic layer such as DRSs.
I will also reflect on the extensive research and developments over the past decade. Given that the empirical coverage of DTS is getting broader, we will discuss, among other things, representations of generalized quantifiers in \citet{Sundholm1989}, \citet{FoxLappin2005}, \citet{TNB2013}, and \citet{Tanaka2014GQ}; modality and factivity discussed in \citet{Ranta1994}, and \citet{Tanaka2014LENLS}; the phenomena of coercion discussed in \citet{Luo2010,Luo2011,Luo2012,Luo2012LP}, \citet{AsherLuo2012} and \citet{KMB2018}; a unified analysis of conventional implicatures and presuppositions in \citet{BekkiMcCready2014} and \citet{MBY2023}.
Overview of DTS as a compositional theory of meaning in terms of dependent type theory, including a theory of anaphora resolution and presupposition binding by combining underspecified types, proof search, and proof conversions.
I am introducing the semantic composition via DTS. ?Starting from the introduction of combinatory categorial grammar (CCG), the type mismatch problem of quantifiers in the non-subject positions, we will reach the notion of \textit{continuation} to remedy the problems. ?Then, we will discuss the classical crossover paradigm and its interaction with quantifier raising.