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/DFST.lhs | 57 +++-- edit-lens/src/Control/DFST/Lens.lhs | 412 +++++++++++++++++++++++------------- edit-lens/src/Control/Edit.lhs | 6 +- edit-lens/src/Control/FST.lhs | 270 +++++++++++++++++------ edit-lens/src/Control/Lens/Edit.lhs | 10 +- 5 files changed, 520 insertions(+), 235 deletions(-) (limited to 'edit-lens/src/Control') 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. -- cgit v1.2.3