Finish for submission

1 files changed, 16 insertions, 17 deletions

diff --git a/edit-lens/src/Control/FST.lhs b/edit-lens/src/Control/FST.lhs
index 9cc7524..165f247 100644
--- a/edit-lens/src/Control/FST.lhs
+++ b/edit-lens/src/Control/FST.lhs
@@ -47,12 +47,12 @@ import Text.Dot
 \end{comment}
 
 \begin{defn}[Finite State Transducers]
-Unter einem \emph{finite state transducer} verstehen wir ein 6-Tupel $(\Sigma, \Delta, Q, I, F, E)$ mit $\Sigma$ dem endlichen Eingabe-Alphabet, $\Delta$ dem endlichen Ausgabe-Alphabet, $Q$ einer endlichen Menge an Zuständen, $I \subset Q$ der Menge von initialen Zuständen, $F \subset Q$ der Menge von akzeptierenden Endzuständen, und $E \subset Q \times (\Sigma \cup \{ \epsilon \}) \times (\Delta \cup \{ \epsilon \}) \times Q$ der Transitionsrelation.
+Unter einem \emph{finite state transducer} verstehen wir ein 6-Tupel $(\Sigma, \Delta, Q, I, F, E)$ mit $\Sigma$ dem endlichen Eingabe-Alphabet, $\Delta$ dem endlichen Ausgabe-Alphabet, $Q$ einer endlichen Menge an Zuständen, $I \subset Q$ der Menge von initialen Zuständen, $F \subset Q$ der Menge von akzeptierenden Endzuständen und $E \subset Q \times (\Sigma \cup \{ \epsilon \}) \times (\Delta \cup \{ \epsilon \}) \times Q$ der Transitionsrelation.
 
-Semantisch ist ein finite state transducer ein endlicher Automat erweitert um die Fähigkeit bei Zustandsübergängen ein Symbol aus seinem Ausgabe-Alphabet an ein Ausgabe-Wort anzuhängen.
+Semantisch ist ein finite state transducer ein endlicher Automat, erweitert um die Fähigkeit bei Zustandsübergängen ein Symbol aus seinem Ausgabe-Alphabet an ein Ausgabe-Wort anzuhängen (Siehe Definition \ref{defn:fst-eval}).
 
 In Haskell lockern wir die Anforderung, dass die Ein- und Ausgabe-Alphabete endlich sein müssen und annotieren sie nur im Typsystem.
-Zudem speichern wir die Transitionsrelation als multimap um effiziente lookups von Zustand-Eingabe-Paaren zu ermöglichen.
+Zudem speichern wir die Transitionsrelation als multimap, um effiziente lookups von Zustand-Eingabe-Paaren zu ermöglichen.
 
 \begin{code}
 data FST state input output = FST
@@ -64,7 +64,7 @@ data FST state input output = FST
 \end{defn}
 
 \begin{eg} \label{eg:linebreak}
-  Als wiederkehrendes Beispiel betrachten wir einen Transducer $L_{80} = (\Sigma, \Delta, Q, I, F, E)$, der für ein beliebiges Alphabet $\Sigma \supseteq \{ \text{\tt ' '}, \text{\tt \textbackslash n} \}$ durch Umwandlung zwischen Leerzeichen und Zeilenumbrüchen sicherstellt, dass jede Zeile des Ausgabetextes möglichst wenige aber mindestens 80 Zeichen enthält, und nur an Wortgrenzen umbricht:
+  Als wiederkehrendes Beispiel betrachten wir einen Transducer $L_{80} = (\Sigma, \Delta, Q, I, F, E)$, der für ein beliebiges Alphabet $\Sigma \supseteq \{ \text{\tt ' '}, \text{\tt \textbackslash n} \}$ durch Umwandlung zwischen Leerzeichen und Zeilenumbrüchen sicherstellt, dass jede Zeile des Ausgabetextes möglichst wenige, aber mindestens 80 Zeichen enthält und nur an Wortgrenzen umbricht:
 
   \begin{align*}
     \Delta & = \Sigma \\
@@ -103,7 +103,7 @@ data FST state input output = FST
       \draw[-] (rest)--(i.north);
       \draw[-] (rest)--(si.west);
     \end{tikzpicture}
-    \caption{\label{fig:linebreak} Ein Transducer der, durch Übersetzung zwischen Leerzeichen und Zeilenumbrüchen, sicher stellt, dass jede Zeile eines Texts mindestens 80 Zeichen hat}
+    \caption{\label{fig:linebreak} Ein Transducer der durch Übersetzung zwischen Leerzeichen und Zeilenumbrüchen sicher stellt, dass jede Zeile eines Texts mindestens 80 Zeichen hat}
   \end{figure}
 \end{eg}
 
