NOTE: This transcription was contributed by Martin P.M. van der Burgt, who has devised a process for producing transcripts automatically. Although its markup is incomplete, we believe it serves a useful purpose by virtue of its searchability and its accessibility to text-reading software. It will be replaced by a fully marked-up version when time permits. —HR
A mild variant of Combinatory Logic.
The following is written in reaction to the description of Combinatory Logic as given in [1] by D.A.Turner. With plus standing for the prefix adding operator, Turner defines the successor function suc by
def suc x = plus 1 x . |
To the right of the equality sign, juxtaposition is assumed to be associative to the left; more fully bracketed we would have had
def suc x = (plus 1) x . |
Because at both sides of the equality sign, the variable x occurs only as the very last atom, we can abstract x from both sides by omission, yielding def suc = plus 1 .
This wouldn’t have been possible if suc had been defined by
def suc x = (plus x) 1 |
Combinatory logic is a discipline for rewriting, if necessary, such right-hand sides in such a way that X —or, in general: the variable to be abstracted from— only occurs as the last atom of the expression. Given
def f x = E |
G x = E (Law of Abstraction) |
Turner denotes G by [x]E or by ([x]E) —to be pronounced as “abstract x from E”— and describes (following Curry) abstraction as a textual operation. I almost quote from [1] —remember that juxtaposition associates to the left, at least at both sides of the equality sign— “We introduce three combinators S , K, and I [It is customary to print these constants in bold face, EWD] , defined by the equations
S f g x =f x (g x) | (S) | |
K y x = y | (K) | |
I x = x | (I) |
[x](E1 E2) = S ([x]E1) ([x]E2) | ||
[x]x = I | ||
[X]y = K y |
After having pointed out that this abstraction process leads to very long-winded formulae, Turner introduces for brevity’s sake two extra combinators B and C , defined by
B f g x = f (g x) | (B) | |
C f g x = f x g ; | (C) |
((C f) g) x = (f x) q. |
* *
*
So much for Turner’s description of combinatory logic. His notational conventions have the (potential) technical advantage that each formula can be represented by a binary tree with labels —combinators or identifiers— in its leaves.
I found the fact that during the abstraction process combinators and identifiers (for variables) are treated on the same footing more confusing than illuminating. As it stands, the abstraction process also defines how to abstract a combinator from an expression; perhaps somewhat rashly I regard this, however, as a rather meaningless facility.
Note. Not only some abstractions, but also some applications should be regarded as meaningless. I owe to C.S.Scholten the following very nasty example. From
def funny x = x x |
x x = S I I x |
def funny = S I I . |
funny funny=S I I (S I I) = | |
I (S I I) (I (S I I))= | |
S I I (S I I) = funny funny . |
I was also disturbed by the extreme asymmetry introduced by the combination of a) the placing of the combinators and b) the association to the left. This is particularly noticeable in the fully bracketed form of rule (S):
((S f) g) x = (f x) (g x) |
Note. It could be argued that application is not only asymmetric —in general “a b ≠ b a”— but that the two components are very different, being “function” and “argument” respectively. But two remarks are in order.
Firstly, the distinction between “function” and “argument” is not as clear-cut as is often thought. with z standing for a complex number and re(z) and im(z) standing for its real and imaginary parts respectively, we could regard re and im as real functions defined on a complex domain. With z as a record with two fields we would write z.re and z.im respectively, i.e. a complex value can be regarded as a real function on the domain {re, im}.
Secondly, it is exactly combinatory logic that allows expressions for a and b , such that “a b” and “b a” , though different, are extremely meaningful. (See below.) (End of Note.)
A third complaint only emerged when exercising it. While abstracting and applying I found myself all the time adding and removing bracket pairs. This is not to be wondered at: when we look at the S-rule in its fully bracketed form, it is not clear at all, how the bracket pairs to the right and to the left correspond with each other.
So I set myself the goal of finding an equivalent notation to which the above objections would not apply. Most of the exploratory work was done together with C.S.Scholten; the synthesis to be described below emerged on 8 April 1980 in a session of the Tuesday Afternoon Club, which screened the manuscript for what follows a week later.
* *
*
In the following there is no such thing as association from the left, and I shall introduce no redundant or optional bracket pairs. My starting point is the set of fully bracketed expressions, satisfying the syntax
< exp > ::= < identifier > | (< exp > < exp > ) . |
I shall not introduce the need to abstract a variable from an expression in which that variable does not occur. The formal definition for occurrence is the following obvious one: with x and y standing for identifiers and E, E1, and E2 standing for expression, we define
x in E = if E = y → x = y | |||
▯ E = (E1 E2) → (x in E1) or (x in E2) | |||
fi . |
< term > ::= < empty > | < exp > | (< term > coms+ < term > ) . |
< term > ::= < empty > | < exp > | ( < term > coms < term > ) |
NB. See Appendix on page EWD735 - 8, etc.!!!!!
Note that each bracket pair always surrounds two terms, separated by a possibly empty sequence of’ combinators, such that neither of the terms is empty or the combinator sequence is non-empty. I shall not introduce the need to abstract a variable from a term in which that variable does not occur; with furthermore T , T1 , and T2 standing for terms, we define
x in T = if T = empty → false | |||
▯ T = E → x in E | |||
▯ T = (Tl coms+ T2) → (x in Tl) or (x in T2) | |||
fi . |
[x]T = if x in T | 0. | ||||||||
if T = x → empty | 1. | ||||||||
▯ T = (Tl coms T2) → | 2. | ||||||||
if x in Tl → | 3. | ||||||||
if x in T2 → ([x]T1 S coms [x]T2) | 4. | ||||||||
▯ non x in T2 → ([x]T1 C coms T2) | 5. | ||||||||
fi | 6. | ||||||||
▯ non x in Tl → {x in T2} | 7. | ||||||||
if T = (T1 x) → Tl | 8. | ||||||||
▯ T ≠ (Tl x) → (Tl B coms [x]T2) | 9. | ||||||||
fi | |||||||||
fi | |||||||||
fi | |||||||||
fi |
Because in line 2 coms = < empty > implies that neither T1 nor T2 is empty, line 4 represents the only possibility of generating a bracket pair containing a single atom: (S) . Therefore, in line 8 T1 is not empty. (End of Notes.)
A reduction rule is applicable whenever we encounter a term of the form
((T1 coms+ T2) h) ; |
((T1 S coms T2) h) = ([T1 h] coms [T2 h]) | |
((T1 C coms T2) h) = ([T1 h] coms T2) | |
((T1 B coms T2) h) = (T1 coms [T2 h]) |
[T h] = if T= < empty > → h ▯ T ≠ < empty > → (T h) fi . |
[[x]T X] = T (Law of Abstraction) |
Note. We have already observed that in a term derived by abstraction from an expression and of the form (T1 S T2) both T1 and T2 may be empty. If it is of the form (T1 B T2), T1 will not be empty; if it is of the form (T1 C T2), T2 will not be empty. As a result, reduction will never lead to a redundant bracket pair. (End of Note.)
* *
*
Of course the new notation doesn’t rule out anomalies like funny. We would have
def funny = (S) . |
((S)(S)) = ([(S)][(S)]) = ((S)(S)) . |
As another example we consider the function twice , given by
((twice f) x) = (f (f x)) , hence | |
(twice f) = (f B f) , hence | |
twice = (SB) |
((thrice f) x) = (f (f (f x))) , hence | |
(thrice f) = (r B (F B f)) , hence | |
thrice = (SB (SB)) |
(thrice twice) = ((SB (SB)) twice) | |
= (twice B (twice B twice)) | |
= ((SB) B ((SB) B (SB))) |
((thrice twice) f) = (((SB) B ((SB) B (SB))) f) | |
= ((SB) ((SB) (f B f))) | |
= ((SB) ((r B f) B (f B f))) | |
= (((f B f) B ( f B f)) B ((f B f) B (f B f))) . |
As a final example, consider E = ((* ((+ x) y)) y)
I then derive without further intermediate results
[x]E = ((* B (+ C y)) C y) | |
[y][x]E = ((* BB (+ BC)) SC) |
In Turner’s style we would have had E = * (+ x y) y .
In that case I had to derive
[x]E = C [x](* (+ x y)) y | |
= C (B * (C [x](+ x) y)) y | |
= E (B * (C + y)) y . |
[y][x]E = S (B C B (B *) (C +)) I , or fully bracketed —almost fully, that is— | |
= (S ((((B C) B) (B *)) (C +))) I |
* *
*
The difference between the two techniques is clearly that I propose to attach strings of combinators to internal nodes of the parse tree; the other convention expands the binary tree and stores the information of the strings of combinators in the leaves thus created. I haven’t learned yet, how to translate trees of the one type into trees of the other type. I cannot escape the impression that Curry’s conventions for “tree expansion” are in some sense more arbitrary than the conventions I have explored here.
Another moral of the story is that “Currying” as introduced by Turner is from a logical point of view no more than another red herring. Why replace “x + y” first by ’plus x y“, when we can parse these formulae as ”(x +) y“ and ”(plus x) y“ ? The only justification is that [x](plus x) = plus is shorter than [x](x +) = (C I) + —according to Curry/Turner— or (C +) —according to the conventions explored here— : in short, no more than a minor optimization if we assume that x is more frequently abstracted from (X +) than + .
I have the feeling that the above explorations should be continued.
NB. Appendix on the next pages!!! (End of NB.)
Plataanstraat 5 | 23 April 1980 |
5671 AL NUENEN | prof.dr.Edsger W.Dijkstre |
The Netherlands | Burroughs Research Fellow |
Appendix. (Written after the above had been read together with C.S.Scholten.)
A first remark is that we can simplify the abstraction process as described on page EWD735 - 4 by replacing the alternative construct on lines 8, 9, and 10 simply by (T1 B coms [X]T2) . Cleaning things up we get
[x]T = if x in T → | .0 | ||||||
if T = x → empty | .1 | ||||||
▯ T = (Tl coms T2) → | |||||||
if x in T1 and x in T2 → ([x]Tl S coms [x]T2) | |||||||
▯ x in Tl and non x in T2 → ([x]T1 C coms T2) | |||||||
▯ non x in Tl and x in T2 → (T1 B coms [x]T2) | |||||||
fi | |||||||
fi | |||||||
fi . |
A more important remark is that my correction on page EWD735 - 5 was a short-sighted patch. We should have defined the syntax for terms independently of that for expression, viz.
< term > ::= < empty > | < identifier > | ( < term > coms < term >) . |
T is empty or | ||
T is an identifier or | ||
T is of the form (T1 coms T2) such that | ||
(T1 ≠ empty or ooms contains an S or a C) and | ||
(T2 ≠ empty or come contains an S or a B and | ||
T1 and T2 are both healthy |
Furthermore —both in the original form of abstraction and in the cleaned up one— a healthy T implies (when defined) a healthy [x]T . Furthermore , for healthy T and healthy, but non-empty h , [T h] as defined on page EwD735 - 5 is healthy. In short, neither abstraction nor reduction ever introduces an unhealthy term!
Salvo errore et omissione, the above does the job. By the time that we have discovered the significance —if any— of our exercise, this text has to be rewritten anyhow; hence I think that this rough “working document” has reached the stage to be concluded. Besides that, I am tired.
* *
*
At this stage it is very hard to formulate my acknowledgments. I am indebted to D.A.Turner for his article, to Hamilton Richards for having drawn my attention to it; I am greatly indebted to C.S.Scholten for joining me in my effort to understand combinatory logic in my way: his assistance in all stages of the development has been invaluable; I am indebted to the members of the Tuesday Afternoon Club for their help and criticism. The initiative and the errors are mine.
(End of Appendix.) |
Plataanstraat 5 | 6 May 1980 |
5671 AL NUENEN | prof.dr.Edsger W.Dijkstra |
The Netherlands | Burroughs Research Fellow |
Transcribed by Martin P.M. van der Burgt
Last revision