×

Normal forms and normal theories in conditional rewriting. (English) Zbl 1356.68124

Summary: We present several new concepts and results on conditional term rewriting within the general framework of order-sorted rewrite theories (OSRTs), which support types, subtypes and rewriting modulo axioms, and contains the more restricted framework of conditional term rewriting systems (CTRSs) as a special case. The concepts shed light on several subtle issues about conditional rewriting and conditional termination. We point out that the notions of irreducible term and of normal form, which coincide for unconditional rewriting, have been conflated for conditional rewriting but are in fact totally different notions. Normal form is a stronger concept. We call any rewrite theory where all irreducible terms are normal forms a normal theory. We argue that normality is essential to have good executability and computability properties. Therefore we call all other theories abnormal, freaks of nature to be avoided. The distinction between irreducible terms and normal forms helps in clarifying various notions of strong and weak termination. We show that abnormal theories can be terminating in various, equally abnormal ways; and argue that any computationally meaningful notion of strong or weak conditional termination should be a property of normal theories. In particular we define the notion of a weakly operationally terminating (or weakly normalizing) OSRT, discuss several evaluation mechanisms to compute normal forms in such theories, and investigate general conditions under which the rewriting-based operational semantics and the initial algebra semantics of a confluent, weakly normalizing OSRT coincide thanks to a notion of canonical term algebra. Finally, we investigate appropriate conditions and proof methods to ensure that a rewrite theory is normal; and characterize the stronger property of a rewrite theory being operationally terminating in terms of a natural generalization of the notion of quasi-decreasing order.

MSC:

68Q42 Grammars and rewriting systems

Software:

CafeOBJ; OBJ3; Maude
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Arts, T.; Giesl, J., Termination of term rewriting using dependency pairs, Theor. Comput. Sci., 236, 1-2, 133-178 (2000) · Zbl 0938.68051
[2] Bergstra, J. A.; Klop, J. W., Conditional rewrite rules: confluence and termination, J. Comput. Syst. Sci., 32, 3, 323-362 (1986) · Zbl 0658.68031
[3] Clavel, M.; Durán, F.; Eker, S.; Meseguer, J.; Lincoln, P.; Martí-Oliet, N.; Talcott, C., All About Maude - A High-Performance Logical Framework, Lect. Notes Comput. Sci., vol. 4350 (2007), Springer · Zbl 1115.68046
[4] Durán, F.; Lucas, S.; Marché, C.; Meseguer, J.; Urbain, X., Proving operational termination of membership equational programs, High.-Order Symb. Comput., 21, 1-2, 59-88 (2008) · Zbl 1192.68154
[5] Durán, F.; Lucas, S.; Meseguer, J., Termination modulo combinations of equational theories, (Frontiers of Combining Systems, Proceedings of the 7th International Symposium. Frontiers of Combining Systems, Proceedings of the 7th International Symposium, FroCoS 2009, Trento, Italy, September 16-18, 2009. Frontiers of Combining Systems, Proceedings of the 7th International Symposium. Frontiers of Combining Systems, Proceedings of the 7th International Symposium, FroCoS 2009, Trento, Italy, September 16-18, 2009, Lect. Notes Comput. Sci., vol. 5749 (2009), Springer), 246-262 · Zbl 1193.68145
[6] Futatsugi, K.; Diaconescu, R., CafeOBJ Report, AMAST Series (1998), World Scientific · Zbl 0962.68115
[7] Goguen, J.; Meseguer, J., Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theor. Comput. Sci., 105, 217-273 (1992) · Zbl 0778.68056
[8] Goguen, J.; Winkler, T.; Meseguer, J.; Futatsugi, K.; Jouannaud, J.-P., Introducing OBJ, (Software Engineering with OBJ: Algebraic Specification in Action (2000), Kluwer), 3-167
[9] Hendrix, J.; Meseguer, J., On the completeness of context-sensitive order-sorted specifications, (RTA. RTA, Lect. Notes Comput. Sci., vol. 4533 (2007)), 229-245 · Zbl 1203.68098
[10] Jouannaud, J.-P.; Kirchner, Hélène, Completion of a set of rules modulo a set of equations, SIAM J. Comput., 15, 1155-1194 (November 1986)
[11] Kaplan, S., Conditional rewrite rules, Theor. Comput. Sci., 33, 175-193 (1984) · Zbl 0577.03013
[12] Lucas, S., Context-sensitive computations in functional and functional logic programs, J. Funct. Logic Program., 1, 4, 446-453 (1998)
[13] Lucas, S.; Marché, C.; Meseguer, J., Operational termination of conditional term rewriting systems, Inf. Process. Lett., 95, 4, 446-453 (2005) · Zbl 1185.68374
[14] Lucas, S.; Meseguer, J., Strong and weak operational termination of order-sorted rewrite theories, (Escobar, S., Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS. Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS, Grenoble, France, April 5-6, 2014. Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS. Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS, Grenoble, France, April 5-6, 2014, Lect. Notes Comput. Sci., vol. 8663 (2014), Springer), 178-194 · Zbl 1367.68144
[15] Lucas, S.; Meseguer, J., Localized operational termination in general logics, (Nicola, R. D.; Hennicker, R., Software, Services, and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering. Software, Services, and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, Lect. Notes Comput. Sci., vol. 8950 (2015), Springer), 91-114 · Zbl 1453.68053
[16] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theor. Comput. Sci., 96, 1, 73-155 (1992) · Zbl 0758.68043
[17] Meseguer, J., Membership algebra as a logical framework for equational specification, (Parisi-Presicce, F., Proc. WADT’97. Proc. WADT’97, Lect. Notes Comput. Sci., vol. 1376 (1998), Springer), 18-61 · Zbl 0903.08009
[18] Meseguer, J., Strict coherence of conditional rewriting modulo axioms (August 2014), C.S. Department, University of Illinois at Urbana-Champaign, Technical report
[19] Meseguer, J., Order-sorted rewriting and congruence closure (2015), CS Dept. University of Illinois at Urbana-Champaign, Available at: · Zbl 1475.68142
[20] Ohlebusch, E., Advanced Topics in Term Rewriting (2002), Springer Verlag · Zbl 0999.68095
[21] Rocha, C.; Meseguer, J.; Muñoz, C. A., Rewriting modulo SMT and open system analysis, (Escobar, S., Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS. Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS, Grenoble, France, April 5-6, 2014. Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS. Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS, Grenoble, France, April 5-6, 2014, Lect. Notes Comput. Sci., vol. 8663 (2014), Springer), 247-262 · Zbl 1367.68151
[22] TeReSe, Term Rewriting Systems (2003), Cambridge University Press
[23] van Deursen, A.; Heering, J.; Klint, P., Language Prototyping: An Algebraic Specification Approach (1996), World Scientific · Zbl 0962.68114
[24] Yamada, T.; Avenhaus, J.; Loría-Sáenz, C.; Middeldorp, A., Logicality of conditional rewrite systems, Theor. Comput. Sci., 236, 1-2, 209-232 (2000) · Zbl 0938.68050
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.