zustand.tex

\chapter{Zuweisungen und Zustand}

Die SECD-Maschine
kennt keine Zuweisungen; es folgt darum noch die Darstellung der
\textit{SECDH-Maschine}, die auch einen \textit{Speicher} kennt und
damit Zuweisungen korrekt modelliert.

\section{Der $\lambda$-Kalkül mit Zustand}

Der bisher vorgestellte $\lambda$-Kalkül liefert keinerlei Erklärung
für das Verhalten von Zuweisungen.  Tatsächlich hat sich schon in
Abschnitt~\ref{sec:assignment-problems} angedeutet, dass Zuweisungen
die Formalisierung deutlich erschweren.  Möglich ist es trotzdem, und
dieser Abschnitt zeigt, wie es geht.

Als erstes muss wieder einmal die Sprache des $\lambda$-Kalküls
erweitert werden, diesmal um \lstinline{set!}-Ausdrücke:
%
\begin{definition}[Sprache des angewandten $\lambda$-Kalküls mit Zustand
  $\mathcal{L}_{\lambda{}S}$]\index{angewandter $\lambda$-Kalkül}\index{Zustand}
  Sei $V$ eine abzählbare Menge von Variablen.  Sei $B$ eine Menge von
  \textit{Basiswerten\index{Basiswert}} mit $\mathtt{void} \in B$.
  Sei für eine natürliche Zahl $n$ und $i \in \{1, \ldots, n\}$
  jeweils $\Sigma^i$ eine Menge von \textit{$i$-stelligen
    Primitiva\index{Primitivum}}.  Jedem $F^i\in\Sigma^i$ ist eine
  $i$-stellige Funktion $F_B^i: B\times\ldots\times B \rightarrow
  B$~-- ihre \textit{Operation}~-- zugordnet.
  Seit $A$ eine abzählbare Menge von Adressen mit $V\cap A =
  \varnothing$.\index{Adresse}. 

  Die Sprache des angewandten $\lambda$"=Kalküls mit Zustand, die
  Menge der \textit{angewandten $\lambda$-Terme mit Zustand},
  $\mathcal{L}_{\lambda{}S}$\index{L@$\mathcal{L}_{\lambda{}S}$}, ist
  durch folgende Grammatik definiert:
  \begin{grammar}
    \meta{$\mathcal{L}_{\lambda{}S}$} \: \meta{$V$}
    \> \| (\meta{$\mathcal{L}_{\lambda{}S}$} \meta{$\mathcal{L}_{\lambda{}S}$})
    \> \| ($\lambda$\meta{$V$}.\meta{$\mathcal{L}_{\lambda{}S}$})
    \> \| \meta{$B$}
    \> \| (\meta{$\Sigma^1$}~\meta{$\mathcal{L}_{\lambda{}S}$})
    \> \| (\meta{$\Sigma^2$}~\meta{$\mathcal{L}_{\lambda{}S}$}~\meta{$\mathcal{L}_{\lambda{}S}$})
    \> \ldots
    \> \| (\meta{$\Sigma^n$}~\meta{$\mathcal{L}_{\lambda{}S}$}~\ldots~\meta{$\mathcal{L}_{\lambda{}S}$})  \quad \textrm{($n$-mal)}
    \> \| (set! \meta{V} \meta{$\mathcal{L}_{\lambda{}S}$})
  \end{grammar}
  %
\end{definition}
%
Der \lstinline{void}-Wert wird als Rückgabewert von
\lstinline{set!}-Ausdrücken dienen.