@@ -131,8 +131,8 @@ instance (Show state, Show input, Show output, Ord state, Ord input, Ord output)
 \end{code}
 \end{comment}
 
-\begin{defn}[Auswertung von FSTs]
-Wir definieren die \emph{Auswertung} von finite state transducers induktiv indem wir zunächst angeben wie ein einzelner Auswertungs-Schritt erfolgt.
+\begin{defn}[Auswertung von FSTs] \label{defn:fst-eval}
+Wir definieren die \emph{Auswertung} von finite state transducers induktiv, indem wir zunächst angeben, wie ein einzelner Auswertungs-Schritt erfolgt.
 
 Hierzu kommentieren wir die Haskell-Implementierung eines Auswertungs-Schritts.
 Notwendigerweise ist die Auswertung eines FSTs nicht deterministisch, wir produzieren daher eine Liste von möglichen Resultaten in keiner besonderen Reihenfolge.
@@ -145,7 +145,7 @@ step :: forall input output state. (Ord input, Ord output, Ord state)
      -> [(Maybe input, state, Maybe output)] -- ^ Tuples of unconsumed input, next state, and produced output
 step FST{..} Nothing inS = (\s -> (inS, s, Nothing)) <$> Set.toList stInitial
 \end{code}
-Ist kein vorheriger Schritt erfolgt so wählen wir einen initialen Zustand, konsumieren keine Eingabe, und produzieren keine Ausgabe.
+Ist kein vorheriger Schritt erfolgt, so wählen wir einen initialen Zustand, konsumieren keine Eingabe und produzieren keine Ausgabe.
 
 \begin{code}
 step FST{..} (Just c) inS = let
@@ -154,7 +154,7 @@ step FST{..} (Just c) inS = let
   in Set.toList $ Set.map (\(n, mOut) -> (Nothing, n, mOut)) consuming `Set.union` Set.map (\(n, mOut) -> (inS, n, mOut)) unconsuming
 \end{code}
 Ansonsten wählen wir einen Eintrag aus der Transitionstabelle für den aktuellen Zustand, der entweder keine oder die gegebene Eingabe konsumiert.
-Im Ergebnis geben wir den nächsten Zustand, die Ausgabe aus der Transitionstabelle, und ob die Eingabe konsumiert wurde an.
+Im Ergebnis geben wir den nächsten Zustand, die Ausgabe aus der Transitionstabelle und ob die Eingabe konsumiert wurde, an.
 
 \begin{code}
 runFST' :: forall input output state. (Ord input, Ord output, Ord state)
@@ -199,9 +199,8 @@ akzeptierenden Endzustände liegt.
 \end{comment}
 \end{defn}
 
