Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs

Introduction

I deeply appreciate the honor of the ACM invitation to give the 1977 Turing Lecture and to publish this account of it with the details promised in the lecture. Readers wishing to see a summary of this paper should turn to Section 16, the last section.

1 Conventional Programming Languages: Fat and Flabby

Programming languages appear to be in trouble. Each successive language incorporates, with a little cleaning up, all the features of its predecessors plus a few more. Some languages have manuals exceeding 500 pages; others cram a complex description into shorter manuals by using dense formalisms. The Department of Defense has current plans for a committee-designed language standard that could require a manual as long as 1,000 pages. Each new language claims new and fashionable features, such as strong typing or structured control statements, but the plain fact is that few languages make programming sufficiently cheaper or more reliable to justify the cost of producing and learning to use them.

Since large increases in size bring only small increases in power, smaller, more elegant languages such as Pascal continue to be popular. But there is a desperate need for a powerful methodology to help us think about programs, and no conventional language even begins to meet that need. In fact, conventional languages create unnecessary confusion in the way we think about programs.

For twenty years programming languages have been steadily progressing toward their present condition of obesity; as a result, the study and invention of programming languages has lost much of its excitement. Instead, it is now the province of those who prefer to work with thick compendia of details rather than wrestle with new ideas. Discussions about programming languages often resemble medieval debates about the number of angels that can dance on the head of a pin instead of exciting contests between fundamentally differing concepts.

Many creative computer scientists have retreated from inventing languages to inventing tools for describing them. Unfortunately, they have been largely content to apply their elegant new tools to studying the warts and moles of existing languages. After examining the appalling type structure of conventional languages, using the elegant tools developed by Dana Scott, it is surprising that so many of us remain passively content with that structure instead of energetically searching for new ones.

The purpose of this article is twofold; first, to suggest that basic defects in the framework of conventional languages make their expressive weakness and their cancerous growth inevitable, and second, to suggest some alternate avenues of exploration toward the design of new kinds of languages.

2 Models of Computing Systems

Underlying every programming language is a model of a computing system that its programs control. Some models are pure abstractions, some are represented by hardware, and others by compiling or interpretive programs. Before we examine conventional languages more closely, it is useful to make a brief survey of existing models as an introduction to the current universe of alternatives. Existing models may be crudely classified by the criteria outlined below.

2.1 Criteria for Models

2.1.1 Foundations. Is there an elegant and concise mathematical description of the model? Is it useful in proving helpful facts about the behavior of the model? Or is the model so complex that its description is bulky and of little mathematical use?

2.1.2 History sensitivity. Does the model include a notion of storage, so that one program can save information that can affect the behavior of a later program? That is, is the model history sensitive?

2.1.3 Type of semantics. Does a program successively transform states (which are not programs) until a terminal state is reached (state-transition semantics)? Are states simple or complex? Or can a “program” be successively reduced to simpler “programs” to yield a final

“normal form program,” which is the result (reduction semantics)?

2.1.4 Clarity and conceptual usefulness of programs. Are programs of the model clear expressions of a process or computation? Do they embody concepts that help us to formulate and reason about processes?

2.2 Classification of Models

Using the above criteria we can crudely characterize three classes of models for computing systems—simple operational models, applicative models, and von Neumann models.

2.2.1 Simple operational models. Examples: Turing machines, various automata. Foundations: concise and useful. History sensitivity: have storage, are history sensitive. Semantics: state transition with very simple states. Program clarity: programs unclear and conceptually not helpful.

2.2.2 Applicative models. Examples: Church’s lambda calculus [5], Curry’s system of combinators [6], pure Lisp [17], functional programming systems described in this paper. Foundations: concise and useful. History sensitivity: no storage, not history sensitive. Semantics: reduction semantics, no states. Program clarity: programs can be clear and conceptually useful.

2.2.3 Von Neumann models. Examples: von Neumann computers, conventional programming languages. Foundations: complex, bulky, not useful. History sensitivity: have storage, are history sensitive. Semantics: state transition with complex states. Program clarity: programs can be moderately clear, are not very useful conceptually.

The above classification is admittedly crude and debatable. Some recent models may not fit easily into any of these categories. For example, the data-flow languages developed by Arvind and Gostelow [1], Dennis [7], Kosinski [13], and others partly fit the class of simple operational models, but their programs are clearer than those of earlier models in the class and it is perhaps possible to argue that some have reduction semantics. In any event, this classification will serve as a crude map of the territory to be discussed. We shall be concerned only with applicative and von Neumann models.

3 Von Neumann Computers

In order to understand the problems of conventional programming languages, we must first examine their intellectual parent, the von Neumann computer. What is a von Neumann computer? When von Neumann and others conceived it over thirty years ago, it was an elegant, practical, and unifying idea that simplified a number of engineering and programming problems that existed then. Although the conditions that produced its architecture have changed radically, we nevertheless still identify the notion of “computer” with this thirty year old concept.

In its simplest form a von Neumann computer has three parts: a central processing unit (or CPU), a store, and a connecting tube that can transmit a single word between the CPU and the store (and send an address to the store). I propose to call this tube the von Neumann bottleneck. The task of a program is to change the contents of the store in some major way; when one considers that this task must be accomplished entirely by pumping single words back and forth through the von Neumann bottleneck, the reason for its name becomes clear.

Ironically, a large part of the traffic in the bottleneck is not useful data but merely names of data, as well as operations and data used only to compute such names. Before a word can be sent through the tube its address must be in the CPU; hence it must either be sent through the tube from the store or be generated by some CPU operation. If the address is sent from the store, then its address must either have been sent from the store or generated in the CPU, and so on. If, on the other hand, the address is generated in the CPU, it must be generated either by a fixed rule (e.g., “add 1 to the program counter”) or by an instruction that was sent through the tube, in which case its address must have been sent ... and so on.

Surely there must be a less primitive way of making big changes in the store than by pushing vast numbers of words back and forth through the von Neumann bottleneck. Not only is this tube a literal bottleneck for the data traffic of a problem, but, more importantly, it is an intellectual bottleneck that has kept us tied to word-at-a-time thinking instead of encouraging us to think in terms of the larger conceptual units of the task at hand. Thus programming is basically planning and detailing the enormous traffic of words through the von Neumann bottleneck, and much of that traffic concerns not significant data itself but where to find it.

4 Von Neumann Languages

Conventional programming languages are basically high level, complex versions of the von Neumann computer. Our thirty year old belief that there is only one kind of computer is the basis of our belief that there is only one kind of programming language, the conventional—von Neumann—language. The differences between Fortran and Algol 68, although considerable, are less significant than the fact that both are based on the programming style of the von Neumann computer. Although I refer to conventional languages as “von Neumann languages” to take note of their origin and style, I do not, of course, blame the great mathematician for their complexity. In fact, some might say that I bear some responsibility for that problem.

Von Neumann programming languages use variables to imitate the computer’s storage cells; control statements elaborate its jump and test instructions; and assignment statements imitate its fetching, storing, and arithmetic.

The assignment statement is the von Neumann bottleneck of programming languages and keeps us thinking in word-at-a-time terms in much the same way the computer’s bottleneck does.

Consider a typical program; at its center are a number of assignment statements containing some subscripted variables. Each assignment statement produces a one-word result. The program must cause these statements to be executed many times, while altering subscript values, in order to make the desired overall change in the store, since it must be done one word at a time. The programmer is thus concerned with the flow of words through the assignment bottleneck as he designs the nest of control statements to cause the necessary repetitions.

Moreover, the assignment statement splits programming into two worlds. The first world comprises the right sides of assignment statements. This is an orderly world of expressions, a world that has useful algebraic properties (except that those properties are often destroyed by side effects). It is the world in which most useful computation takes place.

The second world of conventional programming languages is the world of statements. The primary statement in that world is the assignment statement itself. All the other statements of the language exist in order to make it possible to perform a computation that must be based on this primitive construct: the assignment statement.

This world of statements is a disorderly one, with few useful mathematical properties. Structured programming can be seen as a modest effort to introduce some order into this chaotic world, but it accomplishes little in attacking the fundamental problems created by the word-at-a-time von Neumann style of programming, with its primitive use of loops, subscripts, and branching flow of control.

Our fixation on von Neumann languages has continued the primacy of the von Neumann computer, and our dependency on it has made non-von Neumann languages uneconomical and has limited their development. The absence of full scale, effective programming styles founded on non-von Neumann principles has deprived designers of an intellectual foundation for new computer architectures. (For a brief discussion of that topic, see Section 15.)

Applicative computing systems’ lack of storage and history sensitivity is the basic reason they have not provided a foundation for computer design. Moreover, most applicative systems employ the substitution operation of the lambda calculus as their basic operation. This operation is one of virtually unlimited power, but its complete and efficient realization presents great difficulties to the machine designer. Furthermore, in an effort to introduce storage and to improve their efficiency on von Neumann computers, applicative systems have tended to become engulfed in a large von Neumann system. For example, pure Lisp is often buried in large extensions with many von Neumann features. The resulting complex systems offer little guidance to the machine designer.

5 Comparison of von Neumann and Functional Programs

