Think about propL

1 files changed, 11 insertions, 2 deletions

diff --git a/edit-lens/src/Data/String/DFST/Lens.lhs b/edit-lens/src/Data/String/DFST/Lens.lhs
index 8fd748a..bf06f53 100644
--- a/edit-lens/src/Data/String/DFST/Lens.lhs
+++ b/edit-lens/src/Data/String/DFST/Lens.lhs
@@ -108,11 +108,20 @@ Da wir wissen welche Stelle im input-String von einem gegebenen edit betroffen i
 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.
 
-% TODO propL
+
+% 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.
   
 \begin{code}
 
-data DFSTAction state = DFSTAction { runDFSTAction :: state -> (state, String -> String)}
+data DFSTAction state = DFSTAction { runDFSTAction :: state -> (state, String -> String) }
 
 instance Monoid (DFSTAction state) where
   mempty = DFSTAction $ \x -> (x, id)