×

zbMATH — the first resource for mathematics

Shallow confluence of conditional term rewriting systems. (English) Zbl 1156.68028
Summary: Recursion can be conveniently modeled with left-linear positive/negative-conditional term rewriting systems, provided that non-termination, non-trivial critical overlaps, non-right-stability, non-normality, and extra variables are admitted. For such systems we present novel sufficient criteria for shallow confluence and arrive at the first decidable confluence criterion admitting non-trivial critical overlaps. To this end, we restrict the introduction of extra variables of right-hand sides to binding equations and require the critical pairs to have somehow complementary literals in their conditions. Shallow confluence implies [level] confluence, has applications in functional logic programming, and guarantees the object-level consistency of the underlying data types in the inductive theorem prover QuodLibet.

MSC:
68Q42 Grammars and rewriting systems
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] ()
[2] ()
[3] Autexier, S.; Hutter, D.; Mantel, H.; Schairer, A., \scinka 5.0 — A logical voyager, (), 207-211
[4] Avenhaus, J.; Becker, K., A framework for operational equational specifications with pre-defined structures, J. symbolic comput., 27, 271-310, (1999) · Zbl 0928.68078
[5] Avenhaus, J.; Loría-Sáenz, C.A., On conditional rewrite systems with extra variables and deterministic logic programs, (), 215-229
[6] Avenhaus, J.; Loría-Sáenz, C.A., Higher-order conditional rewriting and narrowing, (), 269-284
[7] Avenhaus, J., Madlener, K., 1990. Term rewriting and equational reasoning. In Banerji (1990, pp. 1-43) · Zbl 0704.68061
[8] Avenhaus, J.; Kühler, U.; Schmidt-Samoa, T.; Wirth, C.-P., How to prove inductive theorems? \scquodlibet!, (), 328-333, (July 23, 2003)
[9] Bachmair, L., Ganzinger, H., 1991. Perfect model semantics for logic programs with equality. In Furukawa (1991, pp. 645-659)
[10] ()
[11] Barendregt, H.P., The lambda calculus, (1984), North-Holland (Elsevier) · Zbl 0549.03012
[12] ()
[13] Becker, K., Semantics for positive/negative-conditional rewrite systems, (), 213-225
[14] Bergstra, J.A.; Klop, J.W., Conditional rewrite rules: confluence and termination, J. computer and system sci., 32, 323-362, (1986) · Zbl 0658.68031
[15] Bertling, H.; Ganzinger, H., Completion-time optimization of rewrite-time goal solving, (), 45-58
[16] Boyer, R.S.; Moore, J.S., A computational logic, (1979), Academic Press (Elsevier) · Zbl 0708.68060
[17] Boyer, R.S.; Moore, J.S., A computational logic handbook, (1988), Academic Press (Elsevier) · Zbl 0678.68091
[18] Bundy, A., 1999. The automation of proof by mathematical induction. Informatics research Report no. 2, Division of Informatics, Univ. Edinburgh. Also in Robinson and Voronkov (2001, vol. 1, pp. 845-911) · Zbl 0994.03007
[19] Courcelle, B., Proc. 9th int. colloquium on trees in algebra and programming, CAAP 1984, Bordeaux, (1984), Cambridge Univ. Press
[20] Deemter, K. van, Peters, S. (Eds.), 1996. Semantic ambiguity and underspecification. CLSI LN No. 55, Stanford
[21] Dershowitz, N., Jouannaud, J.-P., 1990. Rewrite systems. In Leeuwen (1990, vol. B, pp. 243-320) · Zbl 0900.68283
[22] Dershowitz, N.; Okada, M.; Sivakumar, G., Confluence of conditional rewrite systems, (), 31-44 · Zbl 0666.68094
[23] Dershowitz, N.; Okada, M.; Sivakumar, G., Canonical conditional rewrite systems, (), 538-549
[24] Fritz, K. von, The discovery of incommensurability by hippasus of metapontum, Annals of mathematics, 46, 242-264, (1945), German translation Die Entdeckung der Inkommensurabilität durch Hippasos von Metapont in Becker (1965, pp. 271-308) · Zbl 0060.00518
[25] ()
[26] ()
[27] ()
[28] ()
[29] Gentzen, G., 1938. Die gegenwärtige Lage in der mathematischen Grundlagenforschung — Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie. Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften 4, pp. 1-44, Leipzig. Reprinted as facsimile by Wissenschaftliche Buchgesellschaft, Darmstadt, Verlag von S. Hirzel, Stuttgart; English translation in Gentzen (1969)
[30] Gentzen, G., ()
[31] Geser, A., 1994. An Improved General Path Order. MIP-9407, Univ. Passau; Also in J. Applicable Algebra in Engineering, Communication and Computing, AAECC 7 (7) (1996) 469-511
[32] Gillman, L., Writing mathematics well, (1987), The Mathematical Association of America
[33] Gogolla, M., 1983. Algebraic specifications with partially ordered sorts and declarations. Report 169/1983. FB Informatik, Univ Dortmund. Short version is Gogolla (1984)
[34] Gogolla, M., 1984. Partially ordered sorts in algebraic specifications. In Courcelle (1984, pp. 139-154). Long version is Gogolla (1983)
[35] Gramlich, B., 1995. Confluence without termination via parallel critical pairs. SEKI-Report SR-95-13 (SFB), FB Informatik, Univ. Kaiserslautern; Short Version in 21st CAAP 1996. LNCS, vol. 1059. Springer, pp. 211-225
[36] Hanus, M., 1994. On extra variables in (equational) logic programming, MPI-I-94-2-246, Max Planck Inst. für Informatik, Saarbrücken. Short version in Sterling (1995, pp. 665-679)
[37] Hanus, M. (Ed.), 2006. \scCurry — An integrated functional logic language, Web only. http://www.informatik.uni-kiel.de/ curry/report.html, March 30, 2007
[38] Hilbert, D.; Bernays, P., Grundlagen der Mathematik, (Feb. 22, 2008), Springer
[39] Hindley, J.R., An abstract church – rosser theorem. II: applications, J. symbolic logic, 39, 1, 1-21, (1974) · Zbl 0291.02015
[40] Hobbs, J.R., 1996. Monotone decreasing quantifiers in a scope-free logical form. In: Deemter and Peters (1996, pp. 55-76). http://www.isi.edu/ hobbs/monotone-decreasing.pdf, Feb. 21, 2005
[41] Hudlak, P., Peterson, J., Fasel, J.H., 1999. A gentle introduction to Haskell, Web only. http://www.haskell.org/tutorial, March 30, 2007
[42] Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, J. ACM, 27, 4, 797-821, (1980) · Zbl 0458.68007
[43] Huet, G., Lankford, D.S., 1978. On the uniform halting problem for term rewriting systems. Rapport de Recherche 283, INRIA, http://www.ens-lyon.fr/LIP/REWRITING/OLD_PUBLICATIONS_ON_TERMINATION/HUET_LANKFORD, Nov. 25, 2005
[44] ()
[45] Kaplan, S., Positive/negative-conditional rewriting, (), 129-143
[46] Kaufmann, M.; Manolios, P.; Moore, JS., Computer-aided reasoning: an approach, (2000), Kluwer (Springer)
[47] Klop, J.W., 1992. Term rewriting systems. In Abramsky et al. (1992, vol. II, pp. 1-116)
[48] Kühler, U., 2000. A tactic-based inductive theorem prover for data types with partial operations. Ph.D. Thesis, Infix, Akademische Verlagsgesellschaft Aka GmbH, Sankt Augustin, Berlin. http://www.ags.uni-sb.de/ cp/p/kuehlerdiss, July 23 2005
[49] Kühler, U., Wirth, C.-P., 1996. Conditional equational specifications of data types with partial operations for inductive theorem proving. SEKI-Report SR-96-11, FB Informatik, Univ. Kaiserslautern; Short Version in 8th RTA 1997. LNCS, vol. 1232. Springer, pp. 38-52. http://www.ags.uni-sb.de/ cp/p/rta97, Aug. 05, 2001
[50] ()
[51] Löchner, B., Things to know when implementing LPO, Int. J. artificial intelligence tools, 15, 53-79, (2006)
[52] Loría-Sáenz, C.A., 1994. A theoretical framework for reasoning about program construction based on rewrite systems. Ph.D. Thesis, Univ. Kaiserslautern
[53] Mayr, R.; Nipkow, T., Higher-order rewrite systems and their confluence, Theoret. comput. sci., 192, 3-29, (1998) · Zbl 0895.68078
[54] Middeldorp, A.; Hamoen, E., Completeness results for basic narrowing, J. applicable algebra in engineering, communication and computing, AAECC, 5, 213-253, (1994) · Zbl 0810.68088
[55] Nipkow, T., Paulson, L.C., Wenzel, M., 2000. Isabelle’s logics: HOL, Web only. http://isabelle.in.tum.de/PSV2000/doc/logics-HOL.pdf, Sept. 11, 2005
[56] Nipkow, T.; Paulson, L.C.; Wenzel, M., ()
[57] Oostrom, V. van, 1994. Confluence for abstract and higher-order rewriting. Ph.D. Thesis, Vrije Univ. te Amsterdam
[58] Oostrom, V. van, Raamsdonk, F. van, 1994. Weak orthogonality implies confluence: The higher-order case. Technical Report: ISRL-94-5, Nippon Telegraph and Telephone Corporation; Short version in 3rd LFCS 1994. LNCS, vol. 813. Springer, pp. 379-392 · Zbl 0964.68523
[59] Oyamaguchi, M.; Ohta, Y., A new parallel closed condition for church – rosser of left-linear term rewriting systems, (), 187-201 · Zbl 1379.68202
[60] Padawitz, P., Computing in Horn clause theories, (1988), Springer · Zbl 0646.68004
[61] Padawitz, P., Generic induction proofs, (), 175-197
[62] Padawitz, P., Swinging types = functions + relations + transition systems, Theoret. computer sci., 243, 93-165, (2000) · Zbl 0947.68098
[63] Paulson, L.C., \scml for the working programmer, (1996), Cambridge Univ. Press · Zbl 0863.68032
[64] Plaisted, D.A., 1993. Equational reasoning and term rewriting systems. In Gabbay et al. (1993, pp. 273-364)
[65] Raamsdonk, F. van, Higher-order rewriting, (), 220-239 · Zbl 0939.68063
[66] ()
[67] Rosen, B.K., Tree-manipulating systems and church – rosser theorems, J. ACM, 20, 1, 160-187, (1973) · Zbl 0267.68013
[68] Schmidt-Samoa, T., An even closer integration of linear arithmetic into inductive theorem proving, Electronic notes in theoretical computer sci., 151, 3-20, (May 27, 2005)
[69] Schmidt-Samoa, T., Flexible heuristics for simplification with conditional lemmas by marking formulas as forbidden, mandatory, obligatory, and generous, J. applied non-classical logics, 16, 209-239, (March 08, 2006)
[70] Schmidt-Samoa, T., 2006c. Flexible heuristic control for combining automation and user-interaction in inductive theorem proving. Ph.D. Thesis, Univ. Kaiserslautern, http://www.ags.uni-sb.de/ cp/p/samoadiss, July 30, 2006
[71] Slind, K., Function definition in higher-order logic, (), 381-397
[72] Smolka, G., Nutt, W., Goguen, J., Meseguer, J., 1989, Order-sorted equational computation. In: Aït-Kaci and Nivat (1989, vol. 2, pp. 297-367)
[73] Steele, G.L., \sccommon lisp— the language, (1990), Digital Press (Elsevier)
[74] ()
[75] Suzuki, T.; Middeldorp, A.; Ida, T., Level-confluence of conditional rewrite systems with extra variables in right-hand sides, (), 179-193
[76] Takahashi, Y.; Sakai, M.; Toyama, Y., On the confluence property of conditional term rewriting systems, IEICE transactions, J79-D-I, 11, 897-902, (1996), (in Japanese)
[77] Tarski, A., What are logical notions?, (), 143-154 · Zbl 0622.03004
[78] Toyama, Y., 1988. Commutativity of term rewriting systems. In Fuchi and Kott (1988, pp. 393-407). Also in Toyama (1990) · Zbl 0675.68022
[79] Toyama, Y., 1990. Term rewriting systems and the Church-Rosser property, Ph.D. Thesis, Tohoku Univ./ Nippon Telegraph and Telephone Corporation
[80] Waldmann, U., 1989a. Semantics of order-sorted specifications. Report 297/1989, FB Informatik, Univ. Dortmund, Revised version in Theoretical Computer Sci. (1992) 94, 1-35 · Zbl 0746.68064
[81] Waldmann, U., 1989b. Unification in order-sorted signatures. Report 298/1989, FB Informatik, Univ. Dortmund, revised version 1990. http://www.mpi-sb.mpg.de/ uwe/paper/UNIDO-INF-298.dvi.gz, Dec. 12, 2005
[82] Walther, C., Argument-bounded algorithms as a basis for automated termination proofs, (), 601-622
[83] Walther, C., 1994. Mathematical induction. In Gabbay et al. (1994, pp. 127-228)
[84] Wirth, C.-P., 1995. Syntactic confluence criteria for positive/negative-conditional term rewriting systems. SEKI-Report SR-95-09 (SFB). FB Informatik, Univ. Kaiserslautern. http://www.ags.uni-sb.de/ cp/p/sr9509, Aug. 05, 2001
[85] Wirth, C.-P., 1997. Positive/negative-conditional equations: A constructor-based framework for specification and inductive theorem proving, Ph.D. Thesis, Verlag Dr. Kovač, Hamburg, http://www.ags.uni-sb.de/ cp/p/diss, Aug. 05, 2001
[86] Wirth, C.-P., Descente infinie + deduction, Logic J. of the IGPL, 12, 1-96, (Sept. 12, 2003)
[87] Wirth, C.-P., 2005. History and future of implicit and inductionless induction: Beware the old jade and the zombie!. In Hutter and Stephan (2005, pp. 192-203). http://www.ags.uni-sb.de/ cp/p/zombie, Dec. 02, 2002 · Zbl 1098.68699
[88] Wirth, C.-P., 2006. Progress in computer-assisted inductive theorem proving by human-orientedness and descente infinie? SEKI-Working Paper SWP-2006-01, ISSN 1860-5931. http://www.ags.uni-sb.de/ cp/p/swp200601/welcome.html, Aug. 16, 2006
[89] Wirth, C.-P., Hilbert’s epsilon as an operator of indefinite committed choice, J. appl. logic, (Oct. 15, 2007)
[90] Wirth, C.-P.; Gramlich, B., A constructor-basedapproach for positive/negative-conditionalequational specifications, J. symbolic comput., 17, 51-90, (Aug. 05, 2001)
[91] Wirth, C.-P.; Gramlich, B., On notions of inductive validity for first-order equational clauses, (), 162-176, (Aug. 05, 2001)
[92] Wirth, C.-P., Lunde, R., 1994. Writing positive/negative-conditional equations conveniently. SEKI-Working-Paper SWP-94-04 (SFB), FB Informatik, Univ. Kaiserslautern. http://www.ags.uni-sb.de/ cp/p/swp9404, Aug. 05, 2001
[93] Wirth, C.-P., Gramlich, B., Kühler, U., Prote, H., 1993. Constructor-based inductive validity in positive/negative-conditional equational specifications. SEKI-Report SR-93-05 (SFB). FB Informatik, Univ. Kaiserslautern. Revised and extended version of first part is Wirth and Gramlich (1994a), revised version of second part is Wirth and Gramlich (1994b)
[94] Yamada, T.; Avenhaus, J.; Loría-Sáenz, C.A.; Middeldorp, A., Logicality of conditional rewrite systems, Theoret. computer sci., 236, 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. 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.