Quelltext der Seite Strukturelle Induktion

Die '''strukturelle Induktion''' ist ein [[Beweis (Logik)|Beweisverfahren]], das unter anderem in der [[Logik]], der [[Theoretische Informatik|theoretischen Informatik]] und der [[Graphentheorie]] eingesetzt wird. Es handelt sich um eine allgemeinere Form der [[vollständige Induktion|vollständigen Induktion]].
Mit dem Verfahren lassen sich Aussagen über die Elemente von [[rekursiv]] aufgebauten [[Menge (Mathematik)|Mengen]] (zum Beispiel Mengen von [[Liste]]n, [[Formel]]n, [[Graph (Graphentheorie)|Graphen]]) beweisen.

Bei der vollständigen Induktion werden Eigenschaften der natürlichen Zahlen bewiesen; bei der strukturellen Induktion werden Eigenschaften für Mengen bewiesen, deren Elemente aus Grundelementen durch eine endliche Anzahl von Konstruktionsschritten (unter Verwendung bereits konstruierter Elemente) bzw. mittels eines [[Erzeugungssystem]]s entstehen.
Es gibt also minimale (auch: einfachste oder Grund-)Elemente und rekursiv definierte (oder: rekursiv gebildete) Elemente der Menge.
Bei den natürlichen Zahlen ist das Grundelement <math>0</math> (oder <math>1</math>, je nach Definition der natürlichen Zahlen) und der Konstruktionsschritt ist der Übergang von einer Zahl <math>n</math> zur Zahl <math>n+1</math>.

Um eine Aussage für die Elemente einer Menge zu beweisen, zeigt man im Induktionsanfang die Gültigkeit der Aussage für die einfachsten Elemente und im Induktionsschluss die Gültigkeit der Aussage für die rekursiv gebildeten Elemente unter der Voraussetzung, dass die Aussage für die in der Konstruktion verwendeten Elemente gilt.
Ist beides erfüllt, so gilt die Aussage für alle Elemente. Man führt die Induktion also über den strukturellen Aufbau der Elemente.

Strukturelle Induktion ist ein Spezialfall der Induktion für Mengen mit einer [[wohlfundierte Relation|wohlfundierten Relation]].

== Beispiel für eine Definition durch strukturelle Rekursion ==

Die Menge der [[Aussagenlogik|aussagenlogischen]] Formeln lässt sich mittels struktureller Rekursion wie folgt definieren:
:Rekursionsanfang: Falls <math>A\!\,</math> eine atomare aussagenlogische Formel ist, ist <math>A\!\,</math> eine aussagenlogische Formel.
:Rekursionsschritt 1: Falls <math>F\!\,</math> eine aussagenlogische Formel ist, ist auch <math>\lnot F</math> eine aussagenlogische Formel.
:Rekursionsschritt 2: Falls <math>F\!\,</math> und <math>G\!\,</math> aussagenlogische Formeln sind, ist auch <math>(F \land G)</math> eine aussagenlogische Formel.
:Rekursionsschritt 3: Falls <math>F\!\,</math> und <math>G\!\,</math> aussagenlogische Formeln sind, ist auch <math>(F \lor G)</math> eine aussagenlogische Formel.
:Rekursionsschritt 4: Falls <math>F\!\,</math> und <math>G\!\,</math> aussagenlogische Formeln sind, ist auch <math>\!\,(F \to G)</math> eine aussagenlogische Formel.
:Rekursionsschritt 5: Falls <math>F\!\,</math> und <math>G\!\,</math> aussagenlogische Formeln sind, ist auch <math>(F \leftrightarrow G)</math> eine aussagenlogische Formel.

Nach dieser Definition sind z.&nbsp;B. die folgenden Zeichenketten aussagenlogische Formeln:
* <math>\lnot (A \land B)</math>
* <math>(A \to (B \lor \lnot C))</math>
* <math>((A \lor \lnot B) \land (\lnot A \lor B))</math>

Weitere Beispiele für Definitionen durch strukturelle Rekursion finden sich in den Artikeln [[Elementare Sprache]] und [[Wort (Theoretische Informatik)]] (Definition der Spiegelung).

== Beispiel für einen Beweis durch strukturelle Induktion ==

Bewiesen wird der Satz:
:Für jede [[Aussagenlogik|aussagenlogische]] Formel <math>F</math> gibt es eine äquivalente aussagenlogische Formel <math>[F]</math>, in der als einzige Operatoren <math>\lnot</math> und <math>\land</math> vorkommen.

