\chapter{Delta Monad が Monad である証明}
\label{chapter:proof_delta}
第\ref{chapter:agda}章では Agda における証明手法について述べた。
第\ref{chapter:proof_delta}章では Agda を用いて Delta Monad が Monad であることを証明していく。
証明のゴールは Delta Monad が Funcor 則と Monad 則を満たすことの証明である。
なお、証明は全ての Delta が同じバージョンを持つという制約下において成り立った。

% {{{ Agda における Delta Monad の表現

\section{Agda における Delta Monad の表現}
\label{section:delta_in_agda}
\ref{section:delta_in_agda}節では Agda において Delta Monad を再定義する。
Agda は Haskell において実装されているため、ほとんど同様に定義できる(リスト\ref{src:delta_in_agda})。

\begin{table}[html]
    \lstinputlisting[label=src:delta_in_agda, caption=Agdaにおける Delta Monad のデータ定義] {src/delta.agda.replaced}
\end{table}

data型 Delta は型A の値と Nat を持つ。

level とは型のlevelの区別に用いられるものである。
Agda では型も値として扱えるため、同じ式において型と値が混同することがある。
厳密に型と値を区別したい場合、level を定義することで区別する。
levelは任意の level と、関数 suc により定義される。
関数 suc は level を一つ上昇させる関数である。
level l を適用した型を用いる時は Set l と記述する。
今回は証明する対象のプログラムは Set l の level とし、それ以外は Set (suc l) の level とする。

Nat は自然数であり、プログラムのバージョンに対応する。
自然数の定義は\ref{section:reasoning} 節にあるリスト \ref{src:nat}にならうものとする。

data 型 Delta は2つのコンストラクタにより構成される。

\begin{itemize}
    \item mono

        プログラムの最初の変更単位を受けとり、バージョン1とする。
        型Aを取り、バージョンが1のDeltaを構成することでその表現とする。

    \item delta

        変更単位と変更単位の列を受けとり、変更単位を追加する。
        これは変更によるバージョンアップに相当する。
        よって任意の1以上のバージョンを持つ Delta に変更単位を加えることでバージョンを1上昇させる。
\end{itemize}

Agda においてもデータ型 Delta が定義できた。
これからこの定義を用いて Functor則と Monad 則を証明していく。

% }}}

% {{{ Agda における Functor 則

\section{Agda における Functor 則}
\label{section:functor_in_agda}
Agda における Functor 則はリスト \ref{src:record_functor} のように記述した。

\begin{table}[html]
    \lstinputlisting[label=src:record_functor, caption=Agdaにおける Functor則の定義] {src/record_functor.agda.replaced}
\end{table}

Agda ではある性質を持つデータは record 構文によって記述する。
record の値は record の定義時に要請した field を全て満たすことで構築される。
よって、あるデータAが持つべき性質は field に定義し、A を用いた証明によって field を満たす。
field を満たすことで record が構成できた場合、A がある性質を満たすことを Agda において証明したことになる。

record Functor は implicit な値 level と、型引数を持つ関数 F を持つ。
record Functor が取る F は Set l を取り Set l を取る関数である。
Set l が証明の対象となるプログラムであるため、関数F はプログラムのlevel で表現する。
よって、プログラムの level l を取り、変更せずに level l の Set を返すようにする。
それに対し、 F に対する証明となる record Functor は、証明の対象とするプログラムそのものではない。
よって suc により level を一段上げる。
これは、証明の対象となるプログラムと証明そのものを混同しないためである。

record Functor の field には以下のようなものがある。

\begin{itemize}
    \item fmap

        Functor に要請される、category から category への map 関数である。
        型の定義はほとんど Haskell と同じである。
        fmap は任意の型に対して適用可能でなくてはいけないため、map する対象の型Aと map される対象の型Bは implicit とする。

    \item preserve-id

        Functor則の id の保存である。
        型F A  を持つ値x に対するfmap id と id の等価性がなくてはならない。

    \item covariant

        Functor則における関数の合成の保存である。
        関数fとgを合成してから fmap により mapping しても、 f と g を個別に mapping してから合成しても等価性を持たなくてはならない。

    \item fmap-equiv

        ある型A の値x に対して等価である関数f と g を考えた時、 型F A の値 fx の対し、 fmap f としても fmap gとしても等価であることを保証する。
        これは本来はFunctor則には存在しない。
        Agda において Monad の証明に必要であったために追加した。
\end{itemize}

% }}}

