Mercurial > hg > Papers > 2015 > atton-thesis

annotate proof_delta.tex @ 42:4cc65012412f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
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
42
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
102 % {{{ Delta が Functor 則を満たす証明
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
103
40
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 \section{Delta が Functor 則を満たす証明}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 \label{section:delta_is_functor}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 \ref{section:functor_in_agda}節では Agda における Functor則の表現について述べた。
42
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
107 \ref{section:delta_is_functor}節では \ref{section:delta_in_agda}節の Delta Monad の定義を用いてFunctor則を証明していく。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
108
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
109 まず、Agdaにおける delta に対する fmap の定義を示す(リスト\ref{src:delta_fmap_in_agda})。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
110
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
111 \begin{table}[html]
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
112 \lstinputlisting[label=src:delta_fmap_in_agda, caption= Agda における Delta に対する fmap の定義] {src/delta_fmap.agda}
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
113 \end{table}
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
114
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
115 バージョンが1以上の Delta について fmap を定義する。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
116 関数 f は型 A から B への関数とし、 Delta A から Delta B への関数に mapping する。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
117 コンストラクタ2つのパターンマッチを使って再帰的に f を delta の内部の値への適応することで fmap を行なう。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
118
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
119 データ型Delta と関数fmap を定義できたので、これらが Functor 則を満たすか証明していく。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
120 なお、今回 Delta は全ての場合においてバージョンを1以上持つものとする。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
121 その制約は引数の Delta のバージョンに必ず S を付けることで1以下の値を受けつけないようにすることで行なう。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
122
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
123
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
124 \begin{itemize}
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
125 \item fmap は id を保存する
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
126
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
127 リスト\ref{src:delta_preserve_id}に証明を示す。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
128
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
129 \begin{table}[html]
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
130 \lstinputlisting[label=src:delta_preserve_id, caption= Delta における fmap も id を保存する] {src/delta_preserve_id.agda.replaced}
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
131 \end{table}
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
132
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
133
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
134 コンストラクタにようてパターン分けをする
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
135 mono の場合はfmapの定義により同じ項に変形されるために relf で証明できる。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
136 delta の場合、delta の 第一引数は mono の時のように同じ項に変形できる。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
137 しかし第二引数は fmap の定義により \verb/delta-fmap d id/ に変形される。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
138 見掛け上は等式の左辺と変わらないように見えるが、先頭1つめを除いているため、引数で受けたバージョンよりも1値が下がっている。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
139 よって最終的にバージョン1である mono になるまで再帰的に delta-preserve-id 関数を用いて変形した後に cong によって先頭1つめを適用し続けることで証明ができる。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
140
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
141 \item fmap は関数の合成を保存する
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
142
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
143 リスト\ref{src:delta_covariant}に証明を示す。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
144
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
145 \begin{table}[html]
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
146 \lstinputlisting[label=src:delta_covariant, caption= Delta における fmap も関数の合成を保存する] {src/delta_covariant.agda.replaced}
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
147 \end{table}
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
148
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
149 id の保存のように、コンストラクタによるパターンマッチを行なう。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
150 バージョンが1の場合は同じものに簡約され、1より大きい場合は再帰的に変形することで証明できる。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
151 \end{itemize}
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
152
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
153 Delta と fmap と2つの証明を用いて Functor record を構成する(リスト\ref{src:delta_is_functor})。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
154
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
155
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
156 \begin{table}[html]
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
157 \lstinputlisting[label=src:delta_is_functor, caption= Delta の定義と証明から Functor record を構成する] {src/delta_is_functor.agda.replaced}
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
158 \end{table}
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
159
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
160 record が正しく構成できたため、Delta は Functor 則を満たす。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
161 Agda ではこのように法則とデータの関連付けを行なう。
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
162
4cc65012412f Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
163 % }}}
40
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
164
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
165 \section{Agda における Monad 則}
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
166 \section{Delta が Monad 則を満たす証明}