From 9a02751c1e588a5bbb83bb7e543c26486d3079d5 Mon Sep 17 00:00:00 2001
From: Gregor Kleen <gkleen@yggdrasil.li>
Date: Tue, 4 Jun 2019 14:05:44 +0200
Subject: Finish example

---
 edit-lens/src/Control/DFST/Lens.lhs | 57 +++++++++++++++++++++++++++++++++----
 1 file changed, 51 insertions(+), 6 deletions(-)

diff --git a/edit-lens/src/Control/DFST/Lens.lhs b/edit-lens/src/Control/DFST/Lens.lhs
index ec81113..56f37a0 100644
--- a/edit-lens/src/Control/DFST/Lens.lhs
+++ b/edit-lens/src/Control/DFST/Lens.lhs
@@ -278,7 +278,7 @@ bfs outgoing predicate
     w^\prime = w = 0\, 1\, \ldots\, 80\, \text{\textbackslash n}\, 81\, \ldots\, 98
   \end{equation*}
 
-  Das von $e$ betroffene Intervall von $w^\prime$ ist $(80, 80)$.
+  Das von $e^\prime$ betroffene Intervall in $w^\prime$ ist $(80, 80)$.
 
   Das Komplement nach Anwendung des DFST auf $w$ ist, wie in Beispiel \ref{eg:linebreakonw100} dargelegt:
 
@@ -286,21 +286,66 @@ bfs outgoing predicate
     \text{act} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\
     0 & \mapsto (0\, 1\, \ldots\, 80\, \text{\tt \textbackslash n}\, 81\, \ldots\, 98, 19) \\
     1 & \mapsto (0\, 1\, \ldots\, 79\, \text{\tt \textbackslash n}\, 80\, \ldots\, 98, 18) \\
-  & \vdots
+      & \vdots
   \end{align*}
 
-  Wir unterteilen $\text{act}$ an $(80, 80)$ in $\text{act}_\text{R} \circ \text{act}_e \circ \text{act}_\text{L}$:
+  Wir unterteilen $\text{act}$ an $(80, 80)$ in $\text{act}_\text{R} \circ \text{act}_{e^\prime} \circ \text{act}_\text{L}$:
 
   \begin{align*}
     \text{act}_\text{R} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\
     n & \mapsto (81\, \ldots\, 98, \min ( 80, n + 19 ) ) \\
     & \\
-    \text{act}_e & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\
+    \text{act}_{e^\prime} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\
     n & \mapsto ( \text{\tt \textbackslash n}, 0 ) \\
     & \\
     \text{act}_\text{L} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\
-    \text{other} & \mapsto (\epsilon, \bot)
+    n & \mapsto (0\, 1\, \ldots\, 80, 80) \\
   \end{align*}
 
-  % TODO
+  Wir bestimmen die Zustände des vorherigen Laufs an den Grenzen des von $e^\prime$ betroffenen Intervalls:
+
+  \begin{align*}
+    Q_\text{L} &= 80 \\
+    Q_\text{R} &= 0 
+  \end{align*}
+
+  Wir wenden $e^\prime = \rho_{80}$ an auf $\restr{w^\prime}{\text{act}_{e^\prime}} \coloneqq \pi_1 \left ( \text{act}_{e^\prime}(Q_\text{L}) \right ) = \text{\tt \textbackslash n}$, das Teilwort erzeugt vom Komplement-Stück $\text{act}_{e^\prime}$:
+
+  \begin{equation*}
+    \restr{w^\prime}{\text{act}_{e^\prime}} \cdot \rho_{80} = \epsilon
+  \end{equation*}
+
+  Da der DFST aus Beispiel \ref{eg:linebreak} keine Transitionen mit mehr als einem Ausgabe-Zeichen enthält ist in diesem Fall keine explizite Umwandlung in einen FST notwendig.
+  Der Einfachheit wegen lassen wir sie aus.
+
+  Der Wort-FST für das leere Wort hat genau einen Zustand und keine Transitionen.
+  Es hat daher auch das Produkt mit dem DFST aus Beispiel \ref{eg:linebreak} keine Transitionen und nur Zustände der Form $(0, n)$ mit $n \in \{ 0, \ldots, 80 \}$.
+  Wie auch im ursprünglichen DFST sind alle Zustände akzeptierend.
+
+  Wir müssen nun bestimmen welche Zustände, unter $\text{act}_\text{R}$, zu einem akzeptierenden Zustand führen.
+  Da alle Zustände akzeptieren ist hier jeder Zustand geeignet.
+
+  Wir müssen nun (vermöge Breitensuche) den kürzesten Pfad im Produkt-FST zwischen $Q_\text{L}$ und einem der Zustände finden, der unter $\text{act}_\text{R}$ zu einem akzeptierenden Zustand im ursprünglichen transducer führt.
+  Der leere Pfad ist geeignet.
+
+  Die DFST-Wirkung (also das Komplement) des leeren Strings (die Eingabe des leeren Pfads) ist:
+  \begin{align*}
+    \text{act}_0 & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\
+    n & \mapsto ( \epsilon, n )
+  \end{align*}
+
+  Mithilfe des Unix Standard-Diff-Algorithmus bestimmen wir $e$ als den minimalen edit, sodass gilt:
+  \begin{equation*}
+    \text{\tt \textbackslash n} \cdot e = \epsilon
+  \end{equation*}
+  Man beachte das $\text{\tt \textbackslash n}$ und $\epsilon$ hierbei die \emph{Eingaben} von $\text{act}_{e^\prime}$ bzw. $\text{act}_0$ sind.
+  Nach Behandlung der Indices ergibt sich $e = \rho_{80}$.
+
+  Als neues Komplement erhalten wir:
+
+  \begin{align*}
+    \text{act}^\prime & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\
+    \text{act}^\prime & = \text{act}_R \circ \text{act}_0 \circ \text{act}_L \\
+    n & \mapsto (0\, 1\, \ldots\, 80\, 81\, \ldots\, 98, 80)
+  \end{align*}
 \end{eg}
-- 
cgit v1.2.3