Lambek kalkulus

A Lambek -számítás ( eng. Lambek calculus , jelölve ) egy Joachim Lambek [1] által 1958-ban javasolt formális logikai rendszer, amely a természetes nyelvek szintaxisát hivatott leírni . Matematikai szempontból a Lambek-számítás a lineáris logika töredéke . $L$

Formális definíció

A Lambek-számítás többféle ekvivalens módon definiálható. Az alábbiakban a Lambek-féle szekvenciális kalkulus definíciója található Gentzen alakjában .

A Lambek-számítás típusokkal dolgozik (nyelvészeti szempontból a típusok bizonyos szókategóriáknak felelnek meg). Egy halmaz rögzített , melynek elemeit primitív típusoknak nevezzük. Nagyon sok minden típus épül belőlük. Formálisan a Lambek-számítás típuskészlete a legkisebb halmaz, amely tartalmazza és kielégíti a következő tulajdonságot: ha , típusok, akkor a , , (a zárójeleket gyakran elhagyják) is típusok. A és műveleteket balra osztásnak , jobbos osztásnak és szorzásnak nevezik . ${\displaystyle Pr=\{p_{1},p_{2},\dots \))$ $Tp$ $Pr$ $A$ $B$ $(A\backslash B)$ $(A\cdot B)$ $(A/B)$ $\backslash$ $/$ $\cdot$

A primitív típusokat általában kis latin betűkkel, a típusokat latin nagybetűkkel, a típussorokat nagy görög betűkkel ( stb .) jelöljük. $\gamma$ $\Delta$

A szekvencia egy formátumú karakterlánc , ahol , és a Lambek-számítás típusai. A nyíltól balra lévő részt előzménynek , a nyíl utáni részt pedig utódlásnak nevezzük . $A_{1},\dots ,A_{n}\to B$ $n>0$ $A_{1},\dots ,A_{n},B$

A Lambek-számítás axiómái és szabályai megmagyarázzák, mely sorozatok származtathatók . Az egyetlen axióma (pontosabban az axiómák séma) a következő formában van:

$A\to A$

A Lambek-számításnak 6 következtetési szabálya van, mindegyik művelethez kettő [2] :

${\cfrac {\Gamma ,A,\Delta \to C\quad \Pi \to B}{\Gamma ,\Pi ,B\backslash A,\Delta \to C))\;(\backslash \ to )\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 \A\quad \Delta \B}{\Gamma ,\Delta \A\cdot B))\;(\cdot )$

Egy sorozatot származtathatónak nevezünk, ha az axiómákból a szabályok alkalmazásával megkapható. Az axiómák és szabályalkalmazások megfelelő láncát levezetésnek nevezzük . A levezethetőség tényét jelöljük . $\Gamma \to A$ $\mathrm {L} \vdash \Gamma \to A$

Példák kikövetkeztetett sorozatokra

A szekvencia (amelyet típusemelésnek neveznek) a Lambek-számításból származtatható: $p\to q/(p\backslash q)$ $p$

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

A sorozat a Lambek-számításból származtatható : $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$

Lambek kategorikus nyelvtanai

A Lambek-féle kategorikus nyelvtan fogalma a formális nyelvtan elméletére utal ; a kategorikus nyelvtanok speciális esetei . Egy véges, nem üres halmazt tekintünk, amelyet ábécének nevezünk. - az összes olyan véges hosszúságú karakterlánc halmaza, amely alfabetikus karakterekből állhat össze ; ennek a halmaznak bármely részhalmazát formális nyelvnek nevezzük. $\Sigma$ ${\displaystyle \Sigma ^{\ast ))$ $\Sigma$

Lambek kategorikus nyelvtana 3 összetevőből áll : $\langle \Sigma ,S,\triangleright \rangle$

$\Sigma$ - ábécé;
$S\in Tp$ - megkülönböztetett típus a nyelvtanban;
$\triangleright \subseteq \Sigma \times Tp$ véges bináris reláció, amely az ábécé minden karakteréhez a Lambek-számítás véges számú típusát rendeli hozzá.

A nyelvtan által felismert nyelv formájú szavak halmaza , így minden karakterhez tartozik egy megfelelő típus (amely jelentése ) és . $\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$

Példa. Legyen , primitív típus, és a relációt a következőképpen definiáljuk: , , . Az ilyen nyelvtan felismeri a nyelvet . Például egy szó egy adott nyelvtan által felismert nyelvhez tartozik, mert kikövetkeztetett szekvenciája van . $\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$

Példák a nyelvészetből

Ha halmaznak vesszük valamely természetes nyelv szavainak halmazát, akkor a Lambek nyelvtanok segítségével leírhatjuk ennek a nyelvnek a mondatkészletét (vagy annak egy részét). A feladat az, hogy olyan nyelvtant találjunk, amely pontosan felismerné az adott nyelv nyelvtanilag helyes mondatait, vagy legalább helyesen írna le néhány, a nyelvészek érdeklődésére számot tartó nyelvi jelenséget. Az alábbiakban a nyelvtanilag helyes mondatoknak megfelelő származtatott szekvenciákra mutatunk be konkrét példákat. $\Sigma$

A John loves Mary angol mondathoz "John loves Mary" hozzá lehet rendelni egy szekvenciát [3] . Itt a János , Mária tulajdonnevek a főnévi kifejezéseket jelölő " főnévi kifejezés" primitív típusnak felelnek meg , a tranzitív szeret ige pedig az összetett típusnak felel meg . A primitív "mondat" típus a kijelentő mondatoknak felel meg. Ez a sorozat a Lambek-számításból származtatható: $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 )$

