SKIing with Y*, Iota and Ackermann

(Source code for this post is here: https://github.com/mikebern/lambda_ski_iota )

There are only six atomic operations for Turing machines – read and write to the tape, move the tape left or right one square,  change state based on the observed symbol and halt. Yet, it’s not hard to see, at least at a high level, how a program in an imperative language such as C or Fortran would be translated to a program for a Turing machine – variables are cells on the tape, operations are modifications of those cells and control structures move the tape according to the specified conditions.  This connection becomes much less obvious for functional programming languages such as Lisp or Haskell, and indeed they are based on another computation paradigm – lambda calculus.

Lambda calculus actually predated Turing machines. The first paper on the former was published in 1932, while on the latter in 1937.  It is deemed impossible to directly compare their computation powers, but Church-Turing thesis postulates that they are able to compute exactly the same class of functions, called computable functions.  Both lambda calculus and Turing machines had inspired creation of high-level programming languages, the first being Fortran followed by Lisp with a gap between the two of less than a year.

So the question arises – what is the ‘assembly language’ for the functional languages? The answer is quite surprising – using only 3 combinators – S, K, I we can express any lambda function. This system is called SKI-calculus . Sometimes it is written as SK(I) or to emphasize that I can be easily expressed using S and K (I =(S K K)). Can we do better than 2 combinators?  Yes! All three can be expressed with only one function called X! There are actually quite a few versions of X. The one that we use here has its own name – Iota (see Wikipedia). For other versions see Fokker, The systematic construction of a one-combinator basis, there is also Hankin X combinator, described in his book Lambda Calculi, A Guide for Computer Scientists on p. 61.

It follows that all algorithms can be written using just X and parentheses. For instance, Quick Sort in SKI calculus

and Sieve of Eratosthenes in X calculus.

The focus of this post is to introduce a tool (written in Clojure) that lets you play with SKI and X encodings. The inspiration for me to write this entry was this post λ-исчисление и LISP (in Russian), which showed how to encode Boolean logic, Church numerals and arithmetic operations on them, Y combinator and a few very common functions such as map, reduce and filter in pure lambda calculus. The translator then can translate all these functions and the functions that use them into SKI and X  expressions.

The main challenges to overcome were dealing with the variable arity of lambda functions, which is not straightforward to deal with in Clojure, and more importantly making Clojure “lazier” to make sure that we can implement Y combinator and the functions that are using it. It was also interesting to implement a lesser known variant  of Y combinator for mutually recursive functions, called Y* and obtain its translation. Finally, it was interesting to implement map and filter by just using reduce (fold) functions. While not terribly surprising, it means that we only need Y combinator for fold – map and filter can use Y indirectly by relying on fold in their implementation.

Why do we need our own numbers, arithmetic and logic operations? We cannot use any build-in numbers or arithmetic operators because we want everything to be expressed using just combinators. One of the possibilities is to use Church encoding, which is what we are using in this post. For example,  the expression 7*7-7 has this representation in SKI:
(((S (S (K S) (S (K (S (K S))) (S (K (S (K (S (K S))))) (S (K (S (K (S (K K))))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (K (S (S I (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I)))) (S (K (S (K K))) (S (K (S I)) (S (K K) I))))))))) (K (K (S (K K) I)))))) (K (K (K I))))) I))) (K I))))) (K (K I))))))) (S (K K) I))))) (K (K I))))))) (K (K (K I)))) (((S (S (K S) (S (K (S (K S))) (S (K (S (K (S (K S))))) (S (K (S (K (S (K K))))) (S (S (K S) (S (K K) (S (K S) (S (K K) I)))) (K (S (S (K S) (S (K K) I)) (K I)))))))) (K (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) (K I))))))))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) (K I)))))))))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) (K I)))))))))

The X version of the same is lengthier: 42 in X

 As you can see the representations are very verbose, partly by the nature of encodings, partly by the fact that no optimizations were done in the translator. The code above is actually a valid Clojure code, and can be executed. Below I describe the necessary scaffolding to make that happen.

