Читать книгу Formal Semantics in Modern Type Theories - Stergios Chatzikyriakidis - Страница 15

The application of dependent type theory to natural language semantics can be traced back to the middle of the 1980s, when Mönnich (1985) and Sundholm (1986) showed how to use Martin-Löf’s (extensional) type theory to deal with the problem of anaphoric representation as found necessary in interpreting donkey sentences such as those studied by Geach (1962). The key novelty is to use the type constructor Σ for existential quantification so that, for example, some of the donkey sentences involving intriguing anaphoric references can be interpreted as intended.¹⁶ Offering an elegant solution to the long-standing problem in linguistic semantics and providing an alternative to dynamic semantics (Kamp 1981; Heim 1983; Groenendijk and Stokhof 1991), the type-theoretical approach has attracted attention of formal semanticists who have been puzzled by this problem for a long time.

A systematic study in applying Martin-Löf’s (intensional) type theory (Martin-Löf 1975; Nordström et al. 1990) to formal semantics was not conducted until Ranta’s work in the early 1990s (see Ranta (1994) and related papers). Although Ranta himself may not have regarded his work as studying logical semantics (see, for example, the preface of Ranta (1994)), his work is widely regarded as the first systematic and significant development in employing a modern type theory as a foundational semantic language, studying a variety of topics including anaphora, temporal reference and contextual environments. For example, following Mönnich and Sundholm’s proposal of using types to represent common nouns, Ranta has carefully studied how to use Σ-types to represent (intersectively) modified CNs, pointing out that the CNs-as-types approach meets with the problem of multiple categorization of verbs, a crucial obstacle that calls for a solution.¹⁷ Another topic that has been carefully studied in Ranta (1994) is how to use the type-theoretical notion of contexts to represent possible worlds (or situations in the informal sense).¹⁸ This idea has been taken up and further explored by many other researchers to study contextual representations including the work by Boldini (2000) in Martin-Löf’s (1984) type theory, Ahn (2001) in pure type systems (Barendregt 1992) and their extensions, and Dapoigny and Barlatier (2010) in the Extended Calculus of Constructions (Luo 1990a, 1994).¹⁹

In the last decade, the study of MTT-semantics has made fruitful and significant developments, starting with the employment of coercive subtyping (Luo 2009c, 2012b) and leading to a full-blown semantic framework. The term Modern Type Theories (MTTs) was first used by the second author in Luo (2009c) which, on the one hand, distinguishes MTTs from simple type theory used in Montague semantics and, on the other hand, incorporates a wider class of (intensional) dependent type theories as foundational languages for MTT-semantics including, for example, the impredicative type theories such as UTT (Luo 1994).²⁰ The developments so far have made significant contributions that may be summarized in the following three respects, which are described in this book:

 – Fundamentals. MTTs are shown to be adequate foundational semantic languages. In this respect, there are two noteworthy developments: subtyping (Luo 2009c, 2012b) and signatures (Luo 2014) for MTT-semantics. For the former, the employment of coercive subtyping (Luo 1999; Luo et al. 2012) has been proposed and shown to be a necessary and crucial mechanism for MTT-semantics.²¹ For the latter, a novel notion of signatures has been studied and proposed for MTT-semantics – MTTs are extended with signatures which, in particular, may contain subtyping entries (Luo 2014; Lungu and Luo 2018), so that everyday situations (or incomplete worlds in the informal sense in model-theoretic semantics) can be described adequately by means of this new contextual mechanism.²²

 – Applications. MTTs are shown to be powerful for semantic constructions. Using MTTs’ rich type structure, various linguistic features have been studied and given semantics in MTTs including, for example, the study of various forms of modifications (Luo 2011a; Chatzikyriakidis and Luo 2013, 2017a) (see section 3.3 and Chapter 4). Two other noteworthy developments are as follows: the development of dot-types for copredication in MTT-semantics²³ (Luo 2009c, 2012b; Chatzikyriakidis and Luo 2018) (see Chapter 5 for more on copredication) and the use of coercive subtyping as a useful tool in various semantic constructions including, for example, sense disambiguation (Luo 2011b) (see section 3.2.2) and construction of dot-types (see Chapter 5), among many other examples as shown later in this book.²⁴

 – Reasoning. MTT-semantics is shown to be a sound basis for computer-assisted reasoning in natural language. MTTs are proof-theoretic: they are not only specified by proof-theoretic rules but also have proof-theoretic meaning theories (Luo 2014), which allow them to be implemented efficiently and used effectively for reasoning on computers. They are implemented by computer scientists in proof assistants and we have used the proof assistant Coq (Coq 2010) to implement MTT-semantics and performed various reasoning tasks and experiments based on such implementations (Luo 2011b; Chatzikyriakidis and Luo 2014, 2016) (see Chapter 6 for more details).

It is worth remarking that, when applied to formal semantics, whether a type theory is predicative or impredicative makes a difference. Although using Σ-types in a predicative type theory both as the existential quantifier and a structural mechanism solves the anaphora problem for simple donkey sentences (see footnote 16 on p13), such interpretations are inadequate when counting is involved (see, for example, those sentences involving “most” (Sundholm 1989; Tanaka 2015)).²⁵ As proposed and discussed in Luo (2012a, 2019b), one would solve this problem by imposing proof irrelevance (i.e. all proofs of a logical proposition are the same); however, such an imposition is only OK for type theories that distinguish logical propositions from other types (as in UTT), not when they are identified (as in Martin-Löf’s type theory). With proof irrelevance in UTT, where both ordinary existential quantifier and Σ-types exist, a satisfactory semantics can be given to a sentence with both anaphora and counting.²⁶ Such a solution is also available for predicative type theories as well: for example, as proposed and studied in Luo (2019b), we can employ MLTT_h, an extension of Martin-Löf’s type theory with the h-logic studied by Voevodsky in the HoTT project (HoTT 2013), to obtain an adequate foundational semantic language, which accommodates both strong and weak quantifiers in a similar fashion.

The study of MTT-semantics, especially its development in the last decade, is a part of a wider research endeavor by many researchers who have recognized the potential advantages of rich type structures in constructing formal semantics. For instance, besides work on MTT-semantics mentioned above, Retoré (2013) has employed the system F (Girard 1972; Reynolds 1974) to study how to use polymorphism in semantic constructions and Bekki (2014) has studied Dependent Type Semantics to discuss issues such as anaphoric expressions and underspecification in dependent type theories.²⁷ Besides these, there are also several pieces of very interesting work on linguistic semantics based on ideas of dependent typing, but not on formal type theories, including those by Asher (2012), Cooper (2005)²⁸ and Grudzińska and Zawadowski (2017), among others.