Stergios Chatzikyriakidis - Formal Semantics in Modern Type Theories

Здесь есть возможность читать онлайн «Stergios Chatzikyriakidis - Formal Semantics in Modern Type Theories» — ознакомительный отрывок электронной книги совершенно бесплатно, а после прочтения отрывка купить полную версию. В некоторых случаях можно слушать аудио, скачать через торрент в формате fb2 и присутствует краткое содержание. Жанр: unrecognised, на английском языке. Описание произведения, (предисловие) а так же отзывы посетителей доступны на портале библиотеки ЛибКат.

Formal Semantics in Modern Type Theories: краткое содержание, описание и аннотация

Предлагаем к чтению аннотацию, описание, краткое содержание или предисловие (зависит от того, что написал сам автор книги «Formal Semantics in Modern Type Theories»). Если вы не нашли необходимую информацию о книге — напишите в комментариях, мы постараемся отыскать её.

This book studies formal semantics in modern type theories (MTTsemantics). Compared with simple type theory, MTTs have much richer type structures and provide powerful means for adequate semantic constructions. This offers a serious alternative to the traditional settheoretical foundation for linguistic semantics and opens up a new avenue for developing formal semantics that is both model-theoretic and proof-theoretic, which was not available before the development of MTTsemantics. This book provides a reader-friendly and precise description of MTTs and offers a comprehensive introduction to MTT-semantics. It develops several case studies, such as adjectival modification and copredication, to exemplify the attractiveness of using MTTs for the study of linguistic meaning. It also examines existing proof assistant technology based on MTT-semantics for the verification of semantic constructions and reasoning in natural language. Several advanced topics are also briefly studied, including dependent event types, an application of dependent typing to event semantics.

Formal Semantics in Modern Type Theories — читать онлайн ознакомительный отрывок

Ниже представлен текст книги, разбитый по страницам. Система сохранения места последней прочитанной страницы, позволяет с удобством читать онлайн бесплатно книгу «Formal Semantics in Modern Type Theories», без необходимости каждый раз заново искать на чём Вы остановились. Поставьте закладку, и сможете в любой момент перейти на страницу, на которой закончили чтение.

Тёмная тема
Сбросить

Интервал:

Закладка:

Сделать

Simple examples in Montague semantics can be found in Table 1.1, briefly showing how to interpret some of the basic linguistic categories in the Montagovian setting, including common nouns (CN), verbs (IV), adjectives (ADJ), verb-modifying adverbs (ADV VP), modified CNs, quantifiers and sentences (S). In the following section, we can find Table 1.3 with examples for these categories interpreted in MTT-semantics. For example, in Montague semantics, verb phrases are interpreted as predicates of type etand sentences as formulas of type t, as ( 1.5) and ( 1.6) illustrate (see, the lines for IV and S in Table 1.1):

( 1.5) talk : et

( 1.6) ∃ x : e. man ( x ) ∧ talk ( x )

A remark we should make is that, in type theories, typing judgments and logical formulas are different. In particular, a typing judgment is not a logical formula: ( 1.5) is a typing judgment stating that talk is of type et, while ( 1.6) is a logical formula of type t. With such examples, the difference seems to be apparent and there is no need to be emphasized. However, this becomes more important in the setting of modern type theories where much richer typing mechanisms are employed (see, for example, Chapter 2).

A notational convention is adopted in this book: we shall use a different font to represent semantics of a natural language phrase. For instance, for the natural language words “man” and “talk”, we shall use man and talk for their semantics (as in Table 1.1).

A linguistic feature that has been studied carefully in the Montagovian framework is intensionality, following the proposal made by Carnap (1947) that the intension of an expression be modeled by a function on possible states of affairs whose value, at a particular state, is the extension of the expression in that state. Nearly all constructions in English have some intensional instances (see, for example, a discussion on this in Partee (1988), among others). This has led Montague to give a special treatment of intensionality in his IL. It can be treated by adding a special base type s to simple type theory C , which allows one to consider types like s → A . 11

Formal Semantics in Modern Type Theories - изображение 9

For instance, we may interpret the intension of a sentence as a function from possible worlds to truth values, of type st. This approach to intensionality has been extensively studied, although it is not regarded as completely satisfactory in some aspects: for example, it suffers from the so-called problem of logical omniscience in that logically equivalent sentences are regarded as having the same meaning, which may be incorrect in an intensional context. In this book, we shall largely ignore the intensionality issue, with some exceptions, 12 not because it is not important (it obviously is), but rather that it is orthogonal to most, if not all, of the issues we are going to discuss.

