Propriété de Church-Rosser

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

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 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[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]

  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, no 3,‎ , p. 472–482 (JSTOR 1989762).

Bibliographie[modifier | modifier le code]

  • 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 p. (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 », (ISBN 978-1852335656, zbMATH 1083.03001).

Articles liés[modifier | modifier le code]

Liens externes[modifier | modifier le code]