Propriété de Church-Rosser

Pour les articles homonymes, voir Rosser (homonymie).

Cet article est une ébauche concernant l’informatique.

Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.

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.

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}$.

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.

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

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

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

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

• Portail de l'informatique théorique
• Portail de la logique
• Portail des mathématiques