Исчисление Ламбека

Исчисление Ламбека (англ. Lambek calculus, обозначается ${\displaystyle L}$) — формальная логическая система, предложенная в 1958 году Иоахимом Ламбеком^{[англ.][1]}, которая предназначена для описания синтаксиса естественных языков. С математической точки зрения исчисление Ламбека является фрагментом линейной логики.

Исчисление Ламбека можно определить несколькими эквивалентными способами. Ниже представлено определение секвенциального исчисления Ламбека в генценовском виде.

Исчисление Ламбека работает с типами (с точки зрения лингвистики, типы соответствуют определённым категориям слов). Фиксируется множество ${\displaystyle Pr=\{p_{1},p_{2},\dots \}}$, элементы которого называются примитивными типами. Из них строится множество всех типов. Формально, множество ${\displaystyle Tp}$ типов исчисления Ламбека — это наименьшее множество, содержащее ${\displaystyle Pr}$ и удовлетворяющее следующему свойству: если ${\displaystyle A}$, ${\displaystyle B}$ — типы, то ${\displaystyle (A\backslash B)}$, ${\displaystyle (A\cdot B)}$, ${\displaystyle (A/B)}$ (скобки часто опускаются) также являются типами. Операции ${\displaystyle \backslash }$, ${\displaystyle /}$ и ${\displaystyle \cdot }$ называются левым делением, правым делением и умножением соответственно.

Примитивные типы принято обозначать строчными латинскими буквами, типы — заглавными латинскими буквами, последовательности типов — заглавными греческими буквами (${\displaystyle \Gamma }$, ${\displaystyle \Delta }$ и т. п.).

Секвенцией называется строка вида ${\displaystyle A_{1},\dots ,A_{n}\to B}$, где ${\displaystyle n>0}$, а ${\displaystyle A_{1},\dots ,A_{n},B}$ — типы исчисления Ламбека. Часть слева от стрелки называется антецедентом, а часть после стрелки — сукцедентом.

Аксиомы и правила исчисления Ламбека объясняют, какие секвенции являются выводимыми. Единственная аксиома (точнее, схема аксиом) имеет вид:

${\displaystyle A\to A}$

В исчислении Ламбека имеется 6 правил вывода, по два на каждую операцию^[2]:

${\displaystyle {\cfrac {\Gamma ,A,\Delta \to C\quad \Pi \to B}{\Gamma ,\Pi ,B\backslash A,\Delta \to C}}\;(\backslash \to )\qquad {\cfrac {B,\Pi \to A}{\Pi \to B\backslash A}}\;(\to \backslash )}$

${\displaystyle {\cfrac {\Gamma ,A,\Delta \to C\quad \Pi \to B}{\Gamma ,A/B,\Pi ,\Delta \to C}}\;(/\to )\qquad {\cfrac {\Pi ,B\to A}{\Pi \to A/B}}\;(\to /)}$

${\displaystyle {\cfrac {\Gamma ,A,B,\Delta \to C}{\Gamma ,A\cdot B,\Delta \to C}}\;(\cdot \to )\qquad {\cfrac {\Gamma \to A\quad \Delta \to B}{\Gamma ,\Delta \to A\cdot B}}\;(\to \cdot )}$

Секвенция ${\displaystyle \Gamma \to A}$ называется выводимой, если её можно получить из аксиом путём применения правил. Соответствующая цепочка аксиом и применений правил называется выводом. Факт выводимости обозначается как ${\displaystyle \mathrm {L} \vdash \Gamma \to A}$.

• Секвенция ${\displaystyle p\to q/(p\backslash q)}$ (называемая поднятием типа ${\displaystyle p}$) выводима в исчислении Ламбека:

${\displaystyle {\cfrac {{\cfrac {{\cfrac {}{q\to q}}\quad {\cfrac {}{p\to p}}}{p,p\backslash q\to q}}\quad (\backslash \to )}{p\to q/(p\backslash q)}}(\to /)}$

• Секвенция ${\displaystyle p\cdot (q/r)\to (p\cdot q)/r}$ выводима в исчислении Ламбека:

${\displaystyle {\cfrac {{\cfrac {{\cfrac {{\cfrac {p\to p\quad q\to q}{p,q\to p\cdot q}}(\to \cdot )\quad {\cfrac {}{r\to r}}}{p,q/r,r\to p\cdot q}}(/\to )}{p\cdot (q/r),r\to p\cdot q}}(\cdot \to )}{p\cdot (q/r)\to (p\cdot q)/r}}(\to /)}$

