Kombinatorikus logika

A matematikai logikában a kombinációs logika olyan elméleti logika, amelyet Moses Schönfinkel vezetett be 1920-ban egy 1929-es konferencián, és amelyet Haskell Brooks Curry fejlesztett ki annak érdekében, hogy kiküszöbölje a matematika változóinak szükségességét a funkció fogalmának szigorú formalizálása és a szükséges operátorok számának minimalizálása érdekében. hogy meghatározzuk a predikátumok kiszámítását Henry M. Sheffer nyomán . Újabban a számítástechnikában a számítás elméleti modelljeként és a funkcionális programozási nyelvek tervezésének alapjaként használják .

A kombinatorikus logika alapkoncepciója a kombinátoré, amely egy magasabb rendű függvény  ; csak a függvényalkalmazást és esetleg más kombinátorokat használja új magasabb rendű függvények meghatározásához. Minden egyszerűen gépelhető kombinátor demonstráció Hilbert számára az intuíciós logikában és fordítva. Ezt hívjuk Curry-Howard levelezésnek

Bevezetés

A kombinatorikus logika két alapvető „műveleten” alapul (két „kombinátort is mondunk”) S és K , amelyeket később meghatározunk; pontosabban meghatározzuk annak viselkedését vagy "szándékát", mert a kombinatorikus logika a logika megközelítése, amely inkább megmutatja a dolgok működését, mint az objektumok leírását, akkor azt mondjuk, hogy ez a logika szándékos megközelítése. Ha meg akarjuk definiálni azt a függvényt, amelyet C-nek fogunk hívni, és amely három paramétert vesz fel, és ennek eredményeként az első a harmadikra ​​lesz alkalmazva, az egész pedig a másodikra ​​vonatkozik, akkor megírhatjuk:

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

amely, mint láthatjuk, nem tartalmaz változót. Sajnálhatjuk, hogy a változók nem használatának előnyét a kifejezések hossza és bizonyos olvashatatlanság fizeti meg. Ma a kombinatorikus logikát főleg a logikusok használják, hogy pozitívan megválaszolják a kérdést: "Meg lehet-e tenni változók nélkül?" »Számítógépes tudósok pedig funkcionális nyelvek összeállításához .

A kombinatorikus logika elsőrendű átírási rendszer . Vagyis a lambda-számítástól eltérően nem tartalmaz összekapcsolt változókat, ami sokkal egyszerűbb elméletet tesz lehetővé. Csak három operátora van: egy bináris operátor és két állandó.

Zárójeles Az írás egyszerűsítése érdekében a kombinatorikus logika eltávolít bizonyos zárójeleket, és a bal oldali konvenció asszociativitás alapján átveszi őket. Más szavakkal, az (abcd ... z) a (... (((ab) c) d) ... z) rövidítése.

Alapvető kombinátorok

Az I jelölésű identitás-kombinátort az határozza meg

I x = x .

Egy másik kombinátor, amelyet K jelöl , állandó függvényeket készít: ( K x ) az a függvény, amely bármely paraméter esetén x-et ad vissza , más szóval

( K x ) y = x

minden x és y kifejezésre . Akárcsak a lambda-calculus esetében , az alkalmazásokat balról jobbra kapcsoljuk, ami lehetővé teszi a zárójelek eltávolítását, ezért írjuk

K x y = x .

Egy másik kombinátor, az S nevű , elosztja a paramétert (itt z ) a komponens alkalmazások számára:

S x yz = xz ( yz )

S az x és z alkalmazásának eredményét alkalmazza y és z alkalmazásának eredményére .

Azt lehet kialakítani a S és a K , sőt:

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

Ezért elrendeljük, hogy én egy származéka kombináló és I = SKK és úgy döntünk, hogy leírja az összes combinators használó S és K , ami ésszerű, mert tudjuk mutatni, hogy ez elegendő, hogy leírja az „összes” funkciót d „egy bizonyos formájának .

A csökkentés

Valójában a transzformációk úgy működnek, mint a redukciók, és ezért megírjuk őket →. Megkapjuk tehát a kombinatorikus logika két alapvető redukciós szabályát.

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

Néhány származékos kombinátor

• B ≡ S ( KS ) K . A B kombinátor megfelel a funkciókompozíció operátornak, amelyet általában "  " jeleznek  . Neve a Barbara szillogizmusból származik . Így van∘{\ displaystyle \ circ}

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

• A C ≡ S (BBS) (KK) egy kombinátor, amely megfordítja a paramétereit.

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 . A W kombinátor lehetővé teszi egy másik kombinátor, nevezetesen a WW építését , amelynek az a tulajdonsága, hogy önmagára redukálódik. Így van

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

A típusrendszer

