Logica combinatorie

În logica matematică , logica combinațională este o logică teoretică introdusă de Moses Schönfinkel în 1920 la o conferință din 1929 și dezvoltată de Haskell Brooks Curry pentru a elimina necesitatea variabilelor în matematică pentru a formaliza strict noțiunea de funcție și pentru a minimiza numărul de operatori necesari pentru a defini calculul predicatelor după Henry M. Sheffer . Mai recent, a fost folosit în informatică ca model teoretic de calcul și ca bază pentru proiectarea limbajelor de programare funcționale .

Conceptul de bază al logicii combinatorii este cel al combinatorului care este o funcție de ordin superior  ; utilizează doar aplicația funcțională și, eventual, alte combinatoare pentru a defini noi funcții de ordin superior. Fiecare combinator simplu tipabil este o demonstrație pentru Hilbert în logica intuiționistă și invers. Numim asta corespondența Curry-Howard

Introducere

Logica combinatorie se bazează pe două „operații” de bază (spunem și două „combinatoare”) S și K pe care le vom defini mai târziu; mai precis îi vom defini comportamentul sau „intenția”, deoarece logica combinatorie este o abordare a logicii care arată mai degrabă cum funcționează lucrurile decât cum pot fi descrise obiectele, spunem atunci că este o abordare intenționată a logicii. Dacă vrem să definim funcția pe care o vom numi C și care ia trei parametri și returnează ca rezultat primul aplicat la al treilea, întregul fiind aplicat celui de-al doilea, îl putem scrie:

C ≡ S ((S (KS) K) (S (KS) K) S) (KK)

care, după cum putem vedea, nu include o variabilă. Putem regreta că avantajul neutilizării variabilelor este plătit de lungimea expresiilor și de o anumită ilizibilitate. Astăzi, logica combinatorie este utilizată în principal de logicieni pentru a răspunde pozitiv la întrebarea „Este posibil să se facă fără variabile?” »Și de către informaticieni pentru a compila limbaje funcționale.

Logica combinatorie este un sistem de rescriere de prim ordin . Adică, spre deosebire de calculul lambda , acesta nu include nicio variabilă legată, ceea ce permite o teorie mult mai simplă. Are doar trei operatori: un operator binar și două constante.

Parantezare Pentru a simplifica scrierea, logica combinatorie elimină anumite paranteze și adoptă prin convenție asociativitatea din stânga. Cu alte cuvinte, (abcd ... z) este o prescurtare pentru (... (((ab) c) d) ... z).

Combinatoare de bază

Combinatorul de identitate, notat I , este definit de

I x = x .

Un alt combinator, notat cu K , face funcții constante: ( K x ) este funcția care, pentru orice parametru, returnează x , cu alte cuvinte

( K x ) y = x

pentru toți termenii x și y . Ca și în lambda-calculus , asociem aplicațiile de la stânga la dreapta, ceea ce face posibilă eliminarea parantezelor, așa că scriem

K x y = x .

Un alt combinator, notat S , distribuie parametrul (aici z ) aplicațiilor componente:

S x yz = xz ( yz )

S aplică rezultatul aplicării lui x la z la rezultatul aplicării lui y la z .

I pot fi construite din S și K , într - adevăr:

( S K K ) x = S K K x = K x ( K x ) = x .

Prin urmare, decretăm că I este un combinator derivat și că I = SKK și decidem să descriem toți combinatorii folosind S și K , ceea ce este rezonabil, deoarece putem arăta că acest lucru este suficient pentru a descrie „toate” funcțiile unei anumite forme. .

Reducerea

De fapt, transformările funcționează ca reduceri și pentru asta le scriem →. Prin urmare, obținem cele două reguli de reducere de bază ale logicii combinatorii.

K xy → x, S xyz → xz (yz).

Unele combinatoare derivate

• B ≡ S ( KS ) K . Combinatorul B corespunde operatorului de compoziție a funcției notat de obicei „   ”. Numele său este derivat din silogismul Barbara . Deci avem∘{\ displaystyle \ circ}

B xyz ≡ S ( KS ) K xyz → KS x ( K x) yz → S ( K x) yz → K xz (yz) → x (yz).

• C ≡ S (BBS) (KK) este un combinator care își inversează parametrii.

C xyz ≡ S (BBS) (KK) xyz → BBS x ( KK x) yz → B ( S x) ( K K x) yz → S x ( K K xy) z → xz ( KK xyz) → xz ( K yz) → xzy