• ${\displaystyle \mathrm {L} \vdash p/q,q/r\to p/r}$.
• ${\displaystyle \mathrm {L} \vdash (q\backslash p)/r\to q\backslash (p/r)}$, ${\displaystyle \mathrm {L} \vdash q\backslash (p/r)\to (q\backslash p)/r}$.

Понятие категориальных грамматик Ламбека относится к теории формальных грамматик; они представляют собой частный случай категориальных грамматик. Рассматривается конечное непустое множество ${\displaystyle \Sigma }$, называемое алфавитом. ${\displaystyle \Sigma ^{\ast }}$ — множество всех строк конечной длины, которые можно составить из символов алфавита ${\displaystyle \Sigma }$; любое подмножество этого множества называется формальным языком.

Категориальная грамматика Ламбека — структура ${\displaystyle \langle \Sigma ,S,\triangleright \rangle }$ из 3 компонент:

1. ${\displaystyle \Sigma }$ — алфавит;
2. ${\displaystyle S\in Tp}$ — выделенный тип в грамматике;
3. ${\displaystyle \triangleright \subseteq \Sigma \times Tp}$ — конечное бинарное отношение, ставящее в соответствие каждому символу алфавита конечное число типов исчисления Ламбека.

Язык, распознаваемый грамматикой ${\displaystyle \langle \Sigma ,S,\triangleright \rangle }$, — это множество слов вида ${\displaystyle a_{1}\dots a_{n},\;n>0}$, таких, что для каждого символа ${\displaystyle a_{i},\;i=1,\dots ,n}$ существует соответствующий ему тип ${\displaystyle T_{i}}$ (это означает, что ${\displaystyle a_{i}\triangleright T_{i}}$) и ${\displaystyle \mathrm {L} \vdash T_{1},\dots ,T_{n}\to S}$.

Пример. Пусть ${\displaystyle \Sigma =\{a,b\}}$, ${\displaystyle S=s}$ — примитивный тип, а отношение ${\displaystyle \triangleright }$ задано следующим образом ${\displaystyle a\triangleright s/p}$, ${\displaystyle b\triangleright p}$, ${\displaystyle b\triangleright s\backslash p}$. Такая грамматика распознает язык ${\displaystyle \{a^{n}b^{n}|n>0\}}$. Например, слово ${\displaystyle aaabbb}$ принадлежит языку, распознаваемому данной грамматикой, поскольку ему соответствует выводимая секвенция ${\displaystyle s/p,s/p,s/p,p,s\backslash p,s\backslash p\to s}$.

Если в качестве ${\displaystyle \Sigma }$ взять множество слов некоторого естественного языка, появится возможность использовать грамматики Ламбека для описания множества предложений этого языка (или его части). Ставится задача поиска грамматики, которая бы распознавала в точности грамматически верные предложения данного языка или хотя бы корректно описывала некоторые интересующие лингвистов языковые явления. Частные примеры выводимых секвенций, соответствующих грамматически верным предложениям, приведены ниже.

• Английскому предложению John loves Mary "Джон любит Мэри" можно поставить в соответствие секвенцию ${\displaystyle NP,(NP\backslash S)/NP,NP\to S}$ ^[3]. Здесь именам собственным John, Mary соответствует примитивный тип ${\displaystyle NP}$ "noun phrase", обозначающий именные группы, а переходному глаголу loves соответствует сложный тип ${\displaystyle (NP\backslash S)/NP}$. Примитивный тип ${\displaystyle S}$ "sentence" соответствует повествовательным предложениям. Данная секвенция выводима в исчислении Ламбека:

${\displaystyle {\cfrac {{\cfrac {S\to S\quad NP\to NP}{NP,NP\backslash S\to S}}(\backslash \to )\quad NP\to NP}{NP,(NP\backslash S)/NP,NP\to S}}(/\to )}$

• Более сложному английскому предложению John loves but Bill hates Mary "Джон любит, а Билл ненавидит Мэри" ставится в соответствие выводимая секвенция ${\displaystyle NP,(NP\backslash S)/NP,((S/NP)\backslash (S/NP))/(S/NP),NP,(NP\backslash S)/NP,NP\to S}$ ^[4].

Чтобы связать примеры выше с данным в начале раздела формальным определением категориальных грамматик, возьмём в качестве выделенного типа примитивный тип ${\displaystyle S}$, а отношение ${\displaystyle \triangleright }$ определим так, чтобы словам в английских предложениях выше сопоставлялись соответствующие им в рассмотренных секвенциях типы. Тогда предложения John loves Mary, John loves but Bill hates Mary будут принадлежать языку, распознаваемому данной грамматикой.

