Propriété de Church-Rosser

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

Soit R un système de réécriture. Notons \rightarrow_R la relation de réduction, \rightarrow_R^* sa clôture réflexive et transitive, ainsi que \leftrightarrow_R^* sa clôture réflexive, transitive et symétrique.

On dit que R a la propriété de Church-Rosser si pour tous les termes M_1, M_2 tels que M_1 \leftrightarrow_R^* M_2, il existe un terme M' tel que M_1 \rightarrow_R^* M' et M_2 \rightarrow_R^* M'.

Cette propriété est équivalente à la propriété de confluence, notion de premier ordre dans la théorie des bases de Gröbner (en particulier dans la définition même de ces bases).

Exemple[modifier | modifier le code]

En lambda-calcul, on montre que la beta réduction (en) a la propriété de Church-Rosser[1].

Notes et références[modifier | modifier le code]

  1. Voir J.-L. Krivine en bibliographie, et Michel de Rougemont et Richard Lassaigne, Logique et fondements de l'informatique (logique du premier ordre, calculabilité et lambda calcul), Chapitre 9.2 : Réduction et forme normale, Hermes Science Publications, 1997, page 191.

Bibliographie[modifier | modifier le code]

  • Jean-Louis Krivine, Lambda-calcul, types et modèles. Masson, Paris, 1990 ; traduction anglaise : Lambda-calculus, types and models. Ellis Horwood, 1993. Voir la version anglaise en ligne p.18 sq.