More hboxes and page breaks.

Some drive-by fixes.

i1akku.tex

@@ -285,7 +285,7 @@ \section{Zwischenergebnisse mitführen}
        ... (invert-helper (rest list) ...) ...))))
 \end{lstlisting}
 %
-Im \lstinline{cons}-Fall müssen wir insbesondere das Argument zum zweiten
+Im \lstinline{cons}-Fall müssen wir das Argument zum zweiten
 Parameter von \lstinline{invert-helper} ergänzen: Wir sind natürlich
 versucht, da einfach \lstinline{inverted} hinzuschreiben wie bei
 vielen anderen rekursiven Funktionen vorher.  Aber wir müssen doch die
@@ -321,7 +321,7 @@ \section{Zwischenergebnisse mitführen}
                       (cons (first list) inverted))))))
 \end{lstlisting}
 %
-Die Funktion kann schon was, ist aber natürlich nicht identisch zur
+Die Funktion kann schon was, ist aber nicht identisch zur
 ursprünglichen \lstinline{invert}-Funktion, die ja nur eine Eingabe
 hat.  Um "<einfach nur eine Liste umzudrehen">, können wir
 \lstinline{invert-helper} mit einem leeren Akkumulator aufrufen, wie

i1hop.tex

@@ -710,8 +710,8 @@ \section{Higher-Order-Funktionen auf Listen}
 \end{lstlisting}
 %
 Nehmen wir an, wir wollen alle Spiele mit Beteiligung von Nürnberg
-extrahieren, indem wir \lstinline{extract-list} verwenden.  Um
-\lstinline{extract-list} zu verwenden, brauchen wir eine Funktion mit
+extrahieren, indem wir die Funktion \lstinline{extract-list}
+verwenden.  Dafür brauchen wir eine Funktion mit
 Signatur~\lstinline{(game -> boolean)}.  Die können wir folgendermaßen
 definieren:
 %
@@ -1030,7 +1030,7 @@ \section{Listen umwandeln}
 \end{lstlisting}
 %
 Wir haben zwar über zwei Funktionen abstrahiert, die sich mit Spielen
-beschäftigt.  Aber \lstinline{list-apply} hat nichts
+beschäftigen.  Aber die entstandene Funktion \lstinline{list-apply} hat nichts
 Fußball-spezifisches mehr an sich.  Wir wissen also nichts über die
 Signatur der Elemente der Eingabeliste.  Wir schreiben dort also eine
 Signaturvariable hin:
@@ -1044,15 +1044,17 @@ \section{Listen umwandeln}
 \lstinline{%element} hinschreiben:
 %
 \begin{lstlisting}
-(: list-apply ((%element -> ...) (list-of %element) -> (list-of ...)))
+(: list-apply ((%element -> ...) (list-of %element)
+               -> (list-of ...)))
 \end{lstlisting}
 %
 Die Definition von \lstinline{list-apply} legt auch für das Ergebnis
 von  \lstinline{f} keine Signatur fest.  Wir schreiben also auch da
 eine Signaturvariable hin:
 %
 \begin{lstlisting}
-(: list-apply ((%element -> %result) (list-of %element) -> (list-of ...)))
+(: list-apply ((%element -> %result) (list-of %element)
+               -> (list-of ...)))
 \end{lstlisting}
 %
 Es fehlt nur noch die Signatur für die Elemente der Ergebnisliste.
@@ -1061,7 +1063,8 @@ \section{Listen umwandeln}
 ist.  Dort muss deshalb auch \lstinline{%result} hin:
 %
 \begin{lstlisting}
-(: list-apply ((%element -> %result) (list-of %element) -> (list-of %result)))
+(: list-apply ((%element -> %result) (list-of %element)
+               -> (list-of %result)))
 \end{lstlisting}
 %
 Bei solchen Signaturen, in denen überhaupt nichts über die

i1lambda.tex

