Selected Papers

A new class of machine models as a framework for the rational discussion of programming languages is introduced. In particular, a basis is provided for endowing programming languages with semantics. The notion of Random-Access Stored-Program Machine (RASP) is intended to capture some of the most salient features of the central processing unit of a modern digital computer. An instruction of such a machine is understood as a mapping from states (of the machine) into states. Some classification of instructions is introduced. It is pointed out in several theorems that programs of finitely determined instructions are properly more powerful if address modification is permitted than when it is forbidden, thereby shedding some light on the role of address modification in digital computers. The relation between problem-oriented languages (POL) and machine languages (ML) is briefly considered.

A programming language L presumably should be designed, at least in part, to express algorithms of a given class M. Given an algorithm in the class M, there should be a name in L which expresses it. In addition, L should possess names for the “tasks performable by algorithms” in M. A theory of the language L should presumably include statements about algorithms in M and their tasks.

The objective of this paper is to point out that the “semantics” of cycle-free program schemes (of the kind intuitively described in Section 2) may be explicated by existing algebraic notions. More explicitly, equivalence classes of schemes correspond to morphisms in a free algebraic theory (cf., Lawvere (1963), and Eilenberg and Wright (1967)), and an interpretation of the collection of morphisms is a coproduct-preserving functor into an appropriate target category.

A notion, of “exit-automaton” is introduced to play a role analogous to “machine scheme” or “program scheme”. Exit-automata and machines are equipped with algebraic structure leading to a simple characterization of their behaviors.

The notion algebraic theory was introduced by Lawvere in 1963 (cf. S. Eilenberg and J. B. Wright, Automata in general algebras, Information and Control 11 (1967) 4) to study equationally definable classes of algebras from a more intrinsic point of view. We make use of it to study Turing machines and machines with a similar kind of control at a level of abstraction which disregards the nature of ‘storage’ or ‘external memory’.

Many kinds of phenomena are studied with the aid of (rooted) digraphs such as those indicated by Figs. 1.1 and 1.2.

The two digraphs, while different, usually represent the same phenomenon, say, the same “computational process.” Our interest in rooted trees stems from the fact that these two digraphs “unfold” into the SAME infinite tree. In some cases at least it is also true that different (i.e. non-isomorphic) trees represent different phenomena (of the same kind). In these cases the unfolding (i.e. the trees) are surrogates for the phenomena.

We study the solutions to a (vector) equation somewhat analogous to the traditional equations of linear algebra. Whereas, in introductory linear algebra the domain of discourse is the field of real numbers (or an arbitrary field) our domain of discourse is the algebraic theory of (multi-rooted, leaf-labeled) trees (or, more generally, any iterative theory).

This paper is a sequel to a previous paper S. L. Bloom, C. C. Elgot and J. B. Wright, Solutions of the iteration equation and extensions of the scalar iteration operations, SIAM J. Comput., 9 (1980), pp. 25–45. In that paper it was proved that for each morphism ⊥: 1 → 0 in an iterative theory J there is exactly one extension of the scalar iteration operation in J to all scalar morphisms such that \( I_1^{ + } = \bot \) and all scalar iterative identities remain valid. In this paper the scalar iteration operation in the pointed iterative theory (J, ⊥) is extended to vector morphisms while preserving all the old identities.

The main result shows that the vector iterate g in (J, ⊥) satisfies the equation g = (g _⊥), where g _⊥ is a nonsingular morphism simply related to g (so that (g _⊥) is the unique solution of the iteration equation for g _⊥).

In the case that J = ΓTr, the iterative theory of Γ-trees, it is shown that the vector iterate g ⁺ in (J, ⊥) is a metric limit of “modified powers” of g.

While “Dijkstra flow-chart schemes” (built out of assignment statement schemes by means of composition, if-then and whiledo) are simple and perspicuous, they lack the descriptive power of flow-chart schemes (provided additional “variables” are not permitted). On the other hand, the analogous multiexit composition binary alternation-conditional iteration (CACI) schemes introduced below, which are virtually as simple and perspicuous as Dijkstra schemes, describe exactly the same computational processes as flow-chart schemes (without the aid of additional variables).

Theorem 9.1 makes contact with “reducible flow-graphs” an active area in its own right.

The flowchart schemes called “reducible” are of interest because The reducible flowchart schemes admit both graph-theoretic and algebraic descriptions. A flowchart scheme F with n begins and p exits is reducible iff both (a) for every vertex v there is a begin-path (i.e. a path from a begin vertex) which ends in v (b) for every closed path C there is a vertex v_C of C such that every begin path to a vertex of C meets v_C. Algebraically: F is reducible iff it can be built up from atomic flowchart schemes (which may be thought of as corresponding to single instructions) and surjective trivial flowchart schemes (which may be thought of as redirecting flow of control) by means of composition (∘), separated pairing (+), and scalar iteration (†). Dropping † yields the accessible, acyclic flowchart schemes.

The equational axioms referred to in the title relate ≈-identified (i.e. isomorphism-identified) flowchart schemes by these three operations. The structure freely generated by the set Γ of atomic flowchart schemes is Γ Red, the theory (or multi-sorted algebra) of reducible flowchart schemes. The axioms involving only + and ∘ yield ΓAc, the theory of accessible, acyclic flowchart schemes. Semantical domains which may be used to interpret Γ Red also satisfy these axioms. The set of equational statements true for Γ Red (which are also logical consequences of the axioms) determine a congruence on the algebra of expressions built out of Γ, Sur, +, ∘ and † whose quotient is another description of Γ Red.

Thus the expressions built up using these three operations provide an alternative notation for reducible flowchart programs; the purpose of the axioms is to determine when two expressions represent the same schematic program.

The mutual exclusion problem introduced (as far as we know) by Dijkstra in 1965 is intriguing because on the one hand it appears to be typical of a broad class of important systems problems and on the other poses difficult problems of mathematization. There has been extensive attention to this (and other synchronization problems) since that date. Nevertheless our approach to the problem differs from all the others in at least two important ways. First: we take the problem to be “construct from n uncoordinated sequential processes, n coordinated ones which satisfy (1) mutual exclusion, (2) fairness and (3) simulation.” Second: our mathematical model can directly represent simultaneous actions. Since we do not constrain the synchronization in some of the usual ways, however, the realm of possible solutions is much broader than considered elsewhere. The main solution we offer is simple in that each process need read only one binary variable (or register), viz. its own, and write in one, viz. its neighbor’s. The emphasis of our approach is in the mathematical formulation of the problem, and the proof that the solution satisfies the desired properties, rather than in the novelty of the solution itself. The other solutions offered serve to emphasize the enormous differences in implementation associated with what we call the “conceptual solution,” and the fact that instructions (or atomic actions) don’t compose i.e. a sequence of two (single entry — single exit) instructions of a process is not system equivalent to any single instruction. Contrary to many other solutions to the mutual exclusion problem, the solutions given here do not employ a test and set primitive i.e. an indivisible test and set instruction.