Meditations on the Void

Raison d'Etre

Unlambda is an eager implementation of a programming language based on the S, K, and I combinators from Combinatory logic. This, in itself, has generated quite a bit of interest, but Unlambda also has some novel features: instead of implicit function application (ordered by nesting parenthetical expressions), it has an explicit apply operator, it has also added some functors that fall outside combinatory logic, such as the print operators (reminiscent of Forth's dot operator, and subject to an extensive analysis in the Zot section of the Iota and Jot simplest languages site), call with current continuation operator (c), the promise operator (d for "delay"), and the void operator (v) which consumes the argument and returns itself as the function result.

The v operator poses an interesting problem. Implementing it as a primitive is simple enough, for example, a simple Prolog evaluator would implement it as follows:

apply(v0, _Arg, v0)

where apply/3's prototype is apply(+Functor, +Argument, -Result), and the symbol v0 represents the evaluated v combinator.

which is also just as simply represented in the λ-calculus as: v = λx.v. But the λ-calculus requires all symbols be defined appropriately (in this case, a symbol must be a λ variable and in the lexical scope of its enclosing λ-term). Here, v is a name outside the calculus; in order to use the symbol v inside a λ-term it must first be defined in a λ-expression. This begs the question, though: what is the appropriate λ-term to define v? We will discuss this as we develop the solution throughout this paper.

So, it is a simple task to implement v as a primitive for use by an Unlambda machine. However, a programming language using only S, K, and I is Turing-complete (see the Wikipedia entry for the proof), so it is possible to implement v using the simpler s, k, and i combinators of Unlambda. Since several Unlambda implementations have implemented v using this approach, the aim of this paper is not to discover the solution (as it is already known), instead, this paper explores the process by which this solution is found, and, more generally, it explores the discipline to solve any given computable problem using the S, K, and I combinators.

False Starts

Trial 1: v as infinite k

In my first attempt at implementing v I took the most direct path: v consumes its argument and returns itself. Examining the S, K, and I functors I observed that K consumes the second argument, or put another way, K composed with its first argument consumes the second argument and returns the first.

This observation seemed promising, so I followed it up with some tests. The question for

v = ``k x arg

is what (composed) function should the x argument represent (besides v, as we are using only S, K, and I to represent v)? Viewed inductively, the question shows us that

``k x arg => x

where the x argument must perform the same task (consume the argument and return a function that consumes its argument)

If the new function x is used only once, a working candidate is simply `kk! This candidate does have an unfortunate side-effect: when applied to an argument, it returns k, and not a v-equivalent. To rectify this, we add one more k composition x = `k`kk, so that when this function is used (only once!) it returns a v semi-equivalent (that is not to be used).

For a known number of applications, this approach is workable:

So, one could follow the philosophy of "I will use v at most N times, so my v function is `k`k`k`k`k`k`k`k...`kk", which is a philosophy that has very few supporters (but, unfortunately, too many practitioners) in the Computer Science community. There are many good reasons to frown upon this programming style; the first four that come to mind are:

1. inability to handle unknowns -- for example, if v is returned from an SKI expression, the returned function has no way of knowing how many times it will be applied (and therefore will likely return an incorrect v representation)
2. lacks generality (Unlambda machines do not implement v this way)
3. brittleness: each v is tied to a specific implementation (a change in the expression elsewhere (using v more than expected) requires changing each v representation)
4. inefficient: if v is used less than expected, we have wasted time composing extra k combinators and wasted space in carrying around those unused k combinators.

So this approach in static situations has the singular advantage that it works and is easy to implement, but otherwise it is unacceptable generally.

Trial 2: a λ-calculus representation...

The λ-calculus, like the SKI combinators, can express any computable expression, and, as it allows variables, offers a different perspective on this problem. I set out to define an appropriate λ-term representing v. Once that was done, I needed only to follow the translation rules and simplification rules explained in [Davie], pp. 155-6, and on the Unlambda site.

My first attempt was to use the λ-term "λv.λ.x.v"; this neatly provides a definition for v as well as provides what it does: consumes the argument and returns the consumer function.

Translating that λ-term into combinators posed some problems:

λv.(λx.v) ⇒ λv.(K v) ⇒ S(λv.K)(λv.v) ⇒ S(K K)I

This is all very simple but entirely misses the point, for:

```s`kki<x> ⇒ ```kk<x>`i<x> ⇒ `k<x>

The issue here is that v is being treated as a constant (not as a constant function), so the result is to return the constant function (K), and not v (one of the reduction rules is S(Kx)I reduces to x).

...with the Y combinator

The problem with the above formulation (v as a λ-term) is that v was made an argument to the λ-term, but it was never determined what value v was to take during application. Obviously, v must be itself. As λ-terms do not refer to themselves directly, the "fixed-point" methodology has been developed to allow for indirect self-reference of λ-terms. The Y-combinator represents the fixed-point of a function, so that it may be passed as a parameter to another function (that is a generalization of the fixed-point) and called -- this is the usual method to represent recursion in the λ-calculus.

The Y-combinator has the interesting property of (Y H) = H (Y H) where H represents the fixed-point function. This property allows the function "to call itself". The most common example given is the recursive definition of factorial in the λ-calculus:

factorial = λfac.λx.(x = 0) -> 1 ; x * (fac (x - 1))

(Y factorial)	= factorial (Y factorial)
	= (λfac.λx.(x = 0) -> 1 ; x * (fac (x - 1))) (Y factorial)
	= (λx.(x = 0) -> 1 ; x * ((Y factorial) (x - 1)))

Given the (positive) value for x, (Y factorial) eventually reduces to the number 0, and in this way the λ-calculus avails itself to recursion.

Using the Y-combinator, the function v becomes:

fnv = λv.λx.v

(Y fnv)	= fnv (Y fnv)
	= (λv.λx.v)(Y fnv)
	= λx.(Y fnv)

From this result, we use the combinatory transformation rules (given that we know fnv = k, and various sources show the Y-combinator is ((SS)K)((S(K((SS)(S((SS)K)))))K) or ``s``s`k``ss`s``sskk`k``s`k``ss`s``sskk) to produce:

λx.(Y fnv)	=``s(λx.Y)(λx.k)
	= ``s`kY`kk (but note that ``s`kx`ky reduces to `k`xy)
	= `k`Yk (which by H (Y H) reduces to (Y H))
	= ```s``s`k``ss`s``sskk`k``s`k``ss`s``sskkk

Very nice! But are we done? No. `Yk has no termination (remember (Y H) = H (Y H) = H H (Y H) = ..., and unlike factorial, which has a termination test, v has no such test) ... it builds an infinite number of nested constant functions before it is ever applied to its argument:

``Yk<x>	= ``k`Yk<x>
	= ``k`k`Yk<x>
	= ``k`k`k`Yk<x>
	= ``k`k`k`k`Yk<x>
	...

Side note:

In a normal-ordered system, this would not pose a problem, as (Y H) would be evaluated only to the extent needed, so ``Ykx ⇒ ``k`Ykx ⇒ `Yk

So, using combinatory logic, I have just proved that v is infinite k (it is nice when my intuition matches closely with theory), and because Unlambda is applicatively-ordered, using the Y-combinator to construct v (or any recursively-defined supercombinator) is not feasible.

Proving "v" Logically

So far, our attempts to represent v as an Unlambda SKI expression have been stymied by infinite composition. However, we know that v is a simple function to implement as a primitive (i.e. it is "computable"), so it should have a computable (terminating) representation (as opposed to an infinite representation) as an SKI expression.

Indeed it does, but it takes more than simply following formula to obtain the terminating expression (correction, it is possible, but let us leave the Shakespearean infinite-monkey theory of computation aside). We must approach solving v as an SKI expression much like a mathematian solves a proof. First we will build the axioms of our system, then we will apply transformation rules to those axioms to reach our result (sometimes the application of the transformation rules will require a good deal of creativity to advance the proof).

The axioms of the eager SKI system that allows the v combinator are as follows:

1. rule of k: ``kxy ⇒ x
2. rule of s: ```sxyz ⇒ ``xz`yz

[Davie] also shows some transformation rules; we will use one transformation rule in this system:

1. xy: ``s`kx`ky ⇒ `k`xy

With these axioms and transformation rules we will find v, which is defined as:

• definition of v: `vx => v

To keep the proof concise we will introduce some lemmas, without proof (these proofs are left as an exercise to the thorough reader):

1. split lemma: there exists some pair (e, f) such that `ef => v
2. reversible lemma: the axioms and transformation rules are reversible
3. referential transparency lemma: any functions that have the same results from the same inputs are interchangeable

The proof starts with the definition, and substitutes v for some arguments, using the reasoning from trial 1 and trial 2 to obtain an SKI expression:

1.	`vx	⇒	v	by v definition
2.	v	⇒	`kv	by the reversed rule of k
3.	`kv	⇒	`k`ef	by the split lemmma
4.	`k`ef	⇒	``s`ke`kf	by reverse xy
hypothesis-4.	(e, f) = (v, v)			Given `vv = v from the v definition
prelude-5.	``ksv	⇒	s	by the rule of k
5.	``s`ke`kf	⇒	````ksv`ke`kf (pre-5)    ⇒ ````ksv`kv`kv (hyp-4)	from the referential transparency lemma
6.	````ksv`kv`kv	⇒	````s`kskv`kv	by the reversed rule of s
7.	````s`kskv`kv	⇒	```s``s`kskkv	by the reversed rule of s
8.	```s``s`kskkv	⇒	```s``s`kskk``s``s`kskk = v	by hyp-4
Q.E.D.

From the above derivation we have v as ```s``s`kskk``s``s`kskk, now we must show that `vx = v using the SKI expression for v. To do this we will use the SKI expression for the false boolean predicate (`ki) to test the integrity of the SKI expression for v (I considered i at first, but that choice may have unintended consequences of returning i's argument) using only the axioms and the transformation rule to transform `vx back into v:

`v`ki	≡	````s``s`kskk``s``s`kskk`ki	SKI substitution for v
	⇒	````s`ksk``s``s`kskk`k``s``s`ksk`ki	by the rule of s
	⇒	`````ks``s``s`kskk`k``s``s`kskk`k``s``s`kskk`ki	by the rule of s
	⇒	```s`k``s``s`kskk`k``s``s`kskk`ki	by the rule of k
	⇒	``k```s``s`kskk``s``s`kskk`ki	by the xy transform
	⇒	```s``s`kskk``s``s`kskk ≡ v	by the rule of k
Q.E.D.

Summary

The above proof shows that it is possible to express the v function with a terminating SKI expression. Programming in general is hard work, but Unlambda makes that work even harder with its applicative (vice normal) order and with its indirect form of abstraction.

These challenges, far from being stumbling blocks, provide an opportunity to examine problems in new ways and with renewed rigor. Not only can one (re)learn the foundations of computer science and the λ-calculus, but one can also apply these lessons to everyday problem solving tasks.

Programming in Unlambda is challenging, but it is also rewarding.

Epilogue

Smullyan takes a different approach to (first) proving that v exists and then deriving the combinators that represent v (the derived combinator is never given a symbolic representation in this work). Smullyan defines and proves properties of combinators and combinator expressions. He first defines and proves an egocentric property of a combinator (so that CC = C for an egocentric combinator) and then goes on to define an hopelessly egocentric property of some combinator (where Cx = C) and shows that composing other properties of some combinators will yield an hopelessly egocentric combinator expression. These discussions occur in his work, chapter 9, §2 and §9 (the definitions) and chapter 11, §3 and §4 (the derivations).