@@ -58,9 +58,9 @@ \section{Was hat ein alter "<Kalkül"> mit Programmieren zu tun?}
 Als Teil dieses Projekts entwickelte er die Programmiersprache
 LISP~\cite{McCarthy1960}.  Als ausgebildeter Mathematiker suchte
 McCarthy dafür Inspiration in der Mathematik.  Mathematische Notation
-hat das Problem, dass sie schrecklich vielfältig ist.  Die gleiche
-Notation wird in unterschiedlichen Kontexten für unterschiedliche
-Zwecke benutzt.  Allgemein mathematische Notation für den Computer
+hat das Problem, dass die gleiche
+Notation in unterschiedlichen Kontexten für unterschiedliche
+Zwecke benutzt wird.  Allgemein mathematische Notation für den Computer
 verständlich zu machen, ist darum extrem aufwendig und war für
 McCarthy undenkbar, der es mit Computern zu tun hatte, die nur einen
 winzigen Bruchteil der heutigen Rechen- und Speicherkapazität haben.
@@ -217,20 +217,21 @@ \section{Die Sprache des $\lambda$-Kalküls}
 eine Applikation~-- nach der öffnenden Klammer steht ein weitere
 Klammer, das $\lambda$ kommt erst danach.
 %
-\begin{aufgabeinline}
+\begin{aufgabe}
   Klassifiziere, ob es sich jeweils um eine
   Variable, eine Applikation oder eine Abstraktion handelt:
   \begin{displaymath}
-    \begin{array}{c}
+  \begin{array}[b]{c}
       \lrm y\\
       (\lrm x~\lrm y)\\
       (\lambda \lrm x.\lrm y)\\
       ((\lambda \lrm x.\lrm y)~f)\\
       \lrm f\\
       (\lrm f~(\lambda \lrm x.\lrm y))
-    \end{array}
+  \end{array}\tag*{$\square$} % hack because \begin{array}[b] and \qed
+                              % don't get along
   \end{displaymath}
-\end{aufgabeinline}
+\end{aufgabe}
 % 
 Manchmal sprechen wir aber auch über
 $\lambda$-Terme einer bestimmten Form im Allgemeinen, zum Beispiel
@@ -307,8 +308,8 @@ \section{Die Sprache des $\lambda$-Kalküls}
 \item $e_0 \ldots e_n$ steht für $(\ldots(e_0~e_1)~e_2) \ldots e_n)$.
 \end{itemize}
 %
-Dementsprechend ist $\lambda \lrm{fxy}.\lrm f~\lrm x~\lrm y$ eine andere Schreibweise für
-den folgenden Term \[(\lambda \lrm f.(\lambda \lrm x.(\lambda \lrm y.((\lrm f~\lrm x)~\lrm y))))\]
+$\lambda \lrm{fxy}.\lrm f~\lrm x~\lrm y$ ist also eine andere Schreibweise für
+den Term $(\lambda \lrm f.(\lambda \lrm x.(\lambda \lrm y.((\lrm f~\lrm x)~\lrm y))))$.
 
 Hier sind weitere Beispiele für Terme und ihre Abkürzungen:
 %
@@ -323,17 +324,17 @@ \section{Die Sprache des $\lambda$-Kalküls}
   \end{array}
 \end{displaymath}
 %
-\begin{aufgabeinline}
+\begin{aufgabe}
   Schreibe für die folgenden Abkürzungen die "<vollständigen">
   $\lambda$-Terme auf:
 \begin{displaymath}
   \begin{array}{c}
     \lrm f~\lrm x~\lrm y~\lrm z\\
     \lambda \lrm x\lrm y\lrm z.\lrm x~\lrm y~\lrm z\\
     ((\lambda \lrm x\lrm y.\lrm x~\lrm y)~\lrm a~\lrm b)
-  \end{array}  
+  \end{array}
 \end{displaymath}
-\end{aufgabeinline}
+\end{aufgabe}
 
 \section{$\lambda$-Intuition}
 
