SK/SKI/BCKW Combinator Calculus
Most of the information you can find online about SK/SKI/BCKW combinator calculus is fragmentary, intended for a specific, usually academic, purpose, or just hard to find.
To remedy this, at least for me, I will be putting as much stuff I can find here, with links to sources if I have them.
Consider the SK calculus expressions under each section to be using different "namespaces". In other words, the symbols (barring S, K, I, B, C, K, and W) defined in one section don't carry over into other sections unless specified. For example, under "Birds", T represents a Thrush, but under "Logic" it represents True.
If you want to try simplifying some expressions, you can use any number of interpreters, though they usually expect it in a specific form, not necessarily the one used here. You can also use my one, which is fast and probably not innaccurate.
Extra Reading and Sources
- To Dissect a Mockingbird (Also has it's own list of references)
- Combinator Birds
- Unlambda
- Wikipedia article on SKI combinators
- Wikipedia article on BCKW combinators
- Wikipedia article on Lambda calculus
Introduction
In SK calculus, everything is a function, which for these purposeses, is a thing represented by a letter or symbol that can be 'applied' to other functions.
The application of "x" to "y" is written as "xy". An application between two functions is also a function and can be applied to other functions. The application of the application of "x" to "y" to "z" is written as "xyz". Because applications are also functions, you can apply functions to applications, which is different from applying applications to functions. The application of the function "x" to the application of "y" to "z" is written as "x(yz)".
On top of this, the application of a specific function can be defined to be equivalent to some other combination of applying functions. For example, say you define "Fxy" as equivalent to "y", than you can simplify other expressions containing "F". "F(Fab)(Fc)e" becomes simply "e" and the rest follows from there.
This is similar to lambda calculas, except in lambda calculas functions need to be defined first. In SK calculus (and friends), at least two functions must be defined beforehand by context (S, and K, for example), and all other functions are defined as combinations of them.
The following functions are, for historical reasons, considered "standard".
- Sxyz = xz(yz)
- Kxy = x
- Ix = x
- Bxyz = x(yz)
- Cxyz = xzy
- Wxy = xyy
Because B, C, W, and I can be defined (relatively) easily in terms of S and K, they are sometimes left out of a base definition, though still useful.
- B = S(KS)K
- C = S(S(K(S(KS)K))S)(KK)
- W = SS(SK)
- I = SKK
Arithmetic
Everything in SK calculus is a function, so numbers must be too. A traditional way of representing numbers as functions is using Church numerals, where the representation of a number N is a function that applies it's first argument to it's second N times. In SK calculus, it is easy to define a successor function "+" that increments a number given to it, and then the numbers 1 and 0. From there, all other numbers can be defined.
- 0 = SK
- 1 = SKK
- + = SB = S(S(KS)K)
- 2 = +1
- 3 = +2
- ...
A predecessor function "-" (for decrementing numbers) can also be defined, although it is somewhat slow and large.
- - = S(K(SI(K(SK)))) (S(SI(K(S(K(S(K(S(SI(K(SK)))))K)) (S(S(SI(KK))(SI(K(SK)))) (S(K(SB))(SI(K(SK)))))))) (K(S(SI(KK))(K(SK)))))
Adding numbers is easy, use b+a, where a and b are the numbers you want to add, and "+" is the successor function. Subtraction is done the same way but with minus instead of the plus. Another easy operation, counter-intuitively, is exponentation. "a to the power of b" is written as ba. Multiplication takes the form b(a+)0, where the result is "a multiplied by b".
In summary:
- a plus b: b+a
- a minus b: b-a
- a times b: b(a+)0
- a to the power of b: ba
Division is weird but I derived a division operator (with the help of the birds and lambda calculus). "a divided by b" is "/ba":
- / = C(BB(WI(BW(W(BBB(C(BC(B(BBB) (BW(B(C(C(BC(C(BB(BC(CI) (KK)(SK)))+))0))))))-))))))+
It works using recursion and stuff. Bear in mind that it is very slow for "large" numbers (15 for example).
Logic (and lists)
Boolean logic can be expressed using ifelse-like statements, meaning that True is a function that returns the first of it's two arguments, and False returns the second.
- T = K
- F = SK
The basic AND, OR, and NOT operators can be created just by using True and False. "a AND b" can be rephrased as "if a is True, than b, otherwise False". Likewise "a OR b" can be rephrased as "if a is True, than True, otherwise b". Finally, "NOT a" can be rephrased as "if a is True, than False, otherwise True".
- a AND b: abF
- a OR b: aTb
- NOT a = aFT
Other commonly used operators can also be formed using these three.
- a NAND b: aF(bFT)
- a NOR b: a(bFT)T
- a XOR b: a(bFT)b
- a NXOR b: ab(bFT)
- a IMP b: abT
Lists can be created with a join function "," that applies the third argument to the first two, allowing either of them to be retrieved. Using this join function, a list of five values a, b, c, d, and e can be written ,a(,b(,c(,d(,eK)))). Because True returns it's first argument and False returns it's second argument, they can be given to a list to return the corresponding sides of the join.
- , = BC(CI)
Birds
Sourced from: Combinator Birds.
- Bluebird [abc -> a(bc)]: B = S(KS)K
- Blackbird [abcd -> a(bcd)]: BBB
- Bunting [abcde -> a(bcde)]: B(BBB)B
- Becard [abcd -> a(b(cd))]: B(BB)B
- Cardinal [abc -> acb]: C = S(BBS)(KK)
- Dove [abcd -> ab(cd)]: D = BB
- Dickcissel [abcde -> abc(de)]: B(BB)
- Dovekies [abcde -> a(bc)(de)]: BB(BB)
- Eagle [abcde -> ab(cde)]: E = B(BBB)
- Bald Eagle [abcdefg -> a(bcd)(efg)]: BEE
- Finch [abc -> cba]: F = ETTET = B(BBB)(CI)(CI)(B(BBB))(CI)
- Goldfinch [abcd -> ad(bc)] G = BBC
- Hummingbird [abc -> abcb]: H = BW(BC)
- Identity Bird [a -> a]: I = SKK
- Jay [abcd -> ab(adc)]: J = B(BC)(W(BC(B(BBB))))
- Kestrel [ab -> a]: K
- Lark [ab -> a(bb)]: L = CBM = CB(WI)
- Mockingbird [a -> aa]: M = WI = SII
- Double Mockingbird [ab -> ab(ab)]: BM = B(WI)
- Owl [ab -> b(ab)]: O = SI
- Queer Bird [abc -> b(ac)]: Q = CB
- Quixotic Bird [abc -> a(cb)]: BCB
- Quizzical Bird [abc -> b(ca)]: C(BCB)
- Quirky Bird [abc -> c(ab)]: BT = B(CI)
- Quacky Bird [abc -> c(ba)]: B(BC)(BC(BC))B
- Robin [abc -> bca]: R = BBT = BB(CI)
- Starling [abc -> ac(bc)]: S
- Thrush [ab -> ba]: T = CI
- Turing [ab -> b(aab)]: U = LO = CB(WI)(SI)
- Vireo [abc -> cab]: BCT = BC(CI)
- Warbler [ab -> abb]: C(BMR) = C(B(WI)BB(CI))
- Converse Warbler [ab -> baa]: CW
- Sage Bird [a -> ...]: Y = SLL = S(CB(WI))(CB(WI))
- Identity Bird Once Removed [ab -> ab]: S(SK)
- Warbler Once Removed [abc -> abcc]: BW
- Cardinal Once Removed [abcd -> abdc]: BC
- Robin Once Removed [abcd -> acdb]: BC(BC)
- Finch Once Removed [abcd -> adcb]: B(BC)(BC(BC))
- Vireo Once Removed [abcd -> acbd]: BC(B(BC)(BC(BC)))
- Warbler Twice Removed [abcd -> abcdd]: B(BW)
- Cardinal Twice Removed [abcde -> abced]: B(BC)
- Robin Twice Removed [abcde -> abdec]: B(BC(BC))
- Finch Twice Removed [abcde -> abedc]: B(B(BC)(BC(BC)))
- Vireo Twice Removed [abcde -> abecd]: B(BC(B(BC)(BC(BC))))
- Kite [ab -> b]: KI = SK
- Omega [...]: WI(WI)
- Konstant Mocker [ab -> bb]: KM = K(WI)
- Crossed Konstant Mocker [ab -> aa]: C(KM) = C(K(WI))
- Theta [...]: YO = S(CB(WI))(CB(WI))(SI)