Kombinatorna logika

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

Podrobniji članak o temi: lambda račun

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 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 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 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 Θ(3ⁿ).

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 sa λ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

Kombinatori generirani T[ ] transformacijom se mogu učiniti manjima ako uzmemo u obzir pravilo η-redukcije:

       T[λx.(E x)] = T[E]   (ako x nije slobodan u E)

''λx''.(''E'' x) je funkcija koja prima argument, x, i aplicira funkciju E na nj - ovo je ekstenzionalno jednako samoj funkciji E. Stoga je dovoljno konvertirati E u kombinatorni oblik.

Uzimajući u obzir ovo pojednostavljenje, gornji primjer postaje:

         T[λx.λy.(y x)] 
       = ...
       = (S (K (S I))   T[λx.(K x)])

       = (S (K (S I))   K)                 (po η-redukciji)

Kombinator je ekvivalentan prethodnom, duljem:

         (S (K (S I))   K x y)
       = (K (S I) x (K x) y)
       = (S I (K x) y)
       = (I y (K x y))
       = (y (K x y))
       = (y x)

Slično, izvorna inačica T[] transformacije je transformirala funkciju identiteta λf.λx.(f x) u (S (S (K S) (S (K K) I)) (K I)). Pravilom η-redukcije, λf.λx.(f x) je transformirana u I.

Baza jedne točke

Postoje baze s jednom točkom iz koje može biti komponiran bilo koji kombinator koji je ekstenzionalno jednak bilo kojem lambda terminu. Najjednostavniji primjer takve baze jest {X} pri čemu je:

       X ≡ λx.((xS)K)

Nije teško provjeriti da je:

       X (X (X X)) =^ηß K and
       X (X (X (X X)))) =^ηß S.

S obzirom da je {K, S} baza, slijedi da je {X} također baza.

Kombinatori B, C

Kao dodatak S i K, Schönfinkelov papir uključuje dva kombinatora koja su danas nazvana B i C, sa sljedećim redukcijama:

       (C a b c) = (a c b)
       (B a b c) = (a (b c))

Također objašnjava kako se oni mogu iskazati rabeći samo S i K.

Ovi su kombinatori izuzetno korisni prilikom prevođenja predikatne logike ili lambda računa u kombinatorne izraze. Rabio ih je i Curry, a mnogo kasnije i David Turner, čije se ime povezuje s računskom uporabom. Rabeći ih, možemo proširiti transformacijska pravila kao što slijedi:

T[V] => V
T[(E1 E2)] => (T[E1] T[E2])
T[λx.E] => (K T[E]) (ako x nije slobodan uis not free in 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]) (ako je x slobodan i u E1 i u E2)
T[λx.(E1 E2)] => (C T[λx.E1] T[E2]) (ako je x slobodan u E1 ali ne i u E2)
T[λx.(E1 E2)] => (B T[E1] T[λx.E2]) (ako je x slobodan u E2 ali ne i u E1)

Rabeći B i C kombinatore, transformacija od λx.λy.(y x) izgleda ovako:

         T[λx.λy.(y x)] 
       = T[λx.T[λy.(y x)]]
       = T[λx.(C T[λy.y] x)]     (pravilom 7)
       = T[λx.(C I x)]
       = (C I)                   (η-redukcija)
       = C_*(tradicionalna kanonska notacija: X_* = X I)
       = I'(tradicionalna kanonska notacija: X' = C X)

I zaista, (C I x y) se reducira u (y x):

         (C I x y)
       = (I y x)
       = (y x)

Motivacija je u ovom slučaju ta da su B i C ograničene verzije od S. Dok S prima vrijednost i spustituira je i u aplikandu i argumentu prije obavljanja aplikacije, C obavlja supstituciju samo u aplikandu, a B samo u argumentu.

Današnja je imena kombinatorima dao Haskell Curry u svojoj doktorskoj disertaciji iz 1930. (vidi B,C,K,W Sustav). U izvornom papiru Schönfinkela, ono što danas zovemo S, K, I, B i C je bilo zvano S, C, I, Z, i T, redoslijedom.

CL_K nasuprot CL_I računu

Valja vršiti razlikovanje između CL_K opisanog u ovom članku i CL_I računa. Distinkcija odgovara onoj između λ_K i λ_I računa. Za razliku od λ_K računa, λ_I ograničava apstrakcije na:

λv.E1 pri čemu v ima najmanje jedno slobodno pojavljivanje u E1.

