Lambekův počet

Lambek kalkul ( angl. Lambek calculus , označovaný ) je formální logický systém navržený v roce 1958 Joachimem Lambkem [1] , který je určen k popisu syntaxe přirozených jazyků . Z matematického hlediska je Lambekův počet fragmentem lineární logiky . $L$

Formální definice

Lambekův kalkul lze definovat několika ekvivalentními způsoby. Níže je uvedena definice Lambkova sekvenčního počtu v Gentzenově formě .

Lambekův kalkul pracuje s typy (z hlediska lingvistiky typy odpovídají určitým kategoriím slov). Sada je pevná , jejíž prvky se nazývají primitivní typy. Staví se z nich spousta všech typů. Formálně je množina typů Lambekova kalkulu nejmenší množinou, která obsahuje a splňuje následující vlastnost: if , are types, pak , , (závorky se často vynechávají) jsou také typy. Operace , a se nazývají levé dělení , pravé dělení a násobení . ${\displaystyle Pr=\{p_{1},p_{2},\tečky \))$ $Tp$ $Pr$ $A$ $B$ $(A\obrácené lomítko B)$ $(A\cdot B)$ $(A/B)$ $\backslash$ $/$ $\cdot$

Primitivní typy se obvykle označují malými latinskými písmeny, typy velkými latinskými písmeny, sekvence typů velkými řeckými písmeny ( atd .). $\gamma$ $\Delta$

Sequent je řetězec ve tvaru , kde , a jsou typy Lambekova kalkulu. Část nalevo od šipky se nazývá předchůdce a část za šipkou se nazývá následná . $A_{1},\tečky ,A_{n}\to B$ $n>0$ $A_{1},\dots ,A_{n},B$

Axiómy a pravidla Lambekova počtu vysvětlují, které sekvence jsou odvoditelné . Jediný axiom (přesněji schéma axiomů) má tvar:

$A\to A$

Lambekův kalkul má 6 inferenčních pravidel, dvě pro každou operaci [2] :

${\cfrac {\Gamma ,A,\Delta \to C\quad \Pi \to B}{\Gamma ,\Pi ,B\obrácené lomítko A,\Delta \to C))\;(\obrácené lomítko \ to )\qquad {\cfrac {B,\Pi \to A}{\Pi \to B\obrácené lomítko A}}\;(\to \obrácené lomítko )$

${\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 /)$

${\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 )$

Posloupnost se nazývá odvoditelná , pokud ji lze získat z axiomů aplikací pravidel. Odpovídající řetězec axiomů a aplikací pravidel se nazývá derivace . Fakt odvoditelnosti se označuje jako . $\Gamma \to A$ $\mathrm {L} \vdash \Gamma \to A$

Příklady odvozených sekvencí

Sequent (nazývaný typ lifting ) je odvoditelný v Lambekově kalkulu: $p\to q/(p\obrácené lomítko q)$ $p$

${\cfrac {{\cfrac {{\cfrac {}{q\to q}}\quad {\cfrac {}{p\to p}}}{p,p\obrácené lomítko q\to q}} \quad (\obrácené lomítko \to )}{p\to q/(p\obrácené lomítko q)}}(\to /)$

Posloupnost je odvoditelná v Lambekově kalkulu: $p\cdot (q/r)\to (p\cdot q)/r$

${\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 /)$

$\mathrm {L} \vdash p/q,q/r\to p/r$ .
$\mathrm {L} \vdash (q\obrácené lomítko p)/r\to q\obrácené lomítko (p/r)$ , . $\mathrm {L} \vdash q\obrácené lomítko (p/r)\to (q\obrácené lomítko p)/r$

Lambekovy kategorické gramatiky

Pojem Lambekových kategorických gramatik odkazuje na teorii formálních gramatik ; jsou speciálním případem kategorických gramatik . Uvažujeme konečnou neprázdnou množinu zvanou abeceda. - množina všech řetězců konečné délky, které mohou být složeny z abecedních znaků ; jakákoli podmnožina této množiny se nazývá formální jazyk. $\Sigma$ ${\displaystyle \Sigma ^{\ast ))$ $\Sigma$

