Главная
Новости
Строительство
Ремонт
Дизайн и интерьер

















Яндекс.Метрика





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

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

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

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

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

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

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

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

A → A {displaystyle A o A}

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

Γ , A , Δ → C Π → B Γ , Π , B ∖ A , Δ → C ( ∖ → ) B , Π → A Π → B ∖ A ( → ∖ ) {displaystyle {cfrac {Gamma ,A,Delta o Cquad Pi o B}{Gamma ,Pi ,Backslash A,Delta o C}};(ackslash o )qquad {cfrac {B,Pi o A}{Pi o Backslash A}};( o ackslash )}

Γ , A , Δ → C Π → B Γ , A / B , Π , Δ → C ( / → ) Π , B → A Π → A / B ( → / ) {displaystyle {cfrac {Gamma ,A,Delta o Cquad Pi o B}{Gamma ,A/B,Pi ,Delta o C}};(/ o )qquad {cfrac {Pi ,B o A}{Pi o A/B}};( o /)}

Γ , A , B , Δ → C Γ , A ⋅ B , Δ → C ( ⋅ → ) Γ → A Δ → B Γ , Δ → A ⋅ B ( → ⋅ ) {displaystyle {cfrac {Gamma ,A,B,Delta o C}{Gamma ,Acdot B,Delta o C}};(cdot o )qquad {cfrac {Gamma o Aquad Delta o B}{Gamma ,Delta o Acdot B}};( o cdot )}

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

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

  • Секвенция p → q / ( p ∖ q ) {displaystyle p o q/(packslash q)} (называемая поднятием типа p {displaystyle p} ) выводима в исчислении Ламбека:

q → q p → p p , p ∖ q → q ( ∖ → ) p → q / ( p ∖ q ) ( → / ) {displaystyle {cfrac {{cfrac {{cfrac {}{q o q}}quad {cfrac {}{p o p}}}{p,packslash q o q}}quad (ackslash o )}{p o q/(packslash q)}}( o /)}

  • Секвенция p ⋅ ( q / r ) → ( p ⋅ q ) / r {displaystyle pcdot (q/r) o (pcdot q)/r} выводима в исчислении Ламбека:

p → p q → q p , q → p ⋅ q ( → ⋅ ) r → r p , q / r , r → p ⋅ q ( / → ) p ⋅ ( q / r ) , r → p ⋅ q ( ⋅ → ) p ⋅ ( q / r ) → ( p ⋅ q ) / r ( → / ) {displaystyle {cfrac {{cfrac {{cfrac {{cfrac {p o pquad q o q}{p,q o pcdot q}}( o cdot )quad {cfrac {}{r o r}}}{p,q/r,r o pcdot q}}(/ o )}{pcdot (q/r),r o pcdot q}}(cdot o )}{pcdot (q/r) o (pcdot q)/r}}( o /)}

  • L ⊢ p / q , q / r → p / r {displaystyle mathrm {L} vdash p/q,q/r o p/r} .
  • L ⊢ ( q ∖ p ) / r → q ∖ ( p / r ) {displaystyle mathrm {L} vdash (qackslash p)/r o qackslash (p/r)} , L ⊢ q ∖ ( p / r ) → ( q ∖ p ) / r {displaystyle mathrm {L} vdash qackslash (p/r) o (qackslash p)/r} .

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

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