Project layout

This is a leiningen project consisting of four source files and a couple of test files. The source files are listed below in order of dependencies between them.

1. combinator_definitions.clj – contains definitions of all combinators and supporting functions.
2. lambda_to_ski_translator.clj – this file contains the source code for the translator.
3. ski_encoding.clj – contains definitions of functions and their translations to SKI calculus.
4. iota_encoding.clj – contains code to translate from SKI calculus to X and also contains a few examples.

Executing iota_encoding.clj will pull dependencies and execute the code from all other source files. The code was developed in LightTable.

I wanted to write a simple self-contained system, which is easy to understand and modify, so translations produced are far from optimal, but the code is quite compact and follows from the first principles. There are other related projects, notably, unlambda, LazyK, and pointfree package of Haskell (used by the LamdaBot).

Working with Variadic Functions

First, we need to get around the fact that a function application in Clojure would throw an ArityException if we don’t supply the exact number of arguments that the function expects:

(defn fun1 [x] x)
(fun1) ; throws ArityException - too few parameters
(fun1 fun1 fun1) ; throws ArityException - too many parameters

In contrast, λx.x and (λx.x) (λy.y) (λz.z) are both well-formed lambda expressions and evaluate to λx.x and λz.z respectively. The first expression expects one argument, but gets none, while in the second expression, (λx.x) expects one argument but gets two – (λy.y) and (λz.z) (so it consumes the first one, returns a function, which, in turn, consumes the the second argument, returning another function).

To resolve this difficulty we will use variadize function defined in combinator_definitions.clj. Below is given the strict variant of this function – it works well for arithmetics and boolean logic but is not “lazy enough” to work for Y and Y* combinators. Modifications to cover these fixed-point combinators are given below.

(defn variadize-strict
  ([fnct] (variadize-strict fnct (arg-count fnct)))
  ([fnct num-args]
   (if (zero?  num-args) (fnct)
       (fn [& args]
         (cond
           (> (count args) num-args) (apply (apply fnct (take num-args args)) (drop num-args args))
           (= (count args) num-args) (apply fnct args)
           :else (variadize-strict (reduce partial fnct args) (- num-args (count args))))))))

The function takes the function to be “variadized” and the number of arguments it expects. If that number is not provided, it’s determined using Java reflection by arg-count function. The function returned by variadize-strict keeps track of the argument it had been supplied with at the moment of the call. If this number is less than the expected number, we use partial application (curring), it it’s exactly the expected number then we simply apply the variadized-strict to the arguments, and if there more arguments than the function is expecting, then we apply the function to the number of arguments it expects and the remaining arguments are supplied to the result of the that application. Please see unit-tests in combinator_definitions_test.clj  for examples.

Since we have only four basic combinators that we are working with – S, K, I, and X, it’s straightforward to variadize all of them. For instance, here is how we are defining S:

(defn S-def [f g x] (f x (g x))) (def S (variadize S-def))

Note that implementation of the same functionality just by using multi-arity and variadic functions in Clojure is not straightforward, and will likely to result in more convoluted code.

A note on SKI combinatorial calculus

Here are definitions of S, K, and I (see SKI combinator calculus):

• I x = x
• K x y = x
• S x y z = x z (y z)

When I looked at the definitions for the first time they didn’t make much sense to me – why these arbitrary functions were chosen as a basis, and why is it complete? In fact, choosing these functions for the basis makes a perfect sense and it can be shown by just a couple of examples. S is the most complicated one, so let’s start with it. This combinator captures the case of ‘function application’ – when we apply a function x to its single argument y, and, in addition, both x and y depend on the same value z. We don’t have to worry about applying a function to several arguments because that can be taken care of by currying.

Consider (a bit contrived) example of a function that doubles it’s argument:  λz.(λv. sum z v) (λy.y z) :  z is the argument to be doubled and sum is a function that just adds its two arguments.  Can we use S to express this function? Yes, it’s quite trivial – x (in the definition of S) is (λv. sum z v),  y is (λy.y z), which obviously evaluates to z (it’s in this overcomplicated form just to illustrate the point that both x and y depend on z), and z is z. Temporarily adding sum to our set of basic combinators, we see that our function is translated to (S sum I):

