Satz von Church-Rosser

mathematischer Satz
(Weitergeleitet von Church-Rosser-Theorem)

Das Church-Rosser-Theorem (bewiesen im Jahr 1936 von Alonzo Church und John Barkley Rosser) ist ein wichtiges Resultat aus der Theorie des Lambda-Kalküls. Eine Konsequenz dieses Theorems ist, dass jeder Term des Lambda-Kalküls höchstens eine Normalform besitzt. Das Church-Rosser-Theorem lässt Verallgemeinerungen auf abstrakte Reduktionssysteme zu.

Die Aussage des Theorems

Bearbeiten

Das Church-Rosser-Theorem besagt folgendes: Wenn zwei unterschiedliche Terme a und b äquivalent sind, d. h. mit Reduktionsschritten beliebiger Richtung ineinander transformiert werden können, dann gibt es einen weiteren Term c, zu dem sowohl a als auch b reduziert werden können.

Formale Definitionen

Bearbeiten

Sei   die Reduktionsrelation im Lambda-Kalkül; d. h. die Relation, die durch die  –, – und  − Konversionen definiert wird. Hierdurch wird der Lambda-Kalkül zu einem Spezialfall eines Reduktionssystems; speziell eines Termersetzungssystems.

  ist die transitive Hülle von   (der Vereinigung der Relation   mit der Identitätrelation), d. h.   ist die kleinste Quasiordnung (reflexive und transitive Relation), die   enthält. Sie ist auch die reflexive und transitive Hülle von  .

  ist  , d. h. die Vereinigung der Relation   mit ihrer inversen Relation;   wird auch als symmetrische Hülle von   bezeichnet.   ist die transitive Hülle von  .

Das Church-Rosser-Theorem lässt sich dann wie folgt formulieren:

Theorem (Church-Rosser): Seien   und   zwei Terme im Lambda-Kalkül und  , dann existiert ein Term   mit   und  .

Church-Rosser-Eigenschaft und Konfluenz

Bearbeiten

In abstrakten Reduktionssystemen wird die Church-Rosser-Eigenschaft wie folgt definiert:

Definition: Die Reduktionsrelation   heißt „Church-Rosser“ (oder „besitzt die Church-Rosser-Eigenschaft“), wenn für alle Terme a und b gilt: Aus  , folgt, dass ein Term   existiert mit   und  .

 

Von Bedeutung ist auch die folgende Definition der Konfluenz:

Definition (s. Bild rechts zur Illustration): Ein Reduktionssystem heißt konfluent, wenn es zu drei Termen a, b und c mit   einen Term d gibt mit   und  .

Satz.[1] In einem abstrakten Reduktionssystem (ARS) sind die folgenden Bedingungen äquivalent: (i) Das System hat die Church-Rosser-Eigenschaft, (ii) es ist konfluent.

Folgerung. Wenn in einem konfluenten ARS   gilt, dann

  • wenn x und y Normalformen sind, dann gilt x = y,
  • wenn y eine Normalform ist, dann ist  .

Literatur

Bearbeiten
  • Alonzo Church, J. Barkley Rosser: Some properties of conversion. In: Transactions of the American Mathematical Society. Band 39, Nr. 3, Mai 1936, S. 472–482.
  • Franz Baader, Tobias Nipkow: Term Rewriting and All That. Cambridge University Press 1999, ISBN 0-521-77920-0, S. 9–11.
Bearbeiten

Einzelnachweise

Bearbeiten
  1. F. Baader, T. Nipkow, S. 11.