Higher-order rewrite systems and their confluence. (English) Zbl 0895.68078
Summary: We study higher-order rewrite systems (HRSs) which extend term rewriting to \(\lambda\)-terms. HRSs can describe computations over terms with bound variables. We show that rewriting with HRSs is closely related to undirected equational reasoning. We define pattern rewrite systems (PRSs) as a special case of HRSs and extend three confluence results from term rewriting to PRSs: the critical pair lemma by Knuth and Bendix, confluence of rewriting modulo equations à la Huet, and confluence of orthogonal PRSs.
MSC:
| 68Q42 | Grammars and rewriting systems |
Keywords:
higher-order rewrite systemsReferences:
| [1] | Aczel, P., A general Church-Rosser theorem, Tech. Report, Univ. of Manchester (1978) |
| [2] | Barbanera, F.; Fernández, M.; Geuvers, H., Modularity of strong normalization and confluence in the algebraic λ-cube, (9th IEEE Symp. Logic in Computer Science, IEEE Computer Society Press. 9th IEEE Symp. Logic in Computer Science, IEEE Computer Society Press, Silver Spring, MD (1994)), 406-415 |
| [3] | Barendregt, H. P., The Lambda Calculus, its Syntax and Semantics (1984), North-Holland: North-Holland Amsterdam · Zbl 0551.03007 |
| [4] | Barendregt, H. P., Lambda calculi with types, (Abramsky, S.; Gabbay, D. M.; Maibaum, T. S.E., Handbook of Logic in Computer Science, vol. 2 (1992), Oxford Univ. Press: Oxford Univ. Press Oxford), 118-309 · Zbl 0806.68003 |
| [5] | Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, (van Leeuwen, J., Formal Models and Semantics. Formal Models and Semantics, Handbook of Theoretical Computer Science, vol. B (1990), Elsevier: Elsevier Amsterdam), 243-320 · Zbl 0900.68283 |
| [6] | Dougherty, D. J., Adding algebraic rewriting to the untyped lambda-calculus, (Book, R. V., Proc. 4th Int. Conf. Rewriting Techniques and Applications. Proc. 4th Int. Conf. Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 488 (1991), Springer: Springer Berlin), 34-48 · Zbl 1503.03023 |
| [7] | Gallier, J. H., Logic for Computer Science (1986), Harper & Row: Harper & Row New York · Zbl 0605.03004 |
| [8] | Goldfarb, W. D., The undecidability of the second-order unification problem, Theoret. Comput. Sci., 13, 225-230 (1981) · Zbl 0457.03006 |
| [9] | Gordon, M. J.C.; Melham, T. F., Introduction to HOL: A Theorem-Proving Environment for Higher Order Logic (1993), Cambridge Univ. Press: Cambridge Univ. Press Cambridge · Zbl 0779.68007 |
| [10] | Hindley, J. R.; Seldin, J. P., Introduction to Combinators and λ-Calculus (1986), Cambridge Univ. Press: Cambridge Univ. Press Cambridge · Zbl 0614.03014 |
| [11] | Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, J. ACM, 27, 797-821 (1980) · Zbl 0458.68007 |
| [12] | Huet, G.; Lévy, J.-J., Computations in orthogonal rewriting systems, (Lassez, J.-L.; Plotkin, G., Computational Logic: Essays in Honor of Alan Robinson (1991), MIT Press: MIT Press Cambridge, MA), 395-443 · Zbl 0793.03002 |
| [13] | Jouannaud, J.-P.; Rubio, A., Higher-order simplification orderings, (Comon, H., Rewriting Techniques and Applications. Rewriting Techniques and Applications, Lecture Notes in Computer Science (1997), Springer: Springer Berlin) |
| [14] | Kahrs, S., Towards a domain theory for termination proofs, (Hsiang, J., Rewriting Techniques and Applications. Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 914 (1995), Springer: Springer Berlin), 241-255 · Zbl 1503.68120 |
| [15] | Kahrs, S., The variable containment problem, (Dowek, G.; Heering, J.; Meinke, K.; Möller, B., Higher-Order Algebra, Logic, and Term Rewriting. Higher-Order Algebra, Logic, and Term Rewriting, Lecture Notes in Computer Science, vol. 1074 (1996), Springer: Springer Berlin), 109-123 · Zbl 1407.68090 |
| [16] | Klop, J. W., Combinatory Reduction Systems, (Mathematical Centre Tracts, vol. 127 (1980), Mathematisch Centrum: Mathematisch Centrum Amsterdam) · Zbl 0466.03006 |
| [17] | Klop, J. W., Term rewriting systems, (Abramsky, S.; Gabbay, D. M.; Maibaum, T. S.E., Handbook of Logic in Computer Science, vol. 2 (1992), Oxford Univ. Press: Oxford Univ. Press Oxford), 2-116 · Zbl 0777.68001 |
| [18] | Klop, J. W.; van Oostrom, V.; van Raamsdonk, F., Combinatory reduction systems: introduction and survey, Theoret. Comput. Sci., 121, 279-308 (1993) · Zbl 0796.03024 |
| [19] | Knuth, D. E.; Bendix, P. B., Simple word problems in universal algebra, (Leech, J., Computational Problems in Abstract Algebra (1970), Pergamon Press: Pergamon Press Oxford), 263-297 · Zbl 0188.04902 |
| [20] | Loría-Sáenz, C. A., A theoretical framework for reasoning about program construction based on extensions of rewrite systems, (Ph.D. Thesis (1993), Universität Kaiserslautern) |
| [21] | Lysne, O.; Piris, J., A termination ordering for higher-order rewrite systems, (Hsiang, J., Rewriting Techniques and Applications. Rewriting Techniques and Applications, Lecture Notes in Computer Science (1995), Springer: Springer Berlin), 26-40 · Zbl 1503.68134 |
| [22] | Mayr, R., Konfluenz bei Termersetzungssystemen auf λ-Termen, (Master’s Thesis (1994), Institut für Informatik, Technische Universität München) |
| [23] | Miller, D., A logic programming language with lambda-abstraction, function variables, and simple unification, J. Logic Comput., 1, 4, 497-536 (1991) · Zbl 0738.68016 |
| [24] | Müller, F., Confluence of the lambda-calculus with left-linear algebraic rewriting, Inform. Process. Lett., 41, 293-299 (1992) · Zbl 0780.68079 |
| [25] | Nipkow, T., Higher-order critical pairs, (6th IEEE Symp. Logic in Computer Sci., IEEE Computer Soc. Press. 6th IEEE Symp. Logic in Computer Sci., IEEE Computer Soc. Press, Silver Spring, MD (1991)), 342-349 |
| [26] | Nipkow, T., Functional unification of higher-order patterns, (8th IEEE Symp. Logic in Computer Science, IEEE Computer Soc. Press. 8th IEEE Symp. Logic in Computer Science, IEEE Computer Soc. Press, Silver Spring, MD (1993)), 64-74 |
| [27] | Nipkow, T., Orthogonal higher-order rewrite systems are confluent, (Bezem, M.; Groote, J. F., Proc. Int. Conf. Typed Lambda Calculi and Applications. Proc. Int. Conf. Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, vol. 664 (1993), Springer: Springer Berlin), 306-317 · Zbl 0789.68081 |
| [28] | O’Donnell, M. J., Computing in Systems Described by Equations, (Lecture Notes in Computer Science, vol. 58 (1977), Springer: Springer Berlin) · Zbl 0421.68038 |
| [29] | van Oostrom, V., Confluence for abstract and higher-order rewriting, (Ph.D. Thesis (1994), Vrije Universiteit: Vrije Universiteit Amsterdam) |
| [30] | van Oostrom, V.; van Raamsdonk, F., Comparing combinatory reduction systems and higher-order rewrite systems, (Heering, J.; Meinke, K.; Möller, B.; Nipkow, T., Higher-Order Algebra, Logic and Term Rewriting. Higher-Order Algebra, Logic and Term Rewriting, Lecture Notes in Computer Science, vol. 816 (1994), Springer: Springer Berlin), 276-304 |
| [31] | van Oostrom, V.; van Raamsdonk, F., Weak orthogonality implies confluence: the higher-order case, (Nerode, A., Logical Foundations of Computer Science. Logical Foundations of Computer Science, Lecture Notes in Computer Science, vol. 813 (1994), Springer: Springer Berlin), 379-392 · Zbl 0964.68523 |
| [32] | Padovani, V., On equivalence classes of interpolation equations, (Dezani-Ciancaglini, M.; Plotkin, G., Typed Lambda Calculi and Applications. Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, vol. 902 (1995), Springer: Springer Berlin), 335-349 · Zbl 1063.03523 |
| [33] | Paulson, L. C., Isabelle: A Generic Theorem Prover, (Lecture Notes in Computer Science, vol. 828 (1994), Springer: Springer Berlin) · Zbl 0825.68059 |
| [34] | van de Pol, J., Termination proofs for higher-order rewrite systems, (Heering, J.; Meinke, K.; Möller, B.; Nipkow, T., Higher-Order Algebra, Logic and Term Rewriting. Higher-Order Algebra, Logic and Term Rewriting, Lecture Notes in Computer Science, vol. 816 (1994), Springer: Springer Berlin), 305-325 |
| [35] | van de Pol, J.; Schwichtenberg, H., Strict functionals for termination proofs, (Dezani-Ciancaglini, M.; Plotkin, G., Typed Lambda Calculi and Applications. Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, vol. 902 (1995), Springer: Springer Berlin), 350-364 · Zbl 1063.03505 |
| [36] | Qian, Z., Linear unification of higher-order patterns, (Gaudel, M.-C.; Jouannaud, J.-P., Proc. Coll. Trees in Algebra and Programming. Proc. Coll. Trees in Algebra and Programming, Lecture Notes in Computer Science, vol. 668 (1993), Springer: Springer Berlin), 391-405 · Zbl 1497.68096 |
| [37] | van Raamsdonk, F., Confluence and superdevelopments, (Kirchner, C., Rewriting Techniques and Applications. Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 690 (1993), Springer: Springer Berlin), 168-182 · Zbl 1503.68165 |
| [38] | van Raamsdonk, F., Confluence and normalization for higher-order rewriting, (Ph.D. Thesis (1996), Vrije Universiteit: Vrije Universiteit Amsterdam) |
| [39] | Stenlund, S., Combinators, λ-Terms, and Proof Theory (1972), D. Reidel: D. Reidel Dordrecht · Zbl 0248.02032 |
| [40] | Takahashi, M., λ-calculi with conditional rules, (Bezem, M.; Groote, J. F., Typed Lambda Calculi and Applications. Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, vol. 664 (1993), Springer: Springer Berlin), 406-417 · Zbl 0806.03014 |
| [41] | Wolfram, D. A., The Clausal Theory of Types, (Cambridge Tracts in Theoretical Computer Science, vol. 21 (1993), Cambridge Univ. Press: Cambridge Univ. Press Cambridge) · Zbl 0782.68007 |
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.