Lambekova kategoriální gramatika je strukturou 3 komponent: $\langle \Sigma ,S,\triangleright \rangle$

$\Sigma$ - abeceda;
$S\in Tp$ - význačný typ v gramatice;
$\triangleright \subseteq \Sigma \times Tp$ je konečná binární relace, která přiřazuje každému znaku abecedy konečný počet typů Lambekova kalkulu.

Jazyk rozpoznávaný gramatikou je množina slov ve tvaru , takže pro každý znak existuje odpovídající typ (což znamená ) a . $\langle \Sigma ,S,\triangleright \rangle$ $a_{1}\tečky a_{n},\;n>0$ $a_{i},\;i=1,\tečky ,n$ $T_{i}$ $a_{i}\triangleright T_{i}$ $\mathrm {L} \vdash T_{1},\tečky ,T_{n}\to S$

Příklad. Nechť , je primitivní typ a vztah je definován následovně , , . Taková gramatika rozpoznává jazyk . Například slovo patří do jazyka rozpoznávaného danou gramatikou, protože má odvozenou následnou . $\Sigma =\{a,b\}$ $S=s$ $\triangleright$ $a\triangleright s/p$ $b\triangleright p$ $b\triangleright s\zpětné lomítko p$ $\{a^{n}b^{n}|n>0\}$ $aaabbb$ $s/p,s/p,s/p,p,s\obrácené lomítko p,s\zpětné lomítko p\to s$

Příklady z lingvistiky

Pokud za množinu vezmeme množinu slov nějakého přirozeného jazyka, bude možné použít lambecké gramatiky k popisu množiny vět tohoto jazyka (nebo její části). Úkolem je najít gramatiku, která by přesně rozpoznávala gramaticky správné věty daného jazyka nebo alespoň správně popisovala některé jazykové jevy, které lingvisty zajímají. Konkrétní příklady odvoditelných sekvencí odpovídajících gramaticky správným větám jsou uvedeny níže. $\Sigma$

Anglické větě John loves Mary „John loves Mary“ lze přiřadit sekvenci [3] . Vlastní jména Jan , Marie zde odpovídají primitivnímu typu "podstatná fráze" označující podstatné jmenné fráze a tranzitivní sloveso loves odpovídá typu komplexnímu . Primitivní typ „věta“ odpovídá větám oznamovacím. Tato posloupnost je odvoditelná v Lambekově kalkulu: $NP,(NP\obrácené lomítko S)/NP,NP\to S$ $NP$ $(NP\obrácené lomítko S)/NP$ $S$

${\cfrac {{\cfrac {S\to S\quad NP\to NP}{NP,NP\obrácené lomítko S\to S))(\obrácené lomítko \to )\quad NP\to NP}{NP, (NP\obrácené lomítko S)/NP,NP\to S}}(/\do )$

Složitější anglické větě John loves but Bill hates Mary „John miluje, ale Bill nenávidí Mary“ je přiřazena odvozená sekvence [4] . $NP,(NP\obrácené lomítko S)/NP,((S/NP)\obrácené lomítko (S/NP))/(S/NP),NP,(NP\obrácené lomítko S)/NP,NP\to S$

Abychom spojili výše uvedené příklady s formální definicí kategorických gramatik uvedených na začátku oddílu, vezmeme primitivní typ jako rozlišující typ a definujeme vztah tak, aby slova v anglických větách výše byla porovnána s typy jim odpovídající v uvažovaných sekvencích. Pak věty John loves Mary , John loves but Bill hates Mary budou patřit do jazyka, který tato gramatika uznává. $S$ $\triangleright$

Vlastnosti

V Lambekově kalkulu je pravidlo řezu přípustné [1] . Jinými slovy, odvoditelnost posloupnosti vyplývá z odvoditelnosti posloupností tvaru . $\Pi \to A$ $\Gamma ,A,\Delta \to B$ $\Gamma ,\Pi ,\Delta \to B$
Třída jazyků generovaná gramatikou Lambek se shoduje s třídou bezkontextových jazyků bez prázdného slova [5] .
Problém kontroly odvoditelnosti sequence v Lambekově kalkulu je NP-úplný [6] .
Lambekův kalkul je správný a úplný s ohledem na dělení pologrupových modelů a existuje univerzální model. Je také kompletní s ohledem na -modely ( jazykové modely , angl. jazykové modely ) a s ohledem na -modely ( relační modely , angl. relační modely ) [7] . $L$ $R$
Lambda kalkul lze přidat k lambda kalkulu , takže závěry v Lambkově kalkulu budou doprovázeny převody typu lambda [8] . Z lingvistického hlediska to umožňuje modelování sémantiky vět.

Úpravy

Existuje řada variant Lambekova kalkulu založených na přidávání operací jiných než dělení a násobení a přidávání nových axiomů a inferenčních pravidel. Níže jsou uvedeny některé z možností.

Lambekův počet s jednotkou ( ). Umožňuje sekvence formuláře (které mají v předchůdci 0 typů). Jednotka ( ) je přidána k sadě platných znaků, ze kterých jsou sestavovány typy. Pro to je zaveden jeden axiom a jedno pravidlo: ${\displaystyle L_{\mathbf {1} }^{\ast ))$ $\to B$ $\mathbf {1}$

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

Multiplikativně-aditivní Lambek kalkul ( multiplikativně-aditivní Lambek kalkul ) je rozšíření, ve kterém se typy budují nejen pomocí dělení a násobení, ale také pomocí konjunkce a disjunkce . Pro ně je zavedeno následujících 6 pravidel: $L$ $\wedge$ $\vee$

${\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)$

${\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})$

${\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 )$

Viz také

Poznámky

↑ 12 Lambek , 1958 .
↑ Pentus, 1995 , str. 732.
↑ Moortgat, 1988 , s. čtrnáct.
↑ Moortgat, 1988 , s. 36.
↑ Pentus, 1995 .
↑ Pentus, 2006 .
↑ Pentus, 1999 .
↑ Moortgat, 1988 .

Literatura

Lambek, J. The Mathematics of Sentence Structure // The American Mathematical Monthly . - 1958. - Sv. 65 , č. 3 . — S. 154-170 . — ISSN 0002-9890 . - doi : 10.2307/2310058 .
Moortgat, M. Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus : [ eng. ] . Publikace Foris. - 1988. - ISBN 9789067653879 .
Pentus M. R. Lambek kalkul a formální gramatiky // Základní a aplikovaná matematika. - 1995. - T. 1 , č. 3 . - S. 729-751 . (Ruština)
Pentus M. R. Úplnost syntaktického počtu Lambek // Základní a aplikovaná matematika. - 1999. - V. 5 , č. 1 . - S. 193-219 . (Ruština)
Pentus, M. Lambek kalkul je NP-kompletní (anglicky) // Theoretical Computer Science. - 2006. - Sv. 357 , č.p. 1 . — S. 186-201 . — ISSN 0304-3975 . - doi : 10.1016/j.tcs.2006.03.018 .

Logika

Filosofie • Sémantika • Syntaxe • Historie

Logické skupiny

klasická logika	Aristotelská logika výroková logika Logika prvního řádu Logika druhého řádu logika vyššího řádu
matematická logika	teorie množin Teorie modelu Teorie vyčíslitelnosti Důkazová teorie a konstruktivní matematika Lineární logika formální systém přirozený závěr Sekvenční počet Algebra logiky Relevantní logika Deontická logika intuicionistická logika Lambekův počet
Neklasická logika	intuicionismus fuzzy logika Substrukturální logika logika Popisná logika Vícehodnotová logika Logická syntéza Závazná logika Temporální logika Modální logika ( Hybrid logic ) epistemická logika
Filosofická logika	Kritické myšlení neformální logika deduktivní uvažování

Komponenty

Seznam booleovských symbolů