i1indu.tex

% Diese Datei ist Teil des Buchs "Schreibe Dein Programm!"
% Das Buch ist lizensiert unter der Creative-Commons-Lizenz
% "Namensnennung - Weitergabe unter gleichen Bedingungen 4.0 International (CC BY-SA 4.0)"
% https://creativecommons.org/licenses/by-sa/4.0/deed.de

\chapter{Exkurs: Induktive Beweise und Definitionen}
\label{cha:indu}

In den vergangenen Kapiteln haben wir uns oft mit Selbstbezügen in
Datendefinitionen beschäftigt und den rekursiven Funktionen, die sie
akzeptieren.  Dieses Kapitel beschäftigt sich mit der mathematischen
Seite solcher Funktionen.  Es ist für Dich als Lektüre sinnvoll, wenn
Du Dich besonders für Mathematik interessierst oder studiumshalber
dafür interessieren musst.  Für das Verständnis der folgenden Kapitel
kannst Du es aber auch weglassen.

Die Mathematik bildet Daten mit Selbstbezug als sogenannte
\textit{induktiv definierte} Mengen ab.  Dies ermöglicht uns, dass wir
uns von der Korrektheit einer Funktion mit Hilfe eines sogenannten
induktiven Beweises überzeugen.  Dieses Kapitel zeigt, was das ist und
wie das geht.

\section{Aussagen über natürliche Zahlen}
\label{sec:mathematical-induction}
\label{sec:gausssche-summenformel}

In der Mathematik gibt es viele kuriose Aussagen über natürliche
Zahlen.  Legendenstatus hat z.B.\ die Gaußsche
Summenformel\index{Gaußsche Summenformel}.  Diese besagt, dass für
eine natürliche Zahl $n$ die Summer aller Zahlen von 1 bis $n$ mit der
Formel
\[\frac{n\times (n+1)}{2}\]
berechnet werden kann: Man muss also gar nicht mühsam die Zahlen
einzeln addieren.  Mathematiker lieben spezielle Schreibweisen und
könnten Gauß' Behauptung folgendermaßen aufschreiben:
%
\[\forall n\in\mathbb{N}: \sum_{i=0}^n i =
  \frac{n\times (n+1)}{2}\]
%
Das $\forall$ heißt "<für alle">, das $\in$ heißt "<Element von">
$\mathbb{N}$ ist das Kürzel für die Menge der natürlichen Zahlen.
Am Anfang steht also "<für alle $n$, die Element von $\mathbb{N}$
sind"> oder ganz lapidar "<für alle natürlichen Zahlen $n$">.

Das $\sum$ ist ein griechisches Sigma und steht für "<Summe">.  Das
$i=0$ untendrunter und das $n$ obendrüber bedeuten, dass eine neue
Variable $i$ eingeführt wird, und die nacheinander die Werte $0, 1, 2,
\ldots n$ annimmt, und für jeden Wert in die Formel rechts vom $\sum$
eingesetzt wird.  In der Gaußschen Summenformel steht rechts nur 
$i$, das heißt die Summe ist $0 + 1 + 2 + \cdot \ + n$.

Wie können wir die Gaußsche Summenformel beweisen?  Gauß' Argument war, dass,
wenn er die Summe ausschreibt (wir lassen die $0$ weg):
%
\[ 1+2+\ldots+(n-1) + n \]
%
\ldots~die beiden "<äußeren"> Summanden $1$ und $n$ zusammen $n+1$
ergeben, die beiden "<nächstinneren"> Summanden $2$ und $n-1$
ebenfalls $n+1$ undsoweiter bis zur "<Mitte">~-- effektiv also halb so
oft $n+1$ auf sich selbst addiert wird wie die Reihe selbst lang ist.
Es ist also einfach nachzuvollziehen, wie Gauß auf die Formel kam und
warum sie korrekt ist.

Was ist aber mit folgender Reihe?
%
\[ \sum_{i=0}^n i^2 \]
%
Der Blick auf die ausgeschriebene Form hilft nicht direkt weiter:
%
\[ 1+4+9+16+\ldots+(n-1)^2+n^2 \]
%
Allerdings lohnt es sich, einen Blick auf die ersten paar Glieder der
Reihe zu werfen, und diese tabellarisch über die Gaußsche Summen zu
setzen:
%
\begin{displaymath}
  \begin{array}{crrrrrrrr}
    n & 0 & 1 & 2 & 3 & 4 & 5 & 6 & \ldots\\\hline
    \sum_{i=0}^n i^2 & 0 & 1 & 5 & 14 & 30 & 55 & 91 & \ldots\\
    \sum_{i=0}^n i   & 0 & 1 & 3 & 6 & 10 & 15 & 21 & \ldots\\
  \end{array}
\end{displaymath}
%
Wenn Du die Paare der Summen der beiden Reihen lang genug anstarrt, siehst
Du vielleicht, dass sich alle als Brüche auf den Nenner $3$ kürzen lassen:
%
\begin{displaymath}
  \begin{array}{crrrrrrrr}
    n & 0 & 1 & 2 & 3 & 4 & 5 & 6 & \ldots\\\hline
    \dfrac{\sum_{i=0}^n i^2}{\sum_{i=0}^n i} & \dfrac{?}{3} & \dfrac{3}{3} &
    \dfrac{5}{3} & \dfrac{7}{3} & \dfrac{9}{3} & \dfrac{11}{3} & \dfrac{13}{3} & \ldots
  \end{array}
\end{displaymath}
%
Einzige Ausnahme ist der Bruch für $0$: dort wird durch $0$ geteilt, es
ist also unklar, welcher Bruch an dieser Stelle in der Tabelle stehen
sollte.  Ansonsten suggeriert die Tabelle folgende Formel:
%
\begin{displaymath}
  \dfrac{\sum_{i=0}^n i^2}{\sum_{i=0}^n i} = \dfrac{2n+1}{3}
\end{displaymath}
%
Die Gleichung kann mit $\sum_{i=0}^n i = n(n+1)/2$ multipliziert werden, um eine
Antwort für die ursprüngliche Frage zu ergeben:
%
\begin{equation}
  \sum_{i=0}^n i^2 = \dfrac{n(n+1)(2n+1)}{6}
  \label{eq:squares-induction-prequel}
\end{equation}
%
Schöne Formel~-- aber stimmt sie auch für alle $n\in\mathbb{N}$?  (Für
den unklaren Fall $0$ stimmt sie.)  Falls Du
magst, kannst Du sie noch für weitere $n$, zum Beispiel $7, 8, \ldots$~-- ausprobieren,
und tatsächlich zeigen sich zunächst keine Gegenbeispiele.  Aber das
ist langweilig und würde immer noch nicht reichen, um die Behauptung
für \emph{alle} $n\in\mathbb{N}$ zu beweisen.

Wenn die Behauptung für alle $n\in\mathbb{N}$ stimmt, also
insbesondere auch für ein bestimmtes $n\in\mathbb{N}$, dann sollte sie
auch für $n+1$ gelten, das wäre dann die folgende Gleichung, bei der
gegenüber der Gleichung oben für $n$ jeweils $n+1$ eingesetzt wurde:
%
\begin{displaymath}
  \sum_{i=0}^{n+1} i^2 = \dfrac{(n+1)((n+1)+1)(2(n+1)+1)}{6}
\end{displaymath}
%
Das können wir etwas vereinfachen:
%
\begin{equation}
  \sum_{i=0}^{n+1} i^2 = \dfrac{(n+1)(n+2)(2n+3)}{6}
  \label{eq:squares-induction-consequence}
\end{equation}
%
Bei der Reihe $\sum_{i=0}^{n+1} i^2$ können wir den letzen Summand
ausgliedern und die Gleichung damit folgendermaßen schreiben:
%
\[(\sum_{i=0}^{n}
i^2) + (n+1)^2 = \dfrac{(n+1)(n+2)(2n+3)}{6}\]
%
Damit bietet sich die Chance, die jeweiligen Seiten von
Gleichung~\ref{eq:squares-induction-prequel} von den Seiten von
Gleichung~\ref{eq:squares-induction-consequence} abzuziehen:
%
\[(\sum_{i=0}^{n}
i^2) + (n+1)^2 - \sum_{i=0}^n i^2 = \dfrac{(n+1)(n+2)(2n+3)}{6} - \dfrac{n(n+1)(2n+1)}{6}\]
%
Es bleibt:
\[ (n+1)^2 = \dfrac{(n+1)(n+2)(2n+3)}{6} - \dfrac{n(n+1)(2n+1)}{6}\]
%
Wenn diese Gleichung stimmt, dann stimmt auch
Gleichung~\ref{eq:squares-induction-consequence}.  Das lässt sich
ausrechnen:
%
\begin{displaymath}
\begin{split}
\dfrac{(n+1)(n+2)(2n+3)}{6} - \dfrac{n(n+1)(2n+1)}{6} &=
\dfrac{(n+1)(n+2)(2n+3) - n(n+1)(2n+1)}{6}\\
&= \dfrac{(n+1)(\left(n+2)(2n+3)-n(2n+1)\right)}{6}\\
&= \dfrac{(n+1)(2n^2+3n+4n+6-2n^2-n)}{6}\\
&= \dfrac{(n+1)(6n+6)}{6}\\
&= \dfrac{6(n+1)^2}{6}\\
&= (n+1)^2
\end{split}
\end{displaymath}
%
Tatsache!  Aber was wurde jetzt eigentlich gezeigt?  Es ist leicht,
bei den vielen Schritten von oben den Faden zu verlieren.  Hier noch
einmal die Zusammenfassung:

