imported>M2k~dewiki: BKL ersetzt mit bkl-replace

2026-04-23T13:32:41Z

Neue Seite

In der [[Mathematische Logik|Mathematischen Logik]] und der [[Theoretische Informatik|Theoretischen Informatik]] steht die Bezeichnung '''Reduktionssystem''', oder '''abstraktes Reduktionssystem''', abgekürzt '''ARS''', für eine Verallgemeinerung von [[Termersetzungssystem]]en. In seiner einfachsten Form ist ein ARS eine [[Menge (Mathematik)|Menge]] von Objekten zusammen mit einer [[Relation (Mathematik)#Eigenschaften zweistelliger Relationen|binären Relation]], die gewöhnlich mit <math>\rightarrow</math> bezeichnet wird. Trotz seiner Einfachheit genügt ein ARS zur Beschreibung wichtiger Eigenschaften von Termersetzungssystemen, wie z. B. ''[[Normalform]]en'', ''[[Terminiertheit]]'' und verschiedene Begriffe der ''[[Konfluenz (Informatik)|Konfluenz]]''.

Historisch hat es einige verschiedene Abstrahierungen der Termersetzung gegeben, jede mit ihren Besonderheiten. Die heute am meisten verwendete [[Formalisierung]], der hier gefolgt wird, beruht auf den Arbeiten von [[Gérard Huet]] (1980).<ref>Ronald V. Book, Friedrich Otto: ''String-rewriting Systems.'' S. 9.</ref>

== Definition ==
Ein ARS besteht aus einer Menge ''A'', den Objekten, zusammen mit einer binären Relation auf ''A'', üblicherweise mit <math>\rightarrow</math> bezeichnet. Diese Relation heißt ''Reduktionsrelation'' oder einfach ''Reduktion''.<ref>Ronald V. Book, Friedrich Otto: ''String-rewriting Systems.'' S. 10.</ref>

Als [[mathematisches Objekt]] ist ein ARS das gleiche wie ein unmarkiertes [[Transitionssystem]]. Dennoch unterscheiden sich Schwerpunkt und Terminologie in diesen beiden Bereichen: In einem Transitionssystem ist man daran interessiert, die Markierungen als Aktionen zu deuten, während in einem ARS der Fokus darauf liegt, wie Objekte in andere transformiert (reduziert) werden.<ref>Marc Bezem, J. W. Klop, Roel de Vrijer: ''Term rewriting systems.'' S. 7–8.</ref>

== Beispiel ==
Die Menge der Objekte sei ''T'' = {''a'', ''b'', ''c''} und die binäre Relation → sei wie folgt definiert: → <math>= \{(a,b),(b,a),(a,c),(b,c)\}</math>; das schreibt man üblicherweise als
<div style="text-align:center">''a'' → ''b'', ''b'' → ''a'', ''a'' → ''c'', ''b'' → ''c''.</div>
Liest man dies als Regeln, durch die Elemente in andere transformiert werden können, dann sieht man, dass sowohl ''a'' als auch ''b'' in ''c'' transformiert (reduziert) werden können. Dies ist offenbar eine wichtige Eigenschaft des Systems. ''c'' ist in gewisser Weise ein „einfachstes“ Objekt des Systems, da keine der Regeln auf ''c'' angewendet werden kann, um dieses Element weiter zu transformieren.

== Grundlegende Begriffe ==

Das obige Beispiel führt zu einigen wichtigen Begriffen im Rahmen eines ARS.<ref>Franz Baader, Tobias Nipkow: ''Term Rewriting and All That.'' S. 8–9.</ref>

* <math>\stackrel{*}{\rightarrow}</math> ist die [[Transitive Hülle (Relation)|transitive Hülle]] von <math>\rightarrow \cup =</math>, wobei = die [[Identität]] ist; d. h. <math>\stackrel{*}{\rightarrow}</math> ist die kleinste [[Quasiordnung]] ([[Reflexive Relation|reflexive]] und [[Transitive Relation|transitive]] Relation), die <math>\rightarrow</math> enthält. Sie ist auch die [[Reflexiv-transitive Hülle|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 [[Relation (Mathematik)#Umkehrrelation|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 \cup =</math>, d. h. <math>\stackrel{*}{\leftrightarrow}</math> ist die kleinste [[Äquivalenzrelation]], die <math>\rightarrow</math> enthält. Sie wird auch als ''reflexive transitive symmetrische Hülle'' von <math>\rightarrow</math> bezeichnet.

== Normalformen und das Wortproblem ==
Ein Objekt ''x'' in ''A'' heißt ''reduzibel'', wenn es ein von ''x'' verschiedenes Objekt ''y'' in ''A'' gibt mit <math>x \rightarrow y</math>; andernfalls heißt es ''irreduzibel'' oder eine ''Normalform''. Ein Objekt ''y'' heißt Normalform von ''x'', wenn <math>x \stackrel{*}{\rightarrow} y</math> gilt und ''y'' irreduzibel ist. Wenn ''x'' eine ''eindeutige'' Normalform besitzt, dann wird diese mit <math>x\downarrow</math> bezeichnet.

Im Beispiel oben ist ''c'' eine Normalform von ''a'' und von ''b''. Da ''a'' und ''b'' reduzibel sind, ist ''c'' sogar die einzige Normalform dieser Elemente, <math>c = a\downarrow = b\downarrow</math>. Wenn jedes Objekt mindestens eine Normalform besitzt, heißt das ARS ''normalisierend''.

Eines der wichtigen Probleme, das im Kontext eines ARS formuliert werden kann, ist das ''[[Wortproblem]]'': Gegeben ''x'' und ''y'', sind diese beiden Objekte äquivalent unter der Relation <math>\stackrel{*}{\leftrightarrow}</math>? Dies ist ein sehr allgemeiner Rahmen für das Wortproblem; so ist z. B. das Wortproblem für Gruppen ein Spezialfall des ARS-Wortproblems. Das Wortproblem ist einfacher zu behandeln, wenn es eindeutige Normalformen gibt: in diesem Fall gilt, dass zwei Objekte mit gleicher Normalform äquivalent unter <math>\stackrel{*}{\leftrightarrow}</math> sind. Das Wortproblem für ein ARS ist im Allgemeinen un[[entscheidbar]].

Für die Untersuchung der Frage, ob Normalformen existieren, sind die Begriffe der [[Church-Rosser-Theorem|Church-Rosser-Eigenschaft]] und der [[Konfluenz (Informatik)|Konfluenz]] von zentraler Bedeutung.<ref>Franz Baader, Tobias Nipkow: ''Term Rewriting and All That.'' S. 11 f.</ref>

== Quellen ==
* [[Franz Baader (Informatiker)|Franz Baader]], Tobias Nipkow: ''Term Rewriting and All That.'' Cambridge University Press, 1998. Für Anfänger geeignet.
* Nachum Dershowitz and Jean-Pierre Jouannaud [http://citeseer.ist.psu.edu/dershowitz90rewrite.html ''Rewrite Systems''], Chapter 6 in Jan van Leeuwen (Ed.), ''Handbook of Theoretical Computer Science.'' Band B: ''Formal Models and Semantics.'' Elsevier / MIT Press, 1990, ISBN 0-444-88074-7, S. 243–320.
* [[Ronald V. Book]], Friedrich Otto: ''String-rewriting Systems.'' Springer, Berlin 1993. Kapitel 1: ''Abstract reduction systems.'' ISBN 0-387-97965-4.
* Marc Bezem, J. W. Klop, Roel de Vrijer: ''Term rewriting systems.'' Cambridge University Press, 2003, ISBN 0-521-39115-6, Kapitel 1. (Dies ist eine umfangreiche Monografie).
* John Harrison: ''Handbook of Practical Logic and Automated Reasoning.'' Cambridge University Press, 2009, ISBN 978-0-521-89957-4, Kapitel 4: ''Equality.''
* Gérard Huet: ''Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems.'' In: [[Journal of the ACM]] (JACM), Band 27, Nr. 4, Oktober 1980, S. 797–821.

== Einzelnachweise ==
<references />

[[Kategorie:Logik]]
[[Kategorie:Theoretische Informatik]]
[[Kategorie:Normalform]]

Reduktionssystem - Versionsgeschichte

imported>M2k~dewiki: BKL ersetzt mit bkl-replace