title: Propriété de Church-Rosser
text: # 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 $\rightarrow _{R}$ la relation de réduction, $\rightarrow _{R}^{*}$ sa clôture réflexive transitive, et enfin $\longleftrightarrow _{R}^{*}$ 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}\longleftrightarrow _{R}^{*}M_{2}$, il existe un terme $M$ tel que $M_{1}\rightarrow _{R}^{*}M$ et $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^,.$
  
  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).
  
  