Es \emph{schien} so, als ob folgende Gleichung stimmen würde:
%
\begin{displaymath}
  \sum_{i=0}^n i^2 = \dfrac{n(n+1)(2n+1)}{6}
\end{displaymath}
%
Es \emph{ist} so, dass folgende Gleichung stimmt:
%
\[ (n+1)^2 = \dfrac{(n+1)(n+2)(2n+3)}{6} - \dfrac{n(n+1)(2n+1)}{6}\]
%
Wenn also die Gleichung, die so scheint, stimmen würde, dann folgte
daraus diese Gleichung:
%
\begin{displaymath}
  \sum_{i=0}^{n+1} i^2 = \dfrac{(n+1)(n+2)(2n+3)}{6}
\end{displaymath}
%
Das ist aber die gleiche Behauptung, nur für $n+1$ statt $n$~-- mit
anderen Worten folgt aus der Behauptung für $n$ die Behauptung für
$n+1$.  Da wir oben durch Ausrechnen bereits gezeigt haben, dass die
Behauptung für $1,\ldots,6$ gilt, gilt sie auch für $7$.  Da sie für
$7$ gilt, gilt sie auch für $8$.  Undsoweiter für alle natürlichen
Zahlen.  Wir müssen das nicht für jede Zahl einzeln auszuprobieren.  Die Vermutung
von oben ist deshalb bewiesen.

\section{Induktive Beweise führen}
\label{sec:nat-induction-ka}
\label{page:mathematical-induction}
Das im vorigen Abschnitt verwendete Beweisprinzip für Beweise 
von Sätzen der Form "<für alle $n\in\enn$ \ldots">
heißt
\textit{vollständige Induktion}\index{Induktion}\index{Induktion!vollständig}.\footnote{Nicht zu
verwechseln mit der \textit{philosophischen Induktion}.  Die
vollständige Induktion ist zwar verwandt, philosophisch gesehen aber
eher eine deduktive Technik.}  Diese
funktioniert bei Aufgaben, bei denen eine Behauptung für alle
$n\in\mathbb{N}$ zu beweisen ist.  Für den Beweis werden folgende
Zutaten benötigt:
%
\begin{enumerate}
\item ein Beweis dafür, dass die Behauptung für $n=0$ stimmt und
\item ein Beweis dafür, dass, wenn die Behauptung für ein beliebiges
  $n$ gilt, sie auch für $n+1$ gilt.
\end{enumerate}
%
Die erste Zutat (der
\textit{Induktionsanfang}\index{Induktionsanfang}) lässt sich meist
durch Einsetzen beweisen, für die zweite Zutat (den
\textit{Induktionsschluss}\index{Induktionsschluss}) ist in der Regel Algebra
nötig.  Da die Behauptung nach Zutat Nr.~1 für $0$ gilt, muss sie nach
Zutat Nr.~2 auch für $1$ gelten, und deshalb auch für $2,\ldots$ und
damit für alle natürlichen Zahlen.  (Es muss nicht unbedingt bei $0$
losgehen, sondern kann auch bei einer beliebigen Zahl $a$ losgehen~--
dann gilt aber die Behauptung nur für alle natürlichen Zahlen ab $a$.)

Wenn die Behauptung erst einmal formuliert ist, sind induktive Beweise
oft einfach zu führen, da sie meist dem obigen Schema folgen.  Das
wichtigste dabei ist, das Schema auch tatsächlich einzuhalten.  Darum
empfiehlt es sich, dass Du folgende Anleitung befolgst~-- eine Art
Konstruktionsanleitung für Beweise mit vollständiger Induktion:
%
\begin{enumerate}
\item Formuliere die zu beweisende Behauptung als Behauptung der
  Form "<Für alle $n\in\mathbb{N}$ gilt~\ldots">, falls das noch nicht
  geschehen ist.
\item Schreibe die Überschrift "<$n = 0$:">. Schreibe die
  Behauptung noch einmal ab, wobei Du das "<für alle $n\in\mathbb{N}$"> weglassen und für $n$ die $0$ einsetzt.
\item Beweise die abgeschriebene Behauptung.  (Das ist oft
  einfach.)
\item Schreibe das Wort "<Induktionsvoraussetzung:"> Schreibe
  darunter die Behauptung noch einmal ab, wobei Du das "<für
  alle $n\in\mathbb{N}$"> weglässt~-- lass das $n$ da, wo es ist.
