Satz von Church-Rosser
# 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 $\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

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