| Modular Church-Rosser Modulo:The Complete Picture |
| Received:July 19, 2008 Revised:June 23, 2008 Download PDF |
| Jean-Pierre Jouannaud,Yoshihito Toyama. Modular Church-Rosser Modulo:The Complete Picture. International Journal of Software and Informatics, 2008,2(1):61~75 |
| Hits: 3306 |
| Download times: 2672 |
| Jean-Pierre Jouannaud Yoshihito Toyama |
|
| Fund:The present paper is an improved version of Ref.[5] in which proofs have been greatly simplified and results made as general as it could possibly be. |
|
| Abstract:In Ref.[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 Refs.[8,12]. In this paper, 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 di?erent 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. |
| keywords:term rewriting confiuence modularity modulo |
| View Full Text View/Add Comment Download reader |
|
|
|
