Modular Church-Rosser Modulo: the Full Picture

Jean-Pierre Jouannaud 1 Yoshihito Toyama
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : 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 by Klop, Middledorp, Toyama and de Vrijer. 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 in two different properties: a cleaning lemma, whose goal is to anticipate the application of collapsing reductions; a modularity property of ordered completion, that allows to pairwise match the caps and alien substitutions of two equivalent terms. We then show that Toyama's modularity result scales up to rewriting modulo equations under natural assumptions met by all relations introduced in the litterature.
Type de document :
Article dans une revue
International Journal of Software and Informatics (IJSI), ISCAS, 2008
Liste complète des métadonnées

https://hal.inria.fr/inria-00350970
Contributeur : Jean-Pierre Jouannaud <>
Soumis le : jeudi 8 janvier 2009 - 08:38:57
Dernière modification le : vendredi 25 mai 2018 - 12:02:06

Identifiants

  • HAL Id : inria-00350970, version 1

Collections

Citation

Jean-Pierre Jouannaud, Yoshihito Toyama. Modular Church-Rosser Modulo: the Full Picture. International Journal of Software and Informatics (IJSI), ISCAS, 2008. 〈inria-00350970〉

Partager

Métriques

Consultations de la notice

163