\item Schreibe "<Induktionsschluss (zu zeigen):">.
  Schreibe darunter die Behauptung noch einmal ab, wobei Du für
  $n$ stattdessen $(n+1)$ einsetzt.  (Das "<für alle
  $n\in\mathbb{N}$"> wieder weg.)
\item Beweise den Induktionsschluss unter Verwendung der
  Induktionsvoraussetzung.  

  Wenn die Behauptung eine Gleichung der Form $A = B$ ist, kannst
  Du häufig die Induktionsvoraussetzung entweder direkt oder nach
  einigen Umformungen in den Induktionsschluss einsetzen.
\end{enumerate}
%
Wir gehen die Anleitung anhand des obigen Beispiels durch.  Die
Behauptung ist:
%
\begin{displaymath}
  \sum_{i=0}^n i^2 = \dfrac{n(n+1)(2n+1)}{6}
\end{displaymath}
%
Die Behauptung ist durch Raten entstanden~-- es gibt leider keine
Patentanleitung, solche Gleichungen zu finden: Hier sind
Experimentierfreude und Geduld gefragt.  Steht die Behauptung erst
einmal fest, ist sie allerdings recht einfach zu beweisen:
%
\begin{enumerate}
\item Ausgeschrieben hat die Behauptung bereits die richtige Form:
\begin{displaymath}
  \forall n\in\mathbb{N}: \sum_{i=0}^n i^2 = \dfrac{n(n+1)(2n+1)}{6}
\end{displaymath}
\item $n=0$:
\begin{displaymath}
  \sum_{i=0}^0 i^2 = \dfrac{0(0+1)(2\cdot 0+1)}{6}
\end{displaymath}
\item Beide Seiten der Gleichung sind $0$, sie ist also bewiesen.
\item Induktionsvoraussetzung:
%
\begin{displaymath}
  \sum_{i=0}^n i^2 = \dfrac{n(n+1)(2n+1)}{6}
\end{displaymath}
\item Induktionsschluss (zu zeigen):
\begin{displaymath}
  \sum_{i=0}^{n+1} i^2 = \dfrac{(n+1)((n+1)+1)(2(n+1)+1)}{6}
\end{displaymath}
\item Die Summe auf der linken Seite können wir aufteilen:
%
\begin{displaymath}
  (\sum_{i=0}^{n} i^2) + (n+1)^2  = \dfrac{(n+1)((n+1)+1)(2(n+1)+1)}{6}
\end{displaymath}
%
Damit können wir die Induktionsvoraussetzung einsetzen, in der
$\sum_{i=0}^{n} i^2$ auf der linken Seite steht~-- dieser Kniff
funktioniert fast immer bei Induktionsbeweisen für Gleichungen über
Summen oder Produkte.  Es entsteht folgende Gleichung:
%
\begin{displaymath}
  (\dfrac{n(n+1)(2n+1)}{6}) + (n+1)^2  =
  \dfrac{(n+1)((n+1)+1)(2(n+1)+1)}{6}
\end{displaymath}
%
Die linke Seite können wir folgendermaßen vereinfachen:
%
\begin{displaymath}
\begin{split}
  \dfrac{n(n+1)(2n+1)}{6} + (n+1)^2  &=
  \dfrac{n(n+1)(2n+1) + 6(n+1)^2}{6} \\ &=
  \dfrac{(n+1)(n(2n+1) + 6(n+1))}{6} \\ &=
  \dfrac{(n+1)(2n^2+n + 6n+6)}{6} \\ &=
  \dfrac{(n+1)(2n^2+  7n+6)}{6}
\end{split}
\end{displaymath}
%
Die rechte Seite können wir folgendermaßen vereinfachen:
%
\begin{displaymath}
  \begin{split}
  \dfrac{(n+1)((n+1)+1)(2(n+1)+1)}{6} &=
  \dfrac{(n+1)(n+2)(2(n+1)+1)}{6} \\ &=
  \dfrac{(n+1)(n+2)(2n+2+1)}{6} \\ &=
  \dfrac{(n+1)(n+2)(2n+3)}{6} \\ &=
  \dfrac{(n+1)(2n^2 + 4n + 3n + 6)}{6} \\ &=
  \dfrac{(n+1)(2n^2 + 4n + 3n + 6)}{6} \\ &=
  \dfrac{(n+1)(2n^2 + 7n + 6)}{6}
\end{split}
\end{displaymath}
\end{enumerate}
Damit ist bei der linken und der rechten Seite jeweils das gleiche
herausgekommen und die Behauptung ist bewiesen.

\section{Struktur der natürlichen Zahlen}

Die vollständige Induktion aus dem vorigen Abschnitt ist nur für die
Menge der natürlichen Zahlen geeignet.  Sie funktioniert aber nicht für alle
Mengen: Für die reellen Zahlen $\mathbb{R}$ z.B.\ erreicht die
Konstruktion "<bei $0$ anfangen und dann immer um $1$ hochzählen"> einfach
nicht alle Elemente der Menge.%\footnote{Bei den ganzen Zahlen
%  $\mathbb{Z}$ und den rationalen Zahlen $\mathbb{Q}$ ist das anders,
%  da es sich um \textit{abzählbare Mengen} handelt.  Das ist
%  allerdings für unsere Zwecke nicht direkt relevant.}  HK: hier verwirrend...
Die
natürlichen Zahlen sind also etwas besonderes.  Das haben wir schon in
Kapitel~\ref{cha:recursion-numbers} gesehen: es sind Zahlen, die zählen,
und auf Seite~\pageref{page:datendefinition-N} steht eine
Datendefinition:
%
\begin{lstlisting}
; Eine natürliche Zahl ist eine der folgenden:
; - 0
; - der Nachfolger einer natürlichen Zahl
\end{lstlisting}
%
Diese Datendefinition können wir als Bastelanleitung für die Menge der
natürlichen Zahlen auffassen:
Diese Datendefinition erreicht \emph{jede} natürliche Zahl~-- jede Zahl kann
in der Form $0+1+\ldots+1$ geschrieben werden.  Für diese Art
Bastelanleitung für Mengen ist charakteristisch, dass es ein oder
mehrere \textit{Basiselemente}\index{Basiselement} gibt (in diesem
Fall die $0$) und dann ein oder mehrere Regeln, die aus beliebigeren
"<kleineren"> Elementen "<größere"> Elemente mit Hilfe eines Selbstbezug konstruieren, in diesem
Fall die Regel, die besagt, dass für jede natürliche Zahl auch ihr
Nachfolger eine natürliche Zahl ist.

Das mathematische Pendant für die Datendefinition der natürlichen
Zahlen sieht so aus:
%
\begin{definition}[natürliche Zahlen]
  \label{def:N}
  Die Menge der natürlichen Zahlen $\mathbb{N}$ ist folgendermaßen definiert:
  \begin{enumerate}
  \item $0\in\mathbb{N}$
  \item Für $n\in\mathbb{N}$ ist auch $n+1\in\mathbb{N}$.
  \item Die obigen Regeln definieren \emph{alle} $n\in\mathbb{N}$.
  \end{enumerate}
\end{definition}
% 
Eine solche Definition heißt auch \textit{induktive
  Definition}\index{induktive Definition}, die eine \textit{induktive
  Menge}\index{induktive Menge} definiert.  Die letzte Klausel ist bei
induktiven Definition immer dabei~--
ohne sie könnte zum Beispiel die Menge der reellen
Zahlen als $\mathbb{N}$ durchgehen, weil die Klauseln davor 
keinen Anspruch auf Vollständigkeit erheben könnten.  Diese Klausel
heißt \textit{induktiver Abschluss}.\index{induktiver Abschluss}

Wenn Du genau hinschaust, siehst Du, dass die induktive Definition genau die
gleiche Struktur hat wie die Definition der Induktion von
Seite~\pageref{page:mathematical-induction}: Es gibt eine Klausel für
die $0$ und eine Klausel für den Schritt von $n$ nach $n+1$.  Die induktive
Definition sagt, dass es zwei verschiedene Sorten von natürlichen
Zahlen gibt, nämlich das Basiselement $0$ aus der ersten Regel der
Definition und die (positiven) Zahlen $n+1$ aus der zweiten Klausel.
Diese Struktur entspricht außerdem der Datendefinition und der Schablone aus
Konstruktionsanleitung~\ref{ka:nats-eingabe-schablone} auf
Seite~\pageref{ka:nats-eingabe-schablone}.

Entsprechend muss eine Behauptung über die natürlichen Zahlen für beide
Sorten bewiesen werden: Einerseits für das Basiselement $0$ und
andererseits für die positiven Zahlen, die keine Basiselemente sind.
Die Klauseln für die Basiselemente heißen
\textit{Induktionsverankerungen}\index{Induktionsverankerung}.  Da die
zweite Klausel einen \textit{Selbstbezug}\index{Selbstbezug}
enthält~-- es muss schon eine natürliche Zahl da sein, um eine weitere
zu finden~-- muss dort ein Induktionsschluss bewiesen werden.

Die natürlichen Zahlen haben nur ein Basiselement und es gibt nur eine
Klausel mit Selbstbezug.  In Abschnitt~\ref{sec:financial-contracts} auf
Seite~\ref{sec:financial-contracts} ging es um Finanzverträge~-- da
gab es mehr als eine Klausel mit Selbstbezug, und auch in diesem
Kapitel werden wir noch ein solches Beispiel sehen.

\section{Endliche Folgen}
\label{sec:finite-sequences}

Die natürlichen Zahlen sind nicht die einzige induktiv definierte
Menge.  Ein weiteres Beispiel sind die \index{Folge}\index{endliche
  Folge}\textit{endlichen Folgen}, die den Listen entsprechen:

\begin{definition}
  \label{def:finite-sequences}
  Sei $M$ eine beliebige Menge.  Die Menge $M^\ast$ der \textit{endlichen
    Folgen} über $M$ ist folgendermaßen definiert:\index{*@$M^\ast$}
    \begin{enumerate}
    \item Es gibt eine \textit{leere Folge}\footnote{In
        Kapitel~\ref{cha:list} wurde bereits erklärt, wieso es sinnvoll
        ist, mit der leeren Folge anzufangen.}
        % Auf den ersten
        % Blick scheint das Konzept einer leeren Folge, die keine
        % Elemente enthält, merkwürdig. Die Informatik hat aber die
        % Erfahrung gemacht, dass allzu oft Programme abstürzen, weil
        % sie irgendwo "<nichts"> vorfinden, wo sie doch mindestens
        % "<etwas"> erwarteten. Auf den zweiten Blick ist die leere
        % Folge aber das Analog zu der $0$ bei den natürlichen Zahlen.}
     $\epsilon \in
      M^\ast$.\index{*@$\epsilon$}\index{leere Folge}
    \item Wenn $f \in M^\ast$ eine Folge ist und $m \in M$, so ist $mf
      \in M^\ast$, also auch eine Folge.
    \item Die obigen Regeln definieren \emph{alle} $f\in M^\ast$.
    \end{enumerate}
\end{definition}
%
Eine Folge entsteht also aus einer 
bestehenden Folge dadurch, dass vorn noch ein Element angehängt wird.  
Folgen über $M = \{a,b,c\}$ sind deshalb etwa
\[ \epsilon, a\epsilon, b\epsilon, c\epsilon, aa\epsilon ,
ab\epsilon , ac\epsilon ,\ldots, abc\epsilon,\ldots\ cbba\epsilon,
\ldots \quad\textrm{(nicht alphabetisch sortiert)}\]
Da das $\epsilon$ bei nichtleeren Folgen immer dazugehört, wird es oft
nicht mitnotiert.

Die Definition der endlichen Folgen ist analog zur
Definition~\ref{def:N}: Die erste Klausel ist der \textit{Basisfall},
die zweite Klausel enthält einen \textit{Selbstbezug} und die dritte
Klausel bildet den induktiven Abschluss.

