Mercurial > hg > Papers > 2015 > atton-thesis

comparison proof_delta.tex @ 41:8fc2ac1f901f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add delta definition in agda
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 13 Feb 2015 11:48:40 +0900
parents 470d99799398
children 4cc65012412f
comparison
equal deleted inserted replaced
40:470d99799398 41:8fc2ac1f901f
1 \chapter{Delta Monad が Monad である証明} 1 \chapter{Delta Monad が Monad である証明}
2 \label{chapter:proof_delta} 2 \label{chapter:proof_delta}
3 第\ref{chapter:agda}章では Agda における証明手法について述べた。 3 第\ref{chapter:agda}章では Agda における証明手法について述べた。
4 第\ref{chapter:proof_delta}章では Agda を用いて Delta Monad が Monad であることを証明していく。 4 第\ref{chapter:proof_delta}章では Agda を用いて Delta Monad が Monad であることを証明していく。
5 証明のゴールは Delta Monad が Funcor 則と Monad 則を満たすことの証明である。 5 証明のゴールは Delta Monad が Funcor 則と Monad 則を満たすことの証明である。
6
7 % {{{ Agda における Delta Monad の表現
8
9 \section{Agda における Delta Monad の表現}
10 \label{section:delta_in_agda}
11 \ref{section:delta_in_agda}節では Agda において Delta Monad を再定義する。
12 Agda は Haskell において実装されているため、ほとんど同様に定義できる(リスト\ref{src:delta_in_agda})。
13
14 \begin{table}[html]
15 \lstinputlisting[label=src:delta_in_agda, caption=Agdaにおける Delta Monad のデータ定義] {src/delta.agda.replaced}
16 \end{table}
17
18 data型 Delta は型A の値と Nat を持つ。
19
20 level とは型のlevelの区別に用いられるものである。
21 Agda では型も値として扱えるため、同じ式において型と値が混同することがある。
22 厳密に型と値を区別したい場合、level を定義することで区別する。
23 levelは任意の level と、関数 suc により定義される。
24 関数 suc は level を一つ上昇させる関数である。
25 level l を適用した型を用いる時は Set l と記述する。
26 今回は証明する対象のプログラムは Set l の level とし、それ以外は Set (suc l) の level とする。
27
28 Nat は自然数であり、プログラムのバージョンに対応する。
29 自然数の定義は\ref{section:reasoning} 節にあるリスト \ref{src:nat}にならうものとする。
30
31 data 型 Delta は2つのコンストラクタにより構成される。
32
33 \begin{itemize}
34 \item mono
35
36 プログラムの最初の変更単位を受けとり、バージョン1とする。
37 型Aを取り、バージョンが1のDeltaを構成することでその表現とする。
38
39 \item delta
40
41 変更単位と変更単位の列を受けとり、変更単位を追加する。
42 これは変更によるバージョンアップに相当する。
43 よって任意の1以上のバージョンを持つ Delta に変更単位を加えることでバージョンを1上昇させる。
44 \end{itemize}
45
46 Agda においてもデータ型 Delta が定義できた。
47 これからこの定義を用いて Functor則と Monad 則を証明していく。
48
49 % }}}
6 50
7 % {{{ Agda における Functor 則 51 % {{{ Agda における Functor 則
8 52
9 \section{Agda における Functor 則} 53 \section{Agda における Functor 則}
10 \label{section:functor_in_agda} 54 \label{section:functor_in_agda}
18 record の値は record の定義時に要請した field を全て満たすことで構築される。 62 record の値は record の定義時に要請した field を全て満たすことで構築される。
19 よって、あるデータAが持つべき性質は field に定義し、A を用いた証明によって field を満たす。 63 よって、あるデータAが持つべき性質は field に定義し、A を用いた証明によって field を満たす。
20 field を満たすことにより record が構成できることで A がある性質を満たすことを証明する。 64 field を満たすことにより record が構成できることで A がある性質を満たすことを証明する。
21 65
22 record Funcor は implicit な値 level と、型引数を持つ関数 F を持つ。 66 record Funcor は implicit な値 level と、型引数を持つ関数 F を持つ。
23 level とは型のlevelの区別に用いられるものである。
24 Agda では型も値として扱えるため、同じ式において型と値が混同することがある。
25 厳密に型と値を区別したい場合、level を定義することで区別する。
26 levelは任意の level と、関数 suc により定義される。
27 関数 suc は level を一つ上昇させる関数である。
28 level l を適用した型を用いる時は Set l と記述する。
29
30 record Functor が取る F は Set l を取り Set l を取る関数である。 67 record Functor が取る F は Set l を取り Set l を取る関数である。
31 Set l が証明の対象となるプログラムであるため、関数F はプログラムのlevel で表現する。 68 Set l が証明の対象となるプログラムであるため、関数F はプログラムのlevel で表現する。
32 よって、プログラムの level l を取り、プログラムの level l の Set を返すようにする。 69 よって、プログラムの level l を取り、プログラムの level l の Set を返すようにする。
33 それに対し、 F に対する証明となる record Functor は、証明の対象とするプログラムそのものではない。 70 それに対し、 F に対する証明となる record Functor は、証明の対象とするプログラムそのものではない。
34 よって suc により level を一段上げる。 71 よって suc により level を一段上げる。