To get a more detailed picture of some of the defects of von Neumann languages, let us compare a conventional program for inner product with a functional one written in a simple language to be detailed further on.

5.1 A von Neumann Program for Inner Product

            
              c = 0
for i := 1 step 1 until n do
    c := c + a[i]×b[i]
            
          

Several properties of this program are worth noting: a) Its statements operate on an invisible “state” according to complex rules. b) It is not hierarchical. Except for the right side of the assignment statement, it does not construct complex entities from simpler ones. (Larger programs, however, often do.) c) It is dynamic and repetitive. One must mentally execute it to understand it. d) It computes word-at-a-time by repetition (of the assignment) and by modification (of variable i). e) Part of the data, n, is in the program; thus it lacks generality and works only for vectors of length n. f) It names its arguments; it can only be used for vectors a and b. To become general, it requires a procedure declaration. These involve complex issues (e.g., call-by-name versus call-by-value). g) Its “housekeeping” operations are represented by symbols in scattered places (in the for statement and the subscripts in the assignment). This makes it impossible to consolidate housekeeping operations, the most common of all, into single, powerful, widely useful operators. Thus in programming those operations one must always start again at square one, writing “for i := ...” and “for j := ...” followed by assignment statements sprinkled with i’s and j’s.

5.2 A Functional Program for Inner Product

Def Innerproduct ≡ (Insert +)∘(ApplyToAll ×)∘Transpose

Or, in abbreviated form:

Def IP ≡ (/+)∘(α×)∘Trans.

Composition (∘), Insert (/), and ApplyToAll (α) are functional forms that combine existing functions to form new ones. Thus f∘g is the function obtained by applying first g and then f, and αf is the function obtained by applying f to every member of the argument. If we write f:x for the result of applying f to the object x, then we can explain each step in evaluating Innerproduct applied to the pair of vectors <<1, 2, 3>, <6, 5, 4>> as follows:

            
              IP:<<1,2,3>, <6,5,4>> =
Definition of IP      ⇒ (/+)∘(α×)∘Trans: <<1,2,3>, <6,5,4>>
Effect of composition, ∘   ⇒ (/+):((α×):(Trans:
                                    <<1,2,3>, <6,5,4>>))
            
          

Applying Transpose $\Rightarrow (/+):((\alpha\times): <<1,6>, <2,5>, <3,4>>)$ Effect of ApplyToAll, $\alpha$ $\Rightarrow (/+): <\times: <1,6>, \times: <2,5>, \times: <3,4>>$ Applying $\times$ $\Rightarrow (/+): <6,10,12>$ Effect of Insert, / $\Rightarrow +: <6, +: <10,12>>$ Applying + $\Rightarrow +: <6,22>$ Applying + again $\Rightarrow 28$

Let us compare the properties of this program with those of the von Neumann program.

a) It operates only on its arguments. There are no hidden states or complex transition rules. There are only two kinds of rules, one for applying a function to its argument, the other for obtaining the function denoted by a functional form such as composition, $f \circ g$, or ApplyToAll, $\alpha f$, when one knows the functions $f$ and $g$, the parameters of the forms.

b) It is hierarchical, being built from three simpler functions ($+,\times,\mathrm{Trans}$) and three functional forms $f \circ g$, $\alpha f$, and $/f$.

c) It is static and nonrepetitive, in the sense that its structure is helpful in understanding it without mentally executing it. For example, if one understands the action of the forms $f \circ g$ and $\alpha f$, and of the functions $\times$ and Trans, then one understands the action of $\alpha \times$ and of $(\alpha \times) \circ \mathrm{Trans}$, and so on.

d) It operates on whole conceptual units, not words; it has three steps; no step is repeated.

e) It incorporates no data; it is completely general; it works for any pair of conformable vectors.

f) It does not name its arguments; it can be applied to any pair of vectors without any procedure declaration or complex substitution rules.

g) It employs housekeeping forms and functions that are generally useful in many other programs; in fact, only + and $\times$ are not concerned with housekeeping. These forms and functions can combine with others to create higher level housekeeping operators.

Section 14 sketches a kind of system designed to make the above functional style of programming available in a history-sensitive system with a simple framework, but much work remains to be done before the above applicative style can become the basis for elegant and practical programming languages. For the present, the above comparison exhibits a number of serious flaws in von Neumann programming languages and can serve as a starting point in an effort to account for their present fat and flabby condition.

6 Language Frameworks versus Changeable Parts

Let us distinguish two parts of a programming language. First, its framework which gives the overall rules of the system, and second, its changeable parts, whose existence is anticipated by the framework but whose particular behavior is not specified by it. For example, the for statement, and almost all other statements, are part of Algol’s framework but library functions and user-defined procedures are changeable parts. Thus the framework of a language describes its fixed features and provides a general environment for its changeable features.

Now suppose a language had a small framework which could accommodate a great variety of powerful features entirely as changeable parts. Then such a framework could support many different features and styles without being changed itself. In contrast to this pleasant possibility, von Neumann languages always seem to have an immense framework and very limited changeable parts. What causes this to happen? The answer concerns two problems of von Neumann languages.

The first problem results from the von Neumann style of word-at-a-time programming, which requires that words flow back and forth to the state, just like the flow through the von Neumann bottleneck. Thus a von Neumann language must have a semantics closely coupled to the state, in which every detail of a computation changes the state. The consequence of this semantics closely coupled to states is that every detail of every feature must be built into the state and its transition rules.

Thus every feature of a von Neumann language must be spelled out in stupefying detail in its framework. Furthermore, many complex features are needed to prop up the basically weak word-at-a-time style. The result is the inevitable rigid and enormous framework of a von Neumann language.

7 Changeable Parts and Combining Forms

The second problem of von Neumann languages is that their changeable parts have so little expressive power. Their gargantuan size is eloquent proof of this; after all, if the designer knew that all those complicated features, which he now builds into the framework, could be added later on as changeable parts, he would not be so eager to build them into the framework.

Perhaps the most important element in providing powerful changeable parts in a language is the availability of combining forms that can be generally used to build new procedures from old ones. Von Neumann languages provide only primitive combining forms, and the von Neumann framework presents obstacles to their full use.

One obstacle to the use of combining forms is the split between the expression world and the statement world in von Neumann languages. Functional forms naturally belong to the world of expressions; but no matter how powerful they are they can only build expressions that produce a one-word result. And it is in the statement world that these one-word results must be combined into the overall result. Combining single words is not what we really should be thinking about, but it is a large part of programming any task in von Neumann languages. To help assemble the overall result from single words these languages provide some primitive combining forms in the statement world—the for, while, and if-then-else statements—but the split between the two worlds prevents the combining forms in either world from attaining the full power they can achieve in an undivided world.

A second obstacle to the use of combining forms in von Neumann languages is their use of elaborate naming conventions, which are further complicated by the substitution rules required in calling procedures. Each of these requires a complex mechanism to be built into the framework so that variables, subscripted variables, pointers, file names, procedure names, call-by-value formal parameters, call-by-name formal parameters, and so on, can all be properly interpreted. All these names, conventions, and rules interfere with the use of simple combining forms.

8 APL versus Word-at-a-Time Programming

Since I have said so much about word-at-a-time programming, I must now say something about APL [12]. We owe a great debt to Kenneth Iverson for showing us that there are programs that are neither word-at-a-time nor dependent on lambda expressions, and for introducing us to the use of new functional forms. And since APL assignment statements can store arrays, the effect of its functional forms is extended beyond a single assignment.

Unfortunately, however, APL still splits programming into a world of expressions and a world of statements. Thus the effort to write one-line programs is partly motivated by the desire to stay in the more orderly world of expressions. APL has exactly three functional forms, called inner product, outer product, and reduction. These are sometimes difficult to use, there are not enough of them, and their use is confined to the world of expressions.

Finally, APL semantics is still too closely coupled to states. Consequently, despite the greater simplicity and power of the language, its framework has the complexity and rigidity characteristic of von Neumann languages.

9 Von Neumann Languages Lack Useful Mathematical Properties

So far we have discussed the gross size and inflexibility of von Neumann languages; another important defect is their lack of useful mathematical properties and the obstacles they present to reasoning about programs. Although a great amount of excellent work has been published on proving facts about programs, von Neumann languages have almost no properties that are helpful in this direction and have many properties that are obstacles (e.g., side effects, aliasing).

Denotational semantics [23] and its foundations [20, 21] provide an extremely helpful mathematical understanding of the domain and function spaces implicit in programs. When applied to an applicative language (such as that of the “recursive programs” of [16]), its foundations provide powerful tools for describing the language and for proving properties of programs. When applied to a von Neumann language, on the other hand, it provides a precise semantic description and is helpful in identifying trouble spots in the language. But the complexity of the language is mirrored in the complexity of the description, which is a bewildering collection of productions, domains, functions, and equations that is only slightly more helpful in proving facts about programs than the reference manual of the language, since it is less ambiguous.

Axiomatic semantics [11] precisely restates the inelegant properties of von Neumann programs (i.e., transformations on states) as transformations on predicates. The word-at-a-time, repetitive game is not thereby changed, merely the playing field. The complexity of this axiomatic game of proving facts about von Neumann programs makes the successes of its practitioners all the more admirable. Their success rests on two factors in addition to their ingenuity: First, the game is restricted to small, weak subsets of full von Neumann languages that have states vastly simpler than real ones. Second, the new playing field (predicates and their transformations) is richer, more orderly and effective than the old (states and their transformations). But restricting the game and transferring it to a more effective domain does not enable it to handle real programs (with the necessary complexities of procedure calls and aliasing), nor does it eliminate the clumsy properties of the basic von Neumann style. As axiomatic semantics is extended to cover more of a typical von Neumann language, it begins to lose its effectiveness with the increasing complexity that is required.

Thus denotational and axiomatic semantics are descriptive formalisms whose foundations embody elegant and powerful concepts; but using them to describe a von Neumann language can not produce an elegant and powerful language any more than the use of elegant and modern machines to build an Edsel can produce an elegant and modern car.

In any case, proofs about programs use the language of logic, not the language of programming. Proofs talk about programs but cannot involve them directly since the axioms of von Neumann languages are so unusable. In contrast, many ordinary proofs are derived by algebraic methods. These methods require a language that has certain algebraic properties. Algebraic laws can then be used in a rather mechanical way to transform a problem into its solution. For example, to solve the equation

for $x$ (given that $a+b \neq 0$), we mechanically apply the distributive, identity, and cancellation laws, in succession, to obtain

Thus we have proved that $x = 1$ without leaving the “language” of algebra. Von Neumann languages, with their grotesque syntax, offer few such possibilities for transforming programs.

As we shall see later, programs can be expressed in a language that has an associated algebra. This algebra can be used to transform programs and to solve some equations whose “unknowns” are programs, in much the same way one solves equations in high school algebra. Algebraic transformations and proofs use the language of the programs themselves, rather than the language of logic, which talks about programs.

10 What Are the Alternatives to von Neumann Languages?

Before discussing alternatives to von Neumann languages, let me remark that I regret the need for the above negative and not very precise discussion of these languages. But the complacent acceptance most of us give to these enormous, weak languages has puzzled and disturbed me for a long time. I am disturbed because that acceptance has consumed a vast effort toward making von Neumann languages fatter that might have been better spent in looking for new structures. For this reason I have tried to analyze some of the basic defects of conventional languages and show that those defects cannot be resolved unless we discover a new kind of language framework.

In seeking an alternative to conventional languages we must first recognize that a system cannot be history-sensitive (permit execution of one program to affect the behavior of a subsequent one) unless the system has some kind of state (which the first program can change and the second can access). Thus a history-sensitive model of a computing system must have a state-transition semantics, at least in this weak sense. But this does not mean that every computation must depend heavily on a complex state, with many state changes required for each small part of the computation (as in von Neumann languages).

To illustrate some alternatives to von Neumann languages, I propose to sketch a class of history-sensitive computing systems, where each system: a) has a loosely coupled state-transition semantics in which a state transition occurs only once in a major computation; b) has a simply structured state and simple transition rules; c) depends heavily on an underlying applicative system both to provide the basic programming language of the system and to describe its state transitions.

These systems, which I call applicative state transition (or AST) systems, are described in Section 14. These simple systems avoid many of the complexities and weaknesses of von Neumann languages and provide for a powerful and extensive set of changeable parts. However, they are sketched only as crude examples of a vast area of non-von Neumann systems with various attractive properties. I have been studying this area for the past three or four years and have not yet found a satisfying solution to the many conflicting requirements that a good language must resolve. But I believe this search has indicated a useful approach to designing non-von Neumann languages.

This approach involves four elements, which can be summarized as follows.

a) A functional style of programming without variables. A simple, informal functional programming (FP) system is described. It is based on the use of combining forms for building programs. Several programs are given to illustrate functional programming.

b) An algebra of functional programs. An algebra is described whose variables denote FP functional programs and whose “operations” are FP functional forms, the combining forms of FP programs. Some laws of the algebra are given. Theorems and examples are given that show how certain function expressions may be transformed into equivalent infinite expansions that explain the behavior of the function. The FP algebra is compared with algebras associated with the classical applicative systems of Church and Curry.

c) A formal functional programming system. A formal (FFP) system is described that extends the capabilities of the above informal FP systems. An FFP system is thus a precisely defined system that provides the ability to use the functional programming style of FP systems and their algebra of programs. FFP systems can be used as the basis for applicative state transition systems.

d) Applicative state transition systems. As discussed above. The rest of the paper describes these four elements, gives some brief remarks on computer design, and ends with a summary of the paper.

11 Functional Programming Systems (FP Systems)

11.1 Introduction

In this section we give an informal description of a class of simple applicative programming systems called functional programming (FP) systems, in which “programs” are simply functions without variables. The description is followed by some examples and by a discussion of various properties of FP systems.

An FP system is founded on the use of a fixed set of combining forms called functional forms. These, plus simple definitions, are the only means of building new functions from existing ones; they use no variables or substitution rules, and they become the operations of an associated algebra of programs. All the functions of an FP system are of one type: they map objects into objects and always take a single argument.

In contrast, a lambda-calculus based system is founded on the use of the lambda expression, with an associated set of substitution rules for variables, for building new functions. The lambda expression (with its substitution rules) is capable of defining all possible computable functions of all possible types and of any number of arguments. This freedom and power has its disadvantages as well as its obvious advantages. It is analogous to the power of unrestricted control statements in conventional languages: with unrestricted freedom comes chaos. If one constantly invents new combining forms to suit the occasion, as one can in the lambda calculus, one will not become familiar with the style or useful properties of the few combining forms that are adequate for all purposes. Just as structured programming eschews many control statements to obtain programs with simpler structure, better properties, and uniform methods for understanding their behavior, so functional programming eschews the lambda expression, substitution, and multiple function types. It thereby achieves programs built with familiar functional forms with known useful properties. These programs are so structured that their behavior can often be understood and proven by mechanical use of algebraic techniques similar to those used in solving high school algebra problems.

Functional forms, unlike most programming constructs, need not be chosen on an ad hoc basis. Since they are the operations of an associated algebra, one chooses only those functional forms that not only provide powerful programming constructs, but that also have attractive algebraic properties: one chooses them to maximize the strength and utility of the algebraic laws that relate them to other functional forms of the system.

In the following description we shall be imprecise in not distinguishing between (a) a function symbol or expression and (b) the function it denotes. We shall indicate the symbols and expressions used to denote functions by example and usage. Section 13 describes a formal extension of FP systems (FFP systems); they can serve to clarify any ambiguities about FP systems.

11.2 Description

An FP system comprises the following: 1) a set O of objects; 2) a set F of functions that map objects into objects; 3) an operation, application; 4) a set F of functional forms; these are used to combine existing functions, or objects, to form new functions in F; 5) a set D of definitions that define some functions in F and assign a name to each.

What follows is an informal description of each of the above entities with examples.

11.2.1 Objects, O.

An object $x$ is either an atom, a sequence $\langle x_1,\ldots,x_n\rangle$ whose elements $x_i$ are objects, or $\perp$ (“bottom” or “undefined”). Thus the choice of a set A of atoms determines the set of objects. We shall take A to be the set of nonnull strings of capital letters, digits, and special symbols not used by the notation of the FP system. Some of these strings belong to the class of atoms called “numbers.” The atom $\phi$ is used to denote the empty sequence and is the only object which is both an atom and a sequence.

There is one important constraint in the construction of objects: if $x$ is a sequence with $\perp$ as an element, then $x=\perp$. That is, the “sequence constructor” is “$\perp$-preserving.” Thus no proper sequence has $\perp$ as an element.

Examples of objects

11.2.2 Application.

An FP system has a single operation, application. If $f$ is a function and $x$ is an object, then $f:x$ is an application and denotes the object which is the result of applying $f$ to $x$. $f$ is the operator of the application and $x$ is the operand.

Examples of applications

11.2.3 Functions, F.

All functions $f$ in F map objects into objects and have a bottom-preserving property: $f:\perp=\perp$, for all $f$ in F. Every function in F is either primitive, that is, supplied with the system, or it is defined (see below), or it is a functional form (see below).

It is sometimes useful to distinguish between two cases in which $f:x=\perp$. If the computation of $f:x$ terminates and yields the object $\perp$, we say $f$ is undefined at $x$, that is, $f$ terminates but has no meaningful value at $x$. Otherwise we say $f$ is nonterminating at $x$.

Examples of primitive functions

Our intention is to provide FP systems with widely useful and powerful primitive functions rather than weak ones that could then be used to define useful ones. The following examples define some typical primitive functions, many of which are used in later examples of programs. In the following definitions we use a variant of McCarthy’s conditional expressions [17]; thus we write

instead of McCarthy’s expression

The following definitions are to hold for all objects $x$, $x_i$, $y$, $y_i$, $z$, $z_i$:

Selector functions

and for any positive integer $s$

Thus, for example, $3:\langle A,B,C\rangle=C$ and $2:\langle A\rangle=\perp$. Note that the function symbols 1, 2, etc. are distinct from the atoms 1, 2, etc.

Tail

Identity

Atom atom: $x=x$ is an atom $\to T$; $x\ne\bot\to F$; $\bot$

Equals eq: $x=<y,z>\ \&\ y=z\to T$; $x\ne<y,z>\ \&\ y\ne z\to F$; $\bot$

Null null: $x=x\to\phi\to T$; $x\ne\bot\to F$; $\bot$

Reverse reverse: $x=x\to\phi\to\phi$; $x=<x_1,\ldots,x_n>\to<x_n,\ldots,x_1>$; $\bot$

Distribute from left; distribute from right distl: $x=x=<y,\phi>\to\phi$; $x=<y,<z_1,\ldots,z_n>>\to<<y,z_1>,\ldots,<y,z_n>>$; $\bot$ distr: $x=x=<\phi,y>\to\phi$; $x=<<y_1,\ldots,y_n>,z>\to<<y_1,z>,\ldots,<y_n,z>>$; $\bot$

Length length: $x=x=<x_1,\ldots,x_n>\to n$; $x=\phi\to0$; $\bot$

Add, subtract, multiply, and divide

$+:x=x=<y,z>\ \&\ y,z$ are numbers $\to y+z$; $\bot$

$-:x=x=<y,z>\ \&\ y,z$ are numbers $\to y-z$; $\bot$

$\times:x=x=<y,z>\ \&\ y,z$ are numbers $\to y\times z$; $\bot$

$\div:x=x=<y,z>\ \&\ y,z$ are numbers $\to y\div z$; $\bot$

(where $y\ne0=\bot$)

Transpose trans: $x=x=<\phi,\ldots,\phi>\to\phi$; $x=<x_1,\ldots,x_n>\to<y_1,\ldots,y_m>$; $\bot$ where

$x_i=<x_{i1},\ldots,x_{im}>$ and

$y_j=<x_{1j},\ldots,x_{nj}>$, $1\le i\le n$, $1\le j\le m$.

And, or, not and: $x=x=<T,T>\to T$; $x=<T,F>\vee x=<F,T>\vee x=<F,F>\to F$; $\bot$ etc.

Append left; append right apndl: $x=x=<y,\phi>\to<y>$; $x=<y,<z_1,\ldots,z_n>>\to<y,z_1,\ldots,z_n>$; $\bot$ apndr: $x=x=<\phi,z>\to<z>$; $x=<<y_1,\ldots,y_n>,z>\to<y_1,\ldots,y_n,z>$; $\bot$

Right selectors; Right tail

1r: $x=x=<x_1,\ldots,x_n>\to x_n$; $\bot$

2r: $x=x=<x_1,\ldots,x_n>\ \&\ n\ge2\to x_{n-1}$; $\bot$ etc.

tlr: $x=x=<x_1>\to\phi$; $x=<x_1,\ldots,x_n>\ \&\ n\ge2\to<x_1,\ldots,x_{n-1}>$; $\bot$

Rotate left; rotate right rotl: $x=x\to\phi\to\phi$; $x=<x_1>\to<x_1>$; $x=<x_1,\ldots,x_n>\ \&\ n\ge2\to<x_2,\ldots,x_n,x_1>$; $\bot$ etc.

11.2.4 Functional forms, F.

A functional form is an expression denoting a function; that function depends on the functions or objects which are the parameters of the expression. Thus, for example, if $f$ and $g$ are any functions, then $f\circ g$ is a functional form, the composition of $f$ and $g$, $f$ and $g$ are its parameters, and it denotes the function such that, for any object $x$,

$(f\circ g):x=f:(g:x)$.

Some functional forms may have objects as parameters. For example, for any object $x$, $\bar{x}$ is a functional form, the constant function of $x$, so that for any object $y$

$\bar{x}:y=y=\bot\to\bot;x$.

In particular, $\bot$ is the everywhere-$\bot$ function.

Below we give some functional forms, many of which are used later in this paper. We use $p$, $f$ and $g$ with and without subscripts to denote arbitrary functions; and $x$, $x_1,\ldots,x_n$, $y$ as arbitrary objects. Square brackets [...] are used to indicate the functional form for construction, which denotes a function, whereas pointed brackets $<...>$ denote sequences, which are objects. Parentheses are used both in particular functional forms (e.g. in condition) and generally to indicate grouping.

Composition

$(f\circ g):x=f:(g:x)$

Construction

$[f_1,\ldots,f_n]:x=<f_1:x,\ldots,f_n:x>$ (Recall that since $<\ldots,\bot,\ldots>=\bot$ and all functions are $\bot$-preserving, so is $[f_1,\ldots,f_n]$.)

Condition

$(p\to f,g):x=(p:x)=T\to f:x;\ (p:x)=F\to g:x;\ \bot$

Conditional expressions (used outside of FP systems to describe their functions) and the functional form condition are both identified by “$\to$”. They are quite different although closely related, as shown in the above definitions. But no confusion should arise, since the elements of a conditional expression all denote values, whereas the elements of the functional form condition all denote functions, never values. When no ambiguity arises we omit right-associated parentheses; we write, for example, $p_1\to f_1;p_2\to f_2;g$ for $(p_1\to f_1;(p_2\to f_2;g))$.

Constant (Here $x$ is an object parameter.)

$\bar{x}:y=y=\bot\to\bot;x$

Insert

$/f:x=x=<x_1>\to x_1;x=<x_1,\ldots,x_n>\ \&\ n\ge2$ $\to f:<x_1,/f:<x_2,\ldots,x_n>>;\bot$

If $f$ has a unique right unit $u_f\ne\bot$, where $f:<x,u_f>\in\{x,\bot\}$ for all objects $x$, then the above definition is extended: $/f:\phi=u_f$. Thus

$/+:<4,5,6> = +:<4, +:<5,/+:<6>>>$

$= +:<4,+:<5,6>> = 15$

$/+:\phi=0$

Apply to all

$\alpha f:x=x=\phi\to\phi;$

$x=<x_1,\ldots,x_n>\to<f:x_1,\ldots,f:x_n>;\bot$

Communications of the ACM

August 1978

Volume 21

Number 8 p_i = distl:<m_i,n'> = <<m_i,n_1'>, ... , <m_i,n_s'>> \tag{1} for i = 1, ... , r and $n_j'$ is the jth column of $n$ (the jth row of $n'$). Thus $p_i$, a sequence of row and column pairs, corresponds to the i-th product row. The operator $\alpha\alpha IP$, or $\alpha(\alpha IP)$, causes $\alpha IP$ to be applied to each $p_i$, which in turn causes IP to be applied to each row and column pair in each $p_i$. The result of the last step is therefore the sequence of rows comprising the product matrix. If either matrix is not rectangular, or if the length of a row of $m$ differs from that of a column of $n$, or if any element of $m$ or $n$ is not a number, the result is $\perp$.

This program MM does not name its arguments or any intermediate results; contains no variables, no loops, no control statements nor procedure declarations; has no initialization instructions; is not word-at-a-time in nature; is hierarchically constructed from simpler components; uses generally applicable housekeeping forms and operators (e.g., $\alpha f$, distl, distr, trans); is perfectly general; yields $\perp$ whenever its argument is inappropriate in any way; does not constrain the order of evaluation unnecessarily (all applications of IP to row and column pairs can be done in parallel or in any order); and, using algebraic laws (see below), can be transformed into more "efficient" or into more "explanatory" programs (e.g., one that is recursively defined). None of these properties hold for the typical von Neumann matrix multiplication program.

Although it has an unfamiliar and hence puzzling form, the program MM describes the essential operations of matrix multiplication without overdetermining the process or obscuring parts of it, as most programs do; hence many straightforward programs for the operation can be obtained from it by formal transformations. It is an inherently inefficient program for von Neumann computers (with regard to the use of space), but efficient ones can be derived from it and realizations of FP systems can be imagined that could execute MM without the prodigal use of space it implies. Efficiency questions are beyond the scope of this paper; let me suggest only that since the language is so simple and does not dictate any binding of lambda-type variables to data, there may be better opportunities for the system to do some kind of "lazy" evaluation [9, 10] and to control data management more efficiently than is possible in lambda-calculus based systems.

11.4 Remarks About FP Systems

11.4.1 FP systems as programming languages. FP systems are so minimal that some readers may find it difficult to view them as programming languages. Viewed as such, a function $f$ is a program, an object $x$ is the contents of the store, and $f:x$ is the contents of the store after program $f$ is activated with $x$ in the store. The set of definitions is the program library. The primitive functions and the functional forms provided by the system are the basic statements of a particular programming language. Thus, depending on the choice of primitive functions and functional forms, the FP framework provides for a large class of languages with various styles and capabilities. The algebra of programs associated with each of these depends on its particular set of functional forms. The primitive functions, functional forms, and programs given in this paper comprise an effort to develop just one of these possible styles.

11.4.2 Limitations of FP systems. FP systems have a number of limitations. For example, a given FP system is a fixed language; it is not history sensitive: no program can alter the library of programs. It can treat input and output only in the sense that $x$ is an input and $f:x$ is the output. If the set of primitive functions and functional forms is weak, it may not be able to express every computable function.

An FP system cannot compute a program since function expressions are not objects. Nor can one define new functional forms within an FP system. (Both of these limitations are removed in formal functional programming (FFP) systems in which objects "represent" functions.) Thus no FP system can have a function, apply, such that apply:$<x,y> \equiv x:y$ because, on the left, $x$ is an object, and, on the right, $x$ is a function. (Note that we have been careful to keep the set of function symbols and the set of objects distinct: thus $l$ is a function symbol, and $l$ is an object.)

The primary limitation of FP systems is that they are not history sensitive. Therefore they must be extended somehow before they can become practically useful. For discussion of such extensions, see the sections on FFP and AST systems (Sections 13 and 14).

11.4.3 Expressive power of FP systems. Suppose two FP systems, $\mathrm{FP}_1$ and $\mathrm{FP}_2$, both have the same set of objects and the same set of primitive functions, but the set of functional forms of $\mathrm{FP}_1$ properly includes that of $\mathrm{FP}_2$. Suppose also that both systems can express all computable functions on objects. Nevertheless, we can say that $\mathrm{FP}_1$ is more expressive than $\mathrm{FP}_2$, since every function expression in $\mathrm{FP}_2$ can be duplicated in $\mathrm{FP}_1$, but by using a functional form not belonging to $\mathrm{FP}_2$, $\mathrm{FP}_1$ can express some functions more directly and easily than $\mathrm{FP}_2$.

I believe the above observation could be developed into a theory of the expressive power of languages in which a language A would be more expressive than language B under the following roughly stated conditions. First, form all possible functions of all types in A by applying all existing functions to objects and to each other in all possible ways until no new function of any type can be formed. (The set of objects is a type; the set of continuous functions [T→U] from type T to type U is a type. If $f \in [T \to U]$ and $t \in T$, then $ft$ in U can be formed by applying $f$ to $t$.) Do the same in language B. Next, compare each type in A to the corresponding type in B. If, for every type, A's type includes B's corresponding type, then A is more expressive than B (or equally expressive). If some type of A’s functions is incomparable to B’s, then A and B are not comparable in expressive power.

11.4.4 Advantages of FP systems. The main reason FP systems are considerably simpler than either conventional languages or lambda-calculus-based languages is that they use only the most elementary fixed naming system (naming a function in a definition) with a simple fixed rule of substituting a function for its name. Thus they avoid the complexities both of the naming systems of conventional languages and of the substitution rules of the lambda calculus. FP systems permit the definition of different naming systems (see Sections 13.3.4 and 14.7) for various purposes. These need not be complex, since many programs can do without them completely. Most importantly, they treat names as functions that can be combined with other functions without special treatment.

FP systems offer an escape from conventional word-at-a-time programming to a degree greater even than APL [12] (the most successful attack on the problem to date within the von Neumann framework) because they provide a more powerful set of functional forms within a unified world of expressions. They offer the opportunity to develop higher level techniques for thinking about, manipulating, and writing programs.

12 The Algebra of Programs for FP Systems

12.1 Introduction

The algebra of the programs described below is the work of an amateur in algebra, and I want to show that it is a game amateurs can profitably play and enjoy, a game that does not require a deep understanding of logic and mathematics. In spite of its simplicity, it can help one to understand and prove things about programs in a systematic, rather mechanical way.

So far, proving a program correct requires knowledge of some moderately heavy topics in mathematics and logic: properties of complete partially ordered sets, continuous functions, least fixed points of functionals, the first-order predicate calculus, predicate transformers, weakest preconditions, to mention a few topics in a few approaches to proving programs correct. These topics have been very useful for professionals who make it their business to devise proof techniques; they have published a lot of beautiful work on this subject, starting with the work of McCarthy and Floyd, and, more recently, that of Burstall, Dijkstra, Manna and his associates, Milner, Morris, Reynolds, and many others. Much of this work is based on the foundations laid down by Dana Scott (denotational semantics) and C. A. R. Hoare (axiomatic semantics). But its theoretical level places it beyond the scope of most amateurs who work outside of this specialized field.

If the average programmer is to prove his programs correct, he will need much simpler techniques than those the professionals have so far put forward. The algebra of programs below may be one starting point for such a proof discipline and, coupled with current work on algebraic manipulation, it may also help provide a basis for automating some of that discipline.

One advantage of this algebra over other proof techniques is that the programmer can use his programming language as the language for deriving proofs, rather than having to state proofs in a separate logical system that merely talks about his programs.

At the heart of the algebra of programs are laws and theorems that state that one function expression is the same as another. Thus the law $[f,g] \circ h \equiv [f \circ h, g \circ h]$ says that the construction of $f$ and $g$ (composed with $h$) is the same function as the construction of ($f$ composed with $h$) and ($g$ composed with $h$) no matter what the functions $f$, $g$, and $h$ are. Such laws are easy to understand, easy to justify, and easy and powerful to use. However, we also wish to use such laws to solve equations in which an “unknown” function appears on both sides of the equation. The problem is that if $f$ satisfies some such equation, it will often happen that some extension $f'$ of $f$ will also satisfy the same equation. Thus, to give a unique meaning to solutions of such equations, we shall require a foundation for the algebra of programs (which uses Scott’s notion of least fixed points of continuous functionals) to assure us that solutions obtained by algebraic manipulation are indeed least, and hence unique, solutions.

Our goal is to develop a foundation for the algebra of programs that disposes of the theoretical issues, so that a programmer can use simple algebraic laws and one or two theorems from the foundations to solve problems and create proofs in the same mechanical style we use to solve high-school algebra problems, and so that he can do so without knowing anything about least fixed points or predicate transformers.

One particular foundational problem arises: given equations of the form

where the $p_i$’s and $q_i$’s are functions not involving $f$ and $E_i(f)$ is a function expression involving $f$, the laws of the algebra will often permit the formal “extension” of this equation by one more “clause” by deriving

which, by replacing $E_i(f)$ in (1) by the right side of (2), yields

This formal extension may go on without limit. One question the foundations must then answer is: when can the least $f$ satisfying (1) be represented by the infinite expansion

in which the final clause involving $f$ has been dropped, so that we now have a solution whose right side is free of f’s? Such solutions are helpful in two ways: first, they give proofs of “termination” in the sense that (4) means that f:x is defined if and only if there is an n such that, for every i less than n, p_i:x = F and p_n:x = T and q_n:x is defined. Second, (4) gives a case-by-case description of f that can often clarify its behavior.

The foundations for the algebra given in a subsequent section are a modest start toward the goal stated above. For a limited class of equations its “linear expansion theorem” gives a useful answer as to when one can go from indefinitely extendable equations like (1) to infinite expansions like (4). For a larger class of equations, a more general “expansion theorem” gives a less helpful answer to similar questions. Hopefully, more powerful theorems covering additional classes of equations can be found. But for the present, one need only know the conclusions of these two simple foundational theorems in order to follow the theorems and examples appearing in this section.

The results of the foundations subsection are summarized in a separate, earlier subsection titled “expansion theorems,” without reference to fixed point concepts. The foundations subsection itself is placed later where it can be skipped by readers who do not want to go into that subject.

12.2 Some Laws of the Algebra of Programs

In the algebra of programs for an FP system variables range over the set of functions of the system. The “operations” of the algebra are the functional forms of the system. Thus, for example, [f,g]o h is an expression of the algebra for the FP system described above, in which f, g, and h are variables denoting arbitrary functions of that system. And

[f,g]o h ≡ [f o h, g o h] is a law of the algebra which says that, whatever functions one chooses for f, g, and h, the function on the left is the same as that on the right. Thus this algebraic law is merely a restatement of the following proposition about any FP system that includes the functional forms [f,g] and f o g:

PROPOSITION: For all functions f, g, and h and all objects x, ([f,g]o h):x ≡ [f o h, g o h]:x. PROOF: ([f,g]o h):x = [f,g]: (h:x) by definition of composition = <f:(h:x), g:(h:x)> by definition of construction = <(f o h):x, (g o h):x> by definition of composition = [f o h, g o h]:x by definition of construction □

Some laws have a domain smaller than the domain of all objects. Thus 1°[f,g] ≡ f does not hold for objects x such that g:x = ⊥. We write defined°g →→ 1° [f,g] ≡ f to indicate that the law (or theorem) on the right holds within the domain of objects x for which defined°g:x = T. Where

Def defined ≡ $\bar{T}$ i.e. defined:x ≡ x=⊥ → ⊥; T. In general we shall write a qualified functional equation:

p →→ f ≡ g to mean that, for any object x, whenever p:x = T, then f:x = g:x.

Ordinary algebra concerns itself with two operations, addition and multiplication; it needs few laws. The algebra of programs is concerned with more operations (functional forms) and therefore needs more laws.

Each of the following laws requires a corresponding proposition to validate it. The interested reader will find most proofs of such propositions easy (two are given below). We first define the usual ordering on functions and equivalence in terms of this ordering:

DEFINITION f≤g iff for all objects x, either f:x = ⊥, or f:x = g:x. DEFINITION f ≡ g iff f≤g and g≤f.

It is easy to verify that ≤ is a partial ordering, that f≤g means g is an extension of f, and that f≡g iff f:x = g:x for all objects x. We now give a list of algebraic laws organized by the two principal functional forms involved.

I Composition and construction

            
              I.1   [f_1, ..., f_n]°g ≡ [f_1°g, ..., f_n°g]
I.2   αf°[g_1, ..., g_n] ≡ [f°g_1, ..., f°g_n]
I.3   /f°[g_1, ..., g_n]
      ≡ f°[g_1, /f°[g_2, ..., g_n]]   when n≥2
      ≡ f°[g_1, f°[g_2, ..., f°[g_{n-1}, g_n]...]]
/f°[g] ≡ g
I.4   f°[x,g] ≡ (bu f x)°g
I.5   1° [f_1, ..., f_n] ≤f_1
      s°[f_1, ..., f_s, ..., f_n] ≤f_s for any selector s, s≤n
      defined°f_i (for all i≠s, 1≤i≤n) →→
      s°[f_1, ..., f_n] ≡ f_s

I.5.1   [f_1°1, ..., f_n°n]°[g_1, ..., g_n] ≡ [f_1°g_1, ..., f_n°g_n]
I.6   tl°[f_1] ≤ φ and
      tl°[f_1, ..., f_n] ≤ [f_2, ..., f_n]   for n≥2
      defined°f_1 →→ tl°[f_1] ≡ φ
      and tl°[f_1, ..., f_n] ≡ [f_2, ..., f_n] for n≥2
            
          

I.7 distl°[f, [g_1, ..., g_n]] ≡ [[f,g_1], ..., [f,g_n]] defined°f →→ distl°[f,φ] ≡φ The analogous law holds for distr. I.8 apndl°[f, [g_1, ..., g_n]] ≡ [f,g_1, ..., g_n] null°g →→ apndl°[f,g] ≡ [f] And so on for apndr, reverse, rotl, etc. I.9 [... , 1, ...] ≡ 1 I.10 apndl° [f°g, αf°h] ≡ αf°apndl°[g,h] I.11 pair & not°null°1 →→ apndl°[[1°1,2], distr°[tl°1,2]] ≡ distr

Where $f \& g \equiv \mathrm{and}^{\circ}[f,g];$ pair $\equiv \mathrm{atom} \rightarrow \bar{F}; \mathrm{eq}^{\circ}[\mathrm{length},\bar{2}]$

II Composition and condition (right associated parentheses omitted) (Law II.2 is noted in Manna et al. [16], p. 493.) II.1 $(p \rightarrow f; g)^{\circ}h \equiv p^{\circ}h \rightarrow f^{\circ}h; g^{\circ}h$ II.2 $h^{\circ}(p \rightarrow f; g) \equiv p \rightarrow h^{\circ}f; h^{\circ}g$ II.3 $\mathrm{or}^{\circ}[q,\mathrm{not}^{\circ}q] \rightarrow \rightarrow \mathrm{and}^{\circ}[p,q] \rightarrow f;$ $\mathrm{and}^{\circ}[p,\mathrm{not}^{\circ}q] \rightarrow g; h \equiv p \rightarrow (q \rightarrow f; g); h$ II.3.1 $p \rightarrow (p \rightarrow f; g); h \equiv p \rightarrow f; h$ III Composition and miscellaneous III.1 $\bar{x}^{\circ}f \leq \bar{x}$ defined$f \rightarrow \rightarrow \bar{x}^{\circ}f \equiv \bar{x}$ III.1.1 $\bar{1}^{\circ}f \equiv f^{\circ}\bar{1} \equiv \bar{1}$ III.2 $f^{\circ}\mathrm{id} \equiv \mathrm{id}^{\circ}f \equiv f$ III.3 pair $\rightarrow \rightarrow 1^{\circ}\mathrm{distr} \equiv [1 \circ 1,2]$ also: pair $\rightarrow \rightarrow 1^{\circ}\mathrm{tl} \equiv 2$ etc. III.4 $\alpha(f^{\circ}g) \equiv \alpha f^{\circ} \alpha g$ III.5 $\mathrm{null}^{\circ}g \rightarrow \rightarrow \alpha f^{\circ}g \equiv \bar{\phi}$

IV Condition and construction

IV.1 $[f_1, ..., (p \rightarrow g; h), ..., f_n]$ $\equiv p \rightarrow [f_1, ..., g, ..., f_n]; [f_1, ..., h, ..., f_n]$ IV.1.1 $[f_1, ..., (p_1 \rightarrow g_1; ... ; p_n \rightarrow g_n; h), ..., f_m]$ $\equiv p_1 \rightarrow [f_1, ..., g_1, ..., f_m];$ ... ; $p_n \rightarrow [f_1, ..., g_n, ..., f_m]; [f_1, ..., h, ..., f_m]$

This concludes the present list of algebraic laws; it is by no means exhaustive, there are many others.

Proof of two laws We give the proofs of validating propositions for laws I.10 and I.11, which are slightly more involved than most of the others.

PROPOSITION 1 apndl $\circ [f^{\circ}g, \alpha f^{\circ}h] \equiv \alpha f^{\circ} \mathrm{apndl} \circ [g,h]$ Proof. We show that, for every object $x$, both of the above functions yield the same result. Case 1. $h:x$ is neither a sequence nor $\phi$. Then both sides yield $\bot$ when applied to $x$. Case 2. $h:x = \phi$. Then apndl$[f^{\circ}g, \alpha f^{\circ}h]$: $x$ = apndl: $<f^{\circ}g:x, \phi> = <f:(g:x)>$ $\alpha f^{\circ} \mathrm{apndl} \circ [g,h]$: $x$ = $\alpha f^{\circ} \mathrm{apndl}: <g:x, \phi> = \alpha f:<g:x>$ = $<f:(g:x)>$ Case 3. $h:x = <y_1, ..., y_n>$. Then apndl$[f^{\circ}g, \alpha f^{\circ}h]$: $x$ = apndl: $<f^{\circ}g:x, \alpha f: <y_1, ..., y_n>>$ = $<f:(g:x), f:y_1, ..., f:y_n>$ $\alpha f^{\circ} \mathrm{apndl} \circ [g,h]$: $x$ = $\alpha f^{\circ} \mathrm{apndl}: <g:x, <y_1, ..., y_n>>$ = $\alpha f:<g:x, y_1, ..., y_n>$

PROPOSITION 2

Pair & not\circ null\circ 1 \rightarrow \rightarrow apndl\circ[[1^2, 2], distr\circ[t1\circ 1, 2]] \equiv distr where $f \& g$ is the function: and\circ[f, g], and $f^2 \equiv f\circ f$. Proof. We show that both sides produce the same result when applied to any pair $<x,y>$, where $x \neq \phi$, as per the stated qualification. Case 1. $x$ is an atom or $\bot$. Then distr: $<x,y> = \bot$, since $x \neq \phi$. The left side also yields $\bot$ when applied to $<x,y>$, since tl\circ 1:<x,y> = $\bot$ and all functions are $\bot$-preserving. Case 2. $x = <x_1, ..., x_n>$. Then apndl\circ[[1^2, 2], distr\circ[t1\circ 1, 2]]:<x, y> = apndl: <<1:x, y>, distr: <tl:x, y>> = apndl: <<x_1,y>, \phi> = <<x_1,y>>> \text{ if tl:x = } \phi = apndl: <<x_1,y>, <<x_2,y>, ..., <x_n,y>>> \text{ if tl:x } \neq \phi = <<x_1,y>, ..., <x_n,y>> = distr: <x,y>

12.3 Example: Equivalence of Two Matrix Multiplication Programs We have seen earlier the matrix multiplication program:

Def MM $\equiv \alpha \alpha \mathrm{IP} \circ \alpha \mathrm{distl} \circ \mathrm{distr} \circ [1, \mathrm{trans} \circ 2]$.

We shall now show that its initial segment, MM', where

Def MM' $\equiv \alpha \alpha \mathrm{IP} \circ \alpha \mathrm{distl} \circ \mathrm{distr}$, can be defined recursively. (MM' "multiplies" a pair of matrices after the second matrix has been transposed. Note that MM', unlike MM, gives $\bot$ for all arguments that are not pairs.) That is, we shall show that MM' satisfies the following equation which recursively defines the same function (on pairs):

$f \equiv \mathrm{null}^{\circ}1 \rightarrow \bar{\phi}; \mathrm{apndl}^{\circ}[\alpha \mathrm{IP}^{\circ} \mathrm{distl}^{\circ}[1 \circ 1, 2], f^{\circ}[tl \circ 1, 2]]$.

Our proof will take the form of showing that the following function, R,

Def R $\equiv \mathrm{null}^{\circ}1 \rightarrow \bar{\phi};$ apndl\circ[\alpha \mathrm{IP}^{\circ} \mathrm{distl}^{\circ}[1 \circ 1, 2], \mathrm{MM}'^{\circ}[tl \circ 1, 2]] is, for all pairs $<x,y>$, the same function as MM'. R "multiplies" two matrices, when the first has more than zero rows, by computing the first row of the "product" (with $\alpha \mathrm{IP}^{\circ} \mathrm{distl}^{\circ}[1 \circ 1, 2]$) and adjoining it to the "product" of the tail of the first matrix and the second matrix. Thus the theorem we want is pair $\rightarrow \rightarrow \mathrm{MM}' \equiv \mathrm{R}$, from which the following is immediate:

MM $\equiv \mathrm{MM}' \circ [1, \mathrm{trans} \circ 2] \equiv \mathrm{R} \circ [1, \mathrm{trans} \circ 2]$;

where

Def pair $\equiv \mathrm{atom} \rightarrow \bar{F}; \mathrm{eq}^{\circ}[\mathrm{length}, \bar{2}]$.

THEOREM: pair $\rightarrow \rightarrow \mathrm{MM}' \equiv \mathrm{R}$ where

Def MM' ≡ ααIP ∘ αdistl ∘ distr Def R ≡ null∘1 → φ; apndl∘[αIP∘distl∘[1^2, 2], MM'∘[tl∘1, 2]]

Proof. Case 1. pair & null∘1 →→ MM' ≡ R. pair & null∘1 →→ R ≡ φ̄ by def of R pair & null∘1 →→ MM' ≡ φ̄ since distr: <φ,x> = φ by def of distr and αf:φ = φ by def of Apply to all. And so: ααIP ∘ αdistl ∘ distr: <φ,x> = φ. Thus pair & null∘1 →→ MM' ≡ R. Case 2. pair & not∘null∘1 →→ MM' ≡ R. pair & not∘null∘1 →→ R ≡ R', by def of R and R', where Def R' ≡ apndl∘[αIP∘distl∘[1^2, 2], MM'∘[tl∘1, 2]]. We note that R' ≡ apndl∘[f∘g, αf∘h] where f ≡ αIP∘distl g ≡ [1^2, 2] h ≡ distr∘[tl∘1, 2] αf ≡ α(αIP∘distl) ≡ ααIP∘αdistl (by III.4). Thus, by I.10, R' ≡ αf∘apndl∘[g,h]. Now apndl∘[g,h] ≡ apndl∘[[1^2, 2], distr∘[tl∘1, 2]], thus, by I.11, pair & not∘null∘1 →→ apndl∘[g,h] ≡ distr. And so we have, by (1), (2), (3) and (4), pair & not∘null∘1 →→ R ≡ R' ≡ αf∘distr ≡ ααIP∘αdistl∘distr ≡ MM'. Case 1 and Case 2 together prove the theorem. □

12.4 Expansion Theorems

In the following subsections we shall be “solving” some simple equations (where by a “solution” we shall mean the “least” function which satisfies an equation). To do so we shall need the following notions and results drawn from the later subsection on foundations of the algebra, where their proofs appear.

12.4.1 Expansion. Suppose we have an equation of the form

(E1) where E(f) is an expression involving f. Suppose further that there is an infinite sequence of functions f_i for i = 0, 1, 2, ..., each having the following form:

(E2) where the p_i's and q_i's are particular functions, so that E has the property:

(E3)

Then we say that E is expansive and has the f_i's as approximating functions.

If E is expansive and has approximating functions as in (E2), and if f is the solution of (E1), then f can be written as the infinite expansion

(E4) meaning that, for any x, f:x ≠ ⊥ iff there is an n ≥ 0 such that (a) p_i:x = F for all i < n, and (b) p_n:x = T, and (c) q_n:x ≠ ⊥. When f:x ≠ ⊥, then f:x = q_n:x for this n. (The foregoing is a consequence of the “expansion theorem”.) 12.4.2 Linear expansion. A more helpful tool for solving some equations applies when, for any function h,

(LE1) and there exist p_i and q_i such that

for i = 0, 1, 2, ... (LE2) and

(LE3) Under the above conditions E is said to be linearly expansive. If so, and f is the solution of

(LE4) then E is expansive and f can again be written as the infinite expansion

(LE5) using the p_i's and q_i's generated by (LE1) and (LE2).

Although the p_i's and q_i's of (E4) or (LE5) are not unique for a given function, it may be possible to find additional constraints which would make them so, in which case the expansion (LE5) would comprise a canonical form for a function. Even without uniqueness these expansions often permit one to prove the equivalence of two different function expressions, and they often clarify a function’s behavior.

12.5 A Recursion Theorem

Using three of the above laws and linear expansion, one can prove the following theorem of moderate generality that gives a clarifying expansion for many recursively defined functions.

Recursion theorem: Let f be a solution of

(1) where

(2) and p, g, h, i, j are any given functions, then f ≡ p → g; p°j → Q(g); ... ; p°j^n → Q^n(g); ... (3) (where Q^n(g) is h°[i, Q^{n-1}(g)°j], and j^n is j°j^{n-1} for n ≥ 2) and Q^n(g) ≡ /h ° [i, i°j, ..., i°j^{n-1}, g°j^n]. (4)

Proof. We verify that p → g, Q(f) is linearly expansive. Let p_n, q_n and k be any functions. Then

Thus if p_0 ≡ p and q_0 ≡ g, then (5) gives p_1 ≡ p°j and q_1 = Q(g) and in general gives the following functions satisfying (LE2) p_n ≡ p°j^n and q_n ≡ Q^n(g). (6)

Finally,

Thus (5) and (6) verify (LE2) and (7) verifies (LE3), with E_1 ≡ Q. If we let E(f) ≡ p → g; Q(f), then we have (LE1); thus E is linearly expansive. Since f is a solution of f ≡ E(f), conclusion (3) follows from (6) and (LE5). Now

Result (8) is the second conclusion (4). □

12.5.1 Example: correctness proof of a recursive factorial function. Let f be a solution of f ≡ eq0 → \bar{I}; ×°[id, f°s] where

Def s ≡ −°[id, \bar{I}] (subtract 1).

Then f satisfies the hypothesis of the recursion theorem with p ≡ eq0, g ≡ \bar{I}, h ≡ ×, i ≡ id, and j ≡ s. Therefore f ≡ eq0 → \bar{I}; ... ; eq0°s^n → Q^n(\bar{I}); ...

and

Q^n(\bar{I}) ≡ /× ° [id, id°s, ..., id°s^{n-1}, \bar{I}°s^n].

Now id°s^k ≡ s^k by III.2 and eq0°s^n →→ \bar{I}°s^n ≡ \bar{I} by III.1, since eq0°s^n:x implies defined°s^n:x; and also eq0°s^n:x ≡ eq0: (x − n) ≡ x=n. Thus if eq0°s^n: x = T, then x = n and

Q^n(\bar{I}): n = n × (n − 1) × ... × (n − (n − 1)) × (\bar{I}: (n − n)) = n!.

Using these results for \bar{I}°s^n, eq0°s^n, and Q^n(\bar{I}) in the previous expansion for f, we obtain f:x ≡ x=0 → l; ... ; x=n → n × (n − 1) × ... × 1 × 1; ...

Thus we have proved that f terminates on precisely the set of nonnegative integers and that it is the factorial function thereon.

12.6 An Iteration Theorem

This is really a corollary of the recursion theorem. It gives a simple expansion for many iterative programs.

Iteration theorem: Let f be the solution (i.e., the least solution) of f ≡ p → g; h°f°k then f ≡ p → g; p°k → h°g°k; ... ; p°k^n → h^n°g°k^n; ...

Proof. Let h' ≡ h°2, i' ≡ id, f' ≡ k, then f ≡ p → g; h'°[i', f°j'] since h°2°[id, f°k] ≡ h°f°k by I.5 (id is defined except for ⊥, and the equation holds for ⊥). Thus the recursion theorem gives f ≡ p → g; ... ; p°k^n → Q^n(g); ...

where

Q^n(g) ≡ h°2°[id, Q^{n-1}(g)°k] ≡ h°Q^{n-1}(g)°k ≡ h^n°g°k^n by I.5 □

12.6.1 Example: Correctness proof for an iterative factorial function. Let f be the solution of f ≡ eq0°1 → 2; f°[s°1, ×] where Def s ≡ −°[id, \bar{I}] (substract 1). We want to prove that f:<x,1> = x! iff x is a nonnegative integer. Let p ≡ eq0°1, g ≡ 2, h ≡ id, k ≡ [s°1, ×]. Then f ≡ p → g; h°f°k and so f ≡ p → g; ... ; p°k^n → g°k^n; ...

            
              by the iteration theorem, since h^n ≡ id. We want to show that pair →→ k^n ≡ [a_n, b_n] holds for every n ≥ 1, where a_n ≡ s^n°1      (3)
b_n ≡ /× ° [s^{n-1}°1, ..., s°1, 1, 2]      (4)
            
          

Now (2) holds for n = 1 by definition of k. We assume it holds for some n ≥ 1 and prove it then holds for n + 1. Now pair →→ k^{n+1} ≡ k°k^n ≡ [s°1, ×]°[a_n, b_n] (5) since (2) holds for n. And so pair $\longrightarrow k^{n+1} \equiv [s^o a_n, \times^o[a_n, b_n]]$ by I.1 and I.5 (6)

To pass from (5) to (6) we must check that whenever $a_n$ or $b_n$ yield $\perp$ in (5), so will the right side of (6). Now

Combining (6), (7), and (8) gives pair $\longrightarrow k^{n+1} \equiv [a_{n+1}, b_{n+1}].$

