Mercurial > hg > Papers > 2015 > atton-thesis
changeset 45:12c5e455fe55
Writing description proofs of monad-laws for delta
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 15 Feb 2015 10:33:47 +0900 |
| parents | 4f1107f1f6aa |
| children | 1b688e70f2a8 |
| files | Makefile agda.tex proof_delta.tex replace_agda.rb src/delta_association_law.agda src/delta_eta_is_nt.agda src/delta_left_unity_law.agda src/delta_monad_in_agda.agda src/delta_mu_is_nt.agda src/delta_right_unity_law.agda |
| diffstat | 10 files changed, 235 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/Makefile Fri Feb 13 18:10:07 2015 +0900 +++ b/Makefile Sun Feb 15 10:33:47 2015 +0900 @@ -6,6 +6,7 @@ dvipdfmx $< $(TARGET).dvi : $(wildcard *.tex) $(wildcard fig/*.pdf) + ruby replace_agda.rb platex $(TARGET).tex platex $(TARGET).tex platex $(TARGET).tex
--- a/agda.tex Fri Feb 13 18:10:07 2015 +0900 +++ b/agda.tex Sun Feb 15 10:33:47 2015 +0900 @@ -1,13 +1,14 @@ \chapter{証明支援系言語 Agda による証明手法} \label{chapter:agda} -第\ref{chapter:category}章においては functor, natural transformation, monad の定義と functional programming における対応について述べた。 +第\ref{chapter:category}章では functor, natural transformation, monad の定義を行ない、第\ref{chapter:functional_programming}章では functional programming における対応を述べた。 その中で、 Functor 則や Monad 則といった満たすべき性質がいくつか存在した。 -functional programming において、あるデータ型やそれに対応する計算が Functor 則を満たすことを保証することは言語の実装に依存していい。 -例えば、 Haskell において functor は型クラスによって提供されるため、型レベルのチェックに留まっている。 -そのため、型チェックは通るが Functor 則を満たさない functor が定義可能となってしまう。 +functional programming において、あるデータ型と対応する計算が Functor 則を満たすかの保証は言語の実装に依存している。 +例えば、 Haskell において functor は型クラスによって提供されるため、型レベルのチェックを行なう。 +そのため、型チェックは通るが Functor 則を満たさない functor が定義できてしまう。 +よって Haskell において Delta Monad を定義しただけでは証明が存在しない。 +そこで証明支援系言語 Agda を用いて、 Delta が Functor 則と Monad 則を満たすことを証明する。 -そこで、証明支援系言語 Agda を用いて、 Delta が Functor 則と Monad 則を満たすことを証明することとする。 -そのためにまずは Agda における証明手法について述べる。 +第\ref{chapter:agda}章は Agda における証明手法について述べる。 % {{{ Natural Deduction
--- a/proof_delta.tex Fri Feb 13 18:10:07 2015 +0900 +++ b/proof_delta.tex Sun Feb 15 10:33:47 2015 +0900 @@ -202,3 +202,99 @@ \section{Delta が Monad 則を満たす証明} \label{section:delta_is_monad} +\ref{section:monad_laws_in_agda}節において Agda における Monad則の定義を行なった。 +\ref{section:delta_is_monad}節では Delta に対する $ \eta $ と $ \mu $ の定義と Delta における $ triple $ がMonadであることの証明を行なう。 +これから証明する Delta を用いたプログラムは全ての値がバージョンを持ち、全ての関数はバージョンを持った値を返すものとする。 +さらに、バージョンはプログラム全体で1以上の値を持ち、プログラム内で統一されるものとする。 + +まず、リスト\ref{src:delta_instance_monad} で示した Delta Monad のメタ計算を Agda で再定義する(リスト\ref{src:delta_monad_in_agda})。 +Haskell での定義は Kleisli Trple による定義であるため、リスト\ref{src:monad_and_bind}で示した Kleisli Triple と Monad の対応を用いて定義していることに留意する。 + +\begin{table}[html] + \lstinputlisting[label=src:delta_monad_in_agda, caption=Agdaにおける Delta に対する Monad の定義] {src/delta_monad_in_agda.agda.replaced} +\end{table} + + +$ \eta $ に相当する delta-eta はメタ計算における T を1つ増やす演算に相当する。 +内包する値のバージョンに依存して Delta が持つバージョンが決まるため、 Nat の値によりバージョン数を決められるようにしておく。 +これは Delta でない値に対してはバージョン1とし、Deltaである値はDeltaのバージョンと同じバージョンを返すようにする。 +なお、パターンマッチの項に存在する \verb/{}/ は、 implicit な値のパターンマッチに用いられる。 +例えば \verb/{n = S x}/ とすれば、 implicit な値 n は S により構成され、残りの値は x に束縛される。 + +次に $ \mu $ に相当する delta-mu を定義する。 +delta-mu は複数の \verb/TT -> T/に対応するメタ計算であるため、1段ネストされた Delta を受けとり、Deltaとして返す。 +これはバージョン管理された値に対し、バージョン管理された関数を適用した場合の値の選択に相当する。 +例えばバージョンが5であった場合、全ての組み合せは5パターン存在する。 +その中から5つを選ぶルールとして $ \mu $ を定義する。 +$ \mu $ は値と関数が同じバージョンであるような結果を選ぶように定義する。 + +同じバージョンである値を選ぶため、先頭のバージョンの値を取る headDelta 関数と、先頭以外のバージョン列を取る tailDelta 関数を用いている。 + +Delta Monad に対応する $ triple (T, \eta, \mu ) $ が定義できた。 +これから Monad 則を満たすことを証明していく。 + +\begin{enumerate} + \item $ \eta $ が natural transformation であること + + まず、 $ \eta $ が natural transformation であることを示す(リスト\ref{src:delta_eta_is_nt_in_agda})。 + eta は T を1つ増やす演算であるが、値のバージョンに応じて挙動を変える。 + よって n によりパターンマッチすることで証明も変更する。 + 特に n が O である時は同じ項に簡約されるために refl で証明することができ、n が O 以上であれば再帰的に証明することができる。 + + +\begin{table}[html] + \lstinputlisting[label=src:delta_eta_is_nt_in_agda, + caption= Agda における Delta の $ \eta$ が natural transformation である証明] + {src/delta_eta_is_nt.agda.replaced} +\end{table} + \item $ \mu $ が natural transformation であること + + 次に $ \mu $ が natural transformation であることを示す(リスト\ref{src:delta_mu_is_nt_in_agda})。 + + $ \mu $ の証明もバージョンによるパターンマッチで行なわれる。 + バージョンが1である場合は refl で証明できるが、1以上の場合に同じ証明で再帰的に定義できない。 + なぜなら、$ \mu $ はTT に対するであり、 TT の両方のバージョンが等しい場合にのみ適用する。 + しかし証明中で外部のTに対する演算を先に行なっているために内部の項とバージョン数が合わない項が存在する。 + その項に対する演算を含めた等式が証明中で必須となるため、別の項に証明を分離した。 + 分離した証明 \verb/tailDelta-to-tail-nt/ では \verb/d : Delta (Delta A (S (S m))) (S n) / のように内部と外部の Nat が違うことに留意してもらいたい。 + +\begin{table}[html] + \lstinputlisting[basicstyle={\scriptsize}, + numberstyle={\tiny}, + label=src:delta_mu_is_nt_in_agda, + caption= Agda における Delta の $ \mu$ が natural transformation である証明] + {src/delta_mu_is_nt.agda.replaced} +\end{table} + + \item T に対する演算の単位元が存在する + +\begin{table}[html] + \lstinputlisting[basicstyle={\scriptsize}, + numberstyle={\tiny}, + label=src:delta_right_unity_law, + caption= Agda における Delta に対する演算に右側単位元が存在する証明] + {src/delta_right_unity_law.agda.replaced} +\end{table} + +\begin{table}[html] + \lstinputlisting[basicstyle={\scriptsize}, + numberstyle={\tiny}, + label=src:delta_left_unity_law, + caption= Agda における Delta に対する演算に左側単位元が存在する証明] + {src/delta_left_unity_law.agda.replaced} +\end{table} + + \item T に対する演算の可換性が存在する + +\begin{table}[html] + \lstinputlisting[basicstyle={\scriptsize}, + numberstyle={\tiny}, + label=src:delta_association_law, + caption= Agda における Delta に対する演算に可換性が存在する証明] + {src/delta_association_law.agda.replaced} +\end{table} + +\end{enumerate} + + +
--- a/replace_agda.rb Fri Feb 13 18:10:07 2015 +0900 +++ b/replace_agda.rb Sun Feb 15 10:33:47 2015 +0900 @@ -1,6 +1,7 @@ #!/usr/bin/env ruby replace_table = { + '->' => 'rightarrow', '∙' => 'circ', '≡' => 'equiv', '×' => 'times',
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/delta_association_law.agda Sun Feb 15 10:33:47 2015 +0900 @@ -0,0 +1,39 @@ +delta-fmap-mu-to-tail : {l : Level} {A : Set l} (n m : Nat) -> + (d : Delta (Delta (Delta A (S (S m))) (S (S m))) (S n)) -> + delta-fmap tailDelta (delta-fmap delta-mu d) + ≡ + (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta d))) +delta-fmap-mu-to-tail O O (mono (delta d ds)) = refl +delta-fmap-mu-to-tail O (S n) (mono (delta (delta x (delta xx d)) (delta (delta dx (delta dxx dd)) ds))) = refl +delta-fmap-mu-to-tail (S n) O (delta (delta (delta x (mono xx)) (mono (delta dx (mono dxx)))) ds) = begin + delta (mono dxx) (delta-fmap tailDelta (delta-fmap delta-mu ds)) + ≡⟨ cong (\de -> delta (mono dxx) de) (delta-fmap-mu-to-tail n O ds) ⟩ + delta (mono dxx) + (delta-fmap delta-mu + (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) + ∎ +delta-fmap-mu-to-tail (S n) (S m) (delta (delta (delta x (delta xx d)) + (delta (delta dx (delta dxx dd)) ds)) dds) = begin + delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds)))) + (delta-fmap tailDelta (delta-fmap delta-mu dds)) + ≡⟨ cong (\de -> delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds)))) de) + (delta-fmap-mu-to-tail n (S m) dds) ⟩ + delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds)))) + (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta dds))) + ∎ + + + +delta-association-law : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) -> + ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d) +delta-association-law {n = O} (mono d) = refl +delta-association-law {n = S n} (delta (delta (delta x d) dd) ds) = begin + delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) + ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-fmap-mu-to-tail n n ds) ⟩ + delta x (delta-mu (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds)))) + ≡⟨ cong (\de -> delta x de) + (delta-association-law (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) ⟩ + delta x (delta-mu (delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds)))) + ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-mu-is-nt tailDelta (delta-fmap tailDelta ds) ) ⟩ + delta x (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds)))) + ∎
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/delta_eta_is_nt.agda Sun Feb 15 10:33:47 2015 +0900 @@ -0,0 +1,12 @@ +delta-eta-is-nt : {l : Level} {A B : Set l} -> {n : Nat} + (f : A -> B) -> (x : A) -> + (delta-eta {n = n} ∙ f) x ≡ delta-fmap f (delta-eta x) +delta-eta-is-nt {n = O} f x = refl +delta-eta-is-nt {n = S n} f x = begin + (delta-eta ∙ f) x ≡⟨ refl ⟩ + delta-eta (f x) ≡⟨ refl ⟩ + delta (f x) (delta-eta (f x)) + ≡⟨ cong (\de -> delta (f x) de) (delta-eta-is-nt f x) ⟩ + delta (f x) (delta-fmap f (delta-eta x)) ≡⟨ refl ⟩ + delta-fmap f (delta x (delta-eta x)) ≡⟨ refl ⟩ + delta-fmap f (delta-eta x) ∎
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/delta_left_unity_law.agda Sun Feb 15 10:33:47 2015 +0900 @@ -0,0 +1,15 @@ +delta-left-unity-law : {l : Level} {A : Set l} {n : Nat} -> (d : Delta A (S n)) -> + (delta-mu ∙ (delta-fmap delta-eta)) d ≡ id d +delta-left-unity-law (mono x) = refl +delta-left-unity-law {n = (S n)} (delta x d) = begin + (delta-mu ∙ delta-fmap delta-eta) (delta x d) ≡⟨ refl ⟩ + delta-mu ( delta-fmap delta-eta (delta x d)) ≡⟨ refl ⟩ + delta-mu (delta (delta-eta x) (delta-fmap delta-eta d)) ≡⟨ refl ⟩ + delta (headDelta {n = S n} (delta-eta x)) (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d))) + ≡⟨ refl ⟩ + delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d))) + ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (delta-covariant tailDelta delta-eta d)) ⟩ + delta x (delta-mu (delta-fmap (tailDelta ∙ delta-eta {n = S n}) d)) ≡⟨ refl ⟩ + delta x (delta-mu (delta-fmap (delta-eta {n = n}) d)) ≡⟨ cong (\de -> delta x de) (delta-left-unity-law d) ⟩ + delta x d ≡⟨ refl ⟩ + id (delta x d) ∎
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/delta_monad_in_agda.agda Sun Feb 15 10:33:47 2015 +0900 @@ -0,0 +1,17 @@ +headDelta : {l : Level} {A : Set l} {n : Nat} -> Delta A (S n) -> A +headDelta (mono x) = x +headDelta (delta x _) = x + +tailDelta : {l : Level} {A : Set l} {n : Nat} -> + Delta A (S (S n)) -> Delta A (S n) +tailDelta (delta _ d) = d + + +delta-eta : {l : Level} {A : Set l} {n : Nat} -> A -> Delta A (S n) +delta-eta {n = O} x = mono x +delta-eta {n = (S n)} x = delta x (delta-eta {n = n} x) + +delta-mu : {l : Level} {A : Set l} {n : Nat} -> + (Delta (Delta A (S n)) (S n)) -> Delta A (S n) +delta-mu (mono x) = x +delta-mu (delta x d) = delta (headDelta x) (delta-mu (delta-fmap tailDelta d))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/delta_mu_is_nt.agda Sun Feb 15 10:33:47 2015 +0900 @@ -0,0 +1,26 @@ +tailDelta-to-tail-nt : {l : Level} {A B : Set l} (n m : Nat) + (f : A -> B) (d : Delta (Delta A (S (S m))) (S n)) -> + delta-fmap tailDelta (delta-fmap (delta-fmap f) d) ≡ delta-fmap (delta-fmap f) (delta-fmap tailDelta d) +tailDelta-to-tail-nt O O f (mono (delta x d)) = refl +tailDelta-to-tail-nt O (S m) f (mono (delta x d)) = refl +tailDelta-to-tail-nt (S n) O f (delta (delta x (mono xx)) d) = begin + delta (mono (f xx)) (delta-fmap tailDelta (delta-fmap (delta-fmap f) d)) + ≡⟨ cong (\de -> delta (mono (f xx)) de) (tailDelta-to-tail-nt n O f d) ⟩ + delta (mono (f xx)) (delta-fmap (delta-fmap f) (delta-fmap tailDelta d)) + ∎ +tailDelta-to-tail-nt (S n) (S m) f (delta (delta x (delta xx d)) ds) = begin + delta (delta (f xx) (delta-fmap f d)) (delta-fmap tailDelta (delta-fmap (delta-fmap f) ds)) + ≡⟨ cong (\de -> delta (delta (f xx) (delta-fmap f d)) de) (tailDelta-to-tail-nt n (S m) f ds) ⟩ + delta (delta (f xx) (delta-fmap f d)) (delta-fmap (delta-fmap f) (delta-fmap tailDelta ds)) + ∎ + +delta-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} -> (f : A -> B) -> (d : Delta (Delta A (S n)) (S n)) + -> delta-mu (delta-fmap (delta-fmap f) d) ≡ delta-fmap f (delta-mu d) +delta-mu-is-nt {n = O} f (mono d) = refl +delta-mu-is-nt {n = S n} f (delta (delta x d) ds) = begin + delta (f x) (delta-mu (delta-fmap tailDelta (delta-fmap (delta-fmap f) ds))) + ≡⟨ cong (\de -> delta (f x) (delta-mu de)) (tailDelta-to-tail-nt n n f ds ) ⟩ + delta (f x) (delta-mu (delta-fmap (delta-fmap f) (delta-fmap tailDelta ds))) + ≡⟨ cong (\de -> delta (f x) de) (delta-mu-is-nt f (delta-fmap tailDelta ds)) ⟩ + delta (f x) (delta-fmap f (delta-mu (delta-fmap tailDelta ds))) + ∎
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/delta_right_unity_law.agda Sun Feb 15 10:33:47 2015 +0900 @@ -0,0 +1,21 @@ +delta-right-unity-law : {l : Level} {A : Set l} {n : Nat} -> + (d : Delta A (S n)) -> (delta-mu ∙ delta-eta) d ≡ id d +delta-right-unity-law (mono x) = refl +delta-right-unity-law (delta x d) = begin + (delta-mu ∙ delta-eta) (delta x d) + ≡⟨ refl ⟩ + delta-mu (delta-eta (delta x d)) + ≡⟨ refl ⟩ + delta-mu (delta (delta x d) (delta-eta (delta x d))) + ≡⟨ refl ⟩ + delta (headDelta (delta x d)) (delta-mu (delta-fmap tailDelta (delta-eta (delta x d)))) + ≡⟨ refl ⟩ + delta x (delta-mu (delta-fmap tailDelta (delta-eta (delta x d)))) + ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (delta-eta-is-nt tailDelta (delta x d))) ⟩ + delta x (delta-mu (delta-eta (tailDelta (delta x d)))) + ≡⟨ refl ⟩ + delta x (delta-mu (delta-eta d)) + ≡⟨ cong (\de -> delta x de) (delta-right-unity-law d) ⟩ + delta x d + ≡⟨ refl ⟩ + id (delta x d) ∎