swp_2.tex

\chapter{Semantik von Programmiersprachen}
\ifthenelse{\boolean{long}}{}{\begin{comment}}
Im ersten Kapitel haben wir uns damit beschäftigt wie ein Wort (Programm) einer Sprache eindeutig geparst werden kann.
Die Wörter (Programme) haben jedoch noch keine Bedeutung. Wir wollen uns nun damit beschäftigen
Sprachen eine Bedeutung zu geben und Sprachen anhand der Bedeutung der Wörter 
zu unterscheiden. Im Kontext der Semantik verwenden wir vermehrt den Begriff ``Programm einer Programmiersprache'' anstatt ``Wort einer Sprache''.

Im zweiten Kapitel betrachten wir nur noch syntaktisch korrekte Eingaben, d.h. wir betrachten den Fall nachdem der Parser bereits
entschieden hat, dass eine Eingabe ein syntaktisch gültiges Programm ist.

Wir teilen dazu Sprachen hauptsächlich in funktionale, imperative und logische Sprachen.
Zu jedem dieser drei Sprachparadigmen werden wir Sprachen konstruieren und deren
Semantik definieren.

Sowohl für die Definition der Semantik als auch für die Interpretation eines konkreten Programms
in einer Sprache, werden wir mathematische Funktionen definieren: die Interpretationsfunktion sowie weitere Hilfsfunktionen.
Diese mathematische Definition wird es uns erlauben die Korrektheit unserer Programme
zu beweisen.

Um Syntax und Semantik zu unterscheiden werden wir Programme einer Sprache wie bisher unterstreichen.
Die Beschreibung der Semantik ist kein Programm und wird daher auch keinesfalls unterstrichen.

\begin{bsp}
Was drückt der Ausdruck \u{a = b + c} aus? (vgl. Vorlesungsskriptum Seite 42)

Es gibt einige mögliche Interpretationen, hier eine Auswahl davon:
\begin{\whichenum}
\item Imperative Interpretation: Eine Zuweisung wie in $C$. \u{a} hat nach der Ausführung des Ausdrucks den Wert der Summe der Werte von \u{b} und \u{c}.
Andere Variante: Der Wert von \u{a} ist nach der Zuweisung die Zeichenfolge \u{b + c}.
\item Funktionale Interpretation: Eine Funktion \u{a} wird mit den 4 Parametern \u{= b + c} aufgerufen.
\item Logische Interpretation: Ein logischer Ausdruck, beispielsweise ist der Ausdruck Wahr wenn der Wert von \u{a} gleich der Summe der Werte von \u{b} und \u{c} ist.
Andere Variante: Der Wert von 2 der 3 Variablen ist bekannt, der Wert der 3. Variable wird so festgelegt.
\end{\whichenum}
Wir sehen anhand dieses Beispiels, dass es wichtig ist exakt zu definieren wie ein Ausdruck
zu interpretieren ist.
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}
In funktionalen Programmiersprachen besteht jedes Programm aus einer oder mehreren
Funktionen.
\begin{defn}[Funktion]\label{defn:Funktion}
Eine Funktion ist eine Relation zwischen einer Menge $A$ und einer Menge $B$.
Jedem Element aus der Menge $A$ wird genau ein Element der Menge $B$ zugeordnet.
Das heißt: Für jeden möglichen Eingabewert gibt es genau einen Ausgabewert.
\end{defn}

\section{Sprache $\lng{A}$ - einfache arithmetische Ausdrücke}
Arithmetische Ausdrücke sind Funktionen. Wir können beispielsweise die Funktionen
Addition, Subtraktion und Multiplikation von zwei Zahlen in $\R$ definieren mit einem
Eingabewert in $\R \times \R$ und einen Ausgabewert in $\R$. Auch die Division
können wir als Funktion definieren von $\R \times \R \setminus \gbr{0}$ (Division durch $0$ schließen
wir damit aus, da die Division in diesem Fall nicht als Funktion definiert ist) auf Ausgabewerte in $\R$.

\begin{defn}
Die Sprache $\lng{A}$ definieren wir mit Alphabet $\Sigma=\gbr{\u{0},\ldots,\u{9},\u{(},\u{)},\u{+}}$.
Zwecks Einfachheit definieren wir Ziffern (D, digits) und Zahlen:
\begin{\whichitem}
\item $\lng{A}_D = \gbr{\u{0},\ldots,\u{9}}$
\item ZAHL $= (\lng{A}_D \setminus \gbr{\u{0}} \lng{A}_D^*) \cup \gbr{\u{0}}$
\end{\whichitem}
Wir definieren die Sprache $A$ nun nicht mehr über eine Grammatik sondern durch eine induktive Beschreibung (Basisfall und allgemeine Fälle):
\begin{\whichenum}
\item ZAHL$\subset \lng{A}$
\item Wenn $x,y \in \lng{A}$, dann ist auch $\u{(} x \u{)} \u{+} \u{(} y \u{)} \in \lng{A}$.
\end{\whichenum}
\end{defn}
An dieser Stelle sei noch einmal darauf hingewiesen, dass wir $x,y$ nicht unterstreichen dürfen, da sie keine Sprachelemente sind sondern
Platzhalter, mathematisch würde man sie auch als Variablen bezeichnen.
\ifthenelse{\boolean{long}}{}{\begin{comment}}
Wir wollen nun mit unserer Sprache $\lng{A}$ Ausdrücke berechnen können.
Dazu definieren wir eines unserer mächtigsten Werkzeuge im zweiten Kapitel:
Die Interpretationsfunktion $I$ (auch genannt Semantikfunktion).
Man kann sich diese Funktion vorstellen wie einen Interpreter einer Scriptsprache:
Wir geben ein Programm ein und führen es aus, abhängig vom aktuellen Zustand liefert
uns der Interpreter ein Ergebnis zurück.
Genau so soll unsere Interpretationsfunktion arbeiten.
Wir erwarten einen Eingabewert aus $\lng{A}$ und bilden auf $\N_0$ ab, d.h. geben
einen Wert aus $\N_0$ zurück.
Genau wie die Syntax werden wir nun die Semantik induktiv durch die Interpretationsfunktion definieren.
\ifthenelse{\boolean{long}}{}{\end{comment}}
\begin{defn}
Die Semantik der Sprache $\lng{A}$ definieren wir durch:
\begin{\whichenum}
\item $I_{\lng{A}}(x) = \sbr{x}$ wenn $x \in \lng{A}_N$. $x$ ist dabei eine Zeichenkette im Programm, $\sbr{x}$ die
entsprechende Repräsentation in $\N_0$.
\item $I_{\lng{A}}(\u{(}x\u{)+(}y\u{)})=I_{\lng{A}}(x) + I_{\lng{A}}(y)$ wenn $x,y \in \lng{A}$.
\end{\whichenum}
\end{defn}
\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Das Programm $\u{((10)+(9))+(3)}$ (vgl. Vorlesungsskriptum S.45) können wir wie folgt interpretieren:
\begin{align*}
I_{\lng{A}}(\u{((10)+(9))+(3)}) &= I_{\lng{A}}(\u{(10)+(9)}) + I_{\lng{A}}(\u{3}) \tag{entsprechend 2. Fall der Definition} \\
                      &= I_{\lng{A}}(\u{10}) + I_{\lng{A}}(\u{9}) + 3 \tag{beim $\u{3}$ nun der 1. Fall der Definition} \\
                      &= 10 + 9 + 3 = 22
\end{align*}
\end{bsp}
Auch hier sehen wir wieder deutlich die Unterscheidung zwischen Zeichenketten im Programmcode (unterstrichen) und den Werten
auf der semantischen Ebene (nicht unterstrichen). Um den Unterschied weiter zu verdeutlichen
definieren wir nun die Sprache der einfachen arithmetischen Ausdrücke von Binärzahlen $\lng{B}$.

Die Sprache $\lng{B}$ definieren wir mit Alphabet $\Sigma=\gbr{\u{0},\u{1},\u{(},\u{)},\u{+}}$.
\begin{\whichenum}
\item $(\u{1} \gbr{\u{0},\u{1}}^*) \cup \gbr{\u{0}} \subset \lng{B}$
\item Wenn $x,y \in \lng{B}$, dann ist auch $\u{(} x \u{)} \u{+} \u{(} y \u{)} \in \lng{B}$.
\end{\whichenum}
Die Semantik der Sprache $\lng{B}$ definieren wir durch:
\begin{\whichenum}
\item $I_{\lng{B}}(x) = \sbr{x}$ wenn $x \in \lng{B}_N$. $\sbr{x} \in \N_0$ ist nun die
durch die Binärzahl (exakt: die Binärziffernfolge) dargestellte Zahl auf semantischer Ebene, in diesem Fall also im mathematischen Sinne.
\item $I(\u{(}x\u{)+(}y\u{)})=I(x) + I(y)$ wenn $x,y \in \lng{B}$.
\end{\whichenum}
\begin{bsp}
$I(\u{1001})=9$ aber $\u{1001}\neq 9$.

Betrachten wir das Beispiel wie zuvor, nun in Binärdarstellung $\u{((1010)+(1001))+(11)}$: 
\begin{align*}
I_{\lng{B}}(\u{((1010)+(1001))+(11)}) &= I_{\lng{B}}(\u{(1010)+(1001)}) + I_{\lng{B}}(\u{11})\\
                      &= I_{\lng{B}}(\u{1010}) + I_{\lng{B}}(\u{1001}) + 3\\
                      &= 10 + 9 + 3 = 22
\end{align*}
\end{bsp}

Wir versuchen nun der Sprache $\lng{A}$ eine zweite Funktion, die Multiplikation hinzuzufügen.

Die Sprache $\lng{D}$ ist definiert durch:
\begin{\whichenum}
\item ZAHL$\subset \lng{D}$
\item $\u{(} x \u{)} \u{+} \u{(} y \u{)} \in \lng{D}$, wenn $x,y \in \lng{D}$.
\item $\u{(} x \u{)} \u{*} \u{(} y \u{)} \in \lng{D}$, wenn $x,y \in \lng{D}$.
\end{\whichenum}
Die Semantik der Sprache $\lng{D}$ definieren wir durch:
\begin{\whichenum}
\item $I_{\lng{D}}(x) = \sbr{x}$ wenn $x \in \lng{D}_N$.
\item $I_{\lng{D}}(\u{(}x\u{)+(}y\u{)})=I_{\lng{D}}(x) + I_{\lng{D}}(y)$ wenn $x,y \in \lng{A}$.
\item $I_{\lng{D}}(\u{(}x\u{)*(}y\u{)})=I_{\lng{D}}(x) \cdot I_{\lng{D}}(y)$ wenn $x,y \in \lng{A}$.
\end{\whichenum}

