diff options
Diffstat (limited to 'edit-lens')
-rw-r--r-- | edit-lens/src/Control/DFST.lhs | 2 | ||||
-rw-r--r-- | edit-lens/src/Control/DFST/Lens.lhs | 17 | ||||
-rw-r--r-- | edit-lens/src/Control/Edit.lhs | 6 | ||||
-rw-r--r-- | edit-lens/src/Control/FST.lhs | 16 | ||||
-rw-r--r-- | edit-lens/src/Control/FST/Lens.tex | 2 | ||||
-rw-r--r-- | edit-lens/src/Control/Lens/Edit.lhs | 10 | ||||
-rw-r--r-- | edit-lens/src/Control/Lens/Edit/ActionTree.lhs | 6 |
7 files changed, 28 insertions, 31 deletions
diff --git a/edit-lens/src/Control/DFST.lhs b/edit-lens/src/Control/DFST.lhs index 271a13e..eb838ae 100644 --- a/edit-lens/src/Control/DFST.lhs +++ b/edit-lens/src/Control/DFST.lhs | |||
@@ -39,7 +39,7 @@ import Text.Dot | |||
39 | \end{comment} | 39 | \end{comment} |
40 | 40 | ||
41 | \begin{defn}[deterministic finite state transducer] | 41 | \begin{defn}[deterministic finite state transducer] |
42 | 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. | 42 | 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änden einelementig ist. |
43 | 43 | ||
44 | Zusätzlich ändern wir die Darstellung indem wir $\epsilon$-Transitionen kontrahieren. | 44 | Zusätzlich ändern wir die Darstellung indem wir $\epsilon$-Transitionen kontrahieren. |
45 | 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. | 45 | 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. |
diff --git a/edit-lens/src/Control/DFST/Lens.lhs b/edit-lens/src/Control/DFST/Lens.lhs index 8222db2..ec81113 100644 --- a/edit-lens/src/Control/DFST/Lens.lhs +++ b/edit-lens/src/Control/DFST/Lens.lhs | |||
@@ -138,12 +138,12 @@ Wir bedienen uns hierbei einer bestehenden Programmbibliothek \cite{composition- | |||
138 | Auf $s$ wechselt der DFST seinen Zustand, auf $p$ produziert er, abhängig vom aktuellen Zustand, genau ein Zeichen. | 138 | Auf $s$ wechselt der DFST seinen Zustand, auf $p$ produziert er, abhängig vom aktuellen Zustand, genau ein Zeichen. |
139 | 139 | ||
140 | Wir stellen die Wirkung des DFST auf den Eingabe-String $spp$ grafisch analog zur Baumstruktur von \texttt{Compositions} dar. | 140 | Wir stellen die Wirkung des DFST auf den Eingabe-String $spp$ grafisch analog zur Baumstruktur von \texttt{Compositions} dar. |
141 | Wir bedienen uns hier der Darstellung von Automaten-Wirkungen als \emph{Schaltboxen} aus \cite{hofmann2011automatentheorie}, angepasst für DFSTs indem wir die Ausgabe des Automaten an den Pfaden innerhalb der Schaltbox annotieren. | 141 | Wir bedienen uns hier der Darstellung von Automaten-Wirkungen als \emph{Schaltboxen} aus \cite{hofmann2011automatentheorie}, angepasst für DFSTs indem wir die Ausgabe des transducers an den Pfaden innerhalb der Schaltbox annotieren. |
142 | 142 | ||
143 | \begin{figure}[H] | 143 | \begin{figure}[H] |
144 | \centering | 144 | \centering |
145 | \pinclude{presentation/comptree.tex} | 145 | \pinclude{presentation/comptree.tex} |
146 | \caption{Die Wirkung der Eingabe $spp$ auf den Automaten aus Abbildung \ref{fig:switchdfst}} | 146 | \caption{Die Wirkung der Eingabe $spp$ auf den einfachen transducer aus Abbildung \ref{fig:switchdfst}} |
147 | \end{figure} | 147 | \end{figure} |
148 | \end{eg} | 148 | \end{eg} |
149 | 149 | ||
@@ -160,7 +160,7 @@ dfstaProduces = fmap fst . runDFSTAction' | |||
160 | \end{code} | 160 | \end{code} |
161 | \end{comment} | 161 | \end{comment} |
162 | 162 | ||
163 | Für $\Rrightarrow$ können wir die alte DFST-Wirkung zunächst anhand des Intervalls indem der input-String von allen gegebenen edits betroffen ist (\texttt{affected}) in einen unveränderten Prefix und einen womöglich betroffenen Suffix unterteilen. | 163 | Für $\Rrightarrow$ können wir die alte DFST-Wirkung zunächst anhand des Intervalls in dem der input-String von allen gegebenen edits betroffen ist (\texttt{affected}) in einen unveränderten Prefix und einen womöglich betroffenen Suffix unterteilen. |
164 | 164 | ||
165 | 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. | 165 | 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. |
166 | 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. | 166 | 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. |
@@ -170,12 +170,12 @@ Für die asymmetrische edit-lens entgegen der DFST-Richtung $\Lleftarrow$ verwen | |||
170 | 170 | ||
171 | Wir unterteilen zunächst das Komplement an den Grenzen des betroffenen Intervalls im output-String in drei Teile (durch Akkumulation der Elemente des Komplements bis die gewünschte Länge erreicht ist). | 171 | Wir unterteilen zunächst das Komplement an den Grenzen des betroffenen Intervalls im output-String in drei Teile (durch Akkumulation der Elemente des Komplements bis die gewünschte Länge erreicht ist). |
172 | 172 | ||
173 | Wir transformieren dann den DFST in einen FST, dessen Ausgabe wir mit \texttt{restrictOutput} auf das gewünschte Fragment einschränken, setzen als initialen Zustand des FST den Zustand am linken Rand des von den edits betroffenen Intervalls und akzeptieren jene Zustände, von denen aus das Komplement-Fragment ab dem rechten Rand des betroffenen Intervalls zu einem im ursprünglichen DFST akzeptierten Zustand führt. | 173 | Wir transformieren dann den DFST in einen FST, dessen Ausgabe wir mit \texttt{restrictOutput} auf das gewünschte Fragment einschränken, setzen als initialen Zustand des FST den Zustand am linken Rand des von den edits betroffenen Intervalls und akzeptieren jene Zustände, von denen aus das Komplement-Fragment ab dem rechten Rand des betroffenen Intervalls zu einem im ursprünglichen DFST akzeptierenden Zustand führt. |
174 | 174 | ||
175 | Wir verwenden dann gewöhnliche Breitensuche über die Zustände und Transitionen des soeben konstruierten FSTs um einen Lauf-Fragment zu bestimmen, dass wir in das betroffene Intervall einsetzen können. | 175 | Wir verwenden dann gewöhnliche Breitensuche über die Zustände und Transitionen des soeben konstruierten FSTs um einen Lauffragment zu bestimmen, dass wir in das betroffene Intervall einsetzen können. |
176 | Hierbei sind sämtliche Randbedingungen (korrekte Ausgabe, Übereinstimmung an den Intervallgrenzen) bereits in den FST kodiert sodass wir nur noch prüfen müssen, dass der gefunde Lauf in einem akzeptierten Zustand endet. | 176 | Hierbei sind sämtliche Randbedingungen (korrekte Ausgabe, Übereinstimmung an den Intervallgrenzen) bereits in den FST kodiert sodass wir nur noch prüfen müssen, dass der gefunde Lauf in einem akzeptierenden Zustand endet. |
177 | 177 | ||
178 | Die input-edits können nun wiederum, unter Beachtung der Verschiebung der indices um die Länge der Eingabe vor der linken Intervallgrenze, mit dem Unix Standard-Diff-Algorithmus berechnet werden. | 178 | Die input-edits können nun wiederum, unter Beachtung der Verschiebung der Indices um die Länge der Eingabe vor der linken Intervallgrenze, mit dem Unix Standard-Diff-Algorithmus berechnet werden. |
179 | 179 | ||
180 | \begin{comment} | 180 | \begin{comment} |
181 | \begin{code} | 181 | \begin{code} |
@@ -299,7 +299,8 @@ bfs outgoing predicate | |||
299 | n & \mapsto ( \text{\tt \textbackslash n}, 0 ) \\ | 299 | n & \mapsto ( \text{\tt \textbackslash n}, 0 ) \\ |
300 | & \\ | 300 | & \\ |
301 | \text{act}_\text{L} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\ | 301 | \text{act}_\text{L} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\ |
302 | n & \mapsto (0\, 1\, \ldots\, 80, 80) \\ | ||
303 | \text{other} & \mapsto (\epsilon, \bot) | 302 | \text{other} & \mapsto (\epsilon, \bot) |
304 | \end{align*} | 303 | \end{align*} |
304 | |||
305 | % TODO | ||
305 | \end{eg} | 306 | \end{eg} |
diff --git a/edit-lens/src/Control/Edit.lhs b/edit-lens/src/Control/Edit.lhs index ba4b8e6..80c143a 100644 --- a/edit-lens/src/Control/Edit.lhs +++ b/edit-lens/src/Control/Edit.lhs | |||
@@ -6,10 +6,10 @@ module Control.Edit | |||
6 | \end{code} | 6 | \end{code} |
7 | \end{comment} | 7 | \end{comment} |
8 | 8 | ||
9 | Um das Intuitive Verhalten von Änderungen auf Texten\footnote{Im folgenden \emph{edits}} und ihre interne algebraische Struktur zu fassen formalisieren wir sie als \emph{Moduln}: | 9 | Um das intuitive Verhalten von Änderungen auf Texten\footnote{Im folgenden \emph{edits}} und ihre interne algebraische Struktur zu fassen formalisieren wir sie als \emph{Moduln}: |
10 | 10 | ||
11 | \begin{defn}[Moduln] | 11 | \begin{defn}[Moduln] |
12 | Ein Modul $M$ ist eine \emph{partielle Monoidwirkung} zusammen mit einem schwach-initialen Element\footnote{Gemeint ist hier die übliche Definition von \emph{schwach-initial} aus der Kategorientheorie—ein Modul $M$ bildet eine Kategorie mit Objekten aus $\Dom M$ und Morphismen von $x$ nach $y$ den Monoidelementen $\partial x \in \partial M$ sodass $x \cdot \partial x = y$} (bzgl. der Monoidwirkung) auf dem Träger, d.h. $M = (\Dom M, \partial M, \init_M)$ ist ein Tupel aus einer Trägermenge $\Dom M$, einem Monoid $\partial M$ zusammen mit mit einer partiellen Funktion $\cdot \colon \Dom M \times \partial M \to \Dom$, die \emph{kompatibel} ist mit der Monoid-Struktur: | 12 | Ein \emph{Modul} $M$ ist eine partielle Monoidwirkung zusammen mit einem schwach-initialen Element\footnote{Gemeint ist hier die übliche Definition von \emph{schwach-initial} aus der Kategorientheorie—ein Modul $M$ bildet eine Kategorie mit Objekten aus $\Dom M$ und Morphismen von $x$ nach $y$ den Monoidelementen $\partial x \in \partial M$ sodass $x \cdot \partial x = y$} (bzgl. der Monoidwirkung) auf dem Träger, d.h. $M = (\Dom M, \partial M, \init_M)$ ist ein Tupel aus einer Trägermenge $\Dom M$, einem Monoid $\partial M$ zusammen mit mit einer partiellen Funktion $\cdot \colon \Dom M \times \partial M \to \Dom$, die \emph{kompatibel} ist mit der Monoid-Struktur: |
13 | 13 | ||
14 | \begin{itemize} | 14 | \begin{itemize} |
15 | \item $\forall m \in \Dom M \colon m \cdot 1_{\partial M} = m$ | 15 | \item $\forall m \in \Dom M \colon m \cdot 1_{\partial M} = m$ |
@@ -22,7 +22,7 @@ $$\forall m \in \Dom M \ \exists \partial m \in \partial M \colon m = \init_M \c | |||
22 | 22 | ||
23 | 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. | 23 | 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 | 24 | ||
25 | In Haskell charakterisieren wir Moduln über ihren Monoid, d.h. die Wahl des Monoiden \texttt{m} legt den Träger \texttt{Domain m}, die Wirkung \texttt{apply}, das initiale Element \texttt{init} und $(\init_M \cdot)^{-1}$ eindeutig fest\footnote{Betrachten wir mehrere Moduln über dem selben Träger (oder mit verschiedenen Wirkungen) führen wir neue, isomorphe, Typen ein (\texttt{newtype}-Wrappern)}. | 25 | In Haskell charakterisieren wir Moduln über ihren Monoid, d.h. die Wahl des Monoiden \texttt{m} legt den Träger \texttt{Domain m}, die Wirkung \texttt{apply}, das initiale Element \texttt{init} und $(\init_M \cdot)^{-1}$ eindeutig fest\footnote{Betrachten wir mehrere Moduln über dem selben Träger (oder mit verschiedenen Wirkungen) führen wir neue, isomorphe Typen ein (\texttt{newtype}-Wrapper)}. |
26 | Eine Repräsentierung als Typklasse bietet sich an: | 26 | Eine Repräsentierung als Typklasse bietet sich an: |
27 | 27 | ||
28 | \begin{code} | 28 | \begin{code} |
diff --git a/edit-lens/src/Control/FST.lhs b/edit-lens/src/Control/FST.lhs index 9739adc..9cc7524 100644 --- a/edit-lens/src/Control/FST.lhs +++ b/edit-lens/src/Control/FST.lhs | |||
@@ -46,8 +46,8 @@ import Text.Dot | |||
46 | \end{code} | 46 | \end{code} |
47 | \end{comment} | 47 | \end{comment} |
48 | 48 | ||
49 | \begin{defn}[Finite state transducers] | 49 | \begin{defn}[Finite State Transducers] |
50 | 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. | 50 | Unter einem \emph{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. |
51 | 51 | ||
52 | 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. | 52 | 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. |
53 | 53 | ||
@@ -64,7 +64,7 @@ data FST state input output = FST | |||
64 | \end{defn} | 64 | \end{defn} |
65 | 65 | ||
66 | \begin{eg} \label{eg:linebreak} | 66 | \begin{eg} \label{eg:linebreak} |
67 | Als wiederkehrendes Beispiel betrachten wir einen Transducer $L_{80} = (\Sigma, \Delta, Q, I, F, E)$, der für ein beliebiges Alphabet $\Sigma \supseteq \{ \text{\tt ' '}, \text{\tt \textbackslash n} \}$ durch Umwandlung zwischen Leerzeichen und Zeilenumbrüchen sicherstellt, dass jede Zeile des Ausgabetextes mindestens 80 Zeichen enthält, jedoch nur an Wortgrenzen umbricht: | 67 | Als wiederkehrendes Beispiel betrachten wir einen Transducer $L_{80} = (\Sigma, \Delta, Q, I, F, E)$, der für ein beliebiges Alphabet $\Sigma \supseteq \{ \text{\tt ' '}, \text{\tt \textbackslash n} \}$ durch Umwandlung zwischen Leerzeichen und Zeilenumbrüchen sicherstellt, dass jede Zeile des Ausgabetextes möglichst wenige aber mindestens 80 Zeichen enthält, und nur an Wortgrenzen umbricht: |
68 | 68 | ||
69 | \begin{align*} | 69 | \begin{align*} |
70 | \Delta & = \Sigma \\ | 70 | \Delta & = \Sigma \\ |
@@ -132,7 +132,7 @@ instance (Show state, Show input, Show output, Ord state, Ord input, Ord output) | |||
132 | \end{comment} | 132 | \end{comment} |
133 | 133 | ||
134 | \begin{defn}[Auswertung von FSTs] | 134 | \begin{defn}[Auswertung von FSTs] |
135 | Wir definieren die Auswertung von finite state transducers induktiv indem wir zunächst angeben wie ein einzelner Auswertungs-Schritt erfolgt. | 135 | Wir definieren die \emph{Auswertung} von finite state transducers induktiv indem wir zunächst angeben wie ein einzelner Auswertungs-Schritt erfolgt. |
136 | 136 | ||
137 | Hierzu kommentieren wir die Haskell-Implementierung eines Auswertungs-Schritts. | 137 | Hierzu kommentieren wir die Haskell-Implementierung eines Auswertungs-Schritts. |
138 | Notwendigerweise ist die Auswertung eines FSTs nicht deterministisch, wir produzieren daher eine Liste von möglichen Resultaten in keiner besonderen Reihenfolge. | 138 | Notwendigerweise ist die Auswertung eines FSTs nicht deterministisch, wir produzieren daher eine Liste von möglichen Resultaten in keiner besonderen Reihenfolge. |
@@ -223,7 +223,7 @@ Hierfür berechnen wir das Graphen-Produkt der FSTs: | |||
223 | \begin{defn}[FST-Produkt] | 223 | \begin{defn}[FST-Produkt] |
224 | 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$. | 224 | 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$. |
225 | 225 | ||
226 | $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: | 226 | $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: |
227 | 227 | ||
228 | \begin{align*} | 228 | \begin{align*} |
229 | \Sigma^\times & = \Sigma \cap \Sigma^\prime \\ | 229 | \Sigma^\times & = \Sigma \cap \Sigma^\prime \\ |
@@ -270,7 +270,7 @@ productFST fst1 fst2 = FST | |||
270 | 270 | ||
271 | Es ist später erforderlich einen FST derart einzuschränken, dass er eine gegebene Ausgabe produziert. | 271 | Es ist später erforderlich einen FST derart einzuschränken, dass er eine gegebene Ausgabe produziert. |
272 | 272 | ||
273 | Hierzu nehmen wir das FST-Produkt mit einem FST, der, ungeachtet der Eingabe, immer die gegebene Ausgabe produziert. | 273 | Hierzu nehmen wir das FST-Produkt mit einem FST, der, ungeachtet der Eingabe, immer die gewünschte Ausgabe produziert. |
274 | 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. | 274 | 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. |
275 | 275 | ||
276 | Zur Konstruktion eines derartigen \emph{Wort-FST}s nehmen wir Indizes im Ausgabe-Wort (natürliche Zahlen) als Zustände. | 276 | Zur Konstruktion eines derartigen \emph{Wort-FST}s nehmen wir Indizes im Ausgabe-Wort (natürliche Zahlen) als Zustände. |
@@ -374,12 +374,12 @@ restrictOutput :: forall state input output. (Ord state, Ord input, Ord output) | |||
374 | (rest2) edge node {$(98, 98)$} (99); | 374 | (rest2) edge node {$(98, 98)$} (99); |
375 | \end{tikzpicture} | 375 | \end{tikzpicture} |
376 | 376 | ||
377 | \caption{\label{fig:l80timesw100} Die Einschränkung des Automaten aus Abbildung \ref{fig:linebreak} auf das Wort aus Abbildung \ref{fig:w100}} | 377 | \caption{\label{fig:l80timesw100} Die Einschränkung des Automaten aus Abbildung \ref{fig:linebreak} (Zeilenumbrüche $\leftrightarrow$ Leerzeichen) auf das Wort aus Abbildung \ref{fig:w100} ($1 \ldots 80 \text{\texttt{\textbackslash n}} 81 \ldots 98$)} |
378 | \end{figure} | 378 | \end{figure} |
379 | \end{eg} | 379 | \end{eg} |
380 | 380 | ||
381 | \begin{rem} | 381 | \begin{rem} |
382 | Es ist bemerkenswert, dass in Beispiel \ref{eg:l80timesw100} die Zirkuläre Struktur von $L_{80}$ durch Produkt mit einem Wort verloren geht. | 382 | Es ist bemerkenswert, dass in Beispiel \ref{eg:l80timesw100} die zirkuläre Struktur von $L_{80}$ durch das Produkt mit einem Wort verloren geht. |
383 | 383 | ||
384 | I.\@A.\@ ist das Produkt eines beliebigen FST mit einem Wort-FST zwar nicht azyklisch, erbt jedoch die lineare Struktur des Wort-FST in dem Sinne, dass Fortschritt in Richtung der akzeptierenden Zustände nur möglich ist indem der $(i, \sigma, w_i, i + 1)$-Klasse von Transitionen des Wort-FSTs gefolgt wird. | 384 | I.\@A.\@ ist das Produkt eines beliebigen FST mit einem Wort-FST zwar nicht azyklisch, erbt jedoch die lineare Struktur des Wort-FST in dem Sinne, dass Fortschritt in Richtung der akzeptierenden Zustände nur möglich ist indem der $(i, \sigma, w_i, i + 1)$-Klasse von Transitionen des Wort-FSTs gefolgt wird. |
385 | \end{rem} | 385 | \end{rem} |
diff --git a/edit-lens/src/Control/FST/Lens.tex b/edit-lens/src/Control/FST/Lens.tex index dc44e10..31af317 100644 --- a/edit-lens/src/Control/FST/Lens.tex +++ b/edit-lens/src/Control/FST/Lens.tex | |||
@@ -15,7 +15,7 @@ $\Lleftarrow$ basiert fundamental darauf im Komplement anhand der erzeugten outp | |||
15 | Um sicher zu stellen, dass jene Suche immer terminiert, müsste die Aufzählung der i.A. unendlich vielen zulässigen output-Strings in \texttt{FSTAction} geschickt gewählt sein. | 15 | Um sicher zu stellen, dass jene Suche immer terminiert, müsste die Aufzählung der i.A. unendlich vielen zulässigen output-Strings in \texttt{FSTAction} geschickt gewählt sein. |
16 | Quellen von Serien unendlich vieler output-Strings sind notwendigerweise Zykel im betrachteten FST. | 16 | Quellen von Serien unendlich vieler output-Strings sind notwendigerweise Zykel im betrachteten FST. |
17 | Wir könnten nun für jeden Zykel im betrachteten FST eine Kante arbiträr wählen und dem Folgen jener Kante Kosten zuweisen. | 17 | Wir könnten nun für jeden Zykel im betrachteten FST eine Kante arbiträr wählen und dem Folgen jener Kante Kosten zuweisen. |
18 | Wenn wir nun sicherstellen, dass output-Strings in Reihenfolge aufsteigender Kosten aufgezählt werden, lässt sich jeder endliche output-String in endlicher Zeit finden. | 18 | Wenn wir nun sicherstellen, dass output-Strings in Reihenfolge aufsteigender Kosten aufgezählt werden, lässt sich zu jedem endlichen output-String eine Eingabe in endlicher Zeit finden. |
19 | 19 | ||
20 | Das obig beschriebene Verfahren weißt eine Asymmetrie auf, die im unterliegenden FST nicht vorhanden ist (sowohl Eingabe- als auch Ausgabe-Symbole sind Annotationen vom gleichen Typ an die Transitionen des FST). | 20 | Das obig beschriebene Verfahren weißt eine Asymmetrie auf, die im unterliegenden FST nicht vorhanden ist (sowohl Eingabe- als auch Ausgabe-Symbole sind Annotationen vom gleichen Typ an die Transitionen des FST). |
21 | Diese Asymmetrie ergibt sich ausschließlich aus der Wahl des Komplements. | 21 | Diese Asymmetrie ergibt sich ausschließlich aus der Wahl des Komplements. |
diff --git a/edit-lens/src/Control/Lens/Edit.lhs b/edit-lens/src/Control/Lens/Edit.lhs index 6561528..5cf8662 100644 --- a/edit-lens/src/Control/Lens/Edit.lhs +++ b/edit-lens/src/Control/Lens/Edit.lhs | |||
@@ -12,7 +12,7 @@ import Control.Edit | |||
12 | \end{comment} | 12 | \end{comment} |
13 | 13 | ||
14 | \begin{defn}[Zustandsbehaftete Monoidhomomorphismen] | 14 | \begin{defn}[Zustandsbehaftete Monoidhomomorphismen] |
15 | Gegeben eine Menge $C$ von \emph{Komplementen} und zwei 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: | 15 | Gegeben eine Menge $C$ von \emph{Komplementen} und zwei Monoiden $M$ und $N$ nennen wir eine partielle Funktion $\psi \colon C \times M \to C \times N$ einen \emph{zustandsbehafteten Monoidhomomorphismus} wenn sie den folgenden Ansprüchen genügt: |
16 | 16 | ||
17 | \begin{itemize} | 17 | \begin{itemize} |
18 | \item $\forall c \in C \colon \psi(1_M, c) = (1_N, c)$ | 18 | \item $\forall c \in C \colon \psi(1_M, c) = (1_N, c)$ |
@@ -28,7 +28,7 @@ type StateMonoidHom s m n = (s, m) -> (s, n) | |||
28 | \end{defn} | 28 | \end{defn} |
29 | 29 | ||
30 | \begin{defn}[edit-lenses] | 30 | \begin{defn}[edit-lenses] |
31 | 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 \in C$ und einer \emph{Konsistenzrelation} $K \subset \Dom M \times C \times \Dom N$ sodass gilt: | 31 | Für Moduln $M$ und $N$ besteht eine \emph{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 \in C$ und einer \emph{Konsistenzrelation} $K \subset \Dom M \times C \times \Dom N$ sodass gilt: |
32 | 32 | ||
33 | \begin{itemize} | 33 | \begin{itemize} |
34 | \item $(\init_M, \ground_C, \init_N) \in K$ | 34 | \item $(\init_M, \ground_C, \init_N) \in K$ |
@@ -69,14 +69,14 @@ instance (Module m, Module n) => HasEditLens (EditLens c m n) m n where | |||
69 | 69 | ||
70 | \subsection{Kompatibilität mit bestehenden lens frameworks} | 70 | \subsection{Kompatibilität mit bestehenden lens frameworks} |
71 | 71 | ||
72 | Das einschlägige bestehende lens framework \cite{lens} konstruiert seine Linsen alá \citeauthor{laarhoven} wie folgt: | 72 | Das einschlägige bestehende lens framework \cite{lens} konstruiert seine Linsen à la \citeauthor{laarhoven} wie folgt: |
73 | 73 | ||
74 | \begin{defn}[lenses alá laarhoven] | 74 | \begin{defn}[lenses à la Laarhoven] |
75 | Für Typen $n$ und $m$ ist eine \emph{lens} $\ell$ von $n$ in $m$ eine Abbildung\footnote{Gdw. die betrachtete Linse einen Isomorphismus kodiert wird auch über den verwendeten Profunktor anstatt $\to$ quantifiziert} folgender Struktur: | 75 | Für Typen $n$ und $m$ ist eine \emph{lens} $\ell$ von $n$ in $m$ eine Abbildung\footnote{Gdw. die betrachtete Linse einen Isomorphismus kodiert wird auch über den verwendeten Profunktor anstatt $\to$ quantifiziert} folgender Struktur: |
76 | 76 | ||
77 | $$ \forall f \, \text{Funktor} \colon \left ( \ell \colon \left ( m \to f(m) \right ) \to \left ( n \to f(n) \right ) \right )$$ | 77 | $$ \forall f \, \text{Funktor} \colon \left ( \ell \colon \left ( m \to f(m) \right ) \to \left ( n \to f(n) \right ) \right )$$ |
78 | 78 | ||
79 | 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. | 79 | Durch geschickte Wahl des Funktors\footnote{\texttt{Const m} bzw. \texttt{Identity}} $f$ können dann $\searrow \colon n \to m$ und $\nearrow \colon (m \to m) \to (n \to n)$ oder verwandte Strukturen (folds, traversals, …) konstruiert werden. |
80 | \end{defn} | 80 | \end{defn} |
81 | 81 | ||
82 | Es liegt nun nahe $\nearrow \colon (m \to m) \to (n \to n)$ mit $\Rrightarrow \colon \partial m \to \partial n$ zu identifizieren. | 82 | Es liegt nun nahe $\nearrow \colon (m \to m) \to (n \to n)$ mit $\Rrightarrow \colon \partial m \to \partial n$ zu identifizieren. |
diff --git a/edit-lens/src/Control/Lens/Edit/ActionTree.lhs b/edit-lens/src/Control/Lens/Edit/ActionTree.lhs index 6632dce..0cfaf24 100644 --- a/edit-lens/src/Control/Lens/Edit/ActionTree.lhs +++ b/edit-lens/src/Control/Lens/Edit/ActionTree.lhs | |||
@@ -42,15 +42,12 @@ import System.IO.Unsafe | |||
42 | \end{code} | 42 | \end{code} |
43 | \end{comment} | 43 | \end{comment} |
44 | 44 | ||
45 | Das beschrieben Verfahren wurde prinzipiell agnostisch in Bezug auf die konkret gewählte Parser-Konstruktion gewählt. | 45 | Das beschrieben Verfahren wurde prinzipiell agnostisch in Bezug auf die konkret gewählte Parser-Konstruktion implementiert. |
46 | 46 | ||
47 | Hierfür wurden die benötigten Operationen auf der DFST-Wirkung und das in $\Lleftarrow$ verwendete Suchschema abstrakt als Typklasse angegeben: | 47 | Hierfür wurden die benötigten Operationen auf der DFST-Wirkung und das in $\Lleftarrow$ verwendete Suchschema abstrakt als Typklasse angegeben: |
48 | 48 | ||
49 | \begin{code} | 49 | \begin{code} |
50 | class Monoid action => Action action input output | action -> input, action -> output where | 50 | class Monoid action => Action action input output | action -> input, action -> output where |
51 | \end{code} | ||
52 | \begin{comment} | ||
53 | \begin{code} | ||
54 | -- | Most operations of `Action` permit access to some underlying description of the parser (i.e. an automaton) | 51 | -- | Most operations of `Action` permit access to some underlying description of the parser (i.e. an automaton) |
55 | type ActionParam action = param | param -> action | 52 | type ActionParam action = param | param -> action |
56 | 53 | ||
@@ -84,7 +81,6 @@ class Monoid action => Action action input output | action -> input, action -> o | |||
84 | -> Compositions action -- ^ Suffix | 81 | -> Compositions action -- ^ Suffix |
85 | -> Maybe (Seq input) | 82 | -> Maybe (Seq input) |
86 | \end{code} | 83 | \end{code} |
87 | \end{comment} | ||
88 | 84 | ||
89 | Das Verfahren kann nun auf andere Sorten von Parser angewendet werden, indem nur die oben aufgeführte \texttt{Action}-Typklasse implementiert wird: | 85 | Das Verfahren kann nun auf andere Sorten von Parser angewendet werden, indem nur die oben aufgeführte \texttt{Action}-Typklasse implementiert wird: |
90 | 86 | ||