Search

Several concepts of algebras with solutions of recursive equation systems are compared: CPO-enrichable algebras are proved to be iteration algebras of Z. Esik, 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.

The axioms of iteration 2-theories capture, up to isomorphism, the equational properties of iteration in conjunction with horizontal and vertical composition in all algebraically complete categories. We give a concrete representation of the free iteration 2-theory generated by a 2-signature.

Sabadini, Walters and others have developed a categorical, machine based theory of concurrency in which there are four essential aspects: a distributive category of data-types; a bicategory Mach whose objects are data types, and whose arrows are input-output machines built from data types; a semantic category (or categories) Sem, suitable to contain the behaviors of machines, and a functor, “behavior”: Mach→Sem. Suitable operations on machines and semantics are found so that the behavior functor preserves these operations. Then, if each machine is decomposable into primitive machines using these operations, the behavior of a general machine is deducible from the behavior of its parts. The theory of non-deterministic finite state automata provides an example of the paradigm and also throws some light on the classical theory of finite state automata. We describe a bicategory whose objects are natural numbers, in which an arrow M: n→p is a finite state automaton with n input states, p output states, and some additional internal states; we require that no transitions begin at output states or end at input states. A machine is represented by an q+n by q+p matrix. The bicategory supports additional operations: non-deterministic choice, parallel interleaving, and feedback. Enough operations are imposed on machines to show that each machine may be obtained from some atomic ones by means of the operations. The semantic category is the (Bloom-Esik) iteration theory Mat (X✶ whose objects are natural numbers and whose arrows from n to p are n×p matrices with entries in the semiring of languages. The behavior functor associates to a machine M: n→p a matrix |M| of languages, one language to each pair of input and output states. Behavior preserves composition, feedback, takes non-deterministic choice to union, and parallel-interleaving to shuffle. Thus, behavior gives a compositional semantics to a primitive notion of concurrent processes.

This paper extends Part 1 of the paper with the same title. Here, matricial iteration theories Matr(S; V) are characterized by identities involving theory operations, a star operation S → S and an omega operation S → V. The initial matricial iteration theory is described explicitly. One answer is given to the following question: If T0 is a submatricial theory of the matricial theory T which is an iteration theory, when can the star and omega operations on T0 be extended to T so that T becomes an iteration theory? Applications to program correctness logic and to finding equational axioms for the regular sets are indicated.

In “Monadic Computation and Iterative Algebraic Theories” Elgot [3] introduced the notion of a vector iterative theory and showed that vector iterative theories have a close connection with several aspects of the theory of computation. In private conversations Elgot formulated the notion of a scalar iterative theory and raised the question whether scalar and vector iterative theories coincide. We answer this question in the affirmative.

In ''Monadic Computation and Iterative Algebraic Theories'' by Calvin C. Elgot,the notion ''iterative theory'' (more fully, ''ideal theory closed under conditional iteration'') is introduced and applied to the study of computational processes. The main point of the present paper is to show the existence (in a constructive sense) of free iterative theories. The main complication is the fact that in an iterative theory I the ''iteration'' operation is not defined for all elements of I. Were it not for this complication, the existence of free iterative theories would follow from general algebraic considerations (extended to many-sorted algebras). Actually we sketch two proofs of the existence of free iterative theories. One argument follows as much as possible general algebraic lines and is given a linguistic flavor in order to emphasize the concreteness of the ideas involved. The second argument depends upon ''normal descriptions'': a morphism in the free iterative theory being an equivalence class of normal descriptions.