An algebraic tree T is one determined by a finite system of fixed point equations. The frontier Fr(T ) of an algebraic tree T is linearly ordered by the lexicographic order <ℓ If (Fr(T) <ℓ) is well-ordered, its order type is an algebraic ordinal. We prove that the algebraic ordinals are exactly the ordinals less than ω $^{ω}$ $^{ω}$ .

Several concepts of algebras with solutions of recursive equation systems are compared: CPO-enrichable algebras are proved to be iteration algebras of Z. Ésik, and iteration algebras are a special case of the recently introduced Elgot algebras (which are the monadic algebras for the free iterative monad). Another special case of iteration algebras are the iterative algebras of E. Nelson and J. Tiuryn, which are algebras with unique solutions of all guarded systems. For each of the above classes of algebras an example is provided showing that the inclusion in a wider class is proper.

We show that, aside from the semiring equations, three equations and two equation schemes characterize the semiring of regular sets with the Kleene star operation.

What is special about the rules of Hoare logic?This paper shows that partial correctness logic can be viewed as a special case of the equational logic of iteration theories [6,7,24].It is shown how to formulate a partial correctness assertion {a} f { /3} as an equation between iteration theory terms.The guards (a, ~) that appear in partial correctness assertions are equationally axiomatized, and a new representation theorem for Boolean algebras is derived.The familiar rules for the structured programming constructs of composition, if-then-else and while-do are shown valid in all guarded iteration theories.A new system of partial correctness logic is described that applies to all flowchart programs.The invariant guard condition, weaker than the well-known condition of expressiveness.is found to be both necessary and sufficient for the completeness of these rules.The Cook completeness theorem [19] follows as an easy corollary.The role played by weakest liberal preconditions in connection with completeness is examined.

The equational properties of iteration, when combined with composition and pairing, are captured by the notion of “iteration theory,” which was introduced in [SIAM J. Comput., 9 (1980), pp. 26–45; 9 (1980), pp. 525–540]. We believe, although all of our evidence will not be exhibited here, that every iterative construction satisfies at least the properties of iteration theories. In this paper, axiomatizations are given for several varieties of iteration theories which occur naturally in the semantics of programming languages, i.e., those generated by theories of trees [J. Comput. Sys. Sci., 16 (1978), pp. 362–399], theories of sequacious functions [Proc. 1973 Colloquium, Vol. 80, Studies in Logic, North Holland, Amsterdam, 1975; pp. 175–230], theories of partial functions, and theories of both sequacious and partial functions with distinguished predicates. We show which additional equations must be added to the axioms for iteration theories [Comput. Ling. Comput. Lang., 14 (1980), pp. 183–207] in order to obtain a set of axioms for these subvarieties. Concrete descriptions of the free theories in each variety are given.

Four classes of algebras are considered. The algebras in each class contain functions whose behavior models a version of the “if-then-else” instruction. In one version, for example, the algebras contain a function $\kappa $ of four arguments such that $\kappa (x,y,u,v) = u$ if $x = y$ and $\kappa (x,y,u,v) = v$ if $x \ne y$. None of the considered classes is an equational class, but equational axioms are found for each class such that an equation is valid in the class if it is derivable in standard equational logic from the axioms.

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). As in linear algebra, we obtain a necessary and sufficient condition for our equations to have unique solutions and we can describe “parametrically” the totality of solutions. However, whereas in linear algebra, there is no way of giving $1 \div 0$ meaning in such a way that all the “old laws” hold, we can give meaning to the “iteration operation” (the analogue of division into 1) in such a way that all the “old laws” still hold. Indeed, we can describe “parametrically” all such ways of extending the (partially defined) scalar iteration operation to all trees (more generally, morphisms).

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 $ \bot :1 \to 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^\dag = \bot $ and all scalar iterative identities remain valid. In this paper the scalar iteration operation in the pointed iterative theory $(J, \bot )$ is extended to vector morphisms while preserving all the old identities. The main result shows that the vector iterate $g^\dag $ in $(J, \bot )$ satisfies the equation $g^\dag = (g_ \bot )^\dag $, where $g_ \bot $ is a nonsingular morphism simply related to g (so that $(g_ \bot )^\dag $ is the unique solution of the iteration equation for $g_ \bot $). In the case that $J = \Gamma {\text{Tr}}$, the iterative theory of $\Gamma $-trees, it is shown that the vector iterate $g^\dag $ in $(J, \bot )$ is a metric limit of “modified powers” of g.

In many studies of computation which make use of rooted labeled trees a partial ordering is usually imposed on the trees in the following way. A particular label, say $ \bot _0 $, is distinguished and identified with the atomic tree whose only vertex is a leaf labeled $ \bot _0 $. A tree f is then defined to be less than a tree A tree g if g can be obtained from f by attaching some new trees to leaves of f labeled $ \bot _0 $. This paper answers the following questions. What is the significance of the tree $ \bot _0 $ in this ordering? Can other nonatomic and perhaps infinite trees $ \bot $ be used to define a partial ordering on the trees in the same way? If so, what if anything distinguishes the partial ordering defined via the atomic tree $ \bot _0 $?