Lambek-laskenta

Lambek-laskenta ( eng. Lambek calculus , merkitty ) on Joachim Lambek [1] vuonna 1958 ehdottama muodollinen looginen järjestelmä , joka on tarkoitettu kuvaamaan luonnollisten kielten syntaksia . Matemaattisesta näkökulmasta Lambek-laskenta on lineaarisen logiikan fragmentti . $L$

Muodollinen määritelmä

Lambek-laskenta voidaan määritellä useilla vastaavilla tavoilla. Alla on Lambekin peräkkäisen laskennan määritelmä Gentzenin muodossa .

Lambek-laskenta toimii tyyppien kanssa (kielitieteen kannalta tyypit vastaavat tiettyjä sanaluokkia). Joukko on kiinteä , jonka alkioita kutsutaan primitiivityypeiksi. Niistä rakennetaan paljon kaikenlaisia. Muodollisesti Lambek-laskimen tyyppijoukko on pienin joukko, joka sisältää ja täyttää seuraavan ominaisuuden: jos , ovat tyyppejä, niin , , (sulut jätetään usein pois) ovat myös tyyppejä. Operaatioita ja kutsutaan vasen jako , oikea jako ja kertolasku . ${\displaystyle Pr=\{p_{1},p_{2},\dots \))$ $Tp$ $Pr$ $A$ $B$ ${\näyttötyyli (A\kenoviiva B)}$ ${\näyttötyyli (A\cdot B)}$ ${\näyttötyyli (A/B)}$ $\backslash$ ${\näyttötyyli /}$ $\cdot$

Primitiiviset tyypit merkitään yleensä latinalaisilla pienillä kirjaimilla, tyypit isoilla latinalaisilla kirjaimilla, tyyppijonoja isoilla kreikkalaisilla kirjaimilla ( , jne.). ${\näyttötyyli \gamma }$ $\Delta$

Sekventti on merkkijono muotoa , jossa , ja ovat Lambek-laskimen tyyppejä. Nuolen vasemmalla puolella olevaa osaa kutsutaan edeltäjäksi ja nuolen jälkeistä osaa seuraavaksi . $A_{1},\dots ,A_{n}\to B$ $n>0$ $A_{1},\dots ,A_{n},B$

Lambek-laskennan aksioomat ja säännöt selittävät, mitkä sekvenssit ovat johdettavissa . Ainoa aksiooma (tarkemmin sanottuna aksioomakaavio) on muodossa:

$A\to A$

Lambek-laskennassa on kuusi päättelysääntöä, kaksi kullekin operaatiolle [2] :

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

Sekvenssiä kutsutaan johdettaviksi , jos se voidaan saada aksioomista sääntöjä soveltamalla. Vastaavaa aksioomien ja sääntösovellusten ketjua kutsutaan johtamiseksi . Johdatettavuuden tosiasiaa merkitään . $\Gamma \to A$ $\mathrm {L} \vdash \Gamma \to A$

Esimerkkejä päätellyistä sarjoista

Sekvenssi (kutsutaan tyyppinostoksi ) on johdettavissa Lambek-laskennassa : $p\to q/(p\backslash q)$ $s$

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

Sekvenssi on johdettavissa Lambek-laskennassa: $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$

Lambekin kategoriset kieliopit

Lambekin kategoristen kielioppien käsite viittaa muodollisten kielioppien teoriaan ; ne ovat kategoristen kielioppien erikoistapaus . Tarkastellaan äärellistä ei-tyhjää joukkoa, jota kutsutaan aakkosiksi. - kaikkien äärellisen pituisten merkkijonojen joukko, jotka voivat koostua aakkosmerkeistä ; mitä tahansa tämän joukon osajoukkoa kutsutaan muodolliseksi kieleksi. $\Sigma$ ${\displaystyle \Sigma ^{\ast ))$ $\Sigma$

Lambekin kategorinen kielioppi koostuu kolmesta osasta: $\langle \Sigma ,S,\triangleright \rangle$

$\Sigma$ - aakkoset;
$S\in Tp$ - erottuva tyyppi kielioppissa;
$\triangleright \subseteq \Sigma \times Tp$ on äärellinen binäärirelaatio, joka määrittää jokaiselle aakkoston merkille äärellisen määrän Lambek-lasken tyyppejä.

