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