Specification and proof in membership equational logic.

*(English)*Zbl 0938.68057Summary: This paper is part of a long-term effort to increase expressiveness of algebraic specification languages while at the same time having a simple semantic foundation on which efficient execution by rewriting and powerful theorem-proving tools can be based. In particular, our rewriting techniques provide semantic foundations for Maude’s functional sublanguage, where they have been efficiently implemented. This effort started in the late 1970s, led by the ADJ group, who promoted equational logic and universal algebra as the semantic basis of program specification languages. An important later milestone was the work around order-sorted algebras and the OBJ family of languages developed at SRI-International in the 1980s. This effort has been substantially advanced in the mid-1990s with the development of Maude, a language based on membership equational logic. Membership equational logic is quite simple, and yet quite powerful. Its atomic formulae are equations and sort membership assertions, and its sentences are Horn clauses. It extends in a conservative way both (a version of) order-sorted equational logic and partial algebra approaches, while Horn logic with equality can be very easily encoded. After introducing the basic concepts of the logic, we give conditions and proof rules with which efficient equational deduction by rewriting can be achieved. We also give completion techniques to transform a specification into one meeting these conditions. We address the important issue of proving that a specification protects a subspecification, a property generalizing the usual notion of sufficient completeness. Using tree-automata techniques, we develop a test-set-based approach for proving inductive theorems about a parameterized specification. We briefly discuss a number of extensions of our techniques, including rewriting modulo axioms such as associativity and commutativity, having extra variables in conditions, and solving goals by narrowing. Finally, we discuss the generality of our approach and how it extends several previous approaches.

##### MSC:

68Q65 | Abstract data types; algebraic specification |

PDF
BibTeX
XML
Cite

\textit{A. Bouhoula} et al., Theor. Comput. Sci. 236, No. 1--2, 35--132 (2000; Zbl 0938.68057)

Full Text:
DOI

**OpenURL**

##### References:

[1] | Aubin, R., Mechanizing structural induction, Theoret. comput. sci., 9, 329-362, (1979) · Zbl 0423.68051 |

[2] | L. Bachmair, Proof by consistency in equational theories, Proc. 3rd IEEE Symp. on Logic in Computer Science, Edinburgh, UK, 1988, pp. 228-233. |

[3] | Barr, M.; Wells, C., Toposes, triples and theories, (1985), Springer Berlin · Zbl 0567.18001 |

[4] | K. Becker, Inductive proofs in specifications parameterized by a built-in theory, SEKI-Report SR-92-02, Universität Kaiserslautern, 1992. |

[5] | J.A. Bergstra, J.V. Tucker, Characterization of computable data types by means of a finite equational specification method, in: J.W. de Bakker, J. van Leeuwen (Eds.), Proc. 7th Internat. Conf. on Automata, Languages and Programming, Lecturer Notes in Computer Science, vol. 81, Springer, Berlin, 1980, pp. 76-90. · Zbl 0449.68003 |

[6] | B. Bogaert, S. Tison, Equality and disequality constraints on brother terms in tree automata, in: A. Finkel (Ed.), Proc. 9th Symp. on Theoretical Aspects of Computer Science, Paris, Lecturer Notes in Computer Science, vol. 577, Springer, Berlin, 1992, pp. 161-172. |

[7] | A. Boudet, Unification in order-sorted algebras with overloading, in: D. Kapur (Ed.), Proc. 11th Internat. Conf. on Automated Deduction, Saratoga Springs, NY, LNAI 607, Springer, Berlin, June 1992, pp. 193-207. · Zbl 0925.03079 |

[8] | Bouhoula, A., Using induction and rewriting to verify and complete parameterized specifications, Theoret. comput. sci., 170, 1 & 2, 245-276, (1996) · Zbl 0874.68198 |

[9] | Bouhoula, A., Automated theorem proving by test set induction, J. symbolic comput., 23, 1, 47-77, (1997) · Zbl 0878.68108 |

[10] | A. Bouhoula, J.-P. Jouannaud, Automata-driven automated induction, in: Proc. 12th IEEE Symp. Logic in Computer Science, Varsaw, IEEE Comp. Soc. Press, Silverspring, MD, 1997, 14-25. · Zbl 1008.03009 |