Kieliopin tunnistama kieli on joukko sanoja, joiden muoto on , niin että jokaiselle merkille on vastaava tyyppi (joka tarkoittaa ) ja . $\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$

Esimerkki. Olkoon , primitiivinen tyyppi, ja relaatio määritellään seuraavasti , , . Tällainen kielioppi tunnistaa kielen . Esimerkiksi sana kuuluu tietyn kieliopin tunnistamaan kieleen, koska sillä on päätelty sekvenssi . $\Sigma =\{a,b\}$ $S=s$ ${\näyttötyyli \triangleright }$ $a\triangleright s/p$ $b\triangleright p$ $b\triangleright s\backslash p$ $\{a^{n}b^{n}|n>0\}$ $aaabbb$ $s/p,s/p,s/p,p,s\backslash p,s\backslash p\to s$

Esimerkkejä kielitieteestä

Jos otamme joukoksi jonkin luonnollisen kielen sanajoukkoa, on mahdollista käyttää Lambekin kielioppeja kuvaamaan tämän kielen lausejoukkoa (tai sen osaa). Tehtävänä on löytää kielioppi, joka tunnistaisi täsmälleen tietyn kielen kieliopillisesti oikeat lauseet tai ainakin kuvaisi oikein joitakin kielitieteilijöitä kiinnostavia kielellisiä ilmiöitä. Alla on erityisiä esimerkkejä johdettavissa olevista sekvensseistä, jotka vastaavat kieliopillisesti oikeita lauseita. $\Sigma$

Englanninkieliselle lauseelle John loves Mary "John loves Mary" voidaan määrittää sekvenssi [3] . Tässä erisnimet John , Mary vastaavat primitiivistä tyyppiä "substantiivilause" , joka tarkoittaa substantiivilauseita , ja transitiivinen verbi rakastaa vastaa kompleksista tyyppiä . Primitiivinen tyyppi "lause" vastaa deklaratiivisia lauseita. Tämä sekvenssi on johdettavissa Lambek-laskennassa: $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\kenoviiva S)/NP,NP\to S}}(/\to )$

Monimutkaisempi englanninkielinen lause John rakastaa, mutta Bill vihaa Marya "John rakastaa, mutta Bill vihaa Marya" määritetään päätellyksi sekvenssiksi [4] . $NP,(NP\kenoviiva S)/NP,((S/NP)\kenoviiva (S/NP))/(S/NP),NP,(NP\kenoviiva S)/NP,NP\to S$

Yllä olevien esimerkkien yhdistämiseksi osion alussa annettuun kategoristen kielioppien muodolliseen määritelmään otamme primitiivisen tyypin erottuvaksi tyypiksi ja määritämme suhteen siten, että yllä olevien englanninkielisten lauseiden sanoja verrataan tyyppeihin. vastaavat niitä tarkasteluissa jaksoissa. Sitten lauseet John rakastaa Mariaa , John rakastaa, mutta Bill vihaa Mariaa , kuuluvat tämän kieliopin tunnistamaan kieleen. $S$ ${\näyttötyyli \triangleright }$

Ominaisuudet

Lambek-laskennassa leikkaussääntö on sallittu [1] . Toisin sanoen sekvenssin johdettavuus seuraa muodon sekvenssien johdettavuudesta . $\Pi \to A$ $\Gamma ,A,\Delta \to B$ $\Gamma ,\Pi ,\Delta \to B$
Lambekin kielioppien luoma kielten luokka on sama kuin yhteydettömien kielten luokka, jossa ei ole tyhjää sanaa [5] .
Lambek-laskennan sekvenssin johdettavuuden tarkistamisen ongelma on NP-täydellinen [6] .
Lambek-laskenta on oikea ja täydellinen jakopuoliryhmämallien suhteen, ja on olemassa universaali malli. Se on täydellinen myös -mallien ( kielimallit , eng. kielimallit ) ja -mallien ( relaatiomallit , eng. relaatiomallit ) suhteen [7] . $L$ $R$
Lambda-laskenta voidaan lisätä lambda-laskentaan , jolloin Lambek-laskennan päätelmiin liittyy lambda-tyypin muunnoksia [8] . Kielellisestä näkökulmasta tämä mahdollistaa lauseiden semantiikan mallintamisen.

Muutokset

