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.
CITATION STYLE
Curien, P. L., & Ghelli, G. (1991). On confluence for weakly normalizing systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 488 LNCS, pp. 215–225). Springer Verlag. https://doi.org/10.1007/3-540-53904-2_98
Mendeley helps you to discover research relevant for your work.