Az egyes kombinátorokhoz típus társítható . A kombinátor típusa megmondja, hogyan veszi figyelembe a paramétereinek típusát egy bizonyos típusú objektum előállításához. Így az I kombinátor önmagában megváltoztatja a paraméterét; ha az α típust ennek az x paraméternek tulajdonítjuk, akkor azt mondhatjuk, hogy I x-nek van α típusa, és nekem α → α típusa van. Itt a → nyíl a funkcionális típusú konstruktort jelzi, nagyjából az α → α a funkciók osztályának típusa α-tól α-ig, → az α típusból új α → α típust épített.

K vesz egy paramétert, mondjuk az α típusra, és egy β típusú paraméter függvényét adja, amely az első paramétert adja meg, ennek az utolsó függvénynek a típusa tehát β → α, a K típusa tehát α → (β → α) , amelyet α → β → α írunk. S három x, y és z paramétert vesz fel; adja meg az α típust a harmadik z paraméternek és γ típust a végeredménynek, a y második paraméter felvesz egy α típusú paramétert, és egy β típusú paramétert ad vissza (típusa ezért α → β), az első vesz egy α típusú paramétert, és egy β → γ típusú függvényt ad vissza, típusa tehát α → (β → γ), amelyet α → β → γ írunk. Összefoglalva, vannak az: α, y: β → α és x: α → β → γ és S xyz: γ, arra a következtetésre jutunk, hogy S típusa (α → β → γ) → (α → β) → α → γ.

Az eredmény MN , amely abból áll, hogy M a N jelentése tipizálható, ha M egy funkcionális típusú, mondjuk α → β, és ha N rendelkezik típus α. Az MN-nek ekkor a β típusa van.

A B típusa (α → β) → (γ → α) → γ → β. Látható, ha megjegyzi, hogy B xyz → * x (yz), vagy az összetételi szabályt alkalmazza S ( KS ) K-ra .

A C típus (α → β → γ) → β → α → γ, ugyanazon okok miatt, mint a B esetében .

A W viszont nem tipizálható. Ezt úgy láthatjuk, hogy emlékezünk arra, hogy S  : (α → β → γ) → (α → β) → α → γ és I  : (α → α). Ha S- et alkalmazunk I- re , akkor α = β → γ-nak kell lennie, akkor ha I-re SI- t alkalmazunk, akkor α = β-nak kell lennie, tehát β = β → γ. Ennek az egyenletnek nincs megoldása. Tehát az SII = W nem tipizálható.

Összefoglalva:

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

Erős szabványosítás

Ha M tipikus kombinátor, akkor minden M-től kezdődő redukciós lánc véges. Ezt a tulajdonságot erős normalizálásnak nevezzük .

Kombinatorikus logika és a Curry-Howard megfelelés

Látható, hogy a modus ponen

P→QPQ{\ displaystyle {\ frac {P \ Q \ qquad P} {Q}}}

hasonlít a típusmegőrzési szabályra, amikor az α → β típusú kombinátort alkalmazzuk az α típusú kombinátorra. Vizsgáljuk meg a propozíciós logika Hilbert-stílusú bemutatásának első két axiómáját is , nevezetesen:

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

Emlékezzünk arra, hogy lehetővé teszik az intuitionista propozíciós számítás formalizálását. Észrevesszük, hogy az első axióma megegyezik a K típusával, és hogy a második axióma azonos az S típusával, ha a P állítást α-val, a Q állítást β-val és az R- t γ-val helyettesítjük. Ezt az állítást és a típus, valamint a kombinátor és a bizonyítás közötti megfelelést Curry-Howard megfelelésnek nevezzük. Ezzel párhuzamosan állítja az à la Hilbert levonási rendszerét az intuitionista propozíciós logika és a kombinatorikus logika számára, amelyeket meg kell jegyezni, függetlenül fedezték fel.

Egy példa

A képlet

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

azt jelenti ( például Coq nyelvén ), hogy B az (α → β) → (γ → α) → γ → β propozíciós képlet bizonyítéka (bármely eleve).

B ≡ S (KS) K

majd hatékony bizonyítékot szolgáltat Hilbert elméletének képletére, amely csak a modus ponenseket, valamint a K és S axiómákat használja .

Ez egy kis átírási munkát igényel: Először visszaállítjuk a zárójeleket

B ≡ (S (KS)) K

Ezután bemutatjuk az üzemeltető ⇒

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

végül a postfix jelölést használjuk  :

B ≡ KSK ⇒ S ⇒ ⇒

Ekkor ez a képlet adja meg a demonstráció lépéseit a dedukció irányába. ⇒ a modus ponens használatát jelöli; K és S, használata axiómák K és S. Pontosabban Q ≡ IP ⇒ jelenti, hogy ha azt a demonstrálása P → Q és P kimutatása P , akkor az IP ⇒ az, hogy a Q . Sajnos ez a képlet nem biztosítja a szubsztitúciók műveleteit, amelyeket fel kell használni az axiómák bevezetésében.

