Kombinatorikus logika

A kombinatorikus logika a matematikai logika egyik ága , amely a formális logikai rendszerek vagy kalkulusok alapvető (vagyis magyarázatot nem igénylő és nem elemzett) fogalmaival és módszereivel foglalkozik [1] [2] . A diszkrét matematikában a kombinatorikus logika szorosan kapcsolódik a lambda-számításhoz , mivel számítási folyamatokat ír le.

Megalakulásuk óta a kombinatorikus logika és a lambda -számítás a nem klasszikus logikák közé tartozik . A lényeg az, hogy a kombinatorikus logika az 1920-as években, a lambda-számítás pedig az 1940-es években jelent meg, mint a metamatematika egy olyan ága, amelynek egy meglehetősen jól körülhatárolt célja - a matematika alapjainak megadása. Ez azt jelenti, hogy a szükséges „alkalmazott” matematikai elmélet – a szubjektumelmélet – megalkotása után, amely a valós külső környezetben zajló folyamatokat vagy jelenségeket tükrözi, a „tiszta” metaelmélet héjként használható a tantárgyelmélet lehetőségeinek és tulajdonságainak tisztázására. . Hamarosan az is kiderült, hogy mindkét rendszer programozási nyelvnek tekinthető (lásd még a kombinatorikus programozást ).

A mai napig mindkét nyelv nemcsak a számítástechnika területén végzett kutatások teljes tömegének alapjává vált , hanem a programozáselméletben is széles körben használják. A számítógépek számítási teljesítményének növekedése az elméleti (logikai és matematikai) ismeretek jelentős részének automatizálásához vezetett, és a kombinatorikus logikát a lambda-számítással együtt a tárgyi érvelés alapjaként ismerik el. .

Alapfogalmak

A kombinatív logikában az alapfogalmak az egyhelyes függvény és a függvény argumentumra való alkalmazásának művelete ( alkalmazás ). A függvény fogalmát elsődlegesnek tekintjük a halmaz fogalmával kapcsolatban . A függvényt általánosan értjük, és az argumentumokkal és értékekkel azonos szintű objektumokkal is működhet. Mivel egy függvény argumentuma lehet függvény is, a sokhelyes függvény egyhelyes függvényre redukálható [3] .

A kombinátor olyan függvény , amely kielégíti az egyenlőséget $f$

fg_{1}g_{2}\dots g_{n}=(\dots ((fg_{1})g_{2})\dots g_{n})=X,

ahol ( ) néhány függvény, X egy olyan objektum, amelyet függvényekből állítottunk össze a [3] alkalmazás segítségével . $g_1, g_2, \pontok, g_n$ $n\geqslant 1$

Bármely kombinátor kifejezhető két S és K kombinátorral, amelyeket a következő egyenlőségek határoznak meg [3] :

Sxyz=xz(yz)

( forgalmazó ),

kxy=x

( csatár ).

Ha adott egy lambda-kifejezés, mindig létrehozhat egy alkalmazó kifejezést . Ehhez csak két kombinátorra van szükség: S és K . Lambda kifejezések formájában: , . Vagyis az ezeken a kombinatorikus objektumokon definiált kombinatorikus logika a lambda-számítás modelljének tekinthető [4] . $K = \lambda x.\lambda yx$ $S=\lambda f.\lambda g.\lambda x.fx(gx)$

További példák a kombinátorokra (a lambda-számítás jelölésében) az azonosságfüggvény , amely könnyen kifejezhető S és K kifejezésekkel [4] :

I = \lambda xx = SKK

és a fixpontos vagy Y-kombinátor :

Y=\lambda h.((\lambda xh(xx))(\lambda xh(xx))).

Történelem

1920-ban a kombinátorokat mint speciális matematikai entitásokat [5] eredetileg M. Sheinfinkel [6] vezette be . Néhány évvel később önállóan fedezte fel őket H. Curry [7] , aki azóta jelentős előrelépést tett a kombinatorikus logika terén (bár más kutatók, például Rosser is hozzájárultak ehhez a munkához különböző időpontokban). Csaknem egy időben Church , Rosser és Kleene megkezdte a λ-konverzió fejlesztését.

