Modular Church-Rosser Modulo: The Complete Picture

12 years 5 months ago
Modular Church-Rosser Modulo: The Complete Picture
In [19], Toyama proved that the union of two confluent term-rewriting systems that share absolutely no function symbols or constants is likewise confluent, a property called modularity. The proof of this beautiful modularity result, technically based on slicing terms into an homogeneous cap and a so called alien, possibly heterogeneous substitution, was later substantially simplified in [8, 12]. In this paper3 , we present a further simplification of the proof of Toyama's result for confluence, which shows that the crux of the problem lies on two different properties: a cleaning lemma, whose goal is to anticipate the application of collapsing reductions and a modularity property of ordered completion that allows to pairwise match the caps and alien substitutions of two equivalent terms obtained from the cleaning lemma. The approach allows for arbitrary kinds of rules, and scales up to rewriting modulo arbitrary sets of equations.
Jean-Pierre Jouannaud, Yoshihito Toyama
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2008
Where IJSI
Authors Jean-Pierre Jouannaud, Yoshihito Toyama
Comments (0)