Mercurial > hg > Papers > 2015 > atton-thesis

annotate proof_delta.tex @ 40:470d99799398

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add description functor record
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 13 Feb 2015 11:31:46 +0900
parents
children 8fc2ac1f901f
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
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 % {{{ Agda における Functor 則
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 \section{Agda における Functor 則}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 \label{section:functor_in_agda}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 Agda における Functor 則はリスト \ref{src:record_functor} のように記述した。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 \begin{table}[html]
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 \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
15 \end{table}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 Agda ではある性質を持つデータは record 構文によって記述する。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 record の値は record の定義時に要請した field を全て満たすことで構築される。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 よって、あるデータAが持つべき性質は field に定義し、A を用いた証明によって field を満たす。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 field を満たすことにより record が構成できることで A がある性質を満たすことを証明する。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 record Funcor は implicit な値 level と、型引数を持つ関数 F を持つ。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 level とは型のlevelの区別に用いられるものである。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 Agda では型も値として扱えるため、同じ式において型と値が混同することがある。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 厳密に型と値を区別したい場合、level を定義することで区別する。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 levelは任意の level と、関数 suc により定義される。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 関数 suc は level を一つ上昇させる関数である。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 level l を適用した型を用いる時は Set l と記述する。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 record Functor が取る F は Set l を取り Set l を取る関数である。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 Set l が証明の対象となるプログラムであるため、関数F はプログラムのlevel で表現する。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 よって、プログラムの level l を取り、プログラムの level l の Set を返すようにする。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 それに対し、 F に対する証明となる record Functor は、証明の対象とするプログラムそのものではない。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 よって suc により level を一段上げる。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 これは、証明の対象となるプログラムと証明そのものを混同しないためである。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 record Functor の field には以下のようなものがある。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 \begin{itemize}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 \item fmap
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 Functor に要請される、category から category への map 関数である。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 型の定義はほとんど Haskell と同じである。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 fmap は任意の型に対して適用可能でなくてはいけないため、map する対象の型Aと map される対象の型Bは implicit である。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 \item preserve-id
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 Functor則の id の保存である。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 型F A を持つ値x に対するfmap id と id の等価性がなくてはならない。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 \item covariant
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 Functor則における関数の合成の保存である。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 関数fとgを合成してから fmap により mapping しても、 f と g を個別に mapping してから合成しても等価性を持たなくてはならない。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 \item fmap-equiv
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 ある型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
59 これは本来はFunctor則には存在しない。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 Agda において Monad の証明に必要であったために追加した。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 \end{itemize}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 % }}}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 \section{Delta が Functor 則を満たす証明}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 \label{section:delta_is_functor}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 \ref{section:functor_in_agda}節では Agda における Functor則の表現について述べた。
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 \ref{section:delta_is_functor}節では
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 \section{Agda における Monad 則}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 \section{Delta が Monad 則を満たす証明}