Abstract
We present a general, abstract method to show confluence of weakly normalizing systems. The technique consists in constructing an interpretation of the source system into a target system which is already confluent. If the interpretation satisfies certain simple conditions, then the source system is confluent. The method has been used implicitly in a number of applications, but does not seem to have been presented so far in its generality. We present, as digressions, two other methods for proving confluence.
This work was carried on with the partial support of E.E.C., Esprit Basic Research Action 3070 FIDE and of Italian C.N.R., P.F.I. “Sistemi informatici e calcolo parallelo”.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi, L. Cardelli, P.-L. Curien, J.-J. Lévy, Explicit Substitutions, Proc. POPL 90, San Francisco, ACM (1990).
V. Breazu-Tannen, T. Coquand, C. Gunter, A. Scedrov, Inheritance and Explicit Coercion, Proc. Logic in Computer Science 89, Monterey, USA (1989).
V. Breazu-Tannen, J. Gallier, Polymorphic Rewriting Conserves Algebraic Confluence, Proc. ICALP 89, Stresa, Lecture Notes in Comput. Sci. 372 (1989).
P.-L. Curien, Categorical Combinators, Sequential Algorithms and Functional Programming, Pitman (1986).
P.-L. Curien, Roberto Di Cosmo, Confluence in the typed λ-calculus extended with Surjective Pairing and a Terminal Type, draft (1990).
P.-L. Curien, G. Ghelli, Coherence of Subsumption, Proc. Colloque sur les Arbres en Algèbre et en Programmation 90, Lecture Notes in Comput. Sci. 431 (1990).
P.-L. Curien, G. Ghelli, Subtyping + Extensionality: Confluence of βη reduction in F≤, draft (1990).
L. Cardelli, P. Wegner, On Understanding Types, Data Abstraction and Polymorphism, ACM Computing Surveys, 17 (4) (1985).
D. van Daalen, The Language Theory of Automath, PhD Thesis, Technical University of Eindhoven, 1980.
J.-Y. Girard, Y. Lafont, P. Taylor, Proofs and Types, Cambridge University Press (1989).
T. Hardin, Confluence Results for the Pure Strong Categorical Combinatory Logic CCL: λ-calculi as Subsystems of CCL, Theoret. Comput. Sci. 65, 291–342 (1989).
R. Harper, F. Honsell, G. Plotkin, A Framework for Defining Logics, Proc. Logic in Computer Science 87, Ithaca (1987).
G. Huet, D.C. Oppen, Equations and Rewrite Rules: A Survey, in Formal Languages Theory: Perspective and Open Problems, R. Book ed., 349–393, Academic Press (1980).
J.-W. Klop, Combinatory Reduction Systems, Mathematical Center Tracts 127 (1980).
J.-W. Klop, R. de Vrijer, Unique Normal Forms for Lambda-calculus with Surjective Pairing, Information and Computation (1989).
G. Pottinger, The Church Rosser Theorem for the Typed lambda-calculus with Surjective Pairing, Notre Dame Journal of Formal Logic 22 (3), 264–68 (1981).
A. Salvesen, The Church-Rosser Theorem for LF with βη-reduction, draft (1989).
Y. Toyama, Term Rewriting Systems and the Church-Rosser Property, PhD Thesis, Tohoku University, 1990.
R. de Vrijer, Surjective Pairing and Strong Normalization, Two Themes in Lambda-calculus, PhD Thesis, Universiteit van Amsterdam, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Curien, PL., Ghelli, G. (1991). On confluence for weakly normalizing systems. In: Book, R.V. (eds) Rewriting Techniques and Applications. RTA 1991. Lecture Notes in Computer Science, vol 488. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53904-2_98
Download citation
DOI: https://doi.org/10.1007/3-540-53904-2_98
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53904-9
Online ISBN: 978-3-540-46383-2
eBook Packages: Springer Book Archive