Search

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.

Recall the definition of matricial theories from Section 3.5.3. Since each matricial theory can be represented as a theory Matr(S; V) for some semiring module pair (S;V), we will be considering only matricial theories of this sort. A matricial iteration theory is a matricial theory which is simultaneously an iteration theory. We show that when T = Matr(S; V) is a matricial iteration theory, the dagger operation determines and is determined by a star operation on the semiring S and an omega operation ω: S → V from the semiring to the module.

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 ...