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]

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 \rightarrow die Reduktionsrelation im Lambda-Kalkül; d.h. die Relation, die durch die \alpha–,\beta– und \eta− Konversionen definiert wird. Hierdurch wird der Lambda-Kalkül zu einem Spezialfall eines Reduktionssystems; speziell eines Termersetzungssystems.

\stackrel{*}{\rightarrow} ist die transitive Hülle von \rightarrow \cup = (der Vereinigung der Relation \rightarrow mit der Identitätrelation), d.h. \stackrel{*}{\rightarrow} ist die kleinste Quasiordnung (reflexive und transitive Relation), die \rightarrow enthält. Sie ist auch die reflexive und transitive Hülle von \rightarrow .

\leftrightarrow ist \rightarrow \cup \rightarrow^{-1}, d.h. die Vereinigung der Relation \rightarrow mit ihrer inversen Relation; \leftrightarrow wird auch als symmetrische Hülle von \rightarrow bezeichnet. \stackrel{*}{\leftrightarrow} ist die transitive Hülle von \leftrightarrow.

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

Theorem (Church-Rosser): Seien a und b zwei Terme im Lambda-Kalkül und 
a \stackrel{*}{\leftrightarrow} b 
, dann existiert ein Term c mit 
a \xrightarrow{*} c
und 
b \xrightarrow{*} c
.

Church-Rosser-Eigenschaft und Konfluenz[Bearbeiten]

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

Definition: Die Reduktionsrelation \rightarrow heißt "Church-Rosser" (oder: besitzt die Church-Rosser-Eigenschaft), wenn für alle Terme a und b gilt: Aus 
a \stackrel{*}{\leftrightarrow} b 
, folgt, dass ein Term c existiert mit 
a \xrightarrow{*} c
und 
b \xrightarrow{*} c
.

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 
a \xrightarrow{*} b , a\xrightarrow{*} c
einen Term d gibt mit 
b \xrightarrow{*} d
und 
c \xrightarrow{*} d
.

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 x \stackrel{*}{\leftrightarrow} y gilt, dann

  • wenn x und y Normalformen sind, dann gilt x = y,
  • wenn y eine Normalform ist, dann ist x \stackrel{*}{\rightarrow} y.

Bemerkungen[Bearbeiten]

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

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