Much ado about nothing

5 files changed, 520 insertions, 235 deletions

diff --git a/edit-lens/src/Control/DFST.lhs b/edit-lens/src/Control/DFST.lhs
index eae2e66..6e16c74 100644
--- a/edit-lens/src/Control/DFST.lhs
+++ b/edit-lens/src/Control/DFST.lhs
@@ -1,6 +1,7 @@
+\begin{comment}
 \begin{code}
 {-# LANGUAGE ScopedTypeVariables
-#-}
+  #-}
 
 {-|
 Description: Deterministic finite state transducers
@@ -11,8 +12,8 @@ module Control.DFST
   , toFST
   ) where
 
-import Data.Map.Strict (Map, (!?))
-import qualified Data.Map.Strict as Map
+import Data.Map.Lazy (Map, (!?))
+import qualified Data.Map.Lazy as Map
 
 import Data.Set (Set)
 import qualified Data.Set as Set
@@ -29,18 +30,34 @@ import Control.Monad.State
 
 import Control.FST (FST(FST))
 import qualified Control.FST as FST
+\end{code}
+\end{comment}
 
+\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ände einelementig ist.
 
+  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}
+  
+\begin{code}
 data DFST state input output = DFST
   { stInitial :: state
   , stTransition :: Map (state, input) (state, Seq output)
-    -- ^ All @(s, c)@-combinations not mapped are assumed to map to @(s, Nothing)@
   , stAccept :: Set state
   }
+\end{code}
 
+Die in der Definition von DFSTs beschriebene Umwandlung lässt sich umkehren, sich also jeder DFST auch als FST auffassen.
 
+Hierfür trennen wir Transitionen $A \overset{(\sigma, \delta^\ast)}{\rightarrow} B$ mit Eingabe $\sigma$ und Ausgabe-Wort $\delta^\ast = \delta_1 \delta_2 \ldots \delta_n$ in eine Serie von Transitionen $A \overset{(\sigma, \delta_1)}{\rightarrow} A_1 \overset{(\epsilon, \delta_2)}{\rightarrow} \ldots \overset{(\epsilon, \delta_n)}{\rightarrow} B$ auf.
+
+\begin{code}
 toFST :: forall state input output. (Ord state, Ord input, Ord output) => DFST state input output -> FST (state, Maybe (input, Natural)) input output
--- ^ Split apart non-singleton outputs into a series of epsilon-transitions
+-- ^ View a DFST as a FST splitting apart non-singleton outputs into a series of epsilon-transitions
+\end{code}
+\begin{comment}
+\begin{code}
 toFST DFST{..} = flip execState initialFST $ forM_ (Map.toList stTransition) handleTransition
   where
     initialFST = FST
@@ -62,21 +79,31 @@ toFST DFST{..} = flip execState initialFST $ forM_ (Map.toList stTransition) han
               -- Both calls to `handleTransition'` (one in `handleTransition`, the other below) satisfy one of the above cases
       addTransition (from, inS) (next, Just outS)
       handleTransition' next Nothing oo to
-  
+\end{code}
+\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.
+
+\begin{code}
 runDFST :: forall state input output. (Ord state, Ord input) => DFST state input output -> Seq input -> Maybe (Seq output)
