www.wikidata.de-de.nina.az

Satz von Church Rosser Das Church Rosser Theorem bewiesen im Jahr 1936 von Alonzo Church und John Barkley Rosser ist ein

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

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 .

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

Literatur Bearbeiten

  • 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 Bearbeiten

Einzelnachweise Bearbeiten

  1. F. Baader, T. Nipkow, S. 11.
wikipedia, wiki, deutsches, deutschland, buch, bücher, bibliothek artikel lesen, herunterladen kostenlos kostenloser herunterladen, MP3, Video, MP4, 3GP, JPG, JPEG, GIF, PNG, Bild, Musik, Lied, Film, Buch, Spiel, Spiele
Veröffentlichungsdatum:
Das Church Rosser Theorem bewiesen im Jahr 1936 von Alonzo Church und John Barkley Rosser ist ein wichtiges Resultat aus der Theorie des Lambda Kalkuls Eine Konsequenz dieses Theorems ist dass jeder Term des Lambda Kalkuls hochstens eine Normalform besitzt Das Church Rosser Theorem lasst Verallgemeinerungen auf abstrakte Reduktionssysteme zu Inhaltsverzeichnis 1 Die Aussage des Theorems 2 Formale Definitionen 3 Church Rosser Eigenschaft und Konfluenz 4 Literatur 5 Weblinks 6 EinzelnachweiseDie Aussage des Theorems BearbeitenDas Church Rosser Theorem besagt folgendes Wenn zwei unterschiedliche Terme a und b aquivalent sind d h mit Reduktionsschritten beliebiger Richtung ineinander transformiert werden konnen dann gibt es einen weiteren Term c zu dem sowohl a als auch b reduziert werden konnen Formale Definitionen BearbeitenSei displaystyle rightarrow nbsp die Reduktionsrelation im Lambda Kalkul d h die Relation die durch die a displaystyle alpha nbsp b displaystyle beta nbsp und h displaystyle eta nbsp Konversionen definiert wird Hierdurch wird der Lambda Kalkul zu einem Spezialfall eines Reduktionssystems speziell eines Termersetzungssystems displaystyle stackrel rightarrow nbsp ist die transitive Hulle von displaystyle rightarrow cup nbsp der Vereinigung der Relation displaystyle rightarrow nbsp mit der Identitatrelation d h displaystyle stackrel rightarrow nbsp ist die kleinste Quasiordnung reflexive und transitive Relation die displaystyle rightarrow nbsp enthalt Sie ist auch die reflexive und transitive Hulle von displaystyle rightarrow nbsp displaystyle leftrightarrow nbsp ist 1 displaystyle rightarrow cup rightarrow 1 nbsp d h die Vereinigung der Relation displaystyle rightarrow nbsp mit ihrer inversen Relation displaystyle leftrightarrow nbsp wird auch als symmetrische Hulle von displaystyle rightarrow nbsp bezeichnet displaystyle stackrel leftrightarrow nbsp ist die transitive Hulle von displaystyle leftrightarrow nbsp Das Church Rosser Theorem lasst sich dann wie folgt formulieren Theorem Church Rosser Seien a displaystyle a nbsp und b displaystyle b nbsp zwei Terme im Lambda Kalkul und a b displaystyle a stackrel leftrightarrow b nbsp dann existiert ein Term c displaystyle c nbsp mit a c displaystyle a xrightarrow c nbsp und b c displaystyle b xrightarrow c nbsp Church Rosser Eigenschaft und Konfluenz BearbeitenIn abstrakten Reduktionssystemen wird die Church Rosser Eigenschaft wie folgt definiert Definition Die Reduktionsrelation displaystyle rightarrow nbsp heisst Church Rosser oder besitzt die Church Rosser Eigenschaft wenn fur alle Terme a und b gilt Aus a b displaystyle a stackrel leftrightarrow b nbsp folgt dass ein Term c displaystyle c nbsp existiert mit a c displaystyle a xrightarrow c nbsp und b c displaystyle b xrightarrow c nbsp nbsp Von Bedeutung ist auch die folgende Definition der Konfluenz Definition s Bild rechts zur Illustration Ein Reduktionssystem heisst konfluent wenn es zu drei Termen a b und c mit a b a c displaystyle a xrightarrow b a xrightarrow c nbsp einen Term d gibt mit b d displaystyle b xrightarrow d nbsp und c d displaystyle c xrightarrow d nbsp Satz 1 In einem abstrakten Reduktionssystem ARS sind die folgenden Bedingungen aquivalent i Das System hat die Church Rosser Eigenschaft ii es ist konfluent Folgerung Wenn in einem konfluenten ARS x y displaystyle x stackrel leftrightarrow y nbsp gilt dann wenn x und y Normalformen sind dann gilt x y wenn y eine Normalform ist dann ist x y displaystyle x stackrel rightarrow y nbsp Literatur BearbeitenAlonzo 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 BearbeitenEric W Weisstein Church Rosser Theorem In MathWorld englisch Einzelnachweise Bearbeiten F Baader T Nipkow S 11 Abgerufen von https de wikipedia org w index php title Satz von Church Rosser amp oldid 194113588