Calculul Lambek

Calculul Lambek ( ing. calculul Lambek , notat ) este un sistem logic formal propus în 1958 de Joachim Lambek [1] , care are scopul de a descrie sintaxa limbilor naturale . Din punct de vedere matematic, calculul Lambek este un fragment de logică liniară . $L$

Definiție formală

Calculul Lambek poate fi definit în mai multe moduri echivalente. Mai jos este definiția calculului secvenţial al lui Lambek în forma lui Gentzen .

Calculul Lambek funcționează cu tipuri (din punct de vedere lingvistic, tipurile corespund anumitor categorii de cuvinte). Un set este fix , ale cărui elemente se numesc tipuri primitive. Din ele sunt construite o mulțime de toate tipurile. Formal, mulțimea de tipuri din calculul Lambek este cea mai mică mulțime care conține și satisface următoarea proprietate: dacă , sunt tipuri, atunci , , (parantezele sunt adesea omise) sunt și tipuri. Operațiile și se numesc împărțire la stânga , împărțire la dreapta și , respectiv , înmulțire . $Pr=\{p_{1},p_{2},\dots \}$ $Tp$ $Pr$ $A$ $B$ $(A\backslash B)$ $(A\cdot B)$ $(A/B)$ $\backslash$ $/$ $\cdot$

Tipurile primitive sunt de obicei notate cu litere latine mici, tipurile cu litere latine mari, secvențele de tipuri cu litere grecești mari ( , etc.). $\gamma$ $\Delta$

Un secvent este un șir de forma , unde , și sunt tipurile calculului Lambek. Partea din stânga săgeții se numește antecedent , iar partea de după săgeată se numește succesent . $A_{1},\dots, A_{n}\to B$ $n>0$ $A_{1},\dots, A_{n},B$

Axiomele și regulile calculului Lambek explică care secvențe sunt derivate . Singura axiomă (mai precis, schema axiomelor) are forma:

$A\to A$

Calculul Lambek are 6 reguli de inferență, câte două pentru fiecare operație [2] :

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

O secvență se numește derivabilă dacă poate fi obținută din axiome prin aplicarea regulilor. Lanțul corespunzător de axiome și aplicații de reguli se numește derivație . Faptul de derivabilitate este notat ca . $\Gamma \to A$ $\mathrm {L} \vdash \Gamma \to A$

Exemple de secvențe deduse

Secvența (numită tip lifting ) este derivată în calculul Lambek: $p\la 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 /)$

Secvența este derivabilă în calculul Lambek: $p\cdot (q/r)\la (p\cdot q)/r$

