Перейти к содержанию

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

Эта статья находится на начальном уровне проработки, в одной из её версий выборочно используется текст из источника, распространяемого под свободной лицензией
Материал из энциклопедии Руниверсалис

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

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

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

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

Примитивные типы принято обозначать строчными латинскими буквами, типы — заглавными латинскими буквами, последовательности типов — заглавными греческими буквами (Γ, Δ и т. п.).

Секвенцией называется строка вида A1,,AnB, где n>0, а A1,,An,B — типы исчисления Ламбека. Часть слева от стрелки называется антецедентом, а часть после стрелки — сукцедентом.

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

AA

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

Γ,A,ΔCΠBΓ,Π,BA,ΔC()B,ΠAΠBA()

Γ,A,ΔCΠBΓ,A/B,Π,ΔC(/)Π,BAΠA/B(/)

Γ,A,B,ΔCΓ,AB,ΔC()ΓAΔBΓ,ΔAB()

Секвенция ΓA называется выводимой, если её можно получить из аксиом путём применения правил. Соответствующая цепочка аксиом и применений правил называется выводом. Факт выводимости обозначается как LΓA.

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

  • Секвенция pq/(pq) (называемая поднятием типа p) выводима в исчислении Ламбека:

qqppp,pqq()pq/(pq)(/)

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

ppqqp,qpq()rrp,q/r,rpq(/)p(q/r),rpq()p(q/r)(pq)/r(/)

  • Lp/q,q/rp/r.
  • L(qp)/rq(p/r), Lq(p/r)(qp)/r.

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

Понятие категориальных грамматик Ламбека относится к теории формальных грамматик; они представляют собой частный случай категориальных грамматик. Рассматривается конечное непустое множество Σ, называемое алфавитом. Σ — множество всех строк конечной длины, которые можно составить из символов алфавита Σ; любое подмножество этого множества называется формальным языком.

Категориальная грамматика Ламбека — структура Σ,S, из 3 компонент:

  1. Σ — алфавит;
  2. STp — выделенный тип в грамматике;
  3. Σ×Tp — конечное бинарное отношение, ставящее в соответствие каждому символу алфавита конечное число типов исчисления Ламбека.

Язык, распознаваемый грамматикой Σ,S,, — это множество слов вида a1an,n>0, таких, что для каждого символа ai,i=1,,n существует соответствующий ему тип Ti (это означает, что aiTi) и LT1,,TnS.

Пример. Пусть Σ={a,b}, S=s — примитивный тип, а отношение задано следующим образом as/p, bp, bsp. Такая грамматика распознает язык {anbn|n>0}. Например, слово aaabbb принадлежит языку, распознаваемому данной грамматикой, поскольку ему соответствует выводимая секвенция s/p,s/p,s/p,p,sp,sps.

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

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

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

SSNPNPNP,NPSS()NPNPNP,(NPS)/NP,NPS(/)

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

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

Свойства

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

Модификации

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

  • Исчисление Ламбека с единицей (L1). В нём допускаются секвенции вида B (у которых 0 типов в антецеденте). В набор допустимых символов, из которых строятся типы, добавляется единица (1). Для неё вводятся одна аксиома и одно правило:

1Γ,ΔAΓ,1,ΔA

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

Γ,A1,ΔCΓ,A1A2,ΔC(1)Γ,A2,ΔCΓ,A1A2,ΔC(2)

ΠA1ΠA1A2(1)ΠA2ΠA1A2(2)

ΠA1ΠA2ΠA1A2()Γ,A1,ΔCΓ,A2,ΔCΓ,A1A2,ΔC()

См. также

Примечания

Литература