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

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

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

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

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

Church-Rosser-Eigenschaft und Konfluenz

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

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

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

Satz.<ref>F. Baader, T. Nipkow, S. 11.</ref> 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 <math>x \stackrel{*}{\leftrightarrow} y</math> gilt, dann

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

Literatur

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.

Weblinks

{{#if: | {{{author}}} | Eric W. Weisstein }}: Church-Rosser Theorem. In: MathWorld (englisch). {{#if: Church-RosserTheorem | {{#ifeq: {{#property:P2812}} | Church-RosserTheorem | | {{#if: {{#property:P2812}} | {{#ifeq: 0 | 0 | }} | {{#ifeq: 0 | 0 | }} }} }} }}

Einzelnachweise