Lambek kalkyl

Lambek-kalkylen ( eng. Lambek calculus , betecknad ) är ett formellt logiskt system som föreslagits 1958 av Joachim Lambek [1] , som är avsett att beskriva syntaxen för naturliga språk . Ur en matematisk synvinkel är Lambek-kalkylen ett fragment av linjär logik . $L$

Formell definition

Lambek-kalkylen kan definieras på flera likvärdiga sätt. Nedan är definitionen av Lambeks sekventiell kalkyl i Gentzens form .

Lambek-kalkylen arbetar med typer (i fråga om lingvistik motsvarar typer vissa kategorier av ord). En uppsättning är fast , vars element kallas primitiva typer. Många av alla typer är byggda av dem. Formellt är uppsättningen typer av Lambek-kalkylen den minsta uppsättningen som innehåller och uppfyller följande egenskap: om , är typer, så är , , (parenteser ofta utelämnade) också typer. Operationerna och kallas vänster division , höger division respektive multiplikation . ${\displaystyle Pr=\{p_{1},p_{2},\dots \))$ $Tp$ $Pr$ $A$ $B$ $(A\backslash B)$ $(A\cdot B)$ $(A/B)$ $\backslash$ $/$ $\cdot$

Primitiva typer betecknas vanligtvis med små latinska bokstäver, typer med stora latinska bokstäver, sekvenser av typer med stora grekiska bokstäver ( , etc.). $\gamma$ $\Delta$

En sekvens är en sträng av formen , där , och är typerna av Lambek-kalkylen. Delen till vänster om pilen kallas antecedenten , och delen efter pilen kallas succedenten . $A_{1},\dots ,A_{n}\to B$ $n>0$ $A_{1},\dots ,A_{n},B$

Lambekkalkylens axiom och regler förklarar vilka sekvenser som är härledbara . Det enda axiomet (mer exakt, axiomschemat) har formen:

$A\to A$

Lambek-kalkylen har 6 slutledningsregler, två för varje operation [2] :

${\cfrac {\Gamma ,A,\Delta \to C\quad \Pi \to B}{\Gamma ,\Pi ,B\backslash A,\Delta \to C))\;(\backslash \ till )\qquad {\cfrac {B,\Pi \to A}{\Pi \to B\backslash A}}\;(\to \backslash )$

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

En sekvens kallas härledbar om den kan erhållas från axiomen genom att tillämpa reglerna. Motsvarande kedja av axiom och regeltillämpningar kallas härledning . Faktumet om härledning betecknas som . $\Gamma \to A$ $\mathrm {L} \vdash \Gamma \to A$

Exempel på härledda sekvenser

Sekvensen (kallad typlyftning ) är härledbar i Lambek-kalkylen: $p\to q/(p\backslash q)$ $sid$

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

Sekvensen är härledbar i Lambek-kalkylen: $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\backslash p)/r\to q\backslash (p/r)$ , . $\mathrm {L} \vdash q\backslash (p/r)\to (q\backslash p)/r$

Lambeks kategoriska grammatik

Begreppet Lambeks kategoriska grammatik hänvisar till teorin om formell grammatik ; de är ett specialfall av kategoriska grammatiker . Vi betraktar en finit icke-tom mängd som kallas alfabetet. - uppsättningen av alla strängar av ändlig längd som kan bestå av alfabetiska tecken ; varje delmängd av denna uppsättning kallas ett formellt språk. $\Sigma$ ${\displaystyle \Sigma ^{\ast ))$ $\Sigma$

Lambeks kategoriska grammatik är en struktur av 3 komponenter: $\langle \Sigma ,S,\triangleright \rangle$

$\Sigma$ - alfabetet;
$S\in Tp$ - framstående typ i grammatik;
$\triangleright \subseteq \Sigma \times Tp$ är en finit binär relation som tilldelar varje tecken i alfabetet ett begränsat antal typer av Lambek-kalkylen.

Ett språk som känns igen av en grammatik är en uppsättning ord av formen , så att det för varje tecken finns en motsvarande typ (vilket betyder ) och . $\langle \Sigma ,S,\triangleright \rangle$ $a_{1}\dots a_{n},\;n>0$ $a_{i},\;i=1,\dots ,n$ $T_{i}$ $a_{i}\triangleright T_{i}$ $\mathrm {L} \vdash T_{1},\dots ,T_{n}\to S$

Exempel. Låt , vara en primitiv typ, och relationen definieras enligt följande , , . En sådan grammatik känner igen ett språk . Till exempel hör ett ord till ett språk som känns igen av en given grammatik eftersom det har en antagen sekvens . $\Sigma =\{a,b\}$ $S=s$ $\triangleright$ $a\triangleright s/p$ $b\triangleright p$ $b\triangleright s\backslash p$ ${\displaystyle \{a^{n}b^{n}|n>0\))$ $aaabbb$ $s/p,s/p,s/p,p,s\backslash p,s\backslash p\to s$

Exempel från lingvistik

Om vi tar uppsättningen av ord i något naturligt språk som en uppsättning, kommer det att vara möjligt att använda Lambek-grammatik för att beskriva uppsättningen meningar i detta språk (eller en del av det). Uppgiften är att hitta en grammatik som skulle känna igen exakt de grammatiskt korrekta meningarna i ett givet språk eller åtminstone korrekt beskriva några av de språkliga fenomen som är intressanta för lingvister. Särskilda exempel på härledbara sekvenser som motsvarar grammatiskt korrekta meningar ges nedan. $\Sigma$

