Finish for submission

8 files changed, 46 insertions, 46 deletions

diff --git a/edit-lens/src/Control/DFST.lhs b/edit-lens/src/Control/DFST.lhs
index eb838ae..48feaf9 100644
--- a/edit-lens/src/Control/DFST.lhs
+++ b/edit-lens/src/Control/DFST.lhs
@@ -41,7 +41,7 @@ import Text.Dot
 \begin{defn}[deterministic finite state transducer]
   Wir nennen einen FST \emph{deterministic}, wenn jedes Paar aus Ausgabezustand und Eingabesymbol maximal eine Transition zulässt, $\epsilon$-Transitionen keine Schleifen bilden und die Menge von initialen Zuständen einelementig ist.
 
-  Zusätzlich ändern wir die Darstellung indem wir $\epsilon$-Transitionen kontrahieren.
+  Zusätzlich ändern wir die Darstellung, indem wir $\epsilon$-Transitionen kontrahieren.
   Wir erweitern hierfür die Ausgabe pro Transition von einem einzelnen Zeichen zu einem Wort beliebiger Länge und fügen, bei jeder Kontraktion einer $\epsilon$-Transition $A \rightarrow B$, die Ausgabe der Transition vorne an die Ausgabe aller Transitionen $B \rightarrow \ast$ von $B$ an.
 \end{defn}
 
@@ -92,7 +92,7 @@ toFST DFST{..} = flip execState initialFST $ forM_ (Map.toList stTransition) han
 \end{comment}
 
 Das Ausführen eines DFST auf eine gegebene Eingabe ist komplett analog zum Ausführen eines FST.
-Unsere Implementierung nutzt die restriktivere Struktur aus unserer Definition von DFSTs um den Determinismus bereits im Typsystem zu kodieren.
+Unsere Implementierung nutzt die restriktivere Struktur aus unserer Definition von DFSTs, um den Determinismus bereits im Typsystem zu kodieren.
 
 \begin{code}
 runDFST :: forall state input output. (Ord state, Ord input) => DFST state input output -> Seq input -> Maybe (Seq output)
diff --git a/edit-lens/src/Control/DFST/Lens.lhs b/edit-lens/src/Control/DFST/Lens.lhs
index 56f37a0..04dade5 100644
--- a/edit-lens/src/Control/DFST/Lens.lhs
+++ b/edit-lens/src/Control/DFST/Lens.lhs
@@ -68,7 +68,7 @@ import Data.Universe (Finite(..))
 \begin{defn}[Ausgabe-Wirkung von DFSTs]
 Wir definieren zunächst die \emph{Ausgabe-Wirkung}\footnote{Wir schreiben im Folgenden auch nur \emph{Wirkung}} eines DFST auf einen festen String als eine Abbildung \texttt{state -> (Seq output, Maybe state)}, die den aktuellen Zustand vor dem Parsen des Strings auf den Zustand danach und die (womöglich leere) Ausgabe schickt.
 Wir annotieren Wirkungen zudem mit dem konsumierten String.
-Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings concateniert werden.
+Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings konkateniert werden.
 
 \begin{code}
 data DFSTAction state input output = DFSTAction