• W ≡ SII . Combinatorul W face posibilă construirea unui alt combinator, și anume WW , care are proprietatea de a fi redus la sine. Avem astfel

WW ≡ SII ( SII ) → I ( SII ) ( I ( SII )) → SII ( I ( SII )) → SII ( SII ) ≡ WW

Sistemul de tip

Un tip poate fi asociat cu fiecare dintre combinatoare. Tipul unui combinator spune cum ia în considerare tipul parametrilor săi pentru a produce un obiect de un anumit tip. Astfel combinatorul I își schimbă parametrul în sine; dacă atribuim tipul α acestui parametru x, atunci putem spune că I x are tipul α și că I are tipul α → α. Aici săgeata → denotă constructorul de tip funcțional, aproximativ α → α este tipul clasei de funcții de la α la α, → a construit un nou tip α → α din tipul α.

K ia un parametru, să zicem de tipul α și redă o funcție a unui parametru de tipul β care redă primul parametru, tipul acestei ultime funcții este deci β → α și tipul lui K este astfel α → (β → α) , pe care scriem α → β → α. S ia trei parametri x, y și z; dați tipul α la al treilea parametru z și tipul γ la rezultatul final, al doilea parametru y ia un parametru de tip α și returnează un parametru de tip spunem β (tipul său este deci α → β), primul parametru x ia un parametru de tip α și returnează o funcție de tip β → γ, tipul său este deci α → (β → γ), pe care îl scriem α → β → γ. Să rezumăm, avem az: α, y: β → α și x: α → β → γ și S xyz: γ, concluzionăm că S are tipul (α → β → γ) → (α → β) → α → γ.

Rezultatul MN care constă în aplicarea lui M la N este tipabil dacă M are un tip funcțional, să zicem α → β și dacă N are tip α. MN are apoi tipul β.

Tipul de B este (α → β) → (γ → α) → γ → β. Fi văzut arătând că B xyz → * x (yz), sau prin aplicarea regulii compoziției la S ( KS ) K .

Tip C este (α → β → γ) → β → α → γ, pentru aceleași motive ca și indicate pentru B .

W, pe de altă parte, nu este tipabil. Putem vedea acest lucru amintind că S  : (α → β → γ) → (α → β) → α → γ și I  : (α → α). Dacă aplicăm S la I trebuie să avem α = β → γ, atunci dacă aplicăm SI la I trebuie să avem α = β, deci β = β → γ. Această ecuație nu are nicio soluție. Deci SII = W nu este tipabil.

În concluzie:

K  : α → β → α S  : (α → β → γ) → (α → β) → α → γ I  : α → α B  : (α → β) → (γ → α) → γ → β C  : (α → β → γ) → β → α → γ

Standardizare puternică

Dacă M este un combinator tipizat, atunci orice lanț de reducere care începe de la M este finit. Această proprietate se numește normalizare puternică .

Logica combinatorie și corespondența Curry-Howard

Se poate observa că modus ponens

P→ÎPÎ{\ displaystyle {\ frac {P \ to Q \ qquad P} {Q}}}

seamănă cu regula de conservare a tipului atunci când aplicăm un combinator de tip α → β unui combinator de tip α. Să examinăm, de asemenea, primele două axiome ale prezentării în stil hilbertian a logicii propoziționale, și anume:

K  : P → Q → P S  ( P → Q → R ) → ( P → Q ) → P → R .

Să ne amintim că permit formalizarea calculului propozițional intuiționist. Observăm că prima axiomă este identică cu tipul de K și că a doua axiomă este identică cu tipul de S dacă înlocuim propoziția P cu α, propoziția Q cu β și propoziția R cu γ. Această corespondență între propunere și tip și între combinator și demonstrație se numește corespondență Curry-Howard. Pune în paralel sistemul de deducție à la Hilbert pentru logica propozițională intuiționistă și logica combinatorie care, ar trebui remarcat, au fost descoperite independent.

Un exemplu

Formula

B  : (α → β) → (γ → α) → γ → β

înseamnă (în limbajul Coq , de exemplu) că B este o dovadă (oricare a priori) a formulei propoziționale (α → β) → (γ → α) → γ → β.

B ≡ S (KS) K

apoi oferă o dovadă eficientă a formulei din teoria lui Hilbert care utilizează doar modus ponens și axiomele K și S.

Acest lucru necesită o mică lucrare de rescriere: mai întâi, restaurăm parantezele

B ≡ (S (KS)) K

apoi, introducem operatorul ⇒

B ≡ (S ⇒ (K ⇒ S)) ⇒ K

