×

Developing developments. (English) Zbl 0903.68104

Summary: In the absence of termination, confluence of rewriting systems is often hard to establish. The class of orthogonal rewriting systems is the main class of not-necessarily-terminating, but confluent rewriting systems. The reason why confluence holds in orthogonal rewriting systems is the absence of the so-called critical pairs, making that rewrite steps never interfere (in a destructive way) with one another. We discuss some ways to adapt the confluence by orthogonality proof method to rewriting systems having ‘innocent’ critical pairs. Confluence results are obtained for lambda calculus with beta, eta and omega rules, lambda calculi with restricted expansion rules and for (first- and higher-order) term rewriting systems for which all critical pairs are development closed.

MSC:

68Q42 Grammars and rewriting systems

Software:

Automath
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] ()
[2] Aczel, P., A general church-rosser theorem, ()
[3] Y. Akama, On Mints’ reduction for ccc-calculus, in: [8, pp. 1-12]. · Zbl 0786.03006
[4] Asperti, A.; Laneve, C., Interaction systems I: the theory of optimal reductions, Math. struct. comput. sci., 4, 457-504, (1994) · Zbl 0871.03006
[5] Asperti, A.; Laneve, C., Interaction systems II: the practice of optimal reductions, Theoret. comput. sci., 159, 191-244, (1996) · Zbl 0873.03015
[6] Barendregt, H.P., The lambda calculus, its syntax and semantics, () · Zbl 0467.03010
[7] H.P. Barendregt, Lambda calculi with types, in: [1, pp. 117-310].
[8] ()
[9] Bognar, M., A survey of abstract rewriting, ()
[10] Church, A.; Church, A., A set of postulates for the foundation of logic, Ann. math., Ann. math., 34, 839-864, (1933) · Zbl 0008.28902
[11] Church, A.; Rosser, J.B., Some properties of conversion, Trans. amer. math. soc., 39, 472-482, (1936) · Zbl 0014.38504
[12] Čubrić, D., Embedding of a free Cartesian closed category into the category of sets, (April 1993), On triples.math.mcgill.ca as pub/cubric/frccc.ps.gz
[13] Curry, H.B.; Curry, H.B., Grundlagen der kombinatorischen logik, Amer. J. math., Amer. J. math., LII, 789-834, (1930), Teil I, II · JFM 56.0048.03
[14] Curry, H.B.; Feys, R., Studies in logic and the foundations of mathematics, () · Zbl 0175.27601
[15] Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, (), 243-320 · Zbl 0900.68283
[16] Di Cosmo, R.; Kesner, D., Combining first order algebraic rewriting systems, recursion and extensional lambda calculi, (), 462-472 · Zbl 1418.68112
[17] Di Cosmo, R.; Kesner, D., Simulating expansions without expansions, Math. struct. comput. sci., 4, 1-48, (1994) · Zbl 0831.03004
[18] Di Cosmo, R.; Piperno, A., Expanding extensional polymorphism, (), 139-153 · Zbl 1063.68554
[19] ()
[20] Reprint, Ulmer Informatik Berichte Nr. 91-03, Universität Ulm.
[21] Girard, J.-Y.; Lafont, Y.; Taylor, P.; Girard, J.-Y.; Lafont, Y.; Taylor, P., Proofs and types, (), reprinting · Zbl 0647.03016
[22] Gonthier, G.; Lévy, J.-J.; Melliès, P.-A., An abstract standardisation theorem, (), 72-81
[23] Gramlich, B., Confluence without termination via parallel critical pairs, ()
[24] Hindley, J.R., The church-rosser property and a result in combinatory logic, () · Zbl 0514.03009
[25] Hindley, R., Reductions of residuals are finite, Trans. amer. math. soc., 240, 345-361, (1978) · Zbl 0387.03007
[26] Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, J. assoc. comput. machinery, 27, 797-821, (1980) · Zbl 0458.68007
[27] Huet, G., Residual theory in λ-calculus: a formal development, J. functional programming, 4, 371-394, (1994) · Zbl 0826.03008
[28] Kahrs, S., Context rewriting, (), 21-35
[29] Khasidashvili, Z.O., Expression reduction systems, (), 200-220, Tbilisi · Zbl 0731.03011
[30] Khasidashvili, Z., The church-rosser theorem in orthogonal combinatory reduction systems, Rapports de recherche 1825, INRIA-Rocquencourt, (December 1992)
[31] J.W. Klop, Term rewriting systems, in: [1, pp. 1-116].
[32] Klop, J.W., Combinatory reduction systems, () · Zbl 0466.03006
[33] Mathematical Centre Tracts, Vol. 127. · Zbl 0796.03024
[34] Melliés, P.-A., Description abstraite des systémes de Réécriture, (), to appear
[35] Miller, D., A logic programming language with lambda-abstraction, function variables, and simple unification, (), 253-281
[36] Mints, G.E., Closed categories and the theory of proofs, J. sov. math., 15, 45-62, (1981) · Zbl 0449.03054
[37] Translation into English of [38, pp. 83-114].
[38] (), Part II
[39] T. Nipkow, Orthogonal higher-order rewrite systems are confluent, in: [8, pp. 306-317]. · Zbl 0789.68081
[40] Nipkow, T., Higher-order critical pairs, (), 342-349
[41] V. van Oostrom, Development closed critical pairs, in: [19, pp. 185-200]. · Zbl 1407.68244
[42] van Oostrom, V., Confluence for abstract and higher-order rewriting, ()
[43] van Oostrom, V., Developing developments, (), extended abstract. · Zbl 0903.68104
[44] van Oostrom, V.; van Raamsdonk, F., Comparing combinatory reduction systems and higher-order rewrite systems, (), 276-304
[45] van Oostrom, V.; van Raamsdonk, F., Weak orthogonality implies confluence: the higher-order case, (), 379-392 · Zbl 0964.68523
[46] Prehofer, C., Solving higher-order equations: from logic to programming, () · Zbl 0922.68081
[47] van Raamsdonk, F., Confluence and superdevelopments, (), 168-182
[48] van Raamsdonk, F., Confluence and normalisation for higher-order rewriting, ()
[49] Rosen, B.K., Tree-manipulating systems and church-rosser theorems, J assoc. comput. machinery, 20, 160-187, (1973) · Zbl 0267.68013
[50] Schroer, D.E., The church-rosser theorem, ()
[51] Stell, J.G., Modelling term rewriting systems by sesqui-categories, ()
[52] M. Takahashi, λ-calculi with conditional rules, in: [8, pp. 406-417]. · Zbl 0806.03014
[53] Toyama, Y., On the church-rosser property of term rewriting systems, (), (in Japanese) · Zbl 1151.68453
[54] Toyama, Y., Commutativity of term rewriting systems, (), 393-407
[55] Wolfram, D.A., The clausal theory of types, () · 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. 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.