Group axioms for iteration. (English) Zbl 0924.68143

Summary: Iteration theories provide a sound and complete axiomatization of the equational properties of the iteration (or fixed point) operation in many models of theoretical computer science including ordered and metric structures, trees and synchronization trees. All known equational axiomatizations of iteration theories consist of a small set of equational axioms for Conway theories and a complicated equation scheme, the commutative identity. Here, we associate an identity with each finite semigroup. We prove that the set consisting of the Conway identities and the group identities associated with the finite (simple) groups is complete. Moreover, we prove that the Conway identities and a subcollection of the semigroup identities associated with a subclass of the finite semigroups is complete iff each finite (simple) group divides one of the semigroups in the subclass. We also formulate a conjecture and study its consequences. The results are a generalization of Krob’s axiomatization of the equational theory of the regular sets. \(\copyright\) Academic Press.


68Q45 Formal languages and automata


Full Text: DOI


[1] Bernátsky, L.; Ésik, Z., Semantics of flowchart programs and the free Conway theories, RAIRO theoret. inform. appl., 32, 35-78, (1998)
[2] Bloom, S.L.; Elgot, C.C.; Wright, J.B., Solutions of the iteration equation and extension of the scalar iteration operation, SIAM J. comput., 9, 26-45, (1980) · Zbl 0454.18011
[3] Bloom, S.L.; Elgot, C.C.; Wright, J.B., Vector iteration in pointed iterative theories, SIAM J. comput., 9, 525-540, (1980) · Zbl 0461.68047
[4] Bloom, S.L.; Ésik, Z., Iteration theories: the equational logic of iterative processes, EATCS monographs on theoretical computer science, (1993), Springer-Verlag Berlin · Zbl 0796.68153
[5] Bloom, S.L.; Ésik, Z., Some quasi-varieties of iteration theories, Proceedings, mathematical foundations of programming semantics ’93, Lncs 802, (1994), Springer-Verlag Berlin, p. 378-409
[6] Bloom, S.L.; Ésik, Z., Solving polynomial fixed point equations, Proceedings, mathematical foundations of computer science ’94, Lncs 841, (1994), Springer-Verlag Berlin, p. 52-67
[7] Conway, J.C., Regular algebra and finite machines, (1971), Chapman and Hall London · Zbl 0231.94041
[8] Eilenberg, S., Automata, languages, and machines, (1976), Academic Press New York
[9] Eilenberg, S. The category \(C\)
[10] Elgot, C.C., Monadic computation and iterative algebraic theories, Proceedings, logic colloquium ’73, Studies in logic, 80, (1975), North Holland Amsterdam, p. 175-230 · Zbl 0327.02040
[11] Elgot, C.C.; Bloom, S.L.; Tindell, R., On the algebraic structure of rooted trees, J. comput. system sci., 16, 362-399, (1978) · Zbl 0389.68007
[12] Ésik, Z., Identities in iterative and rational algebraic theories, Computational linguistics and computer languages, 14, 183-207, (1980) · Zbl 0466.68010
[13] Ésik, Z., Independence of the equational axioms of iteration theories, J. comput. system sci., 36, 66-76, (1988) · Zbl 0649.68010
[14] Ésik, Z., Completeness of park induction, Theoret. comput. sci., 177, 217-283, (1997) · Zbl 0901.68107
[15] Ésik, Z. A proof of the Krohn-Rhodes decomposition theorem · Zbl 0944.68089
[16] Ésik, Z. Axiomatizing iteration categories, Acta Cybernet.
[17] Ésik, Z. The power of the group axioms for iteration, Int. J. Algebra Comput. · Zbl 0924.68143
[18] Ésik, Z.; Labella, A., Equational properties of iteration in algebraically complete categories, Theoret. comput. sci., 195, 61-89, (1988) · Zbl 0903.18003
[19] Ésik, Z.; Virágh, J., On products of automata with identity, Acta cybernet., 7, 299-311, (1986) · Zbl 0621.68039
[20] Ginzburg, A., Algebraic theory of automata, (1968), Academic Press New York · Zbl 0195.02501
[21] Goguen, J.A.; Thatcher, J.W.; Wagner, E.G.; Wright, J.B., Initial algebra semantics and continuous algebras, J. assoc. comput. Mach., 24, 68-95, (1977) · Zbl 0359.68018
[22] Golan, J.S., The theory of semirings with applications in computer science, (1992), Longman Harlow · Zbl 0780.16036
[23] Guessarian, I., Algebraic semantics, Lncs 99, (1981), Springer-Verlag Berlin
[24] Hurkens, A. J. C. McArthur, M. Moschovakis, Y. N. Moss, L. Whitney, G. The logic of recursive equations, J. Symbolic Logic · Zbl 0911.03022
[25] Kozen, D., A completeness theorem for Kleene algebras and the algebra of regular events, Inform. and comput., 110, 366-390, (1994) · Zbl 0806.68082
[26] Krob, D., Complete systems of B-rational identities, Theoret. comput. sci., 89, 207-343, (1991) · Zbl 0737.68053
[27] Lawvere, F.L., Functorial semantics of algebraic theories, Proc. nat. acad. sci., 50, 869-873, (1963) · Zbl 0119.25901
[28] Lallement, G., Semigroups and combinatorial applications, (1979), Wiley-Interscience New York · Zbl 0421.20025
[29] Manes, E.G., Predicate transformer semantics, (1992), Cambridge Univ. Press Cambridge · Zbl 0784.68003
[30] Milner, R., A calculus for communicating systems, Lncs 92, (1980), Springer-Verlag Berlin · Zbl 0452.68027
[31] Milner, R., A complete inference system for a class of regular behaviours, J. comput. system sci., 28, 439-466, (1984) · Zbl 0562.68065
[32] Moschovakis, Y.N., Abstract recursion as a foundation for the theory of algorithms, Proceedings, logic colloquium Aachen ’83, Lnm 1104, (1983), Springer-Verlag Berlin, p. 289-364
[33] Nelson, E., Iterative algebras, Theoret. comput. sci., 25, 67-94, (1983) · Zbl 0533.03014
[34] Park, D.M.R., Fixpoint induction and proofs of program properties, Machine intelligence 5, (1970), Edinburgh Univ. Press Edingburgh, p. 59-78 · Zbl 0219.68007
[35] Plotkin, G.D., Domains, Lecture notes, (1983), Department of Computer Science University of Edinburgh
[36] Sewell, P., Bisimulation is not finitely (first order) equationally axiomatisable, Proceedings, logic in computer science 9, (1994), p. 62-70
[37] Tiuryn, J., Fixed points and algebras with infinitely long expressions, part I: regular algebras, Fund. inform., 2, 103-128, (1978) · Zbl 0401.68062
[38] Tiuryn, J., Unique fixed points vs. least fixed points, Theoret. comput. sci., 12, 229-254, (1980) · Zbl 0439.68026
[39] Winskel, G., The formal semantics of programming languages, Foundations of computing series, (1993), MIT Press Cambridge
[40] Wright, J.B.; Thatcher, J.W.; Goguen, J.; Wagner, E.G., Rational algebraic theories and fixed-point solutions, Proceedings, 17th IEEE symp. foundations of computing, Houston, Texas, (1976) · Zbl 0361.68041
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.