Русская Википедия:Исчисление Ламбека

Содержание

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

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

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

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

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

Примитивные типы принято обозначать строчными латинскими буквами, типы — заглавными латинскими буквами, последовательности типов — заглавными греческими буквами (<math> \Gamma</math>, <math> \Delta</math> и т. п.).

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

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

<math> A\to A</math>

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

<math> \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) </math>

<math> \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/) </math>

<math> \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) </math>

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

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

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

<math> \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/) </math>

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

<math> \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/) </math>

• <math> \mathrm{L}\vdash p/q,q/r\to p/r</math>.
• <math> \mathrm{L}\vdash (q\backslash p)/r\to q\backslash (p/r)</math>, <math> \mathrm{L}\vdash q\backslash (p/r)\to (q\backslash p)/r </math>.

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

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

Категориальная грамматика Ламбека — структура <math> \langle \Sigma, S,\triangleright \rangle</math> из 3 компонент:

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

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

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

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

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

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

<math>\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) </math>

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

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

Свойства

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

Модификации

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

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

<math> \cfrac{}{\to\mathbf{1}} \qquad \cfrac{\Gamma,\Delta\to A}{\Gamma,\mathbf{1},\Delta\to A}</math>

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

<math> \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)</math>

<math> \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)</math>

<math> \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)</math>

См. также

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

Литература

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