Mercurial > hg > Papers > 2015 > atton-thesis
comparison agda.tex @ 23:61e5659e04a9
Add description for natural deduction
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 09 Feb 2015 22:13:18 +0900 |
parents | |
children | 13affa3e65a2 |
comparison
equal
deleted
inserted
replaced
22:fc44782929a7 | 23:61e5659e04a9 |
---|---|
1 \chapter{Agda による証明手法} | |
2 \label{chapter:agda} | |
3 第\ref{chapter:category}章においては functor, natural transformation, monad の定義と functional programming における対応について述べた。 | |
4 その中で、 Functor 則や Monad 則といった満たすべき性質がいくつか存在した。 | |
5 functional programming において、あるデータ型やそれに対応する計算が Functor 則を満たすことを保証することは言語の実装に依存していい。 | |
6 例えば、 Haskell において functor は型クラスによって提供されるため、型レベルのチェックに留まっている。 | |
7 そのため、型チェックは通るが Functor 則を満たさない functor が定義可能となってしまう。 | |
8 | |
9 そこで、証明支援系言語 Agda を用いて、 Delta が Functor 則と Monad 則を満たすことを証明することとする。 | |
10 そのためにまずは Agda における証明手法について述べる。 | |
11 | |
12 % {{{ Natural Deduction | |
13 | |
14 \section{Natural Deduction} | |
15 \label{section:natural_deduction} | |
16 証明には natural deduction(自然演繹)を用いる。 | |
17 natural deduction は Gentzen によって作られた論理と、その証明システムである。 | |
18 命題変数と記号を用いた論理式で論理を記述し、推論規則により変形することで求める論理式を導く。 | |
19 | |
20 natural deduction において | |
21 | |
22 \begin{eqnarray} | |
23 \vdots \\ \nonumber | |
24 A \\ \nonumber | |
25 \end{eqnarray} | |
26 | |
27 と書いた時、最終的に命題Aを証明したことを意味する。 | |
28 証明は木構造で表わされ、葉の命題は仮定となる。 | |
29 仮定には dead か alive の2つの状態が存在する。 | |
30 | |
31 \begin{eqnarray} | |
32 \label{exp:a_implies_b} | |
33 A \\ \nonumber | |
34 \vdots \\ \nonumber | |
35 B \\ \nonumber | |
36 \end{eqnarray} | |
37 | |
38 式\ref{exp:a_implies_b}のように A を仮定して B を導くことができたとする。 | |
39 この時 A は alive な仮定である。 | |
40 証明された B は A の仮定に依存していることを意味する。 | |
41 | |
42 ここで、推論規則により記号 $ \Rightarrow $ を導入する。 | |
43 | |
44 \begin{prooftree} | |
45 \AxiomC{[$ A $]} | |
46 \noLine | |
47 \UnaryInfC{ $ \vdots $} | |
48 \noLine | |
49 \UnaryInfC{ $ B $ } | |
50 \RightLabel{ $ \Rightarrow \mathcal{I} $} | |
51 \UnaryInfC{$ A \Rightarrow B $} | |
52 \end{prooftree} | |
53 | |
54 そうすると、仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。 | |
55 A という仮定に依存して B を導く証明から、A が存在すれば B が存在するという証明を導いたこととなる。 | |
56 このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導くことができる。 | |
57 | |
58 alive な仮定を dead にすることができるのは $ \Rightarrow I $ 規則のみである。 | |
59 それを踏まえ、 natural deduction には以下のような規則が存在する。 | |
60 | |
61 \begin{itemize} | |
62 \item Hypothesis | |
63 | |
64 仮定。葉にある式が仮定となるため、論理式A を仮定する場合に以下のように書く。 | |
65 | |
66 $ A $ | |
67 | |
68 \item Introductions | |
69 | |
70 導入。証明された論理式に対して記号を導入することで新たな証明を導く。 | |
71 | |
72 | |
73 \begin{prooftree} | |
74 \AxiomC{ $ \vdots $} | |
75 \noLine | |
76 \UnaryInfC{ $ A $ } | |
77 \AxiomC{ $ \vdots $} | |
78 \noLine | |
79 \UnaryInfC{ $ B $ } | |
80 \RightLabel{ $ \land \mathcal{I} $} | |
81 \BinaryInfC{$ A \land B $} | |
82 \end{prooftree} | |
83 | |
84 \begin{prooftree} | |
85 \AxiomC{ $ \vdots $} | |
86 \noLine | |
87 \UnaryInfC{ $ A $ } | |
88 \RightLabel{ $ \lor 1 \mathcal{I} $} | |
89 \UnaryInfC{$ A \lor B $} | |
90 \end{prooftree} | |
91 | |
92 \begin{prooftree} | |
93 \AxiomC{ $ \vdots $} | |
94 \noLine | |
95 \UnaryInfC{ $ B $ } | |
96 \RightLabel{ $ \lor 2 \mathcal{I} $} | |
97 \UnaryInfC{$ A \lor B $} | |
98 \end{prooftree} | |
99 | |
100 \begin{prooftree} | |
101 \AxiomC{[$ A $]} | |
102 \noLine | |
103 \UnaryInfC{ $ \vdots $} | |
104 \noLine | |
105 \UnaryInfC{ $ B $ } | |
106 \RightLabel{ $ \Rightarrow \mathcal{I} $} | |
107 \UnaryInfC{$ A \Rightarrow B $} | |
108 \end{prooftree} | |
109 | |
110 \item Eliminations | |
111 | |
112 除去。ある論理記号で構成された証明から別の証明を導く。 | |
113 | |
114 \begin{prooftree} | |
115 \AxiomC{ $ \vdots $} | |
116 \noLine | |
117 \UnaryInfC{ $ A \land B $ } | |
118 \RightLabel{ $ \land 1 \mathcal{E} $} | |
119 \UnaryInfC{$ A $} | |
120 \end{prooftree} | |
121 | |
122 \begin{prooftree} | |
123 \AxiomC{ $ \vdots $} | |
124 \noLine | |
125 \UnaryInfC{ $ A \land B $ } | |
126 \RightLabel{ $ \land 2 \mathcal{E} $} | |
127 \UnaryInfC{$ B $} | |
128 \end{prooftree} | |
129 | |
130 \begin{prooftree} | |
131 \AxiomC{ $ \vdots $} | |
132 \noLine | |
133 \UnaryInfC{ $ A \lor B $ } | |
134 | |
135 \AxiomC{[$A$]} | |
136 \noLine | |
137 \UnaryInfC{ $ \vdots $} | |
138 \noLine | |
139 \UnaryInfC{ $ C $ } | |
140 | |
141 \AxiomC{[$B$]} | |
142 \noLine | |
143 \UnaryInfC{ $ \vdots $} | |
144 \noLine | |
145 \UnaryInfC{ $ C $ } | |
146 | |
147 \RightLabel{ $ \lor \mathcal{E} $} | |
148 \TrinaryInfC{ $ C $ } | |
149 \end{prooftree} | |
150 | |
151 \begin{prooftree} | |
152 \AxiomC{ $ \vdots $} | |
153 \noLine | |
154 \UnaryInfC{ $ A $ } | |
155 | |
156 \AxiomC{ $ \vdots $} | |
157 \noLine | |
158 \UnaryInfC{ $ A \Rightarrow B $ } | |
159 | |
160 \RightLabel{ $ \Rightarrow \mathcal{E} $} | |
161 \BinaryInfC{$ B $} | |
162 \end{prooftree} | |
163 | |
164 \end{itemize} | |
165 | |
166 記号 $ \lor, \land, \Rightarrow $ の導入の除去規則について述べた。 | |
167 natural deduction には他にも $ \forall, \exists, \bot $ といった記号が存在するが、ここでは解説を省略する。 | |
168 | |
169 それぞれの記号は以下のような意味を持つ | |
170 \begin{itemize} | |
171 \item $ \land $ | |
172 conjunction。2つの命題が成り立つことを示す。 | |
173 $ A \land B $ と記述すると A かつ B と考えることができる。 | |
174 | |
175 \item $ \lor $ | |
176 disjunction。2つの命題のうちどちらかが成り立つことを示す。 | |
177 $ A \lor B $ と記述すると A または B と考えることができる。 | |
178 | |
179 \item $ \Rightarrow $ | |
180 implication。左側の命題が成り立つ時、右側の命題が成り立つことを示す。 | |
181 $ A \Rightarrow B $ と記述すると A ならば B と考えることができる。 | |
182 \end{itemize} | |
183 | |
184 例として、natural deduction で三段論法を証明する。 | |
185 なお、三段論法とは「A は B であり、 B は C である。よって A は C である」といった文を示すこととする。 | |
186 | |
187 \begin{prooftree} | |
188 \AxiomC{ $ [A] $ $_{(1)}$} | |
189 \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } | |
190 \RightLabel{ $ \land 1 \mathcal{E} $ } | |
191 \UnaryInfC{ $ (A \Rightarrow B) $ } | |
192 \BinaryInfC{ $ B $ } | |
193 | |
194 \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } | |
195 \RightLabel{ $ \land 2 \mathcal{E} $ } | |
196 \UnaryInfC{ $ (B \Rightarrow C) $ } | |
197 | |
198 \BinaryInfC{ $ C $ } | |
199 \RightLabel{ $ \Rightarrow \mathcal{I} _{(1)}$} | |
200 \UnaryInfC{ $ A \Rightarrow C $} | |
201 \RightLabel{ $ \Rightarrow \mathcal{I} _{(2)}$} | |
202 \UnaryInfC{ $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $} | |
203 \end{prooftree} | |
204 | |
205 まず、三段論法を論理式で表す。 | |
206 | |
207 「A は B であり、 B は C である。よって A は C である」 が証明するべき命題である。 | |
208 まず、「A は B であり」から、Aから性質Bが導けることが分かる。これが $ A \Rightarrow B $ となる。 | |
209 次に、「B は C である」から、Bから性質Cが導けることが分かる。これが $ B \Rightarrow C $ となる。 | |
210 そしてこの2つは同時に成り立つ。 | |
211 よって $ (A \Rightarrow B) \land (B \Rightarrow C)$ が前提となる。 | |
212 この条件2つが成り立つ時に「Aは Cである」が成りたつ。 | |
213 条件と同じように「A は C である」は、 $ A \Rightarrow C $ と書けるため、証明するべき論理式は $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ になる。 | |
214 | |
215 証明の手順はこうである。 | |
216 まず条件$ (A \Rightarrow B) \land (B \Rightarrow C)$とAを2つ仮定する。 | |
217 条件を $ \land 1 \mathcal{E} $ $ \land 2 \mathcal{E} $ により分解する。 | |
218 A と $ A \Rightarrow B$ から B を、 B から $ B \Rightarrow C $ から C を導く。 | |
219 ここで $ \Rightarrow \mathcal{I} $ により $ A \Rightarrow C $ を導く。 | |
220 この際に dead にする仮定は A である。 | |
221 そのために $_{(1)} $ と対応する \verb/[]/の記号に数値を付けてある。 | |
222 これで残る仮定は $ (A \Rightarrow B) \land (B \Rightarrow C)$ となり、これから $ A \Rightarrow C $ を導くことができたためにさらに $ \Rightarrow \mathcal{I} $ を適用する。 | |
223 結果、証明すべき論理式$ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ が導けたために証明終了となる。 | |
224 | |
225 % }}} | |
226 | |
227 \section{Curry-Howard Isomorphism} | |
228 \section{Agda による証明} | |
229 \section{Reasoning} | |
230 |