author-pic

Amila Senadheera

Tech enthusiast

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
Ix → x I combinator - Identify function
Kxy → x K combinator - Constant function
Sxyz(xz)(yz) S combinator - Genaralized form of function application

A combinator is a function without free-variables. A function call is written by juxtaposing two expressions. Ix means apply function I to x and the arrow  →  represents the calculation step. On the right hand side is the output of compulation which is x.

IxxComputation stepOutputArgumentFunction

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:

( I x ) x
Ixx

I takes only one argument and outputs the argument. That's why we called it identity function.

( ( K x ) y ) x
Kxyx

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

( ( ( S x ) y ) z ) ( x z ) ( y z )
Szyxxzyz

S 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). S combines both of them.

Function execution

S, K, and I are well formed functions they don't execute without required number of arguments.

I needs atleast one argument and it only uses the first argument.

Exmaples function executions:

  • I - cannot execute as it expected a single argument.
  • Ixy - needs atleast one argument and it only uses the first argument which results xy.
  • K - cannot execute as it expected two arguments.
  • Kx - one argument is not enough, so function holds.
  • Sxy - two arguments is not enough, so function holds. We call above and this are partially applied functions.
  • Swxyz - More than enough arguments. Only first three arguments used and resutls wy(xy)z.

Definition of Terms

The terms of the SKI calculus are the smallest set such that

  • S, K, and I are terms
  • If x and y are terms,then xy is a term

CFG for SKI terms

We can derive valid SKI terms using the following simple Context Free Grammar.

TermTerm Term Term(Term) TermS TermK TermI

S, K, and I are terminals and Term is the only non-terminal.

Lets see some computation examples

S K x y ( K y ) ( x y ) y
SyxKKyxyy
S I I x ( I x ) ( I x ) x ( I x ) x x
SxIIIxIxxx
( S I I ) ( S I I ) ( I ( S I I ) ) ( I ( S I I ) )
SIISIISIIISIII

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: w = S ( K f ) ( S I I )

Now lets work on function application:

S I I w →* w w = S ( K f ) ( S I I ) w →* ( ( K f ) w ) ( ( S I I ) w ) f ( ( S I I ) w ) f ( w w ) →* f ( f ( w w ) ) →* f ( f ( f ( w w ) ) )

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:

T x y = x F x y = y

Now we can intuitively define T=K and F=SK . You can now apply these combinators to above and see it works (later on, we will see how to derive them systematically).

xKyxTyx=SyxKKyxyyFyx=

Boolean operations

NOT operation

Let B be a Boolean (T or F we chose above)

not B = B F T

B notB
T notT=TFT=K(SK)KSK=F
F
notF=FFT=((SK)(SK))K(KK)((SK)K)K=T
OR operation

Let B be a Boolean (T or F we chose above)

B1 or B2 = B1 T B2

B1 B2 B1orB2
T T
TTT=KKKK=T
T F
TTF=KK(SK)K=T
F T
FTT=(SK)KK(KK)(KK)K=T
F F
FTF=(SK)K(SK)(K(SK))(K(SK))SK=F
AND operation

Let B be a Boolean (T or F we chose above)

B1 and B2 = B1 B2 F