% {{{ Delta が Functor 則を満たす証明

\section{Delta が Functor 則を満たす証明}
\label{section:delta_is_functor}
\ref{section:functor_in_agda}節では Agda における Functor則の表現について述べた。
\ref{section:delta_is_functor}節では \ref{section:delta_in_agda}節の Delta Monad の定義を用いてFunctor則を証明していく。

まず、Agdaにおける delta に対する fmap の定義を示す(リスト\ref{src:delta_fmap_in_agda})。

\begin{table}[html]
    \lstinputlisting[label=src:delta_fmap_in_agda, caption= Agda における Delta に対する fmap の定義] {src/delta_fmap.agda}
\end{table}

バージョンが1以上の Delta について fmap を定義する。
関数 f は型 A から B への関数とし、 Delta A から Delta B への関数に mapping する。
コンストラクタ2つのパターンマッチを使って再帰的に f を delta の内部の値への適応することで fmap を行なう。

データ型Delta と関数fmap を定義できたので、これらが Functor 則を満たすか証明していく。
なお、今回 Delta は全ての場合においてバージョンを1以上持つものとする。
その制約は引数の Delta のバージョンに必ず S を付けることで1以下の値を受けつけないようにすることで行なう。


\begin{itemize}
    \item fmap は id を保存する

        リスト\ref{src:delta_preserve_id}に証明を示す。

        \begin{table}[html]
            \lstinputlisting[label=src:delta_preserve_id, caption= Delta における fmap も id を保存する証明] {src/delta_preserve_id.agda.replaced}
        \end{table}


        コンストラクタにようてパターン分けをする
        mono の場合はfmapの定義により同じ項に変形されるために relf で証明できる。
        delta の場合、delta の 第一引数は mono の時のように同じ項に変形できる。
        しかし第二引数は fmap の定義により \verb/delta-fmap d id/ に変形される。
        見掛け上は等式の左辺と変わらないように見えるが、先頭1つめを除いているため、引数で受けたバージョンよりも1つだけ値が下がっている。
        よって最終的にバージョン1である mono になるまで再帰的に delta-preserve-id 関数を用いて変形した後に cong によって先頭1つめを適用し続けることで証明ができる。

    \item fmap は関数の合成を保存する

        リスト\ref{src:delta_covariant}に証明を示す。

        \begin{table}[html]
            \lstinputlisting[label=src:delta_covariant, caption= Delta における fmap も関数の合成を保存する証明] {src/delta_covariant.agda.replaced}
        \end{table}

        id の保存のように、コンストラクタによるパターンマッチを行なう。
        バージョンが1の場合は同じものに簡約され、1より大きい場合は再帰的に変形することで証明できる。
\end{itemize}

Delta と fmap と2つの証明を用いて Functor record を構成する(リスト\ref{src:delta_is_functor})。


\begin{table}[html]
    \lstinputlisting[label=src:delta_is_functor, caption= Delta が Functor則を満たすことの証明] {src/delta_is_functor.agda.replaced}
\end{table}

record が正しく構成できたため、Delta は Functor 則を満たす。
Agda ではこのように法則とデータの関連付けを行なう。

% }}}

% {{{ Agda における Monad 則

\section{Agda における Monad 則}
\label{section:monad_laws_in_agda}
\ref{section:functor_in_agda}節と\ref{section:delta_is_functor}節では Delta が Functor 則を満たすことの証明を行なった。
\ref{section:monad_laws_in_agda}節では同じように Monad 則の定義を行ない、\ref{section:delta_is_monad}節で証明を行なう。

まずは Monad則の定義を行なう(リスト\ref{src:monad_laws_in_agda})。

\begin{table}[html]
    \lstinputlisting[label=src:monad_laws_in_agda, caption= AgdaにおけるMonad則の定義] {src/monad_laws.agda.replaced}
\end{table}

Monad 則とは $ triple(T, \eta, \mu) $ に対して課すべき制約であった。
そのためまず要素として $ T $ , $ \eta $, $ \mu $ が存在する。
T は Set l を取り Set l を返す型であり、Functor則を満たす。
$ \eta $ は T を増やす関数であり、 $ \mu $ は T を減らす関数である。
これら Monad の構成要素を定義する field である。

次に、$ \eta $ と $ \mu $ は natural transformation である必要がある。
よって field に制約として $ \eta $ と $ \mu $ の natural transformation を定義する。
なお、 field という予約語は複数書いても2つ目以降は無いものとして振る舞う。

ここで、 \verb/ fmap F / という項に注目して欲しい。
値F は Functor T 型を持ち、fmap や2つの証明を内包する。
fmap や証明へのアクセスは \verb/ field-name record-value / と記述する。
例えば、リスト\ref{src:delta_is_functor}で定義した Functor Delta の型を持つ値 \verb/delta-is-functor/ に対して \verb/ fmap delta-is-functor/ とすると関数 delta-fmap が得られる。
つまり、\verb/fmap F f/ とするのは Functor則が証明された F の fmap に関数fを適用することとなる。

最後に $ triple (T, \eta, \mu) $ に対する Monad 則に相当する等式を記述する。
Monad則は可換図として与えられたTに対する演算の可換性と、Tに対する演算の単位元を強制するものであった。
Tに対する演算の可換性は association-law として、単位元の強制は unity-law として記述できる。
unity-law はTに対する演算が右側と左側の二種類があるため、 right-unity-law と left-unity-law に分割した。

これら全ての field を満たすような証明を記述できれば、 $ triple (T, \eta, \mu) $ は Monad であると言える。

% }}}

