wiki

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

Разделы:

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

Table of Contents

Содержание

1 Формальное определение
- 1.1 Примеры выводимых секвенций
2 Категориальные грамматики Ламбека
- 2.1 Примеры из лингвистики
3 Свойства
4 Модификации
5 См. также
6 Примечания
7 Литература

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

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

Исчисление Ламбека работает с типами (с точки зрения лингвистики, типы соответствуют определённым категориям слов). Фиксируется множество Pr={p1,p2,…}{displaystyle Pr={p_{1},p_{2},dots }}

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

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

${displaystyle Gamma }$ , Δ{displaystyle Delta } $Delta$ и т. п.).

Секвенцией называется строка вида A1,…,An→B{displaystyle A_{1},dots ,A_{n}to B}

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

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

A→A{displaystyle Ato A}

${displaystyle Ato A}$

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

Γ,A,Δ→CΠ→BΓ,Π,B∖A,Δ→C(∖→)B,Π→AΠ→B∖A(→∖){displaystyle {cfrac {Gamma ,A,Delta to Cquad Pi to B}{Gamma ,Pi ,Bbackslash A,Delta to C}};(backslash to )qquad {cfrac {B,Pi to A}{Pi to Bbackslash A}};(to backslash )}

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

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

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

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

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

Секвенция Γ→A{displaystyle Gamma to A}

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

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

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

q→qp→pp,p∖q→q(∖→)p→q/(p∖q)(→/){displaystyle {cfrac {{cfrac {{cfrac {}{qto q}}quad {cfrac {}{pto p}}}{p,pbackslash qto q}}quad (backslash to )}{pto q/(pbackslash q)}}(to /)}

${displaystyle {cfrac {{cfrac {{cfrac {}{qto q}}quad {cfrac {}{pto p}}}{p,pbackslash qto q}}quad (backslash to )}{pto q/(pbackslash q)}}(to /)}$

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

p→pq→qp,q→p⋅q(→⋅)r→rp,q/r,r→p⋅q(/→)p⋅(q/r),r→p⋅q(⋅→)p⋅(q/r)→(p⋅q)/r(→/){displaystyle {cfrac {{cfrac {{cfrac {{cfrac {pto pquad qto q}{p,qto pcdot q}}(to cdot )quad {cfrac {}{rto r}}}{p,q/r,rto pcdot q}}(/to )}{pcdot (q/r),rto pcdot q}}(cdot to )}{pcdot (q/r)to (pcdot q)/r}}(to /)}

${displaystyle {cfrac {{cfrac {{cfrac {{cfrac {pto pquad qto q}{p,qto pcdot q}}(to cdot )quad {cfrac {}{rto r}}}{p,q/r,rto pcdot q}}(/to )}{pcdot (q/r),rto pcdot q}}(cdot to )}{pcdot (q/r)to (pcdot q)/r}}(to /)}$

L⊢p/q,q/r→p/r{displaystyle mathrm {L} vdash p/q,q/rto p/r} ${displaystyle mathrm {L} vdash p/q,q/rto p/r}$ .
L⊢(q∖p)/r→q∖(p/r){displaystyle mathrm {L} vdash (qbackslash p)/rto qbackslash (p/r)} ${displaystyle mathrm {L} vdash (qbackslash p)/rto qbackslash (p/r)}$ , L⊢q∖(p/r)→(q∖p)/r{displaystyle mathrm {L} vdash qbackslash (p/r)to (qbackslash p)/r} ${displaystyle mathrm {L} vdash qbackslash (p/r)to (qbackslash p)/r}$ .

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

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

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

Категориальная грамматика Ламбека — структура ⟨Σ,S,▹⟩{displaystyle langle Sigma ,S,triangleright rangle }

${displaystyle langle Sigma ,S,triangleright rangle }$ из 3 компонент:

Σ{displaystyle Sigma } $Sigma$ — алфавит;
S∈Tp{displaystyle Sin Tp} ${displaystyle Sin Tp}$ — выделенный тип в грамматике;
▹⊆Σ×Tp{displaystyle triangleright subseteq Sigma times Tp} ${displaystyle triangleright subseteq Sigma times Tp}$ — конечное бинарное отношение, ставящее в соответствие каждому символу алфавита конечное число типов исчисления Ламбека.

Язык, распознаваемый грамматикой ⟨Σ,S,▹⟩{displaystyle langle Sigma ,S,triangleright rangle }

${displaystyle langle Sigma ,S,triangleright rangle }$ , — это множество слов вида a1…an,n>0{displaystyle a_{1}dots a_{n},;n>0} ${displaystyle a_{1}dots a_{n},;n>0}$ , таких, что для каждого символа ai,i=1,…,n{displaystyle a_{i},;i=1,dots ,n} ${displaystyle a_{i},;i=1,dots ,n}$ существует соответствующий ему тип Ti{displaystyle T_{i}} $T_{i}$ (это означает, что ai▹Ti{displaystyle a_{i}triangleright T_{i}} ${displaystyle a_{i}triangleright T_{i}}$ ) и L⊢T1,…,Tn→S{displaystyle mathrm {L} vdash T_{1},dots ,T_{n}to S} ${displaystyle mathrm {L} vdash T_{1},dots ,T_{n}to S}$ .

Пример. Пусть Σ={a,b}{displaystyle Sigma ={a,b}}

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

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

Если в качестве Σ{displaystyle Sigma }

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

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

S→SNP→NPNP,NP∖S→S(∖→)NP→NPNP,(NP∖S)/NP,NP→S(/→){displaystyle {cfrac {{cfrac {Sto Squad NPto NP}{NP,NPbackslash Sto S}}(backslash to )quad NPto NP}{NP,(NPbackslash S)/NP,NPto S}}(/to )}

${displaystyle {cfrac {{cfrac {Sto Squad NPto NP}{NP,NPbackslash Sto S}}(backslash to )quad NPto NP}{NP,(NPbackslash S)/NP,NPto S}}(/to )}$

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

Чтобы связать примеры выше с данным в начале раздела формальным определением категориальных грамматик, возьмём в качестве выделенного типа примитивный тип S{displaystyle S}

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

Свойства

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

Модификации

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

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

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

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

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

Γ,A1,Δ→CΓ,A1∧A2,Δ→C(∧1→)Γ,A2,Δ→CΓ,A1∧A2,Δ→C(∧2→){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 {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 )}$

Π→A1Π→A1∨A2(→∨1)Π→A2Π→A1∨A2(→∨2){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}}{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})}$

Π→A1Π→A2Π→A1∧A2(→∧)Γ,A1,Δ→CΓ,A2,Δ→CΓ,A1∨A2,Δ→C(∨→){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 Cquad Gamma ,A_{2},Delta to C}{Gamma ,A_{1}vee A_{2},Delta to C}}(vee to )}

${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 Cquad 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.