A kombinátor logika a matematikai logika egy olyan jelölésrendszere, amelyet arra terveztek, hogy kiküszöbölje a kvantifikált változók szükségességét. A rendszert először Moses Schönfinkel vezette be 1920-ban, majd később Haskell Curry fejlesztette tovább.
A matematika területén a kombinációs logikát leggyakrabban a számítástudomány elméleti alapjainak vizsgálatára használják, különösen a Kiszámíthatóság-elméletben és a bizonyításelméletben. Szoros kapcsolatban áll a Lambda-kalkulussal; mindkettő a formális logika és a programozási nyelvek (különösen a funkcionális programozás) alapvető modelljének tekinthető.
A kombinátor logika kombinátorokon alapul. A kombinátor egy olyan magasabb rendű függvény, amely kizárólag a függvényalkalmazás (applikáció) és más, korábban definiált kombinátorok segítségével határozza meg az eredményét. Fontos tulajdonsága, hogy nem tartalmaz szabad változókat. A kombinátorok segítségével bármilyen számítható függvény leírható anélkül, hogy változókat kellene elneveznünk vagy kötnünk.
Matematikai háttér A kombinátor logika a lambda-kalkulus egyik változataként is felfogható, ahol a lambda-kifejezések (absztrakciók) helyett véges számú primitív kombinátort használunk. Ezek segítségével bármilyen lambda-kifejezés átírható változómentes alakra.
Míg a lambda-kalkulusban egy kifejezés így nézhet ki:
Addig a kombinátor logika ugyanez leírható például a következő kombinátorokkal:
A kombinátor logika alapvető művelete az applikáció (függvényalkalmazás). Ha és két kifejezés, akkor jelöli azt a műveletet, amikor az függvényt alkalmazzuk a argumentumra. A zárójelezés konvenciója szerint a művelet balra asszociatív, azaz jelentése .
A kombinátorok definíciója A legegyszerűbb és legismertebb rendszer az úgynevezett SKI-kombinátorkalkulus. Ez három alapvető kombinátorra épül:
Primitív kombinátorok Az alábbiakban a kombinátorok redukciós (kiértékelési) szabályai láthatók:
Az I (Identitás) kombinátor Visszaadja a kapott argumentumot változtatás nélkül.
A K (Konstans) kombinátor Két argumentumot vár; az elsőt visszaadja, a másodikat eldobja (figyelmen kívül hagyja). Ez felel meg a konstans függvény létrehozásának.
Az S (Helyettesítő / Elosztó) kombinátor Három argumentumot vár, és a harmadikat alkalmazza az első kettőre, majd az eredményeket applikálja egymásra.
Az S-K bázis teljessége Köztudottan az S és K kombinátorok önmagukban elegendőek bármilyen számítható függvény leírására (Turing-teljes rendszert alkotnak). Még az I kombinátor is felesleges, mivel kifejezhető a másik kettővel:
Tehát .
A rendszer teljessége azt jelenti, hogy bármely lambda-kalkulusbeli kifejezéshez (amely nem tartalmaz szabad változót) létezik vele ekvivalens kombinátor-logikai kifejezés. Ezt a transzformációt "zárójelezési absztrakciónak" vagy -transzformációnak nevezzük.
Kapcsolat a logikával A Curry–Howard-izomorfizmus értelmében a logikai formulák és a számítógépes programok között mély szerkezeti hasonlóság van. A kombinátor logika a kombinátorok megfeleltethetők a Hilbert-féle axiómarendszer implikációs logikájának.
Az I kombinátor megfelel a axiómának (identitás). A K kombinátor megfelel a axiómának (gyengítés). Az S kombinátor megfelel a axiómának (elosztás).
Emiatt a típusos kombinátor logika használható matematikai bizonyítások automatikus ellenőrzésére is.
Fixpont-kombinátorok A rekurzió megvalósításához a kombinátor logikában úgynevezett fixpont-kombinátorokra van szükség. A legismertebb ilyen az Y kombinátor, amelyet Haskell Curry fedezett fel:
De léteznek egyszerűbb, kifejezetten a kombinátorokra tervezett fixpont-képzők is, mint például a Turing-féle fixpont kombinátor.
Számítástudományi alkalmazások A kombinátor logika alapvető fontosságú a fordítóprogramok tervezésében, különösen a funkcionális nyelvek (például a Haskell vagy a Clean) esetében.
Változómentesítés A fordító a programkódot kombinátorokra bonthatja, így a futtatókörnyezetnek nem kell bonyolult névtereket és változókötéseket kezelnie. Gráf-redukció A kombinátoros kifejezések kiértékelése hatékonyan megvalósítható gráf-redukcióval, ami lehetővé teszi a lusta kiértékelés (lazy evaluation) technikai megvalósítását. Párhuzamosítás Mivel a kombinátoroknak nincsenek mellékhatásaik (side effects) és nem függnek globális változóktól, a részkifejezések kiértékelése könnyen párhuzamosítható.
Lásd még
Lambda-kalkulus Funkcionális programozás Haskell Brooks Curry Neumann János Formális nyelv
Jegyzetek
Források
Kategória:Matematikai logika