×

Descendants and origins in term rewriting. (English) Zbl 1046.68564

Summary: In this paper we treat various aspects of a notion that is central in term rewriting, namely that of descendants or residuals. We address both first-order term rewriting and \(\lambda\)-calculus, their finitary as well as their infinitary variants. A recurrent theme is the parallel moves lemma. Next to the classical notion of descendant, we introduce an extended version, known as origin tracking. Origin tracking has many applications. Here it is employed to give new proofs of three classical theorems: the genericity lemma in \(\lambda\)-calculus, the theorem of Huet and Lévy on needed reductions in first-order term rewriting, and Berry’s sequentiality theorem in (infinitary) \(\lambda\)-calculus.

MSC:

68Q42 Grammars and rewriting systems
03B40 Combinatory logic and lambda calculus
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Abramsky, S.; Ong, C.-H. L., Full abstraction in the lazy lambda calculus, Inform. and Comput., 105, 159-267 (1993) · Zbl 0779.03003
[2] Aczel, P., Technical report (1978)
[3] Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge Univ. Press: Cambridge Univ. Press Cambridge
[4] Barendregt, H. P., Some Extensional Term Models for Combinatory Logics and \(λ\)-calculi (1971), University of Utrecht
[5] Barendregt, H. P., The Lambda Calculus, its Syntax and Semantics. The Lambda Calculus, its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, 103 (1984), North-Holland: North-Holland Amsterdam · Zbl 0551.03007
[6] Barendregt, H. P, Bergstra, J. A, Klop, J. W, and, Volken, H. 1976, Degrees, reductions and representability in the lambda calculus, Preprint 22, Department of Mathematics, Utrecht University.; Barendregt, H. P, Bergstra, J. A, Klop, J. W, and, Volken, H. 1976, Degrees, reductions and representability in the lambda calculus, Preprint 22, Department of Mathematics, Utrecht University. · Zbl 0399.03013
[7] Barendregt, H. P.; Kennaway, J. R.; Klop, J. W.; Sleep, M. R., Needed reduction and spine strategies for the lambda calculus, Inform. and Comput., 75, 191-231 (1987) · Zbl 0635.03009
[8] Berarducci, A.; Intrigila, B., Church-Rosser \(λ\)-theories, infinite \(λ\)-terms and consistency problems, (Steinhorn, C.; Hodges, W.; Hyland, M.; Truss, J., Logic: From Foundations to Applications; European Logic Colloquium 93, Keele, Staffordshire, England (1996), Oxford University Press: Oxford University Press Oxford), 33-58 · Zbl 0867.03004
[9] Berry, G., Séquentialité de l’évaluation formelle des lambda-expressions, (Robinet, B., Transformations de Programmes; 3e Colloque International sur la Programmation, Paris, France (1978), Dunod: Dunod Paris), 66-80 · Zbl 0416.03017
[10] Berry, G., Modèles complètement adéquats et stables des \(λ\)-calculs typés (1979), University of Paris 7
[11] Bertot, Y., Origin functions in \(λ\)-calculus and term rewriting systems, (Raoult, J.-C., 17th Colloquium on Trees in Algebra and Programming, CAAP’92, Rennes, France, February 26-28, 1992. 17th Colloquium on Trees in Algebra and Programming, CAAP’92, Rennes, France, February 26-28, 1992, Lecture Notes in Computer Science, 581 (1992), Springer-Verlag: Springer-Verlag Berlin), 49-65
[12] Boudol, G., Computational semantics of term rewriting systems, (Nivat, M.; Reynolds, J. C., Algebraic Methods in Semantics (Fontainebleau, 1982) (1985), Cambridge Univ. Press: Cambridge Univ. Press Cambridge), 169-236
[13] Church, A., The Calculi of Lambda Conversion (1941), Princeton University Press: Princeton University Press Princeton · JFM 67.0041.01
[14] Church, A.; Rosser, J. B., Some properties of conversion, Trans. Amer. Math. Soc., 39, 472-482 (1936) · Zbl 0014.38504
[15] Curien, P.-L., Categorical Combinatorics, Sequential Algorithms and Functional Programming (1993), Birkhäuser: Birkhäuser Boston
[16] Curry, H. B.; Feys, R., Combinatory Logic (1958), North-Holland: North-Holland Amsterdam · Zbl 0175.27601
[17] Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, (van Leeuwen, J., Formal Methods and Semantics, Handbook of Theoretical Computer Science (1990), MIT Press: MIT Press Cambridge), 243-320 · Zbl 0900.68283
[18] Derschowitz, N.; Kaplan, S.; Plaisted, D. A., Infinite normal forms, ICALP’89. ICALP’89, Lecture Notes in Computer Science, 372 (1989), p. 249-262
[19] Farmer, W. M.; Watro, R. J., Technical report (1989)
[20] Field, J.; Tip, F., Dynamic dependence in term rewriting systems and its application to program slicing, (Hermenegildo, M.; Penjam, J., Proceedings of the Sixth International Symposium on Programming Language Implementation and Logic Programming, PLILP’94. Proceedings of the Sixth International Symposium on Programming Language Implementation and Logic Programming, PLILP’94, Lecture Notes in Computer Science, 844 (1994), Springer-Verlag: Springer-Verlag Berlin), 415-431
[21] Glauert, J.; Khasidashvili, Z., Relative normalization in orthogonal expression reduction systems, (Dershowitz, N.; Lindenstrauss, N., Workshop on Conditional (and Typed) Term Rewriting Systems, CTRS’94. Workshop on Conditional (and Typed) Term Rewriting Systems, CTRS’94, Lecture Notes in Computer Science, 968 (1994), Springer-Verlag: Springer-Verlag Berlin), 144-165
[22] Glauert, J.; Khasidashvili, Z., Relative normalization in deterministic residual structures, (Kirchner, H., Proceedings of the 19th International Colloquium on Trees in Algebra and Programming, CAAP ’96. Proceedings of the 19th International Colloquium on Trees in Algebra and Programming, CAAP ’96, Lecture Notes in Computer Science, 1059 (1996), Springer-Verlag: Springer-Verlag Berlin), 180-195 · Zbl 1508.68155
[23] Gonthier, G.; Lévy, J.-J.; Melliès, P.-A., An abstract standardisation theorem, Proceedings of 7th Annual Symposium on Logic in Computer Science, LICS ’92, Santa Cruz, CA (1992), IEEE Computer Society Press: IEEE Computer Society Press Los Alamitos, p. 72-81
[24] Hindley, J. R., An abstract form of the Church-Rosser theorem, I, J. Symbolic Logic, 34, 545-560 (1969) · Zbl 0195.02102
[25] Hindley, J. R., An abstract Church-Rosser theorem, II, applications, J. Symbolic Logic, 39, 1-22 (1974) · Zbl 0291.02015
[26] Hindley, R., The equivalence of complete reductions, Trans. Amer. Math. Soc., 229, 227-248 (1977) · Zbl 0361.02036
[27] Huet, G.; Lévy, J.-J., Computations in orthogonal rewriting systems, (Lassez, J.-J.; Plotkin, G., Computational Logic: Essays in honor of Alan Robinson (1991), The MIT Press: The MIT Press Cambridge), 395-443
[28] Hudak, P. 1988, Report on the functional programming language Haskell, Draft proposed standard.; Hudak, P. 1988, Report on the functional programming language Haskell, Draft proposed standard.
[29] Kennaway, J. R.; Klop, J. W.; Sleep, M. R.; de Vries, F. J., An infinitary Church-Rosser property for non-collapsing orthogonal term rewriting systems, (Sleep, M. R.; Plasmeijer, M. J.; van Eekelen, M. C.J. D., Term Graph Rewriting—Theory and Practice (1993), Wiley: Wiley New York), 47-59
[30] Kennaway, J. R.; Klop, J. W.; Sleep, M. R.; de Vries, F. J., Infinitary lambda calculus and Böhm models, Proceedings of the Conference on Rewriting Techniques and Applications, RTA95, Kaiserslautern. Proceedings of the Conference on Rewriting Techniques and Applications, RTA95, Kaiserslautern, Lecture Notes in Computer Science, 914 (1995), Springer-Verlag: Springer-Verlag Berlin, p. 257-270 · Zbl 1503.03025
[31] Kennaway, J. R.; Klop, J. W.; Sleep, M. R.; de Vries, F. J., Transfinite reductions in orthogonal term rewriting systems, Inform. and Comput., 119, 18-38 (1995) · Zbl 0832.68063
[32] Kennaway, J. R.; Klop, J. W.; Sleep, M. R.; de Vries, F. J., Infinitary lambda calculus, Theoret. Comput. Sci., 175, 93-125 (1997) · Zbl 0903.68105
[33] Kennaway, J. R.; van Oostrom, V.; de Vries, F. J., Meaningless terms in rewriting, J. Funct. Logic Progr., 1999 (1999) · Zbl 0924.68107
[34] Khasidashvili, Z. O., \(β\)-reductions and \(β\)-developments of \(λ\)-terms with the least number of steps, COLOG-88 (Tallinn, 1988) (1990), Springer-Verlag: Springer-Verlag Berlin, p. 105-111 · Zbl 0716.03004
[35] Khasidashvili, Z., Optimal normalization in orthogonal term rewriting systems, Rewriting Techniques and Applications (Montreal, 1993) (1993), Springer-Verlag: Springer-Verlag Berlin, p. 243-258 · Zbl 1508.68162
[36] Khasidashvili, Z.; Glauert, J., Discrete normalization in deterministic residual structures, (Hanus, M.; Rodrı́guez-Artalejo, M., Proceedings of the 5th International Conference on Algebraic and Logic Programming, ALP ’96. Proceedings of the 5th International Conference on Algebraic and Logic Programming, ALP ’96, Lecture Notes in Computer Science, 1139 (1996), Springer-Verlag: Springer-Verlag Berlin), 135-149 · Zbl 1355.68139
[37] Khasidashvili, Z.; Glauert, J., The geometry of orthogonal reduction spaces, (Degano, P.; Gorrieri, R.; Marchetti-Spaccamela, A., Proceedings of the 24th International Colloquium on Automata, Languages, and Programming, ICALP ’97. Proceedings of the 24th International Colloquium on Automata, Languages, and Programming, ICALP ’97, Lecture Notes in Computer Science, 1256 (1997), Springer-Verlag: Springer-Verlag Berlin), 649-659 · Zbl 1401.68137
[38] Khasidashvili, Z.; van Oostrom, V., Context-sensitive conditional expression reduction systems, Electronic Notes in Theoretical Computer Science, SEGRAGRA ’95, Joint COMPUGRAPH/SEMAGRAPH Workshop on Graph Rewriting and Computation, Volterra (1995), p. 141-150 · Zbl 0910.68098
[39] Klop, J. W., Combinatory Reduction Systems. Combinatory Reduction Systems, Mathematical Centre Tracts Number 127 (1980), CWI: CWI Amsterdam · Zbl 0466.03006
[40] Klop, J. W., Report (1990)
[41] Klop, J. W., Term rewriting systems, (Abramsky, S.; Gabbay, D.; Maibaum, T., Handbook of Logic in Computer Science (1992), Oxford University Press: Oxford University Press Oxford) · Zbl 0657.68028
[42] 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
[43] Klop, J. W.; de Vrijer, R. C., Extended rewriting systems, (Kaplan, S.; Okada, M., Proceedings of the Workshop on Conditional an Typed Rewriting Systems, Montreal. Proceedings of the Workshop on Conditional an Typed Rewriting Systems, Montreal, Lecture Notes in Computer Science, 516 (1991), Springer-Verlag: Springer-Verlag Berlin), 26-50 · Zbl 1507.68151
[44] Krivine, J. L., Lambda-calculus, Types and Models (1993), Massan: Massan Paris · Zbl 0779.03005
[45] Kuper, J., Partiality in Logic and Computation (1994), University of Twente
[46] Lévy, J.-J., An algebraic interpretation of \(λ\)-calculus and a labelled \(λ\)-calculus, (Böhm, C., \(λ\)-calculus and Computer Science. \(λ\)-calculus and Computer Science, Lecture Notes in Computer Science, 37 (1975), Springer-Verlag: Springer-Verlag Berlin), 147-165
[47] Lévy, J.-J., Réductions correctes et optimales dans le lambda-calcul (1978), Université de Paris VII
[48] Maranget, L., La stratégie paresseuse (1992), L’Université Paris VII
[49] Melliès, P.-A., Axiomatic rewriting theory III: A factorisation theorem in rewriting theory, Proceedings of the 7th Conference on Category Theory and Computer Science, CTCS ’97, Santa Margherita Ligure. Proceedings of the 7th Conference on Category Theory and Computer Science, CTCS ’97, Santa Margherita Ligure, Lecture Notes in Computer Science, 1290 (1997), Springer-Verlag: Springer-Verlag Berlin, p. 46-68 · Zbl 0888.68075
[50] Melliès, P.-A., Axiomatic rewriting theory IV: A stability theorem in rewriting theory, Proceedings of the 14th Annual Symposium on Logic in Computer Science, LICS ’98, Indianapolis (1998), IEEE Computer Society Press: IEEE Computer Society Press Los Alamitos, p. 287-298 · Zbl 0945.03529
[51] Middeldorp, A., Call by need computations to root-stable form, Proceedings of the 24th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’97 (1997), p. 94-105
[52] Newman, M. H.A., On theories with a combinatorial definition of “equivalence”, Ann. of Math., 43, 223-243 (1942) · Zbl 0060.12501
[53] Nederpelt, R. P.; Geuvers, J. H.; de Vrijer, R. C., Selected Papers on Automath. Selected Papers on Automath, Studies in Logic and the Foundations of Mathematics, 133 (1994), North-Holland: North-Holland Amsterdam
[54] Nipkow, T., Higher-order critical pairs, Proceedings of the sixth annual IEEE Symposium on Logic in Computer Science (1991), IEEE Computer Society Press: IEEE Computer Society Press Los Alamitos, p. 342-349
[55] Nipkow, T., Orthogonal higher-order rewrite systems are confluent, Proceedings of the International Conference on Typed Lambda Calculi and Application (1993), p. 306-317 · Zbl 0789.68081
[56] O’Donnell, M. J., Computing in Systems Described by Equations. Computing in Systems Described by Equations, Lecture Notes in Computer Science, 58 (1977), Springer-Verlag: Springer-Verlag Berlin · Zbl 0421.68038
[57] van Oostrom, V., Confluence for Abstract and Higher-Order Rewriting (1994), Vrije Universiteit: Vrije Universiteit Amsterdam
[58] van Oostrom, V., Technical report (1996)
[59] van Oostrom, V., Developing developments, Theoret. Comput. Sci., 175, 159-181 (1997) · Zbl 0903.68104
[60] van Oostrom, V., Finite family developments, (Comon, H., Rewriting Techniques and Applications. 8th International Conference, RTA 97. Rewriting Techniques and Applications. 8th International Conference, RTA 97, Lecture Notes in Computer Science, 1232 (1997), Springer-Verlag: Springer-Verlag Berlin), 308-322 · Zbl 1379.68208
[61] van Oostrom, V., Normalisation in weakly orthogonal rewriting, (Narendran, P.; Rusinowitch, M., 10th International Conference on Rewriting Techniques and Applications, RTA ’99, Trento, June. 10th International Conference on Rewriting Techniques and Applications, RTA ’99, Trento, June, Lecture Notes in Computer Science, 1631 (1999), Springer-Verlag: Springer-Verlag Berlin), 60-74
[62] van Oostrom, V.; van Raamsdonk, F., Weak orthogonality implies confluence: The higher-order case, (Nerode, A.; Matiyasevich, Yu. V., Proceedings of the Third International Symposium on Logical Foundations of Computer Science. Proceedings of the Third International Symposium on Logical Foundations of Computer Science, Lecture Notes in Computer Science, 813 (1994), Springer-Verlag: Springer-Verlag Berlin), 379-392 · Zbl 0964.68523
[63] Plasmeijer, M. J.; van Eekelen, M. C.J. D., Functional Programming and Parallel Graph Rewriting (1993), Addison-Wesley: Addison-Wesley Reading · Zbl 0639.68028
[64] Plotkin, G. 1978, Church-Rosser categories, manuscript.; Plotkin, G. 1978, Church-Rosser categories, manuscript.
[65] van Raamsdonk, F., Confluence and superdevelopments, (Kirchner, C., Proceedings of the 5th International Conference on Rewriting Techniques and Applications (RTA 93). Proceedings of the 5th International Conference on Rewriting Techniques and Applications (RTA 93), Lecture Notes in Computer Science, 690 (1993), Springer-Verlag: Springer-Verlag Berlin), 168-182 · Zbl 1503.68165
[66] van Raamsdonk, F., Confluence and Normalisation for Higher-Order Rewriting (1996), Vrije Universiteit Amsterdam
[67] Takahashi, M., Parallel reductions in \(λ\)-calculus, Inform. and Comput., 118, 120-127 (1995) · Zbl 0827.68060
[68] Tip, F., Generation of Program Analysis Tools (1995), Universiteit van Amsterdam
[69] Turner, D. A., Miranda: a non-strict functional language with polymorphic types, (Jouannaud, J.-P., Proceedings of the ACM Conference on Functional Programming Languages and Computer Architecture. Proceedings of the ACM Conference on Functional Programming Languages and Computer Architecture, Lecture Notes in Computer Science, 201 (1985), Springer-Verlag: Springer-Verlag Berlin), 1-16 · Zbl 0592.68014
[70] de Vrijer, R. C., A direct proof of the finite development theorem, J. Symbolic Logic, 50, 339-343 (1985) · Zbl 0601.03001
[71] de Vrijer, R. C., Surjective Pairing and Strong Normalization: Two Themes in Lambda Calculus (1987), University of Amsterdam
[72] de Vrijer, R. C., Extending the lambda calculus with surjective pairing is conservative, Proceedings of the 4th IEEE Symposium on Logic in Computer Science, Asilomar, CA (1989), p. 204-215 · Zbl 0716.03006
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.