în cele din urmă, folosim notația postfix  :

B ≡ KSK ⇒ S ⇒ ⇒

Apoi, această formulă oferă pașii demonstrației în direcția deducției. ⇒ denotă utilizarea modus ponens; K și S, utilizarea axiomelor K și S. Mai precis Q ≡ IP ⇒ înseamnă că dacă eu este demonstrarea P → Q și P demonstrarea P , atunci IP ⇒ este aceea de Q . Din păcate, această formulă nu oferă operații de substituții care trebuie utilizate în introducerea axiomelor.

Notația prefixată,

B ≡ ⇒ ⇒ S ⇒ KSK

reprezintă semnificația probei în limba Coq. Aici, informațiile lipsă sunt formulele P utilizate în modus ponens.

Demonstrație

Pentru a ușura scrierea, notăm

• P⁰ = (P → Q)
• Q⁰ = (R → P → Q)
• R⁰ = (R → P) → (R → Q)
• MP ( P ) denotă utilizarea modus ponens cu premisa P

Prin urmare, scopul este

• B = P⁰ → R⁰ .

1. MP ( P⁰ → Q⁰ ) înlocuiește obiectivul B cu cele 2 goluri
   • P¹ → B
   • P¹ = P⁰ → Q⁰
2. MP ( P⁰ → Q⁰ → R⁰ ) înlocuiește obiectivul P¹ → B cu cele 2 goluri
   • P² → (P¹ → B)
   • P² = P⁰ → Q⁰ → R⁰
3. S dovedește P² → (P¹ → B) deoarece
   • P² → (P¹ → B) = (P⁰ → Q⁰ → R⁰) → (P⁰ → Q⁰) → (P⁰ → R⁰)
4. MP ( Q⁰ → R⁰ ) înlocuiește obiectivul P² cu cele 2 goluri
   • P³ → P²
   • P³ = Q⁰ → R⁰
5. K dovedește P³ → P² deoarece
   • P³ → P² = (Q⁰ → R⁰) → P⁰ → (Q⁰ → R⁰)
6. S dovedește P³ pentru că
   • P³ = (R → P → Q) → (R → P) → (R → Q)
7. K dovedește P¹ pentru că
   • P¹ = P⁰ → Q⁰ = (P → Q) → R → (P → Q) .