• В исчислении Ламбека допустимо правило сечения^[1]. Иначе говоря, из выводимости секвенций вида ${\displaystyle \Pi \to A}$ и ${\displaystyle \Gamma ,A,\Delta \to B}$ следует выводимость секвенции ${\displaystyle \Gamma ,\Pi ,\Delta \to B}$.
• Класс языков, порождаемых грамматиками Ламбека, совпадает с классом контекстно-свободных языков без пустого слова^[5].
• Задача проверки выводимости секвенции в исчислении Ламбека NP-полна^[6].
• Исчисление Ламбека корректно и полно относительно моделей полугрупп с делением, причём существует универсальная модель. Также оно полно относительно ${\displaystyle L}$-моделей (языковые модели, англ. language models), и относительно ${\displaystyle R}$-моделей (реляционные модели, англ. relational models) ^[7].
• В исчисление Ламбека можно добавить аппарат лямбда-исчисления, так что выводы в исчислении Ламбека будут сопровождаться преобразованиями лямбда-типов^[8]. С лингвистической точки зрения это позволяет моделировать семантику предложений.

Существует ряд вариантов исчисления Ламбека, основанных на добавлении операций, отличных от делений и умножения, и добавлении новых аксиом и правил вывода. Ниже рассмотрены некоторые из вариантов.

• Исчисление Ламбека с единицей (${\displaystyle L_{\mathbf {1} }^{\ast }}$). В нём допускаются секвенции вида ${\displaystyle \to B}$ (у которых 0 типов в антецеденте). В набор допустимых символов, из которых строятся типы, добавляется единица (${\displaystyle \mathbf {1} }$). Для неё вводятся одна аксиома и одно правило:

${\displaystyle {\cfrac {}{\to \mathbf {1} }}\qquad {\cfrac {\Gamma ,\Delta \to A}{\Gamma ,\mathbf {1} ,\Delta \to A}}}$

• Мультипликативно-аддитивное исчисление Ламбека (multiplicative-additive Lambek calculus) — расширение ${\displaystyle L}$, в рамках которого типы строятся не только с помощью делений и умножения, но и с помощью конъюнкции ${\displaystyle \wedge }$ и дизъюнкции ${\displaystyle \vee }$. Для них вводятся следующие 6 правил:

${\displaystyle {\cfrac {\Gamma ,A_{1},\Delta \to C}{\Gamma ,A_{1}\wedge A_{2},\Delta \to C}}(\wedge _{1}\to )\qquad {\cfrac {\Gamma ,A_{2},\Delta \to C}{\Gamma ,A_{1}\wedge A_{2},\Delta \to C}}(\wedge _{2}\to )}$

${\displaystyle {\cfrac {\Pi \to A_{1}}{\Pi \to A_{1}\vee A_{2}}}(\to \vee _{1})\qquad {\cfrac {\Pi \to A_{2}}{\Pi \to A_{1}\vee A_{2}}}(\to \vee _{2})}$

${\displaystyle {\cfrac {\Pi \to A_{1}\quad \Pi \to A_{2}}{\Pi \to A_{1}\wedge A_{2}}}(\to \wedge )\qquad {\cfrac {\Gamma ,A_{1},\Delta \to C\quad \Gamma ,A_{2},\Delta \to C}{\Gamma ,A_{1}\vee A_{2},\Delta \to C}}(\vee \to )}$

• Категориальная грамматика
• Исчисление секвенций

• Lambek, J. The Mathematics of Sentence Structure (англ.) // The American Mathematical Monthly. — 1958. — Vol. 65, no. 3. — P. 154-170. — ISSN 0002-9890. — doi:10.2307/2310058.
• Moortgat, M. Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus : [англ.]. — Foris Publications. — 1988. — ISBN 9789067653879.
• Пентус М. Р. Исчисление Ламбека и формальные грамматики (рус.) // Фундаментальная и прикладная математика. — 1995. — Т. 1, № 3. — С. 729-751.
• Пентус М. Р. Полнота синтаксического исчисления Ламбека (рус.) // Фундаментальная и прикладная математика. — 1999. — Т. 5, № 1. — С. 193-219.
• Pentus, M. Lambek calculus is NP-complete (англ.) // Theoretical Computer Science. — 2006. — Vol. 357, no. 1. — P. 186-201. — ISSN 0304-3975. — doi:10.1016/j.tcs.2006.03.018.