From 4bfeb8e8c8365dbc59a45e3cda879c5ee1276ee0 Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Sat, 3 Feb 2018 20:47:53 +0100 Subject: Try to prove stuff about container transducers --- edit-lens/src/Control/Edit/Container/Transducer.lhs | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) (limited to 'edit-lens/src/Control/Edit') diff --git a/edit-lens/src/Control/Edit/Container/Transducer.lhs b/edit-lens/src/Control/Edit/Container/Transducer.lhs index 9db26db..492ec91 100644 --- a/edit-lens/src/Control/Edit/Container/Transducer.lhs +++ b/edit-lens/src/Control/Edit/Container/Transducer.lhs @@ -154,7 +154,21 @@ Beweisskizze: Betrachte nun $\text{Replace}(c)$ gefolgt von $\text{Replace}(\text{init})$ unter $\text{diffContTrans}$ auf $\text{init}$. Für das Ergebnis $e_o^{-1}$ muss gelten, dass $e_o^{-1} \circ e_o = \text{id}$. Wir haben also Inverse für beliebige Elemente des edit-monoiden auf dem Output; also eine Gruppe auf edits auf dem Output die kompatibel ist mit der bestehenden monoid struktur. - + +Beweis: + Nimm an edits auf dem output-container $N$ bilden einen Monoiden, jedoch keine Gruppe, d.h. es existiert $e_o$ sodass für alle $e_o^\prime$, edits auf dem output-container, gilt, dass $e_o \cdot e_o^prime \neq 1$. + Es sei $M$ der Container mit genau einer Shape und belegten Position und ${\text{init}, c}$ als Inhalt mit $\text{Replace}$ als Modul-Struktur. + Es sei $T$ der Container-Transducer mit zwei Zuständen $A$ und $B$ und folgender Transitions-Funktion: + \begin{align*} + (A, \init) & \mapsto (1_{\partial N}, A) + (A, c) & \mapsto ((\text{init}_N \cdot)^{-1}(e_o), B) + (B, \init) & \mapsto (1_{\partial N}, B) + (B, c) & \mapsto (1_{\partial N}, B) + \end{align*} + Wir bezeichnen mit $T(x)$ den output des transducers beim Lauf auf $x$. + + Betrachte nun die edit-linse $(\Rrightarrow, \Lleftarrow)$ für $T$ und insbesondere $e_o^{-1} = \pi_2(\Rrightarrow(\pi_1(\Rrightarrow(\ground, \text{Replace}(c))), \text{Replace}(\text{init})))$. + Da $T(\text{init}_M) = \text{init}_N$ und $T(c) = e_o$ muss nun gelten, dass $e_o^{-1} \cdot e_o = \init_N$, also $\partial N$ eine Gruppe. \begin{code} diffContTrans :: forall state input output. ( Container input, Container output -- cgit v1.2.3