Исчисление Ламбека (англ. Lambek calculus, обозначается
) — формальная логическая система, предложенная в 1958 году Иоахимом Ламбеком[англ.][1], которая предназначена для описания синтаксиса естественных языков. С математической точки зрения исчисление Ламбека является фрагментом линейной логики.
Формальное определение
Исчисление Ламбека можно определить несколькими эквивалентными способами. Ниже представлено определение секвенциального исчисления Ламбека в генценовском виде.
Исчисление Ламбека работает с типами (с точки зрения лингвистики, типы соответствуют определённым категориям слов). Фиксируется множество
, элементы которого называются примитивными типами. Из них строится множество всех типов. Формально, множество
типов исчисления Ламбека — это наименьшее множество, содержащее
и удовлетворяющее следующему свойству: если
,
— типы, то
,
,
(скобки часто опускаются) также являются типами. Операции
,
и
называются левым делением, правым делением и умножением соответственно.
Примитивные типы принято обозначать строчными латинскими буквами, типы — заглавными латинскими буквами, последовательности типов — заглавными греческими буквами (
,
и т. п.).
Секвенцией называется строка вида
, где
, а
— типы исчисления Ламбека. Часть слева от стрелки называется антецедентом, а часть после стрелки — сукцедентом.
Аксиомы и правила исчисления Ламбека объясняют, какие секвенции являются выводимыми. Единственная аксиома (точнее, схема аксиом) имеет вид:
В исчислении Ламбека имеется 6 правил вывода, по два на каждую операцию[2]:
Секвенция
называется выводимой, если её можно получить из аксиом путём применения правил. Соответствующая цепочка аксиом и применений правил называется выводом. Факт выводимости обозначается как
.
Примеры выводимых секвенций
- Секвенция
(называемая поднятием типа
) выводима в исчислении Ламбека:
- Секвенция
выводима в исчислении Ламбека:
.
,
.
Категориальные грамматики Ламбека
Понятие категориальных грамматик Ламбека относится к теории формальных грамматик; они представляют собой частный случай категориальных грамматик. Рассматривается конечное непустое множество
, называемое алфавитом.
— множество всех строк конечной длины, которые можно составить из символов алфавита
; любое подмножество этого множества называется формальным языком.
Категориальная грамматика Ламбека — структура
из 3 компонент:
— алфавит;
— выделенный тип в грамматике;
— конечное бинарное отношение, ставящее в соответствие каждому символу алфавита конечное число типов исчисления Ламбека.
Язык, распознаваемый грамматикой
, — это множество слов вида
, таких, что для каждого символа
существует соответствующий ему тип
(это означает, что
) и
.
Пример. Пусть
,
— примитивный тип, а отношение
задано следующим образом
,
,
. Такая грамматика распознает язык
. Например, слово
принадлежит языку, распознаваемому данной грамматикой, поскольку ему соответствует выводимая секвенция
.
Примеры из лингвистики
Если в качестве
взять множество слов некоторого естественного языка, появится возможность использовать грамматики Ламбека для описания множества предложений этого языка (или его части). Ставится задача поиска грамматики, которая бы распознавала в точности грамматически верные предложения данного языка или хотя бы корректно описывала некоторые интересующие лингвистов языковые явления. Частные примеры выводимых секвенций, соответствующих грамматически верным предложениям, приведены ниже.
- Английскому предложению John loves Mary "Джон любит Мэри" можно поставить в соответствие секвенцию
[3]. Здесь именам собственным John, Mary соответствует примитивный тип
"noun phrase", обозначающий именные группы, а переходному глаголу loves соответствует сложный тип
. Примитивный тип
"sentence" соответствует повествовательным предложениям. Данная секвенция выводима в исчислении Ламбека:
- Более сложному английскому предложению John loves but Bill hates Mary "Джон любит, а Билл ненавидит Мэри" ставится в соответствие выводимая секвенция
[4].
Чтобы связать примеры выше с данным в начале раздела формальным определением категориальных грамматик, возьмём в качестве выделенного типа примитивный тип
, а отношение
определим так, чтобы словам в английских предложениях выше сопоставлялись соответствующие им в рассмотренных секвенциях типы. Тогда предложения John loves Mary, John loves but Bill hates Mary будут принадлежать языку, распознаваемому данной грамматикой.
Свойства
- В исчислении Ламбека допустимо правило сечения[1]. Иначе говоря, из выводимости секвенций вида
и
следует выводимость секвенции
.
- Класс языков, порождаемых грамматиками Ламбека, совпадает с классом контекстно-свободных языков без пустого слова[5].
- Задача проверки выводимости секвенции в исчислении Ламбека NP-полна[6].
- Исчисление Ламбека корректно и полно относительно моделей полугрупп с делением, причём существует универсальная модель. Также оно полно относительно
-моделей (языковые модели, англ. language models), и относительно
-моделей (реляционные модели, англ. relational models) [7].
- В исчисление Ламбека можно добавить аппарат лямбда-исчисления, так что выводы в исчислении Ламбека будут сопровождаться преобразованиями лямбда-типов[8]. С лингвистической точки зрения это позволяет моделировать семантику предложений.
Модификации
Существует ряд вариантов исчисления Ламбека, основанных на добавлении операций, отличных от делений и умножения, и добавлении новых аксиом и правил вывода. Ниже рассмотрены некоторые из вариантов.
- Исчисление Ламбека с единицей (
). В нём допускаются секвенции вида
(у которых 0 типов в антецеденте). В набор допустимых символов, из которых строятся типы, добавляется единица (
). Для неё вводятся одна аксиома и одно правило:
- Мультипликативно-аддитивное исчисление Ламбека (multiplicative-additive Lambek calculus) — расширение
, в рамках которого типы строятся не только с помощью делений и умножения, но и с помощью конъюнкции
и дизъюнкции
. Для них вводятся следующие 6 правил:
См. также
Примечания
- ↑ 1 2 Lambek, 1958.
- ↑ Пентус, 1995, с. 732.
- ↑ Moortgat, 1988, p. 14.
- ↑ Moortgat, 1988, p. 36.
- ↑ Пентус, 1995.
- ↑ Pentus, 2006.
- ↑ Пентус, 1999.
- ↑ Moortgat, 1988.
Литература
![Перейти к шаблону «Логика»](//upload.wikimedia.org/wikipedia/commons/thumb/c/c9/Wikipedia_interwiki_section_gear_icon.svg/14px-Wikipedia_interwiki_section_gear_icon.svg.png) |
---|
|
Группы логик | | |
---|
Компоненты | |
---|
|