Confluence of Terminating Rewriting Computations

Overview & Synopsis

Rewriting is an intentional model of computation which is inherently non-deterministic. Defining functions by rewriting requires to prove that the result of a given computation is unique for every input, a property called confluence. This chapter describes confluence criteria for first-order as well as higher-order, terminating rewriting computations described by means of a set R of rewrite rules and a set E of equations such as associativity and commutativity. These criteria aim at reducing the confluence property of .(R, E) to the joinability of its critical pairs, obtained by overlapping left-hand sides of rules at subterms, which is the only source of non-trivial non-determinism. Joinability is the property that the normal forms of a pair of expressions resulting from an overlap are equal modulo E. Two properties are therefore needed: termination of rewriting modulo E, and existence of finitely many most general unifiers modulo E for computing the overlaps. We show that the first-order and higher-order case yield the same results, obtained by following a uniform approach. In the higher-order case, an abstract axiomatization of types is provided so as to capture by a single result typed computations based on different type systems.