Propriété de Church-Rosser
Modèle:Voir homonymes {{#invoke:Bandeau|ébauche}}
En informatique théorique et en logique mathématique, la propriété de Church-Rosser est une propriété des systèmes de réécriture. Elle est nommée ainsi d'après les mathématiciens Alonzo Church et John Barkley Rosser.
Définition
Soit <math>R</math> un système de réécriture, et notons <math>\rightarrow_R</math> la relation de réduction, <math>\rightarrow_R^*</math> sa clôture réflexive transitive, et enfin <math>\longleftrightarrow_R^*</math> sa clôture réflexive, transitive et symétrique.
On dit que <math>R</math> a la propriété de Church-Rosser si, pour toute paire de termes <math>M_1, M_2</math> tels que <math>M_1 \longleftrightarrow_R^* M_2</math>, il existe un terme <math>M</math> tel que <math>M_1 \rightarrow_R^* M</math> et <math>M_2 \rightarrow_R^* M</math>.
Théorème de Church-Rosser
Le théorème de Church-Rosser est un résultat du lambda-calcul. Il énonce que la bêta-réduction possède la propriété de Church-Rosser<ref>Modèle:Harvsp.</ref>,<ref>Modèle:Harvsp.</ref>.
Ce théorème a été établi par Church et Rosser en 1936<ref>Modèle:Article.</ref>. Le résultat reste vrai dans diverses variantes et extensions du lambda-calcul.
Exemple d'application
Pour les systèmes de réécriture, la propriété de Church-Rosser est équivalente à la propriété de confluence, notion de première importance dans la théorie des bases de Gröbner (en particulier dans la définition même de ces bases).
Notes et références
Bibliographie
- Modèle:Ouvrage. Traduction anglaise : Modèle:Ouvrage.
- Modèle:Ouvrage.
- Modèle:Ouvrage.