@@ -436,8 +437,8 @@ \section{Wie funktionieren Variablen?}
 \emph{bindet} eine Variable innerhalb seines Rumpfes.  Eine freie
 Variable hingegen ist eine, die nicht durch eine Abstraktion gebunden
 ist.  Darum bildet $\free$ bei einer Abstraktion die Differenz aus den
-freien Variablen und der gebundenen
-Variable.  Dahingegen sammelt $\bound$ alle Variablen aus
+freien und den gebundenen
+Variablen.  Dahingegen sammelt $\bound$ alle Variablen aus
 Abstraktionen auf.  Wenn man $\free$ und $\bound$ eines Terms als
 $\free(e)\cup\bound(e)$ zusammennimmt, bekommt man alle Variablen
 eines $\lambda$-Terms.
@@ -456,11 +457,11 @@ \section{Wie funktionieren Variablen?}
 immer auf bestimmte Vorkommen\index{Vorkommen} einer Variablen in
 einem $\lambda$-Term.
 %
-\begin{aufgabeinline}
+\begin{aufgabe}
   Schreibe auf, was bei folgenden Anwendungen von $\free$ und $\bound$
   herauskommt:
   \begin{displaymath}
-    \begin{array}{c}
+    \begin{array}[b]{c}
       \free(\lrm x~\lrm y)\\
       \free(\lambda \lrm x.\lrm x~\lrm y)\\
       \free(\lambda \lrm x\lrm y.\lrm x~\lrm y)\\
@@ -469,9 +470,9 @@ \section{Wie funktionieren Variablen?}
       \bound(\lambda \lrm x.\lrm x~\lrm y)\\
       \bound(\lambda \lrm x\lrm y.\lrm x~\lrm y)\\
       \bound((\lambda\lrm x.\lrm y)~\lrm x)
-    \end{array}
+    \end{array}\tag*{$\square$}
   \end{displaymath}
-\end{aufgabeinline}
+\end{aufgabe}
 %
 Der $\lambda$-Kalkül ist darauf
 angewiesen, Variablen durch andere zu ersetzen, ohne dabei die
@@ -1091,14 +1092,14 @@ \section{Auswertungsstrategien}
 \section{Der $\lambda$-Kalkül als Programmiersprache}
 \label{sec:lambdaprog}
 
-Bisher muss es für Dich so ausgesehen haben, als könne man mit dem
-$\lambda$-Kalkül eigentlich nichts anfangen: Die drei Arten von
+Bisher sieht es so aus, als könne man mit dem
+$\lambda$-Kalkül nichts anfangen: Die drei Arten von
 $\lambda$-Termen entsprechen zwar den Abstraktionen, Applikationen und
-Variablen aus den Lehrsprachen, aber alles andere fehlt.  Dazu gehört
+Variablen aus den Lehrsprachen, aber alles andere fehlt,
 zum Beispiel das Rechnen mit Zahlen, aber auch boolesche Werte und
 Verzweigungen. Wir könnten das alles zum $\lambda$-Kalkül hinzufügen,
-was aber den Kalkül komplizierter macht und damit auch erschwert,
-wichtige Eigenschaften des Kalküls zu zeigen.
+was aber den Kalkül komplizierter macht und damit erschwert,
+wichtige Eigenschaften des Kalküls zu beweisen.
 
 Wir können aber auch versuchen, die fehlenden Konstrukte innerhalb des
 Kalküls nachzubilden.  Wir wissen ja zum Beispiel, dass wir Funktionen
@@ -1131,12 +1132,14 @@ \subsection{Verzweigungen und boolesche Werte}
 Die Verzweigung wendet die Bedingung
 auf Konsequente und Alternative an:
 %
-\begin{align*}
+\begin{displaymath}
+\begin{array}{rl}
   \mathbf{true} & \deq{} \lambda \lrm x \lrm y.\lrm x \\
   \mathbf{false} & \deq{} \lambda \lrm x \lrm y.\lrm y\\
   \mathbf{if} & \deq{} \lambda \lrm t \lrm k \lrm a.\lrm t~\lrm k~\lrm a