Категориальная грамматика Ламбека — структура ⟨ Σ , S , ▹ ⟩ {displaystyle langle Sigma ,S, riangleright angle } из 3 компонент:

  • Σ {displaystyle Sigma } — алфавит;
  • S ∈ T p {displaystyle Sin Tp} — выделенный тип в грамматике;
  • ▹ ⊆ Σ × T p {displaystyle riangleright subseteq Sigma imes Tp} — конечное бинарное отношение, ставящее в соответствие каждому символу алфавита конечное число типов исчисления Ламбека.
  • Язык, распознаваемый грамматикой ⟨ Σ , S , ▹ ⟩ {displaystyle langle Sigma ,S, riangleright angle } , — это множество слов вида a 1 … a n , n > 0 {displaystyle a_{1}dots a_{n},;n>0} , таких, что для каждого символа a i , i = 1 , … , n {displaystyle a_{i},;i=1,dots ,n} существует соответствующий ему тип T i {displaystyle T_{i}} (это означает, что a i ▹ T i {displaystyle a_{i} riangleright T_{i}} ) и L ⊢ T 1 , … , T n → S {displaystyle mathrm {L} vdash T_{1},dots ,T_{n} o S} .

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

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

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

    • Английскому предложению John loves Mary "Джон любит Мэри" можно поставить в соответствие секвенцию N P , ( N P ∖ S ) / N P , N P → S {displaystyle NP,(NPackslash S)/NP,NP o S} . Здесь именам собственным John, Mary соответствует примитивный тип N P {displaystyle NP} "noun phrase", обозначающий именные группы, а переходному глаголу loves соответствует сложный тип ( N P ∖ S ) / N P {displaystyle (NPackslash S)/NP} . Примитивный тип S {displaystyle S} "sentence" соответствует повествовательным предложениям. Данная секвенция выводима в исчислении Ламбека:

    S → S N P → N P N P , N P ∖ S → S ( ∖ → ) N P → N P N P , ( N P ∖ S ) / N P , N P → S ( / → ) {displaystyle {cfrac {{cfrac {S o Squad NP o NP}{NP,NPackslash S o S}}(ackslash o )quad NP o NP}{NP,(NPackslash S)/NP,NP o S}}(/ o )}

    • Более сложному английскому предложению John loves but Bill hates Mary "Джон любит, а Билл ненавидит Мэри" ставится в соответствие выводимая секвенция N P , ( N P ∖ S ) / N P , ( ( S / N P ) ∖ ( S / N P ) ) / ( S / N P ) , N P , ( N P ∖ S ) / N P , N P → S {displaystyle NP,(NPackslash S)/NP,((S/NP)ackslash (S/NP))/(S/NP),NP,(NPackslash S)/NP,NP o S} .

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

    Свойства

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

    Модификации

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

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

    → 1 Γ , Δ → A Γ , 1 , Δ → A {displaystyle {cfrac {}{ o mathbf {1} }}qquad {cfrac {Gamma ,Delta o A}{Gamma ,mathbf {1} ,Delta o A}}}

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

    Γ , A 1 , Δ → C Γ , A 1 ∧ A 2 , Δ → C ( ∧ 1 → ) Γ , A 2 , Δ → C Γ , A 1 ∧ A 2 , Δ → C ( ∧ 2 → ) {displaystyle {cfrac {Gamma ,A_{1},Delta o C}{Gamma ,A_{1}wedge A_{2},Delta o C}}(wedge _{1} o )qquad {cfrac {Gamma ,A_{2},Delta o C}{Gamma ,A_{1}wedge A_{2},Delta o C}}(wedge _{2} o )}

    Π → A 1 Π → A 1 ∨ A 2 ( → ∨ 1 ) Π → A 2 Π → A 1 ∨ A 2 ( → ∨ 2 ) {displaystyle {cfrac {Pi o A_{1}}{Pi o A_{1}vee A_{2}}}( o vee _{1})qquad {cfrac {Pi o A_{2}}{Pi o A_{1}vee A_{2}}}( o vee _{2})}

    Π → A 1 Π → A 2 Π → A 1 ∧ A 2 ( → ∧ ) Γ , A 1 , Δ → C Γ , A 2 , Δ → C Γ , A 1 ∨ A 2 , Δ → C ( ∨ → ) {displaystyle {cfrac {Pi o A_{1}quad Pi o A_{2}}{Pi o A_{1}wedge A_{2}}}( o wedge )qquad {cfrac {Gamma ,A_{1},Delta o Cquad Gamma ,A_{2},Delta o C}{Gamma ,A_{1}vee A_{2},Delta o C}}(vee o )}