1.4. MTT-semantics: formal semantics in modern type theories

In this section, some simple examples in formal semantics in modern type theories (MTT-semantics) are sketched for illustrations. Then, we shall describe the historical developments and some of the major merits for MTTs to be employed as foundational semantic languages.

1.4.1. A glance at MTT-semantics

Here, we sketch some simple examples of MTT-semantic interpretations, which give some ideas of what it is like, although a full-scale introduction to MTT-semantics (in Chapter 3) will not be possible until after the introduction to MTTs in Chapter 2. Let us start by considering the simple example ( 1.1), repeated here as ( 1.7), whose MTT-semantics is given in ( 1.8):

( 1.7) John talks.

( 1.8) talk ( j )

In appearance, the MTT-interpretation ( 1.8) seems to be the same as the Montagovian interpretation ( 1.2). However, although similar, they have subtle differences, as summarized in Table 1.2.

Table 1.2. Semantics of “John talks”

Type in Montague semantic Type in MTT-semantics
j e Human
talk e → t HumanProp
talk ( j ) t Prop

In particular, the typings of these interpretations are different:

– In MTT-semantics, the sentence ( 1.7) is interpreted as the proposition talk(j) : Prop where Prop is the type of all logical propositions – an internal totality that only exists in impredicative type theories such as UTT. 13

– In MTT-semantics, talk(j) is a well-typed proposition because the semantics of “talk” is a predicate talk : Human → Prop, whose domain is the type Human, the collection of humans to which talk can be meaningfully applied and to which j belongs as well. Note that, different from Montague semantics, the domain of talk is Human, rather than the type e of all entities. 14

Table 1.3. Examples in MTT-semantics

Example MTT-semantics
CN man, human Man, Human : Type
IV talk talk : Human → Prop
ADJ handsome handsome : Man → Prop
ADV VP quickly quickly : ΠA:CN. (A → Prop) → (A → Prop)
Modified CN handsome man Σm : Man. handsome(m) : Type
Quantifier some some : ΠA:CN. (A → Prop) → Prop
S A man talks ∃m : Man. talk(m) : Prop

MTT-semantic interpretations for various basic linguistic categories are exemplified in Table 1.3, where the natural language examples are the same as those in Table 1.1 for their Montague semantics. This makes it possible for a quick comparison in order for one to approach MTT-semantics more easily, albeit the understanding can be sketchy and imprecise at this stage. Here are brief explanations of the example interpretations in Table 1.3: some type-theoretical concepts are used without explanation, including polymorphism, Σ-type and universe which will only be introduced in Chapter 2.

– A common noun (CN) can be interpreted as a type and the interpretations of CNs form a universe called CN, the type of the types that interpret CNs.

– A verb (IV) or an adjective (ADJ) can be interpreted as a predicate over a type D that interprets the domain of the verb or adjective, i.e. a function of type D → Prop.

– A verb-modifying adverb (ADVVP) can be interpreted as a polymorphic function from predicates of type A → Prop to predicates of the same type, where A ranges over CNs in the universe CN.

– Modified common nouns (modified CN), when the adjectives are intersective, can be interpreted by means of Σ-types of pairs.

– A quantifier is interpreted as a polymorphic function that takes a type A that interprets a common noun and a predicate over A, and returns a proposition.

– A sentence (S) can be interpreted as a proposition of type Prop. 15

Please note that the semantic interpretations in Table 1.3 are only indicative with typical examples. In some cases, there are further elaborations or completely different ways of interpretation. For example, although CNs modified by intersective adjectives can be interpreted by Σ-types, adjectival modifications by means of other classes of adjectives may better be interpreted with the help of other type constructors (see section 3.3).

Читать дальше
Тёмная тема
Сбросить

Интервал:

Закладка:

Сделать

Похожие книги на «Formal Semantics in Modern Type Theories»

Представляем Вашему вниманию похожие книги на «Formal Semantics in Modern Type Theories» списком для выбора. Мы отобрали схожую по названию и смыслу литературу в надежде предоставить читателям больше вариантов отыскать новые, интересные, ещё непрочитанные произведения.


Отзывы о книге «Formal Semantics in Modern Type Theories»

Обсуждение, отзывы о книге «Formal Semantics in Modern Type Theories» и просто собственные мнения читателей. Оставьте ваши комментарии, напишите, что Вы думаете о произведении, его смысле или главных героях. Укажите что конкретно понравилось, а что нет, и почему Вы так считаете.

x