Propriété de Church-Rosser

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.

Définition[modifier | modifier le code]

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[modifier | modifier le code]

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[modifier | modifier le code]

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[modifier | modifier le code]

↑ Krivine 1993, p. 18 et suivantes.
↑ Rougemont et Lassaigne 1993, Chapitre 9.2 : « Réduction et forme normale », page 191.
↑ (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[modifier | modifier le code]

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[modifier | modifier le code]

Liens externes[modifier | modifier le code]

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

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

[1]

[2]

[3]