SKI kombinatorni račun je računski sustav koji predstavlja reduciranu, netipiziranu inačicu lambda računa.
Sve su operacije lambda računa izražene u SKI kao binarna stabla čiji su listovi jedan od tri simbola S, K, i I (zvani kombinatori). Ustvari, simbol I je dodan samo zbog zgodnosti, i dovoljna su druga dva za sve svrhe SKI sustava.
Iako najformalnije predstavljanje objekata u ovom sustavu zatijeva binarna stabla, ona su obično predstavljena, u svrhu postavljanja tipa, kao zagrađeni izrazi, ili sa zagrađenim svim podstablima, ili samo sa zagrađenom djecom podstablima s desne strane. Stoga, stablo čije je lijevo podstablo stablo KS i čije je desno podstablo stablo SK se obično tipizira kao ((KS)(SK)), ili jednostavnije kao KS(SK), mjesto da bude u potpunosti iscrtano kao stablo (što bi formalnost i čitljivost zahtijevale).
Neformalni opis
Neformalno, rabeći žargon programskih jezika, stablo (xy) se može shvatiti kao "funkcija" x primijenjena na "argument" y. Prilikom "evaluacije" (tj. kad je funkcija "primijenjena" na argument), stablo "vraća vrijednost", tj. transformira se u drugo stablo. Naravno, svo troje od "funkcije", "argumenta" i "vrijednosti" su ili kombinatori, ili binarna stabla, i ako se radi o binarnim stablima tada se i oni mogu shvatiti kao funkcije kadgod bude potrebe za time.
Operacija evaluacije je definirana na sljedeći način:
(x, y, i z predstavljaju izraze načinjene od funkcija S, K, i I, i postavljaju vrijednosti):
I vraća proslijeđeni argument:
- Ix → x
K, kad apliciran na bilo koji argument x, vraća konstantnu funkciju jednog argumenta Kx koja, kad aplicirana na bilo koji argument, vraća x:
- Kxy → x
S je operator supstitucije. Prima tri argumenta i potom vraća prvi argument apliciran na treći, koji je tad apliciran na rezultat aplikacije drugog argumenta na treći. Jasnije:
- Sxyz → xz(yz)
Primjer računanja: SKSK evaluira u KK(SK) S-pravilom. Tada, ako se evaluira KK(SK), dobije se K K-pravilom. Budući da se nijedno pravilo više ne može primjeniti, računanje staje.
Valja uočiti da će za sva stabla x i sva stabla y SKxy uvijek evaluirati u y u dva koraka, i konačni će rezultat evaluiranja SKxy uvijek biti jednak rezultatu evaluiranja y. Kaže se da su SKx i I "funkcijski ekvivalentni" s obzirom da uvijek daju isti rezultat kad su aplicirani na bilo koji y.
Valja uočiti da se iz ovih definicija može pokazati da SKI račun nije minimalni sustav koji u potpunosti može obaviti računanja lambda računa, s obzirom da sva pojavljivanja I u bilo kojem izrazu mogu biti zamijenjena sa (SKK) ili (SKS) or (S K nešto) ii rezultirajući će izraz uvijek dati isti rezultat. Stoga je "I" puki sintaksni šećer.
Ustvari, moguće je definirati potpuni sustav rabeći samo jedan kombinator. Primjer je jota kombinator Chrisa Barkera, definiran na sljedeći način:
- ιx = xSK
Formalna definicija
Termini i derivacije u ovom sustavu također mogu biti formalno definirani:
Termini: Skup T termina je definiran rekurzivno sljedećim pravilima.
- S, K, i I su termini.
- Ako su τ1 i τ2 termini, tada je (τ1τ2) termin.
- Ništa nije termin osim ako to zahtijevaju prva dva pravila.
Derivacije: Derivacija je konačan slijed termina definiran rekurzivno sljedećim pravilima (gdje sva grčka slova predstavljaju validne termine ili izraze sa potpuno balansiranim zagradama):
- Ako je Δ derivacija koja završuje u izrazu oblika α(Iβ)ι, tada je Δ nakon kojeg slijedi termin αβι derivacija.
- Ako je Δ derivacija koja završuje u izrazu oblika α((Kβ)γ)ι, tada je Δ nakon kojeg slijedi termin αβι derivacija.
- Ako je Δ derivacija koja završuje u izrazu oblika α(((Sβ)γ)δ)ι, tada je Δ nakon kojeg slijedi termin α((βδ)(γδ))ι derivacija.
Pretpostavljajući da je slijed validna početna derivacija, može biti prošireni ovim pravilima. [1]
SKI izrazi
Samoaplikacija i rekurzija
SII je izraz koji prima argument i aplicira ga na samog sebe:
- SIIα → Iα(Iα) → αα
Jedno od zanimljivih svojstava ovoga jest to da čini izraz SII(SII) ireducibilnim:
- SII(SII) → I(SII)(I(SII)) → I(SII)(SII) → SII(SII)
Druga stvar koja je posljedica ovoga jest ta da dopušta pisanje funkcije koja aplicira nešto na samoaplikaciju nečega drugog:
- (S(Kα)(SII))β → Kαβ(SIIβ) → α(SIIβ) → α(ββ)
Ova se funkcija može rabiti za ostvarenje rekurzije. Ako je β funkcija koja aplicira α na samoaplikaciju nečega drugog, tada samoaplicirajući β obavlja α rekurzivno na ββ. Jasnije, ako je
- β = S(Kα)(SII)
tada:
- SIIβ → ββ → α(ββ) → α(α(ββ)) → …
Revertirajući izraz
S(K(SI))K revertira sljedeća dva termina:
- S(K(SI))Kαβ →
- K(SI)α(Kα)β →
- SI(Kα)β →
- Iβ(Kαβ) →
- Iβα → βα
Booleova logika
SKI kombinatorni račun također može ostvariti bulovsku logiku u obliku ako-tada-inače strukture. Ako-tada-inače struktura se sastoji od bulovskog izraza koji je ili T (true - istinit) ili F (false - lažan), takvih da:
- Txy → x
i
- Fxy → y
Ključ leži u definiranju dvaju bulovksih izraza. Prvi radi baš poput jednog od osnovnih kombinatora:
- T = K
- Kxy → x
Drugi je također jednostavan:
- F = KI
- KIxy → Iy → y
Jednom kad su Istina i Laž definirani, sva bulovska logika može biti ostvarena pomoću ako-tada-inače struktura.
Bulovski NOT (koji vraća suprotnost danog booleana) radi na isti način kao ako-tada-inače struktura, sa Istinom i Laži kao drugim i trećim vrijednostima, tako da može biti ostvaren kao postfiksna operacija:
- NOT = (F)(T) = (KI)(K)
Ako se ovo stavi u ako-tada-inače strukturu, može se pokazati da ovo ima očekivani rezultat
- (T)NOT=T(F)(T)=F
- (F)NOT=F(F)(T)=T
Bulovski OR (koji vraća Istinu ako je bilo koja od dvije okružujuće bulovske vrijednosti Istina) radi na isti način kao i ako-tada-inače struktura s Istinom kao drugom vrijednošću, tako da može biti ostvarena kao infiksna operacija:
- OR = T = K
Ako se ovo stavi u ako-tada-inače strukturu, može se pokazati da ovo ima očekivani rezultat:
- (T)OR(T)=T(T)(T)=T
- (T)OR(F)=T(T)(F)=T
- (F)OR(T)=F(T)(T)=T
- (F)OR(F)=F(T)(F)=F
Bulovski AND (koji vraća Istinu ako su obje okružujuće bulovske vrijednosti Istinite) radi na isti način kao i ako-tada-inače struktura sa Laži kao trećom vrijednošću, tako da može biti ostvarena kao postfiksna operacija:
- AND = F = KI
Ako se ovo stavi u ako-tada-inače strukturu, može se pokazati da ovo ima očekivani rezultat:
- (T)(T)AND=T(T)(F)=T
- (T)(F)AND=T(F)(F)=F
- (F)(T)AND=F(T)(F)=F
- (F)(F)AND=F(F)(F)=F
S obzirom da ovo definira Istinu, Laž, NOT (kao postfiksni operator), OR (kao infiksni operator) i AND (kao postfiksni operator) pomoću SKI notacije, ovo dokazuje da SKI sustav može u potpunosti izraziti Booleovu logiku.