(* demonstration à l'aide de Coq du syllogisme Barbara par la logique propositionnelle a la Hilbert *) Section Logique_propositionnelle_a_la_Hilbert. Variable P Q R : Prop. (* le modus ponens *) Ltac MP := fun P => match goal with |- ?G => assert(TMP: P->G); [ | apply TMP;clear TMP] end. Ltac K := match goal with | |- (?P -> ?Q -> ?P) => tauto | |- _ => fail end. Ltac S := match goal with | |- (?P -> ?Q -> ?R)->(?P->?Q)->?P->?R => tauto | |- _ => fail end. (* syllogisme Barbara. *) Theorem B : (P->Q)->(R->P)->(R->Q). MP((P->Q)->(R->P->Q)). MP((P->Q)->(R->P->Q)->((R->P)->(R->Q))). S. MP((R->P->Q)->((R->P)->(R->Q))). K. S. K. Qed. End Logique_propositionnelle_a_la_Hilbert.

Corespondența cu calculul λ

Orice expresie a logicii combinatorii admite o expresie echivalentă λ-calcul și orice expresie a λ-calcul admite o expresie logică combinatorie echivalentă.

De la logica combinatorie la calculul λ

Rețineți traducerea combinatorilor la calculul λ, este definită de: [[-]]λ{\ displaystyle [\! [-] \!] _ {\ lambda}}

• dacă denotă o variabilă  ;X{\ displaystyle x}[[X]]λ=X{\ displaystyle [\! [x] \!] _ {\ lambda} = x}
• [[K]]λ=λX.λy.X{\ displaystyle [\! [{\ mathsf {K}}] \!] _ {\ lambda} = \ lambda x. \ lambda yx} ;
• [[S]]λ=λX.λy.λz.Xz(yz){\ displaystyle [\! [{\ mathsf {S}}] \!] _ {\ lambda} = \ lambda x. \ lambda y. \ lambda z.xz (yz)} ;
• [[MNU]]λ=[[M]]λ[[NU]]λ{\ displaystyle [\! [M \, N] \!] _ {\ lambda} = [\! [M] \!] _ {\ lambda} \, [\! [N] \!] _ {\ lambda }}, pentru toți combinatorii și .M{\ displaystyle M}NU{\ displaystyle N}

Abstracție în logica combinatorie

Înainte de a defini reprezentarea calculului λ în logica combinatorie, trebuie să definim o abstracție în logica combinatorială. Dacă este un termen, definim cine va juca rolul . M{\ displaystyle M}[X].M{\ displaystyle [x] .M}λX.M{\ displaystyle \ lambda xM}

(la)[X].M=KMdacă X∉FV(M)(b)[X].X=Eu(vs.)[X].UX=Udacă X∉FV(U)(d)[X].UV=S([X].U)([X].V)dacă sau (la) sau (vs.) născut aplica.{\ displaystyle {\ begin {array} {llcl} (a) & {[} x] .M & = & {\ mathsf {K}} M \ qquad {\ textrm {si}} ~ x \ notin FV (M ) \\ (b) & {[} x] .x & = & {\ mathsf {I}} \\ (c) & {[} x] .Ux & = & U \ qquad {\ textrm {si}} ~ x \ notin FV (U) \\ (d) & {[} x] .UV & = & {\ mathsf {S}} ([x] .U) ([x] .V) \ qquad {\ textrm {si}} ~ {\ textrm {ni}} ~ (a) ~ {\ textrm {ni}} ~ (c) ~ {\ textrm {ne}} ~ {\ textrm {apply}}. \ end {array} }}

De la λ-calcul la logica combinatorie

Definim interpretarea termenilor calculului λ în termenii logicii combinatorii: M{\ displaystyle M}[[M]]VSL{\ displaystyle [\! [M] \!] _ {CL}}

[[X]]VSL=X[[MNU]]VSL=[[M]]VSL[[NU]]VSL[[λX.M]]VSL=[X].[[M]]VSL{\ displaystyle {\ begin {array} {rcl} {[} \! [x] \!] _ {CL} & = & x \\ {[} \! [MN] \!] _ {CL} & = & [\! [M] \!] _ {CL} [\! [N] \!] _ {CL} \\ {[} \! [\ Lambda xM] \!] _ {CL} & = & [ x]. [\! [M] \!] _ {CL} \ end {array}}}

Exemplu

Punctul fix combinat al lui Turing , notat, este exprimat în calculul λ . Apoi putem calcula: Θ{\ displaystyle \ Theta}(λX.λy.y(XXy))(λX.λy.y(XXy)){\ displaystyle (\ lambda x. \ lambda yy \, (x \, x \, y)) \, (\ lambda x. \ lambda yy \, (x \, x \, y))}

[[λy.y(XXy))]]VSL=[y].[[y(XXy))]]VSL=S([y].[[y]]VSL)([y].[[XXy]]VSL)=SEu([[XX]]VSL)=SEu(XX){\ displaystyle {\ begin {array} {rcl} [\! [\ lambda yy \, (x \, x \, y))] \!] _ {CL} & = & [y]. [\! [ y \, (x \, x \, y))] \!] _ {CL} \\ & = & S ([y]. [\! [y] \!] _ {CL}) ([y] . [\! [xxy] \!] _ {CL}) \\ & = & SI ([\! [xx] \!] _ {CL}) \\ & = & SI (xx) \ end {array} }}

atunci

[[λX.λy.y(XXy))]]VSL=[X].[[λy.y(XXy))]]VSL=[X].SEu(XX)=S([X].SEu)([X].XX)=S(S([X].S)([X].Eu))(S([X].X)([X].X)=S(S(KS)(KEu))(SEuEu){\ displaystyle {\ begin {array} {rcl} [\! [\ lambda x. \ lambda yy \, (x \, x \, y))] \!] _ {CL} & = & [x]. [\! [\ lambda yy \, (x \, x \, y))] \!] _ {CL} \\ & = & [x] .SI (xx) \\ & = & S ([x] . IF) ([x] .xx) \\ & = & S (S ([x] .S) ([x] .I)) (S ([x] .x) ([x] .x) \ \ & = & S (S (KS) (KI)) (SII) \ end {array}}}

Apoi definim doi combinatori A și Θ

A : = S (S (KS) (KI)) (SII)

Θ : = AA

Θ este un combinator cu punct fix.

Observăm că, indiferent dacă este termenul λ sau traducerea lui ca combinator, avem ΘX ⟶∗ X(ΘX){\ displaystyle \ Theta x ~ {\ stackrel {*} {\ longrightarrow}} ~ x (\ Theta x)}

Probleme nedecidabile în logica combinatorie