\subsection{Funktionen auf endlichen Folgen}
\label{sec:functions-on-finite-sequences}

Dieser Abschnitt demonstriert, wie mathematische Funktionen auf endlichen Folgen
formuliert werden.  Als Beispiel ist eine Funktion $s :
\err^\ast \rightarrow \err$ gefragt, die für eine Folge deren Summe
ausrechnet, also z.B.:
%
\begin{displaymath}
  \begin{split}
  s(1~2~3~\epsilon) &= 6 \\
  s(2~3~5~7\epsilon) &= 17\\
  s(17~23~42~5~\epsilon) &= 87
\end{split}
\end{displaymath}
% 
Die Funktion entspricht also der Funktion \texttt{list-sum} aus
Abschnitt~\ref{sec:list-sum}.  Da es zwei verschiedene Sorten endlicher Folgen gibt~-- die leere
Folge und die "<nichtleeren"> Folgen~-- liegt es
nahe, die entsprechende Funktion mit einer Verzweigung zu schreiben,
die zwischen den beiden Sorten unterscheidet:
%
\begin{displaymath}
  s(f) \deq
  \begin{cases}
    ? & \textrm{falls $f = \epsilon$}\\
    ? & \textrm{falls $f = mf'$, $m\in M, f'\in M^\ast$}
  \end{cases}
\end{displaymath}
%
Es fehlen nur noch die Teile der Definition, wo Fragezeichen stehen:

Die Summe der leeren Folge ist $0$:  Wenn es sich um eine andere
Zahl $m \neq 0$ handeln würde, ließe sich schließlich die Summe einer
beliebigen Folge durch das Anhängen der leeren Folge um $m$ verändern.
Die erste Lücke ist also schon geschlossen:
%
\begin{displaymath}
  s(f) \deq
  \begin{cases}
    0 & \textrm{falls $f = \epsilon$}\\
    ? & \textrm{falls $f = mf'$, $m\in M, f'\in M^\ast$}
  \end{cases}
\end{displaymath}
%
Im zweiten Fall handelt es sich bei $f$ um ein
zusammengesetztes Objekt mit den Bestandteilen $m$ und $f'$.
Deshalb können $m$ und $f'$ für die Konstruktion des Funktionswerts
herangezogen werden:
%
\begin{displaymath}
  s(f) \deq
  \begin{cases}
    0 & \textrm{falls $f = \epsilon$}\\
    \ldots m \ldots f' \ldots & \textrm{falls $f = mf'$, $m\in M, f'\in M^\ast$}
  \end{cases}
\end{displaymath}
%
Soweit sind die bekannten Techniken für die Konstruktion von
Funktionen auf gemischten und zusammengesetzten Daten zur Anwendung
gekommen, lediglich übertragen von Programm-Funktionen auf
mathematische Funktionen.

