Исчисление Ламбека (англ.Lambek calculus, обозначается ) — формальная логическая система, предложенная в 1958 году Иоахимом Ламбеком[en][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]. Иначе говоря, из выводимости секвенций вида и следует выводимость секвенции .
Задача проверки выводимости секвенции в исчислении Ламбека NP-полна[6].
Исчисление Ламбека корректно и полно относительно моделей полугрупп с делением, причём существует универсальная модель. Также оно полно относительно -моделей (языковые модели, англ. language models), и относительно -моделей (реляционные модели, англ. relational models) [7].
В исчисление Ламбека можно добавить аппарат лямбда-исчисления, так что выводы в исчислении Ламбека будут сопровождаться преобразованиями лямбда-типов[8]. С лингвистической точки зрения это позволяет моделировать семантику предложений.
Модификации
Существует ряд вариантов исчисления Ламбека, основанных на добавлении операций, отличных от делений и умножения, и добавлении новых аксиом и правил вывода. Ниже рассмотрены некоторые из вариантов.
Исчисление Ламбека с единицей (). В нём допускаются секвенции вида (у которых 0 типов в антецеденте). В набор допустимых символов, из которых строятся типы, добавляется единица (). Для неё вводятся одна аксиома и одно правило:
Мультипликативно-аддитивное исчисление Ламбека (multiplicative-additive Lambek calculus) — расширение , в рамках которого типы строятся не только с помощью делений и умножения, но и с помощью конъюнкции и дизъюнкции . Для них вводятся следующие 6 правил: