The Essence of Algol^{1}

John C. Reynolds Syracuse University, Syracuse, NY, U.S.A.

Abstract

Although Algol 60 has been uniquely influential in programming language design, its descendants have been significantly different than their prototype. In this paper, we enumerate the principles that we believe embody the essence of Algol, describe a model that satisfies these principles, and illustrate this model with a language that, while more uniform and general, retains the character of Algol.

1. The Influence of Models of Algol

Among programming languages, Algol 60 [1] has been uniquely influential in the theory and practice of language design. It has inspired a variety of models which have in turn inspired a multitude of languages. Yet, almost without exception, the character of these languages has been quite different than that of Algol itself. To some extent, the models failed to capture the essence of Algol and gave rise to languages that reflected that failure.

One main line of development centered around the work of P. J. Landin, who devised an abstract language of applicative expressions [2] and showed that Algol could be translated into this language [3]. This work was influenced by McCarthy’s Lisp [4] and probably by unpublished ideas of C. Strachey; in turn it led to more elaborate models such as those of the Vienna group [5]. Later many of its basic ideas, often considerably transformed, reappeared in the denotational semantics of Scott and Strachey [6].

In [2], after giving a functional description of applicative expressions, Landin presented a state-transition machine, called the SECD machine, for their evaluation. Then in [3] he extended applicative expressions to “imperative applicative expressions” by introducing assignment and a label-like mechanism called the J-operator. The imperative applicative expressions were not described functionally, but by an extension of the SECD machine called the “sharing machine.” In later models, such as that of the Vienna group, sharing was elucidated by introducing a state component usually called the “store” or “memory.”

1Work supported by National Science Foundation Grant MCS-8017577 and U.S. Army Contract DAAK80-80-C-0529. First appeared in J. W. de Bakker and J. C. van Vliet, editors, Algorithmic Languages, pages 345–372, Proceedings of the International Symposium on Algorithmic Languages, Amsterdam, October 1981.

North-Holland, Amsterdam. Reprinted in Algol-like Languages, ed. P. W. O’Hearn and R. D. Tennent, vol.

1, pp. 67–88, Birkhäuser, 1997.

For our present concerns, three aspects of Landin’s model are especially significant. First, the variety of values that can be assigned to variables is the same as the variety that can be denoted by identifiers or passed as parameters. Landin does not emphasize this fact; it is simply a direct consequence of the typelessness of imperative applicative expressions. Second, no distinction is made between assignments to variables and assignments to locations embedded within data structures. Again, this is inherent in the nature of the model, in which variables themselves are locations embedded within the data structures of the sharing machine.

Finally, since operands are evaluated before operators, the basic method of parameter passing is call by value, and call by name is described in terms of call by value using parameterless functions (in contrast to the Algol 60 report [1], where call by value is described in terms of call by name using appropriately initialized local variables). This approach apparently stems from the view that undefined values do not “exist,” so that a function cannot map an undefined value into a defined value (as in Lisp, where the conditional must be regarded as a special form rather than a function). This is in contrast with the more recent view of Scott that an undefined value is as legitimate as any other; its only peculiarity is being least in a partial ordering that must be respected by functions.

Directly or indirectly, Landin’s model was the basis for a number of programming languages, including his own Iswim [7], Evans and Wozencraft’s Pal [8], and my Gedanken [9]. Less obviously, the model influenced Algol 68 [10], despite the significant distinction that this language is highly typed. All of these languages inherited from the model the characteristics described above: anything that can be passed as a parameter can be assigned to a variable, there is no fundamental distinction between assignments to variables and to components of data structures, and call by value is either the only or the basic mode of parameter transmission.

As a consequence, all of these languages are significantly different from Algol; in certain respects they are closer to the spirit of Lisp. They are all subject to the criticism of references made by Hoare [11]. (Strictly speaking, only Algol 68 and Gedanken use the reference concept, but Hoare’s criticism is equally applicable to the sharing or L-value approach used in Iswim and Pal.)

Moreover, except for Algol 68, none of these languages obey a stack discipline. It would require a clever compiler to make any use of a stack during program execution, and even then it would be difficult for a programmer to foresee when such use would occur.

In Algol 68, a stack discipline is obtained by imposing the restriction that a procedure value becomes undefined upon exit from any block in which a global variable of the procedure is declared. However, this restriction is imposed for the specific purpose of rescuing the stack; a stack discipline is not a natural consequence of the basic character of the language.

Another line of development stemming from Algol 60 has led to languages such as Pascal [12] and its descendants, e.g. Euclid [13], Mesa [14], and Ada [15], which are significantly lower-level than Algol. Each of these languages seriously restricts the block or procedure mechanism of Algol by eliminating features such as call by name, dynamic arrays, or procedure parameters.

I am not familiar enough with the history of these languages to do more than speculate about the influence of models. However, a desire to be “closer to the machine” than Algol 60 seems evident from the abandonment of features requiring inefficient or “clever” implementations. In this respect, implementations themselves can be thought of as models influencing language design.

In addition, the influence of program-proving formalisms, particularly the work of Hoare [16], is clear. An axiomatic definition of Pascal [17] seems to have influenced that language, and the axiomatization of Euclid [13] was a major goal of its design.

Since Hoare’s treatment of procedures [18] does not encompass call by name, procedure parameters, or aliasing, it may account for the weakening of the procedure mechanism in some of these languages. Certainly the view of procedures given by this kind of axiomatization is profoundly different than the copy rule.

2. Some Principles

The preceding somewhat biased history is intended to motivate a new model that I believe captures the essence of Algol and can be used to develop a more uniform and general “Idealized Algol” retaining the character of its prototype. Although its genesis lies in the definition of the simple imperative language given in [19], the crux of the model is a treatment of procedures and block structure developed by F. J. Oles and myself.

This paper only describes the basic nature of the model, and it avoids the mathematical sophistication, involving universal algebra and category theory, that is needed to reveal its elegance. A complete and mathematically literate description is given in [20].

It should be emphasized that the description of “Idealized Algol” in this paper is extremely tentative and only intended to illustrate the model.

Before delving into the details, we state the principles that we believe embody the essence of Algol:

1. Algol is obtained from the simple imperative language by imposing a procedure mechanism based on a fully typed, call-by-name lambda calculus.

In other words, Landin was right in perceiving the lambda calculus underlying Algol, but wrong in embracing call by value rather than call by name.

The qualification “fully typed” indicates agreement with van Wijngaarden that all type errors should be syntactic errors, and that this goal requires a syntax with an infinite number of phrase classes, themselves possessing grammatical or (more abstractly) algebraic structure. (I believe that this characteristic will be the most influential and long lasting aspect of Algol 68.) The failure of this property for Algol 60 is a design mistake, not part of its essence.

When carried to the extreme, this principle suggests that the lambda calculus is the source of all identifier binding. More precisely, except for syntactic sugar (language constructs that can be defined as abbreviations in terms of more basic constructs, as the for statement is defined in the Algol 60 Report), the only binding mechanism should be the lambda expression.

2. There are two fundamentally different kinds of type: data types, each of which denotes a set of values appropriate for certain variables and expressions, and phrase types, each of which denotes a set of meanings appropriate for certain identifiers and phrases.

This syntactic distinction reflects that fact that in Algol values (which can be assigned to variables) are inherently different from meanings (which can be denoted by identifiers and phrases, and passed as parameters). Thus Algol-like languages contradict the principle of completeness [9].