B1 B2 B1andB2
T T
TTF=KK(SK)K=T
T F
TFF=K(SK)(SK)SK=F
F T
FTF=(SK)K(SK)((K(SK))((K(SK))SK=F
F F
FFF=(SK)(SK)(SK)((K(SK))(((SK)(SK))SK=F
Example boolean expression evaluations

Now we can apply the boolean expresion rules we showed above and using T and F encoded as K and SK.

( not F ) and T = ( F F T ) T F T T F T

F or ( not F ) = F T ( F F T ) F T T T

What about conditionals?

Let B be a Boolean (T or F we chose above). Now we can intuitively think of an expression as below:

if B then x else y = B x y

B Bxy
T Kxyx
F (SK)xy(Ky)(xy)y

What about writing a combinator for swap operation?

swap x y = y x

How can we write a combinator for swap using S, K, and I. Seems it is not as easy as the ones could derive right away.

Actually swap can systematically be derived as:

swap = S ( K ( S I ) ) ( S ( K K ) I )

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 A() 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 S, K, and I.

Consider a function equation of one variable as:

f x = E

If we apply function f to argument x, the result is E.

We want a combinator A(E,x) that implements f. So,

A ( E , x ) x = E

Note that A(E,x) doesn't use x. We say that we have abstracted E with respect to x.

Now, we can see how to abstract out each rule to mappers.

Below are definitions of generalized mappers with none of them using x.

  • A(x,x)=I

    Correctness:

    Ix=x
  • A(E,x)=KE
    if x does not appear in E

    Correctness:

    KEx=E
  • A(E1E2,x)=SA(E1,x)A(E2,x)

    Correctness:

    S A ( E1 , x ) A ( E2 , x ) x ( A ( E1 , x ) x ) ( A ( E2 , x ) x ) E1 ( A ( E2 , x ) x ) E1 E2

Let's try to systematically derive a combinator for 'swap'

swap ( x , y ) = ( y , x )

Let's abstract out each argument, one at a time. First we eliminate y which is the last argument. We can eliminate first argument x.

Eliminating y:

swap x = A ( yx , y ) = S A ( y , y ) A ( x , y ) = S I ( K x )

Eliminating x:

swap = A ( S I ( K x ) , x ) = S A ( S I , x ) A ( Kx , x ) = S ( K ( S I ) ) ( S A ( K , x ) A ( x , x ) ) = S ( K ( S I ) ) ( S ( K K ) I )

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 A(E1E2,x), we never said E1 or E2 does not include x. But we can simplify further when we know if either E1 or E2 contains x.

Let's define two new combinators like below:

  • c1xyz=x(yz)
    c1 is a version of S where first argument is constant (means x does not use z)
  • c2xyz=(xz)y
    c2 is a version of S where second argument is constant (means y does not use z)

Okay now we can think about mappers using them:

  • A(E1E2,x)=c1E1A(E2,x)
    where E1 does not use x
  • A(E1E2,x)=c2A(E1,x)E2
    where E2 does not use x
  • A(E1E2,x)=SA(E1,x)A(E2,x)
    This general case can be applied without knowing specifics about E1 or E2

Now let's use abstraction algorithem to derive combinators for c1 and c2 in terms of S, K and I:

Deriving c1

c1 x y z = x ( y z )

c1 x y = A ( x ( y z ) , z ) = S A ( x , z ) A ( y z , z ) = S ( K x ) ( S A ( y z ) A ( z , z ) ) = S ( K x ) ( S ( K y ) I )

Observe below,

S ( K y ) I w ( ( K y ) w ) ( I w ) y w

Therefore,

S ( K y ) I = y

So, now we can write,

c1 x y = S ( K x ) y

Then we get,

c1 x = S ( K x )

Then,

c1 = A ( S ( K x ) , x ) = S A ( S , x ) A ( K x , x ) = S ( K S ) ( S A ( K , x ) A ( x , x ) ) = S ( K S ) ( S ( K K ) I )

Observe below,

( S ( K K ) I ) w = ( ( K K ) w ) ( I w ) = K w

Therefore,

S ( K K ) I = K

Finally, we can write,

c1 = S ( K S ) K

Deriving c2

c2 x y z = ( x z ) y

Note that for the derivation of c2 we can use c1 combinator directly.

c2 x y = A ( ( x z ) y , z ) = S A ( x z , z ) A ( y , z ) = S ( c1 x A ( z , z ) ) ( K y ) = S ( c1 x I ) ( K y )

c2 x = A ( S ( c1 x I ) ( K y ) , y ) = S A ( S ( c1 x I ) , y ) A ( K y , y ) = S ( K ( S ( c1 x I ) ) ( c1 K A ( y , y ) ) = S ( K ( S ( c1 x I ) ) ( c1 K I )

c2 = A ( S ( K ( S ( c1 x I ) ) ) ( c1 K I ) , x ) = S A ( S ( K ( S ( c1 x I ) ) ) , x ) A ( c1 K I , x ) = S ( c1 S A ( K ( S ( c1 x I ) , x ) ) ( K ( c1 K I ) ) = S ( c1 S ( c1 K A ( S ( c1 x I ) , x ) ) ) ( K ( c1 K I ) ) = S ( c1 S ( c1 K ( c1 S A ( c1 x I , x ) ) ) ) ( K ( c1 K I ) ) = S ( c1 S ( c1 K ( c1 S ( S A ( c1 x , x ) A ( I , x ) ) ) ) ) ( K ( c1 K I ) ) = S ( c1 S ( c1 K ( c1 S ( S ( c1 c1 A ( x , x ) ) ( K I ) ) ) ) ) ( K ( c1 K I ) ) = S ( c1 S ( c1 K ( c1 S ( S ( c1 c1 I ) ( K I ) ) ) ) ) ( K ( c1 K I ) )

Think how long c2 would be if we didn't use the c1 combinator.

Let's again derive 'swap' but this time using the helpers

swap x y = y x

swap x = A ( y x , y ) = c2 A ( y , y ) x = c2 I x

swap = A ( c2 I x , x ) = c1 ( c2 I ) A ( x , x ) = c1 ( c2 I ) I

Great!! it's in a very short form thanks to c1 and c2.

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:

pair x y first = x

pair x y second = y

Remember how we use T and F to handle if-then-else above. We can choose:

first = T second = F

Then we can state:

pair x y z = z x y

Let's abstract out pair combinator now:

pair x y z = z x y

pair x y = A ( z x y , z ) = c2 A ( z x , z ) y = c2 ( c2 A ( z , z ) x ) y = c2 ( c2 I x ) y

pair x = A ( c2 ( c2 I x ) y , y ) = c1 ( c2 ( c2 I x ) ) A ( y , y ) = c1 ( c2 ( c2 I x ) ) I

pair = A ( c1 ( c2 ( c2 I x ) ) I , x ) = c2 A ( c1 ( c2 ( c2 I x ) ) , x ) I = c2 ( c1 c1 A ( c2 ( c2 I x ) , x ) ) I = c2 ( c1 c1 ( c1 c2 A ( c2 I x , x ) ) ) I = c2 ( c1 c1 ( c1 c2 ( c1 ( c2 I ) A ( x , x ) ) ) ) I = c2 ( c1 c1 ( c1 c2 ( c1 ( c2 I ) I ) ) ) I

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:

  • swap x

    can read as swap with x. You can give an argument function z and get the output function zx which is the opposite of as it was before (apply x to z)
  • pair B or

    pair of functions. You can input T to get function B or input F to get function or

Natural Numbers

Remember how we got the boolean true and false values. Boolean are actually encoded using S, K, and I. 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 n times to another as the natural number n. Let's find that combinator that applies it's first argument n times to its second argument as below:

n f x = f n ( x )
nxffffx.............

Note 0 f x = x when 0 = S K

0 f x = ( S K ) f x ( K x ) ( f x ) x

We can find a combinator succ (successive application) as below:

succ n f x = f ( n f x ) where succ = S ( S ( K S ) K )

Correctness:

succ n f x = S ( S ( K S ) K ) n f x ( S ( K S ) K f ) ( n f ) x ( K S f ) ( K f ) ( n f ) x S ( K f ) ( n f ) x ( ( K f ) x ) ( ( n f ) x ) f ( n f x )

Therefore:

succ 0 f x = f ( 0 f x ) = f ( x )

We can define one as:

one = succ 0

one f x = f ( x )

Now apply succ to onefx:

succ one f x = f ( one f x ) = f ( f ( x ) )

So we can write:

two = succ one

Just to be clear, once again let's apply succ to twofx:

succ two f x = f ( two f x ) = f ( f ( f ( x ) ) )

So we can write:

three = succ two

three f x = f ( f ( f ( x ) ) )

Now it's clear that we can express n th natural numbers in the form of:

n = succ n ( 0 )
succSKsuccsuccsucc

Nutual numbers in SKI Calculus have built-in iteration as we see above.

Addition and Multiplication

Now we can think about addition using succ and nfx:

add x y = x succ y

Most importantly x and y are any natural numbers we derive above. We can read the right hand side like apply succ combinator x times to y. We are adding 1 at a time to y, x many times to get (x+y) encoded in S, K and I. Great, now we can abstract out add as a combinator:

add x y = x succ y

add x = A ( x succ y , y ) = c1 ( x succ ) A ( y , y ) = c1 ( x succ ) I

add = A ( c1 ( x succ ) I , x ) = c2 A ( c1 ( x succ ) , x ) I = c2 ( c1 c1 A ( x succ , x ) ) I = c2 ( c1 c1 ( c2 A ( x , x ) succ ) ) I = c2 ( c1 c1 ( c2 I succ ) ) I

Similarly using the application of nfx, muliplication can be expressed in terms of addition as below:

mul x y = x ( add y ) 0

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 mul and add combinators shown above.

We can express (3x4)+5 in SKI calculus as below:

1 ( + 5 ) ( 3 ( + 4 ) 0 ) 1 ( + 5 ) 12 17
+510+43nfx112+5nfx=+510+4+4x+4fff12+5fx17 +514+4+4+518+4

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!


Created by potrace 1.16, written by Peter Selinger 2001-2019 © 2024 Developer Diary.

Made withusing Gatsby, served to your browser from a home grown Raspberry Pi cluster.
contact-me@developerdiary.me