THE MECHANIZATION OF LAMBDA CALCULUS
By W.L. van der Poel
University of Technology
Delft, The Netherlands
Motto: What cannot be made
clear by white chalk alone
cannot be made clear by
coloured chalk either.
1.Introduction
In this article some algorithms for implementing reductions
in the theory of combinators and lambda forms will be described.
These algorithms have formed the basis of many developments have
been made.
The implementation algorithms have led to a rather
mechanical view of the calculi. In particular the process of
writing down forms - that is: the construction of forms - has
been integrated in the algorithms. In this way also non-well
formed formulae will be considered. As long as these incomplete
forms are not put into action they simply have to be regarded as
partially compiled texts. A few results obtained in this
unconventional way have been previously described in Van der Poel
[1980]. More will be given in this article. By including the
compiling of forms in the calculi themselves the language has the
power to talk about itself and to change objects of the language
into subjects.
In general the theory of lambda-beta+ext will be followed
and many results from classical lambda calculus will hold. As the
reduction algorithms always will choose one particular branch,
our systems do not have to obey the Church-Rosser theorem.
One chapter will be devoted to the identity operator. Curry
postulated this as a new primitive in Curry [1975] to be able to
make selectors. It will be shown here that by the possibility to
make new forms by the system itself, the identity operator can be
written without recourse to a new primitive. With the help of
this identity operator an implementation for the CAR, CDR and
CONS functions from LISP will be given. If CR would hold, one can
prove that this would lead to inconsistencies. In our case only
one path can be followed and no inconsistency results.
Another chapter will describe the search for the smallest
"exploder", i.e. a combinator which has no lambda normal form.
This is done by G”del numbering the combinators according to a
certain system. The first one so found could be proved to be an
exploder. The seventh form, consisting of only 7 letters and a
few parentheses turned out to have a lambda normal form
comprising 9 densely printed pages!
2. Definitions and notations
In this article in general the lambda-eta calculus with the
extensionality principle will be followed. For definitions see
Barendregt [1984], chapter 7, and Van der Poel [1980].
Our notation will slightly differ from the usual ones. This
is mainly caused by the requirements and limitations of
machine implementations, most of which have no easy access to
Greek letters, superscripts and subscripts. The frugality of the
notation is a purposely chosen one and contrasts with the
abundance of asterisks, accents, underlining, Greek and Hebrew
letters and ad-hoc invented notation as encountered in the usual
literature on mathematics and symbolic logic. This does not
detract in the slightest from the formal possibilities of the
systems. It might even make things much more perspicuous and
simpler.
Our universe of discourse will consist of combinatory
objects which will be denoted by identifiers. Identifiers are
strings of one or more tokens, not containing spaces, opening
parenteses or closing parentheses. In general identifiers
beginning with a letter will be chosen but occasionally a
suggestive identifier such as a plus-token will be used. Some
identifiers will be regarded as reserved words for the operating
environment and will not be used in the calculus. These are COMB,
LAMB, ERASE, PRINT, LIST, TRACE, UNTRACE, CONV, =, ==, QUIT,
READ, WRITE.
The universe of simple objects will be regarded as finite as
no machine can handle an infinite amount of different objects. In
combinatory logic every object can be applied to every object
resulting in a new object also belonging to the universe. If X
and Y are objects, then (X Y) will denote a new object obtained
by the "application" of X to Y. The notation (X Y Z) will be
short for ((X Y) Z). This will be called the left association
rule. If the application of X to the object (Y Z) is meant, then
one should write (X (Y Z)).
Three letters are reserved as special constants: S, K and L.
The S will be used instead of the S combinator in literature and
follows the rule:
(S X Y Z) => (X Z(Y Z)) (S-rule)
The sign => reads as "reduces to".
The constant K obeys the rule:
(K X Y) => X (K-rule)
K can be regarded as the projection operator or constancy
operator. L will be explained later under the notation for lambda
forms.
All computation with combinators consists of successive
steps of reductions by applying the S-rule, K-rule or replacement
of abbreviations. (See later for abbreviations). The reductions
continue until no further applicable rule can be found. The last
result is then the result of the calculation.
In combinator forms the algorithm will always follow the
"leftmost outermost first" rule. I.e. (S(K X Y)Z P) will follow
the reductions:
(S(K X Y)Z P) => (K X Y P(Z P)) => (X P(Z P))
and not:
(S(K X Y)Z P) => (S X Z P) => (X P(Z P))
In this case Church-Rosser would insure the same result, but in
the sequel many cases will be shown where forms are not CR.
In the combinator case an S with one or two objects
following cannot do anything. However, by transforming to the
lambda form S with two or one argument can be considered a
partially parametrized function. More about this later under
lambda forms.
If there are too many objects following, these arguments are
kept for the next reduction step. This is formulated in the rule:
superfluous trailing arguments are kept.
If nothing can be done on the outer level, only then the
algorithm will look inside the leftmost inner parentheses to see
if anything can be done there.
3. Abbreviations
An important role is played by the concept of
"abbreviation". If a complicated combinator form occurs
frequently as part of a bigger form, an abbreviation can be
assigned to that form. All occurrences of that sub form can then
be shortened to a single identifier. As long as they stay inside
a form abbreviations are not developed into their expansions.
Only when an abbreviation comes to the leftmost outermost place
will it be replaced by the form in full but only at that place.
The inside occurrences could possibly disappear by some K
operator and will not be expanded.
The usual combinators I, B, C and W could have been defined
as abbreviations; e.g. B = (S(K S)K). For the sake of speed this
has not been done. I, B, C and W have been built in and in this
way shorten the number of reduction steps necessary. However, it
is still possible to explicitly redefine any of these combinators
and see how a reduction runs instead. Here is an example for B:
>(B X Y Z)
=(X (Y Z))
NR OF REDUCTIONSTEPS = 1
>B (S(K S)K) B is now redefined
>TRACE Tracing is switched on
>(B X Y Z)
0 (B X Y Z)
0 (S (K S) K X Y Z) Here B is expanded
0 (K S X (K X) Y Z) evaluation.
0 (S (K X) Y Z) Numbers in the margin indicate
0 (K X Z (Y Z)) the level of evaluation
0 (X (Y Z))
1 (Y Z) Nothing can be done on
2 Z the outside level so try
1 (Y Z) inside on level 1 and 2
0 (X (Y Z))
NR OF REDUCTIONSTEPS = 5
The result is the same, the number of steps differs. All examples
in this article have been elaborated by a computer programme
embodying the reduction algorithms. The outputs have been
mechanically inserted in the text by a word processor.
3.2 Lambda forms
The notation for lambda forms has been chosen as follows:
(L F FORM)
where L stands for lambda, F is the formal description variable
and FORM can be a simple or composite form, containing F in zero
or more places as the so-called bound variable and furthermore
containing other free variables and other objects. The free
variables are considered to be bound in enclosing lambda forms,
otherwise we shall call them constant objects.
Lambda forms of more than one variable will always be
written as nested lambda forms of a single variable. See e.g.
Barendregt [1984] 2.1.3 and 2.1.23.
S variable in a lambda forms can be freely replaced by
another variable identifier as long as no clash of names will
occur with another free variable within the bounds of the lambda
form. This is called alpha reduction. In this respect we adhere
to the rules as e.g. formulated in Barendregt [1984] p.24-27. The
algorithms for reduction of lambda forms carefully follow these
formal rules and do not fall into the fallacy formulated on p25
of Barendregt [1984]. S criticism of a previous article (Van der
Poel [1980] by Bunder [1984] fell just into that trap.
Although the notation (L X Y) could suggest that this is a
shorthand for ((L X) Y) according to the left association rule
formulated above for combinators, this is not the case. S lambda
form is considered to be unsplittable. Hence we shall never use
the 3rd Sch”nfinkel axiom in the following way:
(L X(L Y(P Q))) => (S(L X(L Y))(L X(P Q)))
as was done in Van der Poel [1980] ch. 10. However, the reverse
of composing lambda forms out of their three components L, var,
and body will be done frequently in the sequel. Note that the
formal variables in lambda forms are denoted by the same kind of
identifiers as the combinator objects and abbreviations, but as
they are alpha replacable by any other identifier if done
consistently, they have quite another status than the combinator
objects.
The body itself can be quite a normal composite form
consisting of objects, abbreviations, and variables. See example
below.
The algorithms in this article are fourfold:
1) Reducing a combinator form to another combinator form is
straightforward. The algorithm continues until no further
reductions can be made. There are combinator forms which keep on
reducing forever such as (W W W) without taking more space. The
operator must manually intervene to stop the process. Or there
are combinators which progressively consume more and more space
until all memory in the machine is exhausted. We shall call such
a combinator an "exploder". Of course this result is indicated by
a message such as "memory exhausted".
2) Reducing a lambda form to pure combinator form (if possible).
3) Reducing a combinator form to lambda form (if possible).
4) Reducing a lambda form to a simpler lambda form.
This fourfold distinction is perhaps not quite proper as
also mixed combinator and lambda forms can be input. It would be
more appropriate to say that the result in one case yields
combinators, in the other case yields lambda forms.
One set of algorithms is for going from combinator form to
lambda form, the other is for going from lambda form to
combinator form.
3.3 Reducing combinators to lambda forms
Transforming from combinators to lambda forms is
relatively easy. One can use the lambda definition of S, K etc.
as follows:
S => (L X(L Y(L Z(X Z(Y Z)))))
K => (L X(L Y X))
and further one can use:
I => (L X X)
B => (L X(L Y(L Z(X(Y Z)))))
C => (L X(L Y(L Z(X Z Y))))
W => (L X(L Y(X Y Y)))
From there on beta reduction is used to insert possible actual
parameters. Here the very important alpha reduction comes into
play. Whenever an actual parameter contains the same name as a
formal variable, the formal variable is consistently changed to a
newly created and original name. In the implementation as
described here use is made of the GENSYM mechanism of LISP where
the function GENSYM always creates a new original identifier.
In the following example the lambda form (L X(L Y(Y X)))
with formal variables X and Y will get the actual parameters X, Y
and Y, X resp.
>(L X(L Y(Y X))X Y)
=0 (L X (L Y (Y X)) X Y)
0 (L Y (Y X) Y) The object X is substituted for the
0 (Y X) variable X. No harm done
1 X
0 (Y X)
NR OF REDUCTIONSTEPS = 2
>(L X(L Y(Y X))Y X)
=0 (L X (L Y (Y X)) Y X)
0 (L F4 (F4 Y) X) Now the object Y is substituted for
0 (X Y) the formal X and could give a clash
1 Y with the formal Y, hence change
0 (X Y) Y in F4, a newly minted name.
NR OF REDUCTIONSTEPS = 2
2.4 Commands of the operating system.
In the examples we have silently introduced an operating
system. Let us now formally introduce the way abbreviations are
defined and evaluations are set in operation.
When a command of the form
name (form)
is typed in the (form) will be assigned to the name as an
abbreviation for the form. Evaluation will not be done.
S command
name = (form)
will try to reduce the form. The result will be assigned to the
name. S command name = (name) is also allowed.
The form assigned to a name can be printed by a command
PRINT name
and no evaluation will be done
The command COMB will set the system to evaluation toward
combinator forms; the command LAMB will set the system to
evaluation to lambda forms. TRACE will make all separate
reduction steps visible. UNTRACE undoes the TRACE mode.
The command
name CONV (form)
will first evaluate the form to lambda form and then back to
combinator form and assign this to name. In this way sometimes a
simplification can be attained.
The command
name1 == name2
will first convert the forms belonging to name1 and name2 to
lambda form and then both back to combinators. If the resulting
forms are symbol for symbol identical, the result is TRUE,
otherwise FALSE. The reason for transforming first to lambda form
is that (except for the choice of formal variables) a lambda form
has a unique representation. To eliminate the variables, a
transformation back to combinators is made. Now two forms which
are extensionally the same will yield the same resulting text.
Example:
>NAME1 (S K K) (S K K) is a form for I
>NAME2 (S K Z) (S K Z) with arbitrary Z would
work equally well
>NAME1 == NAME2
TRUE Extensionally they are the same
>NAME1 (S K) The same holds for (SK)=(KI)
>NAME2 (K I)
>NAME1 == NAME2
TRUE
>THING CONV (S(K I)) (S(KI)) can be simplified to I
I
The command ERASE name will erase a name, LIST will list all
abbreviation names present in the system at that time. With READ
file and WRITE file a set of defined abbreviations can be saved
and restored on a secondary medium. The command QUIT will step
out of the combinator and lambda environment and return to the
operating environment of the surrounding language. This is of no
concern to the algorithms considered here.
Although all examples in this article have been produced by
algorithms written in LISP (to be more specific: MuLISP (C) of
The Soft Warehouse), several other implementations have been
written in C, Pascal and Harvalias. They are totally different in
their internal machine representation of the combinators but the
operating environment and their combinatory behaviour is exactly
the same.
Of these different implementations the one written
in C is perhaps the most remarkable. This implementation is
specifically meant for machines having a memory mapped screen and
has been devised by E.J. Nijenhuis. The string of symbols
representing the combinator or lambda form is initially written
in screen memory adjusted to the lower right hand corner. As most
reductions only affect the left hand part of the character string
to be treated, the larger part of this string stays in place
during a reduction step. And as the screen image of the string is
the string itself, one can actually see the form grow and shrink
during the reduction steps. When nothing can be done any more on
the outer level, that part of the string is moved to the left
hand upper corner of the screen and ultimately the whole result
is displayed in the left hand upper corner and the right hand
lower corner is fully expended. Execution is so fast that a 5
speed gear was provided to control the delay between the
successive reductions. Of course the capacity of the screen
limits the size of problems that can be done. To this end
combinators and abbreviations are limited to one letter. In that
case the intervening spaces can be omitted to save space. It is
an excellent tool for demonstration purposes.
2.5 Reduction of lambda forms to combinators.
By far the more difficult part of the algorithms was to
construct the transformation of lambda forms to combinators. In
principle this is very simple and rests on the so called
Sch”nfinkel axioms. These run as follows:
1) (L X X) => I
2) (L X Y) => (K Y)
3) (L X (P Q)) => (S(L X P)(L X Q))
The first axiom is applied when the body is simple and is the
same as the formal variable. When the body is simple and is not
the same as the formal variable, then the second axiom applies.
The third case covers a composite body, where P and Q may in turn
be sub forms containing or not containing X.
Although these rules are seemingly simple to apply, in
practice it took quite a while to find out how to do things in
proper sequence.
Three more rules are used in transforming lambda forms. In
the first place beta reduction always has preference and is done
first. E.g.
(L X form actual) => (form [X:=actual])
that is: the actual parameter is substituted for every occurrence
of X in the form, but not for X's bound in inner lambda forms. If
there is any danger of clash of names, the X is first alpha
reduced to another newly minted name. This clash can be detected
by inspecting the actual parameter and the form. If this string
contains X anywhere, there is a potential danger and the alpha
reduction is done.
The second rule is the eta rule:
(L X (form X)) => (form)
when form does not contain X. This rule is a consequence of the
extensionality principle:
if for all X: (F X) = (G X) then F = G
If the effects of F and G on arbitrary arguments are always the
same, we call the forms the same, although they can differ in
appearance. In this way we can prove that (S K) = (K I) because
both (S K X) and (K I X) reduce to I. In the same way
>TRACE
>(S(K X)I Y)
=0 (S (K X) I Y)
0 (K X Y (I Y))
0 (X (I Y))
1 (I Y)
1 Y
0 (X Y)
NR OF REDUCTIONSTEPS = 3
>(I X Y)
=0 (I X Y)
0 (X Y)
1 Y
0 (X Y)
NR OF REDUCTIONSTEPS = 1
Both (S(K X)I) and X produce (X Y) when applied to an arbitrary
Y. By this we can now prove:
(L X(F X)) => (S(L X F)(L X X)) => (S(K F)I) => F
Even if F is composite (but does not contain X!) we can easily
prove that (L X F) => (K F). This is left to the reader.
The third rule does not strictly obey the leftmost outermost
rule. Although the results are correct, often a simpler result
can be attained by first trying to do simplification of the body
alone. E.g. in (L X FORM) first the FORM is treated separately on
level n+1 and later the (L X is joined on again. That means that
temporarily X's appearing in FORM could be regarded as free
objects. S few examples are in place here. Find a combinator for
forming (X Y X) when X and Y are given:
(L X(L Y(X Y X)))
=0 (L X(L Y(X Y X)))
1 (L Y (X Y X)) The inner form is first tried
2 (X Y X)
3 Y
3 X
2 (X Y X)
1 (L Y (X Y X)) But nothing could be done here
1 (S (L Y (X Y)) (L Y X)) So 3rd axiom is applied
2 (L Y (X Y)) A-rule cannot be applied.
2 X Sub form gives X by eta rule
2 (L Y X)
2 (K X) Second sub form gives (K X) by
1 (S X (K X)) second axiom.
0 (L X (S X (K X))) Revert back to level 0.
0 (S (L X (S X)) (L X (K X))) 3rd axiom
1 (L X (S X)) First sub form gives S by eta rule
1 S
1 (L X (K X))
1 K Second gives K by eta rule
0 (S S K) Recompose.
NR OF REDUCTIONSTEPS = 6
The other way round (from combinators to lambda forms) would run:
>LAMB
FROM COMBINATORS TO LAMBDA FORMS
>(S S K)
=0 (S S K)
0 (L F1 (L F2 (L F3 (F1 F3 (F2 F3)))) S K)
0 (L F2 (L F3 (S F3 (F2 F3))) K)
0 (L F3 (S F3 (K F3)))
1 (S F3 (K F3))
1 (L F1 (L F2 (L F3 (F1 F3 (F2 F3)))) F3 (K F3))
1 (L F2 (L F4 (F3 F4 (F2 F4))) (K F3))
1 (L F4 (F3 F4 ((K F3) F4)))
2 (F3 F4 ((K F3) F4))
3 F4
3 (K F3 F4)
3 F3
2 (F3 F4 F3)
1 (L F4 (F3 F4 F3))
0 (L F3 (L F4 (F3 F4 F3)))
NR OF REDUCTIONSTEPS = 7
Note the necessary changes in formal variables. The combinators
are directly used under their own S and K-rule, if possible. In
the first line of level 1 the S-rule was not possible (only 2
arguments) but in the second line of level 3 the K-rule was
applicable.
Let us now consider the form (W C). In combinators it runs:
>TRACE
>WC = (W C)
0 (W C)
0 (S S (K I) C) W is expanded as combinator
0 (S C ((K I) C)) because it has an argument and can
1 C do something
1 (K I C)
1 I
0 (S C I)
NR OF REDUCTIONSTEPS = 3
>UNTRACE Now let's do a conversion via
the lambda form
>THING CONV (W C)
(S S K) and (S C I) appears to be the same
as our previous (S S K)
>WC == THING
TRUE And indeed: WC = THING
The conversion via a lambda form does not always lead to
simplification. Take the form (B C) :
>B (S(K S)K) Let's redefine B and C to express
everything in S and K only
>C (S(B B S)(K K))
>BC = (B C)
(S (K (S (S (K (S (K S) K)) S) (K K))))
NR OF REDUCTIONSTEPS = 8 Now BC is simpler than
>THING CONV (B C)
(S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (K S))))) (K (K
K))) when converted via lambda
>BC == THING
TRUE They are obviously equal
S variant of the described algorithm has been made which is
called SRECOG. The idea was to simplify forms when something of
the form (X Z(Y Z)) could be reduced to (S X Y Z). This has the
disadvantage that (S X Y Z) will never be developed to form (X
Z(Y Z)) any more. But take the following example:
>THING CONV (S(S S)S)
(S (S (K S) (S (S (K S) K) (S I S))) (S (K (S I)) (S I S)))
Now the same with SRECOG:
>THING CONV (S(S S)S)
(S (S S) S)
The actual algorithms will be given in appendix A.
Problem: S K-combinator can destroy information. In general there
is no "backward" reduction e.g. from X to (K X Y). The object Y
is lost forever. But once past these irreversible points in the
reduction graph one can transform a combinator (also containing
K's) to lambda forms and backwards without change. How can one
find the point in the reduction graph where information was
really lost?
4. Selectors and discriminators
Curry once proposed in (Curry [1975]) a way to design a
selector of an element from a list. See also Curry [1972]. The
difficulty is not to eliminate the elements before the element to
be selected but to discard the elements after the selected one.
If the list is ended by a distinctive mark, say #, then one could
successively test whether this special mark is reached or not.
For this test Curry proposed a new primitive ID which can test
the identity of a given element with the end mark. He had to
introduce this as a new primitive as he saw no other way to do it
with the usual combinators. In this chapter it will be shown how
it can be done when the calculus is used to write down new forms
within its own forms.
Let us first demonstrate the method on the example of the
predecessor in the standard Church number representation. We
recall here the usual abstract numbers and arithmetical operators
in the Church system.
ZERO = (K I), ONE = I, TWO = (S ONE) etc.
where SUC = (S B) is the successor. + = (B S(B B)), * = B,
^ = (C I) (= to the power), - = (C(C I P)) where P is the
predecessor on which more later. S discriminator on zero can be
made by IF = (C B K) = (L N(L X(L Y(N(K X)Y)))) with the action:
if N = 0 then Y else X fi
The IF operator shows some peculiarities of combinators and
lambda calculus over the ordinary concept of a mathematical
function. In an ordinary mathematical function f(x,y,z) one would
first evaluate all arguments x, y, and z before applying the
function. The IF operator seemingly assimilates its arguments in
the sequence N, X and Y. But its action is totally different. The
essential thing is what could be called the law of IF:
The non-chosen branch is not evaluated
This is extremely important. If e.g. in a recursive function the
wrong branch would be chosen, then one would wind up in a non
ending sequence of reduction. Take e.g. the well-known example of
the factorial:
FAC (L N(IF N(* N(FAC(P N)))I))
If the argument (* N(FAC(P N))) were chosen after N has reached
zero, the reductions would go on forever.
The predecessor is a little bit more difficult to find than the
other functions. The classical solution is:
>PRINT P
(L N (N G (K ZERO) ONE))
>PRINT G
(L F (D (S (F ZERO)) (F ZERO)))
>PRINT D
(L X (L Y (L N (N (K Y) X))))
and P could be developed in combinator form by the algorithm:
>(P)
=(S (S (S I (K (S (S (K S) (S (K (S I)) (S (K K) (S (K K) (S I (K
(K I))))))) (S (K K) (S (K (S B)) (S I (K (K I)))))))) (K (K (K I
)))) (K I))
NR OF REDUCTIONSTEPS = 41
A simpler form can be made using some results from Van der Poel
[1980]:
>PRINT P
(L N (N W (K I) (S I) (B (S B)) (K (K I))))
>(P)
=(S (S (S (S (S I (K W)) (K (K I))) (K (S I))) (K (S (K (S B)))))
(K (K (K I))))
NR OF REDUCTIONSTEPS = 15
For example if P is applied to FOUR applied to COUNT and SHEEP
one gets:
>(P FOUR COUNT SHEEP)
=(COUNT (COUNT (COUNT SHEEP))) S sheep is counted thrice
NR OF REDUCTIONSTEPS = 48
>LAMB
FROM COMBINATORS TO LAMBDA FORMS
In lambda form:
>(P FOUR)
=(L F3 (L F4 (F3 (F3 (F3 F4)))))
NR OF REDUCTIONSTEPS = 52
We shall use the latter form of P when a normal form for some
operators is wanted.
S much simpler predecessor can be made in the following
unconventional way. Define
>P (C(B C)Q)
>Q (L Q)
Now Q seems to be a very strange abbreviation for an incomplete
lambda form containing Q itself. But when it is applied one gets:
>(P TWO X Y)
=0 (P TWO X Y)
0 (C (B C) Q TWO X Y) P is replaced by its expansion
0 (B C TWO Q X Y) C does its interchanging action
0 (C (TWO Q) X Y) B packs
0 (TWO Q Y X) C interchanges
0 (SUC ONE Q Y X) TWO is successor of ONE
0 (S B ONE Q Y X) S = (S B)
0 (B Q (ONE Q) Y X) B packs
0 (Q ((ONE Q) Y) X) Q is an abbreviation for (L Q)
0 (L Q ((ONE Q) Y) X) Now a well formed lambda form is
0 (ONE X Y) produced with Q as formal var.
0 (I X Y) The rest is trivial
0 (X Y)
1 Y
0 (X Y)
NR OF REDUCTIONSTEPS = 12
One can see that the lambda form (L Q(ONE Q Y)X) is well
formed and made by the calculus. It is only put into action when
fully baked. The half baked Q is handled as an abbreviation. Note
that P in itself has no normal form. Only when applied to objects
will it produce sensible results. Even when only applied to the
abstract number it will give correct results:
>LAMB
FROM COMBINATORS TO LAMBDA FORMS
>(P THREE)
=(L F2 (L F3 (F2 (F2 F3))))
NR OF REDUCTIONSTEPS = 17
The operating system can help to prove simple theorems. E.g.
the associative law of addition and multiplication can be proved
as follows:
>LEFT (+ (+ X Y) Z)
>RIGHT (+ X (+ Y Z))
>LEFT == RIGHT
TRUE
>LEFT* (* (* X Y) Z)
>RIGHT* (* X(* Y Z))
>LEFT* == RIGHT*
TRUE
The commutative law is not so easily proved. If we write:
>LEFT (+ M N)
>RIGHT (+ N M)
>LEFT == RIGHT
(NOT TRUE)
This is caused by the fact that in this case it matters that
N and M are numbers. There is no test for N being a number. But
if actual numbers are substituted, commutativity can be proved
separately for each particular case:
>LEFT (+ THREE FOUR)
>RIGHT (+ FOUR THREE)
>LEFT == RIGHT
TRUE
We shall now first develop a simple discriminator to select
the nth element out of a given list of m elements. In this case
it is known that n-1 elements must be eliminated in front. This
can be done by (P n) times application of K. The elements after
the nth element can be eliminated by (B K K). Hence we get the
following combinator:
>PRINT DNM
(L N (L M (IF (- M N) (P N K (P (- M N) (B K) K)) (P N K I))))
A function of N and M. If N=M, i.e. (- M N) = zero then the case
simplifies to (P N K I): eliminate N-1 elements in front,
otherwise the (P N K eliminates N-1 elements in front and the
(P(- M N)(B K)K) eliminates M-N-1 elements in the back. When
developed in terms of pure combinators DNM looks formidable and
works as follows:
>DNMC = (DNM)
(S (S (K S) (S (S (K S) (S I (K (S (S (S (S (S I (K W)) (K (K I))
) (K (S I))) (K (S (K (S B))))) (K (K (K I))))))) (S (K (S (K K))
) (S (S (K S) (S (K K) (S (S (S (S (S (S I (K W)) (K (K I))) (K (
S I))) (K (S (K (S B))))) (K (K (K I)))) (K K)))) (S (S (K S) (S
(S (K S) (S (S (K S) (S (S (K S) (S (S (K S) (S (S (K S) (S (S (K
S) (S I (K (S (S (S (S (S I (K W)) (K (K I))) (K (S I))) (K (S (K
(S B))))) (K (K (K I))))))) (K (K W)))) (K (K (K I))))) (K (K (S
I))))) (K (K (S (K (S B))))))) (K (K (K (K I)))))) (K (K (S (K K)
))))) (K (K K))))))) (S (K K) (S (S (S (S (S (S (S I (K W)) (K (K
I))) (K (S I))) (K (S (K (S B))))) (K (K (K I)))) (K K)) (K I))))
NR OF REDUCTIONSTEPS = 161
>(DNMC TWO FOUR FIRST SECOND THIRD FOURTH)
=SECOND
NR OF REDUCTIONSTEPS = 352
Indeed the second element out of four is selected. The same holds
for the lambda form:
>LAMB
FROM COMBINATORS TO LAMBDA FORMS
>DNML = (DNMC)
(L F3 (L F4 (F3 (L F3 (F3 (L F1 (L F2 (F1 F2 F2))) (L F2 (L F1 F1
)) (L F2 (L F3 (F3 (F2 F3)))) (L F2 (L F3 (L F5 (L F6 (F5 (F2 F3
F5 F6)))))) (L F2 (L F2 (L F1 F1))))) F4 (L F2 (F3 (L F1 (L F2 (
F1 F2 F2))) (L F2 (L F1 F1)) (L F2 (L F3 (F3 (F2 F3)))) (L F2 (L
F3 (L F7 (L F8 (F7 (F2 F3 F7 F8)))))) (L F2 (L F2 (L F1 F1))) (L
F1 (L F2 F1)) (F3 (L F3 (F3 (L F1 (L F2 (F1 F2 F2))) (L F2 (L F1
F1)) (L F2 (L F3 (F3 (F2 F3)))) (L F2 (L F3 (L F9 (L F10 (F9 (F2
F3 F9 F10)))))) (L F2 (L F2 (L F1 F1))))) F4 (L F1 (L F2 (F1 F2
F2))) (L F2 (L F1 F1)) (L F2 (L F3 (F3 (F2 F3)))) (L F2 (L F3 (L
F11 (L F12 (F11 (F2 F3 F11 F12)))))) (L F2 (L F2 (L F1 F1))) (L
F2 (L F3 (L F13 (F2 F3)))) (L F1 (L F2 F1))))) (F3 (L F1 (L F2 (
F1 F2 F2))) (L F2 (L F1 F1)) (L F2 (L F3 (F3 (F2 F3)))) (L F2 (L
F3 (L F14 (L F15 (F14 (F2 F3 F14 F15)))))) (L F2 (L F2 (L F1 F1))
) (L F1 (L F2 F1)) (L F1 F1)))))
NR OF REDUCTIONSTEPS = 245
>(DNML THREE FOUR FIRST SECOND THIRD FOURTH)
=THIRD
NR OF REDUCTIONSTEPS = 271
Even if the P is replaced by our simple P the selector DNM still
works although DNM itself cannot be brought into normal form:
>P (C(B C)Q)
>Q (L Q)
>(DNM THREE FOUR FIRST SECOND THIRD FOURTH)
=THIRD
NR OF REDUCTIONSTEPS = 125
It has executed in almost half the number of steps as
the previous one!
This kind of selector is not a very satifying one. The list
of element has to be included in the same pair of parentheses as
the selector functions. Furthermore, the number of elements must
be given as an argument. In the sequel we shall choose for
another form nl.:
(L X(X element1 element2 ... elementn))
By packing the list of elements in a lambda form with a leading
argument X one has the possibility of postfixing a function and
including it inside the list parentheses. Its advantages will
become clearer from the examples later.
3.1 The identity operator
Let us first concentrate on the ID operator as proposed by
Curry as a new primitive. Its action should be:
(ID X X) should give true or some representation of true, if
X=X, and (ID X Y) should give a representation of false if X is
not identical with Y. It springs directly to the eye that this
action resembles the first two lambda axioms:
(L X X) => I
and (L X Y) => (K Y)
Unfortunately, anything to the right of (K Y) would be killed by
K and we are left with Y in which we are not really interested.
The solution lies in producing the ultimate lambda form only when
really needed by the calculus itself. If we introduce LA as an
abbreviation for L, then a form containing LA will not be
recognized as a lambda form as long as LA has not been replaced.
And this only happens when it comes to the leftmost front of the
form. After a little fiddling around with the idea we come to the
following form for ID:
LA (L) LA is defined as an abbr. for L
ID (L X (L Y (LA Y (LA X Y) I)))
>TRACE
>(ID JOHN JACK)
=0 (ID JOHN JACK)
0 (L X (L Y (LA Y (LA X Y) I)) JOHN JACK)
0 (L Y (LA Y (LA JOHN Y) I) JACK)
0 (LA JACK (LA JOHN JACK) I)
0 (L JACK (LA JOHN JACK) I)
0 (LA JOHN I)
0 (L JOHN I)
0 (K I)
1 I
0 (K I)
NR OF REDUCTIONSTEPS = 7
>(ID JOHN JOHN)\
TRACE
>TRACE
>(ID JOHN JOHN)
=0 (ID JOHN JOHN)
0 (L X (L Y (LA Y (LA X Y) I)) JOHN JOHN)
0 (L Y (LA Y (LA JOHN Y) I) JOHN)
0 (LA JOHN (LA JOHN JOHN) I)
0 (L JOHN (LA JOHN JOHN) I)
0 (LA I I)
0 (L I I)
0 I
NR OF REDUCTIONSTEPS = 7
Inspection shows where and when the proper lambda forms are
composed and how they deliver I as a representative for TRUE and
(K I) as a representative for FALSE. S normal IF operator as
shown above for arithmetic can do the rest of the work.
Let us now see how the following functions will form a
selector for a given element out of a list of unknown length.
>PRINT OBJECTS
(L X (X FIRST SECOND THIRD FOURTH FIFTH))
In this case we have chosen a list of five objects.
>PRINT SELECT
(L X (L Y (Y (NTH X) #)))
This selector takes the number of the element to be selected
as argument X and the list of objects as Y. It will cause a # to
be appended to the end of the given list (inside the
parentheses)! Further work is done by NTH.
>PRINT NTH
(L N (P N K EATER))
This function will apply N-1 times K to the list of objects
to remove the first N-1 unwanted objects. Then the action is
continued by the most important function EATER, which will eat
all remaining objects after the Nth until the end mark # is
encountered.
>PRINT EATER
(L Y (W I (C (L X (IF (ID X #) (K Y) (K (W I) X))))))
Eater will put the required element in safety in the middle
(K Y). The K will later destroy all unwanted stuff and Y will be
the result. The W I in front will duplicate the whole remaining
function so that one copy is the acting copy and the second copy
is kept for eating the next object. The C puts the second copy
safely behind the list. The (IF (ID tests whether X is already
the end mark or not. The K in (K(W I)X) now destroys the unwanted
term and most remarkably the W I now stand in the front of
exactly the same form as in the beginning but minus an unwanted
term. We shall now show the essential parts of the trace. The
complete trace would be too long for this article. Comments
(indented in small letters) have been inserted.
>(SELECT THREE OBJECTS)
=0 (SELECT THREE OBJECTS)
0 (L X (L Y (Y (NTH X) #)) THREE OBJECTS)
0 (L Y (Y (NTH THREE) #) OBJECTS)
0 (OBJECTS (NTH THREE) #)
0 (L X (X FIRST SECOND THIRD FOURTH FIFTH) (NTH THREE) #)
0 (NTH THREE FIRST SECOND THIRD FOURTH FIFTH #)
The end mark # has been inserted at the end of the list
0 (L N (P N K EATER) THREE FIRST SECOND THIRD FOURTH FIFTH #)
0 (P THREE K EATER FIRST SECOND THIRD FOURTH FIFTH #)
0 (L N (N W (K I) (S I) (B (S B)) (K (K I))) THREE K EATER FIRST
SECOND THIRD FOURTH FIFTH #)
P, the predecessor is doing its action.
......
ultimately ending in:
0 (K (K I) ((B (S B)) (K (K I))) K EATER THIRD FOURTH FIFTH #)
0 (K I K EATER THIRD FOURTH FIFTH #)
0 (I EATER THIRD FOURTH FIFTH #)
The first and second element are now removed and we have
progressed to the EATER function.
0 (EATER THIRD FOURTH FIFTH #)
0 (L Y (W I (C (L X (IF (ID X #) (K Y) (K (W I) X))))) THIRD
FOURTH FIFTH #)
0 (W I (C (L X (IF (ID X #) (K THIRD) (K (W I) X)))) FOURTH FIFTH
#)
0 (I (C (L X (IF (ID X #) (K THIRD) (K (W I) X)))) (C (L X (IF (
ID X #) (K THIRD) (K (W I) X)))) FOURTH FIFTH #)
S copy of the front term has been saved in the back. The
third term is kept behind the middle K.
0 (C (L X (IF (ID X #) (K THIRD) (K (W I) X))) (C (L X (IF (ID X
#) (K THIRD) (K (W I) X)))) FOURTH FIFTH #)
0 (L X (IF (ID X #) (K THIRD) (K (W I) X)) FOURTH (C (L X (IF (ID
X #) (K THIRD) (K (W I) X)))) FIFTH #)
The C has put FOURTH before the saved copy. Now the IF and
ID start looking whether this is the last.
0 (IF (ID FOURTH #) (K THIRD) (K (W I) FOURTH) (C (L X (IF (ID X
#) (K THIRD) (K (W I) X)))) FIFTH #)
0 (L N (L X (L Y (N (K X) Y))) (ID FOURTH #) (K THIRD) (K (W I)
FOURTH) (C (L X (IF (ID X #) (K THIRD) (K (W I) X)))) FIFTH #)
0 (L X (L Y ((ID FOURTH #) (K X) Y)) (K THIRD) (K (W I) FOURTH) (
C (L X (IF (ID X #) (K THIRD) (K (W I) X)))) FIFTH #)
0 (L Y ((ID FOURTH #) (K (K THIRD)) Y) (K (W I) FOURTH) (C (L X (
IF (ID X #) (K THIRD) (K (W I) X)))) FIFTH #)
But FOURTH is not identical to #
0 (ID FOURTH # (K (K THIRD)) (K (W I) FOURTH) (C (L X (IF (ID X #
) (K THIRD) (K (W I) X)))) FIFTH #)
0 (L X (L Y (LA Y (LA X Y) I)) FOURTH # (K (K THIRD)) (K (W I)
FOURTH) (C (L X (IF (ID X #) (K THIRD) (K (W I) X)))) FIFTH #)
0 (L Y (LA Y (LA FOURTH Y) I) # (K (K THIRD)) (K (W I) FOURTH) (C
(L X (IF (ID X #) (K THIRD) (K (W I) X)))) FIFTH #)
0 (LA # (LA FOURTH #) I (K (K THIRD)) (K (W I) FOURTH) (C (L X (
IF (ID X #) (K THIRD) (K (W I) X)))) FIFTH #)
0 (L # (LA FOURTH #) I (K (K THIRD)) (K (W I) FOURTH) (C (L X (IF
(ID X #) (K THIRD) (K (W I) X)))) FIFTH #)
0 (LA FOURTH I (K (K THIRD)) (K (W I) FOURTH) (C (L X (IF (ID X #
) (K THIRD) (K (W I) X)))) FIFTH #)
0 (L FOURTH I (K (K THIRD)) (K (W I) FOURTH) (C (L X (IF (ID X #)
(K THIRD) (K (W I) X)))) FIFTH #)
0 (I (K (W I) FOURTH) (C (L X (IF (ID X #) (K THIRD) (K (W I) X))
)) FIFTH #)
And FOURTH is killed here:
0 (K (W I) FOURTH (C (L X (IF (ID X #) (K THIRD) (K (W I) X))))
FIFTH #)
Now the same story is repeated for FIFTH
0 (W I (C (L X (IF (ID X #) (K THIRD) (K (W I) X)))) FIFTH #)
We will skip and resume the trace when # has been reached.
.....
Yes, now the # is identical to #. FIFTH has been eaten in
the meantime.
0 (IF (ID # #) (K THIRD) (K (W I) #) (C (L X (IF (ID X #) (K
THIRD) (K (W I) X)))))
0 (L N (L X (L Y (N (K X) Y))) (ID # #) (K THIRD) (K (W I) #) (C
(L X (IF (ID X #) (K THIRD) (K (W I) X)))))
0 (L X (L Y ((ID # #) (K X) Y)) (K THIRD) (K (W I) #) (C (L X (IF
(ID X #) (K THIRD) (K (W I) X)))))
0 (L Y ((ID # #) (K (K THIRD)) Y) (K (W I) #) (C (L X (IF (ID X #
) (K THIRD) (K (W I) X)))))
0 (ID # # (K (K THIRD)) (K (W I) #) (C (L X (IF (ID X #) (K THIRD
) (K (W I) X)))))
0 (L X (L Y (LA Y (LA X Y) I)) # # (K (K THIRD)) (K (W I) #) (C (
L X (IF (ID X #) (K THIRD) (K (W I) X)))))
0 (L Y (LA Y (LA # Y) I) # (K (K THIRD)) (K (W I) #) (C (L X (IF
(ID X #) (K THIRD) (K (W I) X)))))
0 (LA # (LA # #) I (K (K THIRD)) (K (W I) #) (C (L X (IF (ID X #)
(K THIRD) (K (W I) X)))))
0 (L # (LA # #) I (K (K THIRD)) (K (W I) #) (C (L X (IF (ID X #)
(K THIRD) (K (W I) X)))))
0 (LA I I (K (K THIRD)) (K (W I) #) (C (L X (IF (ID X #) (K THIRD
) (K (W I) X)))))
(L I I) gives I and the I drops off.
0 (L I I (K (K THIRD)) (K (W I) #) (C (L X (IF (ID X #) (K THIRD)
(K (W I) X)))))
K now destroys the whole rest of the form !
0 (K (K THIRD) (K (W I) #) (C (L X (IF (ID X #) (K THIRD) (K (W I
) X)))))
0 (K THIRD (C (L X (IF (ID X #) (K THIRD) (K (W I) X)))))
0 THIRD
NR OF REDUCTIONSTEPS = 96
and only THIRD remains.
It is not possible to develop the SELECT operator in its own
right. It certainly has no normal form. Only when applied to
proper arguments does it behave correctly. But there is a way to
find a semi closed combinator form for SELECT in the following
manner. Temporarily remove the ID definition from the list and
expand SELECT as a lambda form. The object ID will stay inside as
an unknown object. Now SELECT can be safely expanded. Then
reinsert the definition of ID and the resulting form will work
again.
>LAMB
FROM COMBINATORS TO LAMBDA FORMS
>ERASE ID ID is temporarily erased
OK
>SELECTL = (SELECT) Now SELECTL is developed
(L X (L Y (Y (X (L F1 (L F2 (F1 F2 F2))) (L F2 (L F1 F1)) (L F2 (
L F3 (F3 (F2 F3)))) (L F2 (L F3 (L F4 (L F5 (F4 (F2 F3 F4 F5)))))
) (L F2 (L F2 (L F1 F1))) (L F1 (L F2 F1)) (L Y (L F3 (ID F3 # (L
F2 (L F2 Y)) (L F2 (F2 F2)) (L F2 (L F3 (ID F3 # (L F2 (L F2 Y))
(L F2 (F2 F2)) F2))))))) #)))
NR OF REDUCTIONSTEPS = 60
This lambda form now includes all
functions from NTH, Predecessor and EATER together except ID
itself and only ID contains the dangerous LA.
>READ ID ID is read back in from disk A
DRIVE:A
>(SELECTL THREE OBJECTS) The new SELECTL works exactly as
=THIRD before.
NR OF REDUCTIONSTEPS = 79 Even in fewer steps.
One could raise the objection that the result of these
operations is not itself in the agreed form of a list. It is very
simple to take care of that by replacing the (K Y) in EATER by
(K(LA F1(F1 Y))).
>PRINT NEWEATER
(L Y (W I (C (L X (IF (ID X #) (K (LA F1 (F1 Y))) (K (W I) X)))))
Let us now introduce a list of only two objects:
>OBJECTS (L X (X FIRST SECOND))
Then we could define the LISP CAR function (the first of a
list as:
>PRINT CAR
(L Y (Y NEWEATER #))
and the companion function CDR (the rest of a list) as:
>PRINT CDR
(L Y (Y (K NEWEATER) #))
The number of elements to be stripped in front is now known
and a very simple K will do.
>PRINT CONS
(L X (L Y (LA F2 (F2 (X I) (Y I)))))
The CONS puts together two elements into one new list. To
obtain the elements proper without the surrounding (L X(X .. ))
is very simply done by appending I. CONS packs the two elements
again together into a new list in the lambda form.
>LAMB
FROM COMBINATORS TO LAMBDA FORMS
>(CAR OBJECTS)
=(L F1 (F1 FIRST))
NR OF REDUCTIONSTEPS = 41
>(CDR OBJECTS)
=(L F1 (F1 SECOND))
NR OF REDUCTIONSTEPS = 25
>(CONS(CAR OBJECTS)(CDR OBJECTS))
=(L F2 (F2 FIRST SECOND))
NR OF REDUCTIONSTEPS = 74
If it can be guaranteed that all our objects will contain
exactly two elements (as is the case in pure LISP) then the CAR
and CDR can be made much simpler. One does not have to go to the
trouble of destroying an unknown number of tail elements in the
list and the following functions could be defined:
>PRINT SIMPLECAR
(L X (L Y (Y (X K))))
>PRINT SIMPLECDR
(L X (L Y (Y (X (K I)))))
>(SIMPLECAR OBJECTS)
=(L Y (Y FIRST))
NR OF REDUCTIONSTEPS = 5
>(SIMPLECDR OBJECTS)
=(L Y (Y SECOND))
NR OF REDUCTIONSTEPS = 6
This also works if the list of objects contains a composite
object, e.g.:
>OBJECT (L X(X(X11 X12)(X21 X22)))
>(SIMPLECAR OBJECT)
=(L Y (Y (X11 X12)))
NR OF REDUCTIONSTEPS = 5
S good test for finding out whether an element is atomic or
composite has not yet been found.
In LISP it is customary to write not in pair notation but
rather in list notation. S list can contain an arbitrary number
of elements. The CAR function takes the first from the list, but
the CDR takes all that is left over when the first element is
taken off. If we want to adhere to our chosen list notation:
(L X(X 1 2 3 4 5))
then CAR should give (L X(X 1)) as above and CDR should give
(L X(X 2 3 4 5))
The problem is how to pack the leading X inside the parentheses.
We solved the problem by taking the first element as the name of
a new formal variable and thus get (L 1(1 2 3 4 5)). The variable
1 will always be properly exchanged for a better name by the
alpha reduction, if necessary. The functions now read:
>PRINT CAR
(L Y (Y NEWEATER #))
>PRINT NEWEATER
(L Y (W I (C (L X (IF (ID X #) (K (LA F1 (F1 Y))) (K (W I) X)))))
)
>PRINT CDR
(L X (L (CAR X I) (X I)))
This function forms a new lambda form with the first of the
list as new formal variable, followed by the complete list of
which the first element is now the same as the formal variable.
>OBLIST (L X(X 1 2 3 4 5))
>(CAR OBLIST)
=(L F1 (F1 1))
NR OF REDUCTIONSTEPS = 92
>(CDR OBLIST)
=(L 1 (1 2 3 4 5))
NR OF REDUCTIONSTEPS = 99
It is necessary that the first element is simple. S
composite element would result in an ill formed lambda form.
There is a wide field of further research here.
There is another way of representing lists. This is by using
so called ordered pairs and is very much in accordance with LISP
practice where (X0 X1 X2 X3) is only a short form of writing for:
(X0 . (X1 . (X2 . (X3 . NIL))))
In the same style we could now define
Y3 (L X(X X3 NIL))
Y2 (L X(X X2 Y3))
Y1 (L X(X X1 Y2))
Y0 (L X(X X0 Y1))
Now the complete list Y0 can be developed as
>(Y0)
=(L X (X X0 (L X (X X1 (L X (X X2 (L X (X X3 NIL))))))))
D. Scott [Curry, 1972, p 261] has developed another system
for numerals by the following definition for the successor
>PRINT SCO
(L U (L X (L Y (Y U))))
and the following for number zero:
>PRINT N0
(K)
So for the next numerals we get:
>PRINT N1
(SCO N0)
>PRINT N2
(SCO N1) etc.
Let us develop N2:
>(N2)
=(L X (L Y (Y (L X (L Y (Y (L F1 (L F2 F1))))))))
NR OF REDUCTIONSTEPS = 8
or in combinators
>(N4)
=(K (S I (K (K (S I (K (K (S I (K (K (S I (K K))))))))))))
NR OF REDUCTIONSTEPS = 29
>(N4 X Y)
=(Y (K (S I (K (K (S I (K (K (S I (K K))))))))))
NR OF REDUCTIONSTEPS = 27
>(N0 X Y)
=X
NR OF REDUCTIONSTEPS = 2
For completeness we shall give here the other combinators
for the usual operation in the Scott system:
>PRINT SCOPRED The predecessor
(L N (N K I))
>PRINT SCOIF The zero test
(L N (L X (L Y (N X (K Y)))))
>PRINT S+ The (recursive) plus
(L N (L M (N M (L X (SCO (S+ X M))))))
These combinators are all very simple.
Applied to ordinary arguments X and Y these Scott numbers do
not give rise to nice number representations. But the Scott
numbers have a very important property, mentioned to me in a
personal letter by Scott (Scott [1981]) that they are just
selectors in the above mentioned lists. E.g.:
>(Y0 N0)
=X0
NR OF REDUCTIONSTEPS = 4
>(Y0 N1)
=X1
NR OF REDUCTIONSTEPS = 11
>(Y0 N2)
=X2
NR OF REDUCTIONSTEPS = 18
>(Y0 N3)
=X3
NR OF REDUCTIONSTEPS = 25
Let us trace a case. Then it will be immediately clear how
these selectors work.
>TRACE
(Y0 N2)
=0 (Y0 N2)
0 (L X (X X0 Y1) N2)
0 (N2 X0 Y1)
0 (SCO N1 X0 Y1)
0 (L U (L X (L Y (Y U))) N1 X0 Y1)
0 (L X (L Y (Y N1)) X0 Y1)
0 (L Y (Y N1) Y1)
0 (Y1 N1)
0 (L X (X X1 Y2) N1)
0 (N1 X1 Y2)
0 (SCO N0 X1 Y2)
0 (L U (L X (L Y (Y U))) N0 X1 Y2)
0 (L X (L Y (Y N0)) X1 Y2)
0 (L Y (Y N0) Y2)
0 (Y2 N0)
0 (L X (X X2 Y3) N0)
0 (N0 X2 Y3)
0 (K X2 Y3)
0 X2
NR OF REDUCTIONSTEPS = 18
S reference to these selectors can also be found in
Barendregt, [1984], p134.
The CAR and CDR now work almost the same, except that the
CDR produces a surrounding (L X(X too many. This can be
eliminated by defining:
>PRINT CDRI
(L X (CDR X I))
>PRINT CONSI
(L X (L Y (LA F2 (F2 (X I) Y))))
Now the CAR works as usual:
>(CAR Y0)
=(L Y (Y X0))
NR OF REDUCTIONSTEPS = 9
But the CDR gives a (L Y(Y too many:
>(CDR Y0)
=(L Y (Y (L X (X X1 (L X (X X2 (L X (X X3 NIL))))))))
NR OF REDUCTIONSTEPS = 13
And CDRI is just right:
>(CDRI Y0)
=(L X (X X1 (L X (X X2 (L X (X X3 NIL))))))
NR OF REDUCTIONSTEPS = 17
>(CONSI (CAR Y0)(CDRI Y0))
=(L F2 (F2 X0 (L X (X X1 (L X (X X2 (L X (X X3 NIL))))))))
NR OF REDUCTIONSTEPS = 29
>RESULT = (CONSI (CAR Y0)(CDRI Y0))
(L F2 (F2 X0 (L X (X X1 (L X (X X2 (L X (X X3 NIL))))))))
NR OF REDUCTIONSTEPS = 29
>RESULT == Y0
TRUE
Here too the problem remains to find a good operator
for the ATOM test of LISP. It is still not easy to make a
distinction between the atom JACK and a composite (JOHN JACK).
One way out would be to compose a lambda form which in one case
is a legal one (L JACK something) and in the other case is:
(L (JOHN JACK) ...) which is illegal. Our algorithms do not test
on the formation of such ill-formed forms. This could, however,
very easily be added to the algorithm and it could yield FALSE in
some form or another in that case.
-----------------------------------------------------------------
5. G”delization and exploders.
In this chapter we shall deal with the quest for the
smallest exploder in combinator form. It is an undecidable
problem to determine in general whether a given combinator form
is an exploder or will have a normal form in the end. But every
particular case is decidable in principle if one has the time to
wait until the processor stops, or if one has had the patience to
prove that in this particular case the reduction will go on
forever. Exploders exist in two versions:
1) Exploders in time. The form does not grow but goes through a
cycle of the same steps until the operator stops the
machine. Well-known examples are (W W W) with a cycle of 1,
and (W I(W I)) with a cycle of 2.
2) Exploders in space. The form will grow until the capacity of
the machine has been reached. It could be then that one can
see by inspection that the same substructure is copied over
and over again, or the form can seem to grow and no
structure can be proved before the capacity of the machine
has been reached.
Every proof is a particular proof for that case only. Here
follows an example of an exploder. R is the recursion operator as
defined in Van der Poel [1980].
>R (S I R)
>(R W X)
=0 (R W X)
0 (S I R W X)
0 (I W (R W) X) Every fourth line the recursion on
0 (W (R W) X) W produces a new copy of X hence
0 (R W X X) the machine will ultimately run out
0 (S I R W X X) of space.
0 (I W (R W) X X)
0 (W (R W) X X)
0 (R W X X X)
0 (S I R W X X X)
0 (I W (R W) X X X)
0 (W (R W) X X X)
Here is one which is not so clearly an exploder at least not
from first visual inspection:
>(S(S S)(S S S)(S S)S)
>=0 (S (S S) (S S S) (S S) S)
0 (S S (S S) ((S S S) (S S)) S)
0 (S ((S S S) (S S)) ((S S) ((S S S) (S S))) S)
0 (S S S (S S) S (((S S) ((S S S) (S S))) S))
0 (S (S S) (S (S S)) S (((S S) ((S S S) (S S))) S))
0 (S S S ((S (S S)) S) (((S S) ((S S S) (S S))) S))
0 (S ((S (S S)) S) (S ((S (S S)) S)) (((S S) ((S S S) (S S))) S))
0 (S (S S) S (((S S) ((S S S) (S S))) S) ((S ((S (S S)) S)) (((S
S) ((S S S) (S S))) S)))
0 (S S (((S S) ((S S S) (S S))) S) (S (((S S) ((S S S) (S S))) S)
) ((S ((S (S S)) S)) (((S S) ((S S S) (S S))) S)))
0 (S (S (((S S) ((S S S) (S S))) S)) ((((S S) ((S S S) (S S))) S)
(S (((S S) ((S S S) (S S))) S))) ((S ((S (S S)) S)) (((S S) ((S S
S) (S S))) S)))
0 (S (((S S) ((S S S) (S S))) S) ((S ((S (S S)) S)) (((S S) ((S S
S) (S S))) S)) (((((S S) ((S S S) (S S))) S) (S (((S S) ((S S S)
(S S))) S))) ((S ((S (S S)) S)) (((S S) ((S S S) (S S))) S))))
0 (S S ((S S S) (S S)) S (((((S S) ((S S S) (S S))) S) (S (((S S)
((S S S) (S S))) S))) ((S ((S (S S)) S)) (((S S) ((S S S) (S S)))
S))) (((S ((S (S S)) S)) (((S S) ((S S S) (S S))) S)) (((((S S) (
(S S S) (S S))) S) (S (((S S) ((S S S) (S S))) S))) ((S ((S (S S)
) S)) (((S S) ((S S S) (S S))) S)))))
0 (S S (((S S S) (S S)) S) (((((S S) ((S S S) (S S))) S) (S (((S
S) ((S S S) (S S))) S))) ((S ((S (S S)) S)) (((S S) ((S S S) (S S
))) S))) (((S ((S (S S)) S)) (((S S) ((S S S) (S S))) S)) (((((S
S) ((S S S) (S S))) S) (S (((S S) ((S S S) (S S))) S))) ((S ((S (
S S)) S)) (((S S) ((S S S) (S S))) S)))))
0 (S (((((S S) ((S S S) (S S))) S) (S (((S S) ((S S S) (S S))) S)
)) ((S ((S (S S)) S)) (((S S) ((S S S) (S S))) S))) ((((S S S) (S
S)) S) (((((S S) ((S S S) (S S))) S) (S (((S S) ((S S S) (S S)))
S))) ((S ((S (S S)) S)) (((S S) ((S S S) (S S))) S)))) (((S ((S (
S S)) S)) (((S S) ((S S S) (S S))) S)) (((((S S) ((S S S) (S S)))
S) (S (((S S) ((S S S) (S S))) S))) ((S ((S (S S)) S)) (((S S) ((
S S S) (S S))) S)))))
0 (S S ((S S S) (S S)) S (S (((S S) ((S S S) (S S))) S)) ((S ((S
(S S)) S)) (((S S) ((S S S) (S S))) S)) (((S ((S (S S)) S)) (((S
S) ((S S S) (S S))) S)) (((((S S) ((S S S) (S S))) S) (S (((S S)
((S S S) (S S))) S))) ((S ((S (S S)) S)) (((S S) ((S S S) (S S)))
S)))) (((((S S S) (S S)) S) (((((S S) ((S S S) (S S))) S) (S (((S
S) ((S S S) (S S))) S))) ((S ((S (S S)) S)) (((S S) ((S S S) (S S
))) S)))) (((S ((S (S S)) S)) (((S S) ((S S S) (S S))) S)) (((((S
S) ((S S S) (S S))) S) (S (((S S) ((S S S) (S S))) S))) ((S ((S (
S S)) S)) (((S S) ((S S S) (S S))) S))))))
0 (S S (((S S S) (S S)) S) (S (((S S) ((S S S) (S S))) S)) ((S ((
S (S S)) S)) (((S S) ((S S S) (S S))) S)) (((S ((S (S S)) S)) (((
S S) ((S S S) (S S))) S)) (((((S S) ((S S S) (S S))) S) (S (((S S
) ((S S S) (S S))) S))) ((S ((S (S S)) S)) (((S S) ((S S S) (S S)
)) S)))) (((((S S S) (S S)) S) (((((S S) ((S S S) (S S))) S) (S (
((S S) ((S S S) (S S))) S))) ((S ((S (S S)) S)) (((S S) ((S S S)
(S S))) S)))) (((S ((S (S S)) S)) (((S S) ((S S S) (S S))) S)) ((
(((S S) ((S S S) (S S))) S) (S (((S S) ((S S S) (S S))) S))) ((S
((S (S S)) S)) (((S S) ((S S S) (S S))) S))))))
......etc.
Here is the smallest exploder in combinators found:
>(S(S S)S S S S)
= Memory Space Exhausted
After a while it tells the operator that there was no more
space. This is no proof! Careful inspection has indeed revealed
that this was a true exploder.
There are also cases in which a combinator form, expanded as
combinators only is quite well behaved. Nevertheless these forms
have no lambda normal form. Take for example a well-known
explicit form for the recursion operator R:
>R (W S(B W B))
>W (S S(K I)) For the sake of explicitness even
W and B will be defined in terms
>B (S(K S)K) of S and K alone
>(R)
=(S (S (K (S S (K I))) (S (K S) K)) (S (K (S S (K I))) (S (K S) K
)))
NR OF REDUCTIONSTEPS = 16
A development into lambda forms will immediately show how this
will lead to explosion:
>TRACE
>LAMB
FROM COMBINATORS TO LAMBDA FORMS
>(R)
=0 R
0 (S I R)
0 (L F1 (L F2 (L F3 (F1 F3 (F2 F3)))) I R)
0 (L F2 (L F3 (I F3 (F2 F3))) R)
0 (L F3 (I F3 (R F3)))
1 (I F3 (R F3)) From here on every fourth line will
1 (F3 (R F3)) produce an F3 in front and will
2 (R F3) descend to a next higher level
2 (S I R F3) where exactly the same happens
2 (I F3 (R F3)) over again.
2 (F3 (R F3))
3 (R F3)
3 (S I R F3)
3 (I F3 (R F3))
3 (F3 (R F3))
The system for numbering the combinators is always a bit
arbitrary. Here the following system is chosen: in combinator
forms the right hand parenthesis is not necessary if the left
hand parenthesis is always written for every pair of combinators
as a kind of application operator. This notation is also followed
in Rosenbloom [1950]. E.g.
Usual notation New notation
(S(KS)K) {{S{KSK
(SKK) {{SKK
To distinguish the parentheses of the new notation from those of
the old one, we have chosen braces. As the forms to be numbered
only contain S, K and { there is no need for spaces any more. The
number of braces is always exactly 1 less than the number of
letters in the form. If we now number
K = 1
S = 2
{ = 0
we can make a ternary numbering of the combinators. The choice of
0 for { has been made on purpose so that on the front of the
number the 0's are automatically present and we could represent
our two examples with
{{S{KSK = 0020121 is without ambiguity = 20121
{{SKK = 211 in the same way
Now our G”del numbering starts off with:
Decimal Ternary Form
1 1 K
2 2 S
3 10 K{ ?
4 11 {KK
5 12 {KS
6 20 S{ ?
7 21 {SK
8 22 {SS
etc.
What are we to do with forms that have these trailing braces or
braces with incomplete pairs as in S{K ? The solution to this
problem has been suggested to me by C. B”hm in a personal
communication. The forms with missing elements on the end can be
regarded as parametrized forms. Adjoin as many lambda variables
as needed until the form is complete. E.g. S{K can be made
complete by adjoining:
{{Lx{S{Kx. And K{ becomes {{{{Lx{Ly{K{xy.
S{K would have the number 201. If it is now reduced, we see
that 201 and 20121 will both lead to different representations of
what in effect is B :
>FORM201 (L X(S(K X)))
>FORM20121 (S(K S)K)
>FORM201 == FORM20121
TRUE
>(FORM201 X Y Z)
=(X (Y Z))
NR OF REDUCTIONSTEPS = 4
>(FORM20121 X Y Z)
=(X (Y Z))
NR OF REDUCTIONSTEPS = 5
So different G”del numbers can produce (different)
combinators that have the same effect in the extensional sense.
The quest for exploders now proceeds in the following way:
beginning with 1 all combinators were produced, supplemented by a
sufficient number of lambda variables if necessary. If a result
was produced and the machine goes to the next number, then the
combinator is not an exploder. If, however, the capacity of the
machine was exceeded, this could possibly indicate an exploder. S
piece of the actual output will be given below. The first
possible exploder appeared at number 5072 (decimal). Further
candidates were found at 6379 and 9171. From these results it
soon became clear that all possible exploders in the beginning
only contain S's and {'s and no K's. This can be intuitively
understood from the simplifying action of K. However, it could
very well be that further on there will also be cases with K's.
The actual output from the complete program looks as
follows:
(The programme used is a different one and utilizes
small letters instead of capitals)
number : 1 (1)
form : (k)
extended form : (k)
normal form : k
simplification : k
number : 2 (2)
form : (s)
extended form : (s)
normal form : s
simplification : s
number : 10 (3)
form : (k *)
extended form : (l CSSSS * * l BSSSS * k * CSSSS BSSSS)
normal form : ((l CSSSS) ((l BSSSS) (k (CSSSS BSSSS))))
simplification : (s (k k))
number : 11 (4)
form : (k k)
extended form : (k k)
normal form : (k k)
simplification : (k k)
number : 12 (5)
form : (k s)
extended form : (k s)
normal form : (k s)
simplification : (k s)
number : 20 (6)
form : (s *)
extended form : (l ESSSS * * l DASSS * s * ESSSS DSSSS)
normal form : ((l ESSSS) ((l DSSSS) (s (ESSSS DSSSS))))
simplification : (s (k s))
number : 21 (7)
form : (s k)
extended form : (s k)
normal form : (s k)
simplification : (k i)
number : 22 (8)
form : (s s)
extended form : (s s)
normal form : (s s)
simplification : (s s)
number : 100 (9)
form : (k * *)
extended form : (l IAAAA * * l HAAAA * * l GAAAA * k * * IAAAA
HAAAA GAAAS)
normal form : ((l IAAAS) ((l HAAAS) ((l GAAAS) (k ((IAAAA
HAAAS) GAAAS)))))
simplification : (s (k (s (k k))))
number : 101 (10)
form : (k * k)
extended form : (l JAAAA * k * k JAAAS)
normal form : ((l JAAAS) (k (k JAAAS)))
simplification : (s (k k) k)
number : 102 (11)
form : (k * s)
extended form : (l KAAAA * k * s KAAAS)
normal form : ((l KAAAS) (k (s KAAAS)))
simplification : (s (k k) s)
number : 110 (12)
form : (k k *)
extended form : (l MAAAA * * l LAAAA * * k k * MAAAA LAAAS)
normal form : ((l MAAAS) ((l LAAAS) ((k k) (MAAAA LAAAS))))
simplification : (k (k k))
number : 111 (13)
form : (k k k)
extended form : (k k k)
normal form : ((k k) k)
simplification : k
number : 112 (14)
form : (k k s)
extended form : (k k s)
normal form : ((k k) s)
simplification : k
number : 120 (15)
form : (k s *)
extended form : (l OAAAA * * l NAAAA * * k a * OAAAA NAAAS)
normal form : ((l OAAAS) ((l NAAAS) ((k a) (OAAAA NAAAS))))
simplification : (k (k s))
number : 121 (16)
form : (k s k)
extended form : (k s k)
normal form : ((k s) k)
simplification : s
number : 122 (17)
form : (k s s)
extended form : (k s s)
normal form : ((k s) s)
simplification : s
number : 200 (18)
form : (s * *)
extended form : (l RAAAA * * l QAAAA * * l PAAAA * s * * RAAAA
QAAAA PAAAS)
normal form : ((l RAAAS) ((l QAAAS) ((l PAAAS) (s ((RAAAA
QAAAS) PAAAS)))))
simplification : (s (k (s (k s))))
number : 201 (19)
form : (s * k)
extended form : (l SAAAA * s * k SAAAS)
normal form : ((l SAAAS) (s (k SAAAS)))
simplification : (s (k s) k)
To speed up the search process (the previous search took
some 20 hours up to 10000 on a PDP11/60), a slight variation of
the numbering was set up in which only S and { were used. Now A
can have the value 1 and { still the value 0 and the numbering
can be done in the binary system. The following is the actual
output of a program giving the first 8 cases:
number : 10111111 (191)
form : (s * s s s s s s)
extended form : (s * s s s s s s)
normal form : (((((s (s s)) s) s) s) s)
simplification : ERROR Interrupt
number : 11101111 (239)
form : (s s s * s s s s)
extended form : (s s s * s s s s)
normal form : (((((s s) s) (s s)) s) s)
simplification : ERROR Interrupt
number : 101011111 (351)
form : (s * s * s s s s s)
extended form : (s * s * s s s s s)
normal form : ((((s (s (s s))) s) s) s)
simplification : ERROR Interrupt
number : 101110111 (375)
form : (s * s s s * s s s)
extended form : (s * s s s * s s s)
normal form : ((((s (s s)) s) (s s)) s)
simplification : ERROR Interrupt
number : 101111101 (381)
form : (s * s s s s s * s)
extended form : (l BAAAA * * * * * s * s s s s s * s BAAAS)
normal form : ((l BAAAS) (((((s (s s)) s) s) s) (s BAAAS)))
simplification : ERROR Interrupt
number : 101111110 (382)
form : (s * s s s s s s *)
extended form : (l CAAAA * * l BAAAA * * * * * * s * s s s s
s s * CAAAA BAAAS)
normal form : ERROR Interrupt
number : 101111111 (383)
form : (s * s s s s s s s)
extended form : (s * s s s s s s s)
normal form : ((((((s (s s)) s) s) s) s) s)
simplification : ERROR Interrupt
number : 111010111 (471)
form : (s s s * s * s s s)
extended form : (s s s * s * s s s)
normal form : ((((s s) s) (s (s s))) s)
simplification : ERROR Interrupt
The notation of the normal form in combinators contains all
parentheses as derived from the { notation. Then a transformation
to lambda form takes place and here the machine indicates its
finiteness by the message "ERROR Interrupt" and resumes with the
next case. Succeeding cases give no output.
The case 191 = (S(S S)S S S S) has been inspected later and
could indeed be proved to be an exploder by recognizing recurrent
structures in the development. Case 471 = (S S S(S(S S))S) in the
usual notation is much more interesting. On the machine above it
seemed to be an exploder. But when run later on a much larger
machine it gave a lambda normal form after some minutes. This
lambda form occupies 9 densely written pages and needed 813 newly
created lambda variables! This latter number could be reduced to
far fewer by singling out locally used variables and using the
same variable names over and over again. The program, however,
takes the safe road and creates a new variable on every possible
alpha name conflict.
Let us now take case 381. This can be written in the usual
form as:
>PRINT Q
(L X (S (S S) S S S (S X)))
or with a little bit of experience with "backward reduction" one
can transform this to:
>PRINT QB
(B (S (S S) S S S) S)
These forms can both be expanded in combinator form. The shortest
result is obtained when both are applied to an arbitrary X:
>(Q X)
=(S X (X (S (S (S S) S) (S X)) (S S (S (S (S S) S)) (S X))) (S (X
(S (S (S S) S) (S X)) (S S (S (S (S S) S)) (S X))) (S X (X (S (S
(S S) S) (S X)) (S S (S (S (S S) S)) (S X)))) (X (S (S (S S) S) (
S X)) (S S (S (S (S S) S)) (S X)) (S (X (S (S (S S) S) (S X)) (S
S (S (S (S S) S)) (S X)))) (S X (X (S (S (S S) S) (S X)) (S S (S
(S (S S) S)) (S X)))))))
NR OF REDUCTIONSTEPS = 75
>(QB X)
=(S X (X (S (S (S S) S) (S X)) (S S (S (S (S S) S)) (S X))) (S (X
(S (S (S S) S) (S X)) (S S (S (S (S S) S)) (S X))) (S X (X (S (S
(S S) S) (S X)) (S S (S (S (S S) S)) (S X)))) (X (S (S (S S) S) (
S X)) (S S (S (S (S S) S)) (S X)) (S (X (S (S (S S) S) (S X)) (S
S (S (S (S S) S)) (S X)))) (S X (X (S (S (S S) S) (S X)) (S S (S
(S (S S) S)) (S X)))))))
NR OF REDUCTIONSTEPS = 75
Both examples were done with the SRECOG. Without the S recognizer
this would have become:
(Q X)
>=(X (X (S (S (S S) S) (S X)) (S (S X) (S (S (S S) S) (S X))) (X
(S (S (S S) S) (S X)) (S (S X) (S (S (S S) S) (S X))) (S (X (S (S
(S S) S) (S X)) (S (S X) (S (S (S S) S) (S X))))) (S X (X (S (S (
S S) S) (S X)) (S (S X) (S (S (S S) S) (S X)))))) (X (X (S (S (S
S) S) (S X)) (S (S X) (S (S (S S) S) (S X))) (S (X (S (S (S S) S)
(S X)) (S (S X) (S (S (S S) S) (S X))))) (S X (X (S (S (S S) S) (
S X)) (S (S X) (S (S (S S) S) (S X)))))) (X (S (S (S S) S) (S X))
(S (S X) (S (S (S S) S) (S X))) (X (S (S (S S) S) (S X)) (S (S X)
(S (S (S S) S) (S X))) (S (X (S (S (S S) S) (S X)) (S (S X) (S (S
(S S) S) (S X))))) (S X (X (S (S (S S) S) (S X)) (S (S X) (S (S (
S S) S) (S X))))))))) (X (S (S (S S) S) (S X)) (S (S X) (S (S (S
S) S) (S X))) (X (S (S (S S) S) (S X)) (S (S X) (S (S (S S) S) (S
X))) (X (S (S (S S) S) (S X)) (S (S X) (S (S (S S) S) (S X))) (S
(X (S (S (S S) S) (S X)) (S (S X) (S (S (S S) S) (S X))))) (S X (
X (S (S (S S) S) (S X)) (S (S X) (S (S (S S) S) (S X)))))) (X (X
(S (S (S S) S) (S X)) (S (S X) (S (S (S S) S) (S X))) (S (X (S (S
(S S) S) (S X)) (S (S X) (S (S (S S) S) (S X))))) (S X (X (S (S (
S S) S) (S X)) (S (S X) (S (S (S S) S) (S X)))))) (X (S (S (S S)
S) (S X)) (S (S X) (S (S (S S) S) (S X))) (X (S (S (S S) S) (S X)
) (S (S X) (S (S (S S) S) (S X))) (S (X (S (S (S S) S) (S X)) (S
(S X) (S (S (S S) S) (S X))))) (S X (X (S (S (S S) S) (S X)) (S (
S X) (S (S (S S) S) (S X)))))))))))
NR OF REDUCTIONSTEPS = 47
which is quite a bit longer. Trying to expand to lambda form
apparently explodes but the conclusive proof has not been given.
The expansion of case 471 is given in appendix C,
photographically reduced. If transformed back to combinators,
this gives:
>PRINT QC
=(S (S (S (K S) (S S (S (K S)) (S (S (S (S I S) (S (S (K S) (S (S
(K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S
(K S)))))) (S I))) (S (S S (S I) S) (S (S (K S) (S (S (K S) (S (K
(S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S (K S))))))
(S I)))) (S (S (S (K S) (S S (S (K S)) (S (S (S I S) (S (S (K S)
(S (S (K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (
S S (S (K S)))))) (S I))) (S (S S (S I) S) (S (S (K S) (S (S (K S
) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S (K
S)))))) (S I)))))) (S (S (K S) (S (S (S I S) (S (S (K S) (S (S (K
S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S (K
S)))))) (S I))) (S (S S (S I) S) (S (S (K S) (S (S (K S) (S (K (S
(K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S (K S)))))) (S
I))))) (S S (S (K S)) (S (S (S I S) (S (S (K S) (S (S (K S) (S (K
(S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S (K S))))))
(S I))) (S (S S (S I) S) (S (S (K S) (S (S (K S) (S (K (S (K S)))
(S S (S (K S))))) (S (S S S (K S)) (S S (S (K S)))))) (S I)))))))
(S I (S (S (S (K S) (S I S)) (S S (S I) S)) (S (S (K S) (S (S (K
S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S (K
S)))))) (S I)))))))) (S (S (K S) (S (S (S (S I S) (S (S (K S) (S
(S (K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S
(S (K S)))))) (S I))) (S (S S (S I) S) (S (S (K S) (S (S (K S) (S
(K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S (K S))))
)) (S I)))) (S (S (S (K S) (S S (S (K S)) (S (S (S I S) (S (S (K
S) (S (S (K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)
) (S S (S (K S)))))) (S I))) (S (S S (S I) S) (S (S (K S) (S (S (
K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S
(K S)))))) (S I)))))) (S (S (K S) (S (S (S I S) (S (S (K S) (S (S
(K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S
(K S)))))) (S I))) (S (S S (S I) S) (S (S (K S) (S (S (K S) (S (K
(S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S (K S))))))
(S I))))) (S S (S (K S)) (S (S (S I S) (S (S (K S) (S (S (K S) (S
(K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S (K S))))
)) (S I))) (S (S S (S I) S) (S (S (K S) (S (S (K S) (S (K (S (K S
))) (S S (S (K S))))) (S (S S S (K S)) (S S (S (K S)))))) (S I)))
)))) (S I (S (S (S (K S) (S I S)) (S S (S I) S)) (S (S (K S) (S (
S (K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S
(S (K S)))))) (S I))))))) (S S (S (K S)) (S (S (S (S I S) (S (S (
K S) (S (S (K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K
S)) (S S (S (K S)))))) (S I))) (S (S S (S I) S) (S (S (K S) (S (S
(K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S
(K S)))))) (S I)))) (S (S (S (K S) (S S (S (K S)) (S (S (S I S) (
S (S (K S) (S (S (K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S
S (K S)) (S S (S (K S)))))) (S I))) (S (S S (S I) S) (S (S (K S)
(S (S (K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (
S S (S (K S)))))) (S I)))))) (S (S (K S) (S (S (S I S) (S (S (K S
) (S (S (K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S))
(S S (S (K S)))))) (S I))) (S (S S (S I) S) (S (S (K S) (S (S (K
S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S (K
S)))))) (S I))))) (S S (S (K S)) (S (S (S I S) (S (S (K S) (S (S
(K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S
(K S)))))) (S I))) (S (S S (S I) S) (S (S (K S) (S (S (K S) (S (K
(S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S (K S))))))
(S I))))))) (S I (S (S (S (K S) (S I S)) (S S (S I) S)) (S (S (K
S) (S (S (K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)
) (S S (S (K S)))))) (S I))))))))) (S I (S (S (S (S I S) (S (S (K
S) (S (S (K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)
) (S S (S (K S)))))) (S I))) (S (S S (S I) S) (S (S (K S) (S (S (
K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S
(K S)))))) (S I)))) (S (S (S (K S) (S S (S (K S)) (S (S (S I S) (
S (S (K S) (S (S (K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S
S (K S)) (S S (S (K S)))))) (S I))) (S (S S (S I) S) (S (S (K S)
(S (S (K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (
S S (S (K S)))))) (S I)))))) (S (S (K S) (S (S (S I S) (S (S (K S
) (S (S (K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S))
(S S (S (K S)))))) (S I))) (S (S S (S I) S) (S (S (K S) (S (S (K
S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S (K
S)))))) (S I))))) (S S (S (K S)) (S (S (S I S) (S (S (K S) (S (S
(K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S
(K S)))))) (S I))) (S (S S (S I) S) (S (S (K S) (S (S (K S) (S (K
(S (K S))) (S S (S (K S))))) (S (S S S (K S)) (S S (S (K S))))))
(S I))))))) (S I (S (S (S (K S) (S I S)) (S S (S I) S)) (S (S (K
S) (S (S (K S) (S (K (S (K S))) (S S (S (K S))))) (S (S S S (K S)
) (S S (S (K S)))))) (S I))))))))
If this is again transformed back to lambda forms, it gives
exactly the same form again as in appendix C (possibly apart from
the alpha reduced names). This has been thoroughly verified.
The other cases have not been analyzed yet. They all seem to
be true exploders as they also explode in the bigger machine.
This is left as an exercise for the reader.
Acknowledgements
Many thanks are due to Mike Woodger, who carefully screened
the English text and corrected a few technical and essential
errors.
References
Barendregt, H.P.
[1984] The Lambda Calculus, Its Syntax and Semantics, North-
Holland Publ. Co., Amsterdam.
Bunder, M.W.
[1984] Some problems and inadequacies in the van der Poel-
Schaap-van der Mey theory of combinators, Proc. Royal
Netherlands Academy of Sciences, S 87(4), Dec. 1984,
p373-377, Amsterdam.
Curry, H.B.
[1972] with J.R. Hindley and J.P. Seldin, Combinatory Logic,
Vol II. North-Holland Publ. Co., Amsterdam
[1975] Representation of Markov Algorithms by Combinators. In:
The Logical Enterprise, ed. A.R. Anderson, R. Marcus
and R.M Martin, Yale Univ. Press, New Haven p109-119.
Poel, W.L. van der, C.E. Schaap and G. van der Mey,
[1980] New arithmetical operators in the theory of
combinators. Indag. Math., Vol. 42, Fasc.3 (1980),
Amsterdam.
Rosenbloom, P.
[1950] The Elements of Mathematical Logic, Dover Publ., N.Y.
Scott, D.
[1981] Personal letter, 29th of April.
Version 7th November, 1987
Revised 27th January, 2000