Mercurial > hg > Papers > 2015 > atton-thesis

changeset 53:ca389989b660

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add original sources
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 15 Feb 2015 22:38:43 +0900
parents 6ca594d19ca4
children bf136bd59e7a
files main.tex original_sources.tex proof_deltaM.tex src/deltaM_is_monad.agda src/orig/Delta.hs src/orig/DeltaM.hs src/orig/Example/Delta.hs src/orig/Example/DeltaM.hs thanks.tex
diffstat 9 files changed, 682 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/main.tex	Sun Feb 15 21:56:19 2015 +0900
+++ b/main.tex	Sun Feb 15 22:38:43 2015 +0900
@@ -3,6 +3,7 @@
 \usepackage{mythesis}
 \usepackage{multirow}
 \usepackage{here}
+\usepackage{float}
 \usepackage{listings}
 \usepackage{bussproofs}
 \usepackage{amssymb}
@@ -92,8 +93,7 @@
 
 % 付録
 \appendix
+\input{original_sources}
 % \input{proof_deltaM}
-% TODO: 実験環境
-% TODO: Delta と DeltaM の本体
 
 \end{document}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/original_sources.tex	Sun Feb 15 22:38:43 2015 +0900
@@ -0,0 +1,38 @@
+\chapter{Haskell による Delta と DeltaM の定義と使用例のプログラム}
+\label{chapter:original_sources}
+
+\section{実験環境}
+
+表\ref{table:environment}に実験環境におけるプログラムやライブラリのバージョンを示す。
+
+\begin{table}[htbp]
+    \begin{center}
+        \begin{tabular}{|c||c|} \hline
+            & version   \\ \hline \hline
+            Mac OS X & 10.9.5    \\ \hline
+            ghc      & 7.8.4     \\ \hline
+            Agda     & 2.4.2.2   \\ \hline
+            cabal    & 1.22.0.0  \\ \hline
+        \end{tabular}
+        \label{table:environment}
+        \caption{実験環境}
+    \end{center}
+\end{table}
+
+\section{Delta と DeltaM のソースコード}
+
+\begin{table}[html]
+    \lstinputlisting[basicstyle={\scriptsize},
+                     numberstyle={\tiny},
+                     label=src:original_delta,
+                     caption= Delta のソースコード,
+                     escapechar=&] {src/orig/Delta.hs}
+\end{table}
+
+\begin{table}[html]
+    \lstinputlisting[basicstyle={\scriptsize},
+                     numberstyle={\tiny},
+                     label=src:original_deltaM,
+                     caption= DeltaM のソースコード,
+                     escapechar=&] {src/orig/DeltaM.hs}
+\end{table}
--- a/proof_deltaM.tex	Sun Feb 15 21:56:19 2015 +0900
+++ b/proof_deltaM.tex	Sun Feb 15 22:38:43 2015 +0900
@@ -1,2 +1,20 @@
 \section{DeltaM が Monad 則を満たす証明}
+DeltaM に対する Monad 則の証明も Agda によって行なう。
+プログラム内部のDeltaのバージョン数は全て同じであるとし、1以上とする。
 