Der Beweis:
:Induktionsanfang: Falls <math>F=A</math> für eine atomare aussagenlogische Formel <math>A</math> ist, ist <math>[F]=A</math>.
:Induktionsschritt 1: Falls <math>F=\lnot G</math> für eine aussagenlogische Formel <math>G</math> gilt, ist <math>[F]=\lnot [G]</math>.
:Induktionsschritt 2: Falls <math>F=(G \land H)</math> für aussagenlogische Formeln <math>G</math> und <math>H</math> gilt, ist <math>[F]=([G] \land [H])</math>.
:Induktionsschritt 3: Falls <math>F=(G \lor H)</math> für aussagenlogische Formeln <math>G</math> und <math>H</math> gilt, ist <math>[F]= \lnot (\lnot [G] \land \lnot [H])</math>.
:Induktionsschritt 4: Falls <math>F=(G \to H)</math> für aussagenlogische Formeln <math>G</math> und <math>H</math> gilt, ist <math>[F]= \lnot ([G] \land \lnot [H])</math>.
:Induktionsschritt 5: Falls <math>F=(G \leftrightarrow H)</math> für aussagenlogische Formeln <math>G</math> und <math>H</math> gilt, ist <math>[F]= \lnot (\lnot ([G] \land [H]) \land \lnot (\lnot [G] \land \lnot [H]))</math>.

Das Gleichheitszeichen steht hier für syntaktische Gleichheit, d.&nbsp;h. Gleichheit Zeichen für Zeichen.
In jedem Induktionsschritt wird vorausgesetzt, dass für <math>G</math> und <math>H</math> jeweils
die äquivalenten Formeln <math>[G]</math> und <math>[H]</math> existieren, die nur <math>\lnot</math>
und <math>\land</math> verwenden (Induktionsvoraussetzung).

In einer konkreten Konstruktion kann man die Beweisschritte auch in der
umgekehrten Reihenfolge, also „von außen nach innen“, anwenden.
Für die mittlere der oben angegebenen aussagenlogischen Formeln gelten z.&nbsp;B.
die folgenden Äquivalenzen:
:<math>\begin{align}
  (A \to (B \lor \lnot C))
  & \equiv [(A \to (B \lor \lnot C))] \\
  & \stackrel{\mbox{IS 4}}{=} \lnot ([A] \land \lnot [(B \lor \lnot C)]) \\
  & \stackrel{\mbox{IS 3}}{=} \lnot ([A] \land \lnot \lnot (\lnot [B] \land \lnot [\lnot C])) \\
  & \stackrel{\mbox{IS 1}}{=} \lnot ([A] \land \lnot \lnot (\lnot [B] \land \lnot \lnot [C])) \\
  & \stackrel{3\times\mbox{IA}}{=} \lnot (A \land \lnot \lnot (\lnot B \land \lnot \lnot C))\end{align}</math>
Die Anwendungen des Induktionsschritts&nbsp;1 und des Induktionsanfangs
sind hier leer, d.&nbsp;h., sie verändern den Term nicht.
(Bei der ersten oben angegebenen Formel wären alle Induktionsschritte
und der Induktionsanfang leer.)
Dass sich die letzte Formel noch zu <math>\lnot (A \land (\lnot B \land C))</math> vereinfachen lässt, ist hier übrigens unerheblich.

== Literatur ==
* Hartmut Ehrig, Bernd Mahr, F. Cornelius, Martin Große-Rhode, P. Zeitz: ''Mathematisch-strukturelle Grundlagen der Informatik''. Springer, 2013, S. 162–168

== Weblinks ==
* François Bry: [https://www.en.pms.ifi.lmu.de/publications/projektarbeiten/Claudia.Plant_Alije.Ristemi/node6.html ''Satz 2.1.4 (strukturelle Induktion)'']. Skript, LMU
* Christoph Walter: [https://www.inferenzsysteme.informatik.tu-darmstadt.de/media/is/pm_fgdi3/material/vorlesung/fgdi3_ws-0910_kapitel-7-v2_09-12-10_4auf1.pdf ''Strukturelle Induktion und Induktion nach Rekursion von Prozeduren'']. Skript, Uni Darmstadt

[[Kategorie:Theoretische Informatik]]
[[Kategorie:Mathematische Logik]]
[[Kategorie:Graphentheorie]]