Propriété de Church-Rosser
![Page d’aide sur l’homonymie](http://upload.wikimedia.org/wikipedia/commons/thumb/a/a9/Logo_disambig.svg/20px-Logo_disambig.svg.png)
Pour les articles homonymes, voir Rosser (homonymie).
![](http://upload.wikimedia.org/wikipedia/commons/thumb/0/02/Circle-icons-computer.svg/35px-Circle-icons-computer.svg.png)
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
Soit un système de réécriture, et notons la relation de réduction, sa clôture réflexive transitive, et enfin sa clôture réflexive, transitive et symétrique.
On dit que a la propriété de Church-Rosser si, pour toute paire de termes tels que , il existe un terme tel que et .
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
- ↑ 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, no 3, , p. 472–482 (JSTOR 1989762).
Bibliographie
- Jean-Louis Krivine, Lambda-calcul, types et modèles, Paris, Masson, . Traduction anglaise : Lambda-calculus, types and models, Ellis Horwood, (lire en ligne).
- Michel de Rougemont et Richard Lassaigne, Logique et fondements de l'informatique : Logique du 1er ordre, calculabilité et lambda-calcul, Paris, Hermès, , 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 », , 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
Portail de l'informatique théorique
Portail de la logique
Portail des mathématiques