O formă normală este un combinator în care combinatorii primitivi nu sunt aplicați la suficiente argumente pentru a putea fi simplificate. Este indecidabil să știi

dacă un combinator general are o formă normală, dacă doi combinatori sunt echivalenți, etc.

Acest lucru este echivalent cu indecidabilitatea problemelor corespunzătoare ale calculului lambda .

Referințe

1. Katalin Bimbó , Enciclopedia Stanford a filosofiei , laborator de cercetare a metafizicii, Universitatea Stanford,2016( citește online )
2. Moses Schönfinkel "Über die Bausteine ​​der mathematischen Logik", Mathematische Annalen 92 , p.  305-316. Tradus în franceză de Geneviève Vandevelde: Moses Schönfinkel , „  Despre elementele de bază ale logicii matematice  ”, Matematică și științe umane , vol.  112,1990, p.  5-26 ( citește online ) și tradus în engleză în Moses Schönfinkel ( trad.  Stefan Bauer-Mengelberg), „Despre elementele de bază ale logicii matematice” , în Jean van Heijenoort , A Source Book in Mathematical Logic, 1879-1931 , Harvard Univ. Presa,1967( citiți online ) , p.  355-66.
3. HB Curry , „  Grundlagen der Kombinatorischen Logik  ”, American Journal of Mathematics , vol.  52, n o  3,1930, p.  509-536 ( DOI  10.2307 / 2370619 , citit online , accesat la 11 octombrie 2017 )
4. H. Curry, JR Hindley etJ. P. Seldin, Combinatory Logic II . Olanda de Nord, 1972.
5. Mai exact combinatorul.
6. Deși calculatorul folosind o logică bazată pe super-sumatoare mai puțin vorbăreți decât logica combinaționale bazată pe S și K .
7. Această convenție este destul de nefericită, deoarece se adoptă asociativitatea din dreapta pentru scrierea tipului de combinator .
8. x care apare aici nu este o variabilă în limbajul logicii combinatorii, deoarece, așa cum am spus, logica variabilă nu are variabile; de fapt, x este o „meta-variabilă” care face posibilă prezentarea identităților logicii combinatorii.
9. Teorema completitudinii lui Harvey Friedman .
10. Adică trecem de la ipoteze (aici axiome) la scopul de atins.
11. Adică ordinea tacticii („tactici” în engleză) folosită. Coq continuă modificând obiectivul până când îl identifică cu ipoteze, teoreme sau axiome.
12. J. Roger Hindley și Jonathan P. Seldin, Lambda-Calculu și Combinators an Introduction , Cambrdige University Press,2008( citește online )Secțiunea 2C p. 26.

Bibliografie

• Haskell Curry și Robert Feys , combinatoriu Logic I . Olanda de Nord 1958. Cea mai mare parte a conținutului acestei lucrări a fost depășită de lucrarea din 1972 și ulterioară.
• H. Curry, JR Hindley și JP Seldin, Combinatory Logic II . North-Holland, 1972. O retrospectivă completă a logicii combinatorii, incluzând o abordare cronologică.
• J. Roger Hindley și Jonathan P. Seldin, Lambda-Calculu și Combinators an Introduction , Cambrdige University Press,2008( citește online )
• J.-P. Desclés & ali, Combinatorial Logic and Lambda-calculus - logica operatorului - 2016 - Cépaduès * J.-P. Desclés & ali, Înțelesul calculelor după logica operatorului - 2016 - Cépaduès
• Jean-Pierre Ginisti , Combinatorial logic , Paris, PUF (col. „Que sais-je?” N ° 3205), 1997, 127 p.
• M. Shönfinkel, În: J. van Heijenoort, editor, De la Frege la Gödel , Harvard University Press, Cambridge, MA (1967), pp. 355–366 1924.
• J.-L. Krivine, Lambda-calcul, tipuri și modele , Masson, 1990, cap. Logică combinatorie , traducere în limba engleză disponibilă pe site-ul autorului [1] .
• Robert Feys , Tehnica logicii combinatorii În: Revue Philosophique de Louvain. A treia serie, volumul 44, nr. 1, 1946. pp. 74-103 [2]
• (ro) Henk Barendregt , The Lambda-Calculus , volumul 103, Elsevier Science Publishing Company, Amsterdam, 1984.

linkuri externe

• Înregistrări de autoritate  :
  • Biblioteca Națională a Franței ( date )
  • Sistem de documentare universitară
  • Biblioteca Congresului
  • Gemeinsame Normdatei