Shodno tome, kombinator K nije prisutan ni u λ_I računu niti u CL_I računu. Konstante od CL_I su: I, B, C i S, i one su te koje oblikuju bazu za koju svi CL_I termini mogu biti komponirani (modulo jednakost). Zajedno, B i C simuliraju K. Svaki λ_I termin se može konvertirati u jednak CL_I kombinator prema pravilima sličnima onim predstavljenim gore za konverziju λ_K termina u CL_K kombinatore. Vidjeti poglavlje 9 u Barendregt (1984).

Obrnuta konverzija

Konverzija L[ ] iz kombinatornih termina u lambda termine je trivijalna:

       L[I]       = λx.x
       L[K]       = λx.λy.x
       L[C]       = λx.λy.λz.(x z y)
       L[B]       = λx.λy.λz.(x (y z))
       L[S]       = λx.λy.λz.(x z (y z))
       L[(E1 E2)] = (L[E1] L[E2])

Valja uočiti, međutim, da ova transformacija nije inverzna transformacija bilo koje od već viđenih inačica od T[ ].

Neodlučivost kombinatornog računa

Neodlučivo je ima li općeniti kombinatorni termin normalni oblik, jesu li dva kombinatorna termina ekvivalentna, itd. Ovo je istovjetno neodlučivosti odgovarajućih problema za lambda termine. Međutim, izravan dokaz slijedi:

Prvo, valja uočiti da termin

       Ω = (S I I (S I I))

nema normalni oblik, s obzirom da reducira na sam sebe nakon tri koraka, kao što slijedi:

         (S I I (S I I))
       = (I (S I I) (I (S I I)))
       = (S I I (I (S I I)))
       = (S I I (S I I))

i očito je da nijedna druga redukcija ne može više skratiti izraz.

Sada, neka se pretpostavi da je N kombinator za detekciju normalnih oblika, takav da

       (N x) => T, ako x ima normalni oblik
                F, inače.

(Pri čemu su T i F transformacije konvencionalnih definicija istine i laži u lambda računu, λx.λy.x i λx.λy.y. Kombinatorne su verzije T = K i F = (K I).)

Sada, neka je

       Z = (C (C (B N (S I I)) Ω) I)

i neka se promatra termin (S I I Z). Ima li (S I I Z) normalni oblik? Ima ako i samo ako imaju i sljedeći:

         (S I I Z)
       = (I Z (I Z))
       = (Z (I Z))
       = (Z Z) 
       = (C (C (B N (S I I)) Ω) I Z)           (definicija od Z)
       = (C (B N (S I I)) Ω Z I)
       = (B N (S I I) Z Ω I)
       = (N (S I I Z) Ω I)

Sada valja aplicirati N na (S I I Z). Ili (S I I Z) ima normalni oblik, ili nema. Ako ima normalni oblik, tada se nastavljanjem reducira kao što slijedi:

         (N (S I I Z) Ω I)
       = (K Ω I)                               (definicija od N)
       = Ω

ali Ω nema normalni oblik, iz čega slijedi protuslovlje. Ali ako (S I I Z) nema normalni oblik, tada se nastavljanjem reducira kao što slijedi:

         (N (S I I Z) Ω I)
       = (K I Ω I)                             (definicija od N)
       = (I I)
         I

što znači da je normalni oblik od (S I I Z) jednostavno I, što je još jedno protuslovlje. Stoga hipotetski kombinator normalnog oblika N ne postoji.

Kombinatorni analogon Riceovog teorema kaže da ne postoji potpun netrivijalni predikat. Predikat je takav kombinator koji, kad apliciran, vraća ili T ili F (engl. true, false - istina, laž). Predikat je N netrivijalan ako postoje dva argumenta A i B takva da je NA=T i NB=F. Kombinator N je potpun ako i samo ako NM ima normalni oblik za svaki argument M. Analogon Riceovog teorema tad kaže da je svaki potpuni predikat trivijalan.

Primjene

Kompilacija funkcijskih jezika

Funkcijski programski jezici su često zasnovani na jednostavnoj i univerzalnoj semantici lambda računa.

David Turner je rabio svoje kombinatore za ostvarenje programskog jezika SASL.

Kenneth E. Iverson je rabio primitive zasnovane na Curryjevim kombinatorima u svom programskom jeziku J, nasljedniku APL-a. Ovo je Iversonu omogućilo ono što je zvao "šutljivo" (tacit) programiranje; to jest, programiranje u funkcijskim izrazima bez varijabli, zajedno s moćnim alatima za rad s takvim programima. Ispostavilo se da je šutljivo programiranje moguće na nešto nespretniji način u bilo kojem APL-nalik jeziku sa korisnički definiranim operatorima (Pure Functions in APL and J).