Az előtagú jelölés,

B ≡ ⇒ ⇒ S ⇒ KSK

a bizonyítás jelentését jelenti a Coq nyelvén. Itt a hiányzó információk a mod képleteiben használt P képletei .

Demonstráció

Az írás megkönnyítése érdekében megjegyezzük

• P⁰ = (P → Q)
• Q⁰ = (R → P → Q)
• R⁰ = (R → P) → (R → Q)
• Az MP ( P ) a modus ponenok használatát jelöli a P előfeltevéssel

A cél tehát az

• B = P⁰ → R⁰ .

1. MP ( P⁰ → Q⁰ ) a B gólt a 2 gólra cseréli
   • P1 → B
   • P¹ = P⁰ → Q⁰
2. MP ( P⁰ → Q⁰ → R⁰ ) a P¹ → B célt a 2 gólra cseréli
   • P² → (P¹ → B)
   • P² = P⁰ → Q⁰ → R⁰
3. S bebizonyítja, hogy P² → (P¹ → B), mert
   • P² → (P¹ → B) = (P⁰ → Q⁰ → R⁰) → (P⁰ → Q⁰) → (P⁰ → R⁰)
4. Az MP ( Q⁰ → R⁰ ) a P² gólt a 2 gólra cseréli
   • P³ → P²
   • P³ = Q⁰ → R⁰
5. K bizonyítja P³ → P², mert
   • P³ → P² = (Q⁰ → R⁰) → P⁰ → (Q⁰ → R⁰)
6. S bizonyítja P³-t, mert
   • P³ = (R → P → Q) → (R → P) → (R → Q)
7. K bizonyítja P¹-et, mert
   • 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.

Levelezés a λ-kalkulussal

A kombinatorikus logika bármely kifejezése ekvivalens λ-calculus kifejezést, és a λ-calculus bármely kifejezése ekvivalens kombinatorikus logikai kifejezést fogad el.

A kombinatorikus logikától a λ-számításig

Vegye figyelembe a kombinátorok λ-számításra való fordítását, amelyet a következő határoz meg: [[-]]λ{\ displaystyle [\! [-] \!] _ {\ lambda}}

• if változót jelöl  ,;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)} ;
• [[MNEM]]λ=[[M]]λ[[NEM]]λ{\ displaystyle [\! [M \, N] \!] _ {\ lambda} = [\! [M] \!] _ {\ lambda} \, [\! [N] \!] _ {\ lambda }}, minden kombájn és .M{\ displaystyle M}NEM{\ displaystyle N}

Absztrakció a kombinatorikus logikában

A λ-számítás reprezentációjának meghatározása előtt a kombinatorikus logikában meg kell határoznunk egy absztrakciót a kombinatorikus logikában. Ha ez egy kifejezés, akkor meghatározzuk, hogy kié lesz a szerep . M{\ displaystyle M}[x].M{\ displaystyle [x] .M}λx.M{\ displaystyle \ lambda xM}

(nál nél)[x].M=KMha x∉FV(M)(b)[x].x=én(vs.)[x].Ux=Uha x∉FV(U)(d)[x].UV=S([x].U)([x].V)ha vagy (nál nél) vagy (vs.) született alkalmaz.{\ displaystyle {\ begin {tömb} {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 {tömb} }}

A λ-számítástól a kombinatorikus logikáig

Meghatározzuk a λ-számítás fogalmainak értelmezését a kombinatorikus logika szempontjából: M{\ displaystyle M}[[M]]VSL{\ displaystyle [\! [M] \!] _ {CL}}

[[x]]VSL=x[[MNEM]]VSL=[[M]]VSL[[NEM]]VSL[[λx.M]]VSL=[x].[[M]]VSL{\ displaystyle {\ begin {tömb} {rcl} {[} \! [x] \!] _ {CL} & = & x \\ {[} \! [MN] \!] _ {CL} & = & [\! [M] \!] _ {CL} [\! [N] \!] _ {CL} \\ {[} \! [\ Lambda xM] \!] _ {CL} & = & [ x]. [\! [M] \!] _ {CL} \ end {tömb}}}

Példa

A közösítő fixpont a Turing , megjegyezte expresszálódik λ-kalkulus . Ezután kiszámíthatjuk: Θ{\ 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)=Sén([[xx]]VSL)=Sén(xx){\ displaystyle {\ begin {tömb} {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 {tömb} }}

azután

[[λx.λy.y(xxy))]]VSL=[x].[[λy.y(xxy))]]VSL=[x].Sén(xx)=S([x].Sén)([x].xx)=S(S([x].S)([x].én))(S([x].x)([x].x)=S(S(KS)(Kén))(Sénén){\ displaystyle {\ begin {tömb} {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 {tömb}}}

Ezután meghatározunk két kombinátort A és Θ

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

Θ : = AA

Θ fixpontos kombinátor.

Megfigyeljük, hogy akár a λ-tag, akár annak kombinátorként való fordítása van, megvan Θx ⟶∗ x(Θx){\ displaystyle \ Theta x ~ {\ stackrel {*} {\ longrightarrow}} ~ x (\ Theta x)}

Megoldhatatlan problémák a kombinatorikus logikában

A normál forma olyan kombinátor, amelyben a primitív kombinátorokat nem alkalmazzák annyi érvre, hogy leegyszerűsödjenek. Dönthetetlen tudni

ha egy általános kombinátornak normális formája van, ha két kombinátor egyenértékű, stb.

Ez egyenértékű a lambda-számítás megfelelő problémáinak eldönthetetlenségével .

Hivatkozások

1. Bimbó Katalin , The Stanford Encyclopedia of Philosophy , Metaphysics Research Lab, Stanford University,2016( online olvasás )
2. Moses Schönfinkel "Über die Bausteine ​​der mathematischen Logik", Mathematische Annalen 92 , p.  305-316. Francia nyelvre fordította: Geneviève Vandevelde: Moses Schönfinkel , „  A matematikai logika építőköveiről  ”, Matematika és humán tudományok , vol.  112,1990, P.  5–26 ( online olvasás ) és angol nyelvre fordította: Moses Schönfinkel ( ford.  Stefan Bauer-Mengelberg) „A matematikai logika építőköveiről” , Jean van Heijenoort , Forráskönyv a matematikai logikában, 1879-1931 , Harvard Univ. Nyomja meg,1967( online olvasható ) , 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 , online olvasás , hozzáférés: 2017. október 11. )
4. H. Curry, JR Hindley etJ. P. Seldin, kombinációs logika II . Észak-Hollandia, 1972.
5. Pontosabban a kombinátor.
6. Bár a szuper-kombinátorokon alapuló logikát használó számítógép kevésbé beszédes, mint az S és K alapú kombinációs logika .
7. Ez a konvenció meglehetősen szerencsétlen, mert a kombinátor típusának írásakor a jobb oldali asszociativitást veszik figyelembe .
8. itt megjelenő x nem változó a kombinatorikus logika nyelvén, mert, mint mondtuk, a változó logika változók nélkül; valójában x egy „metaváltozó”, amely lehetővé teszi a kombinatorikus logika azonosságainak bemutatását.
9. Harvey Friedman teljességi tétele .
10. Vagyis a hipotézisektől (itt axiómák) haladunk az elérendő célig.
11. Vagyis az alkalmazott taktikák sorrendje. A Coq a cél módosításával halad, amíg hipotézisekkel, tételekkel vagy axiómákkal azonosítja.
12. J. Roger Hindley és Jonathan P. Seldin, Lambda-Calculu és Combinators bevezetés , Cambrdige University Press,2008( online olvasás )2C. Szakasz o. 26.

Bibliográfia

• Haskell Curry és Robert Feys , I. kombinációs logika . Észak-Holland 1958. E munka tartalmának nagy részét az 1972-es és az azt követő munka elavította.
• H. Curry, JR Hindley és JP Seldin, kombinációs logika II . North-Holland, 1972. A kombinatorikus logika teljes visszatekintése, ideértve a kronológiai megközelítést is.
• J. Roger Hindley és Jonathan P. Seldin , Lambda-Calculu and Combinators an Introduction , Cambrdige University Press,2008( online olvasás )
• J.-P. Desclés & ali, Kombinatorikus logika és Lambda-számítás - operátorlogika - 2016 - Cépaduès * J.-P. Desclés & ali, Jelentés Operátorlogika szerinti számítások - 2016 - Cépaduès
• Jean-Pierre Ginisti , kombinatorikus logika , Párizs, PUF (coll. “Que sais-je?” N ° 3205), 1997, 127 p.
• M. Shönfinkel, In: J. van Heijenoort, szerkesztő, Ország Frege Gödel , Harvard University Press, Cambridge, MA (1967), pp. 355–366 1924.
• J.-L. Krivine, Lambda-calcul, típusok és modellek , Masson, 1990, fejezet. Kombinatorikus logika , angol fordítás elérhető a szerző webhelyén [1] .
• Robert Feys , A kombinatorikus logika technikája In: Revue Philosophique de Louvain. Harmadik sorozat, 44. kötet, 1. szám, 1946. pp. 74–103 [2]
• (en) Henk Barendregt , The Lambda-Calculus , 103. kötet, Elsevier Science Publishing Company, Amszterdam, 1984.

Külső linkek

• Hatósági nyilvántartások  :
  • Francia Nemzeti Könyvtár ( adatok )
  • Egyetemi dokumentációs rendszer
  • Kongresszusi Könyvtár
  • Gemeinsame Normdatei