Formal Semantics in Modern Type Theories. Stergios Chatzikyriakidis
Чтение книги онлайн.

Читать онлайн книгу Formal Semantics in Modern Type Theories - Stergios Chatzikyriakidis страница 11

Название: Formal Semantics in Modern Type Theories

Автор: Stergios Chatzikyriakidis

Издательство: John Wiley & Sons Limited

Жанр: Языкознание

Серия:

isbn: 9781119489214

isbn:

СКАЧАТЬ In other words, Man does not have to be a constant type; instead, in (1.9), it is defined by means of type Human and a predicate male : Human → Prop: a man is a human who is male.

      The type of some as defined in (1.10) is that as shown in Table 1.3.

       – 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.21 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.22

       – 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-semantics23 (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.24

       – 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).