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.

MSC:

 68Q45 Formal languages and automata

iteration
Full Text:

References:

 [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. Iteration Theories: The Equational Logic of Iterative Processes, EATCS Monographs on Theoretical Computer Science (1993), Springer-Verlag: 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. Proceedings, Mathematical Foundations of Programming Semantics ’93, LNCS 802 (1994), Springer-Verlag: Springer-Verlag Berlin, p. 378-409 · Zbl 1509.68047 [6] Bloom, S. L.; Ésik, Z., Solving polynomial fixed point equations, Proceedings, Mathematical Foundations of Computer Science ’94. Proceedings, Mathematical Foundations of Computer Science ’94, LNCS 841 (1994), Springer-Verlag: Springer-Verlag Berlin, p. 52-67 · Zbl 1496.08005 [7] Conway, J. C., Regular Algebra and Finite Machines (1971), Chapman and Hall: Chapman and Hall London · Zbl 0231.94041 [8] Eilenberg, S., Automata, Languages, and Machines (1976), Academic Press: Academic Press New York · Zbl 0359.94067 [9] Eilenberg, S. The category $$C$$; Eilenberg, S. The category $$C$$ [10] Elgot, C. C., Monadic computation and iterative algebraic theories, Proceedings, Logic Colloquium ’73. Proceedings, Logic Colloquium ’73, Studies in Logic, 80 (1975), North Holland: 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; Ésik, Z. A proof of the Krohn-Rhodes decomposition theorem · Zbl 0944.68089 [16] Ésik, Z. Axiomatizing iteration categories, Acta Cybernet.; Ésik, Z. Axiomatizing iteration categories, Acta Cybernet. [17] Ésik, Z. The power of the group axioms for iteration, Int. J. Algebra Comput.; É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: 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: Longman Harlow · Zbl 0780.16036 [23] Guessarian, I., Algebraic Semantics. Algebraic Semantics, LNCS 99 (1981), Springer-Verlag: Springer-Verlag Berlin · Zbl 0474.68010 [24] Hurkens, A. J. C. McArthur, M. Moschovakis, Y. N. Moss, L. Whitney, G. The logic of recursive equations, J. Symbolic Logic; 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: Wiley-Interscience New York · Zbl 0421.20025 [29] Manes, E. G., Predicate Transformer Semantics (1992), Cambridge Univ. Press: Cambridge Univ. Press Cambridge · Zbl 0784.68003 [30] Milner, R., A Calculus for Communicating Systems. A Calculus for Communicating Systems, LNCS 92 (1980), Springer-Verlag: 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. Proceedings, Logic Colloquium Aachen ’83, LNM 1104 (1983), Springer-Verlag: Springer-Verlag Berlin, p. 289-364 · Zbl 0599.03052 [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: Edinburgh Univ. Press Edingburgh, p. 59-78 · Zbl 0219.68007 [35] Plotkin, G. D., Domains. Domains, lecture notes (1983), Department of Computer Science: 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. The Formal Semantics of Programming Languages, Foundations of Computing Series (1993), MIT Press: MIT Press Cambridge · Zbl 0919.68082 [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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.