Formal Semantics in Modern Type Theories. Stergios Chatzikyriakidis

Чтение книги онлайн.

СКАЧАТЬ 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.

       1.4.3. Merits of MTT-semantics

      We contend that, as foundational semantic languages, MTTs are advantageous and MTT-semantics has unique merits, as compared with simple type theory and Montagovian semantics. Here, we outline some of its merits, organized below into two respects, which are further elaborated in the following chapters (and related papers). Please note that this is in no way to cover all, or even most, attractive aspects of MTT-semantics and it only serves the purpose of highlighting some notable features, hopefully making it easier to understand the following pages of the book.

Rich typing for semantic constructions. MTTs have a rich type structure: unlike simple type theory in which there are only the base types e and t and arrow types A → B (or

A, B, in a traditional notation), there are many ways to form types including, for example, dependent types (e.g. Π-types and Σ-types), inductive types (e.g. types of numbers/lists/vectors/trees and disjoint union types), logical types for propositions (under the propositions-as-types principle) and type universes (types that contain types as objects).²⁹ As we mentioned briefly earlier, the typing judgments of the form a : A, intuitively saying that a is an object of type A, are very different from the set-theoretical membership statements of the form s ∈ S: for example, the typing judgment a : A is mechanically decidable, while the membership relation s ∈ S (expressing that s satisfies predicate S) is a formula in the first-order logic and its truth is undecidable. Among other things, this decidability property is essential for any type theory to have a logic based on the propositions-as-types principle.

The rich typing disciplines also give us several advantageous points in semantic constructions. A simple advantage is that rich typing allows us to employ typing judgments, rather than membership statements, to deal with selectional restriction. In MTT-semantics, we can use the typing judgment j : Man to express that “John is a man” and this is different from Montague semantics where we use the formula man(j) to represent the meaning. Therefore, typing also offers us a means to deal with selectional restriction – to exclude meaningless sentences or phrases. This allows us to use typability as a formal criterion to judge whether a sentence is meaningful: for example, we would usually think (in a non-fictional world) that a sentence like “Tables talk” is meaningless with a category error – this is captured by means of typing in MTT-semantics: the MTT-interpretation of “Tables talk” is ill-typed (or an illegal expression). This is different from Montague semantics where the interpretation of “Tables talk” is just a false statement but it is a well-formed formula. (See section 3.1 for a further explanation.)

The rich type structure in MTTs enables us to use types to play the role of representing various collections,³⁰ the role played by sets in the Montagovian set-theoretical semantics. Besides acting as logical propositions, types can also be used in various ways in semantic constructions. For example, this allows one to interpret common nouns as types rather than predicates (see the above, (Luo 2012a) and section 3.2.1); in section 3.3, we show how various adjectival modifications can be modeled by means of rich typing, with Σ-types for intersective modification, Π-types (and the associated polymorphism) for subsective modification, disjoint union types and Π-polymorphism for privative modification, and a logical modal collection operator for non-committal modification. We shall also show in Chapters 4 and 5 that the typing structure can be used to model more advanced linguistic features such as gradable adjectival modification and copredication.

As mentioned earlier, subtyping is not only essential for MTT-semantics, but also very useful in semantic constructions. For instance, coercive subtyping is employed in defining dot-types (Luo 2009c, 2012b) for giving adequate interpretations of sentences involving copredication, an example of which is the sentence in (1.16), where a delicious lunch refers to food and a lunch that took forever refers to a process. Such copredication phenomena have been studied by many researchers such as Pustejovsky (1995) and Asher (2012). For MTT-semantics, the second author has proposed to use dot-types to deal with copredication (Luo 2009c): for this example, lunch involves two aspects: that of being food and that being a process. This is formalized by means of the subtyping relationship (1.17). It is then straightforward to see that the formula in (1.18), which interprets (1.16), is well-typed because of the subtyping relation in (1.17), where l : Lunch is the interpretation of “the lunch”.

(1.16) The lunch was delicious but took forever.

(1.17) Lunch ≤ Food • Process

(1.18) delicious(l) ∧ take_forever(l)

When defining dot-types such as Food • Process, coercive subtyping is used: we have, for example, Food • Process ≤ Food and Food • Process ≤ Process and therefore (1.18) is well-typed: both predicates delicious and take_forever can be applied to l : Lunch because both domains Food and Process are supertypes of Lunch. (For more formal details on subtyping, see СКАЧАТЬ