Mercurial > hg > Papers > 2015 > atton-thesis

annotate 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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
40
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 \chapter{Delta Monad が Monad である証明}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 \label{chapter:proof_delta}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 第\ref{chapter:agda}章では Agda における証明手法について述べた。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 第\ref{chapter:proof_delta}章では Agda を用いて Delta Monad が Monad であることを証明していく。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 証明のゴールは Delta Monad が Funcor 則と Monad 則を満たすことの証明である。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
41
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
7 % {{{ Agda における Delta Monad の表現
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
8
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
9 \section{Agda における Delta Monad の表現}
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
10 \label{section:delta_in_agda}
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
11 \ref{section:delta_in_agda}節では Agda において Delta Monad を再定義する。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
12 Agda は Haskell において実装されているため、ほとんど同様に定義できる(リスト\ref{src:delta_in_agda})。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
13
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
14 \begin{table}[html]
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
15 \lstinputlisting[label=src:delta_in_agda, caption=Agdaにおける Delta Monad のデータ定義] {src/delta.agda.replaced}
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
16 \end{table}
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
17
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
18 data型 Delta は型A の値と Nat を持つ。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
19
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
20 level とは型のlevelの区別に用いられるものである。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
21 Agda では型も値として扱えるため、同じ式において型と値が混同することがある。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
22 厳密に型と値を区別したい場合、level を定義することで区別する。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
23 levelは任意の level と、関数 suc により定義される。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
24 関数 suc は level を一つ上昇させる関数である。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
25 level l を適用した型を用いる時は Set l と記述する。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
26 今回は証明する対象のプログラムは Set l の level とし、それ以外は Set (suc l) の level とする。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
27
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
28 Nat は自然数であり、プログラムのバージョンに対応する。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
29 自然数の定義は\ref{section:reasoning} 節にあるリスト \ref{src:nat}にならうものとする。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
30
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
31 data 型 Delta は2つのコンストラクタにより構成される。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
32
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
33 \begin{itemize}
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
34 \item mono
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
35
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
36 プログラムの最初の変更単位を受けとり、バージョン1とする。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
37 型Aを取り、バージョンが1のDeltaを構成することでその表現とする。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
38
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
39 \item delta
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
40
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
41 変更単位と変更単位の列を受けとり、変更単位を追加する。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
42 これは変更によるバージョンアップに相当する。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
43 よって任意の1以上のバージョンを持つ Delta に変更単位を加えることでバージョンを1上昇させる。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
44 \end{itemize}
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
45
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
46 Agda においてもデータ型 Delta が定義できた。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
47 これからこの定義を用いて Functor則と Monad 則を証明していく。
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
48
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
49 % }}}
8fc2ac1f901f Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
50
40
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 % {{{ Agda における Functor 則
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 \section{Agda における Functor 則}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 \label{section:functor_in_agda}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 Agda における Functor 則はリスト \ref{src:record_functor} のように記述した。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 \begin{table}[html]
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 \lstinputlisting[label=src:record_functor, caption=Agdaにおける Functor則の定義] {src/record_functor.agda.replaced}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 \end{table}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 Agda ではある性質を持つデータは record 構文によって記述する。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 record の値は record の定義時に要請した field を全て満たすことで構築される。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 よって、あるデータAが持つべき性質は field に定義し、A を用いた証明によって field を満たす。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 field を満たすことにより record が構成できることで A がある性質を満たすことを証明する。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 record Funcor は implicit な値 level と、型引数を持つ関数 F を持つ。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 record Functor が取る F は Set l を取り Set l を取る関数である。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 Set l が証明の対象となるプログラムであるため、関数F はプログラムのlevel で表現する。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 よって、プログラムの level l を取り、プログラムの level l の Set を返すようにする。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 それに対し、 F に対する証明となる record Functor は、証明の対象とするプログラムそのものではない。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 よって suc により level を一段上げる。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 これは、証明の対象となるプログラムと証明そのものを混同しないためである。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 record Functor の field には以下のようなものがある。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 \begin{itemize}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 \item fmap
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 Functor に要請される、category から category への map 関数である。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 型の定義はほとんど Haskell と同じである。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 fmap は任意の型に対して適用可能でなくてはいけないため、map する対象の型Aと map される対象の型Bは implicit である。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 \item preserve-id
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 Functor則の id の保存である。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 型F A を持つ値x に対するfmap id と id の等価性がなくてはならない。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 \item covariant
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 Functor則における関数の合成の保存である。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 関数fとgを合成してから fmap により mapping しても、 f と g を個別に mapping してから合成しても等価性を持たなくてはならない。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 \item fmap-equiv
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 ある型A の値x に対して等価である関数f と g を考えた時、 型F A の値 fx の対し、 fmap f としても fmap gとしても等価であることを保証する。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 これは本来はFunctor則には存在しない。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 Agda において Monad の証明に必要であったために追加した。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 \end{itemize}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 % }}}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 \section{Delta が Functor 則を満たす証明}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 \label{section:delta_is_functor}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 \ref{section:functor_in_agda}節では Agda における Functor則の表現について述べた。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 \ref{section:delta_is_functor}節では
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 \section{Agda における Monad 則}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 \section{Delta が Monad 則を満たす証明}