Um Reduktionsregeln für Zuweisungen zu bilden, ist es notwendig, den
Begriff des \textit{Speichers\index{Speicher}} in den $\lambda$-Kalkül
einzuführen: Im $\lambda$-Kalkül mit Zustand stehen Variablen nicht
mehr für Werte, die für sie eingesetzt werden können, sondern für
\textit{Speicherzellen\index{Speicherzelle}}.  Eine Speicherzelle ist
ein Ort im Speicher, der einen Wert aufnimmt, der auch wieder
verändert werden kann.  Dabei wird jede Speicherzelle durch eine
\textit{Adresse\index{Adresse}} identifiziert.  Eine Adresse ist eine
abstrakte Größe, es kommt also gar nicht darauf an, um was für
eine Art Wert es sich handelt~-- im realen Computer ist eine Adresse
in der Regel einfach eine Zahl.  In diesem Abschnitt steht $A$ für die
Menge der Adressen, die abzählbar sein sollte.

Ein Speicher aus der Menge $M$ ist eine Zuordnung zwischen Adressen aus $A$
und Werten\index{Wert}.  Die Werte sind wie schon im normalen
$\lambda$-Kalkül die Basiswerte und die Abstraktionen~-- hier bekommen
sie, weil sie eine Rolle in den Reduktionsregeln spielen, den Namen
$X$:
%
\begin{eqnarray*}
  M &=& \mathcal{P}(A\times X)\\
  X &=& B \cup \{ \lambda v.e | \lambda v.e \in \mathcal{L}_{\lambda{}S} \}
\end{eqnarray*}

Um Reduktionsregeln für den $\lambda$-Kalkül mit Zustand zu
formulieren, muss $\mathcal{L}_{\lambda{}S}$ noch erweitert werden,
damit die Adressen ins Spiel kommen: Adressen werden Terme und sind
auf der linken Seite von Zuweisungen zulässig:
%
\begin{grammar}
  \meta{$\mathcal{L}_{\lambda{}S}$} \: \ldots
  \> \| \meta{A}
  \> \| (set! \meta{A} \meta{$\mathcal{L}_{\lambda{}S}$})
\end{grammar}
%
Adressen tauchen dabei nur als Zwischenschritte bei der Reduktion auf;
sie sind nicht dafür gedacht, dass sie der Programmierer in ein
Programm schreibt.

Da das bisherige Substitutionsprinzip bei Zuweisungen nicht mehr funktioniert, reicht es
nicht, die Reduktionsregeln für den $\lambda$-Kalkül mit Zustand
einfach nur auf Termen auszudrücken: Ein Term, der ja Adressen
enthalten kann, ergibt nur Sinn, wenn er mit einem Speicher kombiniert
wird.  Die Reduktionsregeln überführen somit immer ein Paar, bestehend aus
einem Term und einem Speicher in ein ebensolches Paar.  Hierbei wird der
Einfachheit halber kein Unterschied mehr zwischen den verschiedenen
Arten der Reduktion gemacht:
%
\begin{eqnarray*}
  b, m &\rightarrow& a, m[a\mapsto b] \textrm{ wobei $a$ frisch}
  \\
  \lambda v.e, m &\rightarrow&
  a, m[a\mapsto \lambda v.e]  \textrm{ wobei $a$ frisch}
  \\
  (a_0~a_1), m &\rightarrow& e[v\mapsto a], m[a\mapsto m(a_1)]
  \textrm{ wobei $m(a_0) = \lambda v.e$ und $a$ frisch} 
  \\
  (\mathtt{set!}~a_0~a_1), m &\rightarrow& \mathtt{void}, m[a_0\mapsto m(a_1)]
  \\
  (F^k a_1 \ldots a_k), m &\rightarrow& a, m[a\mapsto F_B(b_1, \ldots, b_k)] \textrm{
    wobei $b_i = m(a_i) \in B$, $a$ frisch}
