Kombinatorna logika je notacija koju su uveli Moses Schönfinkel i Haskell Curry kako bi eliminirali potrebu za varijablama u matematičkoj logici. U zadnje se vrijeme koristi u računarstvu kao teoretski model računanja te također kao baza za funkcijske programske jezike. Zasnovan je na kombinatorima, koji su funkcije višeg reda i koji koriste samo primjenu (aplikaciju) funkcije i možda druge, ranije definirane kombinatore za definiranje rezultata svojih argumenata.
Kombinatorna logika u matematici
Kombinatorna je logika izvorno zamišljena kao 'pred-logika' koja bi osvijetlila uporabu kvantificiranih varijabli u logici, eliminirajući ih. Drugi način eliminacije kvantificiranih varijabli su predikatni funktori koje je osmislio Willard Van Orman Quine. Iako većina sustava kombinatorne logike nadilazi ekspresivnu moć logike prvog reda, Quineovi predikatni funktori su u ekspresivnoj moći istovjetni logici prvog reda.
Izvorni stvoritelj kombinatorne logike, Schönfinkel, nije ništa objavio o kombinatornoj logici nakon izvornog rada iz 1924., te općenito prestao publicirati nakon što je Staljin konsolidirao svoju moć 1929. Curry je ponovno otkrio kombinatore dok je bio doktorski student na Sveučilištu u Göttingenu kasnih 1920-ih, ali taj se legendarni odsjek raspao kad je Hitler došao na vlast 1933. Kasnih 1930-ih su Alonzo Church i njegovi studenti na Princetonu otkrili rivalni formalizam za funkcijsku apstrakciju, lambda račun, koji se pokazao popularnijim od kombinatorne logike. Rezultat ovog povijesnog spleta okolnosti jest da, sve dok se teoretsko računarstvo počelo zanimati za kombinatornu logiku 1960-ih i 70-ih, sav rad na tu temu su odradili Haskell Curry i njegovi studenti, te belgijanac Robert Feys. Vidi Curry i Feys (1958.), te Curry et al. (1972.) za pregled rane povijesti kombinatorne logike. Za suvremeniji paralelni tretman kombinatorne logike i lambda računa, vidi Barendregt (1984.), koji također daje pregled modela koje je Dana Scott izveo za kombinatornu logiku 1960-ih i 70-ih.
Kombinatorna logika u računarstvu
U računarstvu, kombinatorna se logika koristi kao pojednostavljeni model računanja, korišten u teoriji izračunljivosti i teoriji dokaza. Unatoč svojoj jednostavnosti, kombinatorna logika obuhvaća mnoga esencijalna svojstva računanja.
Kombinatorna se logika može shvatiti kao varijanta lambda računa, u kojoj su lambda izrazi (koji predstavljaju funkcijsku apstrakciju) zamijenjeni skupom kombinatora, primitivnih funkcija koji nemaju slobodnih varijabli. Lako je transformirati lambda izraz u kombinatorni izraz, i kombinatorna je redukcija mnogo jednostavnija od lambda redukcije. Stoga je kombinatorna logika korištena za modeliranje nekih nestriktnih funkcijskih programskih jezika i sklopovlja. Najčišći oblik ovoga pogleda jest programski jezik Unlambda, čiji su jedini primitivi S i K kombinatori i znakovni I/O. Iako nije praktičan programski jezik, Unlambda ima teoretsku važnost.
Kombinatornoj logici može biti pridjeljeno mnogo interpretacija. Mnogi raniji radovi Curryja su pokazali kako prevesti skup aksioma konvencionalne logike u jednadžbe kombinatorne logike (Hindley i Meredith 1990). Dana Scott je 1960-ih i 70-ih pokazao kako usuglasiti teoriju modela i kombinatornu logiku.
Sažetak lambda računa
Lambda račun se bavi objektima zvanim lambda termini koji su stringovi simbola jednog od sljedećih oblika:
v λv.E1 (E1 E2)
pri čemu je v ime varijable izvučeno iz predefiniranog beskonačnog skupa imena varijabli, a E1 i E2 su lambda termini. Termini oblika λv.E1 se zovu apstrakcije. Varijabla v je zvana formalni parametar apstrakcije, i E1 je tijelo apstrakcije.
Termini λv.E1 predstavljaju funkciju koja, primijenjena na argument, veže formalni parametar v na argument i potom izračunava rezultirajuću vrijednost od E1 - to jest, vraća E1, sa svakim pojavljivanjem v zamijenjenim argumentom.
Termini oblika (E1 E2) su zvane aplikacije. Aplikacije modeliraju invokaciju funkcije ili izvršavanje: funkcija predstavljena s E1 se invocira, s E2 kao argumentom, i rezultat se izračunava. Ako je E1 (ponekad nazvan aplikandom) apstrakcija, termin može biti reduciran: E2, argument, može biti supstituiran tijelom od E1 mjesto formalnog parametra od E1, te je rezultat novi lambda termin koji je ekvivalentan starome. Ako lambda termin ne sadrži podtermine oblika (λv.E1 E2), tada ne može biti reduciran, i kaže se da je u normalnom obliku.
Izraz E[v := a] predstavlja rezultat uzimanja termina E i zamjene svih slobodnih pojavljivanja od v s a. Stoga se piše:
(λv.E a) => E[v := a]
Po konvenciji, uzima se (a b c d ... z) kao kraći zapis za (...(((a b) c) d) ... z). (tj., aplikcija je asocijativna ulijevo.)
Motivacija za ovu definiciju redukcije jest ta da obuhvaća esencijalno ponašanje svih matematičkih funkcija. Primjerice, neka se razmatra funkcija koja izračunava kvadrat broja. Može se zapisati:
Kvadrat od x jest x*x
(Rabeći "*" za označavanje množenja.) x je ovdje formalni parametar funkcije. Evaluacijom kvadrata za pojedini argument, primjerice 3, on se umeće u definiciju na mjesto formalnog parametra:
Kvadrat od 3 jest 3*3
Da bi se evaluirao rezultirajući izraz 3*3, valja posegnuti za znanjem množenja i brojem 3. S obzirom na to da je bilo koje računanje jednostavno kompozicija evalucije pogodnih funkcija nad pogodnim primitivnim argumentima, ovaj je jednostavni princip supstitucije dovoljan da obuhvati esencijalni mehanizam računanja. Štoviše, u lambda računu, notacije se kao što su '3' i '*' mogu predstaviti bez potrebe za vanjski definiranim primitivnim operatorima ili konstantama. Moguće je identificirati termine u lambda računu koji se, prilikom odgovarajuće interpretacije, ponašaju kao broj 3 i kao operator množenja.
Poznato je da je lambda račun računski istovjetan po svojoj moći mnogim drugim mogućim modelima računanja (uključujući Turingove strojeve); to jest, bilo koje računanje koje može biti ostvareno u ovim drugim modelima se može izraziti u lambda računu, kao i obratno. Prema Church-Turingovoj tezi, oba modela mogu izraziti bilo koje računanje.
Možda je iznenađujuće da lambda račun može predstaviti bilo koje smislivo računanje rabeći jednostavne notacije funkcijske apstrakcije i aplikacije zasnovane na jednostavnim tekstualnim susptitucijama termina varijablama. Još je fascinantnija činjenica da apstrakcije nije ni nužna za takvo nešto - kombinatorna logika je model računanja istovjetan lambda računu, ali bez apstrakcije.
Kombinatorni računi
S obzirom na to da je apstrakcija jedini način za izgradnju funkcija u lambda računu, nešto je mora zamijeniti u kombinatornoj logici. Umjesto apstrakcije, kombinatorni račun pruža ograničen skup primitivnih funkcija iz kojih se mogu izgraditi ostale funkcije.
Kombinatorni termini
Kombinatorni termin je jednog od sljedećih oblika: v P (E1 E2) pri čemu je v varijabla, P jedna od primitivnih funkcija, a E1 i E2 kombinatorni termini. Same primitivne funkcije su kombinatori, odnosno funkcije koje ne sadrže slobodne varijable.
Primjeri kombinatora
Najjednostavniji primjer kombinatora jest I, kombinator identiteta, koji je definiran kao
(I x) = x
za sve termine x. Drugi jednostavni kombinator jest K, koji proizvodi konstantne funkcije: (K x) je funkcija koja, za bilo koji argument, vraća x, tako da vrijedi
((K x) y) = x
za sve termine x i y. Ili, slijedeći istu konvenciju za višestruku aplikaciju kao u lambda računu,
(K x y) = x
Treći je kombinator S, koje je poopćena verzija aplikacije:
(S x y z) = (x z (y z))
S aplicira x na y nakon što prvotno supstituira z u svakom od njih. Drugim riječina, x je primijenjen na y unutar okoliša z.
Ako su dani S i K, I je nepotreban, s obzirom na to da može biti izgrađen iz druga dva:
((S K K) x) = (S K K x) = (K x (K x)) = x
za svaki termin x. Valja uočiti da iako vrijedi ((S K K) x) = (I x) za svaki x, (S K K) nije jednako I. Kaže se da su termini ekstenzionalno jednaki. Ekstenzionalna jednakost obuhvaća matematičku notaciju jednakosti funkcija: dvije su funkcije jednake ako daju isti rezultat za iste argumente. Kao suprotnost, sami termini obuhvaćaju notaciju intenzionalne jednakosti funkcija: dvije su funkcije 'jednake' samo ako imaju identične implementacije. Mnogo je načina za implementirati funkciju identiteta; (S K K) i I među ostalima. U ovom će se članku riječ ekvivalentan rabiti u smislu ekstenzionalne jednakosti, dok će se riječ jednak rabiti za identične kombinatorne termine.
Zanimljiviji kombinator jest kombinator fiksne točke ili Y kombinator, koji se može koristiti za implementaciju rekurzije.
Potpunost S-K baze
Možda je zapanjujuća činjenica da S i K mogu biti komponirani za stvaranje kombinatora koji su ekstenzionalno jednaki bilo kojem lambda terminu, i stoga, po Churchovoj tezi, bilo kojoj izračunljivoj funkciji uopće. Dokaz se sastoji od uvođenja transformacije, T[ ], koja vrši konverziju proizvoljnog lambda termina u ekvivalentni kombinator.
T[ ] se može definirati na sljedeći način:
T[V] => V T[(E1 E2)] => (T[E1] T[E2]) T[λx.E] => (K T[E]) (ako x nije slobodan u E) T[λx.x] => I T[λx.λy.E] => T[λx.T[λy.E]] (ako je x slobodan u E) T[λx.(E1 E2)] => (S T[λx.E1] T[λx.E2]) Ovaj je proces također poznat kao eliminacija apstrakcije.
Konverzija lambda termina u ekvivalentan kombinatorni termin
Na primjer, lambda termin λx.λy.(y x) će se konvertirati u sljedeći kombinator:
T[λx.λy.(y x)] = T[λx.T[λy.(y x)]] (po pravilu 5) = T[λx.(S T[λy.y] T[λy.x])] (po pravilu 6) = T[λx.(S I T[λy.x])] (po pravilu 4) = T[λx.(S I (K x))] (po pravilima 3 i 1) = (S T[λx.(S I)] T[λx.(K x)]) (po pravilu 6) = (S (K (S I)) T[λx.(K x)]) (po pravilu 3) = (S (K (S I)) (S T[λx.K] T[λx.x])) (po pravilu 6) = (S (K (S I)) (S (K K) T[λx.x])) (po pravilu 3) = (S (K (S I)) (S (K K) I)) (po pravilu 4)
Ako pprimijenimo ovaj kombinator na bilo koja dva termina x i y, reducirat će se kao što slijedi:
(S (K (S I)) (S (K K) I) x y) = (K (S I) x (S (K K) I x) y) = (S I (S (K K) I x) y) = (I y (S (K K) I x y)) = (y (S (K K) I x y)) = (y (K K x (I x) y)) = (y (K (I x) y)) = (y (I x)) = (y x)
Kombinatorno je predstavljanje (S (K (S I)) (S (K K) I)) mnogo dulje od predstavljanja preko lambda termina λx.λy.(y x). Ovo je tipično ponašanje. Općenito, T[ ] konstrukcija može proširiti lambda termin duljine n u kombinatorni termin duljine Θ(3n).
Objašnjenje T[ ] transformacije
T[ ] transformacija je motivirana željom za eliminacijom apstrakcije. Dva specijalna slučaja, pravila 3 i 4, su trivijalna: λx.x je očito ekvivalentno I, i λx.E je očito ekvivalentno (K E) ako se x ne pojavljuje slobodan u E.
Prva su dva pravila također jednostavna: Varijable se konvertiraju u same sebe, a aplikacije, koje su dozvoljene u kombinatornim terminima, su konvertirane u kombinatore jednostavnom konverzijom aplikanda i argumenta u kombinatore.
Pravila 5 i 6 su nešto zanimljivija. Pravilo 5 jednostvno kaže da se u svrhu konverzije složene apstrakcije u kombinator mora prvo konvertirati njeno tijelo u kombinator, a potom eliminirati apstrakciju. Pravilo 6 ustvari eliminira apstrakciju.
λx.(E1 E2) je funkcija koja prima argument, npr. a, i supstituira ga u lambda termin (E1 E2) na mjestu x, pri čemu daje (E1 E2)[x : = a]. Ali supstitucija a u (E1 E2) mjesto x je isto što i supstitucija u oba E1 i E2 te je stoga
(E1 E2)[x := a] = (E1[x := a] E2[x := a])
(λx.(E1 E2) a) = ((λx.E1 a) (λx.E2 a)) = (S λx.E1 λx.E2 a) = ((S λx.E1 λx.E2) a)
Po ekstenzionalnoj jednakosti,
λx.(E1 E2) = (S λx.E1 λx.E2)
Stoga, da bi se pronašao kombinator ekvivalentan s λx.(E1 E2), dovoljno je pronaći kombinator ekvivalentan sa (S λx.E1 λx.E2), i
(S T[λx.E1] T[λx.E2])
očito odgovara. Svaki od E1 i E2 očito sadrži strogo manje apstrakcija od (E1 E2), te stoga rekurzija mora terminirati u lambda terminu koji uopće ne sadrži aplikacije—ili varijablu, ili termin oblika λx.E.
Pojednostavljenja transformacije η-redukcija