# Meditations on the Void

## Implementing Unlambda's "v" function in SKI

### 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,`

, and the symbol

+Argument, -Result)`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 => xwhere 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:

Number of Applications | `v` equivalent | |

1 | x = ``k`kk` | |

2 | x = ``k`k`kk` | |

3 | x = ``k`k`k`kk` | |

... | ||

N | x = ((N + 1) * "``k` ")`k` |

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:

- 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) - lacks generality (Unlambda machines do not implement
`v`

this

way) - 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) - 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:

`<x> ⇒`

```s`kki````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`k`

x``k`

y 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```Yk`

x ⇒```k`Yk`

x ⇒``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:

[Davie] also shows some transformation rules;

we will use one transformation rule in this system:

**xy**:```s`k`

x``k`

y ⇒``k``

xy

With these axioms and transformation rules we will find `v`

, which is

defined as:

**definition of v**:``v`

x =>`v`

To keep the proof concise we will introduce some lemmas, without proof

(these proofs are left as an exercise to the thorough reader):

**split lemma**: there

exists some pair (e, f) such that `ef =>`v`

**reversible lemma**: the

axioms and transformation rules are reversible**referential transparency**: any functions that have the same results from the

lemma

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. ``v`

x⇒ `v`

by v

definition2. `v`

⇒ ``kv`

by the

reversed rule of k3. ``kv`

⇒ ``k``

efby the

split lemmma4. ``k``

ef⇒ ```s`k`

e``k`

fby reverse xy hypothesis-4. (e, f) = (v, v) Given ``vv`

=`v`

from the

v definitionprelude-5. ```ksv`

⇒ `s`

by the

rule of k5. ```s`k`

e``k`

f⇒ `````ksv`k`

e``k`

f

(pre-5)

⇒`````ksv`kv`kv`

(hyp-4)from the referential transparency

lemma6. `````ksv`kv`kv`

⇒ `````s`kskv`kv`

by the

reversed rule of s7. `````s`kskv`kv`

⇒ ````s``s`kskkv`

by the

reversed rule of s8. ````s``s`kskkv`

⇒ ````s``s`kskk``s``s`kskk`

=`v`

by

hyp-4Q.E.D.

From the above derivation we have `v`

as ````s``s`kskk``s``s`kskk`

, now we

must show that ``v`

x = `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 ``v`

x 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).

## Works Consulted

[Davie] | An Introduction to Functional Programming Systems Using, by A.J.T. Davie, Cambridge University Press, NY, 1992.Haskell |

[Smullyan] | To Mock a Mockingbird and other logic puzzles, by Raymond Smullyan, Alfred A. Knopf, NY, 1985. |

Copyright © 2004, 2005, Cotillion Group, Inc. All rights reserved.

author: Douglas M. Auclair (dauclair.at.hotmail.dot.com)