Thus (2) holds for $n = 1$ and holds for $n + 1$ whenever it holds for $n$, therefore, by induction, it holds for every $n \geq 1$. Now (2) gives, for pairs:

defined$k^n \longrightarrow p \circ k^n \equiv eq0 \circ 1 \circ [a_n, b_n]$

defined$k^n \longrightarrow g \circ k^n$

(both use I.5). Now (1) tells us that $f:<x, l>$ is defined iff there is an $n$ such that $p \circ k^i:<x, l> = F$ for all $i < n$, and $p \circ k^n:<x, l> = T$, that is, by (10), $eq0 \circ s^n : x = T$, i.e., $x = n$; and $g \circ k^n:<x, l>$ is defined, in which case, by (11),

which is what we set out to prove.

12.6.2 Example: proof of equivalence of two iterative programs. In this example we want to prove that two iteratively defined programs, $f$ and $g$, are the same function. Let $f$ be the solution of

Let $g$ be the solution of

Then, by the iteration theorem:

where (letting $r^0 \equiv id$ for any $r$), for $n = 0, 1, ...$

Now, from the above, using I.5, defined$2 \longrightarrow p_n \equiv p \circ k^n \circ 1$ defined$h^n \circ 2 \longrightarrow p'_n \equiv p \circ k^n \circ 1$ defined$k^n \circ 1 \longrightarrow q_n \equiv q'_n \equiv h^n \circ 2$

Thus defined$h^n \circ 2 \longrightarrow$ defined$2 \equiv \bar{T}$ defined$h^n \circ 2,\longrightarrow p_n \equiv p'_n$ and

since $p_n$ and $p'_n$ provide the qualification needed for $q_n \equiv q'_n \equiv h^n \circ 2$.

Now suppose there is an $x$ such that $f:x \not\equiv g:x$. Then there is an $n$ such that $p_i : x = p'_i : x = F$ for $i < n$, and $p_n : x \not\equiv p'_n : x$. From (12) and (13) this can only happen when $h^n \circ 2 : x = \perp$. But since $h$ is $\perp$-preserving, $h^m \circ 2 : x = \perp$ for all $m \geq n$. Hence $f : x = g : x = \perp$ by (14) and (15). This contradicts the assumption that there is an $x$ for which $f : x \not\equiv g : x$. Hence $f \equiv g$.

This example (by J. H. Morris, Jr.) is treated more elegantly in [16] on p. 498. However, some may find that the above treatment is more constructive, leads one more mechanically to the key questions, and provides more insight into the behavior of the two functions.

12.7 Nonlinear Equations

The preceding examples have concerned "linear" equations (in which the "unknown" function does not have an argument involving itself). The question of the existence of simple expansions that "solve" "quadratic" and higher order equations remains open.

The earlier examples concerned solutions of $f \equiv E(f)$, where $E$ is linearly expansive. The following example involves an $E(f)$ that is quadratic and expansive (but not linearly expansive).

12.7.1 Example: proof of idempotency ([16] p. 497). Let $f$ be the solution of

We wish to prove that $f \equiv f^2$. We verify that $E$ is expansive (Section 12.4.1) with the following approximating functions:

First we note that $p \longrightarrow f_n \equiv id$ and so

Now $E(f_0) \equiv p \rightarrow id; \bar{1}^2 \circ h \equiv f_1$, and

Thus $E$ is expansive by (4) and (5); so by (2) and Section 12.4.1 (E4)

But (6), by the iteration theorem, gives

Now, if $p : x = T$, then $f : x = x = f^2 : x$, by (1). If $p : x = F$, then

= f:(f \circ h:x) = f:(f:x) \quad \text{by (7)} = f^2:x.

If p:x is neither T nor F, then f:x = \bot = f^2:x. Thus f \equiv f^2.

12.8 Foundations for the Algebra of Programs

Our purpose in this section is to establish the validity of the results stated in Section 12.4. Subsequent sections do not depend on this one, hence it can be skipped by readers who wish to do so. We use the standard concepts and results from [16], but the notation used for objects and functions, etc., will be that of this paper.

We take as the domain (and range) for all functions the set O of objects (which includes \bot) of a given FP system. We take F to be the set of functions, and F to be the set of functional forms of that FP system. We write E(f) for any function expression involving functional forms, primitive and defined functions, and the function symbol f; and we regard E as a functional that maps a function f into the corresponding function E(f). We assume that all f \in F are \bot-preserving and that all functional forms in F correspond to continuous functionals in every variable (e.g., [f, g] is continuous in both f and g). (All primitive functions of the FP system given earlier are \bot-preserving, and all its functional forms are continuous.)

Definitions. Let E(f) be a function expression. Let f_0 \equiv \bot f_{i+1} \equiv p_0 \rightarrow q_0; ... ; p_i \rightarrow q_i; \bot \quad \text{for } i = 0, 1, ...

where p_i, q_i \in F. Let E have the property that

E(f_i) \equiv f_{i+1} \quad \text{for } i = 0, 1, ...

Then E is said to be expansive with the approximating functions f_i. We write f \equiv p_0 \rightarrow q_0; ... ; p_n \rightarrow q_n; ...

to mean that $f \equiv \lim_i \{ f_i \}$, where the f_i have the form above. We call the right side an infinite expansion of f. We take f:x to be defined iff there is an n \geq 0 such that (a) p_i:x = F for all i < n, and (b) p_n:x = T, and (c) q_n:x is defined, in which case f:x = q_n:x.

Expansion theorem: Let E(f) be expansive with approximating functions as above. Let f be the least function satisfying f \equiv E(f).

Then f \equiv p_0 \rightarrow q_0; ... ; p_n \rightarrow q_n; ...

Proof. Since E is the composition of continuous functionals (from F) involving only monotonic functions (\bot-preserving functions from F) as constant terms, E is continuous ([16] p. 493). Therefore its least fixed point f is $\lim_i \{ E^i(\bot) \} \equiv \lim_i \{ f_i \}$ ([16] p. 494), which by definition is the above infinite expansion for f.

Definition. Let E(f) be a function expression satisfying the following:

E(h) \equiv p_0 \rightarrow q_0; E_1(h) \quad \text{for all } h \in F \tag{LE1} where p_i \in F and q_i \in F exist such that

E_1(p_i \rightarrow q_i; h) \equiv p_{i+1} \rightarrow q_{i+1}; E_1(h) \quad \text{for all } h \in F \text{ and } i = 0, 1, ... \tag{LE2} and

E_1(\bot) \equiv \bot. \tag{LE3}

Then E is said to be linearly expansive with respect to these p_i's and q_i's.

Linear Expansion Theorem: Let E be linearly expansive with respect to p_i and q_i, i = 0, 1, ... . Then E is expansive with approximating functions f_0 \equiv \bot \tag{1} f_{i+1} \equiv p_0 \rightarrow q_0; ... ; p_i \rightarrow q_i; \bot. \tag{2}

Proof. We want to show that E(f_i) = f_{i+1} for any i \geq 0. Now

E(f_0) \equiv p_0 \rightarrow q_0; E_1(\bot) \equiv p_0 \rightarrow q_0; \bot \equiv f_1 \tag{3} \quad \text{by (LE1) (LE3) (1).}

Let i > 0 be fixed and let f_i \equiv p_0 \rightarrow q_0; w_1 \tag{4a} w_1 \equiv p_1 \rightarrow q_1; w_2 \tag{4b} etc. w_{i-1} \equiv p_{i-1} \rightarrow q_{i-1}; \bot. \tag{4-}

Then, for this i > 0

E(f_i) \equiv p_0 \rightarrow q_0; E_1(f_i) \quad \text{by (LE1)} E_1(f_i) \equiv p_1 \rightarrow q_1; E_1(w_1) \quad \text{by (LE2) and (4a)} E_1(w_1) \equiv p_2 \rightarrow q_2; E_1(w_2) \quad \text{by (LE2) and (4b)} etc.

E_1(w_{i-1}) \equiv p_i \rightarrow q_i; E_1(\bot) \quad \text{by (LE2) and (4-)} \equiv p_i \rightarrow q_i; \bot \quad \text{by (LE3)}

Combining the above gives

E(f_i) \equiv f_{i+1} \quad \text{for arbitrary } i > 0, \text{ by (2).} \tag{5}

By (3), (5) also holds for i = 0; thus it holds for all i \geq 0. Therefore E is expansive and has the required approximating functions. □

Corollary. If E is linearly expansive with respect to p_i and q_i, i = 0, 1, ... , and f is the least function satisfying f \equiv E(f) \tag{LE4} then f \equiv p_0 \rightarrow q_0; ... ; p_n \rightarrow q_n; ... . \tag{LE5}

12.9 The Algebra of Programs for the Lambda Calculus and for Combinators

Because Church's lambda calculus [5] and the system of combinators developed by Schönfinkel and Curry [6] are the primary mathematical systems for representing the notion of application of functions, and because they are more powerful than FP systems, it is natural to enquire what an algebra of programs based on those systems would look like.

The lambda calculus and combinator equivalents of FP composition, $f \circ g$, are