Une approche générique de la réécriture
Dans cet article, nous étudions la réécriture en tant que système de preuve opérationnel de façon générique (c'est-à-dire indépendamment de la logique sous-jacente). Dans ce but, nous proposons des conditions simples qui permettent de caractériser les logiques où ce type de preuve effective peut être appliqué. Ces conditions sont fondées sur une propriété définie sur les arbres de preuve, que nous appelons semi-commutation. Nous montrons alors comment axiomatiser les notions usuelles de terminaison, confluence et confluence locale au sein de ce métaformalisme. Cela nous permet de retrouver les résultats fondamentaux de Church-Rosser et Newman et de proposer une méthode de complétion de Knuth et Bendix générique.
In this paper we study rewriting as an operational proof system in a generic (i.e. logic-independent) way. To do this, we propose simple conditions which allow to characterise logics were this kind of effective proof can be applied. This conditions are based on a proof tree property, that we call semi-commutation. We then show how to define the standard notions of termination, confluence and local confluence in this meta-formalism. It allows us to obtain the fundamental results of Church-Rosser and Newman and to propose a generic Knuth and Bendix completion method.
M.AIGUIER, D.BAHRAMI
réécriture abstraite, logicalité, propriété de Church-Rosser, lemme de Newman, système de Knuth et Bendix, complétion de Knuth et Bendix.
abstract rewriting, logicality, Church-Rosser property, Diamond lemma, Knuth and Bendix system, Knuth and Bendix completion.
Français
|
