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: 2926
Download times: 2235
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



Top Paper  |  FAQ  |  Guest Editors  |  Email Alert  |  Links  |  Copyright  |  Contact Us

© Copyright by Institute of Software, the Chinese Academy of Sciences

京公网安备 11040202500065号