+内部に持つ型引数を持つ型M は Functor と Monad であるとする。
+基本的に同じ法則を用いて証明していくことになる。
+例えば $ \eta $ が natural transformation である証明には、 M の $ \eta $ が natural transformation である証明を用いる。
+また、同じ値に対して同じ振舞いをする関数を fmap しても同じであるという fmap-equiv という等式を導入している。
+これは高階関数に対する等式が定義できなかったためである。
+
+DeltaM に対する Monad 則の証明がリスト\ref{src:deltaM_is_monad}である。
+なお、Functor則に対する証明も行なったが省略する。
+
+\begin{table}
+    \lstinputlisting[basicstyle={\scriptsize},
+                     numberstyle={\tiny},
+                     label=src:deltaM_is_monad,
+                     caption= DeltaM が Monad 則を満たす証明]
+                     {src/deltaM_is_monad.agda.replaced}
+\end{table}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/deltaM_is_monad.agda	Sun Feb 15 22:38:43 2015 +0900
@@ -0,0 +1,443 @@
+open import Level
+open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+
+open import basic
+open import delta
+open import delta.functor
+open import delta.monad
+open import deltaM
+open import deltaM.functor
+open import nat
+open import laws
+
+module deltaM.monad where
+open Functor
+open NaturalTransformation
+open Monad
+
+
+-- sub proofs
+
+deconstruct-id : {l : Level} {A : Set l} {n : Nat}
+                 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
+                 (d : DeltaM M A (S n)) -> deltaM (unDeltaM d) ≡ d
+deconstruct-id {n = O}   (deltaM x) = refl
+deconstruct-id {n = S n} (deltaM x) = refl
+
+headDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat}
+                    {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
+                    (f : A -> B) -> (x : (DeltaM M A (S n))) ->
+                    ((fmap F f) ∙ headDeltaM) x ≡ (headDeltaM ∙ (deltaM-fmap f)) x
+headDeltaM-with-f {n = O} f   (deltaM (mono x))    = refl
+headDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl
+
+
+tailDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat}
+                    {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
+                    (f : A -> B) -> (d : (DeltaM M A (S (S n)))) ->
+                    (tailDeltaM ∙ (deltaM-fmap f)) d ≡ ((deltaM-fmap f) ∙ tailDeltaM) d
+tailDeltaM-with-f {n = O} f (deltaM (delta x d))   = refl
+tailDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl
+
+
+
+fmap-headDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat}
+                                 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
+                                 (x : T (DeltaM M (DeltaM M A (S n)) (S n))) ->
+                   fmap F (headDeltaM ∙ deltaM-mu) x ≡ fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x
+fmap-headDeltaM-with-deltaM-mu {n = O}   x = refl
+fmap-headDeltaM-with-deltaM-mu {n = S n} x = refl
+
+
+fmap-tailDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat}
+                                 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
+               (d : DeltaM M (DeltaM M (DeltaM M A (S (S n))) (S (S n))) (S n)) ->
+                deltaM-fmap (tailDeltaM ∙ deltaM-mu) d ≡ deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) d
+fmap-tailDeltaM-with-deltaM-mu {n = O} (deltaM (mono x)) = refl
+fmap-tailDeltaM-with-deltaM-mu {n = S n} (deltaM d)      = refl
+
+
+
+
+
+-- main proofs
+
+deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat}
+                   {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
+                   (f : A -> B) -> (x : A) ->
+                   ((deltaM-eta {l} {B} {n} {T} {F} {M} )∙ f) x ≡ deltaM-fmap f (deltaM-eta x)
+deltaM-eta-is-nt {l} {A} {B} {O} {M} {fm} {mm} f x   = begin
+  deltaM-eta {n = O} (f x)              ≡⟨ refl ⟩
+  deltaM (mono (eta mm (f x)))          ≡⟨ cong (\de -> deltaM (mono de)) (eta-is-nt mm f x) ⟩
+  deltaM (mono (fmap fm f (eta mm x)))  ≡⟨ refl ⟩
+  deltaM-fmap f (deltaM-eta {n = O} x)  ∎
+deltaM-eta-is-nt {l} {A} {B} {S n} {M} {fm} {mm} f x = begin
+  deltaM-eta {n = S n} (f x)
+  ≡⟨ refl ⟩
+  deltaM (delta-eta {n = S n} (eta mm (f x)))
+  ≡⟨ refl ⟩
+  deltaM (delta (eta mm (f x)) (delta-eta (eta mm (f x))))
+  ≡⟨ cong (\de -> deltaM (delta de (delta-eta de))) (eta-is-nt mm f x) ⟩
+  deltaM (delta (fmap fm f (eta mm x)) (delta-eta (fmap fm f (eta mm x))))
+  ≡⟨ cong (\de ->  deltaM (delta (fmap fm f (eta mm x)) de)) (eta-is-nt delta-is-monad (fmap fm f) (eta mm x)) ⟩
+  deltaM (delta (fmap fm f (eta mm x)) (delta-fmap (fmap fm f) (delta-eta (eta mm x))))
+  ≡⟨ refl ⟩
+  deltaM-fmap f (deltaM-eta {n = S n} x)
+  ∎
+
+
+
+
+deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat}
+                  {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
+                  (f : A -> B) -> (d : DeltaM M (DeltaM M A (S n)) (S n)) ->
+                  deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d)
+deltaM-mu-is-nt {l} {A} {B} {O} {T} {F} {M}  f (deltaM (mono x)) = begin
+  deltaM-fmap f (deltaM-mu (deltaM (mono x)))
+  ≡⟨ refl ⟩
+  deltaM-fmap f (deltaM (mono (mu M (fmap F headDeltaM x))))
+  ≡⟨ refl ⟩
+  deltaM (mono (fmap F f (mu M (fmap F headDeltaM x))))
+  ≡⟨ cong (\de -> deltaM (mono de)) (sym (mu-is-nt M f (fmap F headDeltaM x))) ⟩
+  deltaM (mono (mu M (fmap F (fmap F f) (fmap F headDeltaM x))))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F headDeltaM (fmap F f) x)) ⟩
+  deltaM (mono (mu M (fmap F ((fmap F f) ∙ headDeltaM) x)))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (fmap-equiv F (headDeltaM-with-f f) x) ⟩
+  deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F (deltaM-fmap f) (headDeltaM) x) ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F (deltaM-fmap f) x)))))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x)))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (mono x)))
+  ∎
+deltaM-mu-is-nt {l} {A} {B} {S n} {T} {F} {M} f (deltaM (delta x d)) = begin
+  deltaM-fmap f (deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩
+  deltaM-fmap f (deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta x d)))))
+                               (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d))))))))
+  ≡⟨ refl ⟩
+  deltaM-fmap f (deltaM (delta (mu M (fmap F (headDeltaM {M = M}) x))
+                               (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (fmap F f (mu M (fmap F (headDeltaM {M = M}) x)))
+                (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta de
+                  (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
+           (sym (mu-is-nt M f (fmap F headDeltaM x)))  ⟩
+  deltaM (delta (mu M (fmap F (fmap F f) (fmap F (headDeltaM {M = M}) x)))
+                (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de) (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
+           (sym (covariant F headDeltaM (fmap F f) x)) ⟩
+  deltaM (delta (mu M (fmap F ((fmap F f) ∙ (headDeltaM {M = M})) x))
+                (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de) (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
+           (fmap-equiv F (headDeltaM-with-f f) x)  ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-fmap f (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM de)))
+           (deltaM-mu-is-nt {l} {A} {B} {n} {T} {F} {M} f (deltaM-fmap tailDeltaM (deltaM d))) ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (deltaM-fmap {n = n} f) (deltaM-fmap {n = n} (tailDeltaM {n = n}) (deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de))))
+           (sym (deltaM-covariant (deltaM-fmap f) tailDeltaM (deltaM d))) ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap {n = n} ((deltaM-fmap {n = n} f) ∙ (tailDeltaM {n = n})) (deltaM d)))))
+
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de))))
+               (sym (deltaM-fmap-equiv (tailDeltaM-with-f f) (deltaM d))) ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM ∙ (deltaM-fmap f)) (deltaM d)))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de))))
+           (deltaM-covariant tailDeltaM (deltaM-fmap f) (deltaM d)) ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-fmap (deltaM-fmap f) (deltaM d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d)))))))
+           (covariant F (deltaM-fmap f) headDeltaM x) ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x)))
+                      (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d))))))
+                      (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d))))))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d)))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (delta x d)))
+  ∎
+
+
+
+
+
+deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat}
+                         {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
+                         (d : DeltaM M A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d
+deltaM-right-unity-law {l} {A} {O} {M} {fm} {mm} (deltaM (mono x)) = begin
+  deltaM-mu (deltaM-eta (deltaM (mono x)))             ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (eta mm (deltaM (mono x))))) ≡⟨ refl ⟩
+  deltaM (mono (mu mm (fmap fm (headDeltaM {M = mm})(eta mm (deltaM (mono x))))))
+  ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (eta-is-nt mm headDeltaM (deltaM (mono x)) )) ⟩
+  deltaM (mono (mu mm (eta mm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) (deltaM (mono x)))))) ≡⟨ refl ⟩
+  deltaM (mono (mu mm (eta mm x))) ≡⟨ cong (\de -> deltaM (mono de)) (sym (right-unity-law mm x)) ⟩
+  deltaM (mono x)
+  ∎
+deltaM-right-unity-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
+  deltaM-mu (deltaM-eta (deltaM (delta x d)))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (delta (eta M (deltaM (delta x d))) (delta-eta (eta M (deltaM (delta x d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta {l} {T (DeltaM M A (S (S n)))} {n} (eta M (deltaM (delta x d))) (delta-eta (eta M (deltaM (delta x d)))))))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (eta M (deltaM (delta x d))) (delta-eta (eta M (deltaM (delta x d)))))))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (eta M (deltaM (delta x d)))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de)
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))))
+     (sym (eta-is-nt M headDeltaM (deltaM (delta x d)))) ⟩
+  deltaM (delta (mu M (eta M (headDeltaM {M = M} (deltaM (delta x d)))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (eta M x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
+  ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))))
+           (sym (right-unity-law M x)) ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
+  ≡⟨ refl ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-fmap (fmap F tailDeltaM) (delta-eta (eta M (deltaM (delta x d)))))))))
+  ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM de)))))
+           (sym (delta-eta-is-nt (fmap F tailDeltaM)  (eta M (deltaM (delta x d))))) ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (fmap F tailDeltaM (eta M (deltaM (delta x d)))))))))
+  ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta de))))))
+           (sym (eta-is-nt M tailDeltaM (deltaM (delta x d)))) ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (eta M (tailDeltaM (deltaM (delta x d)))))))))
+  ≡⟨ refl ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (eta M (deltaM d)))))))
+  ≡⟨ refl ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-eta (deltaM d)))))
+  ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-right-unity-law (deltaM d)) ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM d)))
+  ≡⟨ refl ⟩
+  deltaM (delta x d)
+  ∎
+
+
+
+
+
+
+deltaM-left-unity-law : {l : Level} {A : Set l} {n : Nat}
+                        {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
+                        (d : DeltaM M A (S n)) -> (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d
+deltaM-left-unity-law {l} {A}   {O} {T} {F} {M} (deltaM (mono x)) = begin
+  deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (fmap F deltaM-eta x)))      ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-eta x)))))))      ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-eta x))))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F deltaM-eta headDeltaM x)) ⟩
+  deltaM (mono (mu M (fmap F ((headDeltaM {n = O} {M = M}) ∙ deltaM-eta) x)))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (eta M) x)))
+  ≡⟨ cong (\de -> deltaM (mono de)) (left-unity-law M x) ⟩
+  deltaM (mono x)
+  ∎
+deltaM-left-unity-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
+  deltaM-mu (deltaM-fmap deltaM-eta (deltaM (delta x d)))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (delta (fmap F deltaM-eta x) (delta-fmap (fmap F deltaM-eta) d)))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {n = S n} {M = M}) (headDeltaM {n = S n} {M = M} (deltaM (delta (fmap F deltaM-eta x) (delta-fmap (fmap F deltaM-eta) d))))))
+  (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (fmap F deltaM-eta x) (delta-fmap (fmap F deltaM-eta) d))))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {n = S n} {M = M}) (fmap F deltaM-eta x)))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d)))))))
+           (sym (covariant F deltaM-eta headDeltaM x)) ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {n = S n} {M = M}) ∙  deltaM-eta) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (eta M) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))
+  ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d)))))))
+           (left-unity-law M x) ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM {n = n})(deltaM-fmap (deltaM-eta {n = S n})(deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu de)))) (sym (deltaM-covariant tailDeltaM deltaM-eta (deltaM d))) ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((tailDeltaM {n = n}) ∙ (deltaM-eta {n = S n})) (deltaM d)))))
+  ≡⟨ refl ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap deltaM-eta (deltaM d)))))
+  ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-left-unity-law (deltaM d)) ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM d)))
+  ≡⟨ refl ⟩
+  deltaM (delta x d)
+  ∎
+
+deltaM-association-law : {l : Level} {A : Set l} {n : Nat}
+                         {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
+                         (d : DeltaM M (DeltaM M (DeltaM M A (S n)) (S n))  (S n)) ->
+                         deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d)
+deltaM-association-law {l} {A}   {O} {T} {F} {M} (deltaM (mono x))    = begin
+  deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x)))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (fmap F deltaM-mu x)))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-mu x)))))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-mu x))))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F deltaM-mu headDeltaM x)) ⟩
+  deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ deltaM-mu) x)))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x)))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F headDeltaM ((mu M) ∙ (fmap F headDeltaM)) x) ⟩
+  deltaM (mono (mu M ((((fmap F (((mu M) ∙ (fmap F headDeltaM)))) ∙ (fmap F headDeltaM)) x))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M ((((fmap F (((mu M) ∙ (fmap F headDeltaM)))) (fmap F headDeltaM x))))))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F (fmap F headDeltaM) (mu M) (fmap F headDeltaM x)) ⟩
+  deltaM (mono (mu M (((fmap F (mu M)) ∙ (fmap F (fmap F headDeltaM))) (fmap F headDeltaM x))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (mu M) ((fmap F (fmap F headDeltaM) (fmap F headDeltaM x))))))
+  ≡⟨ cong (\de -> deltaM (mono de)) (association-law M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x))) ⟩
+  deltaM (mono (mu M (mu M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x)))))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (mu-is-nt M headDeltaM (fmap F headDeltaM x)) ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (mu M (fmap F (headDeltaM {M = M}) x)))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) x))))))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) x))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono x)))))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM-mu (deltaM (mono x)))
+
+  ∎
+
+deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
+  deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d)))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (delta (fmap F deltaM-mu x) (delta-fmap (fmap F deltaM-mu) d)))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM (delta (fmap F deltaM-mu x) (delta-fmap (fmap F deltaM-mu) d))))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (fmap F deltaM-mu x) (delta-fmap (fmap F deltaM-mu) d))))))))
+
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {A = A} {M = M}) (fmap F deltaM-mu x)))
+                (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d)))))))
+           (sym (covariant F deltaM-mu headDeltaM x)) ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {A = A} {M = M}) ∙  deltaM-mu) x))
+                (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de)
+                          (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d)))))))
+           (fmap-headDeltaM-with-deltaM-mu {A = A} {M = M} x) ⟩
+  deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
+                (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-fmap deltaM-mu (deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
+                                 (unDeltaM {M = M} (deltaM-mu de))))
+           (sym (deltaM-covariant tailDeltaM deltaM-mu (deltaM d))) ⟩
+  deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM ∙ deltaM-mu) (deltaM d)))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
+                                 (unDeltaM {M = M} (deltaM-mu de))))
+           (fmap-tailDeltaM-with-deltaM-mu (deltaM d))  ⟩
+  deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de)
+                          (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
+          (covariant F headDeltaM ((mu M) ∙ (fmap F headDeltaM)) x) ⟩
+  deltaM (delta (mu M (((fmap F ((mu M) ∙ (fmap F headDeltaM))) ∙ (fmap F headDeltaM)) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (((fmap F ((mu M) ∙ (fmap F headDeltaM))) (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de)
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
+           (covariant F (fmap F headDeltaM)  (mu M) (fmap F headDeltaM x)) ⟩
+
+  deltaM (delta (mu M ((((fmap F (mu M)) ∙ (fmap F (fmap F headDeltaM))) (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (mu M) (fmap F (fmap F headDeltaM) (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
+  ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
+           (association-law M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x))) ⟩
+  deltaM (delta (mu M (mu M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
+           (mu-is-nt M headDeltaM (fmap F headDeltaM x)) ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
+  ≡⟨ cong (\de ->   deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) (unDeltaM {M = M} (deltaM-mu de))))
+           (deltaM-covariant (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) tailDeltaM (deltaM d)) ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (((deltaM-fmap (deltaM-mu ∙ (deltaM-fmap tailDeltaM))  ∙ (deltaM-fmap tailDeltaM)) (deltaM d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (((deltaM-fmap (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) (deltaM-fmap tailDeltaM (deltaM d))))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) (unDeltaM {M = M} (deltaM-mu de))))
+           (deltaM-covariant deltaM-mu (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))  ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (((deltaM-fmap deltaM-mu) ∙ (deltaM-fmap (deltaM-fmap tailDeltaM))) (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap deltaM-mu (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) (unDeltaM {M = M} de)))
+           (deltaM-association-law (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))) ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-mu (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))))))
+
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                                 (unDeltaM {M = M} (deltaM-mu de))))
+           (sym (deltaM-mu-is-nt tailDeltaM (deltaM-fmap tailDeltaM (deltaM d)))) ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                                 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM de)))))
+           (sym (deconstruct-id (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))) ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM
+                  (deltaM (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))))
+
+
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (headDeltaM {M = M} ((deltaM (delta (mu M (fmap F headDeltaM x))
+                           (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM ((deltaM (delta (mu M (fmap F headDeltaM x))
+                           (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))))))))
+
+
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (delta (mu M (fmap F headDeltaM x))
+                           (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (delta (mu M (fmap F headDeltaM (headDeltaM {M = M} (deltaM (delta x d)))))
+                           (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d))))))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM-mu (deltaM (delta x d)))
+  ∎
+
+
+
+
+deltaM-is-monad : {l : Level} {A : Set l} {n : Nat}
+                  {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
+                  Monad {l} (\A -> DeltaM M A (S n)) (deltaM-is-functor {l} {n})
+deltaM-is-monad {l} {A} {n} {T} {F} {M} =
+                record { mu     = deltaM-mu
+                       ; eta    = deltaM-eta
+                       ; eta-is-nt = deltaM-eta-is-nt
+                       ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x)))
+                       ; association-law = deltaM-association-law
+                       ; left-unity-law  = deltaM-left-unity-law
+                       ; right-unity-law = (\x -> (sym (deltaM-right-unity-law x)))
+                       }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/orig/Delta.hs	Sun Feb 15 22:38:43 2015 +0900
@@ -0,0 +1,56 @@
+module Delta ( Delta(..) , deltaAppend , headDelta , tailDelta , deltaFromList) where
+
+import Control.Applicative
+
+
+-- Delta definition
+
+data Delta a = Mono a | Delta a (Delta a) deriving Show
+
+instance (Eq a) => Eq (Delta a) where
+    (Mono x) == (Mono y)         = x == y
+    (Mono _) == (Delta _ _)      = False
+    (Delta x xs) == (Delta y ys) = (x == y) && (xs == ys)
+
+-- basic functions
+
+deltaAppend :: Delta a -> Delta a -> Delta a
+deltaAppend (Mono x) d     = Delta x d
+deltaAppend (Delta x d) ds = Delta x (deltaAppend d ds)
+
+headDelta :: Delta a -> a
+headDelta (Mono  x)   = x
+headDelta (Delta x _) = x
+
+tailDelta :: Delta a -> Delta a
+tailDelta d@(Mono _)   = d
+tailDelta (Delta _ ds) = ds
+
+-- instance definitions
+
+instance Functor Delta where
+    fmap f (Mono x)    = Mono  (f x)
+    fmap f (Delta x d) = Delta (f x) (fmap f d)
+
+instance Applicative Delta where
+    pure f                       = Mono  f
+    (Mono f)     <*> (Mono x)    = Mono  (f x)
+    df@(Mono f)  <*> (Delta x d) = Delta (f x) (df <*> d)
+    (Delta f df) <*> d@(Mono x)  = Delta (f x) (df <*> d)
+    (Delta f df) <*> (Delta x d) = Delta (f x) (df <*> d)
+
+bind :: (Delta a) -> (a -> Delta b) -> (Delta b)
+bind (Mono x)    f = f x
+bind (Delta x d) f = Delta (headDelta (f x)) (bind d (tailDelta . f))
+
+mu :: (Delta (Delta a)) -> (Delta a)
+mu d = bind d id
+
+instance Monad Delta where
+    return x = Mono x
+    d >>= f  = mu $ fmap f d
+
+-- utils
+
+deltaFromList :: [a] -> Delta a
+deltaFromList = (foldl1 deltaAppend) . (fmap return)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/orig/DeltaM.hs	Sun Feb 15 22:38:43 2015 +0900
@@ -0,0 +1,56 @@
+module DeltaM (DeltaM(..), unDeltaM, appendDeltaM, tailDeltaM, headDeltaM, checkOut) where
+
+import Control.Applicative
+import Delta
+
+
+-- DeltaM definition (Delta with Monad)
+
+data DeltaM m a = DeltaM (Delta (m a)) deriving (Show)
+
+
+-- DeltaM utils
+
+unDeltaM :: DeltaM m a -> Delta (m a)
+unDeltaM (DeltaM d) = d
+
+headDeltaM :: DeltaM m a -> m a
+headDeltaM (DeltaM d) = headDelta d
+
+tailDeltaM :: DeltaM m a -> DeltaM m a
+tailDeltaM (DeltaM d) = DeltaM $ tailDelta d
+
+appendDeltaM :: DeltaM m a -> DeltaM m a -> DeltaM m a
+appendDeltaM (DeltaM d) (DeltaM dd) = DeltaM (deltaAppend d dd)
+
+checkOut :: Int -> DeltaM m a -> m a
+checkOut 0 (DeltaM (Mono x))    = x
+checkOut 0 (DeltaM (Delta x _)) = x
+checkOut n (DeltaM (Mono x))    = x
+checkOut n (DeltaM (Delta _ d)) = checkOut (n-1) (DeltaM d)
+
+
+-- DeltaM instance definitions
+
+instance (Functor m) => Functor (DeltaM m) where
+    fmap f (DeltaM d) = DeltaM $ fmap (fmap f) d
+
+instance (Applicative m) => Applicative (DeltaM m) where
+    pure f                                          = DeltaM $ Mono $ pure f
+    (DeltaM (Mono f))     <*> (DeltaM (Mono x))     = DeltaM $ Mono $ f <*> x
+    df@(DeltaM (Mono f))  <*> (DeltaM (Delta x d))  = appendDeltaM (DeltaM $ Mono $ f <*> x) (df <*> (DeltaM d))
+    (DeltaM (Delta f df)) <*> dx@(DeltaM (Mono x))  = appendDeltaM (DeltaM $ Mono $ f <*> x) ((DeltaM df) <*> dx)
+    (DeltaM (Delta f df)) <*> (DeltaM (Delta x dx)) = appendDeltaM (DeltaM $ Mono $ f <*> x) ((DeltaM df) <*> (DeltaM dx))
+
+
+mu' :: (Functor m, Monad m) => DeltaM m (DeltaM m a) -> DeltaM m a
+mu' d@(DeltaM (Mono _))    = DeltaM $ Mono $ (>>= id) $ fmap headDeltaM $ headDeltaM d
+mu' d@(DeltaM (Delta _ _)) = DeltaM $ Delta ((>>= id) $ fmap headDeltaM $ headDeltaM d)
+                                            (unDeltaM (mu' (fmap tailDeltaM (tailDeltaM d))))
+
+instance (Functor m, Monad m) => Monad (DeltaM m) where
+    return x = DeltaM $ Mono $ return x
+    d >>= f  = mu' $ fmap f d
+
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/orig/Example/Delta.hs	Sun Feb 15 22:38:43 2015 +0900
@@ -0,0 +1,22 @@
+module Example.Delta where
+
+import Data.Numbers.Primes
+import Delta
+
+-- examples
+
+generator :: Int -> Delta [Int]
+generator x = let intList = [1..x] in
+                  return intList
+
+numberFilter :: [Int] -> Delta [Int]
+numberFilter xs = let primeList = filter isPrime xs
+                      evenList  = filter even xs    in
+                  Delta evenList (Mono primeList)
+
+count :: [Int] -> Delta Int
+count xs = let primeCount = length xs in
+           return primeCount
+
+numberCount :: Int -> Delta Int
+numberCount x = generator x >>= numberFilter >>= count
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/orig/Example/DeltaM.hs	Sun Feb 15 22:38:43 2015 +0900
@@ -0,0 +1,46 @@
+module Example.DeltaM where
+
+import Control.Monad.Writer
+import Data.Numbers.Primes -- $ cabal install primes
+
+import Delta
+import DeltaM
+
+
+-- DeltaM examples
+
+-- DeltaM example utils
+type DeltaLog     = Writer [String]
+type DeltaWithLog = DeltaM DeltaLog
+
+returnW :: (Show a) => a -> DeltaLog a
+returnW x = do tell $ [show x]
+               return x
+
+dmap :: (m a -> b) -> DeltaM m a -> Delta b
+dmap f (DeltaM d) = fmap f d
+
+deltaWithLogFromList :: (Show a) => [a] -> DeltaWithLog a
+deltaWithLogFromList xs = DeltaM $ deltaFromList $ fmap returnW xs
+
+
+-- example : prime filter
+-- usage   : runWriter $ checkOut 0 $ numberCountM 30  -- run specific version
+--         : dmap runWriter $ numberCountM 30          -- run all version
+
+generatorM :: Int -> DeltaWithLog [Int]
+generatorM x = let intList = [1..x] in
+                             DeltaM $ deltaFromList $ fmap returnW $ replicate 2 intList
+
+numberFilterM :: [Int] -> DeltaWithLog [Int]
+numberFilterM xs = let primeList = filter isPrime xs
+                       evenList  = filter even xs    in
+                      DeltaM $ deltaFromList $ fmap returnW [primeList, evenList]
+
+
+countM :: [Int] -> DeltaWithLog Int
+countM xs = let numberCount = length xs in
+                DeltaM $ deltaFromList $ fmap returnW $ replicate 2 numberCount
+
+numberCountM :: Int -> DeltaWithLog Int
+numberCountM x = generatorM x >>= numberFilterM >>= countM
--- a/thanks.tex	Sun Feb 15 21:56:19 2015 +0900
+++ b/thanks.tex	Sun Feb 15 22:38:43 2015 +0900
@@ -6,7 +6,7 @@
 %GISゼミや英語ゼミに参加した人はその分も入れておく．
 %順番は重要なので気を付けるように．(提出前に周りの人に確認してもらう．)
 
-\hspace{1zw}本研究の遂行、また本論文の作成にあたり、御多忙にも関わらず終始懇切なる御指導と御教授を賜わりました河野真治準教授に深く感謝したします。
+\hspace{1zw}本研究の遂行、また本論文の作成にあたり、御多忙にも関わらず終始懇切なる御指導と御教授を賜わりました河野真治准教授に深く感謝致します。
 
 また一年間共に研究を行い、暖かな気遣いと励ましをもって支えてくれた並列信頼研究室のみなさんに感謝致します。