Propriété de Church-Rosser

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.

Pour les articles homonymes, voir Rosser (homonymie).

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

  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

  • 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

Liens externes

  • Portail de l'informatique théorique
  • Portail de la logique
  • Portail des mathématiques
Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.