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 R un système de réécriture, et notons \rightarrow_R la relation de réduction, \rightarrow_R^* sa clôture réflexive et 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 beta 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, vol. 39, Transactions of the American Mathematical Society,‎ , 472–482 p. (JSTOR 1989762), chap. 3.

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