Propriété de Church-Rosser

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 $R$ un système de réécriture, et notons ${\to }_R$ la relation de réduction, $\underset{R}{\overset{*}{\to }}$ sa clôture réflexive transitive, et enfin $\underset{R}{\overset{*}{⟷}}$ sa clôture réflexive, transitive et symétrique.

On dit que $R$ a la propriété de Church-Rosser si, pour toute paire de termes $M_1,M_2$ tels que $M_1\underset{R}{\overset{*}{⟷}}{M}_2$, il existe un terme $M$ tel que $M_1\underset{R}{\overset{*}{\to }}M$ et $M_2\underset{R}{\overset{*}{\to }}M$.

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-RosserModèle:,.

Ce théorème a été établi par Church et Rosser en 1936. 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).

Bibliographie

• Modèle:Ouvrage. Traduction anglaise : Modèle:Ouvrage.
• Modèle:Ouvrage.
• Modèle:Ouvrage.

Articles liés

• Complétion de Knuth-Bendix
• Lambda-calcul
• Système F
• Sémantique de Kripke

Liens externes

• Modèle:MathWorld