Az összetettebb angol mondat John loves de Bill hates Mary "John loves, but Bill hates Mary" (John szereti, de Bill gyűlöli Maryt) a következtetett sorrendet kapja [4] . $NP,(NP\backslash S)/NP,((S/NP)\backslash (S/NP))/(S/NP),NP,(NP\backslash S)/NP,NP\to S$

Ahhoz, hogy a fenti példákat összekapcsoljuk a kategorikus nyelvtanok rész elején megadott formális definíciójával, a primitív típust vesszük megkülönböztetett típusnak , és definiáljuk a kapcsolatot úgy, hogy a fenti angol mondatok szavait összehasonlítsuk a típusokkal. azoknak megfelelő szekvenciákban. Ezután a John szereti Máriát , John szereti, de Bill utálja Maryt mondatok a nyelvtan által felismert nyelvhez tartoznak majd. $S$ $\triangleright$

Tulajdonságok

A Lambek-számításban a vágási szabály megengedett [1] . Más szóval, a szekvencia levezethetősége a formájú szekvenciák származtathatóságából következik . $\Pi \to A$ $\Gamma ,A,\Delta \to B$ $\Gamma ,\Pi ,\Delta \to B$
A Lambek nyelvtanok által generált nyelvek osztálya egybeesik az üres szó nélküli kontextusmentes nyelvek osztályával [5] .
A szekvencia levezethetőségének ellenőrzésének problémája a Lambek-számításban NP-teljes [6] .
A Lambek-számítás helyes és teljes a felosztási félcsoport modellek tekintetében, és létezik egy univerzális modell. Teljes a -modellek ( nyelvi modellek , angol nyelvi modellek ), és a -modellek ( relációs modellek , angol relációs modellek ) tekintetében is [7] . $L$ $R$
A lambda-számítást hozzáadhatjuk a lambda-számításhoz , így a Lambek-számításban a következtetéseket lambda típusú konverziók kísérik [8] . Nyelvi szempontból ez lehetővé teszi a mondatok szemantikájának modellezését.

Módosítások

A Lambek-számításnak számos változata létezik, amelyek az osztáson és szorzáson kívüli műveletek összeadásán, valamint új axiómák és következtetési szabályok hozzáadásán alapulnak. Az alábbiakban bemutatunk néhány lehetőséget.

Lambek-számítás mértékegységgel ( ). Engedélyezi a formájú sorozatokat (amelyeknek az előzményben 0 típusuk van). Egy egység ( ) kerül hozzáadásra az érvényes karakterkészlethez, amelyből a típusok épülnek. Ehhez egy axiómát és egy szabályt vezetnek be: ${\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))$

A multiplikatív-additív Lambek-számítás ( multiplikatív-additív Lambek-számítás ) egy olyan kiterjesztés , amelyben nem csak osztás és szorzás, hanem konjunkció és diszjunkció segítségével is épülnek fel a típusok . Számukra a következő 6 szabályt vezetik be: $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 )$

Lásd még

Jegyzetek

↑ 1958. Lambek 12 .
↑ Pentus, 1995 , p. 732.
↑ Moortgat, 1988 , p. tizennégy.
↑ Moortgat, 1988 , p. 36.
↑ Pentus, 1995 .
↑ Pentus, 2006 .
↑ Pentus, 1999 .
↑ Moortgat, 1988 .

Irodalom

Lambek, J. The Mathematics of Sentence Structure // The American Mathematical Monthly . - 1958. - 1. évf. 65 , sz. 3 . — P. 154-170 . — ISSN 0002-9890 . - doi : 10.2307/2310058 .
Moortgat, M. Kategoriális vizsgálatok: A Lambek-kalkulus logikai és nyelvi vonatkozásai : [ eng. ] . Foris kiadványok. - 1988. - ISBN 9789067653879 .
Pentus M. R. Lambek-számítás és formális nyelvtan // Fundamental and alkalmazott matematika. - 1995. - T. 1 , 3. sz . - S. 729-751 . (Orosz)
Pentus M. R. A Lambek szintaktikai számítás teljessége // Alapvető és alkalmazott matematika. - 1999. - V. 5 , 1. sz . - S. 193-219 . (Orosz)
Pentus, M. A Lambek-számítás NP-teljes (angol) // Theoretical Computer Science. - 2006. - 20. évf. 357. sz . 1 . — P. 186-201 . — ISSN 0304-3975 . - doi : 10.1016/j.tcs.2006.03.018 .

Logikák

Filozófia • Szemantika • Szintaxis • Történelem

Logikai csoportok

klasszikus logika	Arisztotelészi logika propozíciós logika Elsőrendű logika Másodrendű logika magasabb rendű logika
matematikai logika	halmazelmélet Modellelmélet Kiszámíthatóság elmélet Bizonyításelmélet és konstruktív matematika Lineáris logika formális rendszer természetes következtetés Sorozatszámítás Logikai algebra Releváns logika Deontikus logika intuicionista logika Lambek kalkulus
Nem klasszikus logika	intuicionizmus zavaros logika Szubstrukturális logika logika Leírás logika Többértékű logika Logikai szintézis Kötési logika Időbeli logika Modális logika ( Hibrid logika ) episztemikus logika
Filozófiai logika	Kritikus gondolkodás informális logika deduktív érvelés

Alkatrészek

Logikai szimbólumok listája