(defn sum-def [x y] (+ (get-val x) (get-val y)))
(def sum (variadize sum-def))
(def SKI-Double (S sum I))
((SKI-Double 10)) ; 20

The purpose of variadize was explained above, ignore for the moment get-val and the extra pair of parentheses in the last line (they will be explained later). The last line outputs the expected result – ’20’.

Let’s use the translator on the same function:

(translate-lambda-to-ski 'SKI-Double-Translated (template (fn [z#] ((fn [v#] (sum z# v#)) ((fn [y#] y#) z#)))))
((SKI-Double-Translated 10)) ; apply translated function to 10
(get @ski-translations 'SKI-Double-Translated) ; extract SKI-expression
(((S (S (S (K S) (S (K K) (S (K sum) I))) (K I)) (S (K I) I)) 10)); apply SKI-expression to 10

Function translate-lambda-to-ski from lambda_to_ski_translator.clj translates the given lambda function to SKI-calculus and instantiates the translation under the name given as the first parameter, in this case SKI-Double-Translated.

To see the actual translation, we can use get on ski-translations atom, and we can actually run it directly to get the same result. Note though, that translator produces an expression that is larger than the optimal one, which we obtained before.

Let’s see why do we need K. Suppose now that function x does not depend on z, and only y depends on z. For instance, instead of sum we now use add5 – a function that adds ‘5’ to its argument:

(defn add5-def [x] (sum 5 (get-val x)))
(def add5 (variadize add5-def))
(def SKI-Add5 (S (K add5) I))
((SKI-Add5 10)) ; 15

Now add5 does not need z – so we need to discard it, and K does it for us as shown. We can also apply our translator again and get a longer translation, but with the same result:

(translate-lambda-to-ski 'SKI-Add5-Translated (template (fn [z#] ((fn [v#] (add5 v#)) ((fn [y#] y# ) z#)))))
((SKI-Add5-Translated 10))
(get @ski-translations 'SKI-Add5-Translated)
(((S (K (S (K add5) I)) (S (K I) I)) 10)) ; 15

SKI Translator

Our translator follows the simple rules given in Wikipedia. Its source code is in lambda_to_ski_translator.clj and comments there explain how it works.

Here is another example of how to use  translator:

; One of possible implementations of 'Minus' in SKI calculus
(translate-lambda-to-ski 'SKI-Minus2 (template (fn [m# n#] ((n# SKI-Pred) m#))))

It produces output:

(S (K (S (S I (K (S (S (K S) (S (K (S (K S))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I)))) (S (K (S (K K))) (S (K (S I)) (S (K K) I))))))))) (K (K (S (K K) I)))))) (K (K (K I)))))))) (S (K K) I))

And ‘def’s this expression under name Ski-Minus2, so we can call it like this:

; 5 - 3
(to-int (SKI-Minus2 SKI-Five SKI-Three))

There are many more examples with the translator in ski_encoding.clj.

A few implementation notes:

• The name (SKI-Minus2) has to start with the prefix ‘SKI-‘, this is because X translator will later take ‘SKI-Minus2’ translation and will generate X-Minus2 function that only uses X combinator.  Translation to X versions will be done for all functions stored in ski-translations atom.
• Before translation translate-lambda-to-ski will expand all previously translated functions to their definitions (recursively). In our example, SKI-Pred will be replaced by its (source) definition. You can see the definition to be translated by running:

  (get @expanded-sources 'SKI-Minus2)
  

• It also stores the source of the function (as given) in the atom sources and the translation in the atom ski-translations:

  (get @sources 'SKI-Minus2)
  (get @ski-translations 'SKI-Minus2)
  

• template keyword is defined in backtick library. Its effect is similar to ‘ but in addition it also supports gensym. This is essential for the translator – when we are expanding of names, we want to make sure that there are no variable name collisions – the translator does not handle variable shading. For the same reason, it is also required that the variable names are not reused in the function definition, but that is fairly easy to ensure. For instance, the definition  (fn [x#]  ((fn [x#] x#) x#) should be changed to (fn [x#]  ((fn [y#] y#) x#) .

Church encoding

In order to use only S, K, I and X combinators our system should be self-contained – we cannot use Clojure numbers or lists as they obviously cannot be represented in terms of the combinators. So we use Church encoding to introduce our own booleans, numbers, lists and functions on them – all defined as functions in lambda calculus and then translated to SKI and X encodings. The implementation contains a subset of arithmetic and Boolean functions and only supports natural numbers. For lists, we use “Two pairs as a list node”.

To extract the values from the Church primitives use:

• for booleans:

  (to-bool (SKI-Or SKI-True SKI-False)) ; true
  

• for numbers:

  (to-int (SKI-Minus SKI-Two SKI-Two)) ; 0
  

• for lists of integers:

  (to-int-list (X-Cons X-One (X-Cons X-Two (X-Cons X-Three X-Nil)))) ; (1,2,3)
  

All these functions are defined in ski_encoding.clj .

Making Clojure lazy

So we can do some arithmetic and logic computations completely in SKI, but how do we do recursive calculations? Obviously, we cannot just call a function from its body because its name is not one of S, K, I, or X. To make recursion possible we will abstract recursion by using Y combinator and then translate it to SKI-calculus.  Y and its derivation is well explained in this post.

It is not hard to find a working implementation of Y in Clojure. Let look at the example from Deriving the Y-combinator in Clojure :

(defn Y [f] ((fn [g] (g g)) (fn [h] (fn [n] ((f (h h)) n)))))
(def fact-maker (fn [g] (fn [n] (if (= 0 n) 1 (* n (g (- n 1)))))))
((Y fact-maker) 5) ; 120

Everything is swell. But here is a bit of problem if we are working with Church arithmetics. There if  is not the Clojure if, but a user defined function, and as such it does not have the ‘magic’ of the Clojure if, which evaluates only true- or false-branches based on the condition. This is equivalent to replacing if with my-if:

(defn Y [f] ((fn [g] (g g)) (fn [h] (fn [n] ((f (h h)) n)))))
(defn my-if [cond a b] (if cond a b))
(def fact-maker (fn [g] (fn [n] (my-if (= 0 n) 1 (* n (g (- n 1)))))))
((Y fact-maker) 5) ; StackOverflowError!

And we get an exception – Clojure is a strict language. We can get around by modifying fact-maker by wrapping if branches in anonymous functions.  We call the modified function fact-maker2:

(defn Y [f] ((fn [g] (g g)) (fn [h] (fn [n] ((f (h h)) n)))))
(defn my-if [cond a b] (if cond a b))
(def fact-maker2 (fn [g]
 (fn [n] ((my-if (= 0 n) (fn [] 1) (fn [] (* n (g (- n 1)))))))))
((Y fact-maker2) 5) ; again 120

This uses a standard trick to introduce laziness – wrap an expression into an anonymous function to delay its computation. But what do we do for SKI-calculus?  There is no way to use an anonymous function in an SKI-expression! A solution that I use is to push laziness to the combinator level, i.e. making S, K, I and X lazy. It has two main ingredients:

1. Use delay and force functions of Clojure. When a combinator gets it arguments it wraps it with delay and uses force to get the result at the moment when the result of computation is needed. The “delay” is achieved with the variadize function from ski_encoding.clj, which is used in the definitions of all combinators as shown above.

   (defn variadize
     ([fnct] (variadize fnct (arg-count fnct)))
     ([fnct num-args]
      (if (zero?  num-args) (DelayedEval. (delay (fnct)))
          (fn [& args]
            (cond
              (> (count args) num-args)
              (DelayedEval. (delay (apply (apply fnct (take num-args args)) (drop num-args args))))
              (= (count args) num-args) (DelayedEval. (delay (apply fnct args)))
              :else (variadize (reduce partial fnct args) (- num-args (count args))))))))
   

2. The above works well, except for the fact that we need to call force before each application, i.e. (force S (force K …) …), otherwise we would get an exception as we are dealing with delayed computations and not functions. To resolve this problem, we have DelayedEval record which inherits from clojure.lang.IFn, and overrides its invoke and applyTo methods, so that these methods call force when called, thus making use of “force” transparent.  DelayedEval is generated using macros to avoid copy-pasting methods that differ only in the number of arguments (inspired by link), but the end result is similar to this:

   (defrecord DelayedEval [delayed-exp]
     clojure.lang.IFn
     (invoke [this] (let [exp (force delayed-exp)] (if (instance? DelayedEval exp) (exp) exp)))
   
     (invoke [this arg] ((force delayed-exp) arg))
     (invoke [this arg arg2] ((force delayed-exp) arg arg2))
     (invoke [this arg arg2 arg3] ((force delayed-exp) arg arg2 arg3))
     (invoke [this arg arg2 arg3 arg4] ((force delayed-exp) arg arg2 arg3 arg4))
     (applyTo [this args] (apply (force delayed-exp) args)));
   

3. At some point we need to extract the actual result.  We do that with an extra pair of parentheses. This works  because we defined invoke[this] in DelayedEval to recursively evalute itself, until we get an expression which is not DelayedEval. For instance, we use it in to-int function in ski_encoding.clj:

   (defn to-int [ski-int-expr] ((ski-int-expr ski-plus-one 0)))
   

   Another place we use the same trick is get-val function in combinator_definitions.clj:

   (defn get-val [delayed-val] (if (instance? DelayedEval delayed-val) (delayed-val) delayed-val))
   

   This function is needed when we do conversions from Church encoded numbers to regular numbers. Given a DelayedEval expression we evaluate it recursively to get a value that we can use in a regular arithmetic operation.

Combination of variadize and DelayedEval makes it possible to get a working translation of Y to SKI-calculus.

Y combinator

The tool produces this
SKI translation of Y

It is not compact as Y = (S (K (S I I)) (S (S (K S) K) (K (S I I))))) from Wikipedia, but results are the same. In the code the Wikipedia version is defined as Y-Wiki.

With Y and Y-Wiki combinators working we can get SKI and X translations of a few interesting functions (ski_encoding.clj):

Factorial

(translate-lambda-to-ski 'SKI-Fact-Maker (template (fn [g#]
                                                     (fn [n#] (SKI-If (SKI-Eq?  SKI-Zero n#) SKI-One (SKI-Mul n# (g# (SKI-Minus n# SKI-One))))))))

(translate-lambda-to-ski 'SKI-Fact '(SKI-Y SKI-Fact-Maker))
(to-int (SKI-Fact SKI-Five)); 125

McCarthy 91 function

McCarthy 91 is a curious recursive function that  evaluates to 91 for all natural numbers n ≤ 100, and to n − 10 for n > 100:

(translate-lambda-to-ski 'SKI-McCarthy-Maker (template (fn [f#]
                                                         (fn [n#] (SKI-If (SKI-Leq? n# SKI-Hundred) (f# (f# (SKI-Plus n# SKI-Eleven))) (SKI-Minus n# SKI-Ten))))))

(translate-lambda-to-ski 'SKI-McCarthy '(SKI-Y SKI-McCarthy-Maker))
(to-int (SKI-McCarthy SKI-Eleven)); 91

List functions

As mentioned above, we have an implementation of lists, which combined with Y gives us all essential functions to work with lists

translate-lambda-to-ski 'SKI-Map (template (fn [f# l#]
                                              ((SKI-Y
                                                (fn [r#]
                                                  (fn [m#]
                                                    (SKI-If (SKI-Nil? m#) SKI-Nil
                                                            (SKI-Cons (f# (SKI-Head m#)) (r# (SKI-Tail m#))))))) l#))))

(translate-lambda-to-ski 'SKI-Filter (template (fn [f# l#]
                                                 ((SKI-Y
                                                   (fn [r#]
                                                     (fn [m#]
                                                       (SKI-If (SKI-Nil? m#) SKI-Nil
                                                               (SKI-If (f# (SKI-Head m#))
                                                                       (SKI-Cons (SKI-Head m#) (r# (SKI-Tail m#)))
                                                                       (r# (SKI-Tail m#))))))) l#))))

;fold right
(translate-lambda-to-ski 'SKI-Reduce (template (fn [f# z# l#]
                                                 ((SKI-Y
                                                   (fn [r#]
                                                     (fn [m#]
                                                       (SKI-If (SKI-Nil? m#) z#
                                                               (f# (SKI-Head m#) (r# (SKI-Tail m#))))))) l#))))

;fold left
(translate-lambda-to-ski 'SKI-ReduceL (template (fn [f# z# l#]
                                                  ((SKI-Y
                                                    (fn [r#]
                                                      (fn [m# a#]
                                                        (SKI-If (SKI-Nil? m#) a#
                                                                (r#  (SKI-Tail m#) (f# (SKI-Head m#) a#)))))) l# z#))))

SKI-Reduce is an implementation of fold-right. In fact, as shown in the code, it is enough to have SKI-Reduce, to implement map, filter,
length, and concat functions. We can even implement fold-left using SKI-Reduce:

(translate-lambda-to-ski 'SKI-ReduceL2 (template (fn [f# z# l#] (SKI-Reduce (fn [b# g# a#] (g# (f# a# b#))) I l# z#))))

Ackermann function

Ackermann function is defined as:

Note, that the function is recursive in two parameters, while Y supports only one. But since we have lists, we can overcome this by packing m and n into two element list when we need to pass them as a single argument, and unpack them when we need to have access to their values (see implementation in ski_encoding.clj).

Quick Sort and Sieve of Eratosthenes

Having lists, Y, and SKI-Filter we can build some interesting algorithms on lists. ski_encoding.clj contains implementations for Quick Sort and Sieve of Eratosthenes. For Sieve of Eratosthenes we also need SKI-Mod m n, which computes the remainder of m/n. It’s implemented as a recursive function of two arguments and uses the same trick of packing the two arguments into a list as in the implementation of Ackermann function.

Y*

Our last example is an implementation of Y*, which is a fix point combinator for mutually recursive functions. It’s a modified version of Y* combinator found here. The classic even? and odd? functions are implemented. We pack two “maker” functions into a list, pass the list to Y* to find the common fix-point of these functions, which is a again a list of two functions – the first function is even? and the second function is odd?.

Another example where we use Y* is SKI-FunkyMap, which applies its function only to odd elements in the list (indexed from 0).

X Translator

Translation to X is quite simple. We take all functions that were translated by SKI Translator, and replace each of S, K, I by its representation in X. The names of functions are modified by replacing the prefix “SKI” to the prefix “X”, i.e. function SKI-Cons becomes X-Cons.  The code is in iota_encoding.clj, and the mapping rules are the following:

1. S becomes (X (X (X (X X))))
2. K becomes (X (X (X X)))
3. I becomes (X X)

The same approach, of course, can be used for other complete bases for Lambda calculus, for instance, B, C, K, W system. But obviously, a direct translation would be much more efficient.

We can run X programs and get their sources the same way as we do for SKI programs:

(to-int (X-Ackermann (X-Cons X-Three (X-Cons X-Three X-Nil))))
(get iota-translations 'X-Ackermann)

Note though, that iota-translations is a regular map and not an atom as in the case of ski-translations.

Interesting topics

• It would be interesting to add support for signed integers. Currently all examples use the natural numbers only.
• Joy  is a stack based programming language,  such languages also have their systems of (concatenative) combinators.  Look here for an interesting discussion and implementation.
• For derivation of X, take a look at this paper: Fokker, The systematic construction of a one-combinator basis. It contains a derivation of X, as well as, a number of other complete bases for lambda calculus. It’s quite simple to modify the code to use any of these other bases.