×

Equivalences and transformations of regular systems - applications to recursive program schemes and grammars. (English) Zbl 0636.68104

The paper presents a unified theory of recursive systems defined by means of recursive definitions. Recursive program schemes and context-free grammars are considered as main examples of such systems. The equivalences of regular systems associated with solutions of recursive equations are systematically investigated and characterized in terms of system transformations by folding, unfolding and rewriting according to the equational algebraic laws. Correctness of introduced transformation rules is also proved.
Reviewer: A.V.Anisimov

MSC:

68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)

Citations:

Zbl 0636.68105

Software:

ALGOL 60
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Arnold, A.; Nivat, M., Metric interpretations of infinite trees and semantics of nondeterministic recursive programs, Theoret. comput. sci., 11, 181-205, (1980) · Zbl 0427.68022
[2] Arnold, A.; Nivat, M., The metric space of infinite trees. algebraic and topological properties, Fund. inform., III, 4, 445-476, (1980) · Zbl 0453.68021
[3] Backus, J., Can programming be liberated from the von Neumann style? A functional style and its algebra of programs, Comm. ACM, 21, 613-641, (1978) · Zbl 0383.68013
[4] de Bakker, J., Least fixed points revisited, Theoret. comput. sci., 2, 155-181, (1976) · Zbl 0348.68013
[5] de Bakker, J.; Scott, D., A theory of programs, (1969), unpublished
[6] Benson, D.; Guessarian, I., Algebraic solutions to recursion schemes, () · Zbl 0637.68018
[7] Berry, G.; Lévy, J-J., Minimal and optimal computations of recursive programs, J. ACM, 26, 148-175, (1979) · Zbl 0388.68012
[8] Berstel, J., Transductions and context-free languages, (1979), Teubner Stuttgart · Zbl 0424.68040
[9] Birkhoff, G., On the structure of abstract algebras, (), 433-454 · Zbl 0013.00105
[10] Bloom, S., All solutions of a system of recursion equations in infinite trees and other contraction theories, J. comput. system sci., 27, 225-255, (1983) · Zbl 0535.68006
[11] Bloom, S.; Elgot, C.; Wright, J., Solutions of the iteration equation and extensions of the scalar iteration operation, SIAM J. comput., 9, 25-45, (1980) · Zbl 0454.18011
[12] Bloom, S.; Tindell, R., Compatible orderings on the metric theory of trees, SIAM J. comput., 9, 683-691, (1980) · Zbl 0447.05026
[13] Bloom, S.; Tindell, R., Varieties of ‘if-then-else’, SIAM J. comput., 12, 677-707, (1983) · Zbl 0518.68010
[14] Bodnarchuk, V.; Bodnarchuk, V., The metrical space of events, Kibernetika, Kibernetika, 1, 4, 22-30, (1965), (in English)
[15] Book, R.V., The undecidability of a word problem: on a conjecture of strong, maggiolo-schettini and Rosen, Inform. process. lett., 12, 121-122, (1981) · Zbl 0457.03036
[16] Brainerd, W., The minimalization of tree automata, Inform. and control, 13, 484-491, (1968) · Zbl 0181.01602
[17] Brainerd, W., Tree generating regular systems, Inform. and control, 14, 217-231, (1969) · Zbl 0169.31601
[18] Braquelaire, J.P.; Courcelle, B., The solutions of two star-height problems for regular trees, Theoret. comput. sci., 30, 205-239, (1984) · Zbl 0554.68037
[19] Burstall, R.; Darlington, J., A transformation system for developing recursive programs, J. ACM, 24, 44-67, (1977) · Zbl 0343.68014
[20] Chirica, L.; Martin, D., An order-algebraic definition of Knuthian semantics, Math. systems theory, 13, 1-27, (1979) · Zbl 0397.68087
[21] Chottin, L., Etude syntaxique de certains langages solutions d’équations avec opérateurs, Theoret. comput. sci., 5, 51-84, (1977) · Zbl 0364.68069
[22] Courcelle, B.; Courcelle, B., A representation of trees by languages, Theoret. comput. sci., Theoret. comput. sci., 7, 25-55, (1978) · Zbl 0428.68088
[23] Courcelle, B., Attribute grammars: definitions, analysis of dependencies, proof methods, ()
[24] Courcelle, B., Arbres infinis et systèmes d’équations, RAIRO inform. théor., 13, 31-48, (1979) · Zbl 0406.68017
[25] Courcelle, B., Infinite trees in normal form and recursive equations having a unique solution, Math. systems theory, 13, 131-180, (1979) · Zbl 0418.68013
[26] Courcelle, B., Fundamental properties of infinite trees, Theoret. comput. sci., 25, 95-169, (1983) · Zbl 0521.68013
[27] Courcelle, B.; Deransart, P., Proofs of partial correctness for attribute grammars and recursive procedures, INRIA rept. 322, (1984), submitted for publication · Zbl 0719.68038
[28] Courcelle, B.; Franchi-Zannettacci, P.; Courcelle, B.; Franchi-Zannettacci, P., Attribute grammars and recursive program schemes, parts I-II, Theoret. comput. sci., Theoret. comput. sci., 17, 235-257, (1982) · Zbl 0481.68068
[29] Courcelle, B.; Guessarian, I., On some classes of interpretations, J. comput. system sci., 17, 388-413, (1978) · Zbl 0392.68009
[30] Courcelle, B.; Kahn, G.; Vuillemin, J., Algorithmes d’équivalence et de réduction à des expressions minimales, dans une classe d’équations récursives simples, (), 200-213 · Zbl 0285.68022
[31] Courcelle, B.; Nivat, M., Algebraic families of interpretations, (), 137-146
[32] Courcelle, B.; Nivat, M., The algebraic semantics of recursive program schemes, (), 16-30 · Zbl 0384.68016
[33] Courcelle, B.; Raoult, J.C., Completions of ordered magmas, Fund. inform., III, 1, 105-116, (1980) · Zbl 0463.06005
[34] Courcelle, B.; Vuillemin, J., Completeness results for the equivalence of recursive schemes, J. comput. system sci., 12, 179-197, (1976) · Zbl 0342.68008
[35] Cousineau, G., An algebraic definition for control structures, Theoret. comput. sci., 12, 175-192, (1980) · Zbl 0456.68015
[36] Damm, W., The IO- and OI-hierarchies, Theoret. comput. sci., 20, 95-207, (1982) · Zbl 0478.68012
[37] Damm, W., Languages defined by higher program schemes, (), 164-179
[38] Damm, W.; Fehr, E., On the power of self-application and higher-type recursion, (), 177-191 · Zbl 0391.68041
[39] Damm, W.; Fehr, E.; Indermark, K., Higher type recursion and self-application as control structures, (), 461-487 · Zbl 0373.68021
[40] Deransart, P., Speeding up circularity tests for attribute grammars, Acta inform., 20, 375-391, (1984) · Zbl 0515.68055
[41] Eilenberg, S.; Wright, J., Automata in general algebras, Inform. and control, 11, 52-70, (1967) · Zbl 0175.27902
[42] Elgot, C., Monadic computation and iterative algebraic theories, (), 175-230 · Zbl 0327.02040
[43] Elgot, C.; Mezei, F., On relations defined by generalized finite automata, IBM J. res. develop., 9, 47-68, (1965) · Zbl 0135.00704
[44] Engelfriet, J., Bottom-up and top-down tree transformations, a comparison, Math. systems theory, 9, 198-231, (1975) · Zbl 0335.68061
[45] Engelfriet, J.; Schmidt, E.; Engelfriet, J.; Schmidt, E., IO and OI, J. comput. system sci., J. comput. system sci., 16, 1, 67-99, (1978) · Zbl 0371.68020
[46] Gallier, J.H., Nondeterministic flowchart programs with recursive procedures, semantics and correctness II, Theoret. comput. sci., 13, 3, 239-270, (1981) · Zbl 0461.68015
[47] Gallier, J.H., Recursion closed algebraic theories, J. comput. system sci., 23, 69-105, (1981) · Zbl 0472.68006
[48] Gallier, J.H., N-rational algebras, I: basic properties and free algebras; II: varieties and the logic of inequalities, SIAM J. comput., 13, 750-794, (1984) · Zbl 0554.68018
[49] Gautam, N., The validity of equations of complex algebras, Arch. math. logik, grundlag., 3, 117-124, (1957) · Zbl 0081.26005
[50] Gecseg, F.; Steinby, M., Tree-automata, (1984), Akademiai Kiado Budapest · Zbl 0396.68041
[51] Ginsburg, S.; Rice, H., Two families of languages related to ALGOL, J. ACM, 9, 350-371, (1962) · Zbl 0196.01803
[52] Goguen, J., How to prove algebraic inductive hypotheses without induction, (), 356-373
[53] Goguen, J.; Thatcher, J.; Wagner, E., An initial algebra approach to the specification, correctness and implementation of abstract data types, (), 80-149
[54] Goguen, J.; Thatcher, J.; Wagner, E.; Wright, J., Initial algebra semantic and continuous algebras, J. ACM, 24, 68-95, (1977) · Zbl 0359.68018
[55] Guessarian, I., Program transformations and algebraic semantics, Theoret. comput. sci., 9, 39-65, (1979) · Zbl 0399.68023
[56] Guessarian, I., Algebraic semantics, () · Zbl 0602.68017
[57] Harrison, M.A., Introduction to formal language theory, (1978), Addison-Wesley Reading, MA · Zbl 0411.68058
[58] Hitchcock, P.; Park, D., Induction rules and proofs of termination, (), 225-251
[59] Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, J. ACM, 27, 797-821, (1980) · Zbl 0458.68007
[60] Huet, G.; Hullot, J.M., Proofs by induction in equational theories with constructors, (), 96-107
[61] Huet, G.; Oppen, D., Equations and rewrite rules, (), 349-405
[62] Istratescu, V., Fixed point theory, (1981), Reidel Dordrecht
[63] Kott, L., About transformation systems, a theoretical study, (), 232-247 · Zbl 0406.68011
[64] Kott, L., Unfold/fold program transformations, () · Zbl 0577.68034
[65] Lassez, J.-L.; Nguyen, V.; Sonenberg, E., Fixed points theorems and semantics: A folk tale, Inform. process. lett., 14, 112-116, (1982) · Zbl 0488.68015
[66] Lescanne, P., Equivalence entre la famille des ensembles réguliers et la famille des ensembles algébriques, RAIRO inform. théor., 10, 57-81, (1976)
[67] Lescanne, P., Modèles non déterministes de types abstraits, RAIRO inform. théor., 16, 225-244, (1982) · Zbl 0491.68013
[68] Manna, Z.; Vuillemin, J., Fixpoint approach to the theory of computation, Comm. ACM, 15, 528-536, (1972) · Zbl 0245.68011
[69] Markowsky, G.; Rosen, B., Bases for chain-complete posets, IBM J. res. develop., 20, 138-147, (1976) · Zbl 0329.06001
[70] McCarthy, J., A basis for a mathematical theory of computation, (), 33-70
[71] McNauthton, R., Parenthesis grammars, J. ACM, 14, 490-500, (1967) · Zbl 0168.01206
[72] Métivier, Y., About the rewriting systems produced by the Knuth-bendix completion algorithm, Inform. process lett., 16, 31-34, (1983) · Zbl 0506.68032
[73] Mezei, J.; Wright, J., Algebraic automata and context-free sets, Inform. and control, 11, 3-29, (1967) · Zbl 0155.34301
[74] Mycielski, J.; Taylor, W., A compactification of the algebra of terms, Algebra universalis, 6, 159-163, (1976) · Zbl 0358.08001
[75] Nelson, E., Iterative algebras, Theoret. comput. sci., 25, 67-94, (1983) · Zbl 0533.03014
[76] Nivat, M., On the interpretation of recursive polyadic program schemes, (), 255-281
[77] Paul, E., Proof by induction in equational theories with relations between constructors, (), 211-225 · Zbl 0559.03019
[78] Schützenberg, M., On context-free languages and push-down automata, Inform. and control, 6, 246-264, (1963) · Zbl 0123.12502
[79] Shafaat, A., On varieties closed under the construction of power algebras, Bull. austral. math. soc., 11, 213-218, (1974) · Zbl 0295.08002
[80] Tennent, R., The denotational semantics of programming languages, Comm. ACM, 19, 437-453, (1976) · Zbl 0337.68010
[81] Vuillemin, J., Correct and optimal implementations of recursion in a simple programming language, J. comput. system. sci., 9, 332-354, (1974)
[82] Vuillemin, J., Syntaxe, Sémantique et axiomatique d’un langage de programmation simple, (1975), Birkhäuser Verlag Basel/Stuttgart · Zbl 0327.68006
[83] Wright, J.; Thatcher, J.; Wagner, E.; Goguen, J., Rational algebraic theories and fixed point solutions, (), 147-158
[84] Wright, J.; Wagner, E.; Thatcher, J., A uniform approach to inductive posets and inductive closure, Theoret. comput. sci., 7, 57-77, (1978) · Zbl 0732.06001
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.