Propriété de Church-Rosser
# 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).