Lambek-laskusta on useita muunnelmia, jotka perustuvat muiden kuin jakolasku- ja kertolaskutoimintojen lisäämiseen sekä uusien aksioomien ja päättelysääntöjen lisäämiseen. Alla on joitain vaihtoehtoja.

Lambek-laskenta yksiköllä ( ). Se sallii muodon sekvenssit (joilla on 0 tyyppiä edeltäjässä). Yksikkö ( ) lisätään kelvollisten merkkien joukkoon, josta tyypit muodostetaan. Sitä varten otetaan käyttöön yksi aksiooma ja yksi sääntö: $L_{\mathbf {1} }^{\ast }$ $\to B$ $\mathbf {1}$

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

Multiplikatiiv-additiivinen Lambek-laskenta ( multiplikatiivinen-additiivinen Lambek-laskenta ) on laajennus , jossa tyyppejä rakennetaan jaon ja kertomisen lisäksi myös konjunktion ja disjunktion avulla . Heille otetaan käyttöön seuraavat 6 sääntöä: $L$ ${\näyttötyyli \kiila }$ $\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 )$

Katso myös

Muistiinpanot

↑ 12 Lambek , 1958 .
↑ Pentus, 1995 , s. 732.
↑ Moortgat, 1988 , s. neljätoista.
↑ Moortgat, 1988 , s. 36.
↑ Pentus, 1995 .
↑ Pentus, 2006 .
↑ Pentus, 1999 .
↑ Moortgat, 1988 .

Kirjallisuus

Lambek, J. The Mathematics of Sentence Structure // The American Mathematical Monthly . - 1958. - Voi. 65 , no. 3 . — s. 154-170 . — ISSN 0002-9890 . - doi : 10.2307/2310058 .
Moortgat, M. Kategoriaaliset tutkimukset: Lambek Calculuksen loogiset ja kielelliset näkökohdat : [ eng. ] . Foris-julkaisut. - 1988. - ISBN 9789067653879 .
Pentus M. R. Lambek-laskenta ja muodolliset kieliopit // Fundamentaali- ja sovellettu matematiikka. - 1995. - T. 1 , nro 3 . - S. 729-751 . (Venäjän kieli)
Pentus M. R. Lambek-syntaktisen laskennan täydellisyys // Perus- ja sovellettu matematiikka. - 1999. - V. 5 , nro 1 . - S. 193-219 . (Venäjän kieli)
Pentus, M. Lambek-laskenta on NP-täydellinen (englanniksi) // Teoreettinen tietojenkäsittelytiede. - 2006. - Voi. 357 , nro. 1 . — s. 186-201 . — ISSN 0304-3975 . - doi : 10.1016/j.tcs.2006.03.018 .

Logiikka

Filosofia • Semantiikka • Syntaksi • Historia

Logiikkaryhmät

klassista logiikkaa	Aristoteelinen logiikka propositionaalinen logiikka Ensimmäisen asteen logiikka Toisen asteen logiikka korkeamman asteen logiikkaa
matemaattinen logiikka	joukko teoria Mallin teoria Lasketettavuuden teoria Todistusteoria ja konstruktiivinen matematiikka Lineaarinen logiikka muodollinen järjestelmä luonnollinen johtopäätös Sekvenssilaskenta Logiikan algebra Asiaankuuluva logiikka Deonttinen logiikka intuitionistinen logiikka Lambek-laskenta
Ei-klassinen logiikka	intuitionismi sumea logiikka Alirakennelogiikka logiikka Kuvauslogiikka Moniarvoinen logiikka Logiikka synteesi Sidontalogiikka Temporaalinen logiikka Modaalinen logiikka ( Hybridilogiikka ) episteeminen logiikka
Filosofinen logiikka	Kriittinen ajattelu epävirallista logiikkaa deduktiivinen päättely

Komponentit

Sieppaus (logiikka)
Todennäköisyys
lausunto
Vähennys / Induktio / Traduction
Todellisuus
induktiivinen päättely
päättely
boolen vakio
Totta
loogista seuraamista
Looginen muoto
Tarpeelliset ja riittävät olosuhteet
Kuvaus
Määritelmä
Korvaus
Paketti
Kiista ( antinomia )
Synteettinen arviointi / Analyyttinen arviointi
Linkki

Luettelo loogisista symboleista