Much ado about nothing

1 files changed, 42 insertions, 15 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}