Logika

Curry-Howard izomorfizam implicira vezu između logike i programiranja: svaki dokaz teorema intuicionističke logike odgovara redukciji tipiziranog lambda termina, kao i obratno. Štoviše, teoremi se mogu identificirati signaturama tipa funkcije. Specifično, tipizirana kombinatorna logika odgovara Hilbertovom formalnom sustavu (koji se sastoji od aksioma i pravila inferencije) u teoriji dokaza.

K i S kombinatori odgovaraju aksiomima

AK: A → (B → A),

AS: (A → (B → C)) → ((A → B) → (A → C)),

i aplikacija funkcije odgovara pravilu razdvajanja (modus ponens)

MP: iz A i A → B inferiraj B.

Račun koji se sastoji od AK, AS, i MP je potpun za implikacijski fragment intuicionističke logike, što se može vidjeti iz sljedećeg. Neka se promatra skup W svih deduktivno zatvorenih skupova formula, uređenih inkluzijom. Tada je $\langle W,\subseteq \rangle$ intuicionistički Kripkeov okvir, i definiramo model $\Vdash$ u ovom okviru sa

X\Vdash A\iff A\in X.

Ova definicija slijedi uvjete zadovoljavanja na →: s jedne strane, ako $X\Vdash A\to B$ , i $Y\in W$ je takav da $Y\supseteq X$ i $Y\Vdash A$ , tada je $Y\Vdash B$ slijedeći modus ponens. S druge strane, ako $X\not \Vdash A\to B$ , tada je $X,A\not \vdash B$ slijedeći teorem dedukcije, te je stoga deduktivna zatvorenost od $X\cup \{A\}$ element $Y\in W$ takav da $Y\supseteq X$ , $Y\Vdash A$ , i $Y\not \Vdash B$ .

Neka je A bilo koja formula koja nije dokaziva u računu. Tada A ne pripada u deduktivnu zatvorenost X praznog skupa, te je stoga $X\not \Vdash A$ , i A nije intuicionistički validna.

Vidjeti također

SKI kombinatorni račun
B,C,K,W sustav
Kombinator fiksne točke
Stroj redukcije grafa
Superkombinatori
Lambda račun i cilindrička algebra, drugi pristupi modeliranja kvantifikacije i eliminacije varijabli

Izvori

Moses Schönfinkel, 1924, "Über die Bausteine der mathematischen Logik," translated as "On the Building Blocks of Mathematical Logic" in From Frege to Gödel: a source book in mathematical logic, 1879-1931, Jean van Heijenoort, ed. Harvard University Press, 1967. ISBN 0-674-32449-8 Članak koji je osnovao kombinatornu logiku.
Curry, Haskell B.; Robert Feys (1958). Combinatory Logic Vol. I. 1. Amsterdam: North Holland
Curry, Haskell B.; J. Roger Hindley and Jonathan P. Seldin (1972). Combinatory Logic Vol. II. 2. Amsterdam: North Holland. ISBN 0-7204-2208-6
Field, Anthony J. and Peter G. Harrison, 1998. Functional Programming. . Addison-Wesley. ISBN 0-201-19249-7
Paulson, Lawrence C., 1995. Foundations of Functional Programming. University of Cambridge.
Sørensen, Morten Heine B. and Paweł Urzyczyn, 1999. Lectures on the Curry-Howard Isomorphism. University of Copenhagen and University of Warsaw, 1999.
1920-1931 Curry's block notes
Hindley, Roger, and Meredith, 1990, "Principal Type-Schemes and Condensed Detachment," Journal of Symbolic Logic 55: 90-105
Hendrik Pieter Barendregt, 1984. The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, Volume 103, North-Holland. ISBN 0-444-87508-5
Quine, W. V., 1960 "Variables explained away", Proceedings of the American Philosophical Society 104:3:343-347 (Jun. 15, 1960) at JSTOR. Pretiskano kao 23. poglavlje Quineovih Selected Logic Papers (1966), ptr. 227–235

Vanjske poveznice

"Java applet kombinatora"

Daljnje čitanje

Smullyan, Raymond, 1985. To Mock a Mockingbird. Knopf. ISBN 0-394-53491-3. Nježan uvod u kombinatornu logiku, predstavljen kao slijed rekreacijskih zadataka koristeći metafore gledanja ptica.
--------, 1994. Diagonalization and Self-Reference. Oxford Univ. Press. Poglavlja 17-20 su formalniji uvod u kombinatornu logiku, s posebnim naglaskom na rezultate fiksne točke.