@@ -132,13 +132,13 @@ Wir bedienen uns hierbei einer bestehenden Programmbibliothek \cite{composition-
   \begin{figure}[H]
     \centering
     \pinclude{presentation/switchdfst.tex}
-    \caption{\label{fig:switchdfst} Ein einfacher DFST, der zwischen zwei Zustanden wechselt und Ausgabe abhängig vom aktuellen Zustand erzeugt}
+    \caption{\label{fig:switchdfst} Ein einfacher DFST, der zwischen zwei Zuständen wechselt und Ausgabe abhängig vom aktuellen Zustand erzeugt}
   \end{figure}
 
   Auf $s$ wechselt der DFST seinen Zustand, auf $p$ produziert er, abhängig vom aktuellen Zustand, genau ein Zeichen.
 
   Wir stellen die Wirkung des DFST auf den Eingabe-String $spp$ grafisch analog zur Baumstruktur von \texttt{Compositions} dar.
-  Wir bedienen uns hier der Darstellung von Automaten-Wirkungen als \emph{Schaltboxen} aus \cite{hofmann2011automatentheorie}, angepasst für DFSTs indem wir die Ausgabe des transducers an den Pfaden innerhalb der Schaltbox annotieren.
+  Wir bedienen uns hier der Darstellung von Automaten-Wirkungen als \emph{Schaltboxen} aus \cite{hofmann2011automatentheorie}, angepasst für DFSTs, indem wir die Ausgabe des transducers an den Pfaden innerhalb der Schaltbox annotieren.
   
   \begin{figure}[H]
     \centering
@@ -160,22 +160,23 @@ dfstaProduces = fmap fst . runDFSTAction'
 \end{code}
 \end{comment}
 
-Für $\Rrightarrow$ können wir die alte DFST-Wirkung zunächst anhand des Intervalls in dem der input-String von allen gegebenen edits betroffen ist (\texttt{affected}) in einen unveränderten Prefix und einen womöglich betroffenen Suffix unterteilen.
+Für $\Rrightarrow$ können wir die alte DFST-Wirkung zunächst, anhand des Intervalls, in dem der input-String von allen gegebenen edits betroffen ist (\texttt{affected}), in einen unveränderten Prefix und einen womöglich betroffenen Suffix unterteilen.
 
-Da wir wissen welche Stelle im input-String vom ersten gegebenen edit betroffen ist können wir, anhand der Wirkung des Teilstücks bis zu jener Stelle, den betroffenen Suffix wiederum teilen.
+Da wir wissen welche Stelle im input-String vom ersten gegebenen edit betroffen ist, können wir, anhand der Wirkung des Teilstücks bis zu jener Stelle, den betroffenen Suffix wiederum teilen.
 Die Wirkung ab der betroffenen Stelle im input-String können wir als Komposition der Wirkung der durch den edit betroffenen Stelle und derer aller Zeichen danach bestimmen.
-Nun gilt es nur noch die Differenz (als `StringEdits`) des vorherigen Suffixes im output-String und des aus der gerade berechneten Wirkung zu bestimmen, wir bedienen uns hierzu dem Unix Standard-Diff-Algorithmus zwischen der ursprünglichen Ausgabe und dem Ergebnis der Iteration des Verfahrens auf alle gegebenen edits.
+Nun gilt es nur noch die Differenz (als `StringEdits`) des vorherigen Suffixes im output-String und des aus der gerade berechneten Wirkung zu bestimmen.
+Wir bedienen uns hierzu dem Unix Standard-Diff-Algorithmus zwischen der ursprünglichen Ausgabe und dem Ergebnis der Iteration des Verfahrens auf alle gegebenen edits.
 
 Für die asymmetrische edit-lens entgegen der DFST-Richtung $\Lleftarrow$ verwenden wir Breitensuche über die Zustände des DFST innerhalb des von allen gegeben edits betroffenen Intervalls:
 
-Wir unterteilen zunächst das Komplement an den Grenzen des betroffenen Intervalls im output-String in drei Teile (durch Akkumulation der Elemente des Komplements bis die gewünschte Länge erreicht ist).
+Wir unterteilen zunächst das Komplement an den Grenzen des betroffenen Intervalls im output-String in drei Teile durch Akkumulation der Elemente des Komplements bis die gewünschte Länge erreicht ist.
 
 Wir transformieren dann den DFST in einen FST, dessen Ausgabe wir mit \texttt{restrictOutput} auf das gewünschte Fragment einschränken, setzen als initialen Zustand des FST den Zustand am linken Rand des von den edits betroffenen Intervalls und akzeptieren jene Zustände, von denen aus das Komplement-Fragment ab dem rechten Rand des betroffenen Intervalls zu einem im ursprünglichen DFST akzeptierenden Zustand führt.
 
-Wir verwenden dann gewöhnliche Breitensuche über die Zustände und Transitionen des soeben konstruierten FSTs um einen Lauffragment zu bestimmen, dass wir in das betroffene Intervall einsetzen können.
-Hierbei sind sämtliche Randbedingungen (korrekte Ausgabe, Übereinstimmung an den Intervallgrenzen) bereits in den FST kodiert sodass wir nur noch prüfen müssen, dass der gefunde Lauf in einem akzeptierenden Zustand endet.
+Wir verwenden dann gewöhnliche Breitensuche über die Zustände und Transitionen des soeben konstruierten FSTs, um einen Lauffragment zu bestimmen, das wir in das betroffene Intervall einsetzen können.
+Hierbei sind sämtliche Randbedingungen (korrekte Ausgabe, Übereinstimmung an den Intervallgrenzen) bereits in den FST kodiert, sodass wir nur noch prüfen müssen, dass der gefundene Lauf in einem akzeptierenden Zustand endet.
 
-Die input-edits können nun wiederum, unter Beachtung der Verschiebung der Indices um die Länge der Eingabe vor der linken Intervallgrenze, mit dem Unix Standard-Diff-Algorithmus berechnet werden.
+Die input-edits können nun wiederum, unter Beachtung der Verschiebung der Indizes um die Länge der Eingabe vor der linken Intervallgrenze, mit dem Unix Standard-Diff-Algorithmus berechnet werden.
 
 \begin{comment}
 \begin{code}
@@ -323,7 +324,7 @@ bfs outgoing predicate
   Wie auch im ursprünglichen DFST sind alle Zustände akzeptierend.
 
   Wir müssen nun bestimmen welche Zustände, unter $\text{act}_\text{R}$, zu einem akzeptierenden Zustand führen.
-  Da alle Zustände akzeptieren ist hier jeder Zustand geeignet.
+  Da alle Zustände akzeptieren, ist hier jeder Zustand geeignet.
 
   Wir müssen nun (vermöge Breitensuche) den kürzesten Pfad im Produkt-FST zwischen $Q_\text{L}$ und einem der Zustände finden, der unter $\text{act}_\text{R}$ zu einem akzeptierenden Zustand im ursprünglichen transducer führt.
   Der leere Pfad ist geeignet.
@@ -339,7 +340,7 @@ bfs outgoing predicate
     \text{\tt \textbackslash n} \cdot e = \epsilon
   \end{equation*}
   Man beachte das $\text{\tt \textbackslash n}$ und $\epsilon$ hierbei die \emph{Eingaben} von $\text{act}_{e^\prime}$ bzw. $\text{act}_0$ sind.
-  Nach Behandlung der Indices ergibt sich $e = \rho_{80}$.
+  Nach Behandlung der Indizes ergibt sich $e = \rho_{80}$.
 
   Als neues Komplement erhalten wir:
 
diff --git a/edit-lens/src/Control/Edit.lhs b/edit-lens/src/Control/Edit.lhs
index 80c143a..98fa8c4 100644
--- a/edit-lens/src/Control/Edit.lhs
+++ b/edit-lens/src/Control/Edit.lhs
@@ -6,10 +6,10 @@ module Control.Edit
 \end{code}
 \end{comment}
 
-Um das intuitive Verhalten von Änderungen auf Texten\footnote{Im folgenden \emph{edits}} und ihre interne algebraische Struktur zu fassen formalisieren wir sie als \emph{Moduln}:
+Um das intuitive Verhalten von Änderungen auf Texten\footnote{Im folgenden \emph{edits}} und ihre interne algebraische Struktur zu fassen, formalisieren wir sie als \emph{Moduln}:
 
 \begin{defn}[Moduln]
-Ein \emph{Modul} $M$ ist eine partielle Monoidwirkung zusammen mit einem schwach-initialen Element\footnote{Gemeint ist hier die übliche Definition von \emph{schwach-initial} aus der Kategorientheorie—ein Modul $M$ bildet eine Kategorie mit Objekten aus $\Dom M$ und Morphismen von $x$ nach $y$ den Monoidelementen $\partial x \in \partial M$ sodass $x \cdot \partial x = y$} (bzgl. der Monoidwirkung) auf dem Träger, d.h. $M = (\Dom M, \partial M, \init_M)$ ist ein Tupel aus einer Trägermenge $\Dom M$, einem Monoid $\partial M$ zusammen mit mit einer partiellen Funktion $\cdot \colon \Dom M \times \partial M \to \Dom$, die \emph{kompatibel} ist mit der Monoid-Struktur:
+Ein \emph{Modul} $M$ ist eine partielle Monoidwirkung zusammen mit einem schwach-initialen Element\footnote{Gemeint ist hier die übliche Definition von \emph{schwach-initial} aus der Kategorientheorie—ein Modul $M$ bildet eine Kategorie mit Objekten aus $\Dom M$ und Morphismen von $x$ nach $y$ den Monoidelementen $\partial x \in \partial M$ sodass $x \cdot \partial x = y$} (bzgl. der Monoidwirkung) auf dem Träger. D.h. $M = (\Dom M, \partial M, \init_M)$ ist ein Tupel aus einer Trägermenge $\Dom M$, einem Monoid $\partial M$ zusammen mit einer partiellen Funktion $\cdot \colon \Dom M \times \partial M \to \Dom M$, die \emph{kompatibel} ist mit der Monoid-Struktur:
 
 \begin{itemize}
   \item $\forall m \in \Dom M \colon m \cdot 1_{\partial M} = m$
@@ -22,7 +22,7 @@ $$\forall m \in \Dom M \ \exists \partial m \in \partial M \colon m = \init_M \c
 
 Wir führen außerdem eine Abbildung $(\init_M \cdot)^{-1} \colon \Dom M \to \partial m$ ein, die ein $m$ auf ein arbiträr gewähltes $\partial m$ abbildet für das $\init_M \cdot \partial m = m$ gilt.
 
-In Haskell charakterisieren wir Moduln über ihren Monoid, d.h. die Wahl des Monoiden \texttt{m} legt den Träger \texttt{Domain m}, die Wirkung \texttt{apply}, das initiale Element \texttt{init} und $(\init_M \cdot)^{-1}$ eindeutig fest\footnote{Betrachten wir mehrere Moduln über dem selben Träger (oder mit verschiedenen Wirkungen) führen wir neue, isomorphe Typen ein (\texttt{newtype}-Wrapper)}.
+In Haskell charakterisieren wir Moduln über ihren Monoid, d.h. die Wahl des Monoiden \texttt{m} legt den Träger \texttt{Domain m}, die Wirkung \texttt{apply}, das initiale Element \texttt{init} und $(\init_M \cdot)^{-1}$ eindeutig fest\footnote{Betrachten wir mehrere Moduln über dem selben Träger (oder mit verschiedenen Wirkungen), führen wir neue, isomorphe Typen ein (\texttt{newtype}-Wrapper)}.
 Eine Repräsentierung als Typklasse bietet sich an:
 
 \begin{code}
@@ -50,7 +50,7 @@ apply' md e = flip apply e =<< md
 \end{code}
 \end{defn}
 
-Wir weichen von der originalen Definition von Moduln aus \cite{hofmann2012edit} darin ab, dass wir für das ausgezeichnete Element $\init_X$ des Trägers explizit (und konstruktiv\footnote{$(\init_M \cdot)^{-1}$}) fordern, dass es ein schwach-initiales Element bzgl. der Monoidwirkung sei.
+Wir weichen von der originalen Definition von Moduln aus \cite{hofmann2012edit} ab, indem wir für das ausgezeichnete Element $\init_X$ des Trägers explizit (und konstruktiv\footnote{$(\init_M \cdot)^{-1}$}) fordern, dass es ein schwach-initiales Element bzgl. der Monoidwirkung sei.
 
 \begin{comment}
 \begin{defn}[Modulhomomorphismen]
diff --git a/edit-lens/src/Control/Edit/String.lhs b/edit-lens/src/Control/Edit/String.lhs
index c1411cf..f0ca588 100644
--- a/edit-lens/src/Control/Edit/String.lhs
+++ b/edit-lens/src/Control/Edit/String.lhs
@@ -24,7 +24,7 @@ import Data.Monoid
 \end{comment}
 
 \begin{defn}[Atomare edits of strings]
-Wir betrachten, zur Einfachheit, ein minimiales Set von Edits auf Strings\footnote{Wie in der Konstruktion zum Longest Common Subsequence Problem}, bestehend nur aus Einfügung eines einzelnen Zeichens $\sigma$ an einer bestimmten Position $\iota_n(\sigma)$ und löschen des Zeichens an einer einzelnen Position $\rho_n$:
+Wir betrachten zur Einfachheit ein minimiales Set von Edits auf Strings\footnote{Wie in der Konstruktion zum Longest Common Subsequence Problem} bestehend nur aus Einfügung eines einzelnen Zeichens $\sigma$ an einer bestimmten Position $\iota_n(\sigma)$ und löschen des Zeichens an einer einzelnen Position $\rho_n$:
 
 \begin{code}
 data StringEdit pos char = Insert { _sePos :: pos, _seInsertion :: char }
@@ -38,7 +38,7 @@ data StringEdit pos char = Insert { _sePos :: pos, _seInsertion :: char }
 makeLenses ''StringEdit
 \end{code}
 
-Atomare edits werden, als Liste, zu edits komponiert.
+Atomare edits werden als Liste zu edits komponiert.
 Wir führen einen speziellen edit ein, der nicht-Anwendbarkeit der edits repräsentiert:
 \begin{code}
 data StringEdits pos char = StringEdits (Seq (StringEdit pos char))
diff --git a/edit-lens/src/Control/Edit/String/Affected.lhs b/edit-lens/src/Control/Edit/String/Affected.lhs
index 851267b..15f73af 100644
--- a/edit-lens/src/Control/Edit/String/Affected.lhs
+++ b/edit-lens/src/Control/Edit/String/Affected.lhs
@@ -29,7 +29,7 @@ import Data.Maybe (fromMaybe, maybeToList, listToMaybe, catMaybes, isNothing, is
 \end{comment}
 
 Um eine obere Schranke an das von einer Serie von edits betroffene Intervall zu bestimmen ordnen wir zunächst jeder von mindestens einem atomaren edit betroffenen Position $n$ im Eingabe-Wort einen $\text{offset}_n = \text{\# deletions} - \text{\# inserts}$ zu.
-Das gesuchte Intervall ist nun $(\text{minK}, \text{maxK})$, mit $\text{minK}$ der Position im Eingabe-Wort mit niedrigstem $\text{offset}$ und $\text{maxK}$ die Position im Eingabe-Wort mit höchstem $\text{offset}$, $\text{maxK}^\prime$, modifiziert um das Maximum aus $\{ 0 \} \cup \{ \text{maxK}_n \colon n \in \{ 0 \ldots \text{maxK}^\prime \} \}$ wobei $\text{maxK}_n = -1 \cdot (n + \text{offset}_n)$ an Position $n$ ist.
+Das gesuchte Intervall ist nun $(\text{minK}, \text{maxK})$, mit $\text{minK}$ der Position im Eingabe-Wort mit niedrigstem $\text{offset}$ und $\text{maxK}$ die Position im Eingabe-Wort mit höchstem $\text{offset}$ $\text{maxK}^\prime$ modifiziert um das Maximum aus $\{ 0 \} \cup \{ \text{maxK}_n \colon n \in \{ 0 \ldots \text{maxK}^\prime \} \}$ wobei $\text{maxK}_n = -1 \cdot (n + \text{offset}_n)$ an Position $n$ ist.
 
 \begin{code}
 affected :: forall char. StringEdits Natural char -> Maybe (Interval Natural)
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}
diff --git a/edit-lens/src/Control/FST/Lens.tex b/edit-lens/src/Control/FST/Lens.tex
index 31af317..7e9e9e3 100644
--- a/edit-lens/src/Control/FST/Lens.tex
+++ b/edit-lens/src/Control/FST/Lens.tex
@@ -1,4 +1,4 @@
-Es stellt sich die Frage, ob das obig beschriebene Verfahren zur Konstruktion einer edit-lens sich auch auf nondeterminische finite state transducers anwenden lässt.
+Es stellt sich die Frage, ob das obig beschriebene Verfahren zur Konstruktion einer edit-lens sich auch auf nicht determinische finite state transducers anwenden lässt.
 
 Eine natürlich Erweiterung von \texttt{DFSTAction} wäre:
 \begin{lstlisting}[language=Haskell]
@@ -9,7 +9,7 @@ data FSTAction state input output = FSTAction
 \end{lstlisting}
 wobei die Liste aller möglichen output-Strings in der rechten Seite von \texttt{runFSTAction} in aller Regel unendlich ist.
 
-$\Rrightarrow$ würde sich notwendigerweise arbiträr auf einen der möglichen output-Strings festlegen aber ansonsten wohl identisch zum DFST-Fall implementieren lassen.
+$\Rrightarrow$ würde sich notwendigerweise arbiträr auf einen der möglichen output-Strings festlegen, aber ansonsten wohl identisch zum DFST-Fall implementieren lassen.
 
 $\Lleftarrow$ basiert fundamental darauf im Komplement anhand der erzeugten output-Strings zu suchen (um das betroffene Intervall im output-String auf das Komplement zu übertragen).
 Um sicher zu stellen, dass jene Suche immer terminiert, müsste die Aufzählung der i.A. unendlich vielen zulässigen output-Strings in \texttt{FSTAction} geschickt gewählt sein.
diff --git a/edit-lens/src/Control/Lens/Edit.lhs b/edit-lens/src/Control/Lens/Edit.lhs
index 5cf8662..84216bd 100644
--- a/edit-lens/src/Control/Lens/Edit.lhs
+++ b/edit-lens/src/Control/Lens/Edit.lhs
@@ -12,7 +12,7 @@ import Control.Edit
 \end{comment}
 
 \begin{defn}[Zustandsbehaftete Monoidhomomorphismen]
-Gegeben eine Menge $C$ von \emph{Komplementen} und zwei Monoiden $M$ und $N$ nennen wir eine partielle Funktion $\psi \colon C \times M \to C \times N$ einen \emph{zustandsbehafteten Monoidhomomorphismus} wenn sie den folgenden Ansprüchen genügt:
+Gegeben eine Menge $C$ von \emph{Komplementen} und zwei Monoiden $M$ und $N$ nennen wir eine partielle Funktion $\psi \colon C \times M \to C \times N$ einen \emph{zustandsbehafteten Monoidhomomorphismus}, wenn sie den folgenden Ansprüchen genügt:
 
 \begin{itemize}
    \item $\forall c \in C \colon \psi(1_M, c) = (1_N, c)$
@@ -28,7 +28,7 @@ type StateMonoidHom s m n = (s, m) -> (s, n)
 \end{defn}
 
 \begin{defn}[edit-lenses]
-Für Moduln $M$ und $N$ besteht eine \emph{symmetrische edit-lens} zwischen $M$ und $N$ aus zwei zustandsbehafteten Monoidhomomorphismen $\Rrightarrow \colon C \times \partial M \to C \times \partial N$ und $\Lleftarrow \colon C \times \partial N \to C \times \partial M$, mit kompatiblem Komplement $C$, einem ausgezeichneten Element $\ground_C \in C$ und einer \emph{Konsistenzrelation} $K \subset \Dom M \times C \times \Dom N$ sodass gilt:
+Für Moduln $M$ und $N$ besteht eine \emph{symmetrische edit-lens} zwischen $M$ und $N$ aus zwei zustandsbehafteten Monoidhomomorphismen $\Rrightarrow \colon C \times \partial M \to C \times \partial N$ und $\Lleftarrow \colon C \times \partial N \to C \times \partial M$, mit kompatiblem Komplement $C$, einem ausgezeichneten Element $\ground_C \in C$ und einer \emph{Konsistenzrelation} $K \subset \Dom M \times C \times \Dom N$, sodass gilt:
 
 \begin{itemize}
   \item $(\init_M, \ground_C, \init_N) \in K$
@@ -43,7 +43,7 @@ Für Moduln $M$ und $N$ besteht eine \emph{symmetrische edit-lens} zwischen $M$
 
 Wir schreiben auch nur \emph{edit-lens} für den symmetrischen Fall\footnote{Für den asymmetrischen Fall siehe \cite{johnson2016unifying}}.
 
-In Haskell erwähnen wir die Konsistenzrelation nicht in der Erwartung, dass $\Rrightarrow$ und $\Lleftarrow$ nur auf konsistente Zustände angewandt werden (und somit auch entweder einen konsistenten Zustand erzeugen oder nicht definiert sind):
+In Haskell erwähnen wir die Konsistenzrelation nicht, in der Erwartung, dass $\Rrightarrow$ und $\Lleftarrow$ nur auf konsistente Zustände angewandt werden (und somit auch entweder einen konsistenten Zustand erzeugen oder nicht definiert sind):
 
 \begin{code}
 data EditLens c m n where
@@ -67,12 +67,12 @@ instance (Module m, Module n) => HasEditLens (EditLens c m n) m n where
 \end{code}
 \end{defn}
 
-\subsection{Kompatibilität mit bestehenden lens frameworks}
+\subsection{Kompatibilität mit bestehenden lens Frameworks}
 
 Das einschlägige bestehende lens framework \cite{lens} konstruiert seine Linsen à la \citeauthor{laarhoven} wie folgt:
 
 \begin{defn}[lenses à la Laarhoven]
-Für Typen $n$ und $m$ ist eine \emph{lens} $\ell$ von $n$ in $m$ eine Abbildung\footnote{Gdw. die betrachtete Linse einen Isomorphismus kodiert wird auch über den verwendeten Profunktor anstatt $\to$ quantifiziert} folgender Struktur:
+Für Typen $n$ und $m$ ist eine \emph{lens} $\ell$ von $n$ in $m$ eine Abbildung\footnote{Gdw. die betrachtete Linse einen Isomorphismus kodiert, wird auch über den verwendeten Profunktor anstatt $\to$ quantifiziert} folgender Struktur:
 
 $$ \forall f \, \text{Funktor} \colon \left ( \ell \colon \left ( m \to f(m) \right ) \to \left ( n \to f(n) \right ) \right )$$
 
@@ -80,7 +80,7 @@ Durch geschickte Wahl des Funktors\footnote{\texttt{Const m} bzw. \texttt{Identi
 \end{defn}
 
 Es liegt nun nahe $\nearrow \colon (m \to m) \to (n \to n)$ mit $\Rrightarrow \colon \partial m \to \partial n$ zu identifizieren.
-Und in der Tat, eine Funktion $\text{map} \colon (o \to o) \to \partial o$ für $o \in \{ m, n \}$ würde van Laarhoven-lenses in edit-lenses einbetten.
+In der Tat, eine Funktion $\text{map} \colon (o \to o) \to \partial o$ für $o \in \{ m, n \}$ würde van Laarhoven-lenses in edit-lenses einbetten.
 Die charakteristische Eigenschaft der Betrachtung als edit-lens, nämlich die algebraische Struktur von $\partial o$, würde hierbei jedoch notwendigerweise verloren gehen.
 
 Wegen diesem Argument haben wir entschieden keine Komponierbarkeit (durch $\text{id} \colon a \to a$ und $\circ \colon (b \to c) \to (a \to b) \to (a \to c)$, wie in \cite{lens}) von edit-lenses mit van Laarhoven-lenses anzustreben.