WikiSysop: Bot: Automatski unos stranica

2021-08-23T03:03:29Z

Bot: Automatski unos stranica

Nova stranica

'''Kombinatorna logika''' je notacija koju su uveli [[Moses Schönfinkel]] i [[Haskell Curry]] kako bi eliminirali potrebu za [[varijabla]]ma u [[matematička logika|matematičkoj logici]]. U zadnje se vrijeme koristi u računarstvu kao teoretski [[model računanja]] te također kao baza za [[funkcijsko programiranje|funkcijske programske jezike]]. Zasnovan je na '''kombinatorima''', koji su [[funkcija višeg reda|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šte u Göttingenu|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 [[teorija modela|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čunanje|računanja]], korišten u [[teorija izračunljivosti|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čun]]a, u kojoj su lambda izrazi (koji predstavljaju funkcijsku apstrakciju) zamijenjeni skupom ''kombinatora'', primitivnih funkcija koji nemaju [[slobodna varijabla|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 [[striktni programski jezik|nestriktnih]] [[funkcijsko programiranje|funkcijskih]] programskih jezika i [[stroj za redukciju grafa|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 [[teorija modela|teoriju modela]] i kombinatornu logiku.

== Sažetak lambda računa ==
{{glavni|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 [[beta normalni oblik|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 [[asocijativnost|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 [[model računanja|modelima računanja]] (uključujući [[Turingov stroj|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-Turingova teza|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 [[slobodna varijabla|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 [[ekstenzionalna jednakost|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 [[rekurzija|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''<nowiki>[</nowiki>''λx''.''T''<nowiki>[</nowiki>''λy''.''E''<nowiki>]]</nowiki> (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''<nowiki>[</nowiki>''λx''.''T''<nowiki>[</nowiki>''λy''.(''y'' ''x'')<nowiki>]]</nowiki> (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 [[Veliko O notacija|Θ]](3''n'').

==== 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''.((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'', [[Moses Schönfinkel|Schönfinkel]]ov 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 [[Haskell Curry|Curry]], a mnogo kasnije i [[David Turner (računalni znanstvenik)|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''<nowiki>[</nowiki>''λx''.''T''<nowiki>[</nowiki>''λy''.''E''<nowiki>]]</nowiki> (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''<nowiki>[</nowiki>''λx''.''T''<nowiki>[</nowiki>''λy''.(''y'' ''x'')<nowiki>]</nowiki><nowiki>]</nowiki>
= ''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 [[Moses Schönfinkel|Schönfinkel]]a, 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čiv]]o 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 [[Riceov teorem|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 jezik|Funkcijski programski jezici]] su često zasnovani na jednostavnoj i univerzalnoj [[Formalna semantika programskih jezika|semantici]] [[lambda račun]]a.

David Turner je rabio svoje kombinatore za ostvarenje [[SASL (programski jezik)|programskog jezika SASL]].

[[Kenneth E. Iverson]] je rabio primitive zasnovane na Curryjevim kombinatorima u svom [[J (programski jezik)|programskom jeziku J]], nasljedniku [[APL (programski jezik)|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 ([http://portal.acm.org/citation.cfm?id=114065&dl=GUIDE&coll=GUIDE Pure Functions in APL and J]).

=== Logika ===

[[Curry-Howard izomorfizam]] implicira vezu između logike i programiranja: svaki dokaz teorema [[intuicionistička logika|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 [[teorija dokaza|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 [[inkluzija (teorija skupova)|inkluzijom]]. Tada je <math>\langle W,\subseteq\rangle</math> intuicionistički [[Kripkeova semantika|Kripkeov okvir]], i definiramo model <math>\Vdash</math> u ovom okviru sa
:<math>X\Vdash A\iff A\in X.</math>
Ova definicija slijedi uvjete zadovoljavanja na →: s jedne strane, ako <math>X\Vdash A\to B</math>, i <math>Y\in W</math> je takav da <math>Y\supseteq X</math> i <math>Y\Vdash A</math>, tada je <math>Y\Vdash B</math> slijedeći modus ponens. S druge strane, ako <math>X\not\Vdash A\to B</math>, tada je <math>X,A\not\vdash B</math> slijedeći [[teorem dedukcije]], te je stoga deduktivna zatvorenost od <math>X\cup\{A\}</math> element <math>Y\in W</math> takav da <math>Y\supseteq X</math>, <math>Y\Vdash A</math>, i <math>Y\not\Vdash B</math>.

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 <math>X\not\Vdash A</math>, 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]]
* [[Superkombinator]]i
* [[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.
*{{cite book
| last = Curry
| first = Haskell B.
| coauthors = Robert Feys
| title = Combinatory Logic Vol. I
| volume = 1
| year = 1958
| publisher = North Holland
| location = Amsterdam
}}
*{{cite book
| last = Curry
| first = Haskell B.
| coauthors = J. Roger Hindley and Jonathan P. Seldin
| title = Combinatory Logic Vol. II
| volume = 2
| year = 1972
| publisher = North Holland
| location = Amsterdam
| id = {{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. ''[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.
*[http://www.sadl.uleth.ca/gsdl/cgi-bin/library?a=p&p=about&c=curry 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}}
*[[Willard Van Orman Quine|Quine, W. V.]], 1960 "Variables explained away", ''Proceedings of the American Philosophical Society'' '''104''':3:343-347 (Jun. 15, 1960) [http://links.jstor.org/sici?sici=0003-049X%2819600615%29104%3A3%3C343%3AVEA%3E2.0.CO%3B2-W at JSTOR]. Pretiskano kao 23. poglavlje Quineovih ''Selected Logic Papers'' (1966), ptr. 227–235

== Vanjske poveznice ==

* [http://cstein.kings.cam.ac.uk/~chris/combinators.html "Java ''applet'' kombinatora"]

== Daljnje čitanje ==

* [[Raymond Smullyan|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.

[[Kategorija:Lambda račun]]
[[Kategorija:Matematika]]

←Starija inačica		Inačica od 22. ožujak 2022. u 11:43
Redak 1:		Redak 1:
	~~<!--'''Kombinatorna logika'''-->'''~~Kombinatorna logika''' je notacija koju su uveli [[Moses Schönfinkel]] i [[Haskell Curry]] kako bi eliminirali potrebu za [[varijabla]]ma u [[matematička logika\|matematičkoj logici]]. U zadnje se vrijeme koristi u računarstvu kao teoretski [[model računanja]] te također kao baza za [[funkcijsko programiranje\|funkcijske programske jezike]]. Zasnovan je na '''kombinatorima''', koji su [[funkcija višeg reda\|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''' je notacija koju su uveli [[Moses Schönfinkel]] i [[Haskell Curry]] kako bi eliminirali potrebu za [[varijabla]]ma u [[matematička logika\|matematičkoj logici]]. U zadnje se vrijeme koristi u računarstvu kao teoretski [[model računanja]] te također kao baza za [[funkcijsko programiranje\|funkcijske programske jezike]]. Zasnovan je na '''kombinatorima''', koji su [[funkcija višeg reda\|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 logika u matematici ==

Kombinatorna logika - Povijest promjena

WikiSysop: bnz

WikiSysop: Bot: Automatska zamjena teksta (-{{cite book +{{Citiranje knjige)

WikiSysop: Bot: Automatski unos stranica

←Starija inačica		Inačica od 17. studeni 2021. u 05:15
Redak 354:		Redak 354:
	== Izvori ==		== 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.		* [[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.
	*{{~~cite book~~		*{{Citiranje knjige
	\| last = Curry		\| last = Curry
	\| first = Haskell B.		\| first = Haskell B.
Redak 364:		Redak 364:
	\| location = Amsterdam		\| location = Amsterdam
	}}		}}
	*{{~~cite book~~		*{{Citiranje knjige
	\| last = Curry		\| last = Curry
	\| first = Haskell B.		\| first = Haskell B.