Für den nächsten Schritt passt~-- genau wie beim Programmieren~-- ein
rekursiver Aufruf zum Selbstbezug. Die Funktionsdefinition verdichtet sich
folgendermaßen:
%
\begin{displaymath}
  s(f) \deq
  \begin{cases}
    0 & \textrm{falls $f = \epsilon$}\\
    \ldots m \ldots s(f') \ldots & \textrm{falls $f = mf'$, $m\in M, f'\in M^\ast$}
  \end{cases}
\end{displaymath}
%
Hier ist $s(f')$ die Summe aller
Folgenelemente in $f'$.  Gefragt ist die Summe aller Folgenelemente
von $f = mf'$.  Es fehlt also zur Summe nur noch $m$ selbst:
%
\begin{displaymath}
  s(f) \deq
  \begin{cases}
    0 & \textrm{falls $f = \epsilon$}\\
    m + s(f') & \textrm{falls $f = mf'$, $m\in M, f'\in M^\ast$}
  \end{cases}
\end{displaymath}
%
Mit Papier und Bleistift können wir schnell nachvollziehen, dass die
Definition korrekt arbeitet:
%
\begin{displaymath}
  \begin{split}
  s(17~23~42~5~\epsilon) &= 17 + s(23~42~5~\epsilon)
  \\
  &= 17 + 23 + s(42~5~\epsilon)
  \\
  &= 17 + 23 + 42 + s(5~\epsilon)
  \\
  &= 17 + 23 + 42 + 5 + s(\epsilon)
  \\
  &= 17 + 23 + 42 + 5 + 0
  \\
  &= 87
\end{split}
\end{displaymath}
% 
Die Definition von $s$ ruft sich also an der Stelle selbst auf,
an der die induktive Definition der endlichen Folgen den Selbstbezug
"<$f' \in M^\ast$ eine Folge"> enthält.  

Vielleicht begegnest Du der Definition von $s$ mit Skepsis, taucht
doch $s$ sowohl auf der linken als auch auf der rechten Seite auf.  Es
sieht so aus, als sei $s$ "<durch sich selbst definiert">.
Tatsächlich ist dies jedoch kein Problem, da:
%
\begin{itemize}
\item sich $s(f)$ stets selbst auf einer \emph{kürzeren} Folge
  $f'$ aufruft, und
\item schließlich bei der leeren Folge landet, bei der die Verzweigung
  greift und keinen weiteren rekursiven Aufruf mehr vornimmt.
\end{itemize}
%
Solange eine rekursive Funktion dem Schema von $s$ folgt und damit der
Struktur der Folgen selbst, sind diese beiden Bedingungen automatisch
erfüllt.

\subsection{Folgeninduktion}
\label{sec:sequence-induction}
Das Gegenstück zur vollständigen Induktion heißt bei den Folgen
\textit{Folgeninduktion}.  Der "<Schluss von $n$ auf $n+1$"> wird bei
der Folgeninduktion zu je einem Schluss von $f$ auf $mf$ für alle
Folgen $f$ und alle $m\in M$ . Oft kommt es dabei auf das Folgenelement $m$ gar
nicht an.

Zum
Beweis der Behauptung, dass eine bestimmte Behauptung für alle
$f\in M^\ast$ gilt, genügt es, die folgenden Beweise zu führen:
\begin{enumerate} 
\item Die Behauptung gilt für $f=\epsilon$ (\textit{Induktionsanfang})\index{Induktionsanfang}
\item Wenn die Behauptung für eine Folge $f$ gilt, so gilt sie auch
  für alle Folgen $mf$ wobei $m\in{M}$.
  (\textit{Induktionsschluss}).\index{Induktionsschluss}
\end{enumerate}
% 
Die Folgeninduktion funktioniert, weil sie der Struktur der Definition
der endlichen Folgen~\ref{def:finite-sequences} genauso folgt wie die
vollständige Induktion der Struktur der natürlichen Zahlen.  Das Lemma
lässt sich auch mit Hilfe der vollständigen Induktion beweisen~-- siehe
Aufgabe \ref{aufgabe:folgeninduktion}.

Entsprechend der vollständigen Induktion gibt es auch für die
Folgeninduktion eine Anleitung:
%
\begin{enumerate}
\item Formuliere die zu beweisende Behauptung als Behauptung der
  Form "<Für alle $f\in M^\ast$ gilt~\ldots">, falls das noch nicht
  geschehen ist.
\item Schreibe die Überschrift "<$f = \epsilon$:">. Schreibe die
  Behauptung noch einmal ab, wobei Du das "<für alle $f\in M^\ast$"> weglässt und für $f$ das $\epsilon$ einsetzt.
\item Beweise die abgeschriebene Behauptung.  (Das ist oft
  einfach.)
\item Schreibe das Wort "<Induktionsvoraussetzung:"> Schreibe
  darunter die Behauptung noch einmal ab, wobei Du das "<für
  alle $f\in M^\ast$"> weglässt~-- lass das $f$ da, wo es ist.
\item Schreibe "<Induktionsschluss (zu zeigen):">.
  Schreibe darunter die Behauptung noch einmal ab, wobei Du für
  $f$ stattdessen $mf$ einsetzt.  (Lass das "<für alle
  $f\in M^\ast$"> wieder weg.)
\item Beweise den Induktionsschluss unter Verwendung der
  Induktionsvoraussetzung.  Denke daran, die Behauptung für
  \emph{alle} $m\in M$ zu beweisen~-- das ist meist aber nicht immer
  einfach.

  Wenn die Behauptung eine Gleichung der Form $A = B$ ist, kannst
  Du häufig die Induktionsvoraussetzung entweder direkt oder nach
  einigen Umformungen in den Induktionsschluss einsetzen.
\end{enumerate}
%
Für ein sinnvolles Beispiel dient die Funktion cat, die Folgen
aneinanderhängt:\index{cat}
%
\begin{displaymath}
  \textrm{cat}(f_1, f_2)
  \deq
  \begin{cases}
    f_2 & \textrm{ falls $f_1 = \epsilon$}\\
    m\;\textrm{cat}(f_1', f_2)& \textrm{ falls $f_1 = mf_1'$, $m\in M, f_1'\in M^\ast$}
  \end{cases}
\end{displaymath}
Es soll bewiesen werden, dass cat assoziativ\label{Assoziativität} ist, das heißt für alle 
$u,v,w \in M^{\ast}$ gilt
\begin{displaymath}
  {\rm cat}(u,{\rm cat}(v,w))  = {\rm cat}({\rm cat}(u,v),w).
\end{displaymath}
% 
\begin{enumerate}
\item Die Form der Behauptung ist noch problematisch, da in ihr drei Folgen
  auftauchen~-- und keine davon heißt $f$.  Im schlimmsten Fall musst
  Du raten, über welche Folge die Induktion geht und gegebenenfalls
  alle Möglichkeiten durchprobieren.  Wir entscheiden uns für die
  erste Folge $u$ und benennen sie in $f$ um, damit der Beweis auf die
  Anleitung passt:
  %
  \begin{displaymath}
    \forall f\in M^\ast:\forall v,w\in M^\ast: {\rm cat}(f,{\rm cat}(v,w))  =  {\rm cat}({\rm cat}(f,v),w)
  \end{displaymath}
\item
  $f=\epsilon$: Hier gilt
  \begin{displaymath}
    \begin{split}
    {\rm cat}(\epsilon, {\rm cat}(v, w)) & = {\rm cat}(v,w)\\
    {\rm cat}({\rm cat}(\epsilon, v), w) & = {\rm cat}(v,w)
  \end{split}
\end{displaymath}
  nach der definierenden Gleichung.
\item Induktionsvoraussetzung:
%
\begin{displaymath}
  {\rm cat}(f,{\rm cat}(v,w))  = {\rm cat}({\rm cat}(f,v),w)
\end{displaymath}
%
\item Induktionsschluss (zu zeigen): 
%
\begin{displaymath}
  {\rm cat}(mf,{\rm cat}(v,w))  = {\rm cat}({\rm cat}(mf,v),w)
\end{displaymath}
%
\item Wir benutzen die Definition von cat, um die linke Seite weiter
  auszurechnen:
  %
  \begin{displaymath}
    {\rm cat}(mf,{\rm cat}(v,w)) = m \mathrm{cat}(f,\mathrm{cat}(v, w))
  \end{displaymath}
  %
  Hier steht aber $\mathrm{cat}(f,\mathrm{cat}(v, w))$~-- und das
  steht auch auf der linken Seite der Induktionsvoraussetzung.  Wir
  können also einsetzen:
  \begin{displaymath}
    = m {\rm cat}({\rm cat}(f,v),w)
  \end{displaymath}
  Ebenso können wir die rechte Seite ausrechnen:
  \begin{displaymath}
    \begin{split}
    \mathrm{cat}(\mathrm{cat}(mf,v),w) &=
    \mathrm{cat}(m\mathrm{cat}(f,v), w)\\ &=
    m\mathrm{cat}(\mathrm{cat}(f,v), w)
  \end{split}
\end{displaymath}  %
  % 
  Das ist aber das gleiche, das auch bei der linken Seite
  herausgekommen ist~-- der Beweis ist fertig.
\end{enumerate}


\section{Notation für induktive Definitionen}

Induktive Mengen kommen in der Informatik enorm häufig vor~-- so
häufig, dass sich eine Kurzschreibweise für ihre induktiven
Definitionen eingebürgert hat, die sogenannte \textit{kontextfreie
  Grammatik}\index{Grammatik}\index{kontextfreie Grammatik}.  In den
meisten Informatik-Büchern geht mit dem Begriff eine langwierige
mathematische Definition einher, die wir für dieses Buch nicht in aller
Ausführlichkeit benötigen.  Wir benutzen die kontextfreie Grammatik
(ab hier einfach nur "<Grammatik">) informell als Abkürzung für
eine länger ausgeschriebene induktive Definition.  Hier die Grammatik
für die natürlichen Zahlen:
%
\begin{grammar}
  \meta{$\mathbb{N}$} \: 0 \| \meta{$\mathbb{N}$} + 1
\end{grammar}
%
In der Grammatik steht \meta{$\mathbb{N}$} für "<eine natürliche
Zahl">.  Lesen kannst Du die Grammatik so: Eine natürliche Zahl ist
entweder die $0$ oder hat die Form $n + 1$ wobei $n$ wiederum eine
natürliche Zahl ist.  Der obligatorische induktive Abschluss ("<Die
obigen Regeln definieren \emph{alle} $n\in\mathbb{N}$.">) wird
stillschweigend vorausgesetzt
und darum weggelassen.  

Das Zeichen \goesto{} kann also als "<ist"> oder "<hat die Form">
gelesen werden, das Zeichen $\vert$ als "<oder">. Die Notation
\meta{$X$} definiert eine entsprechende Menge $X$.  Die Grammatik ist
also eine Art mathematische Schreibweise für zusammengesetzte Daten,
gemischte Daten ($\vert$) und Selbstbezüge, nur eben für mathematische
Objekte.

Für die Menge der Folgen über einer Menge $M$ genügt also folgende Notation:
%
\begin{grammar}
  \meta{$M^\ast$} \: $\epsilon$ \| \meta{$M$} \meta{$M^\ast$}
\end{grammar}
%
In beiden Definitionen ist jeweils der Selbstbezug klar zu sehen: 
Bei den natürlichen Zahlen taucht  \meta{$\mathbb{N}$} in einer
Klausel auf, bei den Folgen \meta{$M^\ast$}.  Alle anderen Klauseln~--
also die ohne Selbstbezug~-- beschreiben Basisfälle.

\section{Strukturelle Rekursion}

In Abschnitt~\ref{sec:finite-sequences} ist zu sehen, dass die
Definition der beiden Beispielfunktionen auf Folgen ($s$ und
$\mathrm{cat}$) jeweils der induktiven Definition der Folgen
"<folgt">~-- die Definition beider Funktionen hat die Form:
%
\begin{displaymath}
  F(f, \ldots)
  \deq
  \begin{cases}
    \ldots & \textrm{ falls $f = \epsilon$}\\
    \ldots F(f') \ldots \ & \textrm{ falls $f = mf', m\in M, f'\in M^\ast$}
  \end{cases}
\end{displaymath}
%
Das ist kein Zufall: Die rekursive Funktionsdefinition gehört zur
induktiven Mengendefinition wie Pech zu Schwefel.  Zwei Grundregeln
legen diese Form fest:
%
\begin{enumerate}
\item Für jede Klausel gibt es eine Verzweigung mit einem Zweig  der
  induktiven Definition.
\item Bei Selbstbezügen steht im entsprechenden Zweig ein
  Selbstaufruf.
\end{enumerate}
%
Auch bei den natürlichen Zahlen lassen sich viele Operationen rekursiv
aufschreiben.  Zum Beispiel die Potenz:
%
\begin{displaymath}
  b^n \deq
  \begin{cases}
    1 & \textrm{falls } n = 0\\
    b b^{n'} & \textrm{falls } n = n' +1, n'\in\enn
  \end{cases}
\end{displaymath}
%
Die Notation $n = n' + 1$ folgt zwar der induktiven Definition, ist
hier aber gleichbedeutend mit $n>0$ und $n' = n - 1$.  Deshalb werden
induktive Definitionen auf natürlichen Zahlen meist so geschrieben:
%
\begin{displaymath}
  b^n \deq
  \begin{cases}
    1 & \textrm{falls } n = 0\\
    b b^{n-1} & \textrm{falls } n > 0
  \end{cases}
\end{displaymath}
%
Die Korrespondenz zwischen induktiven Definitionen und den rekursiven
Funktionen lässt sich auch allgemein formulieren.  Angenommen, die
Menge $X$ ist durch einer Grammatik definiert, die $n$ Klauseln hat:
%
\begin{grammar}
  \meta{X} \: $C_1$ \| \ldots \| $C_n$
\end{grammar}
%
Eine Funktion auf dieser Menge braucht dann~-- genau wie bei
gemischten Daten~-- eine Verzweigung mit $n$
Zweigen, eine für jede Klausel:
%
\begin{displaymath}
   F(x) \deq
  \begin{cases}
    R_1 & \textrm{falls } x = F_1
    \\
    \ldots
    \\
    R_n & \textrm{falls } x = F_n
  \end{cases}
\end{displaymath}
%
Die Bedingung $x = F_i$ ergibt sich jeweils aus der entsprechenden
Klausel.  Wenn dort Bezüge zu anderen Mengen oder Selbstbezüge stehen,
so werden diese durch Variablen ersetzt und entsprechende
Mengenzugehörigkeiten.  Angenommen, die Klausel $C_i$ hat beispielsweise diese
Form:
\begin{grammar}
  \> [ \meta{A} \& \meta{B} ]
\end{grammar}
%
Dann müsste $F_i$ entsprechend so aussehen:
%
\begin{displaymath}
  x = \mathtt{[}~a~\mathtt{\&}~b~\mathtt{]}, a\in A, b\in B
\end{displaymath}
%
Eine Klausel $C_i$ mit Selbstbezug sähe beispielsweise so aus:
%
\begin{grammar}
  \> \verb|{| \meta{X} \verb|}|
\end{grammar}
%
Das dazugehörige $F_i$ sähe so aus:
%
\begin{displaymath}
  x = \verb|{|~x'~\verb|}|, x'\in X
\end{displaymath}
%
Dementsprechend steht höchstwahrscheinlich in der rechten Seite $R_i$
ein rekursiver Aufruf $F(x')$.

Funktionen dieser Form, die der Struktur einer induktiven Menge direkt
folgen, heißen \textit{strukturell rekursiv}.\index{strukturelle
  Rekursion}\index{Rekursion!strukturell}  

Hier ein Beispiel für eine induktiv definierte Menge, deren Struktur
etwas reichhaltiger ist, als die der natürlichen Zahlen oder der
Folgen.  Die Grammatik beschreibt einfache aussagenlogische Ausdrücke:
%
\begin{grammar}
  \meta{E} \: $\top$ \| $\bot$
  \> \| \meta{E} $\wedge$ \meta{E}
  \> \| \meta{E} $\vee$ \meta{E}
  \> \| $\neg$ \meta{E}
\end{grammar}
%
Gedacht ist das folgendermaßen: $\top$ steht für "<wahr">, $\bot$ für
"<falsch">, $\wedge$ für "<und">, $\vee$ für "<oder"> und $\neg$ für
"<nicht">.  Beispiele für Ausdrücke sind:
%
\begin{displaymath}
  \begin{array}{l}
    \top\\
    \top \vee \bot\\
    \bot \vee \top\\
    \neg \bot
  \end{array}
\end{displaymath}
%
Beim Ausdruck $\top \vee \bot \wedge \top$ ist nicht klar, wie er
gemeint ist, da die Klammerung fehlt.  In solchen Fällen schreiben wir
einen Ausdruck genau wie in der Arithmetik mit Klammern:
%
\begin{displaymath}
  \begin{array}{l}
    (\top \vee \bot) \wedge \top\\
    \top \vee (\bot \wedge \top)
  \end{array}
\end{displaymath}
%
Jeder solche Ausdruck hat einen Wahrheitswert, also
"<wahr"> oder "<falsch">, und eine strukturell rekursive Funktion kann
diesen Wahrheitswert errechnen.  Diese Funktion "<heißt"> $\llbracket
\underline{~}\rrbracket$\index{*@$\llbracket\underline{~}\rrbracket$}~--
für einen Ausdruck $e$ liefert $\llbracket e\rrbracket$ den Wert $1$,
falls der Ausdruck "<wahr"> ist und $1$, falls "<falsch">.  Die
doppelten eckigen Klammern heißen in der Fachsprache "<Semantikklammern">\index{Semantikklammern}
und werden oft benutzt, um Funktionen auf Mengen zu schreiben, die
durch eine Grammatik definiert sind.

Die Funktionsdefinition besteht, wie oben beschrieben, auf jeden Fall
aus einer Verzweigung, die für jede Klausel der Grammatik einen Zweig
aufweist:
%
\begin{displaymath}
  \llbracket e \rrbracket \deq
  \begin{cases}
    ? & \textrm{falls } e = \top\\
    ? & \textrm{falls } e = \bot\\
    ? & 
    \textrm{falls } e =
    e_1\wedge e_2\\
    ? & 
    \textrm{falls } e =
    e_1\vee e_2\\
    ? & \textrm{falls } e = \neg e'
  \end{cases}
\end{displaymath}
%
In den Zweigen für $\wedge$, $\vee$ und $\neg$ sind rekursive Aufrufe
angezeigt, weil in der Grammatik dort Selbstbezüge stehen:
%
\begin{displaymath}
  \llbracket e \rrbracket \deq
  \begin{cases}
    ? & \textrm{falls } e = \top\\
    ? & \textrm{falls } e = \bot\\
    \ldots \llbracket e_1\rrbracket\ldots\llbracket e_2\rrbracket  & 
    \textrm{falls } e =
    e_1\wedge e_2\\
    \ldots \llbracket e_1\rrbracket\ldots\llbracket e_2\rrbracket & 
    \textrm{falls } e =
    e_1\vee e_2\\
    \ldots \llbracket e'\rrbracket\ldots  & \textrm{falls } e = \neg e'
  \end{cases}
\end{displaymath}
%
Die ersten beiden Fälle liefern $1$ und $0$ respektive, für die
weiteren Fälle werden folgende Hilfsfunktionen definiert:

\begin{displaymath}
  \begin{array}{cc}
  a(t_1, t_2) \deq 
  \begin{cases}
    1 & \textrm{falls } t_1 = 1 \textrm{ und } t_2 = 1\\
    0 & sonst
  \end{cases}
  &
  o(t_1, t_2) \deq 
  \begin{cases}
    0 & \textrm{falls } t_1 = 0 \textrm{ und } t_2 = 0\\
    1 & sonst
  \end{cases}
\end{array}
\end{displaymath}

\begin{displaymath}
  n(t) \deq 
  \begin{cases}
    1 & \textrm{falls } t = 0\\
    0 & \textrm{falls } t = 1
  \end{cases}
\end{displaymath}
%
Die Funktion $a$ liefert nur dann 1, wenn $t_1$ \emph{und} $t_2$ 1
sind (sonst $0$).  Die Funktion $o$ liefert dann 1, wenn $t_1$
\emph{oder} $t_2$ 1 sind (sonst $0$).  Die Funktion $n$ liefert dann
1, wenn $t$ \emph{nicht} 1 ist (sonst $0$).  Diese Funktionen
vervollständigen nun die Definition von $\llbracket \underline{~}
\rrbracket$:

\begin{displaymath}
  \llbracket e \rrbracket \deq
  \begin{cases}
    1 & \textrm{falls } e = \top\\
    0 & \textrm{falls } e = \bot\\
    a(\llbracket e_1 \rrbracket, \llbracket e_2 \rrbracket) & 
    \textrm{falls } e =
    e_1\wedge e_2\\
    o(\llbracket e_1 \rrbracket, \llbracket e_2 \rrbracket) & 
    \textrm{falls } e =
    e_1\vee e_2\\
    n(\llbracket e' \rrbracket) & \textrm{falls } e = \neg e'
  \end{cases}
\end{displaymath}

\section{Strukturelle Induktion}
\label{sec:structural-induction}

Beweise von Eigenschaften strukturell rekursiver Funktionen
funktionieren~-- wieder entsprechend den natürlichen Zahlen und den
Folgen~-- mit \textit{struktureller Induktion}\index{strukturelle
  Induktion}\index{Induktion!strukturell}. Strukturelle Induktion folgt
ebenfalls der Struktur der Grammatik~-- vollständige Induktion und
Folgeninduktion sind also Spezialfälle.  Folgendes Beispiel~-- aufbauend
auf den aussagenlogischen Ausdrücken aus dem vorigen Abschnitt~--
illustriert die Technik:

\begin{satz}
  Aus einem aussagenlogischen Ausdruck $e$ entsteht der Ausdruck
  $\overline{e}$\label{page:overline}, indem jedes $\top$ durch $\bot$, jedes $\bot$ durch
  $\top$, jedes $\wedge$ durch $\vee$ und jedes $\vee$ durch $\wedge$
  ersetzt wird.  Es gilt für jeden Ausdruck $e$:
  \begin{displaymath}
    \llbracket \overline{e}\rrbracket = n(\llbracket e\rrbracket)
  \end{displaymath}
\end{satz}
%
Die Behauptung hat bereits die für einen Induktionsbeweis geeignete
Form "<für alle $e$">, wobei $e$ aus einer induktiv definierten Menge
kommt.  Die Behauptung muss jetzt für alle möglichen Fälle von $e$
bewiesen werden~-- da die Grammatik für Ausdrücke fünf Fälle hat, sind
auch fünf Fälle zu beweisen: $e=\top$, $e=\bot$, $e=e_1\wedge e_2$,
$e_1\vee e_2$ und $e=\neg e'$, wobei $e_1$, $e_2$ und $e'$
ihrerseits Ausdrücke sind.

Hier sind die Beweise für die Fälle $e=\top$, $e=\bot$:

\begin{displaymath}
  \begin{array}{c@{\qquad\qquad}c}
  \begin{split}
  \llbracket \top \rrbracket &= 1\\[1ex]
  \llbracket \overline{\top} \rrbracket &= \llbracket \bot \rrbracket
  \\ &= 0
  \\ &= n(1)
\end{split}
&
\begin{split}
  \llbracket \bot \rrbracket &= 0\\[1ex]
  \llbracket \overline{\bot} \rrbracket &= \llbracket \top \rrbracket
  \\ &= 1
  \\ &= n(0)
\end{split}
\end{array}
\end{displaymath}
%
Als Nächstes ist der Fall $e=e_1\wedge e_2$ an der Reihe.  Da die
Klausel 
\begin{grammar}
  \meta{E} \: $\ldots$ \| \meta{E} $\wedge$ \meta{E}
\end{grammar}
%
zwei Selbstbezüge hat, gibt es auch eine zweiteilige
Induktionsvoraussetzung~-- die Behauptung kann für $e_1$ und $e_2$
angenommen werden: $\llbracket \overline{e_1} \rrbracket =
n(\llbracket e_1\rrbracket)$, $\llbracket \overline{e_2} \rrbracket =
n(\llbracket e_2\rrbracket)$.  Der Induktionsschluss dazu sieht so aus:
%
\begin{alignat*}{3}
  \llbracket e_1 \wedge e_2 \rrbracket &= a(\llbracket
  e_1\rrbracket, \llbracket e_2\rrbracket)
  \\[1ex]
  \llbracket \overline{e_1 \wedge e_2} \rrbracket &= \llbracket
  \overline{e_1} \vee \overline{e_2} \rrbracket
  && \qquad \text{Definition von $\overline{\raisebox{1ex}{\hspace{1ex}}}$}
  \\
  &= 
  o(\llbracket \overline{e_1} \rrbracket,  \llbracket \overline{e_2}
  \rrbracket)
  \\
  &= o(n(\llbracket e_1\rrbracket), n(\llbracket e_2\rrbracket))
  && \qquad \text{Induktionsvoraussetzung}
  \\
  &= n(a(\llbracket e_1\rrbracket, \llbracket e_2\rrbracket))
\end{alignat*}
%
Der letzte Schritt ergibt sich aus genauer Betrachtung der
Definitionen von $o$ und $a$ bzw.\ durch Einsetzen aller möglichen
Werte für $t_1$ und $t_2$.

Der Fall $e=e_1\vee e_2$ folgt analog.  Wieder gibt es zwei
Selbstbezüge, also gilt wieder die zweiteilige Induktionsvoraussetzung
$\llbracket \overline{e_1} \rrbracket = n(\llbracket e_1\rrbracket)$,
$\llbracket \overline{e_2} \rrbracket = n(\llbracket e_2\rrbracket)$.
Induktionsschluss (zu zeigen):
%
\begin{alignat*}{3}
  \llbracket e_1 \vee e_2 \rrbracket &= o(\llbracket
  e_1\rrbracket, \llbracket e_2\rrbracket)
  \\[1ex]
  \llbracket \overline{e_1 \vee e_2} \rrbracket &= \llbracket
  \overline{e_1} \wedge \overline{e_2} \rrbracket
  && \qquad \text{Definition von $\overline{\raisebox{1ex}{\hspace{1ex}}}$}
  \\
  &= 
  a(\llbracket \overline{e_1} \rrbracket,  \llbracket \overline{e_2}
  \rrbracket)
  \\
  &= a(n(\llbracket e_1\rrbracket), n(\llbracket e_2\rrbracket))
  && \qquad \text{Induktionsvoraussetzung}
  \\
  &= n(o(\llbracket e_1\rrbracket, \llbracket e_2\rrbracket))
\end{alignat*}
%
Schließlich fehlt noch der Fall $e = \neg e'$.  Hier gibt es nur
einen Selbstbezug, entsprechend lautet die Induktionsvoraussetzung:
$\llbracket \overline{e'} \rrbracket = n(\llbracket e'\rrbracket)$.
Induktionsschluss (zu zeigen):
%
\begin{alignat*}{3}
  \llbracket \neg e' \rrbracket &= n(\llbracket e'\rrbracket)
  \\[1ex]
  \llbracket \overline{\neg e'} \rrbracket
  & =
  \neg \overline{e'}
  && \qquad \text{Definition von $\overline{\raisebox{1ex}{\hspace{1ex}}}$}
  \\
  &=
  n(\llbracket \overline{e'}\rrbracket)
  \\
  &= n(n(\llbracket e' \rrbracket))
  && \qquad \text{Induktionsvoraussetzung}
\end{alignat*}
%
Das Beispiel zeigt, dass strukturell induktive Beweise durchaus mehr
als einen "<Induktionsanfang"> haben können~-- hier die Fälle $\top$
und $\bot$.  Ebenso gibt es mehr als einen Induktionsschluss~-- einen
für jede Klausel mit Selbstbezug, hier sind das drei Fälle.

Für Beweise mit struktureller Induktion gilt also folgende Anleitung:
%
\begin{enumerate}
\item Formuliere Du die zu beweisende Behauptung als
  Behauptung der Form "<Für alle $x\in X$ gilt~\ldots"> (wobei $X$
  eine induktiv definierte Menge ist), falls das noch nicht geschehen
  ist.
\item Führe jetzt einen Beweis für jede einzelne Klausel $C_i$
  der induktiven Definition:
\item Schreibe die Überschrift "<$x = F_i$">, wobei $F_i$ eine
  Bedingung ist, die der Klausel entspricht.  Schreibe die
  Behauptung noch einmal ab, wobei Du das "<für alle $x\in X$">
  weglässt und für $x$ stattdessen $F_i$ einsetzt.
\item Wenn die Klausel keinen Selbstbezug enthält, so beweise die
  Behauptung direkt.
\item Wenn die Klausel einen oder mehrere Selbstbezüge enthält, so
  stehen in der Überschrift Variablen $x_j$ oder $x'$ o.ä., die
  ihrerseits Element von $X$ sind.  Schreibe dann die Überschrift
  "<Induktionsvoraussetzung:">. Schreibe darunter für jeden
  Selbstbezug die Behauptung noch einmal ab, wobei Du das "<für alle
  $x\in X$"> weglässt und für $x$ stattdessen $x_j$ bzw.\ $x'$
  einsetzt.

  Schreibe darunter das Wort "<Induktionsschluss"> und beweise
  die Behauptung.  Denke daran, die Induktionsvoraussetzung zu
  benutzen.
\end{enumerate}

\section*{Anmerkungen}

Die erste konstruktive Definitionen der natürlichen Zahlen wurde
bereits im Jahr 1889 von {\sc Peano} vorgeschlagen:

\begin{definition}[Peano-Axiome]\index{Peano-Axiome} \label{def:peano}
Die Menge $\mathbb{N}$ der natürlichen Zahlen ist durch folgende
Eigenschaften, die \textit{Peano-Axiome}, gegeben:
\begin{enumerate}
\item Es gibt eine natürliche Zahl $0 \in \mathbb{N}$.
\item Zu jeder Zahl $n \in \mathbb{N}$ gibt es eine Zahl $n' \in \mathbb{N}$, die
      \emph{Nachfolger\index{Nachfolger} von n} heißt.
\item Für alle $n \in \mathbb{N}$ ist $n' \not = 0$.
\item Aus $n' = m'$ folgt $n=m$.
\item Eine Menge $M$ von natürlichen Zahlen, welche die $0$ enthält und mit jeder
      Zahl $m \in M$ auch deren Nachfolger $m'$, ist mit $\mathbb{N}$ identisch.
\end{enumerate}
\end{definition}
%
Diese Definition ist äquivalent zu Definition~\ref{def:N} von
Seite~\pageref{def:N}.  Wie in Definition~\ref{def:N}, lässt sich
$\mathbb{N}$ sich aus den Peano-Axiomen schrittweise konstruieren.
Aus 1.\ und 2.\ folgt, dass es natürliche Zahlen
\begin{quote}
  $0, 0', 0'', 0''', 0'''',\ldots$
\end{quote}
gibt.  Ohne die $0$ am Anfang entsteht die Darstellung der natürlichen Zahlen
durch Striche.  Die Axiome 3 und 4 besagen, dass jede Zahl nur eine Strichdarstellung 
besitzt: jedes Anfügen eines Striches "<$\,'\,$"> erzeugt eine
völlig neue Zahl.

Die Peano-Formulierung ist zwar ähnlich zu Definition~\ref{def:N},
weist aber auch interessante Unterschiede auf:
%
\begin{itemize}
\item Für "<$n'$"> ist im täglichen Umgang natürlich die Bezeichnung
  "<$n+1$"> gebräuchlich.
\item Die dritte und vierte Bedingung zusammen besagen, dass die
  Nachfolgerfunktion injektiv ist, das heißt durch fortgesetzte Anwendung
  der Nachfolgerfunktion entstehen immer neue Elemente.
\item Schließlich beschreibt die fünfte Bedingung den
  \textit{induktiven Abschluss\index{induktiver Abschluss}}, der
  festlegt, dass außer den solchermaßen erzeugten Elementen keine
  weiteren existieren.  Axiom 5 wird auch \emph{Induktionsaxiom}
  \index{Induktionsaxiom} genannt.  In Definition~\ref{def:N} hat das
  Induktionsaxiom die üblichere Form "<Die obigen Regeln definieren
  \emph{alle} $n\in\mathbb{N}$.">  Ebenfalls üblich ist eine
  Formulierung wie wie "<\ldots die \emph{kleinste} Menge
  mit den Eigenschaften \ldots">.
\end{itemize}
%

\section*{Aufgaben}

\begin{aufgabe}
Beweise die Gaußsche
Summenformel\index{Gaußsche Summenformel} mit vollständiger Induktion:
\[\forall n\in\mathbb{N}: \sum_{i=0}^n i =
  \frac{n\cdot(n+1)}{2}\]
\end{aufgabe}

\begin{aufgabe}
  Betrachte folgende Tabelle:
  %
  \begin{displaymath}
    \begin{split}
    1 &= 1\\
    1-4&= -(1+2)\\
    1-4+9&= 1+2+3\\
    1-4+9-16&= -(1+2+3+4)
  \end{split}
\end{displaymath}  %
  % 
  Rate die Gleichung, die dieser Tabelle zugrundeliegt und
  schreibe in mathematischer Notation auf.  Beweise die Gleichung!
\end{aufgabe}

\begin{aufgabe}
  Beweise, dass folgende Gleichung für alle $n\in\enn$ gilt:
  \begin{displaymath}
    \sum_{i=0}^n i^3 = \left(\sum_{i=0}^n i\right)^2
  \end{displaymath}
\end{aufgabe}

\begin{aufgabe}
  Was ist falsch an folgendem Induktionsbeweis?

  \textbf{Behauptung} Alle Pferde haben die gleiche Farbe.

  \begin{beweis}\par
    \textbf{Induktionsanfang} Für eine leere Menge von Pferden gilt die
    Behauptung trivialerweise.
    
    \textbf{Induktionsschluss} Gegeben sei eine Menge von $n+1$ Pferden.
    Nimm ein Pferd aus der Menge heraus~-- die restlichen Pferde haben per
    Induktionsannahme die gleiche Farbe.  Nimm ein anderes Pferd aus
    der Menge heraus~-- wieder haben die restlichen Pferde per
    Induktionsannahme die gleiche Farbe.  Da die übrigen Pferde die
    Farbe in der Zwischenzeit nicht plötzlich gewechselt haben können, war es in beiden Fällen
    die gleiche Farbe, und alle $n+1$ Pferde haben diese Farbe.
\end{beweis}
\end{aufgabe}

\begin{aufgabe}
  Beweise mittels Induktion, dass über Folgen für 
  $u,v\in M^{\ast}$ gilt:
  %
  \begin{displaymath}
    \mathrm{len}(\mathrm{cat}(u, v)) = \mathrm{len}(u) + \mathrm{len}(v)
  \end{displaymath}
  %
  Dabei sei $\mathrm{len}$ die Länge von Folgen, definiert als:
  %
  \begin{displaymath}
    \mathrm{len}(f) \deq{}
    \begin{cases}
       0 & \textrm{falls $f = \epsilon$}\\
       \mathrm{len}(f') + 1 & \textrm{falls $f = mf'$}
    \end{cases}
  \end{displaymath}
\end{aufgabe}

\begin{aufgabe} Beweise durch Folgeninduktion:
  \begin{displaymath}
    \begin{split}
      {\rm cat}(v,w)&= {\rm cat}(z,w) \Rightarrow v=z\\
      {\rm cat}(v,w)&= {\rm cat}(v,z) \Rightarrow w=z
  \end{split}
\end{displaymath}
\end{aufgabe}

\begin{aufgabe}
  \label{aufgabe:folgeninduktion}
  Beweise die Korrektheit der Folgeninduktion aus
  Abschnitt~\ref{sec:sequence-induction} (Seite~\pageref{sec:sequence-induction}) mit
  Hilfe der vollständigen Induktion.  Beschreibe dazu, wie sich
  eine Aussage über alle Folgen in eine Aussage über die Längen der
  Folgen umwandeln lässt.  Setze dann die Klauseln der
  vollständigen Induktion mit den entsprechenden Klauseln der
  Folgeninduktion in Beziehung.
\end{aufgabe}

\begin{aufgabe}
  Gib eine induktive Definition der umgangssprachlich
  definierten Funktion $\overline{\raisebox{1ex}{\hspace{1ex}}}$ aus
  Abschnitt~\ref{sec:structural-induction}
  (Seite~\pageref{page:overline}) an.
\end{aufgabe}

\begin{aufgabe}
  Gib eine Datendefinition für die aussagenlogischen Ausdrücke
  aus Abschnitt~\ref{sec:structural-induction} an.  Programmiere
  die Funktion~$\llbracket\underline{~}\rrbracket$ sowie die Funktion 
  $\overline{\raisebox{1ex}{\hspace{1ex}}}$.
\end{aufgabe}

\begin{aufgabe}
  Die \textit{Fibonacci\index{Fibonacci-Function}}-Funktion auf den natürlichen Zahlen ist
  folgendermaßen definiert:
%
  \begin{displaymath}
    \mathit{fib}(n) \deq{} \left\{
      \begin{array}{ll}
        0 & \textrm{falls } x = 0\\
        1 & \textrm{falls } x = 1\\
        \mathit{fib}(n-2) + \mathit{fib}(n-1) & \textrm{sonst}
      \end{array}\right.
    \end{displaymath}
%
    Beweise, dass $\mathit{fib}(n)$ die ganze Zahl ist, die am nächsten
    zu $\Phi^n/\sqrt{5}$ liegt, wobei $\Phi = (1+\sqrt{5})/2$.
    
    Anleitung: Zeige, dass $\mathit{fib}(n) = (\Phi^n -
    \Psi^n)/\sqrt{5}$, wobei $\Psi = (1-\sqrt{5})/2$.
\end{aufgabe}

\begin{aufgabe}
Eine partielle Ordnung $\preccurlyeq$ auf einer Menge $M$ heißt
\textit{wohlfundiert}\index{Ordnung!wohlfundiert} oder \textit{noethersch\index{Ordnung!noethersch}\index{noethersche Ordnung}}, wenn es keine
unendlichen Folgen $(x_i)_{i\in \enn}$ gibt, so dass für alle $i\in\enn$ gilt
%
\begin{displaymath}
  x_{i+1} \preccurlyeq x_{i} \text{ und } x_{i+1} \neq x_{i}
\end{displaymath}
%
auch geschrieben als:
%
\begin{displaymath}
  x_{i+1} \prec x_{i}\ .
\end{displaymath}
%

Das Beweisprinzip der \textit{wohlfundierten}\index{wohlfundierte Induktion}\index{Induktion!wohlfundiert} oder \textit{noetherschen Induktion}\index{noethersche
  Induktion}\index{Induktion!noethersch} ist dafür zuständig, die
Gültigkeit eines Prädikats $P$ auf $M$ zu beweisen, wenn es eine
wohlfundierte Ordnung $\preccurlyeq$ auf auf $M$ gibt.  Es besagt, dass
es ausreicht, $P(z)$ unter der Voraussetzung nachzuweisen, dass $P(y)$
für alle Vorgänger $y$ von $z$ gilt.  Anders gesagt:
%
\begin{displaymath}
  \forall z\in M:(\forall y\in M:~ y\prec z \Rightarrow P(y)) \Rightarrow P(z))
  \Rightarrow \forall x \in M:~P(x)
\end{displaymath}
%
Leite die vollständige und die strukturelle Induktion als Spezialfälle
der wohlfundierten Induktion her.
\end{aufgabe}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "i1"
%%% End: