summaryrefslogtreecommitdiff
path: root/edit-lens
diff options
context:
space:
mode:
Diffstat (limited to 'edit-lens')
-rw-r--r--edit-lens/src/Control/DFST.lhs2
-rw-r--r--edit-lens/src/Control/DFST/Lens.lhs17
-rw-r--r--edit-lens/src/Control/Edit.lhs6
-rw-r--r--edit-lens/src/Control/FST.lhs16
-rw-r--r--edit-lens/src/Control/FST/Lens.tex2
-rw-r--r--edit-lens/src/Control/Lens/Edit.lhs10
-rw-r--r--edit-lens/src/Control/Lens/Edit/ActionTree.lhs6
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
163Fü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. 163Fü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
165Da 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. 165Da 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.
166Die 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. 166Die 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
171Wir 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). 171Wir 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
173Wir 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. 173Wir 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
175Wir 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. 175Wir 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.
176Hierbei 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. 176Hierbei 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
178Die 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. 178Die 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
9Um 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}: 9Um 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]
12Ein 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: 12Ein \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
23Wir 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. 23Wir 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
25In 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)}. 25In 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)}.
26Eine Repräsentierung als Typklasse bietet sich an: 26Eine 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]
50Unter 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. 50Unter 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
52Semantisch 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. 52Semantisch 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]
135Wir definieren die Auswertung von finite state transducers induktiv indem wir zunächst angeben wie ein einzelner Auswertungs-Schritt erfolgt. 135Wir definieren die \emph{Auswertung} von finite state transducers induktiv indem wir zunächst angeben wie ein einzelner Auswertungs-Schritt erfolgt.
136 136
137Hierzu kommentieren wir die Haskell-Implementierung eines Auswertungs-Schritts. 137Hierzu kommentieren wir die Haskell-Implementierung eines Auswertungs-Schritts.
138Notwendigerweise ist die Auswertung eines FSTs nicht deterministisch, wir produzieren daher eine Liste von möglichen Resultaten in keiner besonderen Reihenfolge. 138Notwendigerweise 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
271Es ist später erforderlich einen FST derart einzuschränken, dass er eine gegebene Ausgabe produziert. 271Es ist später erforderlich einen FST derart einzuschränken, dass er eine gegebene Ausgabe produziert.
272 272
273Hierzu nehmen wir das FST-Produkt mit einem FST, der, ungeachtet der Eingabe, immer die gegebene Ausgabe produziert. 273Hierzu nehmen wir das FST-Produkt mit einem FST, der, ungeachtet der Eingabe, immer die gewünschte Ausgabe produziert.
274Da 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. 274Da 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
276Zur Konstruktion eines derartigen \emph{Wort-FST}s nehmen wir Indizes im Ausgabe-Wort (natürliche Zahlen) als Zustände. 276Zur 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
15Um 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. 15Um 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.
16Quellen von Serien unendlich vieler output-Strings sind notwendigerweise Zykel im betrachteten FST. 16Quellen von Serien unendlich vieler output-Strings sind notwendigerweise Zykel im betrachteten FST.
17Wir könnten nun für jeden Zykel im betrachteten FST eine Kante arbiträr wählen und dem Folgen jener Kante Kosten zuweisen. 17Wir könnten nun für jeden Zykel im betrachteten FST eine Kante arbiträr wählen und dem Folgen jener Kante Kosten zuweisen.
18Wenn wir nun sicherstellen, dass output-Strings in Reihenfolge aufsteigender Kosten aufgezählt werden, lässt sich jeder endliche output-String in endlicher Zeit finden. 18Wenn 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
20Das 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). 20Das 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).
21Diese Asymmetrie ergibt sich ausschließlich aus der Wahl des Komplements. 21Diese 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]
15Gegeben 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: 15Gegeben 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]
31Fü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: 31Fü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
72Das einschlägige bestehende lens framework \cite{lens} konstruiert seine Linsen alá \citeauthor{laarhoven} wie folgt: 72Das 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]
75Fü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: 75Fü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
79Durch 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. 79Durch 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
82Es liegt nun nahe $\nearrow \colon (m \to m) \to (n \to n)$ mit $\Rrightarrow \colon \partial m \to \partial n$ zu identifizieren. 82Es 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
45Das beschrieben Verfahren wurde prinzipiell agnostisch in Bezug auf die konkret gewählte Parser-Konstruktion gewählt. 45Das beschrieben Verfahren wurde prinzipiell agnostisch in Bezug auf die konkret gewählte Parser-Konstruktion implementiert.
46 46
47Hierfür wurden die benötigten Operationen auf der DFST-Wirkung und das in $\Lleftarrow$ verwendete Suchschema abstrakt als Typklasse angegeben: 47Hierfü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}
50class Monoid action => Action action input output | action -> input, action -> output where 50class 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
89Das Verfahren kann nun auf andere Sorten von Parser angewendet werden, indem nur die oben aufgeführte \texttt{Action}-Typklasse implementiert wird: 85Das Verfahren kann nun auf andere Sorten von Parser angewendet werden, indem nur die oben aufgeführte \texttt{Action}-Typklasse implementiert wird:
90 86