\end{eqnarray*}
%
Die Formulierung "<$a$ frisch"> bedeutet dabei, dass $a$ eine Adresse
sein sollte, die in $m$ bisher noch nicht benutzt wurde.  Die Operation
$m[a\mapsto x]$ ist ähnlich wie bei Umgebungen definiert: der alte
Speicherinhalt bei $a$ wird zunächst entfernt, und dann eine neue
Zuordnung für $a$ nach $x$ hinzugefügt:
%
\begin{displaymath}
  m[a\mapsto x] \deq (e \setminus \{ (a, x') | (a, x') \in m) \cup \{
    (a, x) \}
\end{displaymath}
%
Die Regeln sind immer noch über Substitution definiert, allerdings
werden für Variablen jetzt nicht mehr Werte sondern Adressen
eingesetzt.  Sie werden, wie beim normalen Call-by-Value-Kalkül auch,
auf Subterme fortgesetzt, die möglichst weit links innen stehen.

Im folgenden Beispiel stehen fettgedruckte Zahlen ${\bf
0}$, ${\bf 1}$ für Adressen. Die Redexe sind jeweils
unterstrichen:
%
{\small
\begin{displaymath}
  \begin{array}{l}
    ((\lambda x.((\lambda y.x) (\mathtt{set!}~x~(+~x~1))))~12), \varnothing
    \\
    \rightarrow({\bf 0}~\underline{12}), \{ ({\bf 0}, \lambda x.((\lambda
    y.x) (\mathtt{set!}~x~(+~x~1)))) \}
    \\
    \rightarrow\underline{({\bf 0}~{\bf 1})}, \{ ({\bf 0}, \lambda x.((\lambda
    y.x) (\mathtt{set!}~x~(+~x~1)))), ({\bf 1}, 12) \}
    \\
    \rightarrow 
    (\underline{(\lambda y.{\bf 2})} (\mathtt{set!}~{\bf
    2}~(+~{\bf 2}~1))),
    \{ ({\bf 0}, \lambda x.((\lambda
    y.x) (\mathtt{set!}~x~(+~x~1)))), ({\bf 1}, 12), ({\bf
    2}, 12)\}\\
    \rightarrow 
    ({\bf 3}~(\mathtt{set!}~{\bf
    2}~(+~{\bf 2}~\underline{1}))),
    \\
    \quad
    \{ ({\bf 0}, \lambda x.((\lambda
    y.x) (\mathtt{set!}~x~(+~x~1)))), ({\bf 1}, 12), ({\bf
    2}, 12), ({\bf 3}, (\lambda y.{\bf 2}) \}
    \\
    \rightarrow 
    ({\bf 3}~(\mathtt{set!}~{\bf
    2}~\underline{(+~{\bf 2}~{\bf 4})})),
    \\
    \quad
    \{ ({\bf 0}, \lambda x.((\lambda
    y.x) (\mathtt{set!}~x~(+~x~1)))), ({\bf 1}, 12), ({\bf
    2}, 12), ({\bf 3}, (\lambda y.{\bf 2}),
    ({\bf 4}, 1) \}\\
    \rightarrow 
    ({\bf 3} \underline{(\mathtt{set!}~{\bf
      2}~{\bf 5})}),
    \\
    \quad
    \{ ({\bf 0}, \lambda x.((\lambda
    y.x) (\mathtt{set!}~x~(+~x~1)))), ({\bf 1}, 12), ({\bf
    2}, 12), ({\bf 3}, (\lambda y.{\bf 2}),
    ({\bf 4}, 1), ({\bf 5}, 13) \}
    \\
    \rightarrow 
    ({\bf 3}~\mathtt{void}),
    \\
    \quad
    \{ ({\bf 0}, \lambda x.((\lambda
    y.x) (\mathtt{set!}~x~(+~x~1)))), ({\bf 1}, 12), ({\bf
    2}, 13), ({\bf 3}, (\lambda y.{\bf 2}),
    ({\bf 4}, 1), ({\bf 5}, 13) \}
    \\
    \rightarrow 
    \underline{({\bf 3}~{\bf 6})},
    \\
    \quad
    \{ ({\bf 0}, \lambda x.((\lambda
    y.x) (\mathtt{set!}~x~(+~x~1)))), ({\bf 1}, 12), ({\bf
    2}, 13), ({\bf 3}, (\lambda y.{\bf 2}),
    ({\bf 4}, 1), ({\bf 5}, 13), ({\bf 6}, \mathtt{void}) \}
    \\
    \rightarrow 
    {\bf 2},
    \\
    \quad    \{ ({\bf 0}, \lambda x.((\lambda
    y.x) (\mathtt{set!}~x~(+~x~1)))), ({\bf 1}, 12), ({\bf
    2}, 13), ({\bf 3}, (\lambda y.{\bf 2}),
    ({\bf 4}, 1), ({\bf 5}, 13), ({\bf 6}, \mathtt{void}) \}
  \end{array}
\end{displaymath}
}
%
Der Endausdruck steht für die Speicherzelle an Adresse ${\bf
2}$, wo der Wert $13$ steht.  Es ist sichtbar, dass die
Auswertungsmaschinerie durch die Einführung von Zustand deutlich
komplizierter wird.

\section{Die SECDH-Maschine}
\index{sec:SECDH-Maschine}

Die SECD-Maschine ist nicht mächtig genug, um den $\lambda$-Kalkül mit
Zustand zu modellieren: Es fehlt ein Speicher.  Darum muss das
Maschinen-Pendant zum $\lambda$-Kalkül mit Zustand um eine
Speicher-Komponente erweitert werden: Heraus kommt die
\textit{SECDH-Maschine}, um die es in diesem Abschnitt geht.

Der Maschinencode für die SECDH-Maschine ist dabei genau wie bei der
SECD-Maschine, nur dass eine spezielle Zuweisungsoperation hinzukommt:
%
\begin{grammar}
  \meta{I} \: \ldots
  \> \| :=
\end{grammar}
%
Die Übersetzungsfunktion produziert diese neue Instruktion bei
\lstinline{set!}-Ausdrücken:
%
\begin{eqnarray*}
  \llbracket e \rrbracket &\deq&
  \begin{cases}
    \ldots\\
    v~\llbracket e'\rrbracket~\mathtt{:=}
    & \textrm{falls $e = (\mathtt{set!}~v~e')$}
  \end{cases}
\end{eqnarray*}  
%
Der Begriff der Adresse aus der Menge $A$ wird direkt aus dem Kalkül
übernommen.  Ähnlich wie im Kalkül landen Zwischenergebnisse nicht
mehr direkt auf dem Stack, sondern stattdessen landen ihre Adressen im
Speicher.  Dementsprechend bilden nun Umgebungen Variablen auf
Adressen ab.  Die neue Komponente $H$ ist gerade der Speicher, auch
genannt \textit{Heap\index{Heap}}, der die Adressen auf Werte
abbildet:
%
\begin{eqnarray*}
  S &=& A^{\ast}\\
  E &=& \mathcal{P}(V\times A)\\
  D &=& (S\times E\times C)^{\ast}\\
  H &=& \mathcal{P}(A\times W)\\
  W &=& B \cup (V\times C\times E)
\end{eqnarray*}
%
Die Regeln für die SECDH-Maschine sind analog zu den Regeln für die
SECD-Maschine.  Zwei Hauptunterschiede gibt es dabei:
%
\begin{itemize}
\item Der Heap aus $H$ gehört nun zum Zustand dazu.  Anders als die
  Umgebung wird er nicht bei der Bildung von Closures "<eingepackt">:
  Stattdessen wird der Heap stets linear von links nach rechts durch
  Regeln durchgefädelt.
\item Zwischenergebnisse nehmen stets den Umweg über den Heap: Immer,
  wenn ein neues Zwischenergebnis entsteht, wird es bei einer neuen
  Adresse im Heap abgelegt. Auf dem Stack landen die
  Adressen der Zwischenergebnisse.
\end{itemize}

\begin{eqnarray*}
  \hookrightarrow &\in& \mathcal{P}((S\times E\times C\times D\times H) \times (S\times E\times C\times D\times H))\\
  (\underline{s}, e, b\underline{c}, \underline{d}, h)
  &\hookrightarrow& 
  (a\underline{s}, e, \underline{c}, \underline{d}, h[a \mapsto b] )
  \\ && \textrm{wobei $a$ frisch}
  \\
  (\underline{s}, e, v\underline{c}, \underline{d}, h)
  &\hookrightarrow&
  (e(v)\underline{s}, e, \underline{c}, \underline{d}, h)
  \\
  (a_k\ldots a_1\underline{s}, e, \mathtt{prim}_{F^k}\underline{c},
  \underline{d}, h)
  &\hookrightarrow&
  (a\underline{s}, e, \underline{c}, \underline{d}, h[a\mapsto b] )
  \\ && \textrm{wobei $a$ frisch, $b_i = h(a_i)$ und $F^k\in\Sigma^k$ und $F^k_B(b_1,\ldots,b_k) = b$}
  \\
  (a_1a_0\underline{s}, e, \mathtt{:=} \underline{c}, \underline{d}, h)
  &\hookrightarrow&
  (a\underline{s}, e, \underline{c}, \underline{d}, h[a_0 \mapsto
  h(a_1)][a\mapsto \mathtt{void}] )
  \\ && \textrm{wobei $a$ frisch}
  \\
  (\underline{s}, e, (v, \underline{c'})\underline{c}, \underline{d},
  h)
  &\hookrightarrow&
  (a\underline{s}, e, \underline{c}, \underline{d}, h[a \mapsto (v,
  \underline{c'}, e)] )
  \\ && \textrm{wobei $a$ frisch}
  \\
  (a_1a_0\underline{s}, e, \mathtt{ap}\underline{c}, \underline{d}, h)
  &\hookrightarrow&
  (\epsilon, e'[v\mapsto a], \underline{c'}, (\underline{s}, e,
  \underline{c}) \underline{d}, h[a\mapsto h(a_1)])
  \\ && \textrm{wobei $a$ frisch und $h(a_0) = (v, \underline{c'}, e')$}
  \\
  (a, e, \epsilon, (\underline{s'}, e', \underline{c'}) \underline{d}, h)
  &\hookrightarrow&
  (a\underline{s'}, e', \underline{c'}, \underline{d}, h)
\end{eqnarray*}

Entsprechend muss die Auswertungsfunktion das Endergebnis im Heap nachschauen:

\begin{eqnarray*}
  \mathit{eval}_\mathit{SECD} & \in & \mathcal{L}_{\lambda{}S} \times Z\\
  \mathit{eval}_\mathit{SECD}(e) & = &
  \begin{cases}
    h(a) & \textrm{falls } (\epsilon, \varnothing, \llbracket
    e\rrbracket, \epsilon, \varnothing)
    \hookrightarrow^* (a, e, \epsilon, \epsilon, h), h(a) \in B\\
    \texttt{function} & \textrm{falls } (\epsilon, \varnothing, \llbracket e\rrbracket, \epsilon,\varnothing)
    \hookrightarrow^* (a, e, \epsilon, \epsilon, h), h(a) = (v, \underline{c}, e')\\
  \end{cases}
\end{eqnarray*}


\section{Programmierung der SECDH-Maschine}


Um die SECDH-Maschine zu programmieren, verwenden wir einige der
Funktionen wieder, die für die SECD-Maschine programmiert
wurden.  Zunächst einmal muss~-- genau wie bei der SECD-Maschine~--
erst einmal die Übersetzung von Termen in Maschinencode realisiert
werden.  Zuweisungsterme haben wie in den Lehrsprachen die folgende Form:
%
\begin{alltt}
(set! \(v\) \(e\))
\end{alltt}
%
Das dazu passende Prädikat ist das folgende:
%
\begin{lstlisting}
; Prädikat für Zuweisungen
(: assignment? (%a -> boolean))
(define assignment?
  (lambda (term)
    (and (cons? term)
         (equal? 'set! (first term)))))

(define assignment (signature (predicate assignment?)))
\end{lstlisting}
%
Mit Hilfe dieser Definition kann die Signatur-Definition von
\lstinline{term} erweitert werden:
%
\begin{lstlisting}
(define term
  (signature
    (mixed symbol
           application
           abstraction
           base
           primitive-application
           assignment)))
\end{lstlisting}
%
Um zu vermeiden, dass Zuweisungen mit regulären Applikationen
verwechselt werden, muss das Prädikat \lstinline{application?} erweitert
werden:
%
\begin{lstlisting}
(: application? (any -> boolean))
(define application?
  (lambda (term)
    (and (cons? term)
         (not (equal? 'set! (first term)))
         (not (equal? 'lambda (first term)))
         (not (primitive? (first term))))))
\end{lstlisting}
%
Als Nächstes wird die zusätzliche $\mathtt{:=}$-Instruktion
repräsentiert.  Hier sind Daten- und Record-Definition:
%
\begin{lstlisting}
; Eine Zuweisungs-Instruktion ist ein Wert
;  (make-:=)
(define-record :=
  make-:= :=?)
\end{lstlisting}
%
Die Signatur-Definition für Maschinen-Instruktionen kann um \lstinline{:=}
erweitert werden:
%
\begin{lstlisting}
(define instruction
  (signature
    (mixed base
           symbol
           ap
           tailap
           prim
           abs
           :=)))
\end{lstlisting}

Bei der Übersetzung in Maschinencode kommt in
\lstinline{term->machine-code} ein weiterer Zweig hinzu:
%
\begin{lstlisting}
; Term in Maschinencode übersetzen
(: term->machine-code (term -> machine-code))
(define term->machine-code
  (lambda (term)
    (cond
      ...
      ((assignment? term)
       (cons (first (rest term))
             (append (term->machine-code (first (rest (rest term))))
                     (list (make-:=))))))))
\end{lstlisting}
%
Wie bei der SECD-Maschine werden die verschiedenen Mengendefinitionen
erst einmal in Daten- und Record-Definitionen übersetzt.  Das ist für
Stacks, Umgebungen und Speicheradressen ganz einfach:
%
\begin{lstlisting}
; Ein Stack ist eine Liste aus Adressen.
(define stackh (signature (list-of address)))

; Eine Umgebung bildet Variablen auf Adressen ab.

; Eine Adresse ist eine ganze Zahl.
(define address (signature natural))
\end{lstlisting}
%
Die Änderung in der Definition von Umgebungen bedingt eine Änderung
der Signatur von \lstinline{make-binding}:
%
\begin{lstlisting}
(: make-binding (symbol address -> binding))
\end{lstlisting}

%
Bei der Repräsentation des Heaps ist wichtig, dass eine Operation zur
Beschaffung frischer Adressen eingebaut wird.  Aus diesem Grund
enthält der Heap zusätzlich zu den Zellen auch noch einen Zähler mit
der nächsten frischen Adresse:
%
\begin{lstlisting}
; Ein Heap ist ein Wert
;   (make-heap s n)
; wobei n die nächste freie Adresse ist und s eine Liste
; von Zellen.
(define-record heap
  make-heap heap?
  (heap-cells (list-of cell))
  (heap-next natural))
\end{lstlisting}
%
Der leere Heap wird schon einmal vorfabriziert:
%
\begin{lstlisting}
(define the-empty-heap (make-heap empty 0))
\end{lstlisting}
%
Jede Zelle ordnet einer Adresse einen Wert zu:
%
\begin{lstlisting}
; Eine Zelle ist ein Wert
;   (make-cell a w)
; wobei a eine Adresse und w ein Wert ist
(define-record cell
  make-cell cell?
  (cell-address address)
  (cell-value value))
\end{lstlisting}
%
Die Funktion \lstinline{heap-store}, erweitert den Heap um eine Zelle
entsprechend der mathematischen Definition:
%
\begin{lstlisting}
; Wert im Speicher ablegen
(: heap-store (heap address value -> heap))
(define heap-store
  (lambda (heap address value)
    (make-heap (cons (make-cell address value)
                     (remove-cell address (heap-cells heap)))
               ...)))
\end{lstlisting}
%
Die Ellipse steht für die nächste frische Adresse: Wenn die bisherige
frische Adresse in \lstinline{heap-store} belegt wird, so muss eine neue
frische Adresse gewählt werden:
%
\begin{lstlisting}
(define heap-store
  (lambda (heap address value)
    (define next (heap-next heap))
    (make-heap (cons (make-cell address value)
                     (remove-cell address (heap-cells heap)))
               (if (= address next)
                   (+ next 1)
                   next))))
\end{lstlisting}
%
Es fehlt noch die Hilfsfunktion \lstinline{remove-cell}:
%
\begin{lstlisting}
; Zelle zu einer Adresse entfernen
(: remove-cell (address (list-of cell) -> (list-of cell)))
(define remove-cell
  (lambda (address cell)
    (cond
      ((empty? cell) empty)
      ((cons? cell)
       (if (= address (cell-address (first cell)))
           (rest cell)
           (cons (first cell)
                 (remove-cell address (rest cell))))))))
\end{lstlisting}
%
Als Nächstes ist die Operation an der Reihe, die den Wert, der an einer
Adresse im Heap gespeichert ist.  Die Funktion \lstinline{heap-lookup} benutzt
eine Hilfsfunktion \lstinline{cells-lookup}, um in der Liste von Zellen
nach der richtigen zu suchen:
%
\begin{lstlisting}
; den Wert an einer Adresse im Heap nachschauen
(: heap-lookup (heap address -> value))
(define heap-lookup
  (lambda (heap address)
    (cells-lookup (heap-cells heap) address)))

; den Wert an einer Adresse in einer Liste von Zellen nachschauen
(: cells-lookup ((list-of cell) address -> value))
(define cells-lookup
  (lambda (cells address)
    (cond
      ((empty? cells) (violation "unassigned address"))
      ((cons? cells)
       (if (= address (cell-address (first cells)))
           (cell-value (first cells))
           (cells-lookup (rest cells) address))))))
\end{lstlisting}
%
Schließlich fehlt noch eine Repräsentation für den $\mathtt{void}$-Wert:
%
\begin{lstlisting}
; Ein void-Wert ist ein Wert
;  (make-void)
(define-record void
  make-void void?)
\end{lstlisting}
%
Auch hier wird nur ein $\mathtt{void}$-Wert benötigt, der 
vorfabriziert wird:
%
\begin{lstlisting}
(define the-void (make-void))
\end{lstlisting}
%
Der Zustand für die SECDH-Maschine wird genau wie bei der
SECD-Maschine repräsentiert, ergänzt um die Komponente für den Heap:
%
\begin{lstlisting}
; Ein SECDH-Zustand ist ein Wert
;   (make-secd s e c d h)
; wobei s ein Stack, e eine Umgebung, c Maschinencode,
; d ein Dump und h ein Speicher ist.
(define-record secdh
  make-secdh secdh?
  (secdh-stack stackh)
  (secdh-environment environment)
  (secdh-code machine-code)
  (secdh-dump dump)
  (secdh-heap heap))
\end{lstlisting}
%
Die Zustandsübergangsfunktion hat exakt die
gleiche Struktur wie die entsprechende Funktion der SECD-Maschine und hält
sich eng an die mathematische Definition der Regeln:
%
\begin{lstlisting}
; eine Zustandstransition berechnen
(: secdh-step (secdh -> secdh))
(define secdh-step
  (lambda (state)
    (define stack (secdh-stack state))
    (define environment (secdh-environment state))
    (define code (secdh-code state))
    (define dump (secdh-dump state))
    (define heap (secdh-heap state))
    (cond
      ((cons? code)
       (cond
         ((base? (first code))
          (define address (heap-next heap))
          (make-secdh
           (cons address stack)
           environment
           (rest code)
           dump
           (heap-store heap address (first code))))
         ((symbol? (first code))
          (make-secdh
           (cons (lookup-environment environment (first code)) stack)
           environment
           (rest code)
           dump
           heap))
         ((prim? (first code))
          (define address (heap-next heap))
          (make-secdh
           (cons address
                 (drop (prim-arity (first code)) stack))
           environment
           (rest code)
           dump
           (heap-store heap address
                       (apply-primitive
                        (prim-operator (first code))
                        (map (lambda (address)
                               (heap-lookup heap address))
                             (take-reverse (prim-arity (first code)) stack))))))
         ((:=? (first code))
          (define address (heap-next heap))
          (make-secdh
           (cons address (rest (rest stack)))
           environment
           (rest code)
           dump
           (heap-store
            (heap-store heap
                        (first (rest stack)) 
                        (heap-lookup heap (first stack)))
            address the-void)))
         ((abs? (first code))
          (define address (heap-next heap))
          (make-secdh
           (cons address stack)
           environment
           (rest code)
           dump
           (heap-store heap address
                       (make-closure (abs-variable (first code))
                                     (abs-code (first code))
                                     environment))))
         ((ap? (first code))
          (define closure (heap-lookup heap (first (rest stack))))
          (define address (heap-next heap))
          (make-secdh empty
                      (extend-environment
                       (closure-environment closure)
                       (closure-variable closure)
                       address)
                      (closure-code closure)
                      (cons
                       (make-frame (rest (rest stack)) environment (rest code))
                       dump)
                      (heap-store heap address (heap-lookup heap (first stack)))))
         ((tailap? (first code))
          (define closure (heap-lookup heap (first (rest stack))))
          (define address (heap-next heap))
          (make-secdh (rest (rest stack))
                      (extend-environment
                       (closure-environment closure)
                       (closure-variable closure)
                       address)
                      (closure-code closure)
                      dump
                      (heap-store heap address (heap-lookup heap (first stack)))))))
      ((empty? code)
       (define frame (first dump))
       (make-secdh
        (cons (first stack)
              (frame-stack frame))
        (frame-environment frame)
        (frame-code frame)
        (rest dump)
        heap)))))
\end{lstlisting}
Es bleibt die Auswertungsfunktion, die ebenfalls genau wie bei der
SECD-Maschine realisiert wird:
%
\begin{lstlisting}
; aus Term SECDH-Anfangszustand machen
(: inject-secdh (term -> secdh))
(define inject-secdh
  (lambda (term)
    (make-secdh empty
                the-empty-environment
                (term->machine-code term)
                empty
               the-empty-heap)))

; bis zum Ende Zustandsübergänge berechnen
(: secdh-step* (secdh -> secdh))
(define secdh-step*
  (lambda (state)
    (if (and (empty? (secdh-code state))
             (empty? (secdh-dump state)))
        state
        (secdh-step* (secdh-step state)))))

; Evaluationsfunktion zur SECD-Maschine berechnen
(: eval-secdh (term -> (mixed value (one-of 'function))))

(check-expect (eval-secdh '(+ 1 2)) 3)
(check-expect (eval-secdh '(((lambda (x) (lambda (y) (+ x y))) 1) 2)) 3)
(check-expect (eval-secdh '((lambda (x) ((lambda (y) x) (set! x (+ x 1)))) 12)) 13)

(define eval-secdh
  (lambda (term)
    (define final (secdh-step* (inject-secdh term)))
    (define value (heap-lookup (secdh-heap final)
                               (first (secdh-stack final))))
    (if (base? value)
        value
        'function)))
\end{lstlisting}


\begin{aufgabe}
  Abstrahiere über \lstinline{remove-environment-binding} und
  \lstinline{remove-cell}.
\end{aufgabe}


\begin{aufgabe}
  \lstinline{Begin} lässt sich im angewandten $\lambda$-Kalkül als
  syntaktischer Zucker auffassen: Wie müssten \lstinline{begin}-Ausdrücke
  in die Sprache des Kalküls übersetzt werden?
\end{aufgabe}

\begin{aufgabe}
  Ãndere die SECDH-Maschine dahingehend, dass
  sie Endrekursion korrekt behandelt.
\end{aufgabe}