-runDFST dfst@DFST{..} str = let (finalState, str') = runDFST' dfst stInitial str Seq.empty
-                            in str' <$ guard (finalState `Set.member` stAccept)
+\end{code}
+\begin{comment}
+\begin{code}
+runDFST dfst@DFST{..} str = do
+  let (str', finalState') = runDFST' dfst stInitial str Seq.empty
+  finalState <- finalState'
+  str' <$ guard (finalState `Set.member` stAccept)
 
 runDFST' :: forall state input output. (Ord state, Ord input)
          => DFST state input output
          -> state               -- ^ Current state
          -> Seq input           -- ^ Remaining input
          -> Seq output          -- ^ Accumulator containing previous output
-         -> (state, Seq output) -- ^ Next state, altered output
-runDFST' _             st  Empty     acc = (st, acc)
-runDFST' dfst@DFST{..} st (c :<| cs) acc
-  | Just (st', mc') <- stTransition !? (st, c)
-  = runDFST' dfst st' cs $ acc <> mc'
-  | otherwise
-  = runDFST' dfst st cs acc
+         -> (Seq output, Maybe state) -- ^ Altered output, Next state
+runDFST' _             st  Empty     acc = (acc, Just st)
+runDFST' dfst@DFST{..} st (c :<| cs) acc = case stTransition !? (st, c) of
+  Just (st', mc') -> runDFST' dfst st' cs $ acc <> mc'
+  Nothing -> (acc, Nothing)
 \end{code}
+\end{comment}
diff --git a/edit-lens/src/Control/DFST/Lens.lhs b/edit-lens/src/Control/DFST/Lens.lhs
index 95be34e..fe33bd6 100644
--- a/edit-lens/src/Control/DFST/Lens.lhs
+++ b/edit-lens/src/Control/DFST/Lens.lhs
@@ -1,12 +1,14 @@
+\begin{comment}
 \begin{code}
 {-# LANGUAGE ScopedTypeVariables
            , TemplateHaskell
            , ConstraintKinds
+           , GeneralizedNewtypeDeriving
 #-}
 
 module Control.DFST.Lens
-  ( StringEdit(..)
-  , StringEdits(..)
+  ( StringEdit(..), sePos, seInsertion
+  , StringEdits(..), _StringEdits, _SEFail, stringEdits
   , insert, delete, replace
   , DFSTAction(..), DFSTComplement
   , dfstLens
@@ -16,7 +18,7 @@ module Control.DFST.Lens
 
 import Control.DFST
 import Control.FST hiding (stInitial, stTransition, stAccept)
-import qualified Control.FST as FST (stInitial, stTransition, stAccept)
+import qualified Control.FST as FST (stInitial, stTransition, stAccept, step)
 import Control.Lens.Edit
 import Control.Lens
 import Control.Lens.TH
@@ -32,11 +34,11 @@ import Data.Sequence (Seq((:<|), (:|>)))
 import qualified Data.Sequence as Seq
 import Data.Set (Set)
 import qualified Data.Set as Set
-import Data.Map.Strict (Map)
-import qualified Data.Map.Strict as Map
+import Data.Map.Lazy (Map)
+import qualified Data.Map.Lazy as Map
 
-import Data.Compositions.Snoc (Compositions)
-import qualified Data.Compositions.Snoc as Comp
+import Data.Compositions (Compositions)
+import qualified Data.Compositions as Comp
 
 import Data.Algorithm.Diff (Diff, getDiff)
 import qualified Data.Algorithm.Diff as Diff
@@ -48,69 +50,72 @@ import Data.Function (on)
 import Data.Foldable (toList)
 import Data.List (partition)
 
-import Debug.Trace
+import Control.Exception (assert)
 
+import System.IO.Unsafe
+import Text.PrettyPrint.Leijen (Pretty(..))
 
-data StringEdit char = Insert { _sePos :: Natural, _seInsertion :: char }
-                     | Delete { _sePos :: Natural }
+\end{code}
+\end{comment}
+
+
+Wir betrachten, zur Einfachheit, ein minimiales Set von Edits auf Strings\footnote{Wie in der Konstruktion zum Longest Common Subsequence Problem}:
+
+\begin{defn}[Atomare edits of strings]
+\begin{code}
+data StringEdit pos char = Insert { _sePos :: pos, _seInsertion :: char }
+                         | Delete { _sePos :: pos }
   deriving (Eq, Ord, Show, Read)
 
+-- Automatically derive van-leerhoven-lenses:
+--
+-- @sePos :: Lens' (StringEdits pos char) pos@
+-- @seInsertion :: Traversal' (StringEdits pos char) char@
 makeLenses ''StringEdit
+\end{code}
+\end{defn}
 
-data StringEdits char = StringEdits (Seq (StringEdit char))
-                      | SEFail
+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))
+                          | SEFail
   deriving (Eq, Ord, Show, Read)
 
 makePrisms ''StringEdits
 
-stringEdits :: Traversal' (StringEdits char) (StringEdit char)
+stringEdits :: Traversal (StringEdits pos char) (StringEdits pos' char') (StringEdit pos char) (StringEdit pos' char')
+\end{code}
+\begin{comment}
+\begin{code}
 stringEdits = _StringEdits . traverse
-
-affected :: forall char. StringEdits char -> Maybe (Interval Natural)
--- ^ For a given set of edits @es@ return the interval @i = a ... b@ such that for any given string @str@ of sufficient length the following holds:
---
---   - For all @n :: Natural@: @n < a ==> str ! n == (str `apply` es) ! n@
---   - There exists a @k :: Integer@ such that for all @n :: Integer@: @n > b ==> str ! (n + k) == (str `apply` es) ! n@
---
--- Intuitively: for any character @c@ of the new string @str `apply` es@ there exists a corresponding character in @str@ (offset by either 0 or a constant shift @k@) if the index of @c@ is /not/ contained in @affected es@.
-affected SEFail = Nothing
-affected (StringEdits es) = Just . toInterval $ go es Map.empty
-  where
-    toInterval :: Map Natural Integer -> Interval Natural
-    toInterval map
-      | Just (((minK, _), _), ((maxK, _), _)) <- (,) <$> Map.minViewWithKey map <*> Map.maxViewWithKey map
-      = let
-          maxV' = maximum . (0 :) $ do
-            offset <- [0..maxK]
-            v <- maybeToList $ Map.lookup (maxK - offset) map
-            v' <- maybeToList . fmap fromInteger $ negate v <$ guard (v <= 0)
-            guard $ v' >= succ offset
-            return $ v' - offset
-        in (minK Int.... maxK + maxV')
-      | otherwise
-      = Int.empty
-    go :: Seq (StringEdit char) -> Map Natural Integer -> Map Natural Integer
-    go Seq.Empty offsets = offsets
-    go (es :> e) offsets = go es offsets'
-      where
-        p = e ^. sePos
-        p' = fromIntegral $ Map.foldrWithKey (\k o p -> bool (fromIntegral p) (o + p) $ k < fromIntegral p) (fromIntegral p) offsets
-        offsets' = Map.alter (Just . myOffset . fromMaybe 0) p offsets
-        myOffset :: Integer -> Integer
-        myOffset
-          | Insert _ _ <- e = pred
-          | Delete _   <- e = succ
-
-insert :: Natural -> char -> StringEdits char
+\end{code}
+\end{comment}
+\begin{code}
+insert :: pos -> char -> StringEdits pos char
+\end{code}
+\begin{comment}
+\begin{code}
 insert n c = StringEdits .  Seq.singleton $ Insert n c
-  
-delete :: Natural -> StringEdits char
+\end{code}
+\end{comment}
+\begin{code}
+delete :: pos -> StringEdits pos char
+\end{code}
+\begin{comment}
+\begin{code}
 delete n = StringEdits .  Seq.singleton $ Delete n
-
-replace :: Natural -> char -> StringEdits char
+\end{code}
+\end{comment}
+\begin{code}
+replace :: Eq pos => pos -> char -> StringEdits pos char
+\end{code}
+\begin{comment}
+\begin{code}
 replace n c = insert n c <> delete n
 
-instance Monoid (StringEdits char) where
+-- | Rudimentarily optimize edit composition
+instance Eq pos => Monoid (StringEdits pos char) where
   mempty = StringEdits Seq.empty
   SEFail `mappend` _ = SEFail
   _ `mappend` SEFail = SEFail
@@ -122,12 +127,16 @@ instance Monoid (StringEdits char) where
     , n == n'
     = StringEdits bs `mappend` StringEdits as
     | otherwise = StringEdits $ x `mappend` y
+\end{code}
+\end{comment}
 
-instance Module (StringEdits char) where
-  type Domain (StringEdits char) = Seq char
+Da wir ein minimales set an atomaren edits gewählt haben, ist die Definiton der Modulnstruktur über Strings des passenden Alphabets recht einfach:
+\begin{code}
+instance Module (StringEdits Natural char) where
+  type Domain (StringEdits Natural char) = Seq char
   apply str SEFail = Nothing
   apply str (StringEdits Seq.Empty) = Just str
-  apply str (StringEdits (es :|> Insert n c)) = (flip apply) (StringEdits es) =<< go str n c
+  apply str (StringEdits (es :|> Insert n c)) = flip apply (StringEdits es) =<< go str n c
     where
       go Seq.Empty n c
         | n == 0 = Just $ Seq.singleton c
@@ -135,7 +144,7 @@ instance Module (StringEdits char) where
       go str@(x :<| xs) n c
         | n == 0 = Just $ c <| str
         | otherwise = (x <|) <$> go xs (pred n) c
-  apply str (StringEdits (es :|> Delete n)) = (flip apply) (StringEdits es) =<< go str n
+  apply str (StringEdits (es :|> Delete n)) = flip apply (StringEdits es) =<< go str n
     where
       go Seq.Empty _ = Nothing
       go (x :<| xs) n
@@ -146,99 +155,128 @@ instance Module (StringEdits char) where
   divInit = StringEdits . Seq.unfoldl go . (0,)
     where
       go (_, Seq.Empty) = Nothing
-      go (n, (c :<| cs)) = Just ((succ n, cs), Insert n c)
+      go (n, c :<| cs ) = Just ((succ n, cs), Insert n c)
 
 \end{code}
 
 % TODO Make notation mathy
 
-Um zunächst eine asymmetrische edit-lens `StringEdits -> StringEdits` mit akzeptabler Komplexität für einen bestimmten `DFST s` (entlang der \emph{Richtung} des DFSTs) zu konstruieren möchten wir folgendes Verfahren anwenden:
+Um zunächst eine asymmetrische edit-lens \texttt{StringEdits -> StringEdits} mit akzeptabler Komplexität für einen bestimmten DFST (entlang der \emph{Richtung} des DFSTs) zu konstruieren möchten wir folgendes Verfahren anwenden:
 
-Gegeben eine Sequenz (`StringEdits`) von zu übersetzenden Änderungen genügt es die Übersetzung eines einzelnen `StringEdit`s in eine womöglich längere Sequenz von `StringEdits` anzugeben, alle `StringEdits` aus der Sequenz zu übersetzen (hierbei muss auf die korrekte Handhabung des Komplements geachtet werden) und jene Übersetzungen dann zu concatenieren.
+Gegeben eine Sequenz von zu übersetzenden Änderungen genügt es die Übersetzung eines einzelnen \texttt{StringEdit}s in eine womöglich längere Sequenz von \texttt{StringEdits} anzugeben, alle \texttt{StringEdits} aus der Sequenz derart zu übersetzen (hierbei muss auf die korrekte Handhabung des Komplements geachtet werden) und jene Übersetzungen dann zu concatenieren.
 
-Wir definieren zunächst die \emph{Wirkung} eines DFST auf einen festen String als eine Abbildung `state -> (state, String)`, die den aktuellen Zustand vorm Parsen des Strings auf den Zustand danach und die (womöglich leere) Ausgabe schickt.
+Wir definieren zunächst die \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.
 
-Die Unterliegende Idee ist nun im Komplement der edit-lens eine Liste von Wirkungen (eine für jedes Zeichen der Eingabe des DFSTs) und einen Cache der monoidalen Summen aller kontinuirlichen Teillisten zu halten.
-Da wir wissen welche Stelle im input-String von einem gegebenen edit betroffen ist können wir, anhand der Wirkung des Teilstücks bis zu jener Stelle, den output-String in einen durch den edit unveränderten Prefix und einen womöglich betroffenen Suffix unterteilen.
-Die Wirkung ab der betroffenen Stelle im input-String können wir also 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 Bestimmten zu bestimmen.
-
-
-% Für die Rückrichtung bietet es sich an eine Art primitive Invertierung des DFSTs zu berechnen.
-% Gegeben den aktuellen DFST $A$ möchten wir einen anderen $A^{-1}$ finden, sodass gilt:
-
-% \begin{itemize}
-%   \item $A^{-1}$ akzeptiert einen String $s^{-1}$ (endet seinen Lauf in einem finalen Zustand) gdw. es einen String $s$ gibt, der unter $A$ die Ausgabe $s^{-1}$ produziert.
-%   \item Wenn $A^{-1}$ einen String $s^{-1}$ akzeptiert so produziert die resultierende Ausgabe $s$ unter $A$ die Ausgabe $s^{-1}$.
-% \end{itemize}
-
-% Kann nicht funktionieren, denn $A^{-1}$ ist notwendigerweise nondeterministisch. Wird $A^{-1}$ dann zu einem DFST forciert (durch arbiträre Wahl einer Transition pro Zustand) gehen Informationen verloren—$A^{-1}$ produziert nicht den minimale edit auf dem input string (in der Tat beliebig schlecht) für einen gegeben edit auf dem output string.
-  
-% Stelle im bisherigen Lauf isolieren, an der edit im output-string passieren soll, breitensuche auf pfaden, die sich von dieser stelle aus unterscheiden?
-% Gegeben einen Pfad und eine markierte Transition, finde Liste aller Pfade aufsteigend sortiert nach Unterschied zu gegebenem Pfad, mit Unterschieden "nahe" der markierten Transition zuerst — zudem jeweils edit auf dem Eingabestring
-% Einfacher ist Breitensuche ab `stInitial` und zunächst diff auf eingabe-strings.
-  
 \begin{code}
-
 data DFSTAction state input output = DFSTAction
-  { runDFSTAction :: state -> (state, Seq output)
+  { runDFSTAction :: state -> (Seq output, Maybe state)
   , dfstaConsumes :: Seq input
   }
 
 instance Monoid (DFSTAction state input output) where
-  mempty = DFSTAction (\x -> (x, Seq.empty)) Seq.empty
+\end{code}
+\begin{comment}
+\begin{code}
+  mempty = DFSTAction (\x -> (Seq.empty, Just x)) Seq.empty
   DFSTAction f cf `mappend` DFSTAction g cg = DFSTAction
-    { runDFSTAction = \s -> let ((f -> (s', out')), out) = g s in (s', out <> out')
+    { runDFSTAction = \x ->
+        let (outG, x') = g x
+            (outF, x'') = maybe (mempty, Nothing) f x'
+         in (outG <> outF, x'')
     , dfstaConsumes = cg <> cf
     }
+\end{code}
+\end{comment}
+\begin{code}
 
 type DFSTComplement state input output = Compositions (DFSTAction state input output)
 
-runDFSTAction' :: DFSTComplement state input output -> state -> (state, Seq output)
+runDFSTAction' :: DFSTComplement state input output -> state -> (Seq output, Maybe state)
 runDFSTAction' = runDFSTAction . Comp.composed
 
 dfstaConsumes' :: DFSTComplement state input output -> Seq input
 dfstaConsumes' = dfstaConsumes . Comp.composed
 
-dfstaProduces :: DFST state input output -> DFSTComplement state input output -> Seq output
-dfstaProduces DFST{..} = snd . flip runDFSTAction' stInitial
+dfstaProduces :: DFSTComplement state input output -> state -> Seq output
+dfstaProduces = fmap fst . runDFSTAction'
+\end{code}
 
-type Debug state input output = (Show state, Show input, Show output)
+Die Unterliegende Idee von $\Rrightarrow$ ist nun im Komplement der edit-lens eine Liste von Wirkungen (eine für jedes Zeichen der Eingabe des DFSTs) und einen Cache der monoidalen Summen aller kontinuirlichen Teillisten zu halten.
 
-type LState state input output = (Natural, (state, Maybe (input, Natural)))
+Wir können die alte DFST-Wirkung zunächst anhand des Intervalls indem der input-String von allen gegebenen edits betroffen ist 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.
+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.
+
+Für die asymmetrische edit-lens entgegen der DFST-Richtung $\Lleftarrow$ verwenden wir Breitensuche über die Zustände des DFST innerhalb eines iterative vergrößerten Intervalls:
+
+Wir bestimmen zunächst (`affected`) eine obere Schranke an das Intervall in dem der Ausgabe-String vom edit betroffen ist und generieren eine von dort quadratisch wachsende Serie von Intervallen.
+
+Für jedes Intervall ("lokalere" Änderungen werden präferiert) schränken wir zunächst den DFST (zur einfachereren Implementierung in seiner Darstellung als FST) vermöge \texttt{restrictOutput} derart ein, dass nur die gewünschte Ausgabe produziert werden kann.
 
-dfstLens :: forall state input output. (Ord state, Ord input, Ord output, Debug state input output) => DFST state input output -> EditLens (DFSTComplement state input output) (StringEdits input) (StringEdits output)
+Wir betrachten dann in jedem Schritt (beginnend mit dem initialen Zustand des DFST) alle ausgehenden Transitionen und ziehen hierbei jene vor, die im vorherigen Lauf (gespeichert im Komplement der edit-lens), ebenfalls genommen wurden.
+Abweichungen vom im Komplement gespeicherten Lauf lassen wir nur innerhalb des betrachteten Intervalls zu und wählen in diesem Fall einen Edit auf der Eingabe, der die gewählte Abweichung produziert.
+Es wird zudem, wie für Breitensuche üblich, jeder besuchte Zustand markiert und ausgehende Transitionen nicht ein zweites mal betrachtet.
+
+Erreichen wir einen finalen Zustand (wegen der Einschränkung des DFSTs wurde dann auch genau die gewünschte Ausgabe produziert), so fügen wir an die gesammelten Eingabe-edits eine Serie von deletions an, die den noch nicht konsumierten suffix der Eingabe verwerfen und brechen die Suche unter Rückgabe der Eingabe-edits und des neuen Laufs ab.
+
+In Haskell formulieren wir das vorzeitige Abbrechen der Suche indem wir eine vollständige Liste von Rückgabe-Kandidaten konstruieren und dann immer ihr erstes Element zurück geben.
+Wegen der verzögerten Auswertungsstrategie von Haskell wird auch tatsächlich nur der erste Rückgabe-Kandidat konstruiert.
+
+\begin{comment}
+\begin{code}
+type LState state input output = (Natural, (state, Maybe (input, Natural)))
+\end{code}
+\end{comment}
+\begin{code}
+dfstLens :: forall state input output. (Ord state, Ord input, Ord output, Show state, Show input, Show output) => DFST state input output -> EditLens (DFSTComplement state input output) (StringEdits Natural input) (StringEdits Natural output)
+\end{code}
+\begin{comment}
+\begin{code}
 dfstLens dfst@DFST{..} = EditLens ground propR propL
   where
     ground :: DFSTComplement state input output
-    ground = Comp.fromList []
+    ground = mempty
 
-    propR :: (DFSTComplement state input output, StringEdits input) -> (DFSTComplement state input output, StringEdits output)
+    propR :: (DFSTComplement state input output, StringEdits Natural input) -> (DFSTComplement state input output, StringEdits Natural output)
     propR (c, SEFail) = (c, SEFail)
     propR (c, StringEdits Seq.Empty) = (c, mempty)
-    propR (c, StringEdits (es :> e))
-      | fst (runDFSTAction' c' stInitial) `Set.member` stAccept = (c', es' <> es'')
-      | otherwise                                               = (c', SEFail)
+    propR (c, es'@(StringEdits (es :> e)))
+      | (_, Just final) <- runDFSTAction' c' stInitial
+      , final `Set.member` stAccept
+      = (c', rEs)
+      | otherwise
+      = (c, SEFail)
       where
+        Just int = affected es'
+        (cAffSuffix, cAffPrefix) = Comp.splitAt (Comp.length c - fromIntegral (Int.inf int)) c
         (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (e ^. sePos . from enum)) c
         cSuffix'
-          | Delete _       <- e = Comp.take (pred $ Comp.length cSuffix) cSuffix -- TODO unsafe
+          | Delete _       <- e
+          , Comp.length cSuffix > 0 = Comp.take (pred $ Comp.length cSuffix) cSuffix
           | Insert _ nChar <- e = cSuffix <> Comp.singleton (DFSTAction (\x -> runDFST' dfst x (pure nChar) Seq.empty) (Seq.singleton nChar))
-        (pState, pOutput)  = runDFSTAction' cPrefix stInitial
-        (_, sOutput ) = runDFSTAction' cSuffix  pState
-        (_, sOutput') = runDFSTAction' cSuffix' pState
-        (c', es') = propR (cSuffix' <> cPrefix, StringEdits es)
-        es'' = strDiff sOutput sOutput' & stringEdits . sePos . from enum +~ Seq.length pOutput
+          | otherwise = Comp.singleton $ DFSTAction (\_ -> (Seq.empty, Nothing)) Seq.empty
+        (c', _) = propR (cSuffix' <> cPrefix, StringEdits es)
+        (cAffSuffix', _) = Comp.splitAt (Comp.length c' - Comp.length cAffPrefix) c'
+        (_, Just pFinal) = runDFSTAction' cPrefix stInitial
+        rEs = strDiff (fst $ runDFSTAction' cAffSuffix pFinal) (fst $ runDFSTAction' cAffSuffix' pFinal) & stringEdits . sePos . from enum +~ length (dfstaProduces cAffPrefix stInitial)
         
 
-    propL :: (DFSTComplement state input output, StringEdits output) -> (DFSTComplement state input output, StringEdits input)
+    propL :: (DFSTComplement state input output, StringEdits Natural output) -> (DFSTComplement state input output, StringEdits Natural input)
     propL (c, StringEdits Seq.Empty) = (c, mempty)
     propL (c, es) = fromMaybe (c, SEFail) $ do
+      let prevOut = dfstaProduces c stInitial
       newOut <- prevOut `apply` es
       affected' <- affected es
       let outFST :: FST (LState state input output) input output
-          outFST = wordFST newOut `productFST` toFST dfst
+          -- outFST = wordFST newOut `productFST` toFST dfst
+          outFST = restrictOutput newOut $ toFST dfst
+      
+          trace x y = flip seq y . unsafePerformIO $ appendFile "lens.log" (x <> "\n\n")
+
           inflate by int
             | Int.null int = Int.empty
             | inf >= by = inf - by Int.... sup + by
@@ -251,53 +289,90 @@ dfstLens dfst@DFST{..} = EditLens ground propR propL
               max = fromIntegral $ Seq.length newOut
               all = 0 Int.... max
           runCandidates :: Interval Natural -- ^ Departure from complement-run only permitted within interval (to guarantee locality)
-                       -> [ ( Seq (LState state input output, Maybe output) -- ^ Computed run
-                            , StringEdits input
-                            , DFSTComplement state input output
-                            )
-                          ]
-          runCandidates focus = continueRun (Seq.empty, mempty) (c, mempty) 0
+                        -> [ ( Seq (LState state input output, Maybe output) -- ^ Computed run
+                             , StringEdits Natural input
+                             , DFSTComplement state input output
+                             )
+                           ]
+          runCandidates focus = map ((,,) <$> view _1 <*> view _2 <*> view (_3 . _2)) $ go Set.empty [(Seq.empty, mempty, (c, mempty), 0)]
             where
-              continueRun :: (Seq (LState state input output, Maybe output), StringEdits input)
+              go _ [] = []
+              go visited (args@(run, edits, compZipper, inP) : alts) = 
+                  [ (run', finalizeEdits remC inP' edits', compZipper', inP') | (run', edits', compZipper'@(remC, _), inP') <- args : conts, isFinal run' ]
+                  ++ go visited' (alts ++ conts)
+                where
+                  conts
+                    | lastSt <- view _1 <$> Seq.lookup (pred $ Seq.length run) run
+                    , lastSt `Set.member` visited = []
+                    | otherwise = continueRun edits compZipper inP run
+                  visited' = Set.insert (view _1 <$> Seq.lookup (pred $ Seq.length run) run) visited
+
+              isFinal :: Seq (LState state input output, Maybe output) -> Bool
+              -- ^ Is the final state of the run a final state of the DFST?
+              isFinal Seq.Empty = (0, (stInitial, Nothing)) `Set.member` FST.stAccept outFST
+                               && (0 Int.... fromIntegral (Seq.length newOut)) `Int.isSubsetOf` focus
+              isFinal (_ :> (lastSt, _)) = lastSt `Set.member` FST.stAccept outFST
+
+              finalizeEdits :: DFSTComplement state input output -- ^ Remaining complement
+                            -> Natural -- ^ Input position
+                            -> StringEdits Natural input -> StringEdits Natural input
+              finalizeEdits remC inP = mappend . mconcat . replicate (Seq.length $ dfstaConsumes' remC) $ delete inP
+              
+              continueRun :: StringEdits Natural input
                           -> (DFSTComplement state input output, DFSTComplement state input output) -- ^ Zipper into complement
                           -> Natural -- ^ Input position
-                          -> [(Seq (LState state input output, Maybe output), StringEdits input, DFSTComplement state input output)]
-              continueRun (run, inEdits) (c', remC) inP = do
+                          -> Seq (LState state input output, Maybe output)
+                          -> [ ( Seq (LState state input output, Maybe output)
+                               , StringEdits Natural input
+                               , (DFSTComplement state input output, DFSTComplement state input output)
+                               , Natural
+                               )
+                             ]
+              -- ^ Nondeterministically make a single further step, continueing a given run
+              continueRun inEdits (c', remC) inP run = do
                 let
                   pos :: Natural
-                  pos = fromIntegral $ Comp.length c - Comp.length c'
+                  -- pos = fromIntegral $ Comp.length c - Comp.length c' -- FIXME: should use length of dfstaProduces
+                  pos = fromIntegral . Seq.length $ dfstaProduces remC stInitial
                   (c'', step) = Comp.splitAt (pred $ Comp.length c') c' -- TODO: unsafe?
                   current :: LState state input output
                   current
                     | Seq.Empty <- run      = (0, (stInitial, Nothing))
                     | (_ :> (st, _)) <- run = st
                   current' :: state
-                  current' = let (_, (st, _)) = current
-                              in st
-                  next' :: state
-                  next' = fst . runDFSTAction' step $ current'
                   oldIn :: Maybe input
-                  oldIn = Seq.lookup 0 $ dfstaConsumes' step
+                  (current', oldIn)
+                    | (_ :> ((_, (st, _)), _)) <- rest
+                    , (_ :> ((_, (_, Just (partialIn, _))), _)) <- partial = (st, Just partialIn)
+                    | (_ :> ((_, (_, Just (partialIn, _))), _)) <- partial = (stInitial, Just partialIn)
+                    | Seq.Empty <- rest = (stInitial, Seq.lookup 0 $ dfstaConsumes' step)
+                    | (_ :> ((_, (st, _)), _)) <- rest = (st, Seq.lookup 0 $ dfstaConsumes' step)
+                    where
+                      (partial, rest) = Seq.spanr (\((_, (_, inp)), _) -> isJust inp) run
+                next' <- trace (show ("next'", pos, focus, run, (current', oldIn), current, dfstaConsumes' step, runDFST' dfst current' (maybe Seq.empty Seq.singleton oldIn) Seq.empty)) . maybeToList . snd $ runDFST' dfst current' (maybe Seq.empty Seq.singleton oldIn) Seq.empty
+                let
                   outgoing :: LState state input output -> [(LState state input output, Maybe input, Maybe output)]
-                  outgoing current = let go (st, minS) os acc
-                                           | st == current = ($ acc) $ Set.fold (\(st', moutS) -> (. ((st', minS, moutS) :))) id os
+                  outgoing current = let go (st, minS) outs acc
+                                           | st == current = Set.foldr (\(st', moutS) -> ((st', minS, moutS) :)) acc outs
                                            | otherwise     = acc
                                       in Map.foldrWithKey go [] $ FST.stTransition outFST 
                   isPreferred :: (LState state input output, Maybe input, Maybe output) -> Bool
-                  isPreferred ((_, (st, Nothing)), inS, _) = st == next' && (fromMaybe True $ (==) <$> oldIn <*> inS)
-                  isPreferred (st, _, _) = any isPreferred $ outgoing st -- By construction of `outFST`, `outgoing st` is a singleton
+                  isPreferred ((_, (st, Nothing)), _, _) = st == next'
+                  isPreferred (st@(_, (_, Just (inS , _))), _, _) = maybe True (== inS) oldIn && any isPreferred (outgoing st) -- By construction of `outFST`, `outgoing st` is a singleton in this case
                   (preferred, alternate) = partition isPreferred $ outgoing current
                   assocEdit :: (LState state input output, Maybe input, Maybe output) -- ^ Transition
                             -> [ ( (DFSTComplement state input output, DFSTComplement state input output) -- ^ new `(c', remC)`, i.e. complement-zipper `(c', remC)` but with edit applied
-                                 , StringEdits input
+                                 , StringEdits Natural input
                                  , Natural
                                  )
                                ]
                   assocEdit (_, Just inS, _)
-                    | oldIn == Just inS = [((c'', step <> remC), mempty, succ inP)]
-                    | isJust oldIn      = [((c'', altStep inS <> remC), replace inP inS, succ inP), ((c', altStep inS <> remC), insert inP inS, succ inP)]
-                    | otherwise         = [((c', altStep inS <> remC), insert inP inS, succ inP)]
-                  assocEdit (_, Nothing, _) = [((c', remC), mempty, inP)] -- TODO: is this correct?
+                    | oldIn == Just inS = [ ((c'', step <> remC), mempty, succ inP) ]
+                    | isJust oldIn      = [ ((c', altStep inS <> remC), insert inP inS, succ inP)
+                                          , ((c'', altStep inS <> remC), replace inP inS, succ inP)
+                                          ]
+                    | otherwise         = [ ((c', altStep inS <> remC), insert inP inS, succ inP) ]
+                  assocEdit (_, Nothing, _) = [((c', remC), mempty, inP)]
                   altStep :: input -> DFSTComplement state input output
                   altStep inS = Comp.singleton DFSTAction{..}
                     where
@@ -306,7 +381,7 @@ dfstLens dfst@DFST{..} = EditLens ground propR propL
                   options
                     | pos `Int.member` focus = preferred ++ alternate
                     | otherwise              = preferred
-                choice@(next, inS, outS) <- options
+                choice@(next, inS, outS) <- trace (unlines $ show (pretty outFST) : map show options) options
                 ((c3, remC'), inEdits', inP') <- assocEdit choice
                 -- let
                 --   -- | Replace prefix of old complement to reflect current candidate
@@ -317,27 +392,70 @@ dfstLens dfst@DFST{..} = EditLens ground propR propL
                 --   fin
                 --     | (trans, inEs, newComplement) <- acc = (trans, dropSuffix <> inEs, newComplement)
                 let
-                  acc = (run :> (next, outS), inEdits' <> inEdits)
-                  dropSuffix = mconcat (replicate (Seq.length $ dfstaConsumes' c3) $ delete inP')
-                  fin
-                    | (trans, inEs) <- acc = (trans, dropSuffix <> inEs, remC')
-                bool id (fin :) (next `Set.member` FST.stAccept outFST) $ continueRun acc (c3, remC') inP'
+                  trans = run :> (next, outS)
+                  inEs = inEdits' <> inEdits
+                --   dropSuffix = mconcat (replicate (Seq.length $ dfstaConsumes' c3) $ delete inP')
+                --   fin
+                --     | (trans, inEs) <- acc = (trans, dropSuffix <> inEs, remC')
+                -- bool id (over _BFS $ cons fin) (next `Set.member` FST.stAccept outFST) $ continueRun acc (c3, remC') inP'
+                return (trans, inEs, (c3, remC'), inP')
               
       -- Properties of the edits computed are determined mostly by the order candidates are generated below
       -- (_, inEs, c') <- (\xs -> foldr (\x f -> x `seq` f) listToMaybe xs $ xs) $ traceShowId fragmentIntervals >>= (\x -> (\y@(y1, y2, _) -> traceShow (y1, y2) y) <$> runCandidates x)
 
-      (_, inEs, c') <- listToMaybe $ runCandidates =<< fragmentIntervals
-      
-      return (c', inEs)
-      where
-        (_, prevOut) = runDFSTAction' c stInitial
+      fmap ((,) <$> view _3 <*> view _2) .  listToMaybe $ runCandidates =<< fragmentIntervals
 
-strDiff :: forall sym. Eq sym => Seq sym -> Seq sym -> StringEdits sym
+strDiff :: forall sym pos. (Eq sym, Integral pos) => Seq sym -> Seq sym -> StringEdits pos sym
 -- ^ @strDiff a b@ calculates a set of edits, which, when applied to @a@, produce @b@
-strDiff a b = snd . foldr toEdit (0, mempty) $ (getDiff `on` toList) a b
+strDiff a b = snd . foldl toEdit (0, mempty) $ (getDiff `on` toList) a b
+  where
+    toEdit :: (pos, StringEdits pos sym) -> Diff sym -> (pos, StringEdits pos sym)
+    toEdit (n, es) (Diff.Both _ _) = (succ n, es)
+    toEdit (n, es) (Diff.First _ ) = (n, delete n <> es)
+    toEdit (n, es) (Diff.Second c) = (succ n, insert n c <> es)
+\end{code}
+\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.
+
+\begin{code}
+affected :: forall char. StringEdits Natural char -> Maybe (Interval Natural)
+-- ^ For a given set of edits @es@ return the interval @i = a ... b@ such that for any given string @str@ of sufficient length the following holds:
+--
+--   - For all @n :: Natural@: @n < a ==> str ! n == (str `apply` es) ! n@
+--   - There exists a @k :: Integer@ such that for all @n :: Integer@: @n > b ==> str ! (n + k) == (str `apply` es) ! n@
+--
+-- Intuitively: for any character @c@ of the new string @str `apply` es@ there exists a corresponding character in @str@ (offset by either 0 or a constant shift @k@) if the index of @c@ is /not/ contained in @affected es@.
+\end{code}
+\begin{comment}
+\begin{code}
+affected SEFail = Nothing
+affected (StringEdits es) = Just . toInterval $ go es Map.empty
   where
-    toEdit :: Diff sym -> (Natural, StringEdits sym) -> (Natural, StringEdits sym)
-    toEdit (Diff.Both _ _) (n, es) = (succ n, es)
-    toEdit (Diff.First _ ) (n, es) = (n, delete n <> es)
-    toEdit (Diff.Second c) (n, es) = (succ n, insert n c <> es)
+    toInterval :: Map Natural Integer -> Interval Natural
+    toInterval map
+      | Just (((minK, _), _), ((maxK, _), _)) <- (,) <$> Map.minViewWithKey map <*> Map.maxViewWithKey map
+      = let
+          maxV' = maximum . (0 :) $ do
+            offset <- [0..maxK]
+            v <- maybeToList $ Map.lookup (maxK - offset) map
+            v' <- maybeToList . fmap fromInteger $ negate v <$ guard (v <= 0)
+            guard $ v' >= succ offset
+            return $ v' - offset
+        in (minK Int.... maxK + maxV')
+      | otherwise
+      = Int.empty
+    go :: Seq (StringEdit Natural char) -> Map Natural Integer -> Map Natural Integer
+    go Seq.Empty offsets = offsets
+    go (es :> e) offsets = go es offsets'
+      where
+        p = e ^. sePos
+        -- p' = fromIntegral $ Map.foldrWithKey (\k o p -> bool (fromIntegral p) (o + p) $ k < fromIntegral p) (fromIntegral p) offsets
+        offsets' = Map.alter (Just . myOffset . fromMaybe 0) p offsets
+        myOffset :: Integer -> Integer
+        myOffset
+          | Insert _ _ <- e = pred
+          | Delete _   <- e = succ
 \end{code}
+\end{comment}
diff --git a/edit-lens/src/Control/Edit.lhs b/edit-lens/src/Control/Edit.lhs
index 19fe336..8c4f045 100644
--- a/edit-lens/src/Control/Edit.lhs
+++ b/edit-lens/src/Control/Edit.lhs
@@ -16,7 +16,7 @@ Ein Modul $M$ ist eine \emph{partielle Monoidwirkung} zusammen mit einem schwach
 
 und einem Element $\init_M \in \Dom M$, sodass gilt:
 
-$$ \forall m \in \Dom M \ \exists \partial m \in \partial M \colon m = \init_M \cdot \partial m$$
+$$\forall m \in \Dom M \ \exists \partial m \in \partial M \colon m = \init_M \cdot \partial m$$
 
 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.
 
@@ -24,6 +24,7 @@ In Haskell charakterisieren wir Moduln über ihren Monoid, d.h. die Wahl des Mon
 Eine Repräsentierung als Typklasse bietet sich an:
 
 \begin{code}
+-- `apply` binds one level weaker than monoid composition `(<>)`
 infix 5 `apply`
 
 class Monoid m => Module m where
@@ -42,11 +43,12 @@ class Monoid m => Module m where
 
 infixl 5 `apply'`
 apply' :: Module m => Maybe (Domain m) -> m -> Maybe (Domain m)
+-- ^ `apply` under `Maybe`s monad-structure
 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) fordern, dass es ein schwach-initiales Element bzgl. der Monoidwirkung sei.
+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.
 
 \begin{comment}
 \begin{defn}[Modulhomomorphismen]
diff --git a/edit-lens/src/Control/FST.lhs b/edit-lens/src/Control/FST.lhs
index 9298e11..9aa5341 100644
--- a/edit-lens/src/Control/FST.lhs
+++ b/edit-lens/src/Control/FST.lhs
@@ -1,3 +1,4 @@
+\begin{comment}
 \begin{code}
 {-# LANGUAGE ScopedTypeVariables
 #-}
@@ -7,16 +8,18 @@ Description: Finite state transducers with epsilon-transitions
 -}
 module Control.FST
   ( FST(..)
+  -- * Using FSTs
+  , runFST, runFST', step
   -- * Constructing FSTs
   , wordFST
   -- * Operations on FSTs
-  , productFST, restrictFST
+  , productFST, restrictOutput, restrictFST
   -- * Debugging Utilities
   , liveFST
   ) where
 
-import Data.Map.Strict (Map, (!?))
-import qualified Data.Map.Strict as Map
+import Data.Map.Lazy (Map, (!?), (!))
+import qualified Data.Map.Lazy as Map
 
 import Data.Set (Set)
 import qualified Data.Set as Set
@@ -24,7 +27,7 @@ import qualified Data.Set as Set
 import Data.Sequence (Seq)
 import qualified Data.Sequence as Seq
 
-import Data.Maybe (mapMaybe, fromMaybe, isJust, fromJust)
+import Data.Maybe (mapMaybe, fromMaybe, isJust, fromJust, isNothing)
 
 import Numeric.Natural
 
@@ -35,12 +38,28 @@ import Control.Monad.State.Strict
 import Text.PrettyPrint.Leijen (Pretty(..))
 import qualified Text.PrettyPrint.Leijen as PP
 
-data FST state input output = FST
+\end{code}
+\end{comment}
+
+\begin{defn}[Finite state transducers]
+Unter einem 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.
+
+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.
+
+\begin{code}
+dFSeata FST state input output = FST
   { stInitial :: Set state
   , stTransition :: Map (state, Maybe input) (Set (state, Maybe output))
   , stAccept :: Set state
   } deriving (Show, Read)
+\end{code}
+\end{defn}
 
+\begin{comment}
+\begin{code}
 instance (Show state, Show input, Show output) => Pretty (FST state input output) where
   pretty FST{..} = PP.vsep
     [ PP.text "Initial states:" PP.</> PP.hang 2 (list . map (PP.text . show) $ Set.toAscList stInitial)
@@ -55,62 +74,164 @@ instance (Show state, Show input, Show output) => Pretty (FST state input output
     ]
     where
       label :: Show a => Maybe a -> PP.Doc
-      label = maybe (PP.text "ɛ") (PP.text . show)
+      label = PP.text . maybe "ɛ" show
       list :: [PP.Doc] -> PP.Doc
       list = PP.encloseSep (PP.lbracket PP.<> PP.space) (PP.space PP.<> PP.rbracket) (PP.comma PP.<> PP.space)
+\end{code}
+\end{comment}
 
-runFST :: forall input output state. (Ord input, Ord output, Ord state) => FST state input output -> Seq input -> [Seq output]
-runFST = fmap (map $ catMaybes . fmap (view _2) . view _2) . runFST'
-  where
-    catMaybes = fmap fromJust . Seq.filter isJust
+Wir definieren die 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.
+
+\begin{code}
+step :: forall input output state. (Ord input, Ord output, Ord state)
+     => FST state input output
+     -> Maybe state -- ^ Current state
+     -> Maybe input -- ^ Head of remaining input
+     -> [(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.
+
+\begin{code}
+step FST{..} (Just c) inS = let
+  consuming = fromMaybe Set.empty $ Map.lookup (c, inS) stTransition
+  unconsuming = fromMaybe Set.empty $ Map.lookup (c, Nothing) stTransition
+  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.
 
+\begin{code}
 runFST' :: forall input output state. (Ord input, Ord output, Ord state)
         => FST state input output
         -> Seq input
         -> [(state, Seq (state, Maybe output))] -- ^ Tuples of initial state and chosen transitions; not neccessarily finite
 -- ^ Compute all possible runs on the given input
-runFST' fst Seq.Empty = guardAccept $ (\(_, st, _) -> (st, Seq.Empty)) <$> step fst Nothing Nothing
-runFST' fst cs = guardAccept $ do
-  initial <- view _2 <$> step fst Nothing Nothing
-  go (initial, Seq.Empty) cs
+runFST' fst@FST{..} cs = do
+  initial <- view _2 <$> step fst Nothing Nothing -- Nondeterministically choose an initial state
+  go (initial, Seq.Empty) cs -- Recursively extend the run consisting of only the initial state
   where
-    guardAccept res = do
-      (initial, path) <- res
-      let
-        finalState
-          | (_ :> (st, _)) <- path = st
-          | otherwise              = initial
-      guard $ finalState `Set.member` stAccept
-      return res
-
     go :: (state, Seq (state, Maybe output)) -> Seq input-> [(state, Seq (state, Maybe output))]
+    -- ^ Uses `step` on last state of run and nondeterministically chooses between alternatives given
+\end{code}
+
+Um alle möglichen Läufe auf einer gegebenen Eingabe zu berechnen wenden wir
+rekursiv \texttt{step} auf den letzten Zustand des Laufs (und der verbleibenden
+Eingabe) an bis keine Eingabe verbleibt und der letzte Zustand in der Menge der
+akzeptierenden Endzustände liegt.
+
+\begin{comment}
+\begin{code}
     go (initial, path) cs = do
       let
+        -- | Determine last state of the run
         current
           | (_ :> (st, _)) <- path = st
           | otherwise              = initial
-      (head, next, out) <- step fst (Just current) (Seq.lookup 0 cs)
-      let
-        nPath = path :> (next, out)
-        ncs = maybe id (:<) head cs
-      go (initial, nPath) ncs
-      
+      case step fst (Just current) (Seq.lookup 0 cs) of
+        [] -> do
+          guard $ current `Set.member` stAccept && Seq.null cs
+          return (initial, path)
+        xs -> do
+          (head, next, out) <- xs
+          let
+            nPath = path :> (next, out)
+            ncs
+              | (_ :< cs') <- cs = maybe id (:<) head cs'
+              | otherwise = Seq.Empty
+          go (initial, nPath) ncs
+\end{code}
+\end{comment}
+
+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]
+-- ^ Compute all possible runs on the given input and return only their output
+\end{code}
+\begin{comment}
+\begin{code}
+runFST = fmap (map $ catMaybes . fmap (view _2) . view _2) . runFST'
+  where
+    catMaybes = fmap fromJust . Seq.filter isJust
+\end{code}
+\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 mit jeder anderen Eingabe (inkl. einem weiteren $\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:
+
+  \begin{align*}
+    \Sigma^\times & = \Sigma \cap \Sigma^\prime \\
+    \Delta^\times & = \Delta \cap \Delta^\prime \\
+    Q^\times & = Q \times Q^\prime \\
+    I^\times & = I \times I^\prime \\
+    F^\times & = F \times F^\prime \\
+    E^\times & \subset Q^\times \times (\Sigma^\times \cup \{ \epsilon \}) \times (\Delta^\times \cup \{ \epsilon \}) \times Q^\times \\
+             & = \left \{ ((q, q^\prime), \sigma, \delta, (\bar{q}, \bar{q^\prime})) \colon (q, \sigma, \delta, \bar{q}) \in E, (q^\prime, \sigma^\prime, \delta^\prime, \bar{q^\prime}) \in E^\prime, \sigma = \sigma^\prime, \delta = \delta^\prime \right \}
+  \end{align*}
+\end{defn}
 
-step :: forall input output state. (Ord input, Ord output, Ord state)
-     => FST state input output
-     -> Maybe state -- ^ Current state
-     -> Maybe input -- ^ Head of remaining input
-     -> [(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
-step FST{..} (Just c) inS = let
-  consuming = fromMaybe Set.empty $ Map.lookup (c, inS) stTransition
-  unconsuming = fromMaybe Set.empty $ Map.lookup (c, Nothing) stTransition
-  in Set.toList $ Set.map (\(n, mOut) -> (Nothing, n, mOut)) consuming `Set.union` Set.map (\(n, mOut) -> (inS, n, mOut)) unconsuming
   
+\begin{code}
+productFST :: forall state1 state2 input output. (Ord state1, Ord state2, Ord input, Ord output) => FST state1 input output -> FST state2 input output -> FST (state1, state2) input output
+-- ^ Cartesian product on states, logical conjunction on transitions and state-properties (initial and accept)
+--
+-- This is the "natural" (that is component-wise) product when considering FSTs to be weighted in the boolean semiring.
+--
+-- Intuitively this corresponds to running both FSTs at the same time requiring them to produce the same output and agree on their input.
+\end{code}
 
-wordFST :: forall input output. Seq output -> FST Natural input output
--- ^ @wordFST str@ is the linear FST generating @str@ as output when given no input
-wordFST outs = FST
+\begin{comment}
+\begin{code}
+productFST fst1 fst2 = FST
+  { stInitial    = Set.fromDistinctAscList $ stInitial fst1 `setProductList` stInitial fst2
+  , stAccept     = Set.fromDistinctAscList $ stAccept fst1 `setProductList` stAccept fst2
+  , stTransition = Map.fromSet transitions . Set.fromDistinctAscList . mapMaybe filterTransition $ Map.keysSet (stTransition fst1) `setProductList` Map.keysSet (stTransition fst2)
+  }
+  where
+    setProductList :: forall a b. Set a -> Set b -> [(a, b)]
+    setProductList as bs = (,) <$> Set.toAscList as <*> Set.toAscList bs
+    filterTransition :: forall label. Eq label => ((state1, Maybe label), (state2, Maybe label)) -> Maybe ((state1, state2), Maybe label)
+    filterTransition ((st1, l1), (st2, l2))
+      | l1 == l2  = Just ((st1, st2), l1)
+      | otherwise = Nothing
+    transitions :: ((state1, state2), Maybe input) -> Set ((state1, state2), Maybe output)
+    transitions ((st1, st2), inS) = Set.fromDistinctAscList . mapMaybe filterTransition $ out1 `setProductList` out2
+      where
+        out1 = fromMaybe Set.empty (stTransition fst1 !? (st1, inS)) `Set.union` fromMaybe Set.empty (stTransition fst1 !? (st1, Nothing))
+        out2 = fromMaybe Set.empty (stTransition fst2 !? (st2, inS)) `Set.union` fromMaybe Set.empty (stTransition fst2 !? (st2, Nothing))
+\end{code}
+\end{comment}
+
+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 gegebene 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.
+
+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{(i, \epsilon)}{\rightarrow} n$, für jedes Eingabesymbol $i$ (um die Unabhängigkeit von der Eingabe sicherzustellen).
+Weiter ist $0$ initial und $\text{length}(\text{Ausgabe})$ der einzige akzeptierende Endzustand.
+
+\begin{code}
+wordFST :: forall input output. (Ord input, Ord output) => Set input -> Seq output -> FST Natural input output
+-- ^ @wordFST inps str@ is the linear FST generating @str@ as output when given any input with symbols in @inps@
+\end{code}
+  
+\begin{comment}
+\begin{code}
+wordFST inps outs = FST
   { stInitial    = Set.singleton 0
   , stAccept     = Set.singleton l
   , stTransition = Map.fromSet next states
@@ -119,36 +240,50 @@ wordFST outs = FST
     l :: Natural
     l = fromIntegral $ Seq.length outs
     states :: Set (Natural, Maybe input)
-    states = Set.fromDistinctAscList [ (n, Nothing) | n <- [0..pred l] ]
+    states
+      | Seq.null outs = Set.empty
+      | otherwise = Set.fromDistinctAscList [ (n, inp) | n <- [0..pred l], inp <- Nothing : map Just (Set.toList inps) ]
     next :: (Natural, Maybe input) -> Set (Natural, Maybe output)
-    next (i, _) = Set.singleton (succ i, Just . Seq.index outs $ fromIntegral i)
+    next (i, _) = Set.fromList
+      [ (succ i, Just . Seq.index outs $ fromIntegral i)
+      , (i, Nothing)
+      ]
+\end{code}
+\end{comment}
 
-productFST :: forall state1 state2 input output. (Ord state1, Ord state2, Ord input, Ord output) => FST state1 input output -> FST state2 input output -> FST (state1, state2) input output
--- ^ Cartesian product on states, logical conjunction on transitions and state-properties (initial and accept)
---
--- This is the "natural" (that is component-wise) product when considering FSTs to be weighted in the boolean semiring.
---
--- Intuitively this corresponds to running both FSTs at the same time requiring them to produce the same output and "agree" (epsilon agreeing with every character) on their input.
-productFST fst1 fst2 = FST
-  { stInitial    = stInitial fst1 `setProduct` stInitial fst2
-  , stAccept     = stAccept fst1 `setProduct` stAccept fst2
-  , stTransition = Map.fromSet transitions . Set.fromList . mapMaybe filterTransition . Set.toAscList $ Map.keysSet (stTransition fst1) `setProduct` Map.keysSet (stTransition fst2)
+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
+-- ^ @restrictOutput out@ is equivalent to @productFST (wordFST inps out)@ where @inps@ is a comprehensive set of all input symbols @inp :: input@
+\end{code}
+
+\begin{comment}
+\begin{code}
+restrictOutput out FST{..} = FST
+  { stInitial    = Set.mapMonotonic (0,) stInitial
+  , stAccept     = Set.mapMonotonic (l,) stAccept
+  , stTransition = Map.filter (not . Set.null) $ Map.fromList (concatMap noProgress $ Map.toList stTransition) `Map.union` Map.fromSet transitions (Set.fromDistinctAscList [((wSt, inSt), inSym) | wSt <- Set.toAscList wordStates, (inSt, inSym) <- Set.toAscList $ Map.keysSet stTransition])
   }
   where
-    setProduct :: forall a b. Set a -> Set b -> Set (a, b)
-    setProduct as bs = Set.fromDistinctAscList $ (,) <$> Set.toAscList as <*> Set.toAscList bs
-    filterTransition :: forall label. Eq label => ((state1, Maybe label), (state2, Maybe label)) -> Maybe ((state1, state2), Maybe label)
-    filterTransition ((st1, Nothing ), (st2, in2     )) = Just ((st1, st2), in2)
-    filterTransition ((st1, in1     ), (st2, Nothing )) = Just ((st1, st2), in1)
-    filterTransition ((st1, Just in1), (st2, Just in2))
-      | in1 == in2 = Just ((st1, st2), Just in1)
-      | otherwise  = Nothing
-    transitions :: ((state1, state2), Maybe input) -> Set ((state1, state2), Maybe output)
-    transitions ((st1, st2), inS) = Set.fromList . mapMaybe filterTransition . Set.toAscList $ out1 `setProduct` out2
+    l :: Natural
+    l = fromIntegral $ Seq.length out
+    wordStates :: Set Natural
+    wordStates
+      | Seq.null out = Set.empty
+      | otherwise = Set.fromDistinctAscList [0..pred l]
+    noProgress :: ((state, Maybe input), Set (state, Maybe output)) -> [(((Natural, state), Maybe input), Set ((Natural, state), Maybe output))]
+    noProgress ((inSt, inSym), outs)
+      = [ (((wState, inSt), inSym), Set.mapMonotonic (\(outSt, Nothing) -> ((wState, outSt), Nothing)) noOutput) | wState <- Set.toList wordStates, not $ Set.null noOutput ]
       where
-        out1 = (fromMaybe Set.empty $ stTransition fst1 !? (st1, inS)) `Set.union` (fromMaybe Set.empty $ stTransition fst1 !? (st1, Nothing))
-        out2 = (fromMaybe Set.empty $ stTransition fst2 !? (st2, inS)) `Set.union` (fromMaybe Set.empty $ stTransition fst2 !? (st2, Nothing))
+        noOutput = Set.filter (\(_, outSym) -> isNothing outSym) outs
+    transitions :: ((Natural, state), Maybe input) -> Set ((Natural, state), Maybe output)
+    transitions ((l, inSt), inSym) = Set.fromDistinctAscList [ ((succ l, outSt), outSym) | (outSt, outSym@(Just _)) <- Set.toAscList $ stTransition ! (inSt, inSym), outSym == Seq.lookup (fromIntegral l) out ]
+\end{code}
+\end{comment}
 
+\begin{comment}
+\begin{code}
 restrictFST :: forall state input output. (Ord state, Ord input, Ord output) => Set state -> FST state input output -> FST state input output
 -- ^ @restrictFST states fst@ removes from @fst@ all states not in @states@ including transitions leading to or originating from them
 restrictFST sts FST{..} = FST
@@ -170,7 +305,7 @@ liveFST :: forall state input output. (Ord state, Ord input, Ord output, Show st
 liveFST fst@FST{..} = flip execState Set.empty $ mapM_ (depthSearch Set.empty) stInitial
   where
     stTransition' :: Map state (Set state)
-    stTransition' = Map.map (Set.map $ \(st, _) -> st) $ Map.mapKeysWith Set.union (\(st, _) -> st) stTransition
+    stTransition' = Map.map (Set.map (\(st, _) -> st)) $ Map.mapKeysWith Set.union (\(st, _) -> st) stTransition
     depthSearch :: Set state -> state -> State (Set state) ()
     depthSearch acc curr = do
       let acc' = Set.insert curr acc
@@ -181,3 +316,4 @@ liveFST fst@FST{..} = flip execState Set.empty $ mapM_ (depthSearch Set.empty) s
       alreadyLive <- get
       mapM_ (depthSearch acc') $ next `Set.difference` alreadyLive
 \end{code}
+\end{comment}
diff --git a/edit-lens/src/Control/Lens/Edit.lhs b/edit-lens/src/Control/Lens/Edit.lhs
index 5a60536..5a106c8 100644
--- a/edit-lens/src/Control/Lens/Edit.lhs
+++ b/edit-lens/src/Control/Lens/Edit.lhs
@@ -1,3 +1,4 @@
+\begin{comment}
 \begin{code}
 module Control.Lens.Edit
   ( Module(..)
@@ -8,9 +9,10 @@ module Control.Lens.Edit
 
 import Control.Edit
 \end{code}
+\end{comment}
 
 \begin{defn}[Zustandsbehaftete Monoidhomomorphismen]
-Mit einer Menge von Komplementen $C$ und Monoiden $M$ und $N$ nennen wir eine partielle Funktion $\psi \colon C \times M \to C \times N$ einen zustandsbehafteten Monoidhomomorphismus wenn sie den folgenden Ansprüchen genügt:
+Gegeben eine Menge von Komplementen $C$ und Monoiden $M$ und $N$ nennen wir eine partielle Funktion $\psi \colon C \times M \to C \times N$ einen 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)$
@@ -26,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 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 \time \partial N \to C \times \partial M$, mit kompatiblem Komplement $C$, einem ausgezeichneten Element $\ground_C$ und einer \emph{Konsistenzrelation} $K \subset \Dom M \times C \times \Dom N$ sodass gilt:
+Für Moduln $M$ und $N$ besteht eine 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$ 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$
@@ -41,7 +43,7 @@ Für Moduln $M$ und $N$ besteht eine symmetrische edit-lens zwischen $M$ und $N$
 
 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 nichtt 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
@@ -74,7 +76,7 @@ Für Typen $n$ und $m$ ist eine \emph{lens} $\ell$ von $n$ in $m$ eine Abbildung
 
 $$ \forall f \, \text{Funktor} \colon \left ( \ell \colon \left ( m \to f(m) \right ) \to \left ( n \to f(n) \right ) \right )$$
 
-Durch geschickte Wahl des Funktors\footnote{\texttt{Const} bzw. \texttt{Identity}} $f$ können dann $\searrow \colon m \to n$ und $\nearrow \colon (m \to m) \to (n \to n)$ rekonstruiert werden oder verwandte Strukturen (folds, traversals, …) konstruiert werden.
+Durch geschickte Wahl des Funktors\footnote{\texttt{Const} bzw. \texttt{Identity}} $f$ können dann $\searrow \colon m \to n$ und $\nearrow \colon (m \to m) \to (n \to n)$ oder verwandte Strukturen (folds, traversals, …) konstruiert werden.
 \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.