%%%
% Neue Aufgabe. Der Befehl nimmt 3 Parameter: Aufgabennummer, Autor und
% Übungsleiter/Tag/Uhrzeit der Übung
%%%
\aufgabe{2}{Autor}{Übungsleiter/Tag/Uhrzeit}

%%%
% Gliederung der Aufgabe in Paragraphen
%%%

\paragraph{Aufgabestellung:}

Wir betrachten das folgende funktionale Programm (gegeben in Haskell-Syntax):

%%%
% Ein Algorithmus
%%%

\begin{lstlisting}
    data List a = Nil | Cons a (List a)

    error = error

    head Nil = error
    head (Cons a as) = a

    tail Nil = Nil
    tail (Cons a as) = as
\end{lstlisting}

%%%
% Auflistungen
%%%

\begin{enumerate}
   \item Dr\"ucken Sie die f\"ur dieses Programm m\"oglichen Transitionen als
         Termersetzungssystem \"uber der Signatur
         $\Sigma=\{\text{\lstinline{Nil}},\text{\lstinline{Cons}},
          \text{\lstinline{head}},\text{\lstinline{tail}},
          \text{\lstinline{error}}\}$ aus.
   \item Identifizieren Sie alle Redexe in dem folgenden (als $\Sigma$-Term zu
         interpretierenden) Ausdruck:
     \begin{center}
       \lstinline{head (Cons (head (Cons (tail Nil) (head Nil))) (Cons (tail Nil) error))}
     \end{center}
   \item Die \emph{Auswertungsstrategie} einer Programmiersprache ist der Teil
         ihrer Semantik, der die Reihenfolge festlegt, in welcher Teile von
         zusammengesetzten Ausdr\"ucken bzw. Aussagen berechnet werden sollen.
         Eine M\"oglichkeit, dies zu formalisieren ist die Angabe einer
         "Reduktionsstrategie", das hei\ss t, festzulegen, welcher der Redexe
         eines gegebenen Terms als n\"achstes reduziert werden soll.
    \begin{enumerate}
      \item Die bei Programmiersprachen am weitesten verbreitete
            Auswertungsstrategie ist die sogenannte \emph{strikte} (engl.
            \emph{eager} oder \emph{strict}) Auswertung. Sie entspricht
            \"ublicherweise der \emph{leftmost-innermost-Reduktion}, die auch
            als \emph{applikative Reduktion} bezeichnet wird:
            Es wird jeweils der erste Redex reduziert, der bei einer
            \emph{post-order}-Traversierung des Term-Baumes
            auftritt. Zeigen Sie, da\ss~der obige Ausdruck unter
            leftmost-innermost-Reduktion divergiert.
      \item Einige Programmiersprachen (darunter auch Haskell) verwenden eine
            nicht-strikte Auswertungsstrategie. Eine solche Strategie entsteht
            bespielsweise bei Verwendung der
            \emph{lefmost-outermost-Reduktion} (auch als \emph{normale
            Reduktion} bezeichnet), bei welcher der erste bei einer
            \emph{pre-order}-Traversierung des Term-Baumes auftretende Redex
            reduziert wird. Zeigen Sie, da\ss~der obige Ausdruck unter
            leftmost-outermost-Reduktion zu einer Normalform reduziert.
    \end{enumerate}
\end{enumerate}

