From 46ae60eaca841b554ba20c6a2b7a15b43c12b4df Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Tue, 18 Dec 2018 13:51:16 +0100 Subject: Much ado about nothing --- edit-lens/src/Control/FST.lhs | 270 +++++++++++++++++++++++++++++++----------- 1 file changed, 203 insertions(+), 67 deletions(-) (limited to 'edit-lens/src/Control/FST.lhs') 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} -- cgit v1.2.3