Moreover, in Algol itself data types are limited to unstructured types such as integer or Boolean, while structuring mechanisms such as procedures and arrays are only applicable to phrase types.

3. The order of evaluation for parts of expressions, and of implicit conversions between data or phrase types, should be indeterminate, but the meaning of the language, at an appropriate level of abstraction, should be independent of this indeterminacy.

By “appropriate” we mean a level of abstraction where overflow and roundoff are ignored and termination with an error message is regarded as equivalent to nontermination. This principle prohibits expressions with side effects such as assignments to nonlocal variables or jumps to nonlocal labels, but not expressions that cause error stops.

If types are described grammatically, the indeterminacy of implicit conversions will cause ambiguity. For example, in a context calling for a real expression, 3 + 4 might be parsed as either

[figure: <real exp>; <integer exp>; <integer exp>; <integer exp>; +; or; <real exp>; <real exp>; <real exp>; <integer exp>; <integer exp>; +]

Except for overflow and (with unfortunate hardware) roundoff, both parses should have the same meaning.

4. Facilities such as procedure definition, recursion, and conditional and case constructions should be uniformly applicable to all phrase types.

This principle leads to procedures whose calls are procedures, but under a call-by-name regime such procedures do not violate a stack discipline in the way that, for example, function-returning functions in Gedanken violate such a discipline. More interestingly, this principle leads to conditional variables and procedures whose calls are variables; indeed arrays can be regarded as a special case of the latter.

5. The language should obey a stack discipline, and its definition should make this discipline obvious.

Almost any form of language definition can be divided into primary and secondary parts, e.g.

Primary  Secondary
Denotational Semantics Domain equations  Semantic equations
Algebraic Semantics  Definition of the target Definition of the target
algebra carrier  algebra operations
Operational Semantics Definition of the set of Definition of the state-
states of the interpreter transition function

By “should make the stack discipline obvious” we mean that the stack discipline should be a consequence of the primary part of the language definition. Specifically, the primary part should show that the execution of a command never changes the “shape” of the store, i.e. the aspect of the store that reflects storage allocation.

3. Data Types and Expressions

To stay close to Algol 60, we take {integer, real, Boolean} as the set of data types. To introduce an implicit conversion from integer to real, we define the partial ordering

• real integer •  • Boolean

and say that τ is a subtype of τ′ when τ ≤ τ′.

For each data type τ there is a phrase type τ exp(ression), and these phrase types inherit the subtype relation of the data types:

• real exp integer exp •  • Boolean exp

When θ ≤ θ′ we again say that θ is a subtype of θ′, now meaning that any phrase of type θ can appear in any context requiring a phrase of type θ′, e.g. any integer expression can occur in any context requiring a real expression.

A type assignment is a function from some finite set of identifiers to phrase types. To describe the syntax of our language we will use phrase-class names of the form <θ, π>, where θ is a phrase type and π is a type assignment, to denote the set of phrases P such that

1. The identifiers occurring free in P belong to the domain of π.

2. When its free identifiers are given the phrase types indicated by π, P has phrase type θ.

We will describe syntax by production schemas (in the spirit though not the notation of van Wijngaarden) in which the metavariables τ, θ, π, and ι range over data types, phrase types, type assignments, and identifiers, respectively. A fragment of an appropriate syntax for expressions is

<θ, π> ::= <θ′, π> when θ′ ≤ θ

<θ, π> ::= ι when ι ∈ dom(π) and π(ι) = θ

<integer exp, π> ::= 0 | 1 | <integer exp, π> + <integer exp, π>

<real exp, π> ::= 0.5 | <real exp, π> + <real exp, π>

<Boolean exp, π> ::= true | false | <τ exp, π> = <τ exp, π> | <Boolean exp, π> and <Boolean exp, π>

(Here dom(π) denotes the domain of the type assignment π.) This is an abstract syntax to the extent that precedence considerations are ignored. One could “concretize” it by adding parentheses around the right side of each production, but a realistic concrete syntax would require far fewer parentheses. In fact, we will use fewer parentheses in our examples of programs, trusting the reader’s intuition to supply the missing ones sensibly.

In the first two production schemas θ ranges over all phrase types, not just the types of expressions introduced so far. The first schema shows the purpose of the subtype relationship. The second shows that an identifier assigned some phrase type can always be used as a phrase of that type.

In accordance with Principle 3, the syntax is ambiguous (aside from parenthesization considerations), but this ambiguity must not result in ambiguous meanings. An appropriate method for insuring this requirement is described in [19]; it requires that the syntax possess a property that might be called “minimal typing”:

For any phrase P and type assignment π, if there is any θ such that P ∈ <θ, π>, then there is a minimal θ_{0} such that P ∈ <θ, π> if and only if θ_{0} ≤ θ.

(When a phrase-class name is used as a set it stands for the set of all phrases that can be derived from that phrase-class name.)

To prohibit expressions with side effects, we will forbid any occurrence of commands within expressions (except in vacuous contexts such as parameters of constant procedures) and insist that the bodies of function procedures be expressions. Actually, this is unnecessarily Draconian; one would like to permit block expressions, as in Algol W [22], but restricted to avoid side effects. However, this topic is beyond the scope of this paper.

4. The Simple Imperative Language

The next step is to introduce variables for each data type. But here we encounter a surprising complication. As a consequence of Principle 4, we want to have conditional variables. For example, when n is an integer variable and x is a real variable, we should be able to write if p then n else x on either side of an assignment statement. When used on the right side, this phrase must be considered as a real expression, since when p is false it can produce a noninteger value. But when used on the left side, it must be considered an integer variable, since when p is true it cannot accept a noninteger value. Thus there are variables that accept a different data type than they produce.

The first step in dealing with this situation is to realize that, in addition to variables, which accept and produce values, and expressions, which only produce values, it is natural to introduce phrases called acceptors, which only accept values. Thus for each data type τ, we will have the phrase type τ acc(eptor). The subtype relation for acceptors is the dual of the subtype relation for data types. For example, since integer is a subtype of real, integer values can be implicitly converted into real values, so that a real acceptor can be used in any context requiring an integer acceptor, i.e. real acc ≤ integer acc.

The second step is to categorize variables separately by the data types that they accept and produce. Thus for each pair of data types τ_{1} and τ_{2}, we have the phrase type τ_{1} (accepting) τ_{2} (producing) var(iable), which is a subtype of both τ_{1} acc and τ_{2} exp. Among variables themselves, τ_{1}τ_{2} var is a subtype of τ′_{1}τ′_{2} var when τ_{1} acc is a subtype of τ′_{1} acc and τ_{2} exp is a subtype of τ′_{2} exp; i.e. when the data types satisfy τ′_{1} ≤ τ_{1} and τ_{2} ≤ τ′_{2}.

The case construction for variables raises the same difficulty as the conditional. But a further problem arises if the empty construction case n of () is permitted. Of course, it would not be unreasonable to prohibit this construction, but it is consistent to view it as a phrase whose phrase type univ(ersal) is a subtype of all phrase types. All phrases of this type have the meaning “undefined,” which implicitly converts into the undefined element ⊥ of the domain of meanings of any other phrase type.

The only other phrase type needed to describe the simple imperative language is comm(and). (Throughout this paper, we will speak of commands rather than statements.) In summary, the phrase types of the simple imperative language, which we will call primitive phrase types, are

τ exp τ acc τ_{1}τ_{2} var comm univ

and the subtype relation is the least partial ordering such that

τ ≤ τ′ implies τ exp ≤ τ′ exp

τ′ ≤ τ implies τ acc ≤ τ′ acc

τ′_{1} ≤ τ_{1} and τ_{2} ≤ τ′_{2} implies τ_{1}τ_{2} var ≤ τ′_{1}τ′_{2} var

τ_{1}τ_{2} var ≤ τ_{1} acc

τ_{1}τ_{2} var ≤ τ_{2} exp

univ ≤ θ

An appropriate syntax is:

<comm, π> ::= skip | <τ acc, π> := <τ exp, π> | <comm, π>; <comm, π> | while <Boolean exp, π> do <comm, π>

<θ, π> ::= if <Boolean exp, π> then <θ, π> else <θ, π>

| case <integer exp, π> of (<θ, π>, …, <θ, π>)

In the last two lines, θ stands for any phrase type, including the nonprimitive types to be introduced later. The minimal typing property holds for these productions if, in the partial ordering of phrase types, every finite set with an upper bound has a least upper bound. In fact, the achievement of this property for primitive phrase types was the real goal of the arguments about acceptors, variables, and univ at the beginning of this section.

For mathematical simplicity, it is tempting to make the partial ordering of phrase types into a lattice by introducing a phrase type ns (nonsense), of which all phrase types are subtypes. However, although a nonsense type simplifies certain theoretical techniques, as in [19], it is not germane to the purposes of this paper.

A complete semantic definition of the simple imperative language is given in [19]; here we will only delineate the basic nature of such a definition by giving its domain equations. For each phrase type θ, there is a domain of meanings D_{θ}, and for each type assignment π, there is a domain of environments Env_{π}, which is the product ∏_{ι ∈ dom(π)} D_{π(ι)} of the domains for the type of each identifier in dom(π). Then for each phrase class <θ, π> there is a semantic function from phrases to environments to meanings, i.e. μ_{θ,π} ∈ <θ, π> → (Env_{π} → D_{θ}).

For direct semantics D_{comm} is a domain of state transitions, i.e. S → S_{⊥}, where S is the set of states of the store (hereafter simply called states), and S_{⊥} indicates the formation of a domain by adding an undefined element ⊥ (denoting nontermination) to the set S. Similarly D_{τ exp} is S → (V_{τ})_{⊥}, where V_{integer} is the set of integers, V_{real} is the set of real numbers, and V_{Boolean} is the set {true, false}.

There are two ways of treating variables. The more conventional is to say that, for each data type, a state has a component mapping an appropriate set of “L-values” (or “names” or “references” or “abstract addresses”) into values of that data type, i.e.

S = (L_{integer} → V_{integer}) × (L_{real} → V_{real}) × (L_{Boolean} → V_{Boolean}).

Then D_{τ var} is S → (L_{τ})_{⊥}.

A preferable approach, however, avoids any commitment to a notion such as L-values or references, and more clearly reveals the relationship among variables, acceptors, and expressions. One regards the meaning of an acceptor as a function mapping each value into the state transformation caused by assigning that value to the acceptor, so that D_{τ acc} = V_{τ} → (S → S_{⊥}). Then the meaning of a variable is a pair of functions describing its meanings in its dual roles of acceptor and expression, so that D_{τ_{1}τ_{2} var} = D_{τ_{1} acc} × D_{τ_{2} exp}. The implicit conversion functions from variables to acceptors and expressions are the projections from D_{τ_{1}τ_{2} var} to D_{τ_{1} acc} and D_{τ_{2} exp}.

These two views of variables provide a nice example of the way in which formal definition can influence language design. As long as we do not impose any structure involving L-values or references upon states, there is no danger of defining anything, such as call by reference, that involves these concepts. On the other hand, the more abstract approach opens the door to features, such as doublets in Pop-2 [21] or implicit “references” in Gedanken [9], that define a variable by giving arbitrary procedures for accepting and producing values.

In fact, the more abstract treatment of variables makes no commitment at all to the structure of states; S is a parameter of the semantics that can sensibly stand for any set at all. To emphasize this generality, we make S an explicit argument of D_{θ} and Env_{π}, and regard the semantics of a phrase as a family of functions, indexed by S, from environments to meanings:

If P ∈ <θ, π> then μ_{θ,π}(P)(S) ∈ Env_{π}(S) → D_{θ}(S),

where

Env_{π}(S) = ∏_{ι∈dom(π)} D_{π(ι)}(S),

D_{comm}(S) = S → S_{⊥}, D_{τ exp}(S) = S → (V_{τ})_{⊥}, D_{τ acc}(S) = V_{τ} → D_{comm}(S), D_{τ_{1}τ_{2} var}(S) = D_{τ_{1} acc}(S) × D_{τ_{2} exp}(S).

However, although the semantics of a phrase is a family of environment-to-meaning functions, the members of this family must bear a close relationship to one another. Roughly speaking, whenever a state set S can be “expanded” into another state set S′, the semantics of a phrase for S must be related to its semantics for S′.

To make the notion of expansion precise, we first introduce some useful notation:

Identity and composition of functions We write I_{S} for the identity function on S, and · for functional composition in diagrammatic order (so that (f · g)(x) = g(f(x)) ).

Strict extension When f ∈ S → S′_{⊥}, we write f_{⊥⊥} for the ⊥-preserving extension of f to S_{⊥} → S′_{⊥}. When f ∈ S → S′, we write f_{⊥} for the ⊥-preserving extension of f to S_{⊥} → S′_{⊥}.

Identity and composition of state-transition functions We write J_{S} for the identity injection from S to S_{⊥}. When f, g ∈ S → S_{⊥}, we write f ∗ g for f · (g_{⊥⊥}) ∈ S → S_{⊥}.

Diagonalization We write D_{S} for the continuous function from S → S → S_{⊥} to S → S_{⊥} such that D_{S}(h)(σ) = h(σ)(σ).

In the last definition (and later in this paper) we assume that → is right associative and that function (and procedure) application is left associative.

Then we define an expansion of S to S′ to be a pair ⟨g, G⟩ of functions g ∈ S′ → S, G ∈ (S → S_{⊥}) → (S′ → S′_{⊥}) such that

1. G is continuous and ⊥-preserving.

2. G(J_{S}) = J_{S′}.

3. When f_{1}, f_{2} ∈ S → S_{⊥}, G(f_{1} ∗ f_{2}) = G(f_{1}) ∗ G(f_{2}).

4. When f ∈ S → S_{⊥}, g · f = G(f) · (g_{⊥}).

5. When h ∈ S → S → S_{⊥}, G(D_{S}(h)) = D_{S′}(g · h · G).

Intuitively, g maps each state in S′ into the member of S that is “embedded” within it, while G maps each state-transition function in S → S_{⊥} into the state-transition function in S′ → S′_{⊥} that “simulates” it.

More precisely, an expansion of S to S′ induces, for each phrase type θ, a function in D_{θ}(S) → D_{θ}(S′) that maps meanings appropriate to S into meanings appropriate to S′. If we write D_{θ}(⟨g, G⟩) for the function in D_{θ}(S) → D_{θ}(S′) induced by ⟨g, G⟩, then

D_{comm}(⟨g, G⟩) = G,

D_{τ exp}(⟨g, G⟩)(e ∈ S → (V_{τ})_{⊥}) = g · e,

D_{τ acc}(⟨g, G⟩)(a ∈ V_{τ} → D_{comm}(S)) = a · G,

D_{τ_{1}τ_{2} var}(⟨g, G⟩)(⟨a, e⟩) = ⟨D_{τ_{1} acc}(⟨g, G⟩)(a), D_{τ_{2} exp}(⟨g, G⟩)(e)⟩.

By pointwise extension, an expansion of S to S′ induces, for each type assignment π, a function in Env_{π}(S) → Env_{π}(S′) that maps environments appropriate to S into environments appropriate to S′. If we write Env_{π}(⟨g, G⟩) for the function in Env_{π}(S) → Env_{π}(S′) induced by ⟨g, G⟩, then

Env_{π}(⟨g, G⟩)(η ∈ Env_{π}(S))(ι) = D_{π(ι)}(⟨g, G⟩)(η(ι)).

We can now state the fundamental relationship between the semantics of a phrase for different state sets: If P is a phrase in <θ, π> and ⟨g, G⟩ is an expansion of S to S′, then

μ_{θ,π}(P)(S) · D_{θ}(⟨g, G⟩) = Env_{π}(⟨g, G⟩) · μ_{θ,π}(P)(S′).

(In fact, properties (1) to (5) of expansions are sufficient to make this relationship hold for all phrases of the simple imperative language.)

As shown in [20], this development can be described succinctly in the language of category theory. State sets and expansions form a category Σ, with ⟨I_{S}, I_{S→S_{⊥}}⟩ as the identity on S and ⟨g, G⟩ · ⟨g′, G′⟩ = ⟨g′ · g, G · G′⟩ as composition. Then each D_{θ} and Env_{π} is a functor from Σ to the category Dom of domains and continuous functions, and the fundamental relationship given above is that μ_{θ,π}(P) is a natural transformation from Env_{π} to D_{θ}.

5. Procedures and Their Declarations

To provide procedures, we introduce a binary operation → upon phrase types. A phrase of type θ_{1} → θ_{2} denotes a procedure whose calls are phrases of type θ_{2} containing an actual parameter of type θ_{1}. Multiple parameters will be treated by Currying, i.e.

P (A_{1}, …, A_{n}) means P (A_{1}) ⋯ (A_{n})

and

λ(F_{1}: θ_{1}, …, F_{n}: θ_{n}). B means λF_{1}: θ_{1}. · · · λF_{n}: θ_{n}. B.

This way of desugaring multiple parameters is sufficiently well known that we will not formalize it.

Thus what would conventionally be called a proper procedure (or τ function procedure) accepting parameters of types θ_{1}, …, θ_{n} is regarded as a phrase of type θ_{1} → ⋯ → θ_{n} → comm (or θ_{1} → ⋯ → θ_{n} → τ exp). Note that parameterless proper procedures are simply commands (as was recognized in Algol W [22], where an actual parameter of this type could be any command), and parameterless function procedures are simply expressions (which is a natural and pleasant consequence of call by name).

It is easy to see that if θ_{2} ≤ θ′_{2}, then θ_{1} → θ_{2} ≤ θ_{1} → θ′_{2}. Less obviously, if θ′_{1} ≤ θ_{1}, then θ_{1} → θ_{2} ≤ θ′_{1} → θ_{2}. For example, since an integer expression can appear in any context requiring a real expression, a proper procedure accepting a real expression can also accept any integer expression and is therefore meaningful in any context requiring a proper procedure accepting an integer expression. Thus real exp → comm ≤ integer exp → comm.

In summary, the set of phrase types is the smallest set containing the primitive phrase types and closed under the binary operation →. Its subtype relation is the least partial ordering satisfying the properties given earlier plus

θ′_{1} ≤ θ_{1} and θ_{2} ≤ θ′_{2} implies θ_{1} → θ_{2} ≤ θ′_{1} → θ′_{2}.

In brief, → is antimonotone in its first operand and monotone in its second operand.

A suitable syntax for application (procedure statements and function designators), abstraction (lambda expressions), and least fixed-points (recursion) is

<θ_{2}, π> ::= <θ_{1} → θ_{2}, π>(<θ_{1}, π>)
<θ_{1} → θ_{2}, π> ::= λι: θ_{1}. <θ_{2}, [π | ι : θ_{1}]>
<θ, π> ::= rec <θ → θ, π>

Here [π | ι : θ_{1}] denotes the type assignment similar to π except that it maps ι into θ_{1}, i.e.

dom([π | ι : θ_{1}]) = dom(π) ∪ {ι},
[π | ι : θ_{1}](ι) = θ_{1},
[π | ι : θ_{1}](ι′) = π(ι′) when ι′ ≠ ι.

For later developments, it will be convenient to extend this notation by using the following abbreviations:

[π | ι_{1} : θ_{1} | ⋯ | ι_{n} : θ_{n}] = [⋯ [π | ι_{1} : θ_{1}] ⋯ | ι_{n} : θ_{n}],
[ι_{1} : θ_{1} | ⋯ | ι_{n} : θ_{n}] = [ϵ | ι_{1} : θ_{1} | ⋯ | ι_{n} : θ_{n}],

where ϵ is the type assignment with empty domain. Note that the latter form can be used to notate any type assignment explicitly.

The obvious approach to semantics is to take the meanings of phrases of type θ_{1} → θ_{2} to be continuous functions from meanings of phrases of type θ_{1} to meanings of phrases of type θ_{2}, i.e. D_{θ_{1}→θ_{2}}(S) = D_{θ_{1}}(S) → D_{θ_{2}}(S). However, when we consider variable declarations in the next section we will find that this approach conflicts with Principle 5.

Even in the absence of a definite semantics, meaning can be clarified by equivalences. We write P ≡_{θ,π} Q to indicate that μ_{θ,π}(P) = μ_{θ,π}(Q), i.e. that P and Q have the same meaning when regarded as phrases in <θ, π>.

First we have the standard equivalences of the (typed) lambda calculus. If P ∈ <θ_{2}, [π | ι: θ_{1}]> and Q ∈ <θ_{1}, π>, then

(λι: θ_{1}. P)(Q) ≡_{θ_{2},π} P |_{ι→Q}, (beta reduction)

where P |_{ι→Q} denotes the result of substituting Q for the free occurrences of ι in P, with appropriate renaming of bound identifiers in P. If P ∈ <θ_{ι} → θ_{2}, π> and ι ∉ dom(π), then

λι: θ_{1}. (P (ι)) ≡_{θ_{1}→θ_{2},π} P. (eta reduction)

Next, an obvious equivalence describes the fixed-point property of rec. If P ∈ <θ → θ, π>, then

rec P ≡_{θ,π} P (rec P).

Finally, two equivalences relate procedures to the conditional construction. If P ∈ <Booleanexp, π>, Q, R ∈ <θ_{1} → θ_{2}, π> and S ∈ <θ_{1}, π>, then

(if P then Q else R)(S) ≡_{θ_{2},π} if P then Q(S) else R(S).

If P ∈ <Booleanexp, π>, Q, R ∈ <θ_{2}, [π | ι: θ_{1}]>, and ι ∉ dom(π), then

λι: θ_{1}. if P then Q else R ≡_{θ_{1}→θ_{2},π} if P then λι: θ_{1}. Q else λι: θ_{1}. R.

For the declaration of procedures, we prefer the let and letrec notation of Landin [3] to that of Algol 60; it is uniformly applicable to all phrase types (not just procedures), it distinguishes clearly between nonrecursive and recursive cases, and it doesn’t make declarations look like commands. The syntax is

<θ, π> ::= let ι_{1} be <θ_{1}, π> & ⋯ & ι_{n} be <θ_{n}, π> in <θ, π′>
| letrec ι_{1} : θ_{1} be <θ_{1}, π′> & ⋯ & ι_{n} : θ_{n} be <θ_{n}, π′> in <θ, π′>

where π′ = [π | ι_{1}: θ_{1} | ⋯ | ι_{n}: θ_{n}]. (Note that the types θ_{1}, …, θ_{n} must be stated explicitly for letrec but not let.)

This notation can be defined as syntactic sugar in terms of application, abstraction, and rec. The nonrecursive let construction is straightforward. If P_{1} ∈ <θ_{1}, π>, …, P_{n} ∈ <θ_{n}, π>, and P ∈ <θ, π′>, then

let ι_{1} be P_{1} & ⋯ & ι_{n} be P_{n} in P ≡_{θ,π}

(λι_{1}: θ_{1}. · · · λι_{n}: θ_{n}. P)(P_{1}) ⋯ (P_{n})

This equivalence can be used to remove all occurrences of let from a program without changing its meaning. Although it is formally similar to the equivalence given by Landin [3], it has a different import since call by name is being used instead of call by value. For example, if E is an integer expression, then let x be E in 3 has the same meaning as (λx: integer exp. 3)(E) which, by beta reduction, has the same meaning as 3, even when E is nonterminating. If x and y are integer variables, let z be x in (x := 4; y := z) has the same meaning as (λz: integer integer var. (x := 4; y := z))(x) which, by beta reduction, has the same meaning as x := 4; y := x.

To treat the recursive letrec construction, we will first define the nonmultiple case and then show how multiple declarations can be reduced to this case. For the nonmultiple case we follow Landin: If P_{1} ∈ <θ_{1}, [π | ι_{1}: θ_{1}]> and P ∈ <θ, [π | ι_{1}: θ_{1}]>, then

letrec ι_{1}: θ_{1} be P_{1} in P ≡_{θ,π} (λι_{1}: θ_{1}. P)(rec λι_{1}: θ_{1}. P_{1}).

For the multiple case we give an equivalence, suggested by F. J. Oles, that avoids the use of products of phrase types. If P_{1} ∈ <θ_{1}, π′>, …, P_{n} ∈ <θ_{n}, π′>, and P ∈ <θ, π′>, where π′ = [π | ι_{1}: θ_{1} | ⋯ | ι_{n}: θ_{n}], then

letrec ι_{1} : θ_{1} be P_{1} & ⋯ & ι_{n} : θ_{n} be P_{n} in P ≡_{θ,π}
letrec ι_{1} : θ_{1} be
(letrec ι_{2} : θ_{2} be P_{2} & ⋯ & ι_{n} : θ_{n} be P_{n} in P_{1})
in (letrec ι_{2} : θ_{2} be P_{2} & ⋯ & ι_{n} : θ_{n} be P_{n} in P).

6. Variable Declarations

To declare variables, we use the syntax

<comm, π> ::= new τ var ι in <comm, [π | ι : ττ var]>

(Note that declared variables always accept and produce the same data type.) However, since this construction involves binding we want to desugar it into a form in which the binding is done by a lambda expression. The solution is to introduce the more basic construction

<comm, π> ::= newvar(τ)<ττvar → comm, π>

and to define

new τ var ι in P ≡_{comm,π} newvar(τ)λι: ττ var. P,

where P ∈ <comm, [π | ι : ττ var]>.

Semantically, variable declarations raise a serious problem. The conventional approach is to permit the set S of store states to contain states with different numbers of L-values, and to define variable declaration to be an operation that adds an L-value to the state. For example, one might take a state to be a collection of strings of values for each data type

S = V_{integer}^{∗} × V_{real}^{∗} × V_{Boolean}^{∗},

and define the declaration of a τ variable to be an operation that adds one more component to the string of values of type τ.

The problem with this view is that it violates Principle 5 by obscuring the stack discipline. Execution of a command containing variable declarations permanently alters the shape of the store, i.e. the number of L-values or the length of the component strings. In effect, the store is a heap without a garbage collector, rather than a stack. It is hardly surprising that this kind of model inspired languages that are closer to Lisp than to Algol.

Our solution to this difficulty takes advantage of the fact that the semantics of a phrase is a family of environment-to-meaning functions for different sets of states. Instead of using a single set containing states of different shapes and regarding variable declaration as changing the shape of a state, we use sets of states with the same shape and regard variable declaration as changing the set of states. Specifically, if C is new τ var ι in C′, then the semantics of C for a state set S depends upon the semantics of C′ for the state set S × V_{τ}. Thus, since the semantics of C for S maps an environment into a mapping in D_{comm}(S) = S → S_{⊥}, it is obvious that executing C will not change the shape of a state.

To make this precise, suppose C′ ∈ <comm, [π | ι: ττ var]>, so that C ∈ <comm, π>. We first note that S and S × V_{τ} are related by the expansion ⟨g, G⟩ in which g is the function from S × V_{τ} to S such that g(⟨σ, v⟩) = σ and G is the function from S → S_{⊥} to (S × V_{τ}) → (S × V_{τ})_{⊥} such that

G(c)(⟨σ, v⟩) = if c(σ) =⊥ then ⊥ else ⟨c(σ), v⟩.

This expansion induces a function Env_{π}(⟨g, G⟩) from Env_{π}(S) to Env_{π}(S × V_{τ}).

Let e be the function from S×V_{τ} to (V_{τ})_{⊥} such that e(⟨σ, v⟩) = v, and a be a function from V_{τ} to (S × V_{τ}) → (S × V_{τ})_{⊥} such that a(v′)(⟨σ, v⟩) = ⟨σ, v′⟩. Then ⟨a, e⟩ ∈ D_{ττ var}(S × V_{τ}) is an appropriate meaning for the variable being declared.

To obtain the meaning of new τ var ι in C′ for the state set S and an environment η ∈ Env_{π}(S), we use Env_{π}(⟨g, G⟩) to map η into Env_{π}(S × V_{τ}) and then alter the resulting environment to map ι into ⟨a, e⟩, obtaining

η′ = [Env_{π}(⟨g, G⟩)(η) | ι : <a, e>].

Then we take the meaning of C′ for the state set S ×V_{τ} and the environment η′, and compose this meaning, which is a state-transition function from S × V_{τ} to (S × V_{τ})_{⊥}, with a function that initializes the new variable to some standard initial value init_{τ} ∈ V_{τ}, and a function which forgets the final value of the variable:

μ_{comm,π}(new τ var ι in C′)(S)(η) =
(λσ. ⟨σ, init_{τ}⟩) · μ_{comm,[π|ι:ττ var]}(C′)(S × V_{τ})(η′) · (g_{⊥}).

(Our unAlgol-like use of a standard initialization is the simplest way to avoid the abyss of nondeterminate semantics.)

However, this approach to variable declaration has a radical effect on the notion of what procedures mean that forces us to abandon the conventional idea that D_{θ_{1}→θ_{2}}(S) = D_{θ_{1}}(S) → D_{θ_{2}}(S). The problem is that variable declarations may intervene between the point of definition of a procedure and its point of call, so that the state set S′ relevant to the call is different than the state set S at the point of definition, though there must be an expansion from S to S′.

As a consequence, a member p of D_{θ_{1}→θ_{2}}(S) must be a family of functions describing the meaning of a procedure for different S′. Moreover, each of these functions, in addition to accepting the usual argument in D_{θ_{1}}(S′) must also accept an expansion from S to S′ that shows how the states of S are embedded in the richer states of S′.

As one might expect, the members of the family p must satisfy a stringent relationship (which can be expressed by saying that p is an appropriate kind of natural transformation). A precise definition is the following (where expand(S, S′) is the set of expansions from S to S′): p ∈ D_{θ_{1}→θ_{2}}(S) if and only if p is a state-set-indexed family of functions,

p(S′) ∈ expand(S, S′) × D_{θ_{1}}(S′) → D_{θ_{2}}(S′),

such that, for all ⟨g, G⟩ ∈ expand(S, S′), ⟨g′, G′⟩ ∈ expand(S′, S′′), and a ∈ D_{θ_{1}}(S′),

D_{θ_{2}}(⟨g′, G′⟩)(p(S′)(⟨g, G⟩, a)) = p(S′′)(⟨g′ · g, G · G′⟩, D_{θ_{1}}(⟨g′, G′⟩)(a)).

To make D_{θ_{1}→θ_{2}}(S) into a domain, its members are ordered pointwise, i.e. p_{1} ⊑ p_{2} if and only if (∀S′) p_{1}(S′) ⊑ p_{2}(S′).

Finally, we must say how an expansion from S to S′ induces a function from D_{θ_{1}→θ_{2}}(S) to D_{θ_{1}→θ_{2}}(S′): If ⟨g, G⟩ ∈ expand(S, S′) and p ∈ D_{θ_{1}→θ_{2}}(S), then D_{θ_{1}→θ_{2}}(⟨g, G⟩)(p) ∈ D_{θ_{1}→θ_{2}}(S′) is the family p′ of functions such that, for all S′′, ⟨g′, G′⟩ ∈ expand(S′, S′′), and a ∈ D_{θ_{1}}(S′′),

p′(S′′)(⟨g′, G′⟩, a) = p(S′′)(⟨g′ · g, G · G′⟩, a).

A full description of this kind of semantics is presented in [20]; in particular abstraction and application are defined and the validity of beta and eta reduction is proved. This is done by showing that the above definition of → makes Dom^{Σ} (the category of functors and natural transformations from Σ to Dom) into a Cartesian closed category, which is an extremely general model of the typed lambda calculus.

Despite its apparent complexity, much of which is due to our avoidance of category theory in this exposition, this kind of semantics shows that our language is obtained by adding the typed lambda calculus to the simple imperative language in a way that imposes a stack discipline. The essential idea is that the procedure mechanism involves a “hidden abstraction” over a family of semantics indexed by state sets.

We suspect that this kind of hidden abstraction may arise in other situations where a formal language is extended by adding a procedural or definitional mechanism based on the lambda calculus. The generality of the idea is indicated by the fact that the definition of → and the proof that Dom^{Σ} is Cartesian closed do not depend upon the nature of the category Σ.

7. Call by Value

In the Algol 60 report, call by value is explained in terms of call by name by saying that a value specification is equivalent to a certain modification of the procedure body. In fact, however, this modification involves only the body and not the formal parameter list, so that it is equally applicable to commands that are not procedure bodies. In essence, call by value is really an operation on commands rather than parameters.

To capture this idea, we introduce the syntax

<comm, [π | ι : τ exp]> ::= τ value ι in <comm, [π | ι : ττ var]>

which is desugared by the equivalence

τ value ι in C ≡_{comm,[π|ι:τ exp]}
new τ var ι′ in (ι′ := ι; (λι: ττ var. C)(ι′)),

where C ∈ <comm, [π | ι: ττ var]> and ι′ ∉ dom(π) ∪ {ι}. (This is only a generalization of call by value for proper procedures; an analogous generalization for function procedures would require block expressions.)

Notice that τ value ι in C has a peculiar binding structure: the first occurrence of ι is a binder whose scope is C, yet this occurrence is itself free. (A similar phenomenon occurs in the conventional notation for indefinite integration.)

Call by result, as in Algol W [22], can obviously be treated similarly.

8. Arrays

Arrays of the kind used in Algol 60 can be viewed as procedures whose calls are variables. Thus an n-dimensional τ array is a phrase of type

\underbrace{integer exp → ⋯ → integer exp}_{n times} → ττ var.

(Notice that this is a phrase type. If arrays were introduced as a data type, one could assign to entire array variables (as in APL) but not to their elements.)

The declaration of such arrays is a straightforward generalization of variable declarations, and can be desugared similarly. The details are left to the reader.

Unfortunately, this kind of array, like that of Algol, has the shortcoming that it does not carry its own bounds information. A possible solution is to introduce, for each n ≥ 1, a phrase type array(n, τ) that is a subtype of the type displayed above, and to provide bound-extraction operations that act upon these new phrase types. The concept of array in [28] could be treated similarly.

9. Labels

Since all one can do with a label ι is to jump to it, its meaning can be taken to be the meaning of goto ι. Thus labels can be viewed as identifiers of phrase type comm, and goto ι can simply be written as ι.

However, as suggested in Algol 68, labels denote a special kind of command, which we will call a completion, that has the property that it never returns control to its successor. If completions are not distinguished as a separate phrase type, it becomes difficult for either a human reader or a compiler to analyze control flow, particularly when procedure parameters denoting completions are only specified to be commands. To avoid this, we introduce compl(etion) as an additional phrase type that is a subtype of comm (so that completions can always be used as commands but not vice-versa).

Thus labels are identifiers of phrase type compl. Moreover, the production schemas for conditional and case constructions, procedure application, and recursion provide a variety of compound phrases of type compl. This variety can be enriched by the following syntax, in which various ways of forming commands are used to form completions:

<compl, π> ::= <comm, π>; <compl, π>
| new τ var ι in <compl, [π | ι : ττ var]>
| newvar(τ) <ττ var → compl, π>
<compl, [π | ι : τ exp]> ::= τ value ι in <compl, [π | ι : ττ var]>

Two more schemas suffice to describe commands and completions in which labels are declared in an Algol-like notation:

<comm, π> ::= <comm, π′>; ι_{1}: <comm, π′>; ⋯; ι_{n}: <comm, π′>

where ι_{1}, …, ι_{n} are distinct and π′ = [π | ι_{1}: compl | ⋯ | ι_{n}: compl];

<compl, π> ::= <comm, π′>; ι_{1}: <comm, π′>; ⋯; ι_{n}: <compl, π′>

where ι_{1}, …, ι_{n} are distinct and π′ = [π | ι_{1}: compl ; ⋯ | ι_{n}: compl]. Since these declarative constructions involve binding, we must desugar them into more basic forms. For this purpose, we introduce an escape operation that is a parameterless variant of Landin’s J-operator [3].

<comm, π> ::= escape <compl → comm, π>.

This operation can be described in terms of a conventional label declaration: If P ∈ <compl → comm, π> and ι ∉ dom(π), then

escape P ≡_{comm,π} (P (ι) ; ι: skip).

Our present goal, however, is the reverse. To describe label declarations in terms of escapes, we proceed in two steps. First, we describe a label-declaring command in terms of a label-declaring completion by adding a final jump to an enclosing escape: If ι_{1}, …, ι_{n}, ι are distinct identifiers, π′ = [π | ι_{1}: compl | ⋯ | ι_{n}: compl], C_{0}, …, C_{n} ∈ <comm, π′>, and ι ∉ dom(π), then

C_{0} ; ι_{1}: C_{1} ; ⋯; ι_{n}: C_{n} ≡_{comm,π}
escape λι: compl. (C_{0} ; ι_{1}: C_{1} ; ⋯; ι_{n}: (C_{n} ; ι)).

Then we describe a label-declaring completion in terms of recursive definitions: If ι_{1}, …, ι_{n} are distinct identifiers, π′ = [π | ι_{1}: compl | ⋯ | ι_{n}: compl], C_{0}, …, C_{n−1} ∈ <comm, π′>, and K ∈ <compl, π′>, then

C_{0} ; ι_{1}: C_{1} ; ⋯; ι_{n}: K ≡_{compl,π}

letrec ι_{1}: compl be (C_{1} ; ι_{2}) & ⋯ & ι_{n−1}: compl be (C_{n−1} ; ι_{n})
& ι_{n}: compl be K
in (C_{0} ; ι_{1}).

We have chosen to desugar the Algol notation for declaring labels because of its familiarity. Other, possibly preferable, notations can be treated similarly; for example, Zahn’s event facility [29] can be described by escapes without recursion. Actually, the wisest approach might be to avoid all syntactic sugar and simply provide escapes.

Semantically, the introduction of labels requires a change from direct to continuation semantics, which will not be discussed here. In [20] it is shown that hidden abstraction on state sets can be extended to continuation semantics, though with a different notion of expansion.

10. Products and Sums

Although procedures and arrays are the only ways of building compound phrase types in Algol, most newer languages provide some kind of product of types, such as records in Algol W or class members in Simula 67 [26], and often some kind of sum of types, such as unions in Algol 68 or variant records in Pascal. In this section we will explore the addition of such mechanisms to our illustrative language.

Since we distinguish two kinds of type, we must decide whether to have products of data types or phrase types (or both). Products of data types would be record-like entities, except that one would always assign to entire records rather than their components. (Complex numbers are a good example of a simple product of data types.) On the other hand, products of phrase types are more like members of Simula classes than like records; one can never assign to the entire object, but only to components that are variables; other types of components, such as procedures, are also possible. In this paper, we will only consider products (and sums) of phrase types, thereby retaining the Algol characteristic that data types are never compound.

We must also decide between numbered and named products, i.e. between selecting components by an ordinal or by an identifier (i.e. field name). In this paper we will explore named products, since they are more commonly used than numbered products, and also since they are amenable to a richer subtype relationship.

To introduce named products of phrase types, we expand the set of phrase types to include

prod π,

where π is a type assignment. Usually we will write products in the form prod[ι_{1}: θ_{1} | ⋯ | ι_{n}: θ_{n}], where ι_{1}, …, ι_{n} are distinct identifiers. However, it should be understood that the phrase type denoted by this expression is independent of the ordering of the pairs ι_{k}: θ_{k}.

For a subtype ordering, one at least wants a component-wise ordering. But a more interesting and useful structure arises if we permit implicit conversions that drop components, e.g.

prod[age: integer exp | sex: Boolean exp | salary: integer var]

≤ prod[age: integer exp | salary: integer var]

In general, we have

prod π ≤ prod π′ if and only if

dom(π′) ⊆ dom(π) and (∀ι ∈ dom(π′))π(ι) ≤ π′(ι).

Next we introduce the syntax of phrases for constructing products and selecting their components:

<prod[ι_{1}: θ_{1} | ⋯ | ι_{n}: θ_{n}], π> ::= ⟨ι_{1}: <θ_{1}, π>, …, ι_{n}: <θ_{n}, π>⟩

where ι_{1}, …, ι_{n} are distinct identifiers, and

<θ, π> ::= <prod[ι: θ], π>. ι

In the second production, notice that our subtype ordering permits us to write [ι: θ] instead of [⋯ | ι: θ | ⋯].

The semantics of products is explicated by the following equivalences: When P_{1} ∈ <θ_{1}, π>, …, P_{n} ∈ <θ_{n}, π>, ι_{1}, …, ι_{n} are distinct, and 1 ≤ k ≤ n,

⟨ι_{1}: P_{1}, …, ι_{n}: P_{n}⟩. ι_{k} ≡_{θ_{k},π} P_{k}.

When P ∈ <prod π′, π> and dom(π′) = {ι_{1}, …, ι_{n}},

⟨ι_{1}: (P. ι_{1}), …, ι_{n}: (P. ι_{n})⟩ ≡_{prod π′,π} P

We have mentioned that this kind of product is closely related to the class concept of Simula 67. In [25] it is shown that class declarations (in the reference-free sense of Hoare [27] rather than of Simula itself) can be desugared into constructions using such products.

Finally, we introduce named sums of phrase types. (Roughly speaking, type sums are disjoint unions.) We expand the set of phrase types to include

sum π,

where π is a type assignment. The subtype relation is

sum π ≤ sum π′ if and only if

dom(π) ⊆ dom(π′) and (∀ι ∈ dom(π)) π(ι) ≤ π′(ι).

In contrast to the situation with products, a subtype of a sum can contain fewer (rather than more) alternatives. To construct sums and to do case analysis, we introduce the syntax

<sum[ι : θ], π> ::= tag ι: <θ, π>
<θ, π> ::= sumcase ι is <sum[ι_{1}: θ_{1} | ⋯ | ι_{n}: θ_{n}], π>
in (ι_{1}: <θ, [π | ι: θ_{1}]>, …, ι_{n}: <θ, [π | ι: θ_{n}]>)

where ι_{1}, …, ι_{n} are distinct identifiers.

Again, the semantics can be explicated by equivalences. When ι_{1}, …, ι_{n} are distinct, 1 ≤ k ≤ n, P_{1} ∈ <θ, [π | ι: θ_{1}]>, …, P_{n} ∈ <θ, [π | ι: θ_{n}]>, and A ∈ <θ_{k}, π>,

sumcase ι is tag ι_{k}: A in (ι_{1}: P_{1}, …, ι_{n}: P_{n}) ≡_{θ,π} let ι be A in P_{k}.

When S ∈ <sum π′, π> and dom(π′) = {ι_{1}, …, ι_{n}},

sumcase ι is S in (ι_{1}: tag ι_{1}: ι, …, ι_{n}: tag ι_{n}: ι) ≡_{sum π′,π} S.

Since sumcase is a binding operation, Principle 1 requires us to express it in terms of a construction in which the binding is done by lambda expressions. For this purpose, we introduce the idea of “source-tupling.” Suppose P_{1}, …, P_{n} are procedures of phrase types θ_{1} → θ, …, θ_{n} → θ, respectively. Then sourcetuple(ι_{1}: P_{1}, …, ι_{n}: P_{n}) is a procedure of type sum[ι_{1}: θ_{1} | ⋯ | ι_{n}: θ_{n}] → θ that will behave like P_{k} when applied to a parameter tagged with ι_{k}.

To make this precise we use the syntax

<sum[ι_{1}: θ_{1} | ⋯ | ι_{n}: θ_{n}] → θ, π> ::=
sourcetuple(ι_{1}: <θ_{1} → θ, π>, …, ι_{n}: <θ_{n} → θ, π>)
where ι_{1}, …, ι_{n} are distinct identifiers.