-\end{align*}
-%
+\end{array}
+\end{displaymath}
+% 
 Wie $\mathbf{if}$\index{if@$\mathbf{if}$} funktioniert,
 zeigt das folgende Beispiel:
 %
@@ -1182,8 +1185,8 @@ \subsection{Natürliche Zahlen}
 $\lceil 2\rceil$ ist $\lambda \lrm f.\lambda \lrm x.\lrm f~(\lrm
 f~\lrm x)$ usw.
 
-Die Nachfolgeroperation\index{Nachfolger} $\mathbf{succ}$, die auf
-eine Zahl eins addiert, macht eine Applikation dazu:\index{succ@$\mathbf{succ}$}
+Hier ist die Definition der \textit{Nachfolgerfunktion}\index{Nachfolger} $\mathbf{succ}$, die auf
+eine Zahl eins addiert. Sie macht eine Applikation dazu:\index{succ@$\mathbf{succ}$}
 %
 \begin{displaymath}
   \mathbf{succ} \deq{} \lambda \lrm n.\lambda \lrm f.\lambda \lrm x.\lrm n~\lrm f~(\lrm f~\lrm x)
@@ -1206,8 +1209,8 @@ \subsection{Natürliche Zahlen}
   &=& \lceil 2\rceil
 \end{eqnarray*}
 %
-Folgende Definition berechnet die Vorgängerfunktion,
-die von einer Zahl eins abzieht:\index{Vorgänger}\index{pred@$\mathbf{pred}$}
+Folgende Definition berechnet das Gegenteil der Nachfolgerfunktion, die \textit{Vorgängerfunktion}.\index{Vorgänger}
+Sie zieht von einer Zahl eins ab:\index{Vorgänger}\index{pred@$\mathbf{pred}$}
 %
 \begin{displaymath}
   \mathbf{pred} \deq{} \lambda \lrm x.\lambda \lrm y.\lambda \lrm z.\lrm x~(\lambda \lrm p.\lambda
@@ -1218,8 +1221,8 @@ \subsection{Natürliche Zahlen}
   Zeige, dass $\mathbf{pred}~\lceil 3\rceil$ zu $\lceil 2\rceil$ reduziert!
 \end{aufgabeinline}
 %
-In Verbindung mit den booleschen Werten lässt sich eine Zahl daraufhin
-testen, ob sie $0$ ist:\index{zerop@$\mathbf{zerop}$}
+In Verbindung mit den booleschen Werten test die folgende Funktion
+$\mathbf{zerop}$ eine Zahl darauf, ob sie $0$ ist:\index{zerop@$\mathbf{zerop}$}
 %
 \begin{displaymath}
   \mathbf{zerop} \deq{} \lambda \lrm n.\lrm n~(\lambda \lrm x.\mathbf{false})~\mathbf{true}
@@ -1273,9 +1276,8 @@ \subsection{Rekursion und Fixpunktsatz}
   x)~\lceil 1\rceil ~(\ast~\lrm x~(\mathbf{fac}~(\mathbf{pred}~\lrm x)))
 \end{displaymath}
 %
-% "=" kommt hier nicht vor, meinst du "zerop" ?
-$\ast$ und $\mathbf{zerop}$ stehen dabei für $\lambda$-Terme, die Church-Numerale
-vergleichen beziehungsweise multiplizieren.  Wir tun mal so, als
+$\ast$ steht für einen $\lambda$-Terme, der Church-Numerale
+multipliziert.  Wir tun so, als
 hätten wir die schon definiert~-- ihre Formulierung ist Teil der
 Übungsaufgabe~\ref{ex:church}.
 
@@ -1330,11 +1332,10 @@ \subsection{Rekursion und Fixpunktsatz}
 dabei trotzdem nie ein Term, der die Fakultäten \emph{aller}
 natürlichen Zahlen berechnen kann, da die Terme immer endlich groß
 bleiben.