Az 1970-es évek óta a kombinátorokat három fő módon használták: egyrészt logikai rendszerek felépítésére , amelyek egy művelet absztrakt jelölésén alapulnak; másodszor a bizonyítások elméletében, mint a különféle típusú konstruktív függvények rögzítésének alapja; harmadszor, egyes programozási nyelvek felépítésében és elemzésében a számítástechnikában .

Kategorikus kombinatorikus logika

A kombinatorikus logika keretein belül megépül a számításelmélet egy speciális változata, az úgynevezett kategorikus absztrakt gép . Ehhez a kombinatorikus logika egy speciális töredékét veszik figyelembe - a kategorikus kombinatorikus logikát [8] . Kombinátorok halmaza képviseli, amelyek mindegyike önálló értékkel rendelkezik, mint egy programozási rendszer utasítása. Így a kombinatorikus logikába még egy hasznos alkalmazás épül be – egy descartes-i zárt kategórián (fc) alapuló programozási rendszer. Ez lehetővé teszi az operátor és az applikatív programozási stílus közötti kapcsolat újragondolását egy új szinten.

Illatív kombinatorikus logika

Az objektumok mint bizonyos helyettesítési tulajdonságokkal rendelkező absztrakt matematikai entitások fogalmát felhasználva logikai gondolkodási rendszereket lehet felépíteni . Az ilyen rendszerek közül a leghíresebb a kombinátorokon alapul.

A kombinátorokon alapuló logika vagy az illatív kombinatorikus logika a kombinátorok elméletéből vagy a lambda-számításból épül fel, kiegészítve további állandókkal - extra állandókkal -, valamint a megfelelő axiómákkal és következtetési szabályokkal, amelyek a deduktív következtetés eszközét biztosítják.

Lásd még

Jegyzetek

↑ Szerk. F. V. Konstantinova. Kombinatorikus logika // Filozófiai Enciklopédia: 5 kötetben . - M . : Szovjet Enciklopédia, 1960-1970.
↑ Kondakov, 1971 .
↑ 1 2 3 MES, 1988 , p. 275-276.
↑ 1 2 Field, Harrison, 1993 , p. 291-293.
↑ Cardone F., Hindley J. R. History of lambda calculus and kombinators ( Archiválva : 2011. október 10., a Wayback Machine ), in Handbook of the History of Logic, 5. kötet, DM Gabbay és J. Woods (szerk.) (Amsterdam: Elsevier Co.) ., megjelenni).
↑ Schonfinkel M. Uber die Baustein der mathematischen Logik. — Matek. Annalen, vol. 92, 1924, p. 305-316.
↑ Curry H. B. Grundlagen der kombinatorischen Logik. American Journal of Mathematics, 52:509-536, 789-834, 1930.
↑ Curien P.-L. Kategorikus kombinatív logika. – LNCS, 194, 1985, p. 139-151.

Irodalom

Wolfenhagen VE Kombinatorikus logika a programozásban. Számítások objektumokkal példákban és feladatokban. - 2. kiadás - M . : AO Center YurInfoR, 2003. - 204 p. — ISBN 5-89158-101-9 .
Kondakov N. I. Logikai szótár / Gorsky D. P. - M . : Nauka, 1971. - 656 p.
Field A., Harrison P. Funkcionális programozás = Funkcionális programozás. — M .: Mir, 1993. — 637 p. — ISBN 5-03-001870-0 .
Matematikai enciklopédikus szótár / Yu. V. Prokhorov. - M . : Szovjet Enciklopédia, 1988. - 847 p.
A. S. Kuzicsev. Kombinatorikus logika // Új Filozófiai Enciklopédia : 4 kötetben / előz. tudományos-szerk. V. S. Stepin tanácsa . — 2. kiadás, javítva. és további - M . : Gondolat , 2010. - 2816 p.

Szótárak és enciklopédiák	Nagy orosz
Bibliográfiai katalógusokban	BNF : 119473722 GND : 4164750-6 J9U : 987007543265905171 LCCN : sh85028814 SUDOC : 027430677