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 ${\displaystyle R}$ un système de réécriture, et notons ${\displaystyle \rightarrow _{R}}$ la relation de réduction, ${\displaystyle \rightarrow _{R}^{*}}$ sa clôture réflexive transitive, et enfin ${\displaystyle \longleftrightarrow _{R}^{*}}$ sa clôture réflexive, transitive et symétrique.

On dit que ${\displaystyle R}$ a la propriété de Church-Rosser si, pour toute paire de termes ${\displaystyle M_{1},M_{2}}$ tels que ${\displaystyle M_{1}\longleftrightarrow _{R}^{*}M_{2}}$, il existe un terme ${\displaystyle M}$ tel que ${\displaystyle M_{1}\rightarrow _{R}^{*}M}$ et ${\displaystyle M_{2}\rightarrow _{R}^{*}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-Rosser^[1],[2].

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