-
-Immerhin aber enthalten alle $\mathbf{fac}_n$-Terme das
-gleiche Muster und unterscheiden sich nur durch Aufruf von
-$\mathbf{fac}_{n-1}$, das jedesmal anders ist.  Wir wenden deshalb Abstraktion
-auf das Problem an und definieren folgenden Term $\mathbf{FAC}$:
+Immerhin unterscheiden sich die $\mathbf{fac}_n$-Terme 
+nur durch den Aufruf von
+$\mathbf{fac}_{n-1}$, der jedesmal anders ist.  Wir abstrahieren
+deshalb und definieren folgenden Term $\mathbf{FAC}$:
 %
 \begin{displaymath}
   \mathbf{FAC} \deq{} \lambda\mathbf{fac}.\lambda \lrm x.\mathbf{if}~(\mathbf{zerop}~\lrm x)~1~(\ast~\lrm x~(\mathbf{fac}~(\mathbf{pred}~\lrm x)))
@@ -1343,14 +1344,15 @@ \subsection{Rekursion und Fixpunktsatz}
 Nun können wir die
 $\mathbf{fac}_n$-Funktionen mit Hilfe von $\mathbf{FAC}$ einfacher beschreiben:
 %
-\begin{eqnarray*}
+\begin{displaymath}
+\begin{array}{rcl}
    \mathbf{fac}_0 &\deq{}& \lambda \lrm x.\mathbf{if}~(\mathbf{zerop}~\lrm x)~\lceil 1\rceil~(\ast~\lrm x~(?~(\mathbf{pred}~\lrm x)))\\
    \mathbf{fac}_1 &\deq{}& \mathbf{FAC}~\mathbf{fac}_0\\
-   \mathbf{fac}_2 &\deq{}& \mathbf{FAC}~\mathbf{fac}_1\\
-   \mathbf{fac}_3 &\deq{}& \mathbf{FAC}~\mathbf{fac}_2\\
+   \mathbf{fac}_2 &\deq{}& \mathbf{FAC}~\mathbf{fac}_1\\[-2ex]
    &\ldots&
-\end{eqnarray*}
-%
+\end{array}
+\end{displaymath}
+% 
 $\mathbf{FAC}$ ist also eine Fabrik für Fakultätsfunktionen und
 teilt mit allen $\mathbf{fac}_i$ die Eigenschaft, dass ihre
 Definition nicht rekursiv ist.
@@ -1381,8 +1383,8 @@ \subsection{Rekursion und Fixpunktsatz}
   Für jeden $\lambda$-Term $F$ gibt es einen $\lambda$-Term $X$ mit
   $F~X\equiv X$.
 \end{satz}
-\begin{beweis}
-  Wähle $X \deq{} \mathbf{Y}~F$, wobei
+
+\noindent\textbf{Beweis:}  Wähle $X \deq{} \mathbf{Y}~F$, wobei
   %
   \begin{displaymath}
     \mathbf{Y} \deq{} \lambda \lrm f.(\lambda \lrm x.\lrm f~(\lrm x~\lrm x))~(\lambda \lrm x.\lrm f~(\lrm x~\lrm x)).
@@ -1391,7 +1393,7 @@ \subsection{Rekursion und Fixpunktsatz}
   Dann gilt:
   %
   \begin{displaymath}
-    \begin{split}
+    \begin{array}[b]{rl}
       \mathbf{Y}~F & = (\lambda \lrm f.(\lambda \lrm x.\lrm f~(\lrm x~\lrm x))~(\lambda \lrm x.\lrm f~(\lrm x~\lrm x)))~F
       \\ & \rightarrow_\beta
       (\lambda \lrm x.F~(\lrm x~\lrm x))~(\lambda \lrm x.F~(\lrm x~\lrm x))
