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 prijegled rane povijesti kombinatorne logike. Za suvremeniji paralelni tretman kombinatorne logike i lambda računa, vidi Barendregt (1984.), koji također daje prijegled 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, primjenjena 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 primjenjen 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*[&nbsp;], koja vrši konverziju proizvoljnog lambda termina u ekvivalentni kombinator.

*T*[&nbsp;] 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 primjenimo 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*[&nbsp;] konstrukcija može proširiti lambda termin duljine *n* u kombinatorni termin duljine Θ(3*n*).

#### Objašnjenje ''T''[&nbsp;] transformacije
*T*[&nbsp;] 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**[&nbsp;] 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*.((x**S**)**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'''<sub>K</sub> nasuprot '''CL'''<sub>I</sub> 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*[&nbsp;] 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**[&nbsp;].

## 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.

## Povezano
* Lambda račun

## Literatura
* 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.  Članak koji je osnovao kombinatornu logiku.
* 
* 
* Field, Anthony J. and Peter G. Harrison, 1998. *Functional Programming*. . Addison-Wesley. 
* Paulson, Lawrence C., 1995. *[http://www.cl.cam.ac.uk/Teaching/Lectures/founds-fp/Founds-FP.ps.gz Foundations of Functional Programming.]* University of Cambridge.
* Sørensen, Morten Heine B. and Paweł Urzyczyn, 1999. *[http://folli.loria.fr/cds/1999/library/pdf/curry-howard.pdf 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. 
* 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

## Dodatna literatura
* Smullyan, Raymond, 1985. *[[To Mock a Mockingbird]]*. Knopf. . 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.

## Vanjske veze
* "Java ''applet'' kombinatora"