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).

Notes et références

1. Krivine 1993, p. 18 et suivantes.
2. Rougemont et Lassaigne 1993, Chapitre 9.2 : « Réduction et forme normale », page 191.
3. (en) Alonzo Church et J. Barkley Rosser, « Some properties of conversion », Transactions of the American Mathematical Society, vol. 39, n^o 3,‎ mai 1936, p. 472–482 (JSTOR 1989762).

Bibliographie

• Jean-Louis Krivine, Lambda-calcul, types et modèles, Paris, Masson, 1990. Traduction anglaise : Lambda-calculus, types and models, Ellis Horwood, 1993 (lire en ligne).
• Michel de Rougemont et Richard Lassaigne, Logique et fondements de l'informatique : Logique du 1^er ordre, calculabilité et lambda-calcul, Paris, Hermès, 1993, viii-248 (ISBN 2-86601-496-0, zbMATH 0863.03004, SUDOC 003003825).
• Michel de Rougemont et Richard Lassaigne, Logic and complexity, Springer-Verlag, coll. « Discrete Mathematics and Theoretical Computer Science », 2003, 361 p. (ISBN 978-1-85233-565-6, zbMATH 1083.03001).

Articles liés

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

Liens externes

• (en) Eric W. Weisstein, « Church-Rosser-Theorem », sur MathWorld