@@ -1401,9 +1403,8 @@ \subsection{Rekursion und Fixpunktsatz}
       F~((\lambda \lrm f.(\lambda \lrm x.\lrm f~(\lrm x~\lrm x))~(\lambda \lrm x.\lrm f~(\lrm x~\lrm x)))~\lrm F)
       \\ & =
       F~(\mathbf{Y}~F)
-    \end{split}
+    \end{array}\tag*{$\square$}
   \end{displaymath}
-\end{beweis}
 %
 Der $\lambda$-Term $\mathbf{Y}$\index{Y@$\mathbf{Y}$}, der Fixpunkte
 berechnet, heißt
@@ -1478,13 +1479,13 @@ \subsection{Rekursion und Fixpunktsatz}
   \end{center}
 \end{figure}
 
-Natürlich gibt es immer noch Elemente "<richtiger">
+Es gibt immer noch Elemente von
 Programmiersprachen, die wir in diesem Kapitel nicht in den
 $\lambda$-Kalkül abgebildet haben, zum Beispiel globale Definitionen,
 Zeichenketten oder
-Signaturen.  All dies ist aber prinzipiell möglich.  Der
-$\lambda$-Kalkül ist deshalb ein sehr einflussreiches Modell für die
-Programmierung und dient als Grundlage für große Teile der
+Signaturen.  All dies ist aber prinzipiell möglich.  Das macht
+$\lambda$-Kalkül zu einem nützlichen Modell für die
+Programmierung und zur Grundlage großer Teile der
 Programmiersprachenforschung.
 
 In anderen Teilen der Informatik ist ein alternatives Modell für
@@ -1497,7 +1498,7 @@ \subsection{Rekursion und Fixpunktsatz}
 theoretischen Informatik eine wichtige Rolle
 spielt.\index{berechenbare Funktionen}
 
-\vfill % formatting hack
+\newpage
 
 \section*{Übungsaufgaben}
 
@@ -1575,7 +1576,6 @@ \section*{Übungsaufgaben}
          ((zero? n) 1)
          ((positive? n)
           (* n (fac (- n 1)))))))))
-
 (FAC 3)
 \end{lstlisting}
   %

i1list.tex

@@ -596,10 +596,12 @@ \section{Listen mit anderen Elementen}
 
 Bevor das Programm wieder
 funktioniert, müssen wir noch ein kleines Problem
-beheben: \lstinline{list-of-numbers} ist nicht mehr
+beheben:
+
+\lstinline{List-of-numbers} ist nicht mehr
 definiert, steht aber noch in den Signatur"=Deklarationen von
 \lstinline{list-sum} und \lstinline{list-product}.  Wir können
-entweder dort \lstinline{list-of-numbers} durch \lstinline{(list-of number)}
+entweder \lstinline{list-of-numbers} durch \lstinline{(list-of number)}
 ersetzen oder eine Signatur-Definition
 dazuschreiben:
 %
@@ -1008,7 +1010,7 @@ \subsection{Gürteltiere extrahieren}
 \end{lstlisting}
 %
 Auch, wenn wir den rekursiven Aufruf \lstinline{(live-dillos (rest dillos))}
-scheinbar "<verbraucht"> haben~-- im  anderen Zweig (Gürteltier lebt
+scheinbar schon "<verbraucht"> haben~-- im  anderen Zweig (Gürteltier lebt
 (noch)) brauchen wir die restlichen lebendigen Gürteltiere noch
 einmal.  Wir müssen diesmal aber darauf achten, dass wir das erste
 Gürteltier in der Ausgabe wieder unterbringen und vorn an die
@@ -1484,7 +1486,7 @@ \section*{Aufgaben}
 
   \begin{enumerate}
   \item Führe eine Datenanalyse für
-    Ackerbestandteile durch und schreibe passende Daten- und
+    Ackerbestandteile durch und schreibe dazu passende Daten- und
     Record-Definitionen.  Gib ein paar Beispiele für
     Ackerbestandteile an, die Du in den nächsten Teilaufgaben in
     Testfällen verwenden kannst.