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, +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:

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:

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

rule of k: ``kxy ⇒ x

rule of s: ```sxyz ⇒ ``xz`yz

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

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

split lemma: there
exists some pair (e, f) such that `ef => v

reversible lemma: the
axioms and transformation rules are reversible

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

Works Consulted

[Davie]	An Introduction to Functional Programming Systems Using Haskell, by A.J.T. Davie, Cambridge University Press, NY, 1992.
[Smullyan]	To Mock a Mockingbird and other logic puzzles, by Raymond Smullyan, Alfred A. Knopf, NY, 1985.

Typed Logic

Pages

Tuesday, April 26, 2005