% {{{ Delta が Monad 則を満たす証明

\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 の値によりバージョン数を決められるようにしておく。
なお、パターンマッチの項に存在する \verb/{}/ は、 implicit な値のパターンマッチに用いられる。
例えば \verb/{n = S x}/ とすれば、 implicit な値 n は S により構成される時にこの定義が実行され、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 以上であれば再帰的に証明することができる。


        \lstinputlisting[label=src:delta_eta_is_nt_in_agda,
                        caption= Agda における Delta の $ \eta$ が natural transformation である証明]
                        {src/delta_eta_is_nt.agda.replaced}
    \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}

\newpage

    \item T に対する演算の単位元が存在する

        図\ref{fig:monad_laws}で示した右側の可換図に相当する。
        単位元に相当する演算は右側と左側の2つが存在するため、証明も2つに分割する。

        右側単位元の証明をリスト\ref{src:delta_right_unity_law}に示す。

    \lstinputlisting[basicstyle={\scriptsize},
                     numberstyle={\tiny},
                     label=src:delta_right_unity_law,
                     caption= Agda における Delta に対する演算に右側単位元が存在する証明]
                     {src/delta_right_unity_law.agda.replaced}

        バージョンが1である時は同じ項となるため refl となる。
        バージョンが1以上である時は再帰的に定義することになるが、途中で $ \eta $ が natural transformation である性質を利用している。

        次に左側単位元の証明をリスト\ref{src:delta_left_unity_law}に示す。

\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}

        これまでの証明と同様にバージョンが1である場合は定義から同じ項となる。
        バージョンが1以上の場合、Functor則の関数の合成の保存を利用して証明を再帰的に行なう。

    \item T に対する演算の可換性が存在する

        図\ref{fig:monad_laws}で示した左側の可換図に相当する。
        演算の可換性の証明をリスト\ref{src:delta_association_law}に示す。

\begin{table}[html]
    \lstinputlisting[basicstyle={\scriptsize},
                     numberstyle={\tiny},
                     label=src:delta_association_law,
                     caption= Agda における Delta に対する演算に可換性が存在する証明]
                     {src/delta_association_law.agda.replaced}
\end{table}

        $ \mu $ を用いて TTT から T にする際に、右側2つのTに対して先に $ \mu $ を用いるか、左側2つから先に用いるかの可換性である。
        よって \verb/Delta (Delta (Delta A))/から \verb/Delta A/ とする演算の等式となる。

        バージョンが1である場合はやはり同じ項に簡約される。
        しかしバージョンが1以上である場合は複雑な式変形を行なう。

        パターンマッチにより最も外側の Delta は分解されるため、バージョンが1下がる。
        しかし内側の Delta 2つはバージョンが異なるため、外側2つの Delta のバージョンが異なってしまい $ \mu $ が適用できない。
        よって \verb/delta-fmap-mu-to-tail/ として部分的な等式を証明してから可換性を証明する。
        \verb/delta-fmap-mu-to-tail/ では Delta のバージョンが \verb/Delta (Delta (Delta A (S (S m))) (S (S m))) (S n)/ となっていることに注目してもらいたい。

        \verb/delta-fmap-mu-to-tail/ に加え、 $ \mu $ が natural transformation であることを利用して再帰的に定義することで証明ができる。

\end{enumerate}


Delta Monad の定義と、5つの証明を用いて Moand の record が構築できることを確認する(リスト\ref{src:delta_is_monad})。

\begin{table}[html]
    \lstinputlisting[label=src:delta_is_monad, caption= Agda における Delta が Monad 則を満たす証明] {src/delta_is_monad.agda.replaced}
\end{table}

全ての Delta が同じバージョンを持つ時、 $ triple(T, \eta, \mu) $ は Monad則を満たすことを示せた。

% }}}