[11] | Bouhoula, A.; Jouannaud, J.-P.; Meseguer, J., Specification and proof in membership equational logic, (), 67-92 · Zbl 0938.68057 |

[12] | Bouhoula, A.; Rusinowitch, M., Implicit induction in conditional theories, J. automat. reason., 14, 2, 189-235, (1995) · Zbl 0819.68114 |

[13] | Boyer, R.S.; Moore, J.S., A computational logic handbook, (1988), Academic Press Inc. New York · Zbl 0678.68091 |

[14] | Burmeister, P., Partial algebras – survey of a unifying approach towards a two-valued model theory for partial algebras, Algebra universalis, 15, 306-358, (1982) · Zbl 0511.03014 |

[15] | A.-C. Caron, H. Comon, J.-L. Coquidé, M. Dauchet, F. Jacquemard, Pumping, cleaning and symbolic constraints solving, in: Proc. Internat. Conf. on Algorithms, Languages and Programming, Jerusalem, Lecturer Notes in Computer Science, vol. 820, Springer, Berlin, 1994, 436-449. · Zbl 1418.68114 |

[16] | A-C. Caron, J.-L. Coquidé, M. Dauchet, Encompassment properties and automata with constraints, in: C. Kirchner (Ed.), Proc. 5th Rewriting Techniques and Applications, Montréal, Lecturer Notes in Computer Science, vol. 690, Springer, Berlin, 1993, pp. 328-342. |

[17] | Cerioli, M.; Meseguer, J., May I borrow your logic? (transporting logical structure along maps), Theoret. comput. sci., 173, 311-347, (1997) · Zbl 0901.68186 |

[18] | J. Christian, Some termination criteria for narrowing and \(e\)-narrowing, in: D. Kapur (Ed.), Proc. 11th Internat. Conf. on Automated Deduction, Saratoga Springs, NY, Lecture Notes in Artificial Intelligence, vol. 607, Springer, Berlin, 1992, pp. 582-588. |

[19] | H. Comon, Sufficient completeness, term rewriting systems and “anti-unification”, Proc. 8th Internat. Conf. on Automated Deduction, Oxford, England, July 1986. · Zbl 0643.68031 |

[20] | H. Comon, An effective method for handling initial algebras, in: Proc. 1st Workshop on Algebraic and Logic Programming, Gaussig, Lecturer Notes in Computer Science, vol. 343, Springer, Berlin, November 1988. · Zbl 0708.68025 |

[21] | H. Comon, Inductive proofs by specifications transformation, in: Proc. 3rd Rewriting Techniques and Applications, Chapel Hill, Lecturer Notes in Computer Science, vol. 355, Springer, Berlin, April 1989, 76-91. |

[22] | H. Comon, Completion of rewrite systems with membership constraints, in: W. Kuich (Ed.), Proc. 19th Internat. Coll. on Automata, Languages and Programming, Vienna, Lecturer Notes in Computer Science, vol. 623, Springer, Berlin, 1992. · Zbl 0983.68091 |

[23] | Comon, H.; Delor, C., Equational formulae with membership constraints, Inform. and comput., 112, 2, 167-216, (1994) · Zbl 0827.03020 |

[24] | H. Comon, F. Jacquemard, Ground reducibility and automata with disequality constraints, in: P. Enjalbert (Ed.), Proc. 11th Symp. on Theoretical Aspects of Computer Science, Caen, Lecturer Notes in Computer Science, vol. 775, Springer, Berlin, 1994, pp. 151-162. · Zbl 0941.68599 |

[25] | Coste, M., Localisation, spectra and sheaf representation, (), 212-238 |

[26] | N. Dershowitz, Well-founded orderings, Information Science Research Office, ATR-83-8478-3, The Aerospace Corporation, El Segundo CA, USA, 1983. |

[27] | Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, (), 243-309 · Zbl 0900.68283 |

[28] | Dershowitz, N.; Okada, M., A rationale for conditional equational programming, Theoret. comput. sci., 75, 111-138, (1990) · Zbl 0702.68034 |

[29] | N. Dershowitz, G. Sivakumar, Solving goals in equational languages, in: S. Kaplan, J.-P. Jouannaud (Eds.), Proc. 1st Internat. Workshop on Conditional Term Rewriting Systems, Orsay, 1987. Lecturer Notes in Computer Science, vol. 308, Springer, Berlin, 1988, 45-55. · Zbl 0666.68093 |

[30] | H. Comon, F. Jacquemard, Ground reducibility is exptime-complete, in: Proc. 12th IEEE Symp. Logic in Computer Science, Varsaw, IEEE Comp. Soc. Press, 1997, Silverspring, MD, pp. 26-34. · Zbl 1090.68047 |

[31] | Fribourg, L., A strong restriction of the inductive completion procedure, J. symbolic comput., 8, 3, 253-276, (1989) · Zbl 0682.68029 |

[32] | K. Futatsugi, J. Goguen, J.-P. Jouannaud, J. Meseguer, Principles of OBJ2, Proc. 12th ACM Symp. on Principles of Programming Languages, New Orleans, 1985, pp. 52-66. |

[33] | P. Gabriel, F. Ulmer, Lokal präsentierbare Kategorien, Lecturer Notes in Mathematics, vol. 221, Springer, Berlin, 1971. |

[34] | Gallier, J.H.; Book, R.V., Reductions in tree replacement systems, Theoret. comput. sci., 37, 123-150, (1985) · Zbl 0602.68072 |

[35] | Ganzinger, H., A completion procedure for conditional equations, J. symbolic comput., 11, 51-81, (1991) · Zbl 0724.68053 |

[36] | Ganzinger, H., Order-sorted completion: the many-sorted way, Theoret. comput. sci., 89, 1, 3-32, (1991) · Zbl 0736.68050 |

[37] | Gnaedig, I.; Kirchner, C.; Kirchner, H., Equational completion in order-sorted algebras, Theoret. comput. sci., 72, 169-202, (1990) · Zbl 0698.68028 |

[38] | M. Gogolla, Algebraic specifications with partially ordered sets and declarations, Technical Report, Universität Dortmund, Dortmund, West Germany, 1983. |

[39] | J. Goguen, Order sorted algebra, Semantics and Theory of Computation Report 14, UCLA, 1978. |

[40] | J. Goguen, J.-P. Jouannaud, J. Meseguer. Operational semantics for order-sorted algebra, in: W. Brauer (Ed.), Proc. 12th Internat. Coll. on Automata, Languages and Programming, Nafplion, Lecturer Notes in Computer Science, vol. 194, Springer, Berlin, 1985, pp. 221-231. · Zbl 0591.68041 |

[41] | J. Goguen, C. Kirchner, H. Kirchner, Aristide Megrelis, J. Meseguer, T. Winkler, An introduction to OBJ 3, Technical Report 88-R-001, CRIN, Nancy, France, 1988. |

[42] | J. Goguen, J. Meseguer, Models and equality for logical programming, in: H. Ehrig, G. Levi, R. Kowalski, U. Montanari (Eds.), Proc. TAPSOFT, Lecturer Notes in Computer Science, vol. 250, Springer, Berlin, 1987, pp. 1-22. · Zbl 0626.68032 |

[43] | Goguen, J.; Meseguer, J., Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theoret. comput. sci., 105, 217-273, (1992) · Zbl 0778.68056 |

[44] | J.A. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, J.-P. Jouannaud, Introducing OBJ, in: J.A. Goguen (Ed.), Applications of Algebraic Specifications Using OBJ, Cambridge University Press, Cambridge, to appear. |

[45] | Guttag, J.V., Abstract data types and software validation, Comm. ACM, 21, 1048-1064, (1978) · Zbl 0387.68012 |

[46] | Guttag, J.V.; Horning, J.J., The algebraic specification of abstract data types, Acta inform., 10, 27-52, (1978) · Zbl 0369.68010 |

[47] | C. Hintermeier, C. Kirchner, H. Kirchner, Dynamically-typed computations for order-sorted equational presentations, in: Proc. 20th Internat. Coll. on Automata, Languages and Programming, Jerusalem Lectures Notes in Computer Science, vol. 880, Springer, Berlin, 1994, pp. 450-461. J. Symbolic Comput. 1998, to appear. · Zbl 0983.68254 |