Then sumcase is desugared by the following equivalence: If ι_{1}, …, ι_{n} are distinct, S ∈ <sum[ι_{1}: θ_{1} | ⋯ | ι_{n}: θ_{n}], π>, P_{k} ∈ <θ, [π | ι: θ_{k}]> for 1 ≤ k ≤ n, then

sumcase ι is S in (ι_{1}: P_{1}, …, ι_{n}: P_{n}) ≡_{θ,π}

sourcetuple(ι_{1}: λι: θ_{1}. P_{1}, …, ι_{n}: λι: θ_{n}. P_{n})(S).

It should be noted that sums of phrase types do not introduce any failure of typing such as the “mutant variable record problem” of Pascal, since one cannot change the tag of a sum by assignment. On the other hand, sums of data types would also avoid these problems since a branch on the tag of a value would not imply any assumption that a variable with that value would continue to possess the same tag. This suggests that the type-safety problem with sum-like constructions is due to a failure to distinguish data and phrase types.

11. Final Remarks

I have neglected the topic of program proving since I have discussed it elsewhere at length. Although Hoare’s work on proving procedures is incompatible with call by name and procedure parameters, an alternative approach called specification logic appears promising. In [23] this logic is formulated for a subset of Algol W; in [24] it is given for a language closer to that described here.

Like Algol itself, our illustrative language raises problems of interference, i.e. variable aliasing and interfering side effects of statements and proper procedures. The language is rich enough that an assertion that two phrases do not interfere must be proved (as in specification logic) rather than derived syntactically. Several years ago in [25], I attempted to restrict a language like that described here to permit interference to be detected syntactically. Unfortunately, this work led to some nasty syntactic complications (described at the end of [25]) that have yet to be resolved. Still, I have hopes for the future of this approach.

Although this paper has dealt with nearly all the significant aspects of Algol 60, it has not gone much beyond the scope of that language. More for lack of understanding than space, I have avoided block expressions, user-defined types, polymorphic procedures, recursively defined types, indeterminate and concurrent computation, references, and compound data types.

It remains to be seen whether our model can be extended to cover these topics. Of course, some of them could reasonably be labelled unAlgol-like. But the essence of Algol is not a straitjacket. It is a conceptual universe for language design that one hopes will encompass languages far more general than its progenitor.

References

[1] P. Naur et al., Revised report on the algorithmic language Algol 60, Comm. ACM 6 (1) (January 1963) 1–17.

[2] P. J. Landin, A λ-calculus approach, in: L. Fox (Ed.), Advances in Programming and Non-Numerical Computation (Pergamon Press, Oxford, 1966) pp. 97–141.

[3] P. J. Landin, A correspondence between Algol 60 and Church’s lambda-notation, Comm. ACM 8 (2,3) (February–March 1965) 89–101 and 158–165.

[4] J. McCarthy, Recursive functions of symbolic expressions and their computation by machine, Part I, Comm. ACM 3 (4) (April 1960) 184–195.

[5] P. Lucas, P. Lauer and H. Stigleitner, Method and Notation for the Formal Definition of Programming Languages, TR 25.087, IBM Laboratory Vienna. (June 1968).

[6] D. Scott and C. Strachey, Toward a mathematical semantics for computer languages, Proc. Symposium on Computers and Automata, Polytechnic Inst. of Brooklyn, Vol. 21, pp. 19–46. (Also: Technical Monograph PRG-6, Oxford Univ. Computing Lab., Programming Research Group (1971).)

[7] P. J. Landin, The next 700 programming languages, Comm. ACM 9 (3) (March 1966) 157–166.

[8] A. Evans, Pal—A language designed for teaching programming linguistics, Proc. ACM 23rd Natl. Conf., 1968 (Brandin Systems Press, Princeton, NJ) pp. 395–403.

[9] J. C. Reynolds, Gedanken—A simple typeless language based on the principle of completeness and the reference concept, Comm. ACM 13 (5) (May 1970) 308–319.

[10] A. van Wijngaarden (ed.) et al., Revised report on the algorithmic language Algol 68, Acta Informatica 5 (1975) 1–236.

[11] C. A. R. Hoare, Recursive data structures, Int. J. Comput. Information Sci. 4 (2) (June 1975) 105–132.

[12] N. Wirth, The programming language Pascal, Acta Informatica 1 (1) (1971) 35–63.

[13] R. L. London, J. V. Guttag, J. J. Horning, B. W. Lampson, J. G. Mitchell and G. J. Popek, Proof rules for the programming language Euclid, Acta Informatica 10 (1) (1978) 1–26.

[14] C. M. Geschke, J. H. Morris, and E. H. Satterthwaite, Early experience with Mesa, Comm. ACM 20 (8) (August 1977) 540–553.

[15] J. D. Ichbiah, J. C. Heliard, O. Roubine, J. G. P. Barnes, B. Krieg-Brueckner and B. A. Wichmann, Preliminary Ada reference manual and Rationale for the design of the Ada programming language, SIGPLAN Notices 14 (6) (June 1979).

[16] C. A. R. Hoare, An axiomatic basis for computer programming, Comm. ACM 12 (10) (October 1969) 576–580 and 583.

[17] C. A. R. Hoare and N. Wirth, An axiomatic definition of the programming language Pascal, Acta Informatica 2 (4) (1973) 335–355.

[18] C. A. R. Hoare, Procedures and parameters: An axiomatic approach, in E. Engeler (Ed.), Symposium on Semantics of Algorithmic Languages, Lecture Notes in Mathematics, Vol. 188 (Springer-Verlag, Berlin, 1971) pp. 102–116.

[19] J. C. Reynolds, Using category theory to design implicit conversions and generic operators, in: N. D. Jones (Ed.), Semantics-Directed Compiler Generation, Proceedings of a Workshop, Aarhus, Denmark, January 14–18, 1980, Lecture Notes in Computer Science, Vol. 94 (Springer-Verlag, Berlin, 1980) pp. 211–258.

[20] F. J. Oles, A Category-Theoretic Approach to the Semantics of Programming Languages, Ph.D. Dissertation (completed August 1982), Syracuse University.

[21] R. M. Burstall, J. S. Collins and R. J. Popplestone, Programming in Pop-2 (Edinburgh University Press, 1971).

[22] N. Wirth and C. A. R. Hoare, A contribution to the development of Algol, Comm. ACM 9 (6) (June 1966) 413–432.

[23] J. C. Reynolds, The Craft of Programming (Prentice-Hall, Englewood Cliffs, NJ, 1981).

[24] J. C. Reynolds, Idealized Algol and its Specification Logic, Computer and Information Science, Syracuse University, Report 1–81 (July 1981).

[25] J. C. Reynolds, Syntactic control of interference, Conference Record of the Fifth Annual Symposium on Principles of Programming Languages, Tucson, January 1978 (Association for Computing Machinery, New York, 1978) pp. 39–46.

[26] O.-J. Dahl, B. Myhrhaug and K. Nygaard, Simula 67 Common Base Language, Norwegian Computing Centre, Oslo (1968).

[27] C. A. R. Hoare, Proof of correctness of data representations, Acta Informatica 1 (4) (1972) 271–281.

[28] E. W. Dijkstra, A Discipline of Programming (Prentice-Hall, Englewood Cliffs, NJ, 1976).

[29] C. T. Zahn, A control statement for natural top-down structured programming, Proceedings, Programming Symposium, Paris, April 9–11, 1974, Lecture Notes in Computer Science, Vol. 19 (Springer-Verlag, Berlin, 1974) pp. 170–180.