Much ado about nothing

1 files changed, 203 insertions, 67 deletions

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}