-Es ist gelegentlich nützlich nur die möglichen Ausgaben eines FST auf gegebener
-Eingabe zu bestimmen, wir führen eine Hilfsfunktion auf Basis von
-{\ttfamily runFST'} ein:
+Es ist gelegentlich nützlich nur die möglichen Ausgaben eines FST auf gegebener Eingabe zu bestimmen.
+Wir führen eine Hilfsfunktion auf Basis von {\ttfamily runFST'} ein:
 
 \begin{code}
 runFST :: forall input output state. (Ord input, Ord output, Ord state) => FST state input output -> Seq input -> [Seq output]
@@ -216,14 +215,14 @@ runFST = fmap (map $ catMaybes . fmap (view _2) . view _2) . runFST'
 \end{comment}
 
 Wir können das Produkt zweier FSTs definieren.
-Intuitiv wollen wir beide FSTs gleichzeitig ausführen und dabei sicherstellen, dass Ein- und Ausgabe der FSTs übereinstimmen\footnote{Da wir $\epsilon$-Transitionen in FSTs erlauben müssen wir uns festlegen wann eine $\epsilon$-Transition übereinstimmt mit einer anderen Transition. Wir definieren, dass $\epsilon$ als Eingabe ausschließlich mit $\epsilon$ übereinstimmt.}.
+Intuitiv wollen wir beide FSTs gleichzeitig ausführen und dabei sicherstellen, dass Ein- und Ausgabe der FSTs übereinstimmen\footnote{Da wir $\epsilon$-Transitionen in FSTs erlauben, müssen wir uns festlegen, wann eine $\epsilon$-Transition übereinstimmt mit einer anderen Transition. Wir definieren, dass $\epsilon$ als Eingabe ausschließlich mit $\epsilon$ übereinstimmt.}.
 
 Hierfür berechnen wir das Graphen-Produkt der FSTs:
 
 \begin{defn}[FST-Produkt]
   Gegeben zwei finite state transducer $T = (\Sigma, \Delta, Q, I, F, E)$ und $T^\prime = (\Sigma^\prime, \Delta^\prime, Q^\prime, I^\prime, F^\prime, E^\prime)$ nennen wir $T^\times = (\Sigma^\times, \Delta^\times, Q^\times, I^\times, F^\times, E^\times)$ das Produkt $T^\times = T \times T^\prime$ von $T$ und $T^\prime$.
 
-  $T^\times$ bestimmt sich als das Graphenprodukt der beiden, die FSTs unterliegenden, Graphen wobei wir die Zustandsübergänge als Kanten mit Gewichten aus dem Boolschen Semiring auffassen:
+  $T^\times$ wird bestimmt als das Graphenprodukt der beiden die FSTs unterliegenden Graphen wobei wir die Zustandsübergänge als Kanten mit Gewichten aus dem Boolschen Semiring auffassen:
 
   \begin{align*}
     \Sigma^\times & = \Sigma \cap \Sigma^\prime \\
@@ -271,7 +270,7 @@ productFST fst1 fst2 = FST
 Es ist später erforderlich einen FST derart einzuschränken, dass er eine gegebene Ausgabe produziert.
 
 Hierzu nehmen wir das FST-Produkt mit einem FST, der, ungeachtet der Eingabe, immer die gewünschte Ausgabe produziert.
-Da die Ausgaben der beiden FSTs übereinstimmen müssen produziert das Produkt mit einem derartigen FST (solange dessen Ausgabe in keinem Sinne von der Eingabe abhängt) die gewünschte Ausgabe.
+Da die Ausgaben der beiden FSTs übereinstimmen müssen, produziert das Produkt mit einem derartigen FST (solange dessen Ausgabe in keinem Sinne von der Eingabe abhängt) die gewünschte Ausgabe.
 
 Zur Konstruktion eines derartigen \emph{Wort-FST}s nehmen wir Indizes im Ausgabe-Wort (natürliche Zahlen) als Zustände.
 Übergänge sind immer entweder der Form $n \rightarrow \text{succ}(n)$, konsumieren keine Eingabe ($\epsilon$) und produzieren als Ausgabe das Zeichen am Index $n$ im Ausgabe-Wort, oder der Form $n \overset{(\sigma, \epsilon)}{\rightarrow} n$, für jedes Eingabesymbol $\sigma$ (um die Unabhängigkeit von der Eingabe sicherzustellen).
@@ -335,7 +334,7 @@ wordFST inps outs = FST
   \end{figure}
 \end{eg}
 
-Da \texttt{wordFST} zur Konstruktion eine komprehensive Menge aller Eingabesymbole benötigt verwenden wir im folgenden eine optimierte Variante des Produkts mit einem Wort-FST.
+Da \texttt{wordFST} zur Konstruktion eine komprehensive Menge aller Eingabesymbole benötigt, verwenden wir im Folgenden eine optimierte Variante des Produkts mit einem Wort-FST.
 
 \begin{code}
 restrictOutput :: forall state input output. (Ord state, Ord input, Ord output) => Seq output -> FST state input output -> FST (Natural, state) input output
@@ -381,7 +380,7 @@ restrictOutput :: forall state input output. (Ord state, Ord input, Ord output)
 \begin{rem}
   Es ist bemerkenswert, dass in Beispiel \ref{eg:l80timesw100} die zirkuläre Struktur von $L_{80}$ durch das Produkt mit einem Wort verloren geht.
 
-  I.\@A.\@ ist das Produkt eines beliebigen FST mit einem Wort-FST zwar nicht azyklisch, erbt jedoch die lineare Struktur des Wort-FST in dem Sinne, dass Fortschritt in Richtung der akzeptierenden Zustände nur möglich ist indem der $(i, \sigma, w_i, i + 1)$-Klasse von Transitionen des Wort-FSTs gefolgt wird.
+  I.\@A.\@ ist das Produkt eines beliebigen FST mit einem Wort-FST zwar nicht azyklisch, erbt jedoch die lineare Struktur des Wort-FST in dem Sinne, dass Fortschritt in Richtung der akzeptierenden Zustände nur möglich ist, indem der $(i, \sigma, w_i, i + 1)$-Klasse von Transitionen des Wort-FSTs gefolgt wird.
 \end{rem}
   
 \begin{comment}