SKI Calculus - A variable-free programming language
Published on May 22, 2024
This post is a beginning of a new series with a new tag called "programming languages". I plan to discuss interesting ideas behind programming languages. This post is devoted to a very simple form of calculation system called SKI calculus. SKI calculus was developed by Schoenfinkel in the 1920's. The properties of SKI Calculus was known even before computers were built. Understanding SKI Calculus lays down foudation for understanding more involved modern languages. Let's first see what are the rules of SKI calculus.
Side Note: You can use SKI Calculus Interpreter to experiment with the SKI programs we discuss below!
SKI Rewrite Rules
Like any other calculation system, there are predefined set of rules:
Rule | Description |
---|---|
I combinator - Identify function | |
K combinator - Constant function | |
S combinator - Genaralized form of function application |
A combinator is a function without free-variables. A function call is written by juxtaposing two expressions. means apply function to and the arrow represents the calculation step. On the right hand side is the output of compulation which is .
Expressions as binary trees and rules as tree transformations
Paranthesis should be used to represent associativity. Whenever no paranthesis are present assume implicit left associativity. Considering these we can represent expressions as simple binary trees and think rewrite rules as tree transformations. See below:
takes only one argument and outputs the argument. That's why we called it identity function.
takes two arguments and returns the first argument, ignoring the second argument. This means that no matter what the second argument is, the result is always the first argument. Hence, it is called a constant function.
takes in three arguments and apply the first argument (a function) and second argument to the third argument. This is the way to program function calls (applications) and reusing values (make copies). combines both of them.
Function execution
, , and are well formed functions they don't execute without required number of arguments.
needs atleast one argument and it only uses the first argument.
Exmaples function executions:
- - cannot execute as it expected a single argument.
- - needs atleast one argument and it only uses the first argument which results .
- - cannot execute as it expected two arguments.
- - one argument is not enough, so function holds.
- - two arguments is not enough, so function holds. We call above and this are partially applied functions.
- - More than enough arguments. Only first three arguments used and resutls .
Definition of Terms
The terms of the SKI calculus are the smallest set such that
- , , and are terms
- If and are terms,then is a term
CFG for SKI terms
We can derive valid SKI terms using the following simple Context Free Grammar.
, , and are terminals and is the only non-terminal.
Lets see some computation examples
If you look closely, this example shows a kind of looping which is never-ending loop. Let's see more on looping later on when discussing natural number representation.
Programming with SKI Calculus
To do actual programming we need a way to recurse (form of iteration or looping), conditionls (if-else or branching), and data structures. The last example above is a form of looping of it is non-terminating but not much use in it.
Recursive function calls are little more involved, which calls the function itself again and again.
For example consider following expression:
Now lets work on function application:
Now this is able to call the function again and again and but it generates never-ending recursive function calls. We will see how to do a fixed number of calls later on under natual numbers discussion.
Branching behavior
We need boolean but, there is no such a thing in SKI Calculus. But we can encode SKI terms intuitively be true and false values. And find combinators for not, and and or boolean operations.
Booleans
Similarly, We can represent false by a function which picks the second of the two argumenets called upon. We can represent true by a function which picks the first of the two argumenets called upon. So:
Now we can intuitively define and . You can now apply these combinators to above and see it works (later on, we will see how to derive them systematically).
Boolean operations
NOT operation
Let be a Boolean ( or we chose above)
OR operation
Let be a Boolean ( or we chose above)
AND operation
Let be a Boolean ( or we chose above)
Example boolean expression evaluations
Now we can apply the boolean expresion rules we showed above and using and encoded as and .
What about conditionals?
Let be a Boolean ( or we chose above). Now we can intuitively think of an expression as below:
What about writing a combinator for swap operation?
How can we write a combinator for swap using , , and . Seems it is not as easy as the ones could derive right away.
Actually swap can systematically be derived as:
By now, it should be clear why it's difficult to guess or intuitively think of one. No worries! There is a systematic way to derive combinators.
Abstraction Algorithem
We need an Abstraction Algorithm that can map the right-hand side to a combinator. We can state mapping functions by reversing the rewrite rules of SKI calculus. The process is to eliminate the variables by replacing them with uses of the combinators , , and .
Consider a function equation of one variable as:
If we apply function to argument , the result is .
We want a combinator that implements . So,
Note that doesn't use . We say that we have abstracted with respect to .
Now, we can see how to abstract out each rule to mappers.
Below are definitions of generalized mappers with none of them using .
-
Correctness: -
if does not appear in
Correctness: -
Correctness:
Let's try to systematically derive a combinator for 'swap'
Let's abstract out each argument, one at a time. First we eliminate which is the last argument. We can eliminate first argument .
Eliminating :
Eliminating :
Okay, Abstraction algorithem is a very simple and systematic procedure. But it can become a tedious task to derive one and can be a very long expression as well. We can do something clever to reduce the size of the combinators by trying to further simplify the third abstraction above.
Helper Combinators for Abstract Algorithem
If you look at the third mapper , we never said or does not include . But we can simplify further when we know if either or contains .
Let's define two new combinators like below:
- is a version of where first argument is constant (means does not use )
- is a version of where second argument is constant (means does not use )
Okay now we can think about mappers using them:
- where does not use
- where does not use
- This general case can be applied without knowing specifics about or
Now let's use abstraction algorithem to derive combinators for and in terms of , and :
Deriving c1
Observe below,
Therefore,
So, now we can write,
Then we get,
Then,
Observe below,
Therefore,
Finally, we can write,
Deriving c2
Note that for the derivation of we can use combinator directly.
Think how long would be if we didn't use the combinator.
Let's again derive 'swap' but this time using the helpers
Great!! it's in a very short form thanks to and .
Introducing Abstract Data Type: Pairs
Let's see how we can represent a simple abstract data structure now. Suppose we want to have a data structure called pair where we can access the first and second elements by specifying it as an argument as below:
Remember how we use and to handle if-then-else above. We can choose:
Then we can state:
Let's abstract out combinator now:
SKI is a language with higher-order functions (functions that take functions as arguments and return functions as results). For example following are higher-order functions:
- can read as swap with . You can give an argument function and get the output function which is the opposite of as it was before (apply to )
-
Natural Numbers
Remember how we got the boolean true and false values. Boolean are actually encoded using , , and . What we can try to get natural numbers is the same. We need to encode each number starting from zero. We can think of a combinator that does apply a function times to another as the natural number . Let's find that combinator that applies it's first argument times to its second argument as below:
Note when
We can find a combinator succ (successive application) as below:
where
Correctness:
Therefore:
We can define as:
Now apply to :
So we can write:
Just to be clear, once again let's apply to :
So we can write:
Now it's clear that we can express n th natural numbers in the form of:
Nutual numbers in SKI Calculus have built-in iteration as we see above.
Addition and Multiplication
Now we can think about addition using and :
Most importantly and are any natural numbers we derive above. We can read the right hand side like apply combinator times to . We are adding 1 at a time to y, x many times to get (x+y) encoded in , and . Great, now we can abstract out as a combinator:
Similarly using the application of , muliplication can be expressed in terms of addition as below:
We can read it as do add y, x many times starting from 0. You can abstract out mul as we did for add, but I won't do it here since it's almost same.
Now let's see how to write some arithmetic expression in SKI Calculus. Note numbers in below are SKI encoded natural numbers and * and + represent and combinators shown above.
We can express (3x4)+5 in SKI calculus as below:
We began by introducing SKI Calculus, then explored conditionals, abstract data types like pairs, and derived natural numbers and simple arithmetic operations. That wraps up this blog post. I hope you've gained some new insights. Also, I'd like to express my gratitude to Alex Aiken for sharing the lecture notes publicly. This entire post is based on my understanding of his lecture slides.
Looking forward to seeing you in a new post! Bye!
If you like it, share it!