${\cfrac {{\cfrac {{\cfrac ({\cfrac {p\la p\quad q\to q}{p,q\to p\cdot q)}(\la \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$

Gramaticile categorice ale lui Lambek

Conceptul de gramatică categorială a lui Lambek se referă la teoria gramaticilor formale ; sunt un caz special de gramatici categorice . Considerăm o mulțime finită nevidă numită alfabet. - mulţimea tuturor şirurilor de lungime finită care pot fi compuse din caractere alfabetice ; orice submulțime a acestei mulțimi se numește limbaj formal. $\Sigma$ $\Sigma ^{\ast }$ $\Sigma$

Gramatica categorică a lui Lambek este o structură din 3 componente: $\langle \Sigma, S,\triangleright \rangle$

$\Sigma$ - alfabet;
$S\in Tp$ - tip distins în gramatică;
$\triangleright \subseteq \Sigma \times Tp$ este o relație binară finită care atribuie fiecărui caracter al alfabetului un număr finit de tipuri ale calculului Lambek.

O limbă recunoscută de o gramatică este un set de cuvinte de forma , astfel încât pentru fiecare caracter să existe un tip corespunzător (care înseamnă ) și . $\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$

Exemplu. Fie , un tip primitiv, iar relația este definită după cum urmează , , . O astfel de gramatică recunoaște o limbă . De exemplu, un cuvânt aparține unei limbi recunoscute de o anumită gramatică deoarece are o secvență dedusă . $\Sigma =\{a,b\}$ $S=s$ $\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$

Exemple din lingvistică

Dacă luăm ca set setul de cuvinte ale unui limbaj natural, va fi posibil să folosim gramaticile Lambek pentru a descrie setul de propoziții din această limbă (sau o parte a acesteia). Sarcina este de a găsi o gramatică care să recunoască exact propozițiile corecte din punct de vedere gramatical ale unei anumite limbi sau cel puțin să descrie corect unele dintre fenomenele lingvistice de interes pentru lingviști. Mai jos sunt date exemple particulare de secvențe derivabile corespunzătoare propozițiilor corecte din punct de vedere gramatical. $\Sigma$

Propoziției din engleză John loves Mary „John loves Mary” i se poate atribui o secvență [3] . Aici numele proprii Ioan , Maria corespund tipului primitiv „expresiune nominală” care denotă sintagme nominale, iar verbul tranzitiv iubește corespunde tipului complex . Tipului primitiv „propoziție” corespunde propozițiilor declarative. Această secvență poate fi derivată în calculul Lambek: $NP,(NP\backslash S)/NP,NP\la S$ $NP$ $(NP\backslash S)/NP$ $S$

${\cfrac {{\cfrac {S\la S\quad NP\to NP}{NP,NP\backslash S\to S))(\backslash \to )\quad NP\to NP}{NP, (NP\backslash S)/NP,NP\la S}}(/\la )$

Propoziției engleze mai complexă, pe care John loves but Bill hates Mary „John loves, but Bill hates Mary” i se atribuie secvența dedusă [4] . $NP,(NP\backslash S)/NP,((S/NP)\backslash (S/NP))/(S/NP),NP,(NP\backslash S)/NP,NP\la S$

Pentru a conecta exemplele de mai sus cu definiția formală a gramaticilor categorice dată la începutul secțiunii, luăm tipul primitiv ca tip distinctiv și definim relația astfel încât cuvintele din propozițiile engleze de mai sus să fie comparate cu tipurile. corespunzând acestora în secvenţele considerate. Apoi propozițiile John loves Mary , John loves but Bill hates Mary vor aparține limbajului recunoscut de această gramatică. $S$ $\triangleright$

Proprietăți

În calculul Lambek, regula de tăiere este admisibilă [1] . Cu alte cuvinte, deductibilitatea secventului decurge din derivabilitatea secventelor de forma . $\Pi \to A$ $\Gamma, A,\Delta \to B$ $\Gamma ,\Pi ,\Delta \to B$
Clasa de limbi generate de gramaticile Lambek coincide cu clasa de limbi fără context fără cuvântul gol [5] .
Problema verificării deductibilității unei secvențe în calculul Lambek este NP-complet [6] .
Calculul Lambek este corect și complet în ceea ce privește modelele de semigrup de diviziune și există un model universal. Este completă și în ceea ce privește -modelele ( modele de limbaj , modele de limbaj ing. ), și cu privire la -modele ( modele relaționale , modele relaționale ing . ) [7] . $L$ $R$
Calculul Lambda poate fi adăugat la calculul lambda , astfel încât inferențe în calculul Lambek să fie însoțite de conversii de tip lambda [8] . Din punct de vedere lingvistic, aceasta permite modelarea semanticii propozițiilor.

Modificări

Există o serie de variante ale calculului Lambek bazate pe adăugarea de operații, altele decât împărțirea și înmulțirea și adăugarea de noi axiome și reguli de inferență. Mai jos sunt câteva dintre opțiuni.

Calcul Lambek cu unitatea ( ). Permite secvențe de formă (care au 0 tipuri în antecedent). Se adaugă o unitate ( ) la setul de caractere valide din care sunt construite tipuri. Pentru aceasta, sunt introduse o axiomă și o regulă: $L_{\mathbf {1} }^{\ast }$ $\la B$ $\mathbf {1}$

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

Calcul Lambek multiplicativ-aditiv ( calculul Lambek multiplicativ-aditiv ) este o extensie în care tipurile sunt construite nu numai cu ajutorul diviziunii și înmulțirii, ci și cu ajutorul conjuncției și disjuncției . Pentru ei, sunt introduse următoarele 6 reguli: $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}\la)$

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

Vezi și

Note

↑ 12 Lambek , 1958 .
↑ Pentus, 1995 , p. 732.
↑ Moortgat, 1988 , p. paisprezece.
↑ Moortgat, 1988 , p. 36.
↑ Pentus, 1995 .
↑ Pentus, 2006 .
↑ Pentus, 1999 .
↑ Moortgat, 1988 .

Literatură

Lambek, J. The Mathematics of Sentence Structure // The American Mathematical Monthly . - 1958. - Vol. 65 , nr. 3 . — P. 154-170 . — ISSN 0002-9890 . - doi : 10.2307/2310058 .
Moortgat, M. Investigații categoriale: Aspecte logice și lingvistice ale calculului Lambek : [ ing. ] . Publicatii Foris. - 1988. - ISBN 9789067653879 .
Pentus M. R. Lambek calcul și gramatici formale // Matematică fundamentală și aplicată. - 1995. - T. 1 , nr 3 . - S. 729-751 . (Rusă)
Pentus M. R. Completitudinea calculului sintactic Lambek // Matematică fundamentală și aplicată. - 1999. - V. 5 , Nr. 1 . - S. 193-219 . (Rusă)
Pentus, M. Lambek calculul este NP-complet (engleză) // Informatică teoretică. - 2006. - Vol. 357 , nr. 1 . — P. 186-201 . — ISSN 0304-3975 . - doi : 10.1016/j.tcs.2006.03.018 .

Logici

Filosofie • Semantică • Sintaxă • Istorie

Grupuri logice

logica clasica	logica aristotelică Logica propozițională Logica de ordinul întâi Logica de ordinul doi logica de ordin superior
logica matematica	teoria multimilor Teoria modelului Teoria computabilității Teoria dovezilor și matematică constructivă Logica liniară sistem formal concluzie firească Calcul de secvență Algebra logicii Logica relevanta Logica deontică logica intuiționistă calculul Lambek
Logica non-clasică	intuitionism logica fuzzy Logica substructurala logica Logica descrierii Logica cu mai multe valori Sinteza logica Logica obligatorie Logica temporală Logica modală ( logica hibridă ) logica epistemică
Logica filozofică	Gândire critică logica informala motiv dedus

Componente

Lista simbolurilor booleene