Satz von Church-Rosser

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

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

Sei $\rightarrow$ 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.

$\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

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

Definition: Die Reduktionsrelations $\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$.

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

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

Literatur

• 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

• Eric W. Weisstein: Church-Rosser-Theorem. In: MathWorld. (englisch)