Mercurial > hg > Papers > 2015 > atton-thesis
view proof_delta.tex @ 42:4cc65012412f
Add proofs of functor-laws on delta
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 13 Feb 2015 17:13:23 +0900 |
parents | 8fc2ac1f901f |
children | b7e693b6d7d9 |
line wrap: on
line source
\chapter{Delta Monad が Monad である証明} \label{chapter:proof_delta} 第\ref{chapter:agda}章では Agda における証明手法について述べた。 第\ref{chapter:proof_delta}章では Agda を用いて Delta Monad が Monad であることを証明していく。 証明のゴールは Delta Monad が Funcor 則と Monad 則を満たすことの証明である。 % {{{ 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 がある性質を満たすことを証明する。 record Funcor は 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 record を構成する] {src/delta_is_functor.agda.replaced} \end{table} record が正しく構成できたため、Delta は Functor 則を満たす。 Agda ではこのように法則とデータの関連付けを行なう。 % }}} \section{Agda における Monad 則} \section{Delta が Monad 則を満たす証明}