Varieties of Iteration Theories
Stephen L. Bloom, Zoltán Ésik · SIAM Journal on Computing · 1988
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.