Würden wir die Klammern aus der Definition $I_{\lng{D}}$ weglassen, so würde es sich nicht um eine Funktion handeln.
Wir nennen diese Sprache ohne Klammern $I_{\lng{D}'}$ um anhand dieser Beweise über die Interpretationsfunktion zu üben.

\begin{beweis}
Laut Definition~\ref{defn:Funktion} ist eine Relation eine Funktion wenn es für jeden möglichen Eingabewert genau einen Ausgabewert gibt.

Möchte man eine Aussage über ``alle'' Werte bzw. ``jeden'' Wert widerlegen so gestaltet sich ein Beweis oft relativ einfach. In so einem
Fall müssen wir nur ein Gegenbeispiel finden, denn dann gilt die Aussage offensichtlich nicht für alle Werte, wir haben ja einen gefunden
für den es nicht gilt. Diese Beweistechnik nennt man ``Beweis durch Widerspruch''.

Wir werden nun zeigen, dass $I_{\lng{D}'}$ für das Programm \u{1+2*3} verschiedene Interpretationsmöglichkeiten zulässt da nicht festgelegt
ist ob der 2. oder 3. Fall der Definition die höhere Priorität hat.
\begin{align*}
I_{\lng{D}'}(\u{1+2*3}) &= I_{\lng{D}'}(\u{1+2}) \cdot I_{\lng{D}'}(\u{3}) \tag{3. Fall der Definition} \\
&= (I_{\lng{D}'}(\u{1}) + I_{\lng{D}'}(\u{2})) \cdot 3 \tag{2. Fall der Definition} \\
&= (1+2) \cdot 3 = 3 \cdot 3 = 9 \\
I_{\lng{D}'}(\u{1+2*3}) &= I_{\lng{D}'}(\u{1}) + I_{\lng{D}'}(\u{2*3}) \tag{2. Fall der Definition} \\
&= 1 + (I_{\lng{D}'}(\u{2}) \cdot I_{\lng{D}'}(\u{3})) \tag{3. Fall der Definition} \\
&= 1 + (2 \cdot 3) = 1 + 6 = 7 \neq 9
\end{align*}
Wir haben gezeigt, dass für einen Eingabewert mehrere unterschiedliche Ausgabewerte möglich sind.
Folglich gibt es nicht für \u{jeden} Eingabewert \u{genau einen} Ausgabewert, daher kann $I_{\lng{D}'}$ keine Funktion sein. \hfill $\Box$
\end{beweis}
Syntax und Semantik müssen also eindeutig sein, damit die Interpretationsfunktion eine Funktion ist.
\ifthenelse{\boolean{long}}{}{\end{comment}}
\section{Sprache $\lng{V}$ - arithmetische Ausdrücke mit Variablen}
Wir erweitern die Sprache $\lng{A}$ durch Variablen und schaffen so eine mächtigere Sprache $\lng{V}$.
Um mit Variablen umgehen zu können brauchen wir nun einerseits eine Menge zulässiger
Variablennamen und andererseits eine Funktion die von Variablennamen auf eine Wertemenge der semantischen Ebene (z.B. $\N_0$) abbildet.
Die Menge der zulässigen Variablennamen nennen wir IVS (Individuenvariablensymbole).
\begin{defn}
Zwecks Einfachheit erlauben wir nur wenige Variablennamen und definieren daher
\[\text{IVS} = \gbr{\u{a},\u{b},\ldots,\u{z}} \cup \gbr{\u{x1},\u{x2},\ldots}.\]
\end{defn}
Die Funktion die von Variablennamen auf eine Wertemenge abbildet nennen wir $\omega$-Environment, (Variablen-)Umgebung.
Man kann sich diese Funktion auch als Tabelle vorstellen bzw. in einem Interpreter als Tabelle implementieren.
\begin{defn}
Die Menge aller Environments sei
\[\text{ENV} = \gbr{x | x \in \P\rbr{\text{IVS} \times \Lambda}}, \forall \rbr{a,b},\rbr{a',b'} \in x : \quad a = a' \to b = b',\]
das heißt, die Potenzmenge des kartesischen Produkts der Variablennamen und der Werte, wobei es keine Tupel gibt, bei denen der gleiche Variablenname mit unterschiedlichen Werten verknüpft ist.
\end{defn}
$\text{IVS} \times \Lambda$ wäre hierbei die Menge die alle möglichen Variablennamen mit allen möglichen Werten verknüpft. Die Potenzmenge dieser Menge enthält alle Teilmengen, das heißt auch jedes spezielle Environment (und ungültige) ist in dieser Menge enthalten. Mit der zusätzlichen Bedingung am Ende der Definition wird die Einschränkung auf gültige Environments getroffen.
Für die Sprache $\lng{V}$ ist $\Lambda=\N_0$.
\begin{defn}
Die Syntax der Sprache $\lng{V}$ ist definiert durch:
\begin{\whichenum}
\item ZAHL$\subset \lng{V}$
\item IVS$\subset \lng{V}$
\item $\u{(} x \u{)} \u{+} \u{(} y \u{)} \in \lng{V}$, wenn $x,y \in \lng{V}$.
\end{\whichenum}
\end{defn}
Die Interpretation eines Programms hängt nun nicht mehr allein vom Programm selbst ab,
sondern auch von den Werten der Variablen im $\omega$-Environment.
\begin{defn}
Die Interpretationsfunktion $I_{\lng{V}}: \text{ENV}\times\lng{V} \to \Lambda$
weist jedem Tupel aus Environment und Programm einen Wert in $\Lambda$ zu.
\begin{\whichenum}
\item $I_{\lng{V}}(\omega,k) = \sbr{k}$ wenn $k \in \text{ZAHL}$, $\omega \in \text{ENV}$.
\item $I_{\lng{V}}(\omega,v) = \omega(v)$ wenn $v \in \text{IVS}$, $\omega \in \text{ENV}$.
\item $I_{\lng{V}}(\u{(}x\u{)+(}y\u{)})=I_{\lng{V}}(\omega,x) + I_{\lng{V}}(\omega,y)$ wenn $x,y \in \lng{V}$, $\omega \in \text{ENV}$.
\end{\whichenum}
\end{defn}
\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Gegeben sei das Environment $\omega(\u{x})=0$, $\omega(\u{y})=1$, $\omega(\u{z})=2$.
Interpretieren Sie das Programm $\u{(((x)+(2))+(y))+(z)}$.
\begin{align*}
I_{\lng{V}}(\omega,\u{(((x)+(2))+(y))+(z)}) &= I_{\lng{V}}(\omega,\u{((x)+(2))+(y)}) + I_{\lng{V}}(\omega,\u{z}) \\
&= I_{\lng{V}}(\omega,\u{(x)+(2)}) + I_{\lng{V}}(\omega,\u{y}) + \omega(\u{z}) \\
&= I_{\lng{V}}(\omega,\u{x}) + I_{\lng{V}}(\omega,\u{2}) + \omega(\u{y}) + 2 \\
&= \omega(\u{x}) + 2 + 1 + 2 \\
&= 0 + 2 + 1 + 2 = 5
\end{align*}
Beachten Sie auch, dass nach wie vor $I_{\lng{V}}(\omega,\u{2})=2$.
Es ist ein bei den Übungen weit verbreiteter Fehler $I_{\lng{V}}(\omega,\u{2}) = \omega(\u{2})$ zu schreiben. Die Interpretationsfunktion wurde so nicht definiert und
außerdem ist $\u{2}$ auch kein gültiger Variablenname.
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

\section{Datentypen}
Bisher haben wir eine Sprache nur für einen Datentypen definiert. Dieser war implizit in der
Definition der Sprache drin (beispielsweise die natürlichen Zahlen). Derartige Definitionen
erlauben kein Ersetzen des Datentyps ohne die Definition der Sprache wesentlich zu überarbeiten.
Da wir dies aber häufig wollen werden wir nun zuerst Datentypen auf der semantischen Ebene
und anschließend die Repräsentation von Datentypen auf der syntaktischen Ebene definieren.
\begin{defn}[Datentyp]
Ein Datentyp ist ein Tupel $\Psi=\rbr{A,F,P,C}$ mit
\begin{\whichitem}
\item $A$: Grundmenge (Wertebereich)
\item $F$: Menge von Funktionen $f_i: A^{k_i} \to A^{l_i}$.

$f_i$ ist die $i$-te Funktion in der Menge, $k_i$ die Dimension vom Urbild (Dimension des Inputs, Anzahl der Funktionsargumente) und $l_i$
die Dimension vom Bild der $i$-ten Funktion (Dimension des Outputs, Anzahl der Funktionsrückgabewerte).
\item $P$: Menge von Prädikaten $p_i: A^{k_i} \to \gbr{T,F}$.

$p_i$ ist die $i$-te Funktion in der Menge und $k_i$ die Dimension vom Urbild (Dimension des Inputs, Anzahl der Funktionsargumente) der $i$-ten Funktion.
\item $C$: Menge von Konstanten $c_i$ wobei $c \subseteq A$.
\end{\whichitem}
Die Mengen $F^{\Sigma}$, $P^{\Sigma}$ und $C^{\Sigma}$ enthalten die entsprechenden Symbole für die syntaktische Repräsentation:
\begin{\whichitem}
\item Funktionssymbole $F^{\Sigma}$: je ein Symbol $f^{\Sigma}_i$ (z.B. Name der Funktion) für jede Funktion $f_i$
\item Prädikatensymbole $P^{\Sigma}$: je ein Symbol $p^{\Sigma}_i$ (z.B. Name des Prädikats) für jedes Prädikat $p_i$
\item Konstantensymbol $C^{\Sigma}$: je ein Symbol $c^{\Sigma}_i$ (z.B. ausgeschriebene Form der Konstante) für jede Konstante $c_i$
\end{\whichitem}
\end{defn}

Konstanten sind eigentlich nur spezielle Funktionen ($0$ Argumente) und wir unterscheiden nur zwecks Übersicht.
\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Definieren Sie den Datentyp Integer mit Funktionen für Addition, Subtraktion und Multiplikation sowie Prädikaten für
``kleiner'' und Gleichheit.

\textit{Lösung:}
Im Fall der Integer ist die Definition der Funktionen und Prädikate trivial, da
alle Funktionen und Prädikate durch die entsprechenden Operationen auf den ganzen Zahlen $\Z$ definiert sind.
Daher genügt es zu definieren welche Funktion welcher Operation entspricht.
\begin{\whichitem}\label{defn:integer}
\item Grundmenge $A=\Z$
\item Funktionen $f_1: +$, $f_2: -$, $f_3: *$

Die Funktionen $+, -, *$ sind auf $\Z$ definiert.
Auf der syntaktischen Ebene definieren wir: $f^{\Sigma}_1: {\tuplus}$, $f^{\Sigma}_2: {\tuminus}$, $f^{\Sigma}_3: {\tumult}$.
\item Prädikate $p_1: <$, $p_2: =$

Die Prädikate $<, =$ sind auf $\Z$ definiert.
Syntaktische Ebene: $p^{\Sigma}_1: {\tult}$, $p^{\Sigma}_2: {\tueq}$.
\item Konstanten $c_1: 0$, $c_2: 1$

Syntaktische Ebene: $c^{\Sigma}_1: {\tunull}$, $c^{\Sigma}_2: {\tueins}$.
\end{\whichitem}
Hinzunahme von Division ist problematisch $/$ da das Ergebnis nicht unbedingt $\in A$ ist.
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}
Wir können bei der Definition eines Datentyps oft (z.B. bei den verschiedenen Datentypen für Zahlen) auf bekannte algebraische Strukturen (Halbgruppen, etc.) zurückgreifen.
\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Definieren Sie den Datentyp String mit der Funktion Konkatenation und dem Prädikat ``Präfix''.

\textit{Lösung:} Hier können wir nun nicht mehr auf eine vorhandene mathematische Definition
zurückgreifen.
\begin{\whichitem}
\item Grundmenge $A=V^*$ mit $V$ einem endlichen Alphabet $\gbr{v_1,\ldots,v_n}$ (z.B. dem ASCII-Alphabet).
\item Funktionen
\begin{\whichenum}
\item $f_1: \circ$ (Konkatenation)
\begin{\whichitem}
\item Wenn $x \in V^*$ ist, dann ist $x \circ \varepsilon = x$
\item Wenn $x \in V^*$ und $a \in V$ ist, dann ist $x \circ a = xa$
\item Wenn $x,y \in V^*$ und $a \in V$ ist, dann ist $x \circ (y \circ a) = (x \circ y) \circ a$
\end{\whichitem}
\end{\whichenum}
\item Prädikate
\begin{\whichenum}
\item $p_1: <<$ (Präfix)
\begin{\whichitem}
\item Wenn $x \in V^*$ ist, dann ist $\varepsilon << x$
\item Wenn $x \in V^*$ ist, dann ist $x << x$
\item Wenn $x$ Präfix von $y$ ist, dann ist $x$ auch Präfix von $y \circ z$
($(x << y) \ra (x << (y \circ z))$).
\end{\whichitem}
\end{\whichenum}
\item Konstanten $c_i: v_i$, $c_{n+1}: \varepsilon$ (eine Konstante für jeden Buchstaben des Alphabets und $\varepsilon$ für den Leerstring).
\end{\whichitem}
Die syntaktische Ebene überlassen wir dem Leser.
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}
\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Definieren Sie den Datentyp des binären Stacks mit Funktionen um Elemente auf den Stack zu legen oder herunterzunehmen, sowie
Prädikaten zur Überprüfung des obersten Elementes.

\textit{Lösung:}
\begin{\whichitem}
\item Grundmenge $A=\gbr{0,1}^* \cup \gbr{\varepsilon}$, d.h. Ziffernfolgen aus $0$ und $1$ oder $\varepsilon$ (leerer Stack).
\item Funktionen
\begin{\whichenum}
\item $f_1: \text{add0}$ liefert den Stack mit einer $0$ daraufgelegt.
\begin{\whichitem}
\item $\text{add0}(\varepsilon)=0$
\item $\text{add0}(x)=0x$ (mit $x \neq \varepsilon$)
\end{\whichitem}
\item $f_2: \text{add1}$ liefert den Stack mit einer $1$ daraufgelegt.
\begin{\whichitem}
\item $\text{add1}(\varepsilon)=1$
\item $\text{add1}(x)=1x$ (mit $x \neq \varepsilon$)
\end{\whichitem}
\item $f_3: \text{sub}$ liefert den Stack ohne das oberste Element.
\begin{\whichitem}
\item $\text{sub}(\varepsilon)=\varepsilon$
\item $\text{sub}(ax)=x$ (mit $a \neq \varepsilon$)
\end{\whichitem}
\end{\whichenum}
\item Prädikate
\begin{\whichenum}
\item $p_1: \text{ist0?}$ testet ob das oberste Element $0$ ist.
\begin{\whichitem}
\item $\text{ist0?}(x) \Lra \texists z : x = 0z$
\end{\whichitem}
\item $p_2: \text{ist1?}$ testet ob das oberste Element $1$ ist.
\begin{\whichitem}
\item $\text{ist1?}(x) \Lra \texists z : x = 1z$
\end{\whichitem}
\item $p_3: \text{istLeer?}$ testet ob das oberste Element $\varepsilon$ ist.
\begin{\whichitem}
\item $\text{istLeer?}(x) \Lra x = \varepsilon$
\end{\whichitem}
\end{\whichenum}
\item Konstanten $c_1: \varepsilon$.
\end{\whichitem}
Auf der syntaktischen Ebene werden die gleichen Bezeichnungen wie auf der semantischen Ebene verwendet.
\end{bsp}

\begin{bsp}
Berechnen Sie den Ausdruck $\text{add0}(\text{add1}(\text{sub}(011)))$ im Datentyp des binären Stacks.

\textit{Lösung:}
\[\text{add0}(\text{add1}(\text{sub}(011))) = \text{add0}(\text{add1}(11)) = \text{add0}(111) = 0111\]
\begin{align*}
\text{ist0?}(0111)&=T \\
\text{ist1?}(0111)&=F \\
\text{istLeer?}(0111)&=F
\end{align*}
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

\section{Sprache der Terme $\lng{T}$}
Wir müssen nun um den Datentyp verwenden zu können eine grundlegende Sprache 
definieren die diesen Datentyp verwendet. Auf dieser Sprache können dann weitere Sprachen
aufgebaut werden.
\begin{defn}[Sprache der Terme $\lng{T}$]\label{defn:semt}
Sei $\Psi=\rbr{A,F,P,C}$ ein Datentyp.
Das Alphabet $\Sigma$ ist dann eine Vereinigung aus den Mengen der
\begin{\whichitem}
\item IVS (Individuenvariablensymbole)
\item Funktionssymbole $F^{\Sigma}$
\item Prädikatensymbole $P^{\Sigma}$
\item Konstantensymbol $C^{\Sigma}$
\item $\u{(}$,$\u{)}$ und $\u{,}$
\item Sondersymbole (Keywords): \u{if}, \u{then}, \u{else}, \u{begin}, \u{end}, $\ldots$
\end{\whichitem}
Die Syntax von $\lng{T} \subseteq \Sigma$ über einem beliebigen Datentypen ist dann definiert durch:
\begin{\whichenum}
\item $C^{\Sigma} \subseteq \lng{T}$, d.h. Konstantensymbole sind Terme
\item $\text{IVS} \subseteq \lng{T}$, d.h. Individuenvariablensymbole sind Terme
\item Wenn $f^{\Sigma}_i$ ein $n$-stelliges Funktionssymbol ist und $t_1,\ldots,t_n$ Terme,
dann ist auch $f^{\Sigma}_i\u{(}t_1\u{,}\ldots\u{,}t_n\u{)}$ ein Term (Unterstreichungen beachten!).
\end{\whichenum}
Die Semantik von $\lng{T}$ definieren wir durch die Interpretationsfunktion $I_{\lng{T}}: \text{ENV} \times \lng{T} \to A$.
\begin{\whichenum}
\item $I_{\lng{T}}(\omega,c^{\Sigma}_i)=c_i$ mit $c_i \in C$ (Semantik-Ebene), $c^{\Sigma}_i \in C^{\Sigma}$ (Syntax-Ebene) und $\omega \in \text{ENV}$.
\item $I_{\lng{T}}(\omega,v)=\omega(v)$ mit $v \in \text{IVS}$ und $\omega \in \text{ENV}$.
\item $I_{\lng{T}}(\omega,f^{\Sigma}_i\u{(}t_1\u{,}\ldots\u{,}t_n\u{)})=f_i(I_{\lng{T}}(\omega,t_1),\ldots,I_{\lng{T}}(\omega,t_n))$ mit $f_i \in F$ (Semantik-Ebene), $f^{\Sigma}_i \in F^{\Sigma}$ (Syntax-Ebene) und $\omega \in \text{ENV}$.
\end{\whichenum}
\end{defn}

\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Führen Sie das Programm \u{plus(plus(x,y),plus(eins,z))} mit dem Environment $\omega(\u{x})=0$, $\omega(\u{y})=1$, $\omega(\u{z})=2$ aus.

\textit{Lösung:}
\begin{align*}
&\quad \I{T}{\omega}{plus(plus(x,y),plus(eins,z))}\\
&= \I{T}{\omega}{plus(x,y)} + \I{T}{\omega}{plus(eins,z)} \\
&= \rbr{\I{T}{\omega}{x} + \I{T}{\omega}{y}} + \rbr{\I{T}{\omega}{eins} + \I{T}{\omega}{z}} \\
&= \omega(\u{x}) + \omega(\u{y}) + 1 + \omega(\u{z}) \\
&= 0+1+1+2 = 4
\end{align*}
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

Laut Definition von $\lng{T}$ gibt es nur die Konstanten $0$ und $1$. Variablen können natürlich jeden beliebigen Wert in $\Z$ annehmen.
Es kann aber auch gezeigt werden, dass alle ganzen Zahlen durch einen variablenfreien Term dargestellt werden können. Daher ist es nicht nötig, dass es für jede Zahl eine Konstante gibt.
Terme sind rekursiv definiert. Die \textbf{vollständige Induktion} (ab hier auch Induktion genannt) ist die übliche Beweistechnik für Beweise über rekursive bzw. rekursiv definierte Ausdrücke.

\ifthenelse{\boolean{long}}{}{\begin{comment}}
Versuchen wir zunächst die \textbf{vollständige Induktion} ganz allgemein zu verstehen.
\begin{bsp}
Dazu macht es Sinn sich ein kleines Beispiel zu überlegen. Dazu definieren wir, dass folgende Aussagen wahr sind:
\begin{\whichitem}
\item Aussage $A$: An Tag $n$ regnet es genau dann, wenn es an Tag $n-1$ geregnet hat.
\item Aussage $T_1$: An Tag $1$ regnet es.
\end{\whichitem}
Wir sehen sofort, dass es wohl immer regnet.
Dies wollen wir nun auch beweisen: An jedem Tag regnet es. Man könnte auch schreiben:
An jedem Tag $i$ regnet es. Zwecks Übersichtlichkeit bezeichnen wir die Aussage ``Es regnet an Tag $i$'' mit $T_i$
und können dann sehr kompakt schreiben: $\tforall i: T_i$.

Wir erbringen nun zunächst den Beweis für die ersten Tage einzeln.
\begin{\whichitem}
\item Tag $1$: $T_1$ war schon gegeben und ist wahr.
\item Tag $2$: $A \wedge T_1 \ra T_2$
\item Tag $3$: $A \wedge T_1 \wedge T_2 \ra T_3$
\item Tag $4$: $A \wedge T_1 \wedge T_2 \wedge T_3 \ra T_4$
\end{\whichitem}
Wir würden so allerdings nie fertig werden da es in unserem Beispiel so viele Tage wie natürliche Zahlen gibt.
Was uns aber auffällt: Für den Beweis von jedem $T_i$ müssen wir auf den Beweis für $T_{i-1}$ zurückgreifen.
Eine Induktion verkürzt hier unsere Arbeit wesentlich.
Wir zeigen einfach die Korrektheit für einen allgemeinen Fall (z.B. $T_{n+1}$) aus seinen Vorgängern ($T_{i}$ mit $i \leq n$) folgt.

Dazu müssen wir zunächst allgemein beschreiben was für jedes einzelne Element bis zu einem gewissen (beliebigen) $n$ gilt: $\tforall i \leq n: T_i$. Wir nennen dies \textbf{Induktionshypothese}.
Diese Aussage ist allerdings nicht bewiesen, es ist lediglich eine Annahme darüber was für jedes Element gilt.

Den entscheidenden Schritt im Beweis führen wir jetzt durch, indem wir von $n$ auf das nachfolgende Element (in unserem Fall $n+1$) springen und zeigen, dass der Beweis für das nachfolgende
Element erbracht werden kann. Dabei müssen wir unbedingt die Annahme (die Induktionshypothese) verwenden, sonst handelt es sich bei unserem Beweis nicht um eine vollständige
Induktion und sehr wahrscheinlich ist der Beweis dann auch nicht fehlerfrei.

Wir wollen nun also beweisen: $\tforall i \leq n+1: T_i$.
Laut Induktionshypothese gilt: $\tforall i \leq n: T_i$.
Es bleibt daher nur zu beweisen übrig: $T_{n+1}$.
Dazu versuchen wir nun umzuformen:
\begin{align*}
T_{n+1} \lra T_{n} \tag{laut Aussage $A$}
\end{align*}
$T_n$ gilt laut Induktionshypothese, der Beweis ist damit erbracht: Wir haben bewiesen, dass $\tforall i: T_i$.
Diesen Teil der Induktion nennen wir \textbf{Induktionsschritt}.
Meist ist hier mehr Arbeit erforderlich als bei diesem kleinen Beispiel. Wir werden das auch beim nächsten Beispiel sehen.
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

Halten wir fest: Die \textbf{vollständige Induktion} besteht aus 3 Einzelschritten: In der \textbf{Induktionsbasis} werden ein oder mehrere Basisfälle direkt bewiesen.
In der \textbf{Induktionshypothese} wird versucht eine allgemeine Aussage (eine Hypothese) zu treffen von der angenommen wird, dass sie bis zum $n$-ten Fall gilt.
Im \textbf{Induktionsschritt} gehen wir einen Schritt weiter, also in den Fall $n+1$ und versuchen diesen zu beweisen. Hier muss unbedingt auf die Induktionshypothese zurückgegriffen
werden, sonst wurde keine vollständige Induktion durchgeführt. Um eine Induktion durchführen zu können müssen die Elemente unbedingt aufzählbar sein
(d.h. man muss eine eindeutige Reihenfolge/Sortierung für die Elemente angeben können).

\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Wir wollen zeigen, dass alle ganzen Zahlen durch einen variablenfreien Term dargestellt werden können.

Bevor wir die Induktion durchführen versuchen wir ein Muster zu erkennen.
\begin{align*}
\I{T}{\omega}{null}&=0 \tag{trivial}\\
\I{T}{\omega}{eins}&=1 \tag{trivial}\\
\I{T}{\omega}{plus(eins,eins)}&=2 \tag{eine Addition}\\
\I{T}{\omega}{plus(eins,plus(eins,eins))}&=3 \tag{verschachtelte Addition}
\end{align*}
Wir erkennen das Muster: Alle Zahlen $\in \N$ können durch rekursive Addition von 1 dargestellt werden.
Diese Rekursion kann beliebig tief werden, wir bauen sie allerdings immer in der gleichen Form (nur rechter Ast rekursiv).
Wir definieren uns einen Platzhalter $t_k$ um beliebig lange solcher Ausdrücke einfach darzustellen:
\begin{align*}
t_2 &= \u{plus(eins,eins)} \\
t_3 &= \u{plus(eins,plus(eins,eins))} \\
&\vdots \\
t_{k+1} &= \u{plus(eins,}t_{k}\u{)} \\
\end{align*}
$k$ entspricht der Anzahl der ${\tueins}$ im Ausdruck.

\begin{\whichitem}
\item \textbf{Induktionsbasis:} \quad
In der Induktionsbasis beweisen wir einen oder mehrere Basisfälle.
Das sind in unserem Fall die beiden Konstanten sowie der Fall $t_2$:
\begin{align*}
\I{T}{\omega}{null}&=0 \\
\I{T}{\omega}{eins}&=1 \\
\Iu{T}{\omega}{t_2}&=\I{T}{\omega}{plus(eins,eins)}=2\\
\end{align*}
\item \textbf{Induktionshypothese:} \quad $\Iu{T}{\omega}{t_n}=n$
\item \textbf{Induktionsschritt:}\\
\begin{align*}
\Iu{T}{\omega}{t_{n+1}}&=n+1 \tag{Einsetzen von $t_{n+1}$}\\
\Iu{T}{\omega}{\u{plus(eins,}t_{n}\u{)}}&=n+1 \tag{Interpretationsfunktion durchführen}\\
+\rbr{\Iu{T}{\omega}{{\tueins}},\Iu{T}{\omega}{t_{n}}}&=n+1 \\
+\rbr{1,\Iu{T}{\omega}{t_{n}}}&=n+1
\intertext{\textbf{Unter Verwendung der Induktionshypothese (d.h. wir setzen die Induktionshypothese $\Iu{T}{\omega}{t_n}=n$ ein):}}
+\rbr{1,n}&=n+1
\end{align*}
Damit ist der Beweis erbracht.
\end{\whichitem}
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

\section{Sprache der Konditionale COND ($\lng{C}$)}
Wir hatten in der Sprache der Terme $\lng{T}$ noch nicht die Möglichkeit Prädikate zu nutzen obwohl Datentypen über
Prädikate verfügen. Dazu definieren wir die Sprache der Konditionale \textbf{COND}. Wir schreiben in diesem Skriptum großteils
nur $\lng{C}$ zwecks Übersichtlichkeit - $\lng{C}$ gesprochen ``COND''.
\begin{defn}[Die Sprache COND ($\lng{C}$)]\label{defn:semcond}
Die Syntax von $\lng{C}$ ist wie folgt definiert:
\begin{\whichenum}
\item $\lng{T} \subseteq \lng{C}$, d.h. alle Terme sind Konditionale.
\item Wenn $p^{\Sigma}_i$ ein $n$-stelliges Prädikatensymbol ist und $u_1,\ldots,u_n,t_1,t_2$ Konditionale,
dann ist auch \; ${\tuif} p_i^{\Sigma}\u{(}u_1\u{,}\ldots\u{,}u_n\u{)}{\tuthen} t_1 {\tuelse} t_2$ \; ein Konditional.
\end{\whichenum}
Die Semantikfunktion $I_{\lng{C}}$ definieren wir durch:
\begin{\whichenum}
\item $\Iu{C}{\omega}{t} = \Iu{T}{\omega}{t}$, wenn $t \in \lng{T}$ und $\omega \in \text{ENV}$.
\item Für jedes Prädikat $p_i$ gilt:
\begin{\whichitem}
\item Wenn $p_i\rbr{\Iu{C}{\omega}{u_1},\ldots,\Iu{C}{\omega}{u_n}}=T$, dann gilt:
\[\Iu{C}{\omega}{{\tuif} p_{i}^{\Sigma} \u{(} u_1\u{,}\ldots\u{,}u_n\u{)}{\tuthen} t_1 {\tuelse} t_2}=\Iu{C}{\omega}{t_1}\]
\item Sonst ist $p_i\rbr{\Iu{C}{\omega}{u_1},\ldots,\Iu{C}{\omega}{u_n}}=F$ und dann gilt:
\[\Iu{C}{\omega}{{\tuif} p_{i}^{\Sigma} \u{(} u_1\u{,}\ldots\u{,}u_n\u{)}{\tuthen} t_1 {\tuelse} t_2}=\Iu{C}{\omega}{t_2}\]
\end{\whichitem}
\end{\whichenum}
\end{defn}

\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Interpretieren Sie \u{if ist0?(sub(x)) then add0(x) else sub(x)} in $\lng{C}$ über dem Datentyp der binären Stacks mit dem Environment $\omega(\u{x})=101$.

Wir beginnen wie auch schon in der Sprache der Terme.
\begin{align*}
&\quad \I{C}{\omega}{if ist0?(sub(x)) then add0(x) else sub(x)}
\intertext{\textcolor{darkblue}{NR: An dieser Stelle müssen wir nun eine Nebenrechnung (NR) durchführen um zu bestimmen ob der $then$- oder der $else$-Zweig ausgeführt wird.\newline
$\I{C}{\omega}{ist0?(sub(x))}$
$=\text{ist0?}\rbr{\I{C}{\omega}{sub(x)}}$
$=\text{ist0?}\rbr{\text{sub}\rbr{\I{C}{\omega}{x}}}$ \newline
$\underbrace{=\text{ist0?}\rbr{\text{sub}\rbr{\I{T}{\omega}{x}}}}_{\text{trivial \tto meist nicht angeschrieben}}$
$=\text{ist0?}\rbr{\text{sub}\rbr{\omega\rbr{\u{x}}}}$
$=\text{ist0?}\rbr{\text{sub}\rbr{101}}$
$=\text{ist0?}\rbr{01} = T$}}
&= \I{C}{\omega}{add0(x)} \tag{folgt aus der NR} \\
&= \text{add0}\rbr{\I{C}{\omega}{x}} = \text{add0}\rbr{\omega\rbr{\u{x}}} = \text{add0}\rbr{101} = 0101
\end{align*}
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

Bei Verschachtelungen von Prädikaten in $\lng{C}$ ist zu beachten, dass Prädikate direkt kein Teil der Sprache sind.
Daher ist auch der Ausdruck \u{if ist0?(ist1?(x)) then x else add0(x)} nicht in $\lng{C}$!
Allerdings ist \u{if ist0?(if ist1?(x) then 110 else 010) then x else add0(x)} in $\lng{C}$.

\section{Rekursionen - Sprache der Ausdrücke EXP ($\lng{E}$)}
Bisher war es nicht möglich Funktionen (insbesondere rekursive) zu definieren. Wir müssen das Konzept ``Funktionsname''
ähnlich wie die Variablennamen (IVS, Individuenvariablensymbole) zuerst einführen.
Der Wert der einem Funktionsnamen zugeordnet wird ist dabei ein Programm.
Wir definieren nun die Sprache \textbf{EXP} ($\lng{E}$). Wie schon bei \textbf{COND} kürzen wir auch hier \textbf{EXP} durch $\lng{E}$ ab - $\lng{E}$ gesprochen ``EXP''.

\begin{defn}
Die Menge der Funktionsvariablensymbole (FVS) enthält ``Namen'' aller Funktionen.
\end{defn}

\begin{defn}
Die Menge der Funktionsenvironments bezeichnen wir mit FENV.
Jedes Funktionsenvironment $\delta: \text{FVS} \to \lng{E}$ liefert für ein Funktionsvariablensymbol die
Implementation in EXP ($\lng{E}$) zurück. $\delta\u{X}$ bezeichne die Implementation der Funktion mit dem Namen $\u{X}$.
\end{defn}

Es muss unbedingt unterschieden werden zwischen
\begin{\whichitem}
\item Funktionen des Datentyps ($+$, $-$, etc.) sowie den dazugehörigen Funktionssymbolen (\u{plus}, \u{minus}, etc.)
\item und ``benutzerdefinierten Funktionen'', d.h. Unterprogramme die auch in der Sprache implementiert werden. Diese bezeichnen wir als Funktionsvariablensymbole.
\end{\whichitem}

\begin{defn}[Syntax von EXP ($\lng{E}$)]
Die Syntax von $\lng{E}$ ist definiert wie folgt:
\begin{\whichitem}
\item $\lng{C} \subseteq \lng{E}$, d.h. alle Konditionale sind Ausdrücke (d.h. $\in \lng{E}$).
\item Wenn $f$ eine $n$-stellige Funktionenvariable ($\in$ FVS)
ist und $t_1,\ldots,t_n$ sind Ausdrücke (d.h. $\in \lng{E}$),
dann ist $f\u{(}t_1\u{,}\ldots\u{,}t_n\u{)}$ ein Ausdruck (d.h. $\in \lng{E}$).
\end{\whichitem}
\end{defn}

Eine Funktion kann also über die Parameter hinaus keine weiteren Variablen haben.
Beim Funktionsaufruf werden Parameter übergeben. Wir behandeln dabei zunächst nur call-by-value.
Hierbei werden die als Parameter übergebenen Ausdrücke \textbf{vor} Ausführung der Funktion
berechnet (interpretiert) und die Variablen der Funktion werden in einem neuen Variablenenvironment
auf die entsprechenden Werte initialisiert.

\begin{defn}[Semantik von EXP ($\lng{E}$)]\label{defn:semexp}
Die Semantikfunktion $I_{\lng{E}}$ definieren wir durch:
\begin{\whichenum}
\item $\Iu{E}{\delta,\omega}{c} = \Iu{C}{\omega}{c}$, wenn $c \in \lng{C}$ und $\omega \in \text{ENV}$.
\item $\Iu{E}{\delta,\omega}{F\u{(}t_1\u{,}\ldots\u{,}t_n\u{)}}$ mit $F \in \text{FENV}$. Funktionsaufruf mit call-by-value:
\begin{\whichenum}
\item Definiere $\omega'$ als neues Environment mit $\omega'(x_i)=\Iu{E}{\delta,\omega}{t_i}$ (für $1 \leq i \leq n$) wobei $x_i$
die Parameter der Funktion $\delta F$ sind. Im Normalfall ist $x_i=\u{xi}$, d.h. $x_1=\u{x1}$, $x_2=\u{x2}$, usw.
\item $\Iu{E}{\delta,\omega}{F\u{(}t_1\u{,}\ldots\u{,}t_n\u{)}}=\Iu{E}{\delta,\omega'}{\delta F}$
\end{\whichenum}
\end{\whichenum}
\end{defn}

\begin{anm}
Mit den Definitionen \ref{defn:semt}, \ref{defn:semcond} und \ref{defn:semexp} halten wir zwecks Übersicht fest:
\begin{\whichenum}
\item $I_{\lng{T}}(\omega,c^{\Sigma}_i)=c_i$ mit $c_i \in C$ (Semantik-Ebene), $c^{\Sigma}_i \in C^{\Sigma}$ (Syntax-Ebene) und $\omega \in \text{ENV}$.
\item $I_{\lng{T}}(\omega,v)=\omega(v)$ mit $v \in \text{IVS}$ und $\omega \in \text{ENV}$.
\item $I_{\lng{T}}(\omega,f^{\Sigma}_i\u{(}t_1\u{,}\ldots\u{,}t_n\u{)})=f_i(I_{\lng{T}}(\omega,t_1),\ldots,I_{\lng{T}}(\omega,t_n))$ mit $f_i \in F$ (Semantik-Ebene), $f^{\Sigma}_i \in F^{\Sigma}$ (Syntax-Ebene) und $\omega \in \text{ENV}$.
\item $\Iu{E}{\delta,\omega}{t} = \Iu{T}{\omega}{t}$, wenn $t \in \lng{T}$ und $\omega \in \text{ENV}$ und $\delta \in \text{FENV}$.
\item Für jedes Prädikat $p_i$ gilt:
\begin{\whichitem}
\item Wenn $p_i\rbr{\Iu{C}{\omega}{u_1},\ldots,\Iu{C}{\omega}{u_n}}=T$, dann gilt:
\[\Iu{C}{\omega}{{\tuif} p_{i}^{\Sigma} \u{(} u_1\u{,}\ldots\u{,}u_n\u{)}{\tuthen} t_1 {\tuelse} t_2}=\Iu{C}{\omega}{t_1}\]
\item Sonst ist $p_i\rbr{\Iu{C}{\omega}{u_1},\ldots,\Iu{C}{\omega}{u_n}}=F$ und dann gilt:
\[\Iu{C}{\omega}{{\tuif} p_{i}^{\Sigma} \u{(} u_1\u{,}\ldots\u{,}u_n\u{)}{\tuthen} t_1 {\tuelse} t_2}=\Iu{C}{\omega}{t_2}\]
\end{\whichitem}
\item $\Iu{E}{\delta,\omega}{F\u{(}t_1\u{,}\ldots\u{,}t_n\u{)}}$ mit $F \in \text{FENV}$. Funktionsaufruf mit call-by-value:
\begin{\whichenum}
\item Definiere $\omega'$ als neues Environment mit $\omega'(x_i)=\Iu{E}{\delta,\omega}{t_i}$ (für $1 \leq i \leq n$) wobei $x_i$
die Parameter der Funktion $\delta F$ sind. Im Normalfall ist $x_i=\u{xi}$, d.h. $x_1=\u{x1}$, $x_2=\u{x2}$, usw.
\item $\Iu{E}{\delta,\omega}{F\u{(}t_1\u{,}\ldots\u{,}t_n\u{)}}=\Iu{E}{\delta,\omega'}{\delta F}$
\end{\whichenum}
\end{\whichenum}
\end{anm}

Wir definieren eine Funktion \u{func} in $\lng{E}$ durch $\delta\tu{func}=\u{\ldots}$.
Im Rahmen der Übung ist es auch zulässig bei der Funktionsdefinition explizit andere Parameter anzugeben ($\delta\tu{func(x,v)}=\u{\ldots}$)
um die Parameternamen festzulegen. In unserem Fall wäre dann $x_1 = \u{x}$ und $x_2 = \u{v}$.
Die Komplexität des $\lng{E}$-Interpreters wird dadurch nicht wesentlich beeinflusst.

\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Interpretieren Sie das Programm \u{F(sub(x))} in $\lng{E}$ über dem Datentyp der Stacks, wobei $\delta\u{F}=$\u{if ist0?(x1) then sub(x1) else add1(x1)} und
$\omega(\u{x})=100$.

\textit{Lösung:}
\begin{align*}
\I{E}{\delta,\omega}{F(sub(x))}
\intertext{\textcolor{darkblue}{Neues Environment (NE): $\omega'(\tu{x1})=\I{E}{\delta,\omega}{\text{sub}(x)}=\text{sub}(\I{E}{\delta,\omega}{x})=\text{sub}(\omega(\u{x}))=\text{sub}(100)=00$}}
&= \I{E}{\delta,\omega'}{\text{if ist0?(x1) then sub(x1) else add1(x1)}} \\
\intertext{\textcolor{darkblue}{NR: $\I{E}{\delta,\omega'}{\text{ist0?(x1)}}=\text{ist0?}(\I{E}{\delta,\omega'}{x1})=\text{ist0?}(\omega'(\tu{x1}))=\text{ist0?}(00)=T$}}
&= \I{E}{\delta,\omega'}{\text{sub(x1)}} \\
&= \text{sub}(\I{E}{\delta,\omega'}{\text{x1}}) \\
&= \text{sub}(\omega'(\tu{x1})) \\
&= \text{sub}(00) \\
&= 0
\end{align*}
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

Im Vorlesungsskriptum findet sich außerdem auf Seite 59 die Definition für Funktionsaufrufe mittels Call-by-Name sowie obiges Beispiel für Call-by-Name durchgerechnet.
Außerdem wird demonstriert, dass es Funktionen gibt (die in Teilbereichen undefiniert sind) die je nach Verfahren ein unterschiedliches Verhalten zeigen.

\ifthenelse{\boolean{long}}{}{\begin{comment}}
Wir haben bereits die vollständige Induktion kennengelernt. Mittels vollständiger Induktion können wir auch die Korrektheit von Programmen in $\lng{E}$
beweisen.

\begin{bsp}
Gegeben sei der Datentyp der nicht-negativen Integer der nur die Funktionen Inkrement um 1 (\u{inc}) und Dekrement um 1 (\u{dec}), sowie die bereits bekannten
Prädikate \u{eq?} und \u{gt?}. Implementieren Sie die Addition zweier Zahlen in $\lng{E}$.

\textit{Lösung:}
Um eine Funktion zu schreiben macht es oft Sinn sich zunächst mathematisch aufzuschreiben wie die Funktion definiert ist.
\[\text{add}(x,y)=\begin{cases} y & \text{ wenn } x=0 \\ \text{add}(\text{dec}(x),\text{inc}(y)) & \text{sonst}\end{cases}\]
Aus dieser Darstellung kann direkt das $\lng{E}$ Programm implementiert werden:
\[\delta\tu{add}=\tu{if eq?(x,0) then y else add(dec(x),inc(y))} \qquad \text{(mit Parametern $x_1 = \u{x}, x_2 = \u{y}$)}\]
Um einen Beweis zu führen brauchen wir nun noch ein ``Golden Device'', eine mathematische Funktion die das geforderte Verhalten korrekt berechnet. Diese
kann für den Beweis einfach als gegeben angenommen werden.
In unserem Fall ist es der Operator $+$ über $\N_0$.

Zu zeigen ist also: $\tforall \omega: \I{E}{\delta,\omega}{add(x,y)}=\omega(\u{x})+\omega(\u{y})$

\begin{\whichitem}
\item Induktionsbasis: Sei $\omega(\u{x})=0$ und $\omega(\u{y})=m$ ($m$ beliebig).
\begin{align*}
\I{E}{\delta,\omega}{add(x,y)}
\intertext{\textcolor{darkblue}{Neues Environment? $\omega'(\u{x})=\omega(\u{x})$, $\omega'(\u{y})=\omega(\u{y})$, d.h. es wäre $\omega'=\omega$. Es gilt Gleichheit, daher ist es völlig egal
ob hier $\omega'$ eingeführt wird oder nicht. Dieser Fall tritt immer dann auf wenn die Aufruf-Parameter gleich den Funktionsparametern aus der Definition sind. In diesen Fällen führen wir in diesem Skriptum zwecks Übersichtlichkeit keine neuen Environments ein.}}
&= \I{E}{\delta,\omega}{\text{if eq?(x,0) then y else add(dec(x),inc(y))}}
\intertext{\textcolor{darkblue}{NR: $\I{E}{\delta,\omega}{\text{eq?}(x,0)}=\text{eq?}(\I{E}{\delta,\omega}{x},\I{E}{\delta,\omega}{0})=\text{eq?}(\omega(\u{x}),0)=\text{eq?}(0,0)=T$}}
&= \I{E}{\delta,\omega}{y} \\
&= \omega(\u{y}) \\
&= m \\
&= \omega(\u{x})+\omega(\u{y})
\end{align*}
Der Basisfall wurde damit bewiesen.
\item Induktionshypothese: $\I{E}{\delta,\omega}{add(x,y)}=\omega(\u{x})+\omega(\u{y})$ gilt für $\omega(\u{x})=n$ und $\omega(\u{y})=m$ ($m$ beliebig)
\item Induktionsschritt: Zu zeigen ist $\I{E}{\delta,\omega}{add(x,y)}=\omega(\u{x})+\omega(\u{y})$ für $\omega(\u{x})=n+1$ und $\omega(\u{y})=m$ ($m$ beliebig):
\begin{align*}
\I{E}{\delta,\omega}{add(x,y)}
&= \I{E}{\delta,\omega}{\text{if eq?(x,0) then y else add(dec(x),inc(y))}}
\intertext{\textcolor{darkblue}{NR: $\I{E}{\delta,\omega}{\text{eq?}(x,0)}=\text{eq?}(\I{E}{\delta,\omega}{x},\I{E}{\delta,\omega}{0})=\text{eq?}(\omega(\u{x}),0)=\text{eq?}(n+1,0)=F$, da $n \in \N_0$ und folglich $n+1 \geq 1$}}
&= \I{E}{\delta,\omega}{\text{add(dec(x),inc(y))}}
\intertext{\textcolor{darkblue}{NE: $\omega'(\u{x})=\I{E}{\delta,\omega}{\text{dec(x)}}=\text{dec}(\I{E}{\delta,\omega}{\text{x}})=\text{dec}(\omega(\u{x}))=\text{dec}(n+1)=n$, \newline
               $\omega'(\u{y})=\I{E}{\delta,\omega}{\text{inc(y)}}=\text{inc}(\I{E}{\delta,\omega}{\text{y}})=\text{inc}(\omega(\u{y}))=\text{inc}(m)=m+1$}}
&= \I{E}{\delta,\omega'}{\text{add(x,y)}} \tag{Wir ersetzen zunächst nur $\omega$!} \\
\intertext{Für diesen Fall ($\omega'(\u{x})=n$) gilt die Induktionshypothese!
Wir sehen, dass der obige Aufruf der Interpretationsfunktion exakt so aussieht wie in der Induktionshypothese.
Unter Verwendung der Induktionshypothese (d.h. wir setzen die Induktionshypothese $\I{E}{\delta,\omega}{add(x,y)}=\omega(\u{x})+\omega(\u{y})$ ein):}
&= \omega'(\u{x})+\omega'(\u{y}) \\
&= n+m+1 \\
&= \omega(\u{x})+\omega(\u{y})
\end{align*}
Wir haben also bewiesen $\I{E}{\delta,\omega}{add(x,y)} = \ldots = \omega(\u{x})+\omega(\u{y})$. Das ist exakt
die Gleichheit die wir für den Beweis der Korrektheit zeigen mussten.
\end{\whichitem}

Im obigen Beweis haben wir folgende Umformung durchgeführt:
\begin{align*}
&\quad \I{E}{\delta,\omega}{\text{add(dec(x),inc(y))}}
\intertext{\textcolor{darkblue}{NE: $\omega'(\u{x})=n$, $\omega'(\u{y})=m+1$}}
&= \I{E}{\delta,\omega'}{\text{add(x,y)}}
\end{align*}
Diese Abkürzung ist im Rahmen der Übung durchaus erwünscht.
Sie ist zulässig da die Interpretationsfunktion $I_{\lng{E}}$ entsprechend
definiert wurde.
Laut Definition ist
\[\I{E}{\delta,\omega'}{\text{add(x,y)}}=\I{E}{\delta,\omega'}{\text{if eq?(x,0) then y else add(dec(x),inc(y))}}.\]
Daher können wir umformen:
\begin{align*}
&\quad \I{E}{\delta,\omega}{\text{add(dec(x),inc(y))}} \\
&= \I{E}{\delta,\omega'}{\text{if eq?(x,0) then y else add(dec(x),inc(y))}} \\
&= \I{E}{\delta,\omega'}{\text{add(x,y)}}
\end{align*}
Dies ist exakt die Umformung die wir gemacht haben.

Ein Vorteil in dieser Variante liegt darin, dass einfach gesehen werden kann wenn die Induktionshypothese
zutrifft.
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

\ifthenelse{\boolean{long}}{}{\begin{comment}}
Die Sprache $\lng{E}$ ist von uns konstruiert und in der Praxis nicht relevant.
Funktionale Sprachen (Lisp, Haskell, OCaml, etc.) im Allgemeinen sind allerdings durchaus relevant - und auch angenehmer zu verwenden als $\lng{E}$.
Dadurch, dass wir $\lng{E}$ genau verstehen wird es uns auch leicht fallen neue Sprachen zu erlernen.
Hier ein Vergleich eines rekursiven Programms zum Ermitteln der $n$-ten Fibonacci-Zahl in verschiedenen funktionalen Sprachen:
\begin{\whichitem}
\item EXP:
\begin{verbatim}
fib(n) = if eq?(n,0) then 1
         else plus(fib(minus(n,1)),fib(minus(n,2)))
\end{verbatim}
\item Erlang:
\begin{verbatim}
fib(0) -> 1;
fib(n) -> fib(n-1) + fib(n-2)
\end{verbatim}
\item Haskell:
\begin{verbatim}
fib 0 = 1
fib n = fib(n-1) + fib(n-2)
\end{verbatim}
\end{\whichitem}
\ifthenelse{\boolean{long}}{}{\end{comment}}

\section{Datentyp der Listen $\mathcal{L}$}
Der Datentyp der Listen kommt in vielen Sprachen vor. Wir verwenden dazu die Darstellung mit eckigen Klammern und groß geschriebenen
Wörtern ([ APE BEE CAT ]).
\begin{defn}[Atom]
Etwas ist ein Atom genau dann wenn kein [ und kein ] darin vorkommt.

Listenelemente die keine ``echten'' Listen sind (APE, BEE, CAT, etc.) werden Atom genannt.
Alle anderen Listen sind keine Atome.
\end{defn}
\begin{defn}[Datentyp der Listen $\mathcal{L}$] \quad
\begin{\whichitem}
\item Grundmenge $A$:
\begin{\whichitem}
\item ATOM $\subseteq A$, d.h. alle Atome sind Listen
\item $[ ] \subseteq A$, d.h. die leere Liste ist eine Liste
\end{\whichitem}
\item Funktionen
\begin{\whichenum}
\item $f_1: \text{first}$ (liefert das erste Element einer Liste)
\begin{\whichitem}
\item Wenn $a \in \text{ATOM}$, dann ist $\text{first}(a)=[ ]$.
\item $\text{first}([ ])=[ ]$.
\item Wenn $\tforall i, \quad 1 \leq i \leq k: \quad \ell_i \in L$, dann ist $\text{first}([ \ell_1 \ldots \ell_k ])=\ell_1$
\end{\whichitem}
\item $f_2: \text{rest}$ (liefert die Liste ohne das erste Element)
\begin{\whichitem}
\item Wenn $a \in \text{ATOM}$, dann ist $\text{rest}(a)=[ ]$.
\item $\text{rest}([ ])=[ ]$.
\item Wenn $\ell \in L$, dann ist $\text{rest}([\ell])=[ ]$
\item Wenn $\tforall i, \quad 1 \leq i \leq k: \quad \ell_i \in L$ und $k > 1$, dann ist $\text{rest}([ \ell_1 \ell_2 \ldots \ell_k ])=[ \ell_2 \ldots \ell_k ]$
\end{\whichitem}
\item $f_3: \text{build}$ (nimmt 2 Listen entgegen und fügt die eine als erste Element in die andere ein)
\begin{\whichitem}
\item Wenn $a \in \text{ATOM}$ und $\ell \in L$, dann ist $\text{build}(\ell,a)=a$.
\item Wenn $\ell \in L$, $\text{build}(\ell,[ ])=[\ell]$.
\item Wenn $\ell \in L$ und $\tforall i, \quad 1 \leq i \leq k: \quad \ell_i \in L$, dann ist $\text{build}(\ell,[ \ell_1 \ldots \ell_k ])=[ \ell \ell_1 \ldots \ell_k ]$
\end{\whichitem}
\end{\whichenum}
\item Prädikate
\begin{\whichenum}
\item $p_1: \text{atom?}$
\begin{\whichitem}
\item $\text{atom?}(x)=T$, genau dann wenn $x \in \text{ATOM}$
\end{\whichitem}
\item $p_2: \text{eq?}$
\begin{\whichitem}
\item $\text{eq?}(x,y)=T$, genau dann wenn $x=y$
\end{\whichitem}
\end{\whichenum}
\item Konstanten: Die leere Liste ($c_1=[]$ mit $c_1^\Sigma=\tu{nil}$), sowie je eine Konstante für jedes Atom
\end{\whichitem}
Die Symbole auf der syntaktischen Ebene werden entsprechend der zuvor verwendeten Bezeichnungen gewählt (z.B. $p_1^{\Sigma}=\tu{atom?}$).
\end{defn}

\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Definieren Sie eine Funktion \u{second} in $\lng{E}$ welches immer das 2. Element einer Liste zurückliefert.
Interpretieren Sie ihre Funktion für den Parameter [ FIR SEC THI ].

\textit{Lösung:} Zuerst trennen wir das erste Element von der Liste, anschließend
geben wir das neue erste Element zurück:
\[\delta\tu{second}=\tu{first(rest(x))}\]
\begin{align*}
&\quad \I{E}{\delta,\omega}{\text{second(x)}}
\intertext{\textcolor{darkblue}{Environment bleibt gleich: $\omega(\u{x})=\text{[ FIR SEC THI ]}$}}
&= \I{E}{\delta,\omega}{\text{first(rest(x))}} \\
&= \text{first}\rbr{\I{E}{\delta,\omega}{\text{rest(x)}}} \\
&= \text{first}\rbr{\text{rest}\rbr{\I{E}{\delta,\omega}{\text{x}}}} \\
&= \text{first}\rbr{\text{rest}\rbr{\omega(\tu{x})}} \\
&= \text{first}\rbr{\text{rest}\rbr{\text{[ FIR SEC THI ]}}} \\
&= \text{first}\rbr{\text{[ SEC THI ]}} \\
&= \text{SEC}
\end{align*}
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}
\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Definieren Sie eine Funktion \u{reverse} in $\lng{E}$ welches eine Liste elementweise umgedreht zurückliefert.
Interpretieren Sie ihre Funktion für den Parameter [ FIR SEC THI ].

\textit{Lösung:} Bei der Konstruktion rekursiver Programme versuchen wir meist von einem Basisfall ausgehend
komplexere Fälle aufzubauen.
Ein Basisfall ist für uns ein Atom, die leere Liste und Listen mit genau einem Element. Diese können wir unverändert zurückliefern.
Andernfalls haben wir eine Liste mit mehreren Elementen. Dann werden wir das erste (bzw. das letzte) Element von der Liste entfernen und
eine neue Liste bauen die aus dem entfernten Element und dem umgedrehten Rest der Liste besteht. Wir wählen die Variante mit dem ersten Element
da der Datentyp der Listen dies einfach ermöglicht. Um das letzte Element zu erhalten müssten wir den Datentyp modifizieren oder ein Programm schreiben
welches nur das letzte Element zurückliefert.

Wir halten also fest:
\[\text{reverse}(x) = \begin{cases}
x & x \in \text{ATOM} \\
x & x = \ebr{} \\
x & x = \ebr{\ell} \\
\ebr{ \ell_{k} \text{reverse}\rbr{[ \ell_1 \ldots \ell_{k-1} ]}} & x = \ebr{\ell_1 \ldots \ell_{k-1} \ell_k}
\end{cases}\]

Dies können wir wieder nicht direkt als $\lng{E}$-Programm umschreiben. Wir haben in der Sprache keine Möglichkeit
auf das letzte Element einer Liste zuzugreifen. Wir könnten dafür eine Funktion $\delta\tu{last}$ schreiben oder
direkt durch eine Rekursion über die Liste iterieren bis zum letzten Element und
in einem zweiten Parameter (``Akkumulator'') die Liste aufbauen.
\begin{align*}
\delta\tu{reverse(x)}&=\tu{if atom?(x) then x else reverse2(x,nil)} \\
\delta\tu{reverse2(x,y)}&=\tu{if eq?(x,nil) then y else reverse2(rest(x),build(first(x),y))}
\end{align*}
Verhält sich dieses Programm wie beabsichtigt?
\begin{align*}
&\quad \I{E}{\delta,\omega}{reverse(x)} \\
&= \I{E}{\delta,\omega}{if atom?(x) then x else reverse2(x,nil)}
\intertext{\textcolor{darkblue}{NR: $\I{E}{\delta,\omega}{atom?(x)}=\text{atom?}\rbr{\I{E}{\delta,\omega}{x}}=\text{atom?}\rbr{\omega(\tu{x})}$\newline$=\text{atom?}\rbr{\text{[ FIR SEC THI ]}}=F$}}
&= \I{E}{\delta,\omega}{reverse2(x,nil)}
\intertext{\textcolor{darkblue}{NE: $\omega'(\tu{x})=\I{E}{\delta,\omega}{x}=\omega(\tu{x})=\text{[ FIR SEC THI ]}$, $\omega'(\tu{y})=\I{E}{\delta,\omega}{nil}=\text{[]}$}}
&= \I{E}{\delta,\omega'}{reverse2(x,y)} \\
&= \I{E}{\delta,\omega'}{if eq?(x,nil) then y else reverse2(rest(x),build(first(x),y))}
\intertext{\textcolor{darkblue}{NR: $\I{E}{\delta,\omega'}{eq?(x,nil)}=\text{eq?}\rbr{\I{E}{\delta,\omega'}{x},\I{E}{\delta,\omega'}{nil}}=\text{eq?}\rbr{\omega'(\tu{x}),[]}$\newline$=\text{eq?}\rbr{\text{[ FIR SEC THI ]},[]}=F$}}
&= \I{E}{\delta,\omega'}{reverse2(rest(x),build(first(x),y))}
\intertext{\textcolor{darkblue}{NE: $\omega''(\tu{x})=\I{E}{\delta,\omega'}{rest(x)}=\text{rest}\rbr{\I{E}{\delta,\omega'}{x}}=\text{rest}\rbr{\omega'(\tu{x})}$\newline$=\text{rest}\rbr{\text{[ FIR SEC THI ]}}=\text{[ SEC THI ]}$, \newline
               $\omega''(\tu{y})=\I{E}{\delta,\omega'}{build(first(x),y)}=\text{build}\rbr{\I{E}{\delta,\omega'}{first(x)},\I{E}{\delta,\omega'}{y}}$\newline$=\text{build}\rbr{\text{first}\rbr{\I{E}{\delta,\omega'}{x}},\I{E}{\delta,\omega'}{y}}=\text{build}\rbr{\text{first}\rbr{\omega'(\tu{x})},\omega'(\tu{y})}$\newline$=\text{build}\rbr{\text{first}\rbr{\text{[ FIR SEC THI ]}},[]}=\text{build}\rbr{\text{FIR},[]}=\text{[ FIR ]}$}}
&= \I{E}{\delta,\omega''}{reverse2(x,y)} \\
&= \I{E}{\delta,\omega''}{if eq?(x,nil) then y else reverse2(rest(x),build(first(x),y))}
\intertext{\textcolor{darkblue}{NR: $\I{E}{\delta,\omega''}{eq?(x,nil)}=\text{eq?}\rbr{\I{E}{\delta,\omega''}{x},\I{E}{\delta,\omega''}{nil}}$\newline$=\text{eq?}\rbr{\omega''(\tu{x}),[]}=\text{eq?}\rbr{\text{[ SEC THI ]},[]}=F$}}
&= \I{E}{\delta,\omega''}{reverse2(rest(x),build(first(x),y))}
\intertext{\textcolor{darkblue}{NE: $\omega'''(\tu{x})=\I{E}{\delta,\omega''}{rest(x)}=\text{rest}\rbr{\I{E}{\delta,\omega''}{x}}=\text{rest}\rbr{\omega''(\tu{x})}$\newline$=\text{rest}\rbr{\text{[ SEC THI ]}}=\text{[ THI ]}$, \newline
               $\omega'''(\tu{y})=\I{E}{\delta,\omega''}{build(first(x),y)}=\text{build}\rbr{\I{E}{\delta,\omega''}{first(x)},\I{E}{\delta,\omega''}{y}}$\newline$=\text{build}\rbr{\text{first}\rbr{\I{E}{\delta,\omega''}{x}},\I{E}{\delta,\omega''}{y}}=\text{build}\rbr{\text{first}\rbr{\omega''(\tu{x})},\omega''(\tu{y})}$\newline$=\text{build}\rbr{\text{first}\rbr{\text{[ SEC THI ]}},\text{[ FIR ]}}=\text{build}\rbr{\text{SEC},\text{[ FIR ]}}=\text{[ SEC FIR ]}$}}
&= \I{E}{\delta,\omega'''}{reverse2(x,y)} \\
&= \I{E}{\delta,\omega'''}{if eq?(x,nil) then y else reverse2(rest(x),build(first(x),y))}
\intertext{\textcolor{darkblue}{NR: $\I{E}{\delta,\omega'''}{eq?(x,nil)}=\text{eq?}\rbr{\I{E}{\delta,\omega'''}{x},\I{E}{\delta,\omega'''}{nil}}$\newline$=\text{eq?}\rbr{\omega'''(\tu{x}),[]}=\text{eq?}\rbr{\text{[ THI ]},[]}=F$}}
&= \I{E}{\delta,\omega'''}{reverse2(rest(x),build(first(x),y))}
\intertext{\textcolor{darkblue}{NE: $\omega''''(\tu{x})=\I{E}{\delta,\omega'''}{rest(x)}=\text{rest}\rbr{\I{E}{\delta,\omega'''}{x}}=\text{rest}\rbr{\omega'''(\tu{x})}$\newline$=\text{rest}\rbr{\text{[ THI ]}}=\text{[ ]}$, \newline
               $\omega''''(\tu{y})=\I{E}{\delta,\omega'''}{build(first(x),y)}=\text{build}\rbr{\I{E}{\delta,\omega'''}{first(x)},\I{E}{\delta,\omega'''}{y}}$\newline$=\text{build}\rbr{\text{first}\rbr{\I{E}{\delta,\omega'''}{x}},\I{E}{\delta,\omega'''}{y}}=\text{build}\rbr{\text{first}\rbr{\omega'''(\tu{x})},\omega'''(\tu{x})}$\newline$=\text{build}\rbr{\text{first}\rbr{\text{[ THI ]}},\text{[ SEC FIR ]}}=\text{build}\rbr{\text{THI},\text{[ SEC FIR ]}}=\text{[ THI SEC FIR ]}$}}
&= \I{E}{\delta,\omega''''}{reverse2(x,y)} \\
&= \I{E}{\delta,\omega''''}{if eq?(x,nil) then y else reverse2(rest(x),build(first(x),y))}
\intertext{\textcolor{darkblue}{NR: $\I{E}{\delta,\omega''''}{eq?(x,nil)}=\text{eq?}\rbr{\I{E}{\delta,\omega'''}{x},\I{E}{\delta,\omega'''}{nil}}$\newline$=\text{eq?}\rbr{\omega'''(\tu{x}),[]}=\text{eq?}\rbr{[],[]}=T$}}
&= \I{E}{\delta,\omega''''}{y} \\
&= \omega''''(\tu{y}) \\
&= \text{[ THI SEC FIR ]}
\end{align*}
Das Programm verhält sich für diesen Fall wie gewünscht. Um zu beweisen, dass es sich immer korrekt verhält müssten wir einen Beweis führen.
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Zeigen oder widerlegen Sie: Es gibt ein Programm in EXP über den Datentyp der Listen,
welches die maximale Verschachtelungs-Tiefe einer Liste berechnet.
Greifen Sie dafür auf die in der Vorlesung besprochene Codierung der natürlichen 
Zahlen zurück.
Beispielsweise würde der Aufruf mit dem Input \verb|[]| als Resultat \verb|[]| berechnen,
der Aufruf mit dem Input \verb|[ a [] [ [] b ] [] ]|
würde als Resultat \verb|[[[]]]| berechnen.

Wenn die Aussage wahr ist, ist eine Implementation anzugeben
und die Korrektheit dieser zu zeigen.

\textit{Lösung:} (Aus der Übung 2011) Wir haben im Tutorium das Programm zur Berechnung der maximalen Verschachtelungstiefe wie folgt implementiert:

\begin{align*}
\delta\u{\text{depth}}&=\u{\text{if atom?(first(x)) then depth(rest(x))}} \\ &\quad \u{\text{else if eq?(x,nil) then nil}} \\ &\quad \u{\text{else max(build(depth(first(x)),nil),depth(rest(x)))}} \\
\delta\u{\text{max}}&=\u{\text{if eq?(x,nil) then y}} \\ &\quad \u{\text{else if eq?(y,nil) x}} \\ &\quad \u{\text{else build(max(rest(x),rest(y)),nil)}}
\end{align*}

Die Korrektheit von $\delta\u{\text{max}}$ wurde im Tutorium per Induktion gezeigt, dem geneigten Leser ist es überlassen diesen Beweis selbst durchzuführen.

Wir haben $f_{d}(\omega(\u{x}))$ als ``Golden Device'' definiert, eine Funktion ($L \to \N$) die die gesuchte Funktion korrekt berechnet.

Bei einer Induktion wollen wir im Allgemeinen von einem Fall auf den nächsten bzw. nachfolgenden schließen.
In unserem Fall ist das gar nicht so leicht, denn die Listen sind beliebig verschachtelt.
Wenn wir z.B. die Listenlänge $n$ verwenden, könnte im rekursiven Aufruf die Länge der Liste $\text{first}(\omega(\u{x}))$ größer als $n$ sein.
Ein Umweg über die Listentiefe $t$ ist eher umständlich.
In so einem Fall ist es recht hilfreich sich zu überlegen ob es ein anderes Kriterium gibt, mit welchem wir beide
Rekursionsaufrufe auf die Hypothese zurückführen können.

Daher erfolgt der Beweis für $\delta\u{\text{depth}}$ mit $\text{atom?}(\text{first}(\omega(\u{x})))=F$ per Induktion nach der Gesamtanzahl $\abs{\omega(\u{x})}$ der Elemente in $\omega(\u{x})$.
Über diese Hilfsfunktion können wir relativ einfach nach dem Schema arbeiten welches in den anderen Beispielen bereits vorkam.

Wir definieren:
\[\abs{\omega(\u{x})} = \begin{cases}1 & \text{eq?}(\omega(\tu{x}),[]) \\
                                     1 & \text{atom?}(\omega(\tu{x}),[]) \\
                                     \abs{\text{first}(\omega(\tu{x}))}+\abs{\text{rest}(\omega(\u{x}))}  & \text{sonst}\end{cases}\]

Die Idee - mit der wir die Induktion durchführen - könnte man schreiben als:
Wenn $\delta\u{\text{depth}}$ korrekt ist für $\abs{\omega(\u{x})}=n$ ($n \in \N$),
dann ist $\delta\u{\text{depth}}$ auch korrekt für $\abs{\omega(\u{x})}=n+1$.

Induktionshypothese:
\[\forall \omega(\u{x}) \in L, \quad \abs{\omega(\u{x})} \leq n : \quad I(\delta,\omega,\tu{depth(x)}) = f_{d}(\omega(\u{x}))\]

Induktionsbasis:
\[\omega(\u{x}) \in L, \abs{\omega(\u{x})} = 1\]
\begin{align*}
&&\quad I(\delta,\omega,&\u{\text{depth(x)}}) \\
&&=I(\delta,\omega,&\u{\text{if atom?(first(x)) then depth(rest(x))}} \\ &&&\u{\text{else if eq?(x,nil) then nil}} \\ &&&\u{\text{else max(build(depth(first(x)),nil),depth(rest(x)))}})
\intertext{\textcolor{darkblue}{NR: $I(\delta,\omega,\u{\text{atom?(first(x))}})=\text{atom?}(I(\delta,\omega,\u{\text{first(x)}}))=\text{atom?(first}(I(\delta,\omega,\u{\text{x}})))$\newline$=\text{atom?(first([]))}=\text{atom?([])}=F$ (da dies zu einer Rekursion führen würde und folglich kein Basisfall ist.)}}
&&=I(\delta,\omega,&\u{\text{if eq?(x,nil) then nil}} \\ &&&\u{\text{else max(build(depth(first(x)),nil),depth(rest(x)))}})
\intertext{\textcolor{darkblue}{Da $\abs{\omega(\u{x})}=1$ ist muss $\omega(\u{x})=\text{[]}$ sein.}}
&&=I(\delta,\omega,&\u{\text{nil}})=\text{[]}=f_{d}(\text{[]})=f_{d}(\omega(\u{x}))
\end{align*}

Induktionsschritt:
\[\omega(\u{x}) \in L, \abs{\omega(\u{x})} = n+1, n \in \N\]
\begin{align*}
&&\quad I(\delta,\omega,&\u{\text{depth(x)}}) \\
&&=I(\delta,\omega,&\u{\text{if atom?(first(x)) then depth(rest(x))}} \\ &&&\u{\text{else if eq?(x,nil) then nil}} \\ &&&\u{\text{else max(build(depth(first(x)),nil),depth(rest(x)))}})
\end{align*}
Fallunterscheidung nach $atom?(first(\omega(\tu{x})))$:
\begin{itemize}
\item Fall $atom?(first(\omega(\tu{x})))=T$
\begin{align*}
\intertext{\textcolor{darkblue}{NR: $I(\delta,\omega,\u{\text{atom?(first(x))}})=\text{atom?}(I(\delta,\omega,\u{\text{first(x)}}))=\text{atom?(first}(I(\delta,\omega,\u{\text{x}})))=T$ (siehe Fallunterscheidung)}}
&&=I(\delta,\omega,&\u{\text{depth(rest(x))}})
\intertext{\textcolor{darkblue}{$\omega'(\tu{x})=I(\delta,\omega,\u{\text{rest(x)}})=\text{rest}(I(\delta,\omega,\u{\text{x}}))=\text{rest}(\omega(\u{x}))$. Die Gesamtanzahl der Elemente dieser Liste ist mindestens um $1$ geringer, da $\text{first}(x)$ aus der Liste entfernt wurde.}}
&&=I(\delta,\omega',&\u{\text{depth(x)}})
\intertext{\textcolor{darkblue}{Für dieses Environment gilt die Induktionshypothese. Wir wenden die Induktionshypothese daher an:}}
&&=&f_{d}(\omega'(\tu{x})) \\
&&=&f_{d}(\text{rest}(\omega(\u{x})))
\intertext{\textcolor{darkblue}{Was korrekt ist, da das Atom $first(\omega(\tu{x}))$ die Listentiefe nicht beeinflusst.}}
\end{align*}
\item Fall $atom?(first(\omega(\tu{x})))=F$
\begin{align*}
\intertext{\textcolor{darkblue}{NR: $I(\delta,\omega,\u{\text{atom?(first(x))}})=\text{atom?}(I(\delta,\omega,\u{\text{first(x)}}))=\text{atom?(first}(I(\delta,\omega,\u{\text{x}})))=F$ (siehe Fallunterscheidung)}}
&&=I(\delta,\omega,&\u{\text{if eq?(x,nil) then nil}} \\ &&&\u{\text{else max(build(depth(first(x)),nil),depth(rest(x)))}})
\intertext{\textcolor{darkblue}{Da $\abs{\omega(\u{x})}>1$ ist, ist $\omega(\u{x})\neq\text{[]}$}}
&&=I(\delta,\omega,&\u{\text{max(build(depth(first(x)),nil),depth(rest(x)))}})
\intertext{\textcolor{darkblue}{Korrektheit von $\delta\u{\text{max}}$ wurde bereits gezeigt}}
&&=&\text{max}(I(\delta,\omega,\u{\text{build(depth(first(x)),nil)}}),I(\delta,\omega,\u{\text{depth(rest(x))}})) \\
&&=&\text{max}(\text{build}(I(\delta,\omega,\u{\text{depth(first(x))}}),\text{[]}),I(\delta,\omega,\u{\text{depth(rest(x))}}))
\intertext{\textcolor{darkblue}{$\omega''(\u{x})=I(\delta,\omega,\u{\text{first(x)}})=\text{first}(I(\delta,\omega,\u{\text{x}}))=\text{first}(\omega(\u{x}))$. Die Gesamtanzahl der Elemente dieser Liste ist mindestens um $1$ geringer, da die Eltern-Liste nicht im rekursiven Aufruf enthalten ist.}}
\intertext{\textcolor{darkblue}{$\omega'''(\u{x})=I(\delta,\omega,\u{\text{rest(x)}})=\text{rest}(I(\delta,\omega,\u{\text{x}}))=\text{rest}(\omega(\u{x}))$. Die Gesamtanzahl der Elemente dieser Liste ist mindestens um $1$ geringer, da $\text{first}(x)$ aus der Liste entfernt wurde.}}
&&=&\text{max}(\text{build}(I(\delta,\omega'',\u{\text{depth(x)}}),\text{[]}),I(\delta,\omega''',\u{\text{depth(x)}}))
\intertext{\textcolor{darkblue}{Damit haben wir für beide rekursiven Aufrufe jeweils ein Environment für, dass die Induktionshypothese gilt. Wir wenden die Induktionshypothese daher an:}}
&&=&\text{max}(\text{build}(f_{d}(\omega''(\u{x})),\text{[]}),f_{d}(\omega'''(\u{x}))) \\
&&=&\text{max}(\text{build}(f_{d}(\text{first}(\omega(\u{x}))),\text{[]}),f_{d}(\text{rest}(\omega(\u{x}))))
\end{align*}
\end{itemize}

Die maximale Verschachtelungstiefe kann nur in $\text{first}(\omega(\u{x}))$ oder $\text{rest}(\omega(\u{x}))$ erreicht werden.
Daher machen wir eine Fallunterscheidung die diese beiden Fälle unterscheidet (und damit alle Fälle abdeckt):
\begin{itemize}
\item Wird die maximale Verschachtelungstiefe $k$ (Anmerkung: $f_{d}(\omega(\u{x}))=\pi(k)$) in $\omega(\u{x})$ in $\text{first}(\omega(\u{x}))$ erreicht
so ist $f_{d}(\omega'(\tu{x}))=\pi(k-1)$, da $\omega'(\tu{x})$ eine Verschachtelungsebene weniger enthält (die der Eltern-Liste).
Dann ist $\text{build}(f_{d}(\omega'(\tu{x})),\text{[]})=\pi(k-1+1)=\pi(k)$.

In diesem Fall gilt also $\text{max}(\text{build}(f_{d}(\omega'(\tu{x})),\text{[]}),f_{d}(\omega''(\u{x}))) = f_{d}(\omega(\u{x})) = \pi(k)$.
\item Andernfalls wird die maximale Verschachtelungstiefe $k$ in $\omega(\u{x})$ in $\text{rest}(\omega(\u{x}))$ erreicht. \\
Dann ist $f_{d}(\omega''(\u{x}))=\pi(k)$, da $\omega''(\u{x})$ der Eltern-Liste mit entferntem ersten Element entspricht.
Dann ist $f_{d}(\omega''(\u{x}))=\pi(k)$.

In diesem Fall gilt also ebenfalls $\text{max}(\text{build}(f_{d}(\omega'(\tu{x})),\text{[]}),f_{d}(\omega''(\u{x}))) = f_{d}(\omega(\u{x})) = \pi(k)$.
\end{itemize}
Daraus folgt
\[\text{max}(\text{build}(f_{d}(\omega'(\tu{x})),\text{[]}),f_{d}(\omega''(\u{x})))=f_{d}(\omega(\u{x})).\]
Damit wurde die Korrektheit von $\delta\u{\text{depth}}$ gezeigt.
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

\section{Kodierung von Datentypen}
In nahezu jedem Programm wird mehr als ein Datentyp verwendet.
Nach unseren Definitionen können wir kein Programm schreiben welches die Länge
einer Liste zurückliefert, da die Länge einer Liste eine Zahl in $\N_0$ ist und keine Liste.

Eine einfache Lösung für dieses Problem ist es Datentypen zu kombinieren.
Wir erzeugen also einen neuen Datentyp der beispielsweise die Kombination aus $L$ und $\N_0$ ist,
wir schreiben dann $L + \N_0$.

\begin{defn}
Die Kombination von 2 Datentypen $D_1$, $D_2$ ergibt einen neuen Datentyp $D_1+D_2$.
Die Mengen $A,F,P,C$ sowie die Mengen der syntaktischen Repräsentationen $A^{\Sigma}, F^{\Sigma}, P^{\Sigma}, C^{\Sigma}, \ldots$
des neuen Datentyps entsprechen der Vereinigung der jeweiligen Mengen der Datentypen $D_1$ und $D_2$.

Funktionen und Prädikate sind weiterhin nur für die Argumente aus dem eigenen Datentyp definiert.
Im Falle eines Aufrufs mit Parametern eines fremden Datentyps wird ein definierter konstanter Wert (ein Fehlerwert) zurückgeliefert.
Dazu können auch neue Konstanten eingeführt werden, welche dann jedoch wieder in allen Funktionen und Prädikaten behandelt werden müssen.
Im Fall von Prädikaten ist der Fehlerwert entweder $T$ oder $F$.
\end{defn}

Die Definition von Atomen beim Datentyp der Listen erlaubt es Listen leicht zu kombinieren. Elemente des
zweiten Datentyps sind Atome.
\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Schreiben Sie ein Programm \tu{nth} in $\lng{E}$ über dem Datentyp $L + \N_0$
welches das $n$-te Element ($n > 0$) einer Liste zurückliefert und die leere Liste falls es kein solches gibt.
Beweisen Sie die Korrektheit Ihrer Implementation.

\textit{Lösung:} Der Basisfall ist das erste Element zurückzuliefern.
In jedem weiteren Fall müssen wir das erste Element entfernen und eine Zählvariable inkrementieren.
\[\delta\tu{nth(x,y)}=\tu{if eq?(y,eins) then first(x) else nth(rest(x),minus(y,eins))}\]
Listen haben die Form $\ebr{\ell_1 \ell_2 \ldots \ell_k}$, wir bezeichnen daher in unserem Beweis mit $\ell_i$ das $i$-te Element.

Bevor wir die Induktion durchführen können müssen wir überlegen nach welcher Variable wir die Induktion führen.
Beide Variablen (\u{x}, \u{y}) werden im Laufe der Rekursion verändert.
Entscheidend ist allerdings welche Variable zum Programmabbruch führt. Das ist bei uns \u{y}.

\u{x} hat dennoch Einfluss auf unseren Beweis, denn es können 2 Fälle auftreten:
Die Anzahl der Elemente der Liste \u{x} kann größer-gleich dem Wert von \u{y} sein,
er kann aber auch kleiner sein.
Wir müssen daher in unserem Beweis eine \textbf{Fallunterscheidung} durchführen.
\begin{\whichitem}
\item Induktionshypothese:
\begin{align*}
&\quad&\tforall \omega(\tu{y}) \leq n \leq \abs{\omega(\tu{x})}: \quad \I{E}{\delta,\omega}{nth(x,y)}&=\ell_{\omega(\tu{y})} \\
&\wedge& \tforall \abs{\omega(\tu{x})} < \omega(\tu{y}) \leq n: \quad \I{E}{\delta,\omega}{nth(x,y)}&=\ebr{}
\end{align*}
Die Fallunterscheidung ist hier durch die \twedge-Verknüpfung vorhanden.
Wir haben damit alle Fälle abgedeckt denn $\abs{\omega(\tu{x})} < \omega(\tu{y})$ ist genau dann wahr, wenn
$\omega(\tu{y}) \leq \abs{\omega(\tu{x})}$ nicht wahr ist.
\item Induktionsbasis: In der Induktionsbasis müssen wir nun beide Fälle der Hypothese für den Basisfall beweisen, d.h.
einmal mit $0 = \abs{\omega(\tu{x})} < \omega(\tu{y}) \leq n = 1$ und einmal mit $1 = \abs{\omega(\tu{x})} < \omega(\tu{y}) \leq n = 1$
\begin{align*}
&\qquad \abs{\omega(\tu{x})} = 0 \qquad \omega(\tu{y}) = 1 \\
&\quad \I{E}{\delta,\omega}{nth(x,y)} \\
&=\I{E}{\delta,\omega}{if eq?(y,eins) then first(x) else nth(rest(x),minus(y,eins))} \\
\intertext{\textcolor{darkblue}{NR: $\I{E}{\delta,\omega}{eq?(y)}=\text{eq?}\rbr{\I{E}{\delta,\omega}{y},\I{E}{\delta,\omega}{eins}}=\text{eq?}\rbr{\omega(\tu{y}),1}$\newline$=\text{eq?}\rbr{1,1}=T$}}
&=\I{E}{\delta,\omega}{first(x)} \\
&=\text{first}\rbr{\I{E}{\delta,\omega}{x}} \\
&=\text{first}\rbr{\omega(\tu{x})} \\
&=\text{first}\rbr{\ebr{}} \tag{wissen wir da $\abs{\omega(\tu{x})} = 0$} \\
&=\ebr{}
\intertext{Nun den zweiten Teil der Basis.}
&\qquad \abs{\omega(\tu{x})} = 1 \qquad \omega(\tu{y}) = 1 \\
&\quad \I{E}{\delta,\omega}{nth(x,y)} \\
&=\I{E}{\delta,\omega}{if eq?(y,eins) then first(x) else nth(rest(x),minus(y,eins))} \\
\intertext{\textcolor{darkblue}{NR: $\I{E}{\delta,\omega}{eq?(y)}=\text{eq?}\rbr{\I{E}{\delta,\omega}{y},\I{E}{\delta,\omega}{eins}}=\text{eq?}\rbr{\omega(\tu{y}),1}$\newline$=\text{eq?}\rbr{1,1}=T$}}
&=\I{E}{\delta,\omega}{first(x)} \\
&=\text{first}\rbr{\I{E}{\delta,\omega}{x}} \\
&=\text{first}\rbr{\omega(\tu{x})} \\
&=\text{first}\rbr{\ebr{\ell_1}} \tag{wissen wir da $\abs{\omega(\tu{x})} = 1$} \\
&=\ell_1
\end{align*}
Die Basisfälle haben wir damit bewiesen.
\item Induktionsschritt:
\begin{align*}
&\qquad \abs{\omega(\tu{x})} \geq 1 \tag{den Fall $0$ haben wir ja schon bewiesen} \\
&\qquad \omega(\tu{y}) = n+1 \\
&\quad \I{E}{\delta,\omega}{nth(x,y)} \\
&=\I{E}{\delta,\omega}{if eq?(y,eins) then first(x) else nth(rest(x),minus(y,eins))}
\intertext{\textcolor{darkblue}{NR: $\I{E}{\delta,\omega}{eq?(y)}=\text{eq?}\rbr{\I{E}{\delta,\omega}{y},\I{E}{\delta,\omega}{eins}}=\text{eq?}\rbr{\omega(\tu{y}),1}$\newline$=\text{eq?}\rbr{n+1,1}=F$}}
&=\I{E}{\delta,\omega}{nth(rest(x),minus(y,eins))}
\intertext{\textcolor{darkblue}{NE: $\omega'(\tu{x})=\I{E}{\delta,\omega}{rest(x)}=\text{rest}\rbr{\I{E}{\delta,\omega}{x}}=\text{rest}\rbr{\omega(\tu{x})}=\text{rest}\rbr{\ebr{\ell_1 \ell_2 \ldots}}$\newline$=\ebr{\ell_2 \ldots}=\ebr{\ell'_1 \ldots}$\newline
                                    Wir definieren hier $\tforall i: \ell'_{i} = \ell_{i+1}$.
                                    \newline
                                    $\omega'(\tu{y})=\I{E}{\delta,\omega}{minus(y,eins)}=\text{minus}\rbr{\I{E}{\delta,\omega}{y},\I{E}{\delta,\omega}{eins}}$\newline$=\text{minus}\rbr{\omega(\tu{y}),1}=\text{minus}\rbr{n+1,1}=n$}}
&=\I{E}{\delta,\omega'}{nth(x,y)}
\intertext{Beobachtung: Über diesen Programmaufruf mit $\omega'(\tu{y})=n$ trifft die Induktionshypothese eine Aussage.}
\end{align*}
Fallunterscheidung nach $\abs{\omega'(\tu{x})}$:
\begin{\whichitem}
\item Fall $\abs{\omega'(\tu{x})} < \omega'(\tu{y})$:
\[\I{E}{\delta,\omega'}{nth(x,y)} = \ebr{}\]
Was das geforderte Ergebnis für diesen Fall ist.
\item Fall $\abs{\omega'(\tu{x})} \geq \omega'(\tu{y})$:
\[\I{E}{\delta,\omega'}{nth(x,y)} = \ell'_{\omega'(\tu{y})} = \ell'_{n} = \ell_{n+1}\]
Was ebenfalls das geforderte Ergebnis für diesen Fall ist.
\end{\whichitem}
\end{\whichitem}
Damit ist der Beweis erbracht. Wir stellen fest, dass Beweise von $\lng{E}$-Programmen oft kürzer sind als
die Interpretation für einen bestimmten Eingabewert.
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

Eine Alternative zur Kombination von Datentypen ist die \textbf{Kodierung} eines Datentyps in einem anderen Datentyp.
Dies findet auch in vielen alltäglichen Programmen Anwendung - genau genommen immer dann wenn nicht nur die eingebauten Datentypen einer Sprache verwendet werden.

\begin{defn}[Mapping-Funktion $\pi$]
Gegeben sei ein Datentyp $D=(A,F,P,C)$ und ein Datentyp $E$ mit der Grundmenge $B$.
\begin{\whichitem}
\item Die Funktion $\pi: A \to B$ weist jedem Wert aus $A$ einen Wert in $B$ zu, d.h. $\tforall x \in A: \: \pi(x) \in B$.
\item Die Funktion $\pi: \gbr{T,F} \to \gbr{T,F}$ weist jedem Wert aus $\gbr{T,F}$ einen Wert in $\gbr{T,F}$ zu, d.h. $\tforall x \in \gbr{T,F}: \: \pi(x) \in \gbr{T,F}$. Häufig kommt hier die Identitätsfunktion zum Einsatz.
\item $\tforall f_i(\ldots) \in F$ wird ein Funktionausdruck $\pi\ebr{f_i}(\ldots)$ über dem Datentyp $E$ konstruiert welcher die Funktion implementiert.
\item $\tforall p_i(\ldots) \in P$ wird ein Prädikatenausdruck $\pi\ebr{p_i}(\ldots)$ über dem Datentyp $E$ konstruiert welcher das Prädikat implementiert.
\item $\tforall c_i \in C$ wird ein Funktionsausdruck (mglw. eine Konstante als 0-parametrige Funktion) $\pi\ebr{c_i}$ über dem Datentyp $E$ konstruiert welcher die Konstante darstellt.
\end{\whichitem}
\end{defn}

\begin{defn}[Kodierungseigenschaften] \quad
\begin{\whichitem}
\item $\tforall x_1,\ldots,x_n \in A, f_i \in F: \pi\ebr{f_i}\rbr{\pi\rbr{x_1},\ldots,\pi\rbr{x_n}} = \pi\rbr{f_i\rbr{x_1,\ldots,x_n}}$, d.h.
für alle Werte $x_1,\ldots,x_n$ in $A$ (die Funktionsargumente) und alle Funktionen in $F$ darf es keinen Einfluss auf das Ergebnis haben,
ob für jedes Funktionsargument der Wert $x_k$ (mit $1 \leq k \leq n$) zuerst kodiert und dann die kodierte Funktion mit diesen berechnet wird
oder zuerst der die Funktion mit den Werten $x_1,\ldots,x_n$ für die Funktionsargumente berechnet und das Ergebnis kodiert wird.
\item $\tforall x \in A, p_i \in P: \pi\ebr{p_i}\rbr{\pi\rbr{x_1},\ldots,\pi\rbr{x_n}} \lra \pi\rbr{p_i\rbr{x_1,\ldots,x_n}}$, gleich wie bei den Funktionen
\end{\whichitem}
\end{defn}

In Abbildung~\ref{Kodierungseigenschaften} ist die Definition als kommutierendes Diagramm dargestellt.
\begin{figure}[h!t]
\begin{center}
\begin{tikzpicture}[node distance=2cm, auto]
\node (A) {$A$};
\node [right of=A,node distance=4cm] (A2) {$A$};
\node [below of=A] (B2) {$B$};
\node [right of=B2,node distance=4cm] (B) {$B$};
\path [->] (A) edge node {$f_i$} (A2);
\path [->] (A2) edge node {$\pi$} (B);
\path [->] (A) edge node {$\pi$} (B2);
\path [->] (B2) edge node {$\pi\ebr{f_i}$} (B);
\node [right of=A2,node distance=4cm] (rA) {$A$};
\node [right of=rA,node distance=4cm] (rTF1) {$\gbr{T,F}$};
\node [below of=rA] (rB) {$B$};
\node [right of=rB,node distance=4cm] (rTF2) {$\gbr{T,F}$};
\path [->] (rA) edge node {$p_i$} (rTF1);
\path [->] (rTF1) edge node {$\pi$} (rTF2);
\path [->] (rA) edge node {$\pi$} (rB);
\path [->] (rB) edge node {$\pi\ebr{p_i}$} (rTF2);
\end{tikzpicture}
\end{center}
 \caption{Kodierungseigenschaften}
 \label{Kodierungseigenschaften}
\end{figure}

\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Kodieren Sie die natürlichen Zahlen inkl. Null (mit der Funktion $+$, Prädikat $\text{eq?}$ und der Konstante $0$) in den Datentyp der Listen und zeigen Sie die Korrektheit
von $\pi[+](x,y)$.

\textit{Lösung:} Wir stellen die natürlichen Zahlen als Verschachtelung von Listen dar.
\begin{align*}
\pi(0)&= \ebr{} \\
\pi(x)&= \text{build}(\pi(x-1),[]) \quad \text{für $x > 0$}
\intertext{Die Funktionen und Prädikate nehmen als Argumente in Listen kodierte natürliche Zahlen entgegen}
\pi[+](\pi(x),\pi(0)) &= \pi(x)\\
\pi[+](\pi(x),\pi(y+1)) &= \pi[+](\pi(x+1),\pi(y)) \\
\pi[\text{eq?}]([],[]) &= T\\
\pi[\text{eq?}](\pi(x+1),\pi(y+1)) &= \pi[\text{eq?}](\pi(x),\pi(y))
\end{align*}

Der Beweis der Korrektheit von $\pi[+](x,y)$ erfolgt durch vollständige Induktion.
Zu zeigen ist $\tforall x,y \in \N_0: \pi\ebr{+}\rbr{\pi(x),\pi(y)} = \pi\rbr{x + y}$.
\begin{\whichitem}
\item Induktionsbasis: mit $x$ beliebig, $y=0$
\begin{align*}
&\quad \pi\ebr{+}\rbr{\pi(x),\pi(y)} \\
&= \pi\ebr{+}\rbr{\pi(x),\pi(0)} \\
&= \pi(x) \\
&= \pi(x + y)
\end{align*}
\item Induktionshypothese:
\[\tforall x,y \in \N_0, x \text{ beliebig}, y \leq n: \pi\ebr{+}\rbr{\pi(x),\pi(y)} = \pi\rbr{x + y}\]
\item Induktionsschritt: $y=n+1$
\begin{align*}
&\quad \pi\ebr{+}\rbr{\pi(x),\pi(y)} \\
&= \pi\ebr{+}\rbr{\pi(x),\pi(n+1)} \\
&= \pi\ebr{+}\rbr{\pi(x+1),\pi(n)}
\intertext{Nun können wir die Induktionshypothese anwenden:}
&= \pi\rbr{x + 1 + n} \\
&= \pi\rbr{x + y}
\end{align*}
\end{\whichitem}
\hfill $\Box$
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

\begin{defn}[Dekodierungsfunktion $\rho$]
Wenn $\rho$ existiert, ist $\rho$ ist die Umkehrfunktion zur Mapping-Funktion $\pi$.
Dann gilt $\rho(\pi(x))=x$.
\end{defn}
$\pi$ ist \textbf{injektiv} wenn $\not \exists x \neq y, \pi(x)=\pi(y)$, d.h.
es gibt keine 2 unterschiedlichen Werte für die $\pi$ das gleiche Ergebnis hat.
$\rho$ existiert genau dann wenn $\pi$ injektiv ist.
$\rho$ gilt nur für die Menge von Werten die $\pi$ annehmen kann (``Bild von $\pi$'').

\section{Kodierung von $\lng{E}$ in den Datentyp der Listen}\label{sec:codingE}
\ifthenelse{\boolean{long}}{}{\begin{comment}}
Wir werden nun darauf hin arbeiten die Unentscheidbarkeit des Halteproblems zu lösen (Kapitel~\ref{sec:halteproblem}).
Dazu werden wir zunächst $\lng{E}$ in den Datentyp der Listen kodieren (Kapitel~\ref{sec:codingE}) und anschließend einen Interpreter für
kodierte $\lng{E}$-Programme in $\lng{E}$ schreiben (Kapitel~\ref{sec:interpreter}).
\ifthenelse{\boolean{long}}{}{\end{comment}}

Wir wollen nun die Interpretationsfunktion ($I_{\lng{E}}: \text{FENV} \times \text{ENV} \times \lng{E} \to A$ mit einem Datentyp $A$) in $\lng{E}$ implementieren.
Wir nennen diesen Interpreter $\delta\tu{IX(delta,omega,exp}$.
Die verschiedenen Input-Mengen müssen wir in Listen kodieren. Dabei unterscheiden wir die Kodierungs- und
Dekodierungsfunktionen: $\pi_{\text{FENV}}$, $\pi_{\text{ENV}}$, $\pi_{\lng{E}}$, $\pi_{A}$, die jedem Element der angegebenen Menge eine
Repräsentation im Datentyp der Listen zuweisen.

Für den Interpreter sollen die Kodierungseigenschaften gelten:
\[\I{E}{\delta,\omega}{\small IX(delta,omega,exp)}=\pi_{A}\rbr{\Iu{E}{\rho_{\text{\tiny FENV}}(\omega(\tu{delta})),\rho_{\text{\tiny ENV}}(\omega(\tu{omega}))}{\rho_{\lng{E}}(\omega(\tu{exp}))}}\]
Der Einfachheit halber behandeln wir nur den Fall $A=L$, dann ist in unserem Fall $\pi_{A}(x)=x$.
Die Kodierung von $\omega$ kann beispielsweise durch eine Liste von 2-elementigen Listen geschehen wobei das 1. Element jeweils der Variablenname
und das 2. Element jeweils der Variablenwert ist. Das heißt der Sachverhalt $\omega(\tu{x1})=\ell_1, \omega(\tu{x2})=\ell_2$ wird dargestellt durch
$\ebr{ \ebr{\text{X1 } \ell_1} \ebr{\rbr{X2 } \ell_2} }$. Analog kann die Kodierung von FENV geschehen wobei hier 2 Werte pro Variable gespeichert werden: Die Parameterliste und das Programm in Listenkodierung.
$\delta$ hat dann folgende Form: 
\[\ebr{\quad\ebr{F_1 \ebr{ \ebr{x_1 \ldots x_n} \pi_{\lng{E}}(\text{exp})}} \quad \ldots \quad \ebr{F_n \ebr{ \ebr{x_1 \ldots x_n} \pi_{\lng{E}}(\text{exp}')}}\quad}.\]

Wir definieren $\ell$ als Funktion die jedes Symbol in ein entsprechendes Atom übersetzt. D.h. $\ell(\tu{first})=\text{FIRST}$, $\ell(\tu{variable}) = \text{VARIABLE}$, $\ell(\tu{myfunc}) = \text{MYFUNC}$, etc.
\begin{defn}[Mapping-Funktion $\pi_{\lng{E}}$]
Wir definieren $\pi_{\lng{E}}$ so, dass jeweils das erste Element einer Liste definiert ob diese Liste eine
Konstante, Variable, Konditional, etc. ist.
\begin{align*}
\tforall c \in C^{\Sigma}: \quad &\pi_{\lng{E}}(c)= \ebr{\text{CONST } \ell(c)} \tag{Konstanten}\\
\tforall v \in \text{IVS}: \quad &\pi_{\lng{E}}(v)= \ebr{\text{IVS } \ell(v)} \tag{Variablen}\\
\tforall f \in F^{\Sigma}: \quad &\pi_{\lng{E}}(f\tu{(}t_1\tu{,}\ldots\tu{,}t_n\tu{)}) \\
&= \ebr{\text{APPLY } \ell(f) \pi_{\lng{E}}(t_1) \ldots \pi_{\lng{E}}(t_n)} \tag{Datentyp-Funktionen}\\
\tforall p \in P^{\Sigma}: \quad &\pi_{\lng{E}}(\tu{if}\;p\;\tu{(}u_1\tu{,}\ldots\tu{,}u_n\tu{)}\;\tu{then}\;t_1\;\tu{else}\;t_2) \\
&= \ebr{\text{COND } \ell(p) \ebr{ \pi_{\lng{E}}(u_1) \ldots \pi_{\lng{E}}(u_n)} \pi_{\lng{E}}(t_1) \pi_{\lng{E}}(t_2)} \tag{Datentyp-Prädikate}\\
\tforall F \in \text{FENV}: \quad &\pi_{\lng{E}}(F\tu{(}t_1\tu{,}\ldots\tu{,}t_n\tu{)}) \\
&= \ebr{\text{CALL } \ell(F) \pi_{\lng{E}}(t_1) \ldots \pi_{\lng{E}}(t_n)} \tag{Funktionen des Funktionsenvironments}
\end{align*}
\end{defn}

Diese Definition erlaubt uns jedes $\lng{E}$-Programm in einer Liste zu kodieren.
\section{Ein $\lng{E}$-Interpreter in $\lng{E}$}\label{sec:interpreter}
Die Implementation des $\lng{E}$-Interpreters $\delta\tu{IX(delta, omega, exp)}$ in $\lng{E}$
erfolgt direkt entsprechend der Definition \ref{defn:semexp} (sowie den dort verwendeten Definitionen \ref{defn:semt} und \ref{defn:semcond})
wobei wir die größeren Teile der Definition auf Unterfunktionen aufteilen.
\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{align*}
\delta &\tu{IX(delta, omega, exp)}\\
=\;&\tu{if eq?(first(exp), CONST) then nth(exp, 2)} \tag{z.B. [CONST NIL]}\\
&\tu{else if eq?(first(exp), IVS) then DoIVS(omega, exp)}\\
&\tu{else if eq?(first(exp), APPLY) then DoAppl(delta, omega, exp)}\\
&\tu{else if eq?(first(exp), COND) then DoCond(delta, omega, exp)}\\
&\tu{else DoCall(delta, omega, exp)}
\ifthenelse{\boolean{long}}{\intertext{\u{DoIVS} implementieren wir indem wir rekursiv durch die Liste \u{omega} suchen und einen Fehler zurückgeben falls die Variable
nicht definiert wurde oder eben die Variable}}{\\}
\delta &\tu{DoIVS(omega, exp)} \tag{Aufruf z.B. mit [IVS X1]}\\
=\;&\tu{if eq?(nth(exp, 2), first(first(omega))) then nth(first(omega), 2)} \\
&\tu{else DoIVS(rest(omega), exp)}
\ifthenelse{\boolean{long}}{\intertext{\u{DoApply} implementieren wir nach der Definition der Interpretationsfunktion,  wobei wir hier sämtliche Datentypfunktionen (first,  rest,  build) hineinkodieren müssen. \u{DoApply} sieht
folglich für jeden Datentyp unterschiedlich aus.}}{\\}
\delta &\tu{DoApply(delta, omega, exp)} \tag{Aufruf z.B. mit [APPLY BUILD X1 X2]} \\
=\;&\tu{if eq?(nth(exp, 2), FIRST) then first(IX(delta, omega, nth(exp, 3)))} \\
&\tu{else if eq?(nth(exp, 2), REST) then rest(IX(delta, omega, nth(exp, 3)))} \\
&\tu{else build(IX(delta, omega, nth(exp, 3)), IX(delta, omega, nth(exp, 4)))}
\ifthenelse{\boolean{long}}{\intertext{Wir definieren eine Unterfunktion die nur die Überprüfung macht (für die beiden Prädikate atom? und eq?):}}{\\}
\delta &\tu{Check(pred, exp)} \\
=\;&\tu{if eq?(pred, ATOM) then if atom?(IX(delta,omega,first(exp))) then TRUE else FALSE} \\
&\tu{else} \\
&\tu{if eq?(IX(delta,omega,first(exp)), IX(delta,omega,nth(exp, 2))) then TRUE else FALSE}
\ifthenelse{\boolean{long}}{\intertext{\u{DoCond} ist sehr ähnlich wie \u{DoApply},  eine Abfrage für jedes Prädikat. Unter Verwendung der \u{Check} Funktion entspricht \u{DoCond} genau dem Konditional-Teil der Interpretationsfunktion.}}{\\}
\delta &\tu{DoCond(delta, omega, exp)} \tag{Aufruf z.B. mit [COND P [ X1 ] X2 X3]} \\
=\;&\tu{if eq?(Check(nth(exp, 2), nth(exp, 3)), TRUE) then IX(delta, omega, nth(exp, 4))} \\
&\tu{else IX(delta, omega, nth(exp, 5))}
\ifthenelse{\boolean{long}}{\intertext{\u{DoCall} ist nun etwas aufwändiger: Wir müssen eine neue Liste \u{omega} bauen und die Anzahl der Parameter ist variabel.
Wir beginnen mit einer Funktion \u{NewEnv}, die ein neues \u{omega} baut und returniert und einer Hilfsfunktion \u{build2} die aus 2 Elementen eine Liste baut.}}{\\}
\delta &\tu{build2(x, y)} \\
=\;&\tu{build(x, build(y, nil))} \\
\delta &\tu{NewEnv(params, values)} \\
=\;&\tu{if eq?(params, nil) then nil } \\
&\tu{else build(build2(first(params), IX(delta,omega,first(values))),}\\
&\qquad\quad\qquad \tu{NewEnv(rest(params), rest(values)))}
\ifthenelse{\boolean{long}}{\intertext{Wir können nun also ein Environment bauen. Die Werte für die Parameter bekommen wir als Listenrest nach dem Funktionsvariablennamen. Die Parameternamen
finden sich in \u{delta} als Liste,  als 1. Element vom Funktionsvariablenwert. Wir müssen allerdings noch die richtige Funktionsvariable finden. Dazu definieren wir
eine Funktion \u{FindFVS}}}{\\}
\delta &\tu{FindFVS(delta, name)} \\
=\;&\tu{if eq?(name, first(first(delta))) then nth(first(delta), 2)} \\
&\tu{else FindFVS(rest(delta), name)}
\ifthenelse{\boolean{long}}{\intertext{Damit können wir \u{DoCall} bauen:}}{\\}
\delta &\tu{DoCall(delta, omega, exp)}  \tag{Aufruf z.B. mit [CALL F X1 X2 X3]} \\
=\;&\tu{IX(delta, NewEnv(FindFVS(delta, first(nth(exp, 2))), rest(rest(exp))), } \\
   &\qquad\;\qquad\tu{FindFVS(delta, rest(nth(exp, 2))))}
\end{align*}
Damit ist der Interpreter vollständig.

Es fällt auf, dass keinerlei Fehlerfälle bzw. Fehlerbehandlung in dem Interpreter vorkommen.
Dies ist für unsere Zwecke auch nicht nötig da wir nur syntaktisch korrekte Programme interpretieren wollen.

Den Interpreter IX kann auch sich selbst interpretieren. Dazu muss er nur in Listenkodierung gebracht werden.
\ifthenelse{\boolean{long}}{}{\end{comment}}

\section{Das Halteproblem}\label{sec:halteproblem}
$\lng{E}$ ist turing-vollständig. Der Beweis dazu kann erbracht werden indem man einen 
Interpreter für (in einer definierten Art und Weise) kodierte Turingmaschinen in EXP schreibt.
\begin{defn}[Church-Turing These]
Die Klasse der Turing-berechenbaren Funktionen ist genau die Klasse der intuitiv berechenbaren Funktionen.
\end{defn}
Sofern die Church-Turing These stimmt gilt ein Beweis für ein Problem in EXP auch für alle anderen turing-vollständigen Sprachen.

\begin{defn}[Entscheidungsproblem]
Ein Prädikat $P$ ist entscheidbar, wenn es ein Programm $\Pi$ in $\lng{E}$ mit folgender Eigenschaft gibt:
\begin{\whichitem}
\item Wenn $P(x_1,\ldots,x_n)=T$: $\Iu{E}{\delta,\omega}{\Pi}=T$ mit $\omega(\tu{xi})=x_i$
\item Wenn $P(x_1,\ldots,x_n)=F$: $\Iu{E}{\delta,\omega}{\Pi}=F$ mit $\omega(\tu{xi})=x_i$
\end{\whichitem}
D.h. in einer endlichen Anzahl von Rechenschritten wird eine Entscheidung getroffen.
\end{defn}

Ein Programm hält für eine Eingabe wenn es mit dieser Eingabe ausgeführt in einer endlichen Anzahl von Rechenschritten terminiert.

\begin{defn}[Halteproblem]
Gibt es ein Programm das entscheiden kann ob ein beliebiges Programm $\Pi$ auf einer Eingabe $x$ hält?
\end{defn}

\begin{satz}
Das Halteproblem ist unentscheidbar.
\end{satz}

\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{beweis}
Wir beweisen, dass das Halteproblem (in $\lng{E}$) unentscheidbar ist, indem wir zeigen
dass es kein Programm in $\lng{E}$ geben kann, welches für beliebige Programme
und Inputs entscheidet ob das Programm hält. Dazu nehmen wir an es wäre entscheidbar in $\lng{E}$ und führen dies dann auf
einen Widerspruch zurück. Diese Beweistechnik nennt man ``Beweis durch Widerspruch''.

Ein $\lng{E}$-Programm kann ein Programm aus mehreren Funktionen bestehen. Jedes $\lng{E}$-Programm kann aber auch mit nur einer Funktion
implementiert werden. Sei $L_\Pi$ die Listenkodierung einer Funktion $\Pi$.

\textit{Annahme:} Es gibt eine Funktion $H(L_\Pi,X): L \times L \to L$ die TRUE zurückgibt falls $L_\Pi$ mit Input $X$ hält,
und FALSE zurückgibt falls $L_\Pi$ mit Input $X$ nicht hält und NIL als Fehlerwert zurückgibt falls $L_\Pi$ keine $\abs{X}$-stellige Funktion kodiert.

\textit{Für den Widerspruch zu zeigen:} 
\[\not \texists \delta: \; \tu{H(x,y)=\ldots} \in \delta, \tforall \omega \in \text{ENV}: \; \I{E}{\delta,\omega}{H(x,y)}=H(\omega(\tu{x}),\omega(\tu{y})),\]
d.h. es existiert kein Funktionsenvironment indem \u{H(x,y)} definiert wurde, so dass für alle möglichen $\omega$-Environments $\I{E}{\delta,\omega}{H(x,y)}=H(\omega(\tu{x}),\omega(\tu{y}))$ berechnet werden kann.

Um dies zu zeigen konstruieren wir eine Funktion $\delta$\u{A}, die genau dann halten soll wenn sie nicht hält:
\[\delta\tu{A(x)}=\tu{if eq?(H(x,x),TRUE) then A(x) else x}\]

Mit $\omega(\tu{x})=\pi(\delta\u{A})$ berechnen wir nun $\I{E}{\delta,\omega}{A(x)}$:
\[\I{E}{\delta,\omega}{A(x)} =\I{E}{\delta,\omega}{if eq?(H(x,x),TRUE) then A(x) else x}=\bigstar\]
Fallunterscheidung nach $\I{E}{\delta,\omega}{H(x,x)}=$
\begin{\whichitem}
\item TRUE (d.h. $\I{E}{\delta,\omega}{A(x)}$ hält): Laut Definition der Interpretationsfunktion wird dann der \u{then}-Zweig ausgeführt.
\[\bigstar=\I{E}{\delta,\omega}{A(x)}
=\I{E}{\delta,\omega}{if eq?(H(x,x),TRUE) then A(x) else x}=\bigstar\]
und da $\I{E}{\delta,\omega}{H(x,x)}=$TRUE
\[\bigstar=\I{E}{\delta,\omega}{A(x)}=\ldots\]
Wir sehen, dass das Programm nicht hält. Dies ist ein Widerspruch.
\item FALSE (d.h. $\I{E}{\delta,\omega}{A(x)}$ hält nicht): Laut Definition der Interpretationsfunktion wird dann der \u{else}-Zweig ausgeführt.
\[\I{E}{\delta,\omega}{if eq?(H(x,x),TRUE) then A(x) else x}=
=\I{E}{\delta,\omega}{x}
=\omega(\tu{x})
\]
Wir sehen, dass das Programm hält. Dies ist ebenfalls ein Widerspruch.
\end{\whichitem}
Die Fallunterscheidung deckt alle Fälle ab. Wir erhalten in jedem Fall einen Widerspruch.
Somit haben wir den Satz bewiesen. \hfill $\Box$
\end{beweis}
\ifthenelse{\boolean{long}}{}{\end{comment}}
\begin{defn}[Äquivalenzproblem]
Gibt es ein Programm das entscheiden kann ob 2 Programme die selbe Funktion berechnen?
\end{defn}

\begin{satz}
Das Äquivalenzproblem ist unentscheidbar.
\end{satz}

Der Beweis ist eine gute Übungsaufgabe.

\section{Sprache der Prädikatenlogischen Ausdrücke PL ($\lng{P}$)}
In $\lng{E}$ hatten wir bereits Prädikate. Diese waren aber nur in Konditionalen an ganz bestimmten Stellen erlaubt (\u{if \textbf{predicate} then \ldots else \ldots}).
Wir wollen nun prädikatenlogische Ausdrücke definieren die auch die Verwendung von logischen Operatoren und Quantoren erlauben.
Wir definieren nun die Sprache \textbf{PL} ($\lng{P}$). Wie schon bei \textbf{EXP} kürzen wir auch hier \textbf{PL} durch $\lng{P}$ ab - $\lng{P}$ gesprochen ``PL''.
Genau wie $\lng{E}$ wird auch $\lng{P}$ über einen Datentyp definiert.

\begin{defn}[Syntax von PL ($\lng{P}$)]
\begin{\whichenum}
\item Wenn $p^{\Sigma}$ ein $n$-stelliges Prädikatensymbol (d.h. $\in P^{\Sigma}$) ist und $t_1,\ldots,t_n$ Terme
(d.h. $\in \lng{T}$) dann ist $p^{\Sigma}\tu{(}t_1\tu{,}\ldots\tu{,}t_n\tu{)}$ ein prädikatenlogischer Ausdruck (d.h. $\in \lng{P}$).
Wir nennen diesen Ausdruck Atomformel.
\item Wenn $q \in \lng{P}$ ist, dann ist auch $\u{\tneg}q \in \lng{P}$.
\item Wenn $q,r \in \lng{P}$ sind, dann sind auch $q\u{\vee}r$,
$q\u{\wedge}r$, $q\u{\to}r$ prädikatenlogische Ausdrücke (d.h. $\in \lng{P}$).
\item Wenn $q \in \lng{P}$ und $v \in \text{IVS}$ ist, dann sind auch
$\u{(\tforall}v\u{)}q \in \lng{P}$ und $\u{(\texists}v\u{)}q \in \lng{P}$.
In diesem Fall sagen wir, dass die Variable $v$ im prädikatenlogischen Ausdruck $q$ durch einen Quantor \textbf{gebunden} ist.
\item Wenn $q \in \lng{P}$, dann ist auch $\tu{(}q\tu{)} \in \lng{P}$.
\end{\whichenum}
\end{defn}

Die Definition von $\lng{P}$ basiert auf der Definition der Sprache der Terme $\lng{T}$.
Konditional-Konstrukte (\u{if ... then ... else ...}) und Funktionsumgebungen
bzw. Funktionsvariablensymbole (``benutzerdefinierte Funktionen'') können nicht in $\lng{P}$ verwendet werden.

Bevor wir die Semantikfunktion definieren können müssen wir uns überlegen wie
wir mit Quantoren umgehen. Wenn eine Variable durch einen Quantor gebunden ist
müssen wir beispielsweise beim Existenz-Quantor einen passenden Wert suchen,
alle anderen Variablen müssen jedoch unverändert bleiben. Beim All-Quantor
müssen wir jeden Wert für eine Variable prüfen, allerdings ebenfalls alle anderen Variablen
unverändert lassen. Für diesen Zweck definieren wir den Begriff für Environments:
``äquivalent modulo'' in Bezug auf eine Variable.
\begin{defn}[äquivalent modulo]
$\omega,\omega' \in \text{ENV}$ sind genau dann äquivalent modulo $v \in \text{IVS}$,
wenn für alle $w \in \text{IVS}$ mit $v \neq w$ gilt: $\omega(w)=\omega'(w)$.
Formal schreiben wir dann: $\omega \sim_{v} \omega'$, gesprochen ``$\omega,\omega'$ äquivalent modulo $v$''.
\end{defn}

\begin{defn}[Semantik von PL ($\lng{P}$)]
Die Semantikfunktion definieren wir als $I: \text{ENV}\times\lng{P}\to\gbr{T,F}$.
Seien $q,r \in \lng{P}$ und $\omega,\omega' \in \text{ENV}$.
\begin{\whichenum}
\item
$\Iu{P}{\omega}{p^{\Sigma}\tu{(}t_1\tu{,}\ldots\tu{,}t_n\tu{)}} = p\rbr{\Iu{T}{\omega}{t_1},\ldots,\Iu{T}{\omega}{t_n}}$, wenn $t_1,\ldots,t_n \in \lng{T}$,
mit einem Prädikatensymbol $p^{\Sigma} \in P^{\Sigma}$ und dem entsprechenden Prädikat $p \in P$.
\item $\Iu{P}{\omega}{q\;\u{\vee}\;r} \Lra \rbr{\Iu{P}{\omega}{q} \vee \Iu{P}{\omega}{r}}$ (Oder-Verknüpfung)
\item $\Iu{P}{\omega}{q\;\u{\wedge}\;r} \Lra \rbr{\Iu{P}{\omega}{q} \wedge \Iu{P}{\omega}{r}}$ (Und-Verknüpfung)
\item $\Iu{P}{\omega}{q\;\u{\to}\;r} \Lra \rbr{\Iu{P}{\omega}{q} \to \Iu{P}{\omega}{r}}$ (Implikation)
\item $\Iu{P}{\omega}{\u{\tneg}\;q} \Lra \tneg \Iu{P}{\omega}{q}$ (Negation)
\item $\Iu{P}{\omega}{\u{(}\;q\;\u{)}} \Lra \Iu{P}{\omega}{q}$ (Klammerung)
\item $\Iu{P}{\omega}{\u{(\tforall}\;v\;\u{)}\;q} \Lra \tforall \omega', \omega \sim_v \omega': \; \Iu{P}{\omega'}{q}$ (All-Quantor)
\item $\Iu{P}{\omega}{\u{(\texists}\;v\;\u{)}\;q} \Lra \texists \omega', \omega \sim_v \omega': \; \Iu{P}{\omega'}{q}$ (Existenz-Quantor)
\end{\whichenum}
\end{defn}

\begin{defn}[Syntax von PL$_0$ ($\lng{P}_0$)]
Die Sprache $\lng{P}_0$ ist die quantorenfreie Teilmenge der Sprache $\lng{P}$. Es ist also $\u{(\tforall}v\u{)}q \not \in \lng{P}_0$ und $\u{(\texists}v\u{)}q \not \in \lng{P}_0$.
\end{defn}

\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Interpretieren Sie die folgenden prädikatenlogischen Ausdrucke in $\lng{P}$ mit dem Datentyp $\N_0$ unter dem Environment $\omega(\tu{x})=0$:
\begin{\whichenum}
\item \u{((lt?(x,plus(eins,eins)) \twedge eq?(x,null)) \tvee lt?(x,eins)) \tto eq?(x,eins)}

\textit{Lösung:}
\begin{align*}
&\I{P}{\omega}{((lt?(x,plus(eins,eins)) \twedge eq?(x,null)) \tvee lt?(x,eins)) \tto eq?(x,eins)} \\
&\Lra \I{P}{\omega}{((lt?(x,plus(eins,eins)) \twedge eq?(x,null)) \tvee lt?(x,eins))} \tto \I{P}{\omega}{eq?(x,eins)} \\
&\Lra \rbr{\I{P}{\omega}{(lt?(x,plus(eins,eins)) \twedge eq?(x,null)) \tvee lt?(x,eins)}} \tto eq?(\I{P}{\omega}{x},\I{P}{\omega}{eins}) \\
&\Lra \rbr{\I{P}{\omega}{(lt?(x,plus(eins,eins)) \twedge eq?(x,null))} \tvee \I{E}{\omega}{lt?(x,eins)}} \tto eq?(\omega(\tu{x}),1) \\
&\Lra \rbr{\rbr{\I{P}{\omega}{lt?(x,plus(eins,eins)) \twedge eq?(x,null)}} \tvee lt?(\I{P}{\omega}{x},\I{P}{\omega}{eins})} \tto eq?(0,1) \\
&\Lra \rbr{\rbr{\I{P}{\omega}{lt?(x,plus(eins,eins))} \twedge \I{P}{\omega}{eq?(x,null)}} \tvee lt?(\omega(\tu{x}),1)} \tto F \\
&\Lra \neg\rbr{\rbr{\I{P}{\omega}{lt?(x,plus(eins,eins))} \twedge \I{P}{\omega}{eq?(x,null)}} \tvee lt?(\omega(\tu{x}),1)} \tvee F \\
&\Lra \neg\rbr{\rbr{\I{P}{\omega}{lt?(x,plus(eins,eins))} \twedge \I{P}{\omega}{eq?(x,null)}} \tvee lt?(\omega(\tu{x}),1)} \\
&\Lra \neg\rbr{\rbr{lt?(\I{P}{\omega}{x},\I{P}{\omega}{plus(eins,eins)}) \twedge eq?(\I{P}{\omega}{x},\I{P}{\omega}{null})} \tvee lt?(0,1)} \\
&\Lra \neg\rbr{\rbr{lt?(\omega(\tu{x}),\I{P}{\omega}{eins} + \I{P}{\omega}{eins}) \twedge eq?(\omega(\tu{x}),0)} \tvee lt?(0,1)} \\
&\Lra \neg\rbr{\rbr{lt?(0,1 + 1) \twedge eq?(0,0)} \tvee T}
\intertext{Damit wissen wir eigentlich schon genug, denn $\neg(\ldots \vee T) \Lra \neg T \Lra F$. Der Vollständigkeit halber rechnen wir hier weiter.}
&\Lra \neg\rbr{\rbr{lt?(0,2) \twedge T} \tvee T} \Lra \neg\rbr{\rbr{T \twedge T} \tvee T} \Lra \neg\rbr{T \tvee T} \Lra \neg T \Lra F
\end{align*}
\item \u{(\texists y) lt?(y,x)}

\textit{Lösung:}
\begin{align*}
&\quad \I{P}{\omega}{(\texists y) lt?(y,x)} \\
&\Lra \texists \omega', \omega \sim_{\u{y}} \omega': \; \Iu{P}{\omega'}{lt?(y,x)} \\
&\Lra \texists \omega', \omega \sim_{\u{y}} \omega': \; \text{lt?}(\Iu{P}{\omega'}{y},\Iu{P}{\omega'}{x}) \\
&\Lra \texists \omega', \omega \sim_{\u{y}} \omega': \; \text{lt?}(\omega'(\tu{y}),\omega'(\tu{x})) \\
&\Lra \texists \omega', \omega \sim_{\u{y}} \omega': \; \text{lt?}(\omega'(\tu{y}),0) \\
&\Lra \texists \omega', \omega \sim_{\u{y}} \omega': \; \omega'(\tu{y}) < 0
\intertext{Da $\omega'(\tu{y}) \in \N_0$, d.h. $\omega'(\tu{y}) \geq 0$, gibt es keinen Wert den $\omega'(\tu{y})$ annehmen könnte um das Prädikat zu erfüllen.}
&\Lra F
\end{align*}
\end{\whichenum}
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

\begin{defn}[Semantischer Status]
Der semantische Status eines prädikatenlogischen Ausdrucks $p \in \lng{P}$ ist:
\begin{\whichitem}
\item Wenn für alle $\omega \in \text{ENV}$ die Interpretation $\Iu{P}{\omega}{p}=T$ ist, dann heißt $p$ \textbf{gültig} oder \textbf{allgemeingültig}.
\item Wenn es mindestens ein $\omega \in \text{ENV}$ gibt, so dass $\Iu{P}{\omega}{p}=T$ ist, dann heißt $p$ \textbf{erfüllbar}.
\item Wenn es kein $\omega \in \text{ENV}$ gibt, so dass $\Iu{P}{\omega}{p}=T$ ist, dann heißt $p$ \textbf{nicht erfüllbar} oder \textbf{unerfüllbar}.
\end{\whichitem}
\end{defn}

Für die meisten Programme sind nur erfüllbare Ausdrücke interessant, da nur diese den Programmfluss nicht beeinflussen.

\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Ermitteln Sie den semantischen Status für Programme in $\lng{P}$ über dem Datentyp der binären Stacks:

\begin{\whichenum}
\item \u{(\tforall x)\tneg \text{istLeer?}(add0(x))}

\textit{Lösung:}
\begin{align*}
\I{P}{\omega}{(\tforall x)\tneg \text{istLeer?}(add0(x))} \\
&\Lra \tforall \omega', \omega \sim_{\u{x}} \omega': \; \Iu{P}{\omega'}{\tneg \text{istLeer?}(add0(x))} \\
&\Lra \tforall \omega', \omega \sim_{\u{x}} \omega': \; \tneg \Iu{P}{\omega'}{\text{istLeer?}(add0(x))} \\
&\Lra \tforall \omega', \omega \sim_{\u{x}} \omega': \; \tneg \text{istLeer?}(\Iu{P}{\omega'}{add0(x)}) \\
&\Lra \tforall \omega', \omega \sim_{\u{x}} \omega': \; \tneg \text{istLeer?}(add0(\Iu{P}{\omega'}{x})) \\
&\Lra \tforall \omega', \omega \sim_{\u{x}} \omega': \; \tneg \text{istLeer?}(add0(\omega'(\tu{x}))) \\
\intertext{add0 legt eine 0 auf den Stack. Ist $\omega'(\tu{x})$ nicht leer ist es danach weiterhin nicht leer.
War $\omega'(\tu{x})$ zuvor leer ist es danach nicht mehr leer.}
&\Lra \tforall \omega', \omega \sim_{\u{x}} \omega': \; \tneg F \\
&\Lra \tforall \omega', \omega \sim_{\u{x}} \omega': \; T \\
\end{align*}
Der Ausdruck ist \textbf{gültig}.
\item \u{ist0?(x)\tto(ist1?(y)\tvee\text{istLeer?}(y))}

\textit{Lösung:}
\begin{align*}
&\quad \I{P}{\omega}{ist0?(x)\tto(ist1?(y)\tvee\text{istLeer?}(y))} \\
&\Lra \I{P}{\omega}{ist0?(x)}\to\rbr{\I{P}{\omega}{ist1?(y)\tvee\text{istLeer?}(y)}} \\
&\Lra \text{ist0?}(\I{P}{\omega}{x})\to\rbr{\I{P}{\omega}{ist1?(y)}\vee\I{P}{\omega}{\text{istLeer?}(y)}} \\
&\Lra \text{ist0?}(\omega(\u{x}))\to \rbr{\text{ist1?}(\I{T}{\omega}{y})\vee\text{istLeer?}(\I{T}{\omega}{y})} \\
&\Lra \text{ist0?}(\omega(\u{x}))\to \rbr{\text{ist1?}(\omega(\u{y}))\vee\text{istLeer?}(\omega(\u{y}))}
\end{align*}
Wir vermuten, dass der semantische Status \textbf{erfüllbar} ist. Um dies zu beweisen müssen wir eine Variablenbelegung mit der der Ausdruck zu $T$ evaluiert und eine
mit der er zu $F$ evaluiert.
Fallunterscheidung nach $\omega(\u{x})$
\begin{\whichitem}
\item $\omega(\u{x})=1$:
\begin{align*}
&\Lra \text{ist0?}(1)\to \rbr{\text{ist1?}(\omega(\u{y}))\vee\text{istLeer?}(\omega(\u{y}))} \\
&\Lra F \to \rbr{\text{ist1?}(\omega(\u{y}))\vee\text{istLeer?}(\omega(\u{y}))} \\
\intertext{``Aus Falschem folgt Beliebiges'', d.h. $\Lra T$ - wir können aber auch weiter umformen:}
&\Lra \tneg F \vee \rbr{\text{ist1?}(\omega(\u{y}))\vee\text{istLeer?}(\omega(\u{y}))} \\
&\Lra T \vee \rbr{\text{ist1?}(\omega(\u{y}))\vee\text{istLeer?}(\omega(\u{y}))} \\
&\Lra T
\end{align*}
\item $\omega(\u{x})=0$:
\begin{align*}
&\Lra \text{ist0?}(0)\to \rbr{\text{ist1?}(\omega(\u{y}))\vee\text{istLeer?}(\omega(\u{y}))} \\
&\Lra T \to \rbr{\text{ist1?}(\omega(\u{y}))\vee\text{istLeer?}(\omega(\u{y}))} \\
\intertext{Die nächsten 3 Umformungszeilen sind trivial, wir führen sie hier trotzdem nochmal genau durch:}
&\Lra \tneg T \vee \rbr{\text{ist1?}(\omega(\u{y}))\vee\text{istLeer?}(\omega(\u{y}))} \\
&\Lra F \vee \rbr{\text{ist1?}(\omega(\u{y}))\vee\text{istLeer?}(\omega(\u{y}))} \\
&\Lra \text{ist1?}(\omega(\u{y}))\vee\text{istLeer?}(\omega(\u{y})) \\
\intertext{Damit der Ausdruck zu $F$ evaluiert müssen die Oder-verknüpften Ausdrücke alle zu $F$ evaluieren. Dazu wählen wir $\omega(\u{y})=0$.}
&\Lra \text{ist1?}(0)\vee\text{istLeer?}(0)
\quad \Lra \quad F\vee F
\quad \Lra \quad F
\end{align*}
\end{\whichitem}
Der Ausdruck ist \textbf{erfüllbar}.
\item \u{istLeer?(x)\twedge ist1?(x)}

\textit{Lösung:}
\begin{align*}
&\quad \I{P}{\omega}{\text{istLeer?}(x)\twedge ist1?(x)} \\
&\Lra \I{P}{\omega}{\text{istLeer?}(x)}\wedge\I{P}{\omega}{ist1?(x)} \\
&\Lra \text{istLeer?}(\I{T}{\omega}{x})\wedge\text{ist1?}(\I{T}{\omega}{x}) \\
&\Lra \text{istLeer?}(\omega(\u{x}))\wedge\text{ist1?}(\omega(\u{x})) \\
\intertext{$\text{istLeer?}(\omega(\u{x}))=T$ genau dann wenn $\omega(\u{x})=\varepsilon$, dann ist aber $\text{ist1?}(\omega(\u{x}))=F$. Die Und-Verknüfpung kann also nicht zu $T$ evaluieren.}
&\Lra F
\end{align*}
Der Ausdruck ist \textbf{nicht erfüllbar}.
\end{\whichenum}
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

Eine Erweiterung von $\lng{E}$ um prädikatenlogische Ausdrücke als Prädikate
führen wir an dieser Stelle nicht durch. Diese ist zwar zumindest mit quantorfreien
Ausdrücken einfach, wir werden allerdings in Abschnitt~\ref{sec:AL} eine Sprache
definieren in der wir die Sprache $\lng{P}$ für Konditionale verwenden.

\section{Assignmentsprachen / Sprache AL ($\lng{A}$)}\label{sec:AL}
\ifthenelse{\boolean{long}}{}{\begin{comment}}
Assignmentsprachen (imperative Sprachen) sind die häufigsten verwendeten Programmiersprachen (z.B. C, C++, Java)
und vermutlich sind auch die meisten Programmiersprachen Assignmentsprachen.

In Tabelle~\ref{unterschiede_funktional_imperativ} findet sich eine Auflistung von Merkmalen funktionaler und imperativer Sprachen.
\begin{table}[h!t]
 \centering

\begin{tabular}{rp{0.25\hsize}p{0.25\hsize}}
 & \textbf{funktional} & \textbf{imperativ} \\
\textbf{Zuweisungen} & nicht möglich & möglich \\
\textbf{Variablenwerte} & unveränderbar & veränderbar \\
\textbf{mathematische Definition} & direkt umsetzbar & muss u.U. ganz anders formuliert werden \\
\textbf{Iteration} & Rekursion & Schleifen \\
\textbf{Berechnungsergebnis} & Wert & Environment
\end{tabular}

\caption{Unterschiede zwischen funktionalen Sprachen und Assignmentsprachen}
 \label{unterschiede_funktional_imperativ}
\end{table}
\ifthenelse{\boolean{long}}{}{\end{comment}}

Der Zustand eines Programms in einer Assignmentsprache ist durch die Variablenwerte definiert.
Befehle stellen Zustandsübergänge dar.

Wir definieren nun die Sprache \textbf{AL}.
Wie schon bei \textbf{EXP} kürzen wir auch hier \textbf{AL} durch $\lng{A}$ ab - $\lng{A}$ gesprochen ``AL''.
\begin{defn}[Syntax von AL $\lng{A}$]
Gegeben die Sprachen $\text{T}$ und $\lng{P}_0$ über einen beliebigen Datentyp $D$,
so definieren wir die Syntax von $\lng{A}$ wie folgt:
\begin{\whichenum}
\item Wenn $v \in \text{IVS}$ und $t \in \lng{T}$,
dann ist $v \tu{:-} t \; \in \lng{A}$ (Assignments).
\item Wenn $a_1,a_2 \in \lng{A}$ dann ist $\tu{begin} \; a_1 \; \tu{;} \; a_2 \; \tu{end} \; \in \lng{A}$ (Blöcke).
\item Wenn $a_1,a_2 \in \lng{A}$ und $p \in \lng{P}_0$, dann ist $\tu{if} \; p \; \tu{then} \; a_1 \; \tu{else} \; a_2 \; \in \lng{A}$ (Konditionale).
\item Wenn $a \in \lng{A}$ und $p \in \lng{P}_0$, dann ist $\tu{while} \; p \; \tu{do} \; a \; \in \lng{A}$ (Schleifen).
\end{\whichenum}
\end{defn}

Zwischen \u{begin} und \u{end} stehen \textbf{genau zwei Befehle} die von genau einem \u{;} getrennt werden. Dies ist keine Einschränkung, da durch Verschachtelung beliebig viele Befehle nacheinander
ausgeführt werden können. Die Syntax von $\lng{A}$ erinnert an eine stark vereinfachte Version von ALGOL (oder einer verwandten Sprache - Pascal, als bekannteres Beispiel).
Es fällt außerdem auf, dass ein Term $t \in \lng{T}$ nur an ganz bestimmten Stellen in der Sprache vorkommen darf.

\begin{defn}[Semantik von AL $\lng{A}$]
Die Interpretationsfunktion $I_{\lng{A}}: \text{ENV} \times \lng{A} \to \text{ENV}$ nimmt ein Environment und ein Programm und berechnet ein neues Environment.
\begin{\whichenum}
\item Assignments: $\Iu{A}{\omega}{v \; \tu{:=} \; t} = \omega'$ mit $\omega' \sim_{v} \omega$ und $\omega'(v)=\Iu{T}{\omega}{t}$.
\item Blöcke: $\Iu{A}{\omega}{\tu{begin} \; a_1 \; \tu{;} \; a_2 \; \tu{end}} = \Iu{A}{\Iu{A}{\omega}{a_1}}{a_2}$.
\item Konditionale:
\begin{\whichenum}
\item $\Iu{A}{\omega}{\tu{if} \; p \; \tu{then} \; a_1 \; \tu{else} \; a_2} = \Iu{A}{\omega}{a_1}$ wenn $\Iu{P}{\omega}{p}=T$.
\item $\Iu{A}{\omega}{\tu{if} \; p \; \tu{then} \; a_1 \; \tu{else} \; a_2} = \Iu{A}{\omega}{a_2}$ wenn $\Iu{P}{\omega}{p}=F$.
\end{\whichenum}
\item Schleifen:
\begin{\whichenum}
\item $\Iu{A}{\omega}{\tu{while} \; p \; \tu{do} \; a} = \Iu{A}{\Iu{A}{\omega}{a}}{\tu{while} \; p \; \tu{do} \; a}$ wenn $\Iu{P}{\omega}{p}=T$.
\item $\Iu{A}{\omega}{\tu{while} \; p \; \tu{do} \; a} = \omega$ wenn $\Iu{P}{\omega}{p}=F$.
\end{\whichenum}
\end{\whichenum}
\end{defn}

\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Implementieren Sie die Multiplikation zweier Zahlen über dem Datentyp $\N_0$. Interpretieren Sie ihre Implementation für $\omega(\u{x})=3$, $\omega(\u{y})=2$.

\textit{Lösung:} Wir initialisieren die Variable \u{z} für das Ergebnis auf $0$ und addieren
\u{x} \tu{y}-mal dazu.
\lstset{numbers=left, numbersep=5pt, xleftmargin=0.3\hsize}
\begin{lstlisting}[mathescape]
$\tu{begin}$
  $\tu{z := null ;}$
  $\tu{while \tneg eq?(y,null) do}$
    $\tu{begin}$
      $\tu{z := plus(z,x) ;}$
      $\tu{y := minus(y,eins)}$
    $\tu{end}$
$\tu{end}$
\end{lstlisting}

In der Interpretation werden wir nicht relevante Zeilen jeweils durch Platzhalter
$Z_k$ ersetzen um so mehr Übersicht zu schaffen.
\begin{align*}
&\quad \Iu{A}{\omega}{\tu{begin z := null ; while \tneg eq?(y,null) do} \; Z_{4,5,6,7} \; \tu{end}} \\
&= \Iu{A}{\I{A}{\omega}{z := null}}{\tu{while \tneg eq?(y,null) do} \; Z_{4,5,6,7}} \\
\intertext{\textcolor{darkblue}{NE: $\omega^{1} \sim_{\tu{z}} \omega$ und berechnen $\omega^{1}(\tu{z})=\I{T}{\omega}{null}=0$}}
&= \Iu{A}{\omega^{1}}{\tu{while \tneg eq?(y,null) do} \; Z_{4,5,6,7}} \\
\intertext{\textcolor{darkblue}{NR: $\I{P}{\omega^{1}}{\tneg eq?(y,null)}
=\tneg \I{P}{\omega^{1}}{eq?(y,null)}
=\tneg \text{eq?}\rbr{\I{T}{\omega^{1}}{y},\I{T}{\omega^{1}}{null}}$\newline$
=\tneg \text{eq?}\rbr{\omega^{1}(\tu{y}),0}
=\tneg \text{eq?}\rbr{2,0}
=\tneg F
=T$}}
&= \Iu{A}{\I{A}{\omega^{1}}{\small begin z := plus(z,x) ; y := minus(y,eins) end}}{\tu{\footnotesize while \tneg eq?(y,null) do} \; Z_{4,5,6,7}} \\
&= \Iu{A}{\I{A}{\I{A}{\omega^{1}}{z := plus(z,x)}}{y := minus(y,eins)}}{\tu{\footnotesize while \tneg eq?(y,null) do} \; Z_{4,5,6,7}} \\
\intertext{\textcolor{darkblue}{NE: $\omega^{2} \sim_{\tu{z}} \omega^{1}$ und berechnen
$\omega^{2}(\tu{z})
=\I{T}{\omega^{1}}{plus(z,x)}
=\text{plus}(\I{T}{\omega^{1}}{z},\I{T}{\omega^{1}}{x})$\newline$
=\text{plus}(\omega^{1}(\u{z}),\omega^{1}(\u{x}))
=\text{plus}(0,3)
=3$}}
&= \Iu{A}{\I{A}{\omega^{2}}{y := minus(y,eins)}}{\tu{while \tneg eq?(y,null) do} \; Z_{4,5,6,7}} \\
\intertext{\textcolor{darkblue}{NE: $\omega^{3} \sim_{\tu{y}} \omega^{2}$ und berechnen
$\omega^{3}(\tu{y})
=\I{T}{\omega^{2}}{minus(y,eins)}$\newline$
=\text{minus}(\I{T}{\omega^{2}}{y},\I{T}{\omega^{2}}{eins})
=\text{minus}(\omega^{2}(\u{y}),1)
=\text{minus}(2,1)
=1$}}
&= \Iu{A}{\omega^{3}}{\tu{while \tneg eq?(y,null) do} \; Z_{4,5,6,7}} \\
\intertext{\textcolor{darkblue}{NR: $\I{P}{\omega^{3}}{\tneg eq?(y,null)}
=\tneg \I{P}{\omega^{3}}{eq?(y,null)}
=\tneg \text{eq?}\rbr{\I{T}{\omega^{3}}{y},\I{T}{\omega^{1}}{null}}$\newline$
=\tneg \text{eq?}\rbr{\omega^{3}(\tu{y}),0}
=\tneg \text{eq?}\rbr{1,0}
=\tneg F
=T$}}
&= \Iu{A}{\I{A}{\omega^{3}}{\small begin z := plus(z,x) ; y := minus(y,eins) end}}{\tu{\footnotesize while \tneg eq?(y,null) do} \; Z_{4,5,6,7}} \\
&= \Iu{A}{\I{A}{\I{A}{\omega^{3}}{z := plus(z,x)}}{y := minus(y,eins)}}{\tu{\footnotesize while \tneg eq?(y,null) do} \; Z_{4,5,6,7}} \\
\intertext{\textcolor{darkblue}{NE: $\omega^{4} \sim_{\tu{z}} \omega^{3}$ und berechnen
$\omega^{4}(\tu{z})
=\I{T}{\omega^{3}}{plus(z,x)}
=\text{plus}(\I{T}{\omega^{3}}{z},\I{T}{\omega^{3}}{x})$\newline$
=\text{plus}(\omega^{3}(\u{z}),\omega^{3}(\u{x}))
=\text{plus}(3,3)
=6$}}
&= \Iu{A}{\I{A}{\omega^{4}}{y := minus(y,eins)}}{\tu{while \tneg eq?(y,null) do} \; Z_{4,5,6,7}} \\
\intertext{\textcolor{darkblue}{NE: $\omega^{5} \sim_{\tu{y}} \omega^{4}$ und berechnen
$\omega^{5}(\tu{y})
=\I{T}{\omega^{4}}{minus(y,eins)}$\newline$
=\text{minus}(\I{T}{\omega^{4}}{y},\I{T}{\omega^{4}}{eins})
=\text{minus}(\omega^{4}(\u{y}),1)
=\text{minus}(1,1)
=0$}}
&= \Iu{A}{\omega^{5}}{\tu{while \tneg eq?(y,null) do} \; Z_{4,5,6,7}} \\
\intertext{\textcolor{darkblue}{NR: $\I{P}{\omega^{5}}{\tneg eq?(y,null)}
=\tneg \I{P}{\omega^{5}}{eq?(y,null)}
=\tneg \text{eq?}\rbr{\I{T}{\omega^{5}}{y},\I{T}{\omega^{5}}{null}}$\newline$
=\tneg \text{eq?}\rbr{\omega^{5}(\tu{y}),0}
=\tneg \text{eq?}\rbr{0,0}
=\tneg T
=F$}}
&= \omega^{(5)}
\end{align*}
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

Korrektheitsbeweise von $\lng{A}$-Programmen unterscheiden sich wesentlich von
jenen für $\lng{E}$-Programmen. In $\lng{E}$ konnten wir nicht-rekursive Funktionen
einfach direkt beweisen (durch Interpretation, evtl. Fallunterscheidung). Rekursive
Funktionen konnten durch vollständige Induktion bewiesen werden. Anstatt der Rekursion
haben wir nun Schleifen. Über diese können wir auch vollständige Induktionen führen.
In $\lng{A}$ ist dies aufgrund des geringen Sprachumfangs einfacher als
in Sprachen die in der Praxis verwendet werden.

\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Beweisen Sie die Korrektheit ihrer Implementation der Multiplikation über dem Datentyp $\N_0$.

\textit{Lösung:} Unser Programm ist korrekt wenn $\omega(\tu{x}) \cdot \omega(\tu{y}) = \omega^k(\tu{z})$,
wobei $\omega$ das initiale Environment ist und $\omega^k$ das Ergebnis des Programms.
Wir verwenden den Platzhalter $Z_k$ aus dem vorherigen Beispiel.

\[\text{Zu zeigen:} \quad \forall \omega \in \text{ENV}: \; \Iu{A}{\omega}{Z_{1,\ldots,8}}=\omega^k \; \wedge \; \omega(\tu{x}) \cdot \omega(\tu{y}) = \omega^k(\tu{z})\]
\begin{align*}
&\quad \Iu{A}{\omega}{\tu{begin z := null ; while \tneg eq?(y,null) do} \; Z_{4,5,6,7} \; \tu{end}} \\
&= \Iu{A}{\I{A}{\omega}{z := null}}{Z_{3,\ldots,7}} \\
\end{align*}
\textcolor{darkblue}{NE: $\omega^{1} \sim_{\tu{z}} \omega$ und berechnen $\omega^{1}(\tu{z})=\I{T}{\omega}{null}=0$}
Über das Teilprogramm $Z_{3,4,5,6,7}$ führen wir nun eine vollständige Induktion durch.
\begin{\whichitem}
\item Induktionshypothese: $\omega(\tu{x})=m$ beliebig, $\omega(\tu{y})=n$, $\omega(\tu{z})=p$ beliebig, mit $\omega^k$ dem Ergebnis der Berechnung (finales Environment).
\[\forall \omega \in \text{ENV}, \omega(\tu{y}) \leq n: \; \Iu{A}{\omega}{Z_{3,\ldots,7}}=\omega^k \; \wedge \; \omega(\tu{x}) \cdot \omega(\tu{y}) + \omega(\tu{z}) = \omega^k(\tu{z})\]
\item Induktionsbasis: $\omega(\tu{x})=m$ beliebig, $\omega(\tu{y})=0$, $\omega(\tu{z})=p$
\begin{align*}
&\quad \Iu{A}{\omega^1}{\tu{while \tneg eq?(y,null) do} \; Z_{4,5,6,7}} \\
\intertext{\textcolor{darkblue}{NR: $\I{P}{\omega^{1}}{\tneg eq?(y,null)}
=\tneg \I{P}{\omega^{1}}{eq?(y,null)}$\newline$
=\tneg \text{eq?}\rbr{\I{T}{\omega^{1}}{y},\I{T}{\omega^{1}}{null}}
=\tneg \text{eq?}\rbr{\omega^{1}(\tu{y}),0}
=\tneg \text{eq?}\rbr{0,0}
=\tneg T
=F$}}
&= \omega^1
\end{align*}
Wir erhalten $\omega^1(\tu{z})=p$. Der Basisfall ist also bewiesen.
\item Induktionsschritt: $\omega(\tu{x})=m$ beliebig, $\omega(\tu{y})=n+1$, $\omega(\tu{z})=p$ beliebig
\begin{align*}
&\quad \Iu{A}{\omega^\ell}{\tu{while \tneg eq?(y,null) do} \; Z_{4,5,6,7}} \\
\intertext{\textcolor{darkblue}{NR: $\I{P}{\omega^{\ell}}{\tneg eq?(y,null)}
=\tneg \I{P}{\omega^{\ell}}{eq?(y,null)}$\newline$
=\tneg \text{eq?}\rbr{\I{T}{\omega^{1}}{y},\I{T}{\omega^{\ell}}{null}}
=\tneg \text{eq?}\rbr{\omega^{\ell}(\tu{y}),0}
=\tneg \text{eq?}\rbr{n+1,0}
=\tneg F
=T$}}
&= \Iu{A}{\I{A}{\omega^{\ell}}{begin z := plus(z,x) ; y := minus(y,eins) end}}{Z_{3,\ldots,7}} \\
&= \Iu{A}{\I{A}{\I{A}{\omega^{\ell}}{z := plus(z,x)}}{y := minus(y,eins)}}{Z_{3,\ldots,7}} \\
\intertext{\textcolor{darkblue}{NE: $\omega^{\ell+1} \sim_{\tu{z}} \omega^{\ell}$ und berechnen
$\omega^{\ell+1}(\tu{z})
=\I{T}{\omega^{\ell}}{plus(z,x)}$\newline$
=\text{plus}(\I{T}{\omega^{\ell}}{z},\I{T}{\omega^{1}}{x})
=\text{plus}(\omega^{\ell}(\u{z}),\omega^{1}(\u{x}))
=\text{plus}(p,m)
=p+m$}}
&= \Iu{A}{\I{A}{\omega^{\ell+1}}{y := minus(y,eins)}}{Z_{3,\ldots,7}} \\
\intertext{\textcolor{darkblue}{NE: $\omega^{\ell+2} \sim_{\tu{y}} \omega^{\ell+1}$ und berechnen
$\omega^{\ell+2}(\tu{y})
=\I{T}{\omega^{\ell+1}}{minus(y,eins)}$\newline$
=\text{minus}(\I{T}{\omega^{\ell+1}}{y},\I{T}{\omega^{\ell+1}}{eins})
=\text{minus}(\omega^{\ell+1}(\u{y}),1)
=\text{minus}(n+1,1)
=n$}}
&= \Iu{A}{\omega^{\ell+2}}{Z_{3,\ldots,7}} \\
\intertext{Wir sehen, dass für $\omega^{\ell+2}$ die Induktionshypothese gilt und verwenden diese:}
&= \omega^k \\
\omega^k(\tu{z}) &= \omega^{\ell+2}(\tu{x}) \cdot \omega^{\ell+2}(\tu{y}) + \omega^{\ell+2}(\tu{z}) \\
&= m \cdot n + (p+m) \\
&= (m+1) \cdot n + p
\end{align*}
Und damit ist auch die Schleife bewiesen. Das Programm ist also korrekt.\hfill$\Box$
\end{\whichitem}
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

Im Vorlesungsskriptum findet sich ab Seite 87 die Definition der Sprache $\lng{A^P}$ skizziert.
Diese ist eine Erweiterung von $\lng{A}$ um das Konzept ``Pointer'' (``Zeiger'').
Variablen werden dabei nur noch Adressen (aus $\N_0$) enthalten, die Werte stehen in einem neuen
Environment an der entsprechenden Adresse.
Für diese Erweiterung ist es nötig $\lng{T}$, $\lng{P}$ und $\lng{A}$ neu zu definieren um ein
neues Environment ($\sigma$) einzuführen.
Anhand dieser Erweiterung wird deutlich, dass das Konzept Pointer im Wesentlichen nur ein zusätzliches Mapping ist,
die Mächtigkeit der Sprache aber nicht ändert - jedoch ``Komfort'' für den Programmierer bringen kann.

\section{Die Sprache LP ($\lng{L}$)}
Das dritte Sprachparadigma welches wir untersuchen wollen ist die ``Logische Programmierung''.
\ifthenelse{\boolean{long}}{}{\begin{comment}}
In logischen Programmen werden Zusammenhänge in Form von logischen Formeln festgehalten.
Die Vorgehensweise (d.h. der Lösungsweg) muss vom Programmierer nicht explizit angegeben werden.
Wir werden die Sprache $\lng{L}$ (gesprochen ``LP'') entwerfen, die durchaus an einfaches Prolog erinnert.

An dieser Stelle ist noch ein Hinweis auf das Vorlesungsskriptum angebracht welches eine weitere Sprache
definiert (``P'' die Sprache der Aussagenlogik) und außerdem Grundlagen der Aussagenlogik wiederholt. Wir
gehen an dieser Stelle davon aus, dass der Leser diese Grundkenntnisse ($a \to b \Lra \neg a \vee b$, ``Wie können Aussagen in menschlicher Sprache in Aussagenlogik ausgedrückt werden?'', etc.) bereits erworben hat
und werden daher gleich die Sprache $\lng{L}$ definieren.

Programme bestehen in $\lng{L}$ aus Fakten und Regeln für Schlussfolgerungen mit einfachen prädikatenlogischen Ausdrücken.
Bei der Semantik von $\lng{L}$ lassen wir die Semantikfunktion bewusst weg und definieren stattdessen Äquivalenzen zu logischen Ausdrücken.
Unterstreichungen lassen wir ebenfalls weg, da wir nicht mehr zwischen Syntax- und Semantik-Ebene trennen müssen.
\ifthenelse{\boolean{long}}{}{\end{comment}}

\begin{defn}[Syntax von LP ($\lng{L}$)] \quad
\begin{\whichenum}
\item $x$ ist eine Konstante wenn $x$ nur aus Kleinbuchstaben und Zahlen besteht. Eine Konstante in $\lng{L}$ ist ein logischer Term.
\item $x$ ist eine Variable wenn $x$ nur aus Buchstaben besteht und der erste Buchstabe groß geschrieben ist. Eine Variable in $\lng{L}$ ist ein logischer Term.
\item Wenn $p$ ein $n$-stelliges Prädikat ist und $t_1,\ldots,t_n$ sind logische Terme,
dann ist $p\texttt{(}t_1\texttt{,}\ldots\texttt{,}t_n\texttt{)}$ eine Atomformel.
\item Wenn $A_1,\ldots,A_k,A$ logische Terme sind, und $A$ eine Atomformel, dann ist der Ausdruck $A  \texttt{:-}  A_1  \texttt{,}  \ldots  \texttt{,}  A_k  \texttt{.}$ eine ``Regel''.
\item Wenn $A$ eine Atomformel ist, dann ist $A \texttt{.}$ (die Kurzschreibweise für $A \texttt{:-} \texttt{.}$) ein ``Fakt''.
\item Ein Programm in $\lng{L}$ besteht aus einer oder mehreren Regeln und einer Atomformel als Anfrage.
\end{\whichenum}
\end{defn}

Wir sehen, dass $\lng{L}$ völlig unabhängig von unseren bisherigen Sprachen (insbesondere der Sprache der Terme $\mathcal{T}$) ist.

\begin{defn}[Semantik von LP ($\lng{L}$)] \quad 
\begin{\whichenum}
\item Der Ausdruck $A\texttt{.}$ ist äquivalent zur Implikation $T \to A$, äquivalent zu $A$ (also ein Fakt).
\item Der Ausdruck $A  \texttt{:-}  A_1  \texttt{,}  \ldots  \texttt{,}  A_k  \texttt{.}$ ist äquivalent zur Implikation $A_1 \wedge \ldots \wedge A_k \to A$.
\item Ein Programm in $\lng{L}$ besteht aus Fakten $f_1,\ldots,f_n$ und Regeln $r_1,\ldots,r_n$. Wir nennen ein Programm auch ``Wissensbasis''.
Das Programm ist äquivalent zu einer logischen Formel $f_1 \wedge \ldots \wedge f_n \wedge r_1 \wedge \ldots \wedge r_n$.
\end{\whichenum}
\end{defn}

\begin{defn}[Literal]
Wir nennen Atomformeln auch (positive) Literale.
Negierte Atomformeln nennen wir auch (negative) Literale.
\end{defn}

\begin{defn}[Hornklausel]
Eine Klausel der Form $b_1 \vee \ldots \vee b_k$ heißt Hornklausel wenn die Anzahl der positiven (d.h. nicht-negierten)
Literale $b_i$ maximal $1$ ist.
\end{defn}

$\lng{L}$-Programme sind Und-verknüpfte Hornklauseln.

\begin{defn}[Anfragen in LP ($\lng{L}$)]
Eine Anfrage in $\lng{L}$ hat die Form $\texttt{:-}  A_1  \texttt{,}  \ldots  \texttt{,}  A_k  \texttt{.}$,
was äquivalent zur Implikation:
\[A_1 \wedge \ldots \wedge A_k \to F \; \Lra \; \neg \rbr{A_1 \wedge \ldots \wedge A_k} \vee F \; \Lra \; \neg A_1 \vee \ldots \vee \neg A_k \vee F\]
Um eine Anfrage zu beantworten wird versucht sie auf einen Widerspruch zurückzuführen.
\end{defn}

\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Schreiben Sie ein Programm in $\lng{L}$ welches die Variation der folgenden Peano-Axiome repräsentiert:
\begin{\whichenum}
\item $0$ ist eine natürliche Zahl.
\item Jede natürliche Zahl $x$ hat eine natürliche Zahl $x'$ als Nachfolger.
\item $0$ ist kein Nachfolger einer natürlichen Zahl.
\item Natürliche Zahlen mit gleichem Vorgänger sind gleich.
\end{\whichenum}

\textit{Lösung:} Wir definieren ein Prädikat \verb|nat(X)| welches wahr ist wenn $X$ eine natürliche Zahl ist.
Dazu verwenden wir eine Funktion \verb|s(X)| welche den Nachfolger einer Zahl $X$ bezeichnet.
Das Prädikat \verb|eq(X,Y)| soll wahr sein wenn \verb|X| und \verb|Y| den gleichen Vorgänger haben.
\begin{verbatim}
nat(0).
nat(s(X)) :- nat(X).
eq(0,0).
eq(s(X),s(Y)) :- eq(X,Y).
\end{verbatim}
Fall 3 ist in unserer Definition implizit erfüllt.

In Sprache können wir unser Programm so darstellen:
\begin{\whichenum}
\item \verb|0| ist eine natürliche Zahl.
\item Wenn \verb|X| eine natürliche Zahl ist, dann ist auch \verb|s(X)| eine natürliche Zahl ($\to$ Implikation).
\item \verb|0| ist gleich \verb|0|.
\item Wenn \verb|X| und \verb|Y| gleich sind, dann sind auch \verb|s(X)| und \verb|s(Y)| gleich ($\to$ Implikation).
\end{\whichenum}
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

Um Anfragen zu beantworten müssen wir einen Algorithmus definieren der ggf.
vom $\lng{L}$-Interpreter ausgeführt würde. Dazu benötigen wir Substitution und
Unification.
\begin{defn}[Variablensubstitution]
Eine Substitution $\Theta = \gbr{x_1 | t_1, \ldots, x_n | t_n}$ ist eine Menge von Paaren der Form
$x_i | t_i$, wobei $x_i$ eine Variable ist und $t_i$ ein logischer Term.
In $t_i$ darf $x_i$ nicht vorkommen. Substitutionen sind transitiv.
\end{defn}

\begin{defn}[Substitutionsanwendung]
Sei $\Theta$ eine Substitution und $t$ ein logischer Term. Einen Term
$t_{\Theta}$ erhält man, indem man für alle Paar $x_i | t_i$ in $\Theta$,
alle Vorkommnisse von $x_i$ und $t_i$ im logischen Term $t$ ersetzt.
Der Term $t_{\Theta}$ wird auch Instanz von $t$ genannt.
\end{defn}

Substitutionsanwendungen kann man sich leicht als ``Suchen und Ersetzen'' behalten.
Eine Substitution ist eine Menge von ``Suchen/Ersetzen'' Tupeln.

\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Gegeben $t=$\verb|male(X)| und $\Theta=\gbr{\texttt{X | terach}}$,
 erhält man durch Anwendung der Substitution die Instanz $t_{\Theta}=$\verb|male(terach)|.
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

Für die Beantwortung unserer Anfragen werden wir 2 Atomformeln durch geeignete Substitution
vereinheitlichen (``unify''). Wollen wir beispielsweise \verb|p(X)| und \verb|p(Y)|
vereinheitlichen, so könnten wir dies mit $\Theta_1=\gbr{\texttt{X|Y}}$, $\Theta_2=\gbr{\texttt{Y|X}}$,
$\Theta_3=\gbr{\texttt{X|a}, \texttt{Y|a}}$, etc.

Wir sehen, dass bei $\Theta_3$ nach der Substitution weniger Variablen in den
beiden Atomformeln vorkommen. Dies bedeutet eine zusätzliche Einschränkung.
Wir sind suchen meist die allgemeinsten Substitutionen die die beiden Ausdrücke vereinheitlichen.
Eine solche Substitution nennen wir MGU (Most General Unifier).

\begin{defn}[MGU] Eine Substitution ist ein MGU (Most General Unifier), wenn es keine
Substitution gibt die allgemeiner ist.
\ifthenelse{\boolean{long}}{

}{}
Eine Substitution $\Theta_1$ ist allgemeiner als eine Substitution $\Theta_2$,
wenn es eine Substitution $\Delta$ gibt, so dass $\Theta_{1,\Delta}=\Theta_2$.
\ifthenelse{\boolean{long}}{

}{}
Ein MGU ist nicht unbedingt eindeutig.
\end{defn}

\begin{algo}[Berechnung von MGU] \quad
\begin{\whichitem}
\item Input: Atomformeln $p$ und $p'$
\item Output: ``Nicht unifizierbar'' oder den MGU $\Theta$.
\item Algorithmus:
\begin{\whichenum}
\item Sei $\Theta = \gbr{}$.
\item Suche den ersten Unterschied zwischen $p$ und $p'$ und ermittle die korrespondierenden
logischen Terme $t$ und $t'$. Gibt es keinen Unterschied returniere $\Theta$ als MGU.
\begin{\whichenum}
\item Sind weder $t$ noch $t'$ Variablen, dann Abbruch: ``Nicht unifizierbar''.
\item Ist $t$ eine Variable $X$ und $t'$ enthält $X$ (oder umgekehrt), dann Abbruch: ``Nicht unifizierbar''.
\item Sonst gehe zu Schritt 3.
\end{\whichenum}
\item Definiere neues $p$, $p'$ und $\Theta$ durch:
\begin{\whichitem}
\item $p := p_{\gbr{\texttt{X|t}}}$, $p' := p'_{\gbr{\texttt{X|t}}}$,
\item $\Theta := \Theta \cup \gbr{\texttt{X|t}}$.
\end{\whichitem}
\item Gehe zu Schritt 2.
\end{\whichenum}
\end{\whichitem}
\end{algo}

\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Berechnen Sie den MGU für \verb|p(X,f(X,g(Z)),i)| und \verb|p(Y,f(V,W),V)|.

\textit{Lösung:} Entsprechend dem Algorithmus berechnen wir den MGU $\Theta$:
\begin{\whichenum}
\item $\Theta=\gbr{}$, $t=$\texttt{p({\color{red} X},f(X,g(Z)),i)} und $t'=$\texttt{p({\color{red} Y},f(V,W),V)}
\item $\Theta=\gbr{\texttt{Y|X}}$, $t=$\texttt{p(X,f({\color{red} X},g(Z)),i)} und $t'=$\texttt{p(X,f({\color{red} V},W),V)}
\item $\Theta=\gbr{\texttt{Y|X},\texttt{V|X}}$, $t=$\texttt{p(X,f(X,{\color{red} g(Z)}),i)} und $t'=$\texttt{p(X,f(X,{\color{red} W}),X)}
\item $\Theta=\gbr{\texttt{Y|X},\texttt{V|X},\texttt{W|g(Z)}}$, $t=$\texttt{p(X,f(X,g(Z)),{\color{red} i})} und $t'=$\texttt{p(X,f(X,g(Z)),{\color{red} X})}
\item $\Theta=\gbr{\texttt{Y|X},\texttt{V|X},\texttt{W|g(Z)},\texttt{X|i}}$, $t=$\texttt{p(X,f(X,g(Z)),i)} und $t'=$\texttt{p(X,f(X,g(Z)),i)}
\end{\whichenum}
\[\Theta=\gbr{\texttt{Y|X},\texttt{V|X},\texttt{W|g(Z)},\texttt{X|i}}=\gbr{\texttt{Y|i},\texttt{V|i},\texttt{W|g(Z)},\texttt{X|i}}\]
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

\begin{algo}[Beantwortung einer Anfrage in LP ($\lng{L}$)] \quad
\begin{\whichitem}
\item Input: Anfrage der Form $:- P_1, \ldots, P_n .$
\item Output: $T$ wenn die Anfrage gezeigt werden kann, sonst $F$.
\item Algorithmus:
\begin{\whichenum}
\item Bringe die Regeln in eine Reihenfolge $r_1,\ldots,r_n$.
\item Ist $:- \quad .$ die Anfrage (d.h. eine leere Anfrage), wird $T$ returniert.
\item Wähle die nächste Teilanfrage (zu Beginn $P_1$)
\item Für alle Regeln $r_i$:
\begin{\whichenum}
\item Wenn die Regel $r_i$ die Form $R :- Q_1, \ldots, Q_n .$ hat und es gibt eine Substitution $\Theta$ so dass
$P_{1,\Theta}=R_{\Theta}$ (wir sagen in diesem Fall ``Die Regel \textbf{matcht} (die Anfrage)''),
dann sei $:- Q_1, \ldots, Q_m, P_2, \ldots P_n .$ die neue Anfrage.
Wir nennen diesen Schritt \textbf{Resolution}.

Bearbeite diese rekursiv:
\begin{\whichenum}
\item Ergibt die Anfrage $T$, fahre mit nächster Teilanfrage fort (Schritt 3).
\item Andernfalls probiere die nächste Regel.
\end{\whichenum}
\item Wenn die Regel nicht matcht, dann probiere die nächste Regel.
\item Wenn es keine Regeln mehr gibt returniere $F$.
\end{\whichenum}
\end{\whichenum}
\end{\whichitem}
\end{algo}
Der Algorithmus returniert $T$ wenn ein Widerspruch in $P_1 \wedge \ldots \wedge P_n \to F$ abgeleitet werden kann.
Dann müssen alle Teilanfragen $P_i$ wahr sein. Der Algorithmus terminiert je nach Wissensbasis und Anfrage nicht (Erfüllbarkeitsproblem von Hornklauseln).

\ifthenelse{\boolean{long}}{}{\begin{comment}}
In diesem Skriptum wird die Reihenfolge der Regeln immer der im Programm entsprechen (Prolog-Variante).
Im Vorlesungsskriptum wird hingegen von einer zufälligen Reihenfolge ausgegangen.
\ifthenelse{\boolean{long}}{}{\end{comment}}

\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Gegeben ist folgendes Programm:
\begin{verbatim}
nat(0).
nat(s(X)) :- nat(X).
\end{verbatim}
Beweisen Sie die Anfrage \verb|:- nat(s(s(0))).| (``Ist 2 eine natürliche Zahl?'').

\textit{Lösung:}
\begin{\whichitem}
\item[$\blacktriangleright$] Anfrage: \verb|:- nat(s(s(0))).|
\item Resolution: 2. Regel matcht: \verb|nat(s(X')) :- nat(X').|

Wenn eine Regel matcht kennzeichnen wir jede Variable so dass sie eindeutig ist (auch wenn die Regel mehrfach matcht im Laufe des Beweises).
\item Unification: $\Theta=\gbr{\texttt{X'|s(0)}}$. \\ In die 2. Regel eingesetzt: \verb|nat(s(s(0))) :- nat(s(0)).|
\item[$\blacktriangleright$] Neue Anfrage: \verb|:- nat(s(0)).|
\item Resolution: 2. Regel matcht: \verb|nat(s(X'')) :- nat(X'').|
\item Unification: $\Theta=\gbr{\texttt{X''|0}}$. \\ In die 2. Regel eingesetzt: \verb|nat(s(0)) :- nat(0).|
\item[$\blacktriangleright$] Neue Anfrage: \verb|:- nat(0).|
\item Resolution: 1. Regel matcht: \verb|nat(0).|.

Ab hier wird der Beweis normalerweise nicht mehr aufgeschrieben, da erkennbar ist
dass nun alle Teilanfragen erfüllt sind.
\item Unification: bereits unifiziert.
\item[$\blacktriangleright$] Neue Anfrage: \verb|:- .|
\end{\whichitem}
Der Beweis ist damit erbracht, 2 ist eine natürliche Zahl.
\end{bsp}
\ifthenelse{\boolean{long}}{}{\end{comment}}

\ifthenelse{\boolean{long}}{}{\begin{comment}}
\begin{bsp}
Gegeben ist folgendes Programm:
\begin{verbatim}
nat(0).
nat(s(X)) :- nat(X).
\end{verbatim}
Ermitteln Sie für welche Werte die Anfrage \verb|:- nat(X).| wahr ist.

\textit{Lösung:} Wir schreiben $\Theta_{i,j}$ für $\Theta_{i,\Theta_{j}}$.
\begin{\whichitem}
\item[$\blacktriangleright$] Anfrage: \verb|:- nat(X).|
\item Resolution: 1. Regel matcht: \verb|nat(0).|
\item Unification: $\Theta_1=\gbr{\texttt{X|0}}$. \verb|0|, d.h. $0$ ist ein gültiger Wert.

Wir fahren jetzt so fort als hätte die 1. Regel nicht gematcht um weitere Ergebnisse zu finden.
\item Weitere Resolution: 2. Regel matcht: \verb|nat(s(X')) :- nat(X').|
\item Unification: $\Theta_2=\gbr{\texttt{X|s(X')}}$.
\item[$\blacktriangleright$] Neue Anfrage: \verb|:- nat(X').|
\item Resolution: 1. Regel matcht: \verb|nat(0).|
\item Unification: $\Theta_3=\gbr{\texttt{X'|0}}$. $\Theta_{2,3}=\gbr{\texttt{X|s(0)}}$. \verb|s(0)|, d.h. $1$ ist ein gültiger Wert.
\item Weitere Resolution: 2. Regel matcht: \verb|nat(s(X'')) :- nat(X'').|
\item Unification: $\Theta_4=\gbr{\texttt{X'|s(X'')}}$.
\item[$\blacktriangleright$] Neue Anfrage: \verb|:- nat(X'').|
\item Resolution: 1. Regel matcht: \verb|nat(0).|
\item Unification: $\Theta_5=\gbr{\texttt{X''|0}}$. $\Theta_{2,3,4,5}=\gbr{\texttt{X|s(s(0))}}$. \verb|s(s(0))|, d.h. $2$ ist ein gültiger Wert.
\end{\whichitem}
\verb|X| nimmt alle Werte $\in \N_{0}$ (dargestellt mittels der Successor-Funktion) an.
\end{bsp}

Im Vorlesungsskriptum findet sich eine alternative (graphisch unterstützte) Notation für die Beantwortung von Anfragen
in $\lng{L}$.
\ifthenelse{\boolean{long}}{}{\end{comment}}