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