This volume contains historical and foundational material, and works on language design. All of the material should be accessible to beginning graduate students in programming languages and theoretical Computer Science.
Part I Historical Background
In 1959, John Backus presented a paper [Bac59] on "the proposed international
algebraic language" (which soon after evolved into the language that became
known as Algol 60 [NB#60]). Backus begins by giving informal descriptions
of the syntax and semantics of the language, and outlines reasons why more
precise descriptions are needed. But he then makes the following admission.
The author had hoped to complete a formal description of the set of legal programs and of their meanings in time to present it here. Only the description of legal programs has been completed however. Therefore the formal treatment of the semantics of legal programs will be included in a subsequent paper.Backus goes on to introduce the meta-notation we now know as Backus-Naur formalism and uses it to specify the syntax of the language; however, the "subsequent paper" on the semantics never materialized, and the semantics is again described informally in the Revised Report on Algol 60[NB#63 ].
Many computer scientists today are unfamiliar with this important document, and so most of it has been included as Chapter 1 of this volume; subsequent corrections and discussion of various "ambiguities" may be found in [Knu67 , DHW76 ].
The importance of having precise descriptions of syntax and semantics is today generally appreciated; however, more than 35 years after Backus's talk, researchers are still trying to produce satisfactory descriptions of Algol-like languages. This situation is not unprecedented: mathematicians needed hundreds of years to sort out the semantic issues underlying the differential and integral calculi, and some thirty years passed between Alonzo Church's formulation of the (untyped) lambda calculus [Chu41 ] and the first mathematical models by Dana Scott [Sco72b].
Scott's work on the lambda calculus was partly motivated by a collaboration with Christopher Strachey [SS71] in which they outlined a "mathematical" approach to the semantics of procedural programming languages, using the powerful domain-theoretic tools Scott had developed. This approach, now termed denotational semantics, has become well known; a short introductory paper by Strachey has been included in this volume as Chapter 2.
In [SS71], Scott and Strachey had suggested that if "you put your domains on the table first" then this would help to reveal language-design issues and possibilities. This point of view is illustrated well by Strachey's chapter. The design of Algol 60 is compared to that of a language Pal with quite different domain structure. The comparison takes place exclusively on the level of domains appropriate to each language, independently of surface syntactic similarities or dissimilarities.
One of the most significant contributions to semantic analysis of programming languages by Strachey and his collaborators, such as Scott [Sco72a], Rod Burstall [Bur70], and Peter Landin [Lan65], is the distinction between the environment and the store (or state). The domain analysis of Algol 60 in Section 3.1 of Chapter 2 reveals the disjointness of the "storable" and "denotable" values in this language; this was later described by John Reynolds (see Chapter 3) as the distinction between "data types" and "phrase types."
In Strachey's paper, labels and jumps are not treated in any detail, but the important concept of continuations, which became the "standard" approach to these features, had already been discovered; see [SW74 , Rey93].
An unsatisfactory aspect of traditional denotational semantics for typed languages is that full advantage was not taken of syntactic typing information; for example, in the discussion of Algol 60 in Chapter 2, there is a single domain of all possible procedures, with "run-time" selection of the appropriate sub-domain.
Also, notice that the treatment of assignment is based on the low-level idea of "locations" or L-values,using global states with fixed structure. The approach to dynamic allocation adopted by Scott and Strachey is described in [Sco72a]; it is based on recording in every state which locations are currently "active" (i.e., in use). This has become known as the "marked-stores" approach.
A planned work by Strachey, "An abstract model of storage," referenced
in both of these papers as being "in preparation", never appeared. (Strachey
died in 1975.) More information on traditional denotational semantics may be
found in [MS76 , Sto77].
Part II Basic Principles
A significant change in attitudes to Algol 60was initiated by the paper "The
Essence of Algol" by John Reynolds, reprinted here as Chapter 3. At the
time (1981), this language was generally regarded as having been superseded
by new and improved "Algol-like" languages, such as Algol 68 [vW#69 ]
and Pascal [Wir71]. But Reynolds argues that such languages are not truly
Algol 60-like, and, in many important respects, are less satisfactory than the
original. This is reminiscent of Tony Hoare's opinion [Hoa74 ] that Algol 60is
a language so far ahead of its time that it was not only an improvement on its predecessors but also on nearly all its successors.Furthermore, Reynolds points out that most formal models of programming languages then in use were failing to do justice to typed languages and to important concepts such as representation-independent storage variables and stack-oriented storage management. As a result, languages designed with such models in mind would inevitably be influenced by concepts that are not truly Algol-like.
In more detail, Reynolds characterized "Algol-like" languages as follows.
Syntactic and semantic descriptions tailored to this view of Algol-like languages differ significantly from that given by Strachey in Chapter 2. Syntactic descriptions must deal with an infinity of phrase types, and must take into account subtypes (coercions) which are not necessarily interpreted as subsets and which can introduce ambiguity. Typing contexts must be used to treat non-context-free constraints; a judgement of the form P \in <\theta,\pi> as used by Reynolds would today be written \pi \vdash P: \theta. Instead of using domains of all possible (infinitary) environments and all possible procedures, there is a domain of finitary environments for each assignment of types to finite sets of identifiers, and a domain of procedures for each type of argument and result.
A representation-independent view of storage variables is obtained by treating them as (acceptor, expression)pairs, where an acceptor can be viewed as a function mapping a storable value to a command meaning. This allows for parameterizing semantic domains and semantic interpretation functions by arbitrary sets of states. It is then possible to deal with local-variable declarations by "expanding" the set of states in use. This puts the stack-oriented nature of the language "on the table" at an early stage in the semantic defini tion. The general semantic framework can be presented quite elegantly using the category-theoretical notions of functors and natural transformations; see Part IV.
Chapters 4 to 7 formalize or develop in various ways some of the key ideas in "The Essence of Algol." Reynolds emphasized that the full beta and eta laws of the typed lambda calculus are valid in an Algol-like language, even for imperative phrases such as commands and variables. "Algol and Functional Programming" by Peter O'Hearn shows that an Algol-like language actually preserves all equivalences of the purely functional fragment, provided "snap-back" operations do not exist. An example of a "snap-back" operation would be a block expression in which a command is executed as part of the evaluation of an expression, but, because of possible side-effects to non-local variables, the initial state for that execution is then restored. Although this is certainly implementable, it violates the natural irreversibility of imperative computation.
The paper "On the Orthogonality of Assignments and Procedures in Algol" by Stephen Weeks and Matthias Felleisen formalizes the orthogonality of the functional (lambda calculus-like) and imperative fragments of an Algol- like language in terms of separate reduction calculi for the two fragments. The essential properties of these are proved independently, and it is also proved that evaluation of a program can be factored into a functional phase, followed by an imperative phase.
The usual basis for specification and verification of programs in simple imperative languages is the familiar "axiomatic" system of [Hoa69 ], based on (precondition, command, postcondition) triples. Unfortunately, most attempts to apply these techniques to languages with full procedures and jumps have been fairly unsatisfactory. The paper "Idealized Algol and its Specification Logic" by John Reynolds, reprinted here as Chapter 6, introduced several innovations:
One way to highlight unsatisfactory aspects of a model of local variables is to show that it fails to be fully abstract; i.e., fails to validate operationally justified equivalences. The paper "Towards Fully Abstract Semantics for Local Variables" by Albert Meyer and Kurt Sieber, included here as Chapter 7, demonstrates that traditional marked-store models fail to validate some extremely simple expected equivalences. This work also showed the weaknesses of existing program logics, because most logics for imperative languages with procedures were sound in marked-store models, with specification logic being a notable exception.
"The Essence of Algol" was originally presented as an invited address
to a symposium in tribute to Adriaan van Wijngaarden, one of the designers of both Algol 60 and Algol 68, on the occasion of his retirement. It is
reported that another of the authors of the Algol report commented that
Reynolds's paper should have been titled "An Essence of Algol." For comparison, the reader may want to consult some of the other opinions that have
been expressed by various authors on what is "essential" about Algol 60
[vW63 , WH66 , Knu67, Str67, Wic73, Hoa74, Cla79, Wex81 , THM83 ], and how
it should be formally described [vW64 , Lan64, Mos74, HJ82, THM83 , AW85 ].
"Design of the Programming Language Forsythe" by John Reynolds describes a language based on the ideas presented in "The Essence of Algol." It
contains one further innovation: The use of "intersection" (conjunctive) types
[CD78 ] to further simplify, unify and generalize the type structure of the language.
"Assignments for Applicative Languages" by Uday Reddy, Vipin Swarup
and Evan Ireland, presents an approach to combining imperative and functional aspects by using types to separate imperative and applicative parts of
a program. Types are used to keep the procedure mechanism independent of
side effects, which allows beta, eta, and other properties of functional languages
to be retained. This Algol-like use of types to constrain the scope of effects
is at the root of a body of more recent work on introducing assignment into
"pure" functional languages [PW93 , LP95].
We have mentioned that, despite being imperative, Algol-like languages
preserve all of the reasoning principles used in "pure" functional programming. However, this does not mean that Algol-like languages are necessarily simple to reason about, since this only involves the easy part: reasoning about parts of programs that don't involve change. In particular, it
is evident from the examples of specification logic in use in [Rey81] that
manipulating non-interference predicates within a logic for program verification is extremely inconvenient. The underlying problem is that interactions between assignments and procedures in conventional higher-order procedural languages can produce undesirable phenomena such as aliasing and
covert interference via non-local variables. For this reason, many researchers
[Bac78, WA85 , BW88, Hug89, Hud89] abandoned procedural languages entirely
and promoted "purely" functional languages in which there is no interference
at all. Other language designers have attempted to avoid these problems by
significantly circumscribing the procedures in their languages; see, for example, the discussion of Euclid in [Mor82 ].
The paper "Syntactic Control of Interference" by John Reynolds, reprinted
here as Chapter 10, demonstrates that it is possible to avoid aliasing and
covert interference while retaining Algol-like higher-order procedures in a
slightly restricted form. The resulting programming language has not only
the desirable functional attributes of Algol 60, but also many of the desirable
attributes of simple imperative languages that are typically lost when procedures are added.
Two main strands emerge. The more developed is the explicit-state approach, where programs are modelled using functions that pass states around
as values. This approach identifies uniformity properties (based on naturality
and relational parametricity) that constrain the way that state is used, analogous to how monotonicity and continuity constrain the way that higher-order
functions work in domain theory. Applications include soundness of a program logic and a type system, structuring and design of a translation to intermediate code, and discovery of new reasoning principles.
The other strand is the implicit-state approach, where a program is viewed
in terms of a history of observable actions instead of in terms of state transformations. This approach is more recent; it promises to give a very different
and complementary way of specifying meanings of imperative programs, and
excellent results have been obtained, indicating its potential.
The term "stack discipline" refers to a way of managing the allocation and
de-allocation of storage variables at runtime. Reynolds regarded the stack
discipline as so integral to Algol's essence that (a mathematical abstraction
of) it deserves a prominent position in a satisfactory semantic definition. He
shows this viewpoint at work in "Using Functor Categories to Generate Intermediate Code," included as Chapter 12. Phrases in an Algol-like language
are translated to intermediate code using the compositionally-defined valuation function for interpretation in a functor category. The semantics is tuned
to compiling (instead of input-output behaviour), with store shapes replaced
by a category of concrete "stack descriptors" and primitive types interpreted
using programs in the intermediate language instead of functions on states.
While Algol's stack discipline was the original focus of functor-category
semantics, the ideas have been used also to model dynamic allocation [PS93,
Sta96a] and local names in the pi-calculus [Sta96b, FMS96]. In both of these
cases a name or location can survive past execution of the block in which it
was created: the shape of the store or active name-space is not preserved.
Thus, the stack discipline is not built into functor categories themselves, but
rather has to do with the specific way that Reynolds and Oles used functors in
the semantics of Algol. The point is that a functor-category model can make
it clear, in the semantics of types, whether and where it is possible for store
shapes to be altered.
The paper "Semantical Analysis of Specification Logic" by Bob Tennent,
reprinted here as Chapter 13, addresses this problem by slightly adapting the
functor-category approach of Chapters 3 and 11 to allow the treatment of certain "intensional" properties of commands within a formally extensional intuitionistic first-order theory. It turns out that specification logic is incompatible
with the law of the excluded middle, and so the use of an underlying intuitionistic logic is not only natural, because of the underlying functor model, but in
a sense necessary.
While Chapter 13 solves the previously known problems in the interpretation of specification logic,
it also points out an additional problem with the treatment of non-interference predicates in Chapter 6 and [Rey81]: non-interference for procedural phrases is not correctly defined by induction on
types as a "logical" predicate. The paper "Semantical Analysis of Specification
Logic, 2" by Peter O'Hearn and Bob Tennent, reprinted here as Chapter 14,
addresses this problem. It gives a type-independent interpretation of non-interference which, for phrases of basic types, reduces to the definition given
in Chapter 13. This interpretation validates all of the axioms for reasoning
about non-interference.
These two papers also contain a semantic analysis of passivity, i.e., the
ability to read from, but not write to, the store. In Chapter 13 it is shown that
expression meanings cannot have side effects, not even "temporary" ones as
in the snap-back form of block expression; this is crucial to allow validation
of a Hoare-like axiom for assignments in an Algol-like language. This notion
of passivity is extended to all types in Chapter 14, again by using a uniform,
type-independent, definition.
Specification logic has evolved somewhat with the development of its semantics. Today we regard its essence as
consisting of four parts. First, specification logic is a theory, in the negative fragment (universal quantification, conjunction, implication, falsity)
of many-sorted
first-order intuitionistic logic with equality.
The atomic formulas of the theory are Hoare triples {P}C{Q} and
non-interference formulas C # E (for arbitrary C and E). Second, the treatment of functional features is LCF-like, with
beta/eta-equality, formal function extensionality, and laws for fixed-point unwinding (and induction). Third, for non-interference we have the decomposition
schema and axioms for passivity and chastity, as in Chapter 14, and the axioms of strong constancy and non-interference composition. And finally there
are analogues of Hoare's axioms for imperative constructs such as sequential
composition and iteration, axioms for precedent strengthening, consequent
weakening, and so on. Most distinctive is the axiom for variable declarations,
which extends the usual Hoare-logic rule by using noninterference assumptions between local variables and non-local identifiers.
Peter O'Hearn and Bob Tennent also use logical relations to construct a
model in Chapter 16. They base their construction on the functor-category
model of Oles, adding to it relational conditions that govern interactions with
local variables. Although their semantic technology is similar to Sieber's, the
emphasis is rather different. Where Sieber views relations as a means to "keep
a model small," O'Hearn and Tennent view relations as a rigorous approximation to an informal notion of parametricity, as support for a conceptual
connection with representation independence and data abstraction [Rey83].
The basic idea is that the information-hiding provided by local variables and
procedural abstraction is analogous to the independence of a program using
an abstract data type from the details of the implementation of the type; see
also [Ten94 ].
Chapter 17, by Andy Pitts, differs from other papers in this volume in that
it concentrates on operational rather than denotational methods. Pitts shows
how relational-parametricity principles, as in the semantics of Chapter 16 and
[OR96 ], can be formulated without explicit reference to a semantic model. He
defines logical relations for Idealized Algol based on an operational semantics, and uses these to derive a completeness result characterizing observational equivalence. A main point of his work is that the separation of the
reasoning principles implicit in models based on logical relations from their
use in constructing the models. This results in a clear and mathematically
simple presentation of the resulting principles, and pleasant technical results.
The development of the material in Chapter 18 was done partly in reaction
to a paper by Uday Reddy [Red94 ] which, it turns out, provided the first model
for the type rules for passivity. Only later it was realized that the treatment
of passivity in Chapters 13 and 14 also provides such a model. Reddy sets
out his approach in detail in "Global State Considered Unnecessary," reprinted
here as Chapter 19.
Reddy's paper is remarkable in a number of respects. First, it is an implicit
state semantics, in that imperative programs are treated in terms of sequences
of observable actions, instead of as transformations on a set of states. (This it
has in common with ideas from the process-calculus literature [Mil89].) At
the same time the semantics is domain-theoretic, in much the same spirit
as domain models of functional languages. This allows suitable categorical
structure to be identified, resulting in a novel semantics of syntactic control
of interference.
The second remarkable aspect of Reddy's paper is that it contains the first
semantic account of the irreversibility of state change in imperative programs.
The idea at issue is expressed by Strachey in Chapter 2 of Volume 1 as follows:
While Reddy's model accounts nicely for local state and irreversibility, it
does not treat interference as well. That is, non-interference seems to be built
into the treatment of procedures, so a semantics of syntactic control of interference can be given, but not full Idealized Algol. This was partially resolved
in [OR95 ] by embedding the model into a functor category but, though the
semantics has good theoretical properties, the model construction is rather
technical and ad hoc in comparison to both Reddy's basic model and other
functor-category models.
In "Linearity, Sharing and State," reprinted here as Chapter 20, Samson
Abramsky and Guy McCusker use the framework of game semantics to formulate an implicit-state model for full Idealized Algol (with side effects in
expressions). Their model construction is striking; it extends the semantics of
the functional language PCF developed by Martin Hyland and Luke Ong [HO94 ]
by simply dropping the "innocence" condition (innocence is a game-theoretic
expression of functional behaviour). Programs denote strategies for playing
a game, and as such may be sensitive to a whole history of events (or "prior
moves"): non-innocent access to the history corresponds to imperative, implicitly stateful, behaviour. It is shown that all "compact" strategies in the
model are definable in the language, and after quotienting, this results in a
fully abstract model.
The game model exemplifies Abramsky's general theme of "composition
as parallel composition plus hiding" [Abr93, Abr94]. It is interesting to revisit Reddy's work in light of this. Reddy also emphasized the parallel nature
of composition or application, but focused on what might be thought of as a
"true-concurrency" or "independent-composition" view of parallelism. This is
what, it appears, stopped him from accounting for interference between procedure and argument in a determinate fashion. In contrast, the parallelism in
the game model is more reminiscent of coroutines (and as such harkens back
to [BC82 ]), with a single thread of control jumping back and forth between procedure and argument. This allows interference to be handled quite naturally
in a way that maintains determinacy.
Up to this point the focus has been on sequential versions of Algol. The
question arises as to whether all of this development is dependent on the
sequential nature of the languages studied, or, rather, what parts of it can
extend smoothly to concurrency. Steve Brookes addresses this question in
Chapter 21. He formulates a functor-category model for a parallel version
of Idealized Algol; the use of a functor category shows that the shape of
the store is the same in the initial and final states in the evaluation of any
command. In a parallel language this does not imply that allocation is truly
stack-like if two threads are interleaved on a single processor, but it does establish invariants for the allocator. The semantics of parallel features is then
a straightforward extension of one previously given for a parallel language
without procedures [Bro93], with care taken to account for appropriate naturality conditions. Brookes regards the integration of this semantics with the
treatment of procedures and storage allocation given by functor categories
as evidence for the orthogonality of procedures and parallelism in Algol-like
languages.
P. W. O'Hearn and R. D. Tennent Part III Language Design
Reynolds concludes "The Essence of Algol" with the following remarks.
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.
Chapters 8 to 10 explore three language-design possibilities.
Introduction to Volume 2
In this volume, Algol-like languages are studied from various modern
denotational-semantic points of view. This material will be suitable for advanced seminars and researchers with adequate background in logic, domain
theory, type theory and category theory.
Part IV Functor-Category Semantics
The functor-category approach to the semantics of local variables outlined
in "The essence of Algol" is described in detail in Frank Oles's Ph.D. thesis. Excerpts from this work have been included here as Chapter 11; see also
[Ole85, OT92]. This chapter describes how the extension of the store via local variable declarations can be represented using a category of store shapes and
expansions, and how a treatment of procedures consistent with this view of
local declarations can be obtained using a category of functors from store
shapes into domains.
Part V Specification Logic
In Chapters 6 and 10, Reynolds focused on non-interference as a means of
controlling and reasoning about interactions between procedures and imperative features. But the semantics of non-interference has proved to be rather
subtle. An operational semantics of specification logic is sketched in [Rey81],
but the final section of Chapter 6 points out that this interpretation is not
completely satisfactory. In particular, it fails to validate two powerful, and
seemingly reasonable, axioms that make use of non-interference assumptions.
Part VI Procedures and Local Variables
In Chapter 7 of Volume 1, Meyer and Sieber emphasized that traditional denotational models of imperative languages fail to capture the sense in which non-local procedures are independent of locally-declared variables. An "invariant-preserving" model described in that paper accounts for some of the difficulties, and this line of work is continued by Kurt Sieber in Chapter 15. Sieber
uses the concept of "logical relations" [Plo73, Sta85] as a means to exclude undesirable elements. A full-abstraction result is given showing the coincidence
of semantic equality and a contextually-defined "observational" equivalence
relation, up to second-order types.
Part VII Interference, Irreversibility and Concurrency
In "Syntactic Control of Interference" (Chapter 10 of Volume 1) Reynolds argues that a language should be constrained to make non-interference easily
detectable. The language design given there is very successful in most respects; but it is pointed out that the treatment of passivity is such that syntactic correctness is not always preserved by fi-reductions. This problem has
since been addressed by Reynolds in [Rey89]. A somewhat simpler solution
to the problem is presented in "Syntactic Control of Interference Revisited"
by Peter O'Hearn, John Power, Makoto Takeyama and Bob Tennent, reprinted
here as Chapter 18.
The machine state behaves in a typically "operational" way. The
state transformation produced by obeying a command is essentially irreversible and it is, by the nature of the computers we use, impossible to
have more than one version of [the state] available at any one time.
The problem is that previous models contain "snapback" operators which contradict this idea of irreversibility. (A treatment of irreversibility has recently
been obtained in an explicit-state setup as well [OR96 ], using a linear form of
parametricity to exclude snap-back operators.)
Acknowledgements
We are very grateful to all of the contributors for their cooperation in producing these volumes, to Robin Milner for supporting this project to Birkh"auser,
to Edwin Beschler of Birkh"auser for his confidence in us, to Lockwood Morris
for proofreading, to Elaine Weinman for TEXnical typing, and to John Jorgensen
for assistance in setting up our fonts.
September, 1996.
Bibliography