[48] | G. Huet, J.-M. Hullot, Proofs by induction in equational theories with constructors, J. Comput. System Sci. 25(2) (1982) 239-266. Preliminary version in: Proc. 21st Symp. on Foundations of Computer Science, IEEE, New York, 1980. · Zbl 0532.68041 |

[49] | J.-M. Hullot, Canonical forms and unification, in Proc. 5th Conf. on Automated Deduction, Les Arcs, France, Lectures Notes in Computer Science, vol. 87, Springer, Berlin, July 1980, pp. 318-334. |

[50] | F. Jacquemard, Automates d’arbres et Applications à la Réécriture, Thèse de doctorat, Université Paris-Sud, Orsay, France, 1996. |

[51] | Jouannaud, J.-P.; Kirchner, H., Completion of a set of rules modulo a set of equations, SIAM J. comput., 15, 4, 1155-1194, (1986) · Zbl 0665.03005 |

[52] | Jouannaud, J.-P.; Kirchner, C., Solving equations in abstract algebrasa rule-based survey of unification, (), 257-321 |

[53] | Jouannaud, J.-P.; Kirchner, C.; Kirchner, H.; Megrelis, A., OBJ: programming with equalities, subsorts, overloading and parametrization, J. logic programm., 12, 257-279, (1992) · Zbl 0754.68021 |

[54] | Jouannaud, J.-P.; Kounalis, E., Automatic proofs by induction in theories without constructors, Inform. comput., 82, 1, 1-33, (1989) · Zbl 0682.68032 |

[55] | Jouannaud, J.-P.; Okada, M., Abstract data type systems, Theoret. comput. sci., 173, 2, 349-391, (1997) · Zbl 0901.68121 |

[56] | J.-P. Jouannaud, A. Rubio, A recursive path ordering for higher-order terms in \(η\)-long \(β\)-normal form, in: H. Ganzinger, (Ed.), Proc. 7th Rewriting Techniques and Applications, NJ, Lectures Notes in Computer Science, vol. 1103, Springer, Berlin, 1996. Theoret. Comput. Sci., to appear. |

[57] | J.-P. Jouannaud, B. Waldmann, Reductive conditional term rewriting systems, Proc. 3rd IFIP Working Conf. on Formal Description of Programming Concepts, Ebberup, Denmark, 1986, pp. 223-244. |

[58] | Kaplan, S., Conditional rewrite rules, Theoret. comput. sci., 33, 175-193, (1984) · Zbl 0577.03013 |

[59] | C. Kirchner, H. Kirchner, Order-sorted computations in G-algebras, unpublished draft, January 1993. |

[60] | C. Kirchner, H. Kirchner, J. Meseguer, Operational semantics of OBJ-3, in: Proc. 15th Internat. Coll. on Automata, Languages and Programming, Tampere, Lectures Notes in Computer Science, vol. 317, Springer, Berlin, 1988, pp. 287-301. · Zbl 0649.68028 |

[61] | H. Kirchner, A general inductive completion algorithm and application to abstract data types, in: R. Shostak (Ed.), Proc. 7th Internat. Conf. on Automated Deduction, Napa Valley (Calif., USA), Lecture Notes in Computer Science, vol. 170, Springer, Berlin, 1984, pp. 282-302. · Zbl 0547.03025 |

[62] | E. Kounalis, Completeness in data type specifications, in: B. Buchberger (Ed.), Proc. EUROCAL Conf., Linz, Austria, Lecture Notes in Computer Science, vol. 204, Springer, Berlin, 1985, pp. 348-362. · Zbl 0572.68015 |

[63] | S. Krisher, A. Bockmayr, Detecting redundant narrowing derivations by the LSE-SL reducibility test, in Proc. 4th Rewriting Techniques and Applications, Como, Italy, Lectures Notes in Computer Science, vol. 488, Springer, Berlin, 1991, pp. 75-85. |

[64] | Lugiez, D.; Moysset, J.-L., Tree automata help one to solve equational formulae in ac-theories, J. symbolic comput., 18, 4, 297-318, (1994) · Zbl 0827.68041 |

[65] | P. Lincoln, M. Clavel, S. Eker, J. Meseguer, Principles of Maude, in: J. Meseguer (Ed.), Proc. 1st Internat. Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science, vol. 4, 1996. · Zbl 0912.68095 |

