Completeness results for basic narrowing. (English) Zbl 0810.68088
Summary: We analyze completeness results for basic narrowing. We show that basic narrowing is not complete with respect to normalizable solutions for equational theories defined by confluent term rewriting systems, contrary to what has been conjectured. By imposing syntactic restrictions on the rewrite rules we recover completeness. We refute a result of Hölldobler which states the completeness of basic conditional narrowing for complete (i.e. confluent and terminating) conditional term rewriting systems without extra variables in the conditions of the rewrite rules. In the last part of the paper we extend the completeness results of Giovannetti and Moiso for level-confluent and terminating conditional systems with extra variables in the conditions to systems that may also have extra variables in the right-hand sides of the rules.
References:
| [1] | Bergstra, J. A., Klop, J. W.: Conditional Rewrite Rules: Confluence and Termination. J. Comput. Syst. Sci.32(3), 323-362 (1986) · Zbl 0658.68031 · doi:10.1016/0022-0000(86)90033-4 |
| [2] | Bockmayr, A.: Beiträge zur Theorie des Logisch-Funktionalen Programmierens. Ph.D. thesis, Universität Karlsruhe, 1990 (In German) |
| [3] | Bosco, P. G., Giovannetti, E., Moiso, C.: Narrowing vs. SLD-Resolution. Theoret. Comput. Sci.59, 3-23 (1988) · Zbl 0648.68043 · doi:10.1016/0304-3975(88)90095-3 |
| [4] | Chabin, J., Réty, P.: Narrowing Directed by a Graph of Terms. Proceedings of the 4th International Conference on Rewriting Techniques and Applications, Como. Lecture Notes in Computer Science, vol. 488, pp. 112-123, Berlin, Heidelberg, New York: Springer 1991 |
| [5] | Dershowitz, N., Jouannaud, J.-P.: Rewrite Systems. In: Handbook of Theoretical Computer Science, Vol. B, pp. 243-320. van Leeuwen, J. (ed), Amsterdam: North-Holland 1990 · Zbl 0900.68283 |
| [6] | Dershowitz, N., Manna, Z.: Proving Termination with Multiset Orderings. Commun. ACM22(8), 465-476 (1979) · Zbl 0431.68016 · doi:10.1145/359138.359142 |
| [7] | Dershowitz, N., Okada, M.: A Rationale for Conditional Equational Programming. Theoret. Comput. Sci.75, 111-138 (1990) · Zbl 0702.68034 · doi:10.1016/0304-3975(90)90064-O |
| [8] | Dershowitz, N., Okada, M., Sivakumar, G.: Confluence of Conditional Rewrite Systems, Proceedings of the 1st International Workshop on Conditional Term Rewriting Systems, Orsay. Lecture Notes in Computer Science, vol 308, pp. 31-44. Berlin, Heidelberg, New York: Springer 1987 |
| [9] | Dershowitz, N., Okada, M., Sivakumar, G.: Canonical Conditional Rewrite System. Proceedings of the 9th Conference on Automated Deduction, Argonne, Lecture Notes in Computer Science, vol. 310, pp. 538-549. Berlin, Heidelberg, New York: Springer 1987 · Zbl 0667.68043 |
| [10] | Dershowitz, N., Plaisted, D. A.: Logic Programming cum Applicative Programming, Proceedings of the 2nd IEEE Symposium on Logic Programming, Boston, pp. 54-66, 1985 |
| [11] | Dershowitz, N., Plaisted, D. A.: Equational Programming. In: Machine Intelligence, vol. 11, Hayes, J. E., Michie, D., Richards, J. (eds). Oxford University Press, pp. 21-56, 1987 |
| [12] | Echahed, R.: On Completeness of Narrowing Strategies. Theoret. Comput. Sci.72, 133-146 (1990) · Zbl 0698.68027 · doi:10.1016/0304-3975(90)90032-D |
| [13] | Echahed, E.: Uniform Narrowing Strategies. Proceedings of the 3rd International Conference of Algebraic and Logic Programming. Volterra, Lecture Notes in Computer Science, vol. 632, pp. 259-275. Berlin, Heidelberg, New York: Springer 1992 |
| [14] | Fay, M.: First-Order Unification in Equational Theories. Proceedings of the 4th International Workshop on Automated Deduction, Austin, pp. 161-167, 1979 |
| [15] | Fribourg, L.: SLOG: A Logic Programming Language Interpreter based on Clausal Super-position and Rewriting. Proceedings of the 2nd IEEE Symposium on Logic Programming, Boston, pp. 172-184, 1985 |
| [16] | Giovannetti, E., Levi, G., Moiso, C., Palamidessi, C.: Kernel-LEAF: A Logic plus Functional Language. J. Comput. Syst. Sci.42, 139-185 (1991) · Zbl 0717.68013 · doi:10.1016/0022-0000(91)90009-T |
| [17] | Giovannetti, E., Moiso, C.: A Completeness Result for E-Unification Algorithms based on Conditional Narrowing. Proceedings of the Workshop on Foundations of Logic and Functional Programming, Trento, Lecture Notes in Computer Science, vol. 306, pp. 157-167. Berlin, Heidelberg, New York: Springer 1986 · Zbl 0645.68043 |
| [18] | Goguen, J. A., Meseguer, J.: EQLOG: Equality, Types and Generic Modules for Logic Programming. In: Logic Programming: Functions, Relations and Equations. De-Groot, D., Lindstrom, G. (eds). Prentice Hall, pp. 295-363, 1986 |
| [19] | Hanus, M.: Compling Logic Programs with Equality. Proceedings of the International Workshop on Language Implementation and Logic Programming, Linköping, Lecture Notes in Computer Science, vol. 456, pp. 387-401. Berlin, Heidelberg, New York: Springer 1990 |
| [20] | Herold, A.: Combination of Unification Algorithms in Equational Theories. Ph.D. thesis, Universität Kaiserslautern, 1987 · Zbl 0679.03002 |
| [21] | Huet, G., L’evy, J. J.: Computations in Orthogonal Rewriting Systems, I and II. In: Computational Logic, Essays in Honor of Alan Robinson. Lassez, J.-L., Plotkin, G. (eds.) The MIT Press, pp. 396-443, 1991. Previous version: Call by Need Computations in Non-Ambiguous Linear Term Rewriting Systems, report 359, INRIA, 1979 |
| [22] | Hölldobler, S.: Foundations of Equational Logic Programming. Lecture Notes in Artificial Intelligence, vol. 353, 1989 · Zbl 0688.68004 |
| [23] | Hullot, J.-M.: Canonical Forms and Unification. Proceedings of the 5th Conference on Automated Deduction. Lecture Notes in Computer Science, vol. 87, pp. 318-334. Berlin, Heidelberg, New York: Springer 1980 |
| [24] | Hullot, J.-M.: Compilation de Formes Canoniques dans les Théories Equationelles. Thèse de troisième cycle, Université de Paris Sud, Orsay, 1980 (In French) |
| [25] | Hußmann, H.: Unification in Conditional-Equational Theories. Proceedings of the European Conference on Computer Algebra. Lecture Notes in Computer Science, vol. 204, pp. 543-553. Berlin, Heidelberg, New York: Springer 1985 |
| [26] | Hußmann, H.: Corrigenda to MIP-8502 ?Unification in Conditional-Equational Theories?. Universität Passau, 1988 |
| [27] | Kaplan, S.: Conditional Rewrite Rules. Theoret. Comput. Sci.33(2), 175-193 (1984) · Zbl 0577.03013 · doi:10.1016/0304-3975(84)90087-2 |
| [28] | Kaplan, S.: Simplifying Conditional Term Rewriting Systems: Unification, Termination and Confluence. J. Symbolic Comput.4(3), 295-334 (1987) · Zbl 0641.68046 · doi:10.1016/S0747-7171(87)80010-X |
| [29] | Kirchner, C.: Méthodes et Outils de Conception Systématique d’Algorithmes d’Unification dans les Théories Equationelles, Thèse de d’état, Université de NancyI, 1985 (In French) |
| [30] | Klop, J. W.: Term Rewriting Systems: from Church-Rosser to Knuth-Bendix and beyond. Proceedings of the 17th International Colloquium on Automata, Languages and Programming, Warwick. Lecture Notes in Computer Science, vol. 443, pp. 350-369. Berlin, Heidelberg, New York: Springer 1990 · Zbl 0765.68008 |
| [31] | Klop, J. W.: Term Rewriting System. In: Handbook of Logic in Computer Science, Vol. II. Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Oxford University Press, pp. 1-112, 1992 |
| [32] | Krischer, S., Bockmayr, A.: Detecting Redundant Narrowing Derivations by the LSE-SL Reducibility Test. Proceedings of the 4th International Conference on Rewriting Techniques and Applications, Como. Lecture Notes in Computer Science, vol. 448, pp. 74-85. Berlin, Heidelberg, New York: Springer 1991 |
| [33] | Martelli, A., Montanari, U.: An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems4(2), 258-282 (1982) · Zbl 0478.68093 · doi:10.1145/357162.357169 |
| [34] | Middeldorp, A.: Modular Properties of Term Rewriting Systems. Ph.D. thesis, Vrije Universiteit, Amsterdam, 1990 · Zbl 0804.68071 |
| [35] | Moreno-Navarro, J. J., Rodríguez-Artalejo, M.: BABEL: A Functional and Logic Programming Language based on Constructor Discipline and Narrowing. Proceedings of the 1st International Conference on Algebraic and Logic Programming, Gaußig, Lecture Notes in Computer Science, vol. 343, pp. 223-232. Berlin, Heidelberg, New York: Springer 1989 · Zbl 0708.68015 |
| [36] | Nutt, W., Réty, P., Smolka, G.: Basic Narrowing Revisited. J. Symbolic Comput.7, 295-317 (1989) · Zbl 0682.68094 · doi:10.1016/S0747-7171(89)80014-8 |
| [37] | Réty, P.: Improving Basic Narrowing Techniques. Proceedings of the 2nd International Conference on Rewriting Techniques and Applications, Bordeaux. Lecture Notes in Computer Science, vol. 256, pp. 228-241. Berlin, Heidelberg, New York: Springer 1987 · Zbl 0638.68101 |
| [38] | Réty, P.: Méthodes d’Unification par Surréduction. Thèse de doctorat, Université de Nancy I, 1988 (In French) |
| [39] | Robinson, J. A.: A Machine-Oriented Logic Based on the Resolution Principle. J. ACM12(1), pp. 23-41 (1965) · Zbl 0139.12303 · doi:10.1145/321250.321253 |
| [40] | Shepherdson, J. C.: Mistakes in Logic Programming: the Role of Standardizing Apart, manuscript, University of Bristol, 1991 |
| [41] | Yamamoto, A.: Completeness of Extended Unification Based on Basic Narrowing. Proceedings of the 7th Logic Programming Conference, Jerusalem pp. 1-10, 1988 |
| [42] | You, Y. H.: Enumerating Outer Narrowing Derivations for Constructor Based Term Rewriting Systems. J. Symbolic Comput.7, 319-343 (1989) · Zbl 0678.68099 · doi:10.1016/S0747-7171(89)80015-X |
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.
