Satz von Church-Rosser

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

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 | Quelltext 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 | Quelltext 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 | Quelltext 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 .

Confluence.png

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 .

Bemerkungen[Bearbeiten | Quelltext bearbeiten]

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

Literatur[Bearbeiten | Quelltext bearbeiten]

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

Weblinks[Bearbeiten | Quelltext bearbeiten]