Mercurial > hg > Papers > 2015 > atton-thesis

comparison paper/agda.tex @ 77:ce7701e4a308

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mini fixes
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 18 Feb 2015 11:10:19 +0900
parents 1181b4facaf9
children 6f699b37dc55
comparison
equal deleted inserted replaced
76:3562c274db60 77:ce7701e4a308
35 \vdots \\ \nonumber 35 \vdots \\ \nonumber
36 B \\ \nonumber 36 B \\ \nonumber
37 \end{eqnarray} 37 \end{eqnarray}
38 38
39 式\ref{exp:a_implies_b}のように A を仮定して B を導くことができたとする。 39 式\ref{exp:a_implies_b}のように A を仮定して B を導くことができたとする。
40 この時 A は alive な仮定である。 40 この時 A は alive な仮定であり、証明された B は A の仮定に依存していることを意味する。
41 証明された B は A の仮定に依存していることを意味する。
42 41
43 ここで、推論規則により記号 $ \Rightarrow $ を導入する。 42 ここで、推論規則により記号 $ \Rightarrow $ を導入する。
44 43
45 \begin{prooftree} 44 \begin{prooftree}
46 \AxiomC{[$ A $]} 45 \AxiomC{[$ A $]}
50 \UnaryInfC{ $ B $ } 49 \UnaryInfC{ $ B $ }
51 \RightLabel{ $ \Rightarrow \mathcal{I} $} 50 \RightLabel{ $ \Rightarrow \mathcal{I} $}
52 \UnaryInfC{$ A \Rightarrow B $} 51 \UnaryInfC{$ A \Rightarrow B $}
53 \end{prooftree} 52 \end{prooftree}
54 53
55 そうすると、仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。 54 $ \Rightarrow \mathcal{I} $ を適用することで仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。
56 A という仮定に依存して B を導く証明から、「A が存在すれば B が存在する」という証明を導いたこととなる。 55 A という仮定に依存して B を導く証明から、「A が存在すれば B が存在する」という証明を導いたこととなる。
57 このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導くことができる。 56 このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導ける。
58 なお、dead な仮定は \verb/[A]/ のように \verb/[]/ で囲んで書く。 57 なお、dead な仮定は \verb/[A]/ のように \verb/[]/ で囲んで書く。
59 58
60 alive な仮定を dead にすることができるのは $ \Rightarrow \mathcal{I} $ 規則のみである。 59 alive な仮定を dead にすることができるのは $ \Rightarrow \mathcal{I} $ 規則のみである。
61 それを踏まえ、 natural deduction には以下のような規則が存在する。 60 それを踏まえ、 natural deduction には以下のような規則が存在する。
62 61
182 implication。左側の命題が成り立つ時、右側の命題が成り立つことを示す。 181 implication。左側の命題が成り立つ時、右側の命題が成り立つことを示す。
183 $ A \Rightarrow B $ と記述すると A ならば B と考えることができる。 182 $ A \Rightarrow B $ と記述すると A ならば B と考えることができる。
184 \end{itemize} 183 \end{itemize}
185 184
186 例として、natural deduction で三段論法を証明する。 185 例として、natural deduction で三段論法を証明する。
187 なお、三段論法とは「A は B であり、 B は C である。よって A は C である」といった文を示すこととする。 186 なお、三段論法とは「A は B であり、 B は C である。よって A は C である」といった文を示す。
188 187
189 \begin{prooftree} 188 \begin{prooftree}
190 \AxiomC{ $ [A] $ $_{(1)}$} 189 \AxiomC{ $ [A] $ $_{(1)}$}
191 \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } 190 \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ }
192 \RightLabel{ $ \land 1 \mathcal{E} $ } 191 \RightLabel{ $ \land 1 \mathcal{E} $ }
335 A と f の2つを仮定したところで、証明である \verb/->E/を定義する。 334 A と f の2つを仮定したところで、証明である \verb/->E/を定義する。
336 証明するべき式は \verb/->E/ の型として与えられ、証明は \verb/->E/ の式として記述する。 335 証明するべき式は \verb/->E/ の型として与えられ、証明は \verb/->E/ の式として記述する。
337 式の型に対する定義を正しく行なうことで証明を与える。 336 式の型に対する定義を正しく行なうことで証明を与える。
338 337
339 $ \Rightarrow \mathcal{E} $ に対応する \verb/->E/ は関数の適用なので、値a と関数 f を受けとって適用することで B が得られる。 338 $ \Rightarrow \mathcal{E} $ に対応する \verb/->E/ は関数の適用なので、値a と関数 f を受けとって適用することで B が得られる。
340 なお、仮定を alive のまま証明を記述するのは依存した仮定を残すことになるため、必要な仮定を引数として受けとったり、implicit な parameter として指定して証明するのが良い。 339 なお、仮定を alive のまま証明を記述するのは依存した仮定を残すため、必要な仮定を引数として受けとったり、implicit な parameter として指定して証明するのが良い。
341 340
342 また、Agda は証明に用いる規則なども Agda 内部で定義することができる。 341 また、Agda は証明に用いる規則なども Agda 内部で定義することができる。
343 例えば、直積型の定義はリスト\ref{src:product}のようなものがある。 342 例えば、直積型の定義はリスト\ref{src:product}のようなものがある。
344 343
345 \begin{table}[html] 344 \begin{table}[html]
433 432
434 \begin{table}[html] 433 \begin{table}[html]
435 \lstinputlisting[label=src:three_plus_one, caption= Agda における 3 + 1 の結果が 4 と等しい証明] {src/three_plus_one.agda} 434 \lstinputlisting[label=src:three_plus_one, caption= Agda における 3 + 1 の結果が 4 と等しい証明] {src/three_plus_one.agda}
436 \end{table} 435 \end{table}
437 436
438 3+1 という1つの関数を定義し、その型として証明すべき式 \verb/(S (S (S O))) + (S O)≡(S (S (S (S O))))/ を記述する。 437 3+1 という関数を定義し、その型として証明すべき式 \verb/(S (S (S O))) + (S O)≡(S (S (S (S O))))/ を記述する。
439 そして証明を関数の定義として記述する。 438 そして証明すべき式を関数の定義として記述する。
440 今回は \verb/_+_/ 関数の定義により \verb/ (S (S (S (S O)))) / に簡約されるためにコンストラクタ refl が証明となる。 439 今回は \verb/_+_/ 関数の定義により \verb/ (S (S (S (S O)))) / に簡約されるためにコンストラクタ refl が証明となる。
441 440
442 $ \equiv $ によって証明する際、必ず同じ式に簡約されるとは限らないため、いくつかの操作が Relation.Binary.PropositionalEquality に定義されている。 441 $ \equiv $ によって証明する際、必ず同じ式に簡約されるとは限らないため、いくつかの操作が Relation.Binary.PropositionalEquality に定義されている。
443 442
444 \begin{itemize} 443 \begin{itemize}