\paragraph{L\"osung zu Teilaufgabe 1.:}

Es gen\"ugt, die Gleichungen des Programmcodes als Reduktionsregeln
f\"ur Terme \"uber der Signatur
$\Sigma=\{\text{\lstinline{Nil}},\text{\lstinline{Cons}},
\text{\lstinline{head}},\text{\lstinline{tail}},\text{\lstinline{error}}\}$
(f\"ur $V=\{a,as\}$) aufzufassen:

%%%
% Ausgerichtete, nummerierte Formeln
%%%

  \begin{align}
      \text{\lstinline{error}} & \to_0 \text{\lstinline{error}}
       \label{eq:nt-1}\\
      \text{\lstinline{head Nil}} & \to_0 \text{\lstinline{error}}
       \label{eq:nt-2}\\
      \text{\lstinline{head (Cons a as)}} & \to_0 \text{\lstinline{a}}
       \label{eq:nt-3}\\
      \text{\lstinline{tail Nil}} & \to_0 \text{\lstinline{Nil}}
       \label{eq:nt-4}\\
      \text{\lstinline{tail (Cons a as)}} & \to_0 \text{\lstinline{as}}
       \label{eq:nt-5}
  \end{align}

\paragraph{L\"osung zu Teilaufgabe 2.:}

Die Wurzeln der einzelnen Redexe des gegebenen Ausdrucks
$t=\text{\lstinline{head (Cons (head (Cons (tail Nil)
(head Nil))) (Cons (tail Nil) error))}}$ sind in dem in Abb.~\ref{fig:redexes}
dargestellten Termbaum markiert. Ein Redex entspricht also dem an der jeweils
markierten Stelle beginnenden Unterbaum des Termbaums.
Weiterhin ist an jeder Markierung angegeben, aus welcher Reduktionsregel der
entsprechende Redex hervorgeht. 

%%%
% Ein Baum
%%%

      \begin{figure}
       \begin{center}
        \begin{tikzpicture}[ node distance=2cm ]
              \node [draw,label=right:\eqref{eq:nt-3}] (o) {head};

              \node [below of=o] (oo) {Cons};
                \node [below left
                 of=oo,xshift=-1cm,draw,label=right:
                 \eqref{eq:nt-3}] (ool)  {head};
                \node [below of=ool] (oolo) {Cons};
                  \node [below left of=oolo,draw,label=right:
                  \eqref{eq:nt-4}] (oolol) {tail};
                     \node [below of=oolol] (oololo) {Nil};
                  \node [below right of=oolo,draw,label=right:
                  \eqref{eq:nt-2}] (oolor) {head};
                     \node [below of=oolor] (ooloro) {Nil};


                \node [below right of=oo,xshift=1cm] (oor) {Cons};
                  \node [below left of=oor,draw,label=right:
                  \eqref{eq:nt-4}]  (oorl)  {tail};
                    \node [below of=oorl] (oorlo) {Nil};
                  \node[below right of=oor,draw,label=right:
                  \eqref{eq:nt-1}] (oorr) {error};

                \draw (o) to (oo);
                  \draw (oo) to (ool);
                    \draw (ool) to (oolo);
                      \draw (oolo) to (oolol);
                         \draw (oolol) to (oololo);
                      \draw (oolo) to (oolor);
                         \draw (oolor) to (ooloro);
                  \draw (oo) to (oor);
                    \draw (oor) to (oorl);
                      \draw (oorl) to (oorlo);
                    \draw (oor) to (oorr);
        \end{tikzpicture}
       \end{center}
      \caption{Termbaum von $t$; die Wurzeln der Redexe von $t$
               sind durch Rechtecke markiert}
        \label{fig:redexes}
      \end{figure}
      
      
\paragraph{L\"osung zu Teilaufgabe 3.a):}

Unter Anwendung von applikativer (leftmost-innermost-)Reduktion erhalten wir
die folgende unendliche Reduktionskette (wobei in jedem Schritt der jeweils
ausgew\"ahlte Redex unterstrichen und die jeweils angewendete Regel angegeben
ist):

 \begin{align*}
   & \text{\lstinline{head (Cons (head (Cons (}}
                  \underline{\text{\lstinline{tail Nil}}}
                  \text{\lstinline{) (head Nil))) (Cons (tail Nil) error))}} &
                   \text{Regel }\eqref{eq:nt-4}\\
   \to & \text{\lstinline{head (Cons (head (Cons Nil (}}
        \underline{\text{\lstinline{head Nil}}}
        \text{\lstinline{))) (Cons (tail Nil) error))}} &
         \text{Regel }\eqref{eq:nt-2}\\
   \to & \text{\lstinline{head (Cons (head (Cons Nil (}}
        \underline{\text{\lstinline{error}}}
        \text{\lstinline{))) (Cons (tail Nil) error))}} & 
        \text{Regel }\eqref{eq:nt-1}\\
   \to & \text{\lstinline{head (Cons (head (Cons Nil (}}
        \underline{\text{\lstinline{error}}}
        \text{\lstinline{))) (Cons (tail Nil) error))}} & 
        \text{Regel }\eqref{eq:nt-1}\\
   \to & \ldots
 \end{align*}
        
  
\paragraph{L\"osung zu Teilaufgabe 3.b):}

Unter Anwendung von normaler (leftmost-outermost-)Reduktion erhalten wir die
folgende in einer Normalform endende Reduktionskette (wobei in jedem Schritt
der jeweils ausgew\"ahlte Redex unterstrichen und die jeweils angewendete
Regel angegeben ist):

 \begin{align*}
   & 
        \underline{\text{\lstinline{head (Cons (head (Cons (tail Nil) 
        (head Nil))) (Cons (tail Nil) error))}}}
                   & \text{Regel }\eqref{eq:nt-3}\\
   \to & \underline{\text{\lstinline{head (Cons (tail Nil) (head Nil))}}}
                   & \text{Regel }\eqref{eq:nt-3}\\
   \to & \underline{\text{\lstinline{tail Nil}}}
                   & \text{Regel }\eqref{eq:nt-4}\\
   \to & \text{\lstinline{Nil}}\\
   \not\to
 \end{align*}
        