[66] | M. Clavel, F. Duran, S. Eker, J. Meseguer, Building equational proving tools by reflection in rewriting logic, SRI-International, 1997. |

[67] | Manca, V.; Salibra, A.; Scollo, G., Equational type logic, Theoret. comput. sci., 77, 131-159, (1990) · Zbl 0716.03022 |

[68] | C. Marché, Normalised rewriting and normalised completion, in Proc. 9th Annual IEEE Symp. on Logic in Computer Science, Paris, IEEE Comp. Soc. Press, Silverspring, MD, July 1994, pp. 394-403. |

[69] | Martı́-Oliet, N.; Meseguer, J., Inclusions and subtypes I: first order case, J. logic comput., 6, 409-438, (1996) · Zbl 0931.03048 |

[70] | N. Martı́-Oliet, J. Meseguer, Inclusions and subtypes II: higher-order case, J. Logic Comput., to appear. · Zbl 0931.03049 |

[71] | Meseguer, J., General logics, (), 275-329 |

[72] | Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theoret. comput. sci., 96, 1, 73-155, (1992) · Zbl 0758.68043 |

[73] | Meseguer, J., A logical theory of concurrent objects and its realization in the maude language, (), 314-390 |

[74] | J. Meseguer, Membership algebra, 1996, Lecture at the Dagstuhl Seminar on Specification and Semantics, July 96. Extended manuscript version distributed at the 1st Internat. Workshop on Rewriting Logic. |

[75] | J. Meseguer, Membership algebra as a semantic framework for equational specification. Invited talk at WADT’97, Tarquinia, Italy, June 1997; in: Lectures Notes in Computer Science, vol. 1376, Springer, Berlin, 1997, pp. 18-61, 1998. |

[76] | J. Meseguer, J. Goguen, Initiality, induction and computability, in: M. Nivat, J. Reynolds (Eds.), Algebraic Methods in Semantics, Ch. 14, Cambridge Univ. Press, Cambridge, 1985. |

[77] | Meseguer, J.; Goguen, J., Order-sorted algebra solves the constructor-selector, multiple representation and coercion problems, Inform. and comput., 103, 1, 114-158, (1993) · Zbl 0796.68144 |

[78] | J. Meseguer, T. Winkler, Parallel programming in Maude, in: J.B. Banâtre, D. Le Métayer (Eds.), Research Directions in High-Level Parallel Programming Languages, Springer, Berlin, June 1991. pp. 253-293. |

[79] | B. Monate, Automates de formes normales et réductibilité inductive, Rapport de DEA, 1997. |

[80] | T. Mossakowski, Equivalences among various logical frameworks of partial algebras, in: H. Kleine Büning (Ed.) Computer Science Logic, Paderborn, Germany, September 1995, Selected Papers, Lectures Notes in Computer Science, vol. 1092, Springer, Berlin, 1996, pp. 403-433. |

[81] | P.D. Mosses, Unified algebras and institutions, Proc. 4th Annual IEEE Symp. on Logic in Computer Science, Asilomar, CA June 1989, pp. 304-312. · Zbl 0716.68066 |

[82] | D.R. Musser, On proving inductive properties of abstract data types, in Proc. 7th ACM Symp. on Principles of Programming Languages, ACM, New York, 1980, pp. 154-162. |

[83] | Poigné, A., Parametrization for order-sorted algebraic specification, J. comput. system sci., 40, 2, 229-268, (1990) · Zbl 0694.68020 |

[84] | G. Smolka, Order-sorted horn logic: semantics and deduction, Research Report SR-86-17, Univ. Kaiserslautern, October 1986. |

[85] | G. Smolka, W. Nutt, J.A. Goguen, J. Meseguer, Order-sorted equational computation, in: H. Aı̈t-Kaci, M. Nivat (Eds.), Resolution of Equations in Algebraic Structures, vol. 2, Rewriting Techniques, Ch. 10, Academic Press, New York, 1989, pp. 297-367. |

[86] | G.F. Stuart, W.W. Wadge, Classified model abstract data type specification, Manuscript, University of Victoria, 1991. |

[87] | W.W. Wadge, Classified algebras, Technical Report, University of Warwick, 1982. |

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.