Den engelska meningen John loves Mary "John loves Mary" kan tilldelas en sekvens [3] . Här motsvarar egennamnen John , Mary den primitiva typen "substantivfras" som betecknar substantivfraser , och det transitiva verbet älskar motsvarar den komplexa typen . Den primitiva typen "sats" motsvarar deklarativa meningar. Denna sekvens är härledbar i Lambek-kalkylen: $NP,(NP\backslash S)/NP,NP\to S$ $NP$ $(NP\backslash S)/NP$ $S$

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

Den mer komplexa engelska meningen John älskar men Bill hatar Mary "John älskar, men Bill hatar Mary" tilldelas den härledda sekvensen [4] . $NP,(NP\backslash S)/NP,((S/NP)\backslash (S/NP))/(S/NP),NP,(NP\backslash S)/NP,NP\to S$

För att koppla ihop exemplen ovan med den formella definitionen av kategorisk grammatik som ges i början av avsnittet, tar vi den primitiva typen som en distingerad typ och definierar relationen så att orden i de engelska meningarna ovan jämförs med typerna motsvarande dem i de betraktade följderna. Då kommer meningarna John loves Mary , John loves men Bill hatar Mary att tillhöra språket som känns igen av denna grammatik. $S$ $\triangleright$

Egenskaper

I Lambek-kalkylen är snittregeln tillåten [1] . Med andra ord, härledbarheten av sekvensen följer av härledbarheten av sekvenser av formen . $\Pi \to A$ $\Gamma ,A,\Delta \to B$ $\Gamma ,\Pi ,\Delta \to B$
Klassen av språk som genereras av Lambek-grammatik sammanfaller med klassen av sammanhangsfria språk utan det tomma ordet [5] .
Problemet med att kontrollera deducerbarheten av en sekvens i Lambek-kalkylen är NP-komplett [6] .
Lambek-kalkylen är korrekt och komplett med avseende på divisionssemigruppsmodeller, och det finns en universell modell. Den är också komplett med avseende på -modeller ( språkmodeller , eng. språkmodeller ), och med avseende på -modeller ( relationsmodeller , eng. relationsmodeller ) [7] . $L$ $R$
Lambdakalkyl kan läggas till lambdakalkylen , så att slutsatser i Lambekalkylen kommer att åtföljas av konverteringar av lambdatyp [8] . Ur en språklig synvinkel tillåter detta modellering av meningarnas semantik .

Ändringar

Det finns ett antal varianter av Lambek-kalkylen baserade på addition av andra operationer än division och multiplikation och tillägg av nya axiom och inferensregler. Nedan finns några av alternativen.

Lambekräkning med enhet ( ). Det tillåter sekvenser av formen (som har 0 typer i föregående). En enhet ( ) läggs till i uppsättningen giltiga tecken som typerna är byggda av. För det introduceras ett axiom och en regel: ${\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))$

Multiplikativ-additiv Lambek-kalkyl ( multiplikativ-additiv Lambek-kalkyl ) är en förlängning där typer byggs inte bara med hjälp av division och multiplikation, utan också med hjälp av konjunktion och disjunktion . För dem införs följande 6 regler: $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 )$

Se även

Anteckningar

↑ 12 Lambek , 1958 .
↑ Pentus, 1995 , sid. 732.
↑ Moortgat, 1988 , sid. fjorton.
↑ Moortgat, 1988 , sid. 36.
↑ Pentus, 1995 .
↑ Pentus, 2006 .
↑ Pentus, 1999 .
↑ Moortgat, 1988 .

Litteratur

Lambek, J. The Mathematics of Sentence Structure // The American Mathematical Monthly . - 1958. - Vol. 65 , nr. 3 . — S. 154-170 . — ISSN 0002-9890 . - doi : 10.2307/2310058 .
Moortgat, M. Kategoriella undersökningar: logiska och språkliga aspekter av Lambek-kalkylen : [ eng. ] . Foris Publikationer. - 1988. - ISBN 9789067653879 .
Pentus M. R. Lambek kalkyl och formell grammatik // Grundläggande och tillämpad matematik. - 1995. - T. 1 , nr 3 . - S. 729-751 . (ryska)
Pentus M. R. Lambek syntaktiska kalkylens fullständighet // Grundläggande och tillämpad matematik. - 1999. - V. 5 , nr 1 . - S. 193-219 . (ryska)
Pentus, M. Lambek kalkyl är NP-komplett (engelska) // Teoretisk datavetenskap. - 2006. - Vol. 357 , nr. 1 . — S. 186-201 . — ISSN 0304-3975 . - doi : 10.1016/j.tcs.2006.03.018 .

Logik

Filosofi • Semantik • Syntax • Historia

Logiska grupper

klassisk logik	Aristotelisk logik propositionell logik Första beställningslogik Andra ordningens logik högre ordningslogik
matematisk logik	mängdteori Modellteori Beräkningsbarhetsteori Bevisteori och konstruktiv matematik Linjär logik formellt system naturlig slutsats Sekvenskalkyl Algebra av logik Relevant logik Deontisk logik intuitionistisk logik Lambek kalkyl
Icke-klassisk logik	intuitionism rolig logik Substrukturell logik logik Beskrivningslogik Flervärdig logik Logisk syntes Bindande logik Temporal logik Modal logik ( Hybrid logik ) epistemisk logik
Filosofisk logik	Kritiskt tänkande informell logik deduktiva resonemang

Komponenter

Bortförande (logik)
Sannolikhet
påstående
Avdrag / Induktion / Traduktion
Verklighet
induktivt resonemang
slutledning
boolesk konstant
Sann
logiskt följa
Logisk form
Nödvändiga och tillräckliga förutsättningar
Beskrivning
Definition
Utbyte
Paket
Kontrovers ( Antinomy )
Syntetisk bedömning / Analytisk bedömning
Länk

Lista över booleska symboler