Understanding Computation (40 page)

This is an explicit reimplementation of the way that variables get
replaced inside the body of a lambda calculus function when it’s called.
Essentially,
#as_a_function_of
gives us
a way to use an SKI expression as the body of a function: it creates a new
expression that behaves just like a function with a particular body and
parameter name, even though the SKI calculus doesn’t have explicit syntax
for functions.

The ability of the SKI calculus to imitate the behavior of functions
makes it straightforward to translate lambda calculus expressions into SKI
expressions. Lambda calculus variables and calls become SKI calculus
symbols and calls, and each lambda calculus function has its body turned
into an SKI calculus “function” with
#as_a_function_of
:

class
LCVariable
def
to_ski
SKISymbol
.
new
(
name
)
end
end
class
LCCall
def
to_ski
SKICall
.
new
(
left
.
to_ski
,
right
.
to_ski
)
end
end
class
LCFunction
def
to_ski
body
.
to_ski
.
as_a_function_of
(
parameter
)
end
end

Let’s check this translation by converting the lambda calculus
representation of the number two (see
Numbers
) into the SKI calculus:

>>
two
=
LambdaCalculusParser
.
new
.
parse
(
'-> p { -> x { p[p[x]] } }'
)
.
to_ast
=> -> p { -> x { p[p[x]] } }
>>
two
.
to_ski
=> S[S[K[S]][S[K[K]][I]]][S[S[K[S]][S[K[K]][I]]][K[I]]]

Does the SKI calculus expression
S[S[K[S]][S[K[K]][I]]][S[S[K[S]][S[K[K]][I]]][K[I]]]
do the same thing as the lambda calculus expression
-> p { -> x { p[p[x]] } }
? Well, it’s
supposed to call its first argument twice on its second argument, so we
can try giving it some arguments to see whether it actually does that,
just like we did in
Semantics
:

>>
inc
,
zero
=
SKISymbol
.
new
(
:inc
),
SKISymbol
.
new
(
:zero
)
=> [inc, zero]
>>
expression
=
SKICall
.
new
(
SKICall
.
new
(
two
.
to_ski
,
inc
),
zero
)
=> S[S[K[S]][S[K[K]][I]]][S[S[K[S]][S[K[K]][I]]][K[I]]][inc][zero]
>>
while
expression
.
reducible?
puts
expression
expression
=
expression
.
reduce
end
;
puts
expression
S[S[K[S]][S[K[K]][I]]][S[S[K[S]][S[K[K]][I]]][K[I]]][inc][zero]
S[K[S]][S[K[K]][I]][inc][S[S[K[S]][S[K[K]][I]]][K[I]][inc]][zero]
K[S][inc][S[K[K]][I][inc]][S[S[K[S]][S[K[K]][I]]][K[I]][inc]][zero]
S[S[K[K]][I][inc]][S[S[K[S]][S[K[K]][I]]][K[I]][inc]][zero]
S[K[K][inc][I[inc]]][S[S[K[S]][S[K[K]][I]]][K[I]][inc]][zero]
S[K[I[inc]]][S[S[K[S]][S[K[K]][I]]][K[I]][inc]][zero]
S[K[inc]][S[S[K[S]][S[K[K]][I]]][K[I]][inc]][zero]
S[K[inc]][S[K[S]][S[K[K]][I]][inc][K[I][inc]]][zero]
S[K[inc]][K[S][inc][S[K[K]][I][inc]][K[I][inc]]][zero]
S[K[inc]][S[S[K[K]][I][inc]][K[I][inc]]][zero]
S[K[inc]][S[K[K][inc][I[inc]]][K[I][inc]]][zero]
S[K[inc]][S[K[I[inc]]][K[I][inc]]][zero]
S[K[inc]][S[K[inc]][K[I][inc]]][zero]
S[K[inc]][S[K[inc]][I]][zero]
K[inc][zero][S[K[inc]][I][zero]]
inc[S[K[inc]][I][zero]]
inc[K[inc][zero][I[zero]]]
inc[inc[I[zero]]]
inc[inc[zero]]
=> nil

Sure enough, calling the converted expression with symbols named
inc
and
zero
has evaluated to
inc[inc[zero]]
, which is exactly what we wanted.
The same translation works successfully for any other lambda calculus
expression, so the SKI combinator calculus can completely simulate the
lambda calculus, and therefore must be universal.

>>
identity
=
SKICall
.
new
(
SKICall
.
new
(
S
,
K
),
K
)
=> S[K][K]
>>
expression
=
SKICall
.
new
(
identity
,
x
)
=> S[K][K][x]
>>
while
expression
.
reducible?
puts
expression
expression
=
expression
.
reduce
end
;
puts
expression
S[K][K][x]
K[x][K[x]]
x
=> nil

The Greek letter iota (
ɩ
) is an extra combinator that
can be added to the SKI calculus. Here is its reduction rule: Reduce
ɩ[
a
]
to
a
[S][K]
.

Our implementation of the SKI calculus makes it easy to plug in a
new combinator:

IOTA
=
SKICombinator
.
new
(
'ɩ'
)
# reduce ɩ[
a
] to
a
[S][K]
def
IOTA
.
call
(
a
)
SKICall
.
new
(
SKICall
.
new
(
a
,
S
),
K
)
end
def
IOTA
.
callable?
(
*
arguments
)
arguments
.
length
==
1
end

Chris Barker proposed a language called
Iota
whose programs
only
use the
ɩ
combinator. Although
it only has one combinator, Iota is a universal language, because any SKI calculus expression
can be converted into it, and we’ve already seen that the SKI calculus is universal.

We can convert an SKI expression to Iota by applying these
substitution rules:

It’s easy to implement this conversion:

class
SKISymbol
def
to_iota
self
end
end
class
SKICall
def
to_iota
SKICall
.
new
(
left
.
to_iota
,
right
.
to_iota
)
end
end
def
S
.
to_iota
SKICall
.
new
(
IOTA
,
SKICall
.
new
(
IOTA
,
SKICall
.
new
(
IOTA
,
SKICall
.
new
(
IOTA
,
IOTA
))))
end
def
K
.
to_iota
SKICall
.
new
(
IOTA
,
SKICall
.
new
(
IOTA
,
SKICall
.
new
(
IOTA
,
IOTA
)))
end
def
I
.
to_iota
SKICall
.
new
(
IOTA
,
IOTA
)
end

It’s not at all obvious whether the Iota versions of the
S
,
K
, and
I
combinators are equivalent to the
originals, so let’s investigate by reducing each of them inside the SKI
calculus and observing their behavior. Here’s what happens when we
translate
S
into Iota and then reduce
it:

>>
expression
=
S
.
to_iota
=> ɩ[ɩ[ɩ[ɩ[ɩ]]]]
>>
while
expression
.
reducible?
puts
expression
expression
=
expression
.
reduce
end
;
puts
expression
ɩ[ɩ[ɩ[ɩ[ɩ]]]]
ɩ[ɩ[ɩ[ɩ[S][K]]]]
ɩ[ɩ[ɩ[S[S][K][K]]]]
ɩ[ɩ[ɩ[S[K][K[K]]]]]
ɩ[ɩ[S[K][K[K]][S][K]]]
ɩ[ɩ[K[S][K[K][S]][K]]]
ɩ[ɩ[K[S][K][K]]]
ɩ[ɩ[S[K]]]
ɩ[S[K][S][K]]
ɩ[K[K][S[K]]]
ɩ[K]
K[S][K]
S
=> nil

So yes,
ɩ[ɩ[ɩ[ɩ[ɩ]]]]
really is
equivalent to
S
. The same thing happens
with
K
:

>>
expression
=
K
.
to_iota
=> ɩ[ɩ[ɩ[ɩ]]]
>>
while
expression
.
reducible?
puts
expression
expression
=
expression
.
reduce
end
;
puts
expression
ɩ[ɩ[ɩ[ɩ]]]
ɩ[ɩ[ɩ[S][K]]]
ɩ[ɩ[S[S][K][K]]]
ɩ[ɩ[S[K][K[K]]]]
ɩ[S[K][K[K]][S][K]]
ɩ[K[S][K[K][S]][K]]
ɩ[K[S][K][K]]
ɩ[S[K]]
S[K][S][K]
K[K][S[K]]
K
=> nil

Things don’t work quite so neatly for
I
. The
ɩ
reduction rule only produces expressions containing the
S
and
K
combinators, so there’s no chance of ending up with a literal
I
:

>>
expression
=
I
.
to_iota
=> ɩ[ɩ]
>>
while
expression
.
reducible?
puts
expression
expression
=
expression
.
reduce
end
;
puts
expression
ɩ[ɩ]
ɩ[S][K]
S[S][K][K]
S[K][K[K]]
=> nil

Now,
S[K][K[K]]
is obviously not
syntactically
equal
to
I
, but it’s another example of an expression
that uses the
S
and
K
combinators to
do the same
thing
as
I
:

>>
identity
=
SKICall
.
new
(
SKICall
.
new
(
S
,
K
),
SKICall
.
new
(
K
,
K
))
=> S[K][K[K]]
>>
expression
=
SKICall
.
new
(
identity
,
x
)
=> S[K][K[K]][x]
>>
while
expression
.
reducible?
puts
expression
expression
=
expression
.
reduce
end
;
puts
expression
S[K][K[K]][x]
K[x][K[K][x]]
K[x][K]
x
=> nil

So the translation into Iota does preserve the individual
behavior
of all three SKI combinators, even though it
doesn’t quite preserve their syntax. We can test the overall effect by
converting a familiar lambda calculus expression into Iota via its SKI
calculus representation, then evaluating it to check how it
behaves:

>>
two
=> -> p { -> x { p[p[x]] } }
>>
two
.
to_ski
=> S[S[K[S]][S[K[K]][I]]][S[S[K[S]][S[K[K]][I]]][K[I]]]
>>
two
.
to_ski
.
to_iota
=> ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[
ɩ[ɩ[ɩ]]]]][ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]
]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ]]]]][ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ]]]]
>>
expression
=
SKICall
.
new
(
SKICall
.
new
(
two
.
to_ski
.
to_iota
,
inc
),
zero
)
=> ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[
ɩ[ɩ[ɩ]]]]][ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]
]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ]]]]][ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ]]]][inc][zero]
>>
expression
=
expression
.
reduce
while
expression
.
reducible?
=> nil
>>
expression
=> inc[inc[zero]]

Again,
inc[inc[zero]]
is the
result we expected, so the Iota expression
ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ]]]]][ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ]]]]][ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ]]]]
really is a working translation of
-> p {
-> x { p[p[x]] } }
into a language with no variables, no
functions, and only one combinator; and because we can do this translation
for any lambda calculus expression, Iota is yet another universal
language.