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

Исчисление Ламбека (Шаблон:Lang-en, обозначается $L$) — формальная логическая система, предложенная в 1958 году Шаблон:IwШаблон:Sfn, которая предназначена для описания синтаксиса естественных языков. С математической точки зрения исчисление Ламбека является фрагментом линейной логики.

Формальное определение

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

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

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

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

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

$A\to A$

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

$\frac{\mathrm{\Gamma },A,\mathrm{\Delta }\to C\mathrm{\Pi }\to B}{\mathrm{\Gamma },\mathrm{\Pi },B\mathrm{\setminus }A,\mathrm{\Delta }\to C}(\mathrm{\setminus }\to )\frac{B,\mathrm{\Pi }\to A}{\mathrm{\Pi }\to B\mathrm{\setminus }A}(\to \mathrm{\setminus })$

$\frac{\mathrm{\Gamma },A,\mathrm{\Delta }\to C\mathrm{\Pi }\to B}{\mathrm{\Gamma },A/B,\mathrm{\Pi },\mathrm{\Delta }\to C}(/\to )\frac{\mathrm{\Pi },B\to A}{\mathrm{\Pi }\to A/B}(\to /)$

$\frac{\mathrm{\Gamma },A,B,\mathrm{\Delta }\to C}{\mathrm{\Gamma },A\cdot B,\mathrm{\Delta }\to C}(\cdot \to )\frac{\mathrm{\Gamma }\to A\mathrm{\Delta }\to B}{\mathrm{\Gamma },\mathrm{\Delta }\to A\cdot B}(\to \cdot )$

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

Примеры выводимых секвенций

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

$\frac{\frac{\frac{}{q\to q}\frac{}{p\to p}}{p,p\mathrm{\setminus }q\to q}(\mathrm{\setminus }\to )}{p\to q/(p\mathrm{\setminus }q)}(\to /)$

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

$\frac{\frac{\frac{\frac{p\to pq\to q}{p,q\to p\cdot q}(\to \cdot )\frac{}{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 /)$

• $\mathrm{L}⊢p/q,q/r\to p/r$.
• $\mathrm{L}⊢(q\mathrm{\setminus }p)/r\to q\mathrm{\setminus }(p/r)$, $\mathrm{L}⊢q\mathrm{\setminus }(p/r)\to (q\mathrm{\setminus }p)/r$.

Категориальные грамматики Ламбека

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

Категориальная грамматика Ламбека — структура $⟨\mathrm{\Sigma },S,▹⟩$ из 3 компонент:

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

Язык, распознаваемый грамматикой $⟨\mathrm{\Sigma },S,▹⟩$, — это множество слов вида $a_1\dots a_n,n>0$, таких, что для каждого символа $a_i,i=1,\dots ,n$ существует соответствующий ему тип $T_i$ (это означает, что $a_i▹T_i$) и $\mathrm{L}⊢T_1,\dots ,T_n\to S$.

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

Примеры из лингвистики

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

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

$\frac{\frac{S\to SNP\to NP}{NP,NP\mathrm{\setminus }S\to S}(\mathrm{\setminus }\to )NP\to NP}{NP,(NP\mathrm{\setminus }S)/NP,NP\to S}(/\to )$

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

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

Свойства

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

Модификации

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

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

$\frac{}{\to \mathrm{𝟏}}\frac{\mathrm{\Gamma },\mathrm{\Delta }\to A}{\mathrm{\Gamma },\mathrm{𝟏},\mathrm{\Delta }\to A}$

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

$\frac{\mathrm{\Gamma },A_1,\mathrm{\Delta }\to C}{\mathrm{\Gamma },A_1\wedge A_2,\mathrm{\Delta }\to C}({\wedge }_1\to )\frac{\mathrm{\Gamma },A_2,\mathrm{\Delta }\to C}{\mathrm{\Gamma },A_1\wedge A_2,\mathrm{\Delta }\to C}({\wedge }_2\to )$

$\frac{\mathrm{\Pi }\to A_1}{\mathrm{\Pi }\to A_1\vee A_2}(\to {\vee }_1)\frac{\mathrm{\Pi }\to A_2}{\mathrm{\Pi }\to A_1\vee A_2}(\to {\vee }_2)$

$\frac{\mathrm{\Pi }\to A_1\mathrm{\Pi }\to A_2}{\mathrm{\Pi }\to A_1\wedge A_2}(\to \wedge )\frac{\mathrm{\Gamma },A_1,\mathrm{\Delta }\to C\mathrm{\Gamma },A_2,\mathrm{\Delta }\to C}{\mathrm{\Gamma },A_1\vee A_2,\mathrm{\Delta }\to C}(\vee \to )$

См. также

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

Литература

• Шаблон:Статья
• Шаблон:Публикация
• Шаблон:Статья
• Шаблон:Статья
• Шаблон:Статья