Mercurial > hg > Papers > 2015 > atton-thesis
annotate agda.tex @ 45:12c5e455fe55
Writing description proofs of monad-laws for delta
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 15 Feb 2015 10:33:47 +0900 |
| parents | 4f1107f1f6aa |
| children | bf136bd59e7a |
| rev | line source |
|---|---|
|
40
470d99799398
Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
1 \chapter{証明支援系言語 Agda による証明手法} |
|
23
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 \label{chapter:agda} |
|
45
12c5e455fe55
Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
3 第\ref{chapter:category}章では functor, natural transformation, monad の定義を行ない、第\ref{chapter:functional_programming}章では functional programming における対応を述べた。 |
|
23
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 その中で、 Functor 則や Monad 則といった満たすべき性質がいくつか存在した。 |
|
45
12c5e455fe55
Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
5 functional programming において、あるデータ型と対応する計算が Functor 則を満たすかの保証は言語の実装に依存している。 |
|
12c5e455fe55
Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
6 例えば、 Haskell において functor は型クラスによって提供されるため、型レベルのチェックを行なう。 |
|
12c5e455fe55
Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
7 そのため、型チェックは通るが Functor 則を満たさない functor が定義できてしまう。 |
|
12c5e455fe55
Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
8 よって Haskell において Delta Monad を定義しただけでは証明が存在しない。 |
|
12c5e455fe55
Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
9 そこで証明支援系言語 Agda を用いて、 Delta が Functor 則と Monad 則を満たすことを証明する。 |
|
23
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 |
|
45
12c5e455fe55
Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
11 第\ref{chapter:agda}章は Agda における証明手法について述べる。 |
|
23
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 % {{{ Natural Deduction |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 \section{Natural Deduction} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 \label{section:natural_deduction} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 証明には natural deduction(自然演繹)を用いる。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 natural deduction は Gentzen によって作られた論理と、その証明システムである。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 命題変数と記号を用いた論理式で論理を記述し、推論規則により変形することで求める論理式を導く。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 natural deduction において |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 \begin{eqnarray} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 \vdots \\ \nonumber |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 A \\ \nonumber |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 \end{eqnarray} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 と書いた時、最終的に命題Aを証明したことを意味する。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 証明は木構造で表わされ、葉の命題は仮定となる。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 仮定には dead か alive の2つの状態が存在する。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 \begin{eqnarray} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 \label{exp:a_implies_b} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 A \\ \nonumber |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 \vdots \\ \nonumber |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 B \\ \nonumber |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 \end{eqnarray} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 式\ref{exp:a_implies_b}のように A を仮定して B を導くことができたとする。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 この時 A は alive な仮定である。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 証明された B は A の仮定に依存していることを意味する。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 ここで、推論規則により記号 $ \Rightarrow $ を導入する。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 \begin{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 \AxiomC{[$ A $]} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 \noLine |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 \UnaryInfC{ $ \vdots $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 \noLine |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 \UnaryInfC{ $ B $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 \RightLabel{ $ \Rightarrow \mathcal{I} $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 \UnaryInfC{$ A \Rightarrow B $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 \end{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 そうすると、仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 A という仮定に依存して B を導く証明から、A が存在すれば B が存在するという証明を導いたこととなる。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導くことができる。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
59 alive な仮定を dead にすることができるのは $ \Rightarrow I $ 規則のみである。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 それを踏まえ、 natural deduction には以下のような規則が存在する。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
62 \begin{itemize} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 \item Hypothesis |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
65 仮定。葉にある式が仮定となるため、論理式A を仮定する場合に以下のように書く。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 $ A $ |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
68 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
69 \item Introductions |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
70 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
71 導入。証明された論理式に対して記号を導入することで新たな証明を導く。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
72 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
73 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
74 \begin{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
75 \AxiomC{ $ \vdots $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
76 \noLine |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
77 \UnaryInfC{ $ A $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
78 \AxiomC{ $ \vdots $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
79 \noLine |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
80 \UnaryInfC{ $ B $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
81 \RightLabel{ $ \land \mathcal{I} $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
82 \BinaryInfC{$ A \land B $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
83 \end{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
84 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
85 \begin{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
86 \AxiomC{ $ \vdots $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
87 \noLine |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
88 \UnaryInfC{ $ A $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
89 \RightLabel{ $ \lor 1 \mathcal{I} $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
90 \UnaryInfC{$ A \lor B $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
91 \end{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
92 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
93 \begin{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
94 \AxiomC{ $ \vdots $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
95 \noLine |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
96 \UnaryInfC{ $ B $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
97 \RightLabel{ $ \lor 2 \mathcal{I} $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
98 \UnaryInfC{$ A \lor B $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
99 \end{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
100 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
101 \begin{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
102 \AxiomC{[$ A $]} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
103 \noLine |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
104 \UnaryInfC{ $ \vdots $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
105 \noLine |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
106 \UnaryInfC{ $ B $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
107 \RightLabel{ $ \Rightarrow \mathcal{I} $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
108 \UnaryInfC{$ A \Rightarrow B $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
109 \end{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
110 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
111 \item Eliminations |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
112 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
113 除去。ある論理記号で構成された証明から別の証明を導く。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
114 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
115 \begin{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
116 \AxiomC{ $ \vdots $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
117 \noLine |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
118 \UnaryInfC{ $ A \land B $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
119 \RightLabel{ $ \land 1 \mathcal{E} $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
120 \UnaryInfC{$ A $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
121 \end{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
122 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
123 \begin{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
124 \AxiomC{ $ \vdots $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
125 \noLine |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
126 \UnaryInfC{ $ A \land B $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
127 \RightLabel{ $ \land 2 \mathcal{E} $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
128 \UnaryInfC{$ B $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
129 \end{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
130 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
131 \begin{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
132 \AxiomC{ $ \vdots $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
133 \noLine |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
134 \UnaryInfC{ $ A \lor B $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
135 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
136 \AxiomC{[$A$]} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
137 \noLine |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
138 \UnaryInfC{ $ \vdots $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
139 \noLine |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
140 \UnaryInfC{ $ C $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
141 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
142 \AxiomC{[$B$]} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
143 \noLine |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
144 \UnaryInfC{ $ \vdots $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
145 \noLine |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
146 \UnaryInfC{ $ C $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
147 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
148 \RightLabel{ $ \lor \mathcal{E} $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
149 \TrinaryInfC{ $ C $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
150 \end{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
151 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
152 \begin{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
153 \AxiomC{ $ \vdots $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
154 \noLine |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
155 \UnaryInfC{ $ A $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
156 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
157 \AxiomC{ $ \vdots $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
158 \noLine |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
159 \UnaryInfC{ $ A \Rightarrow B $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
160 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
161 \RightLabel{ $ \Rightarrow \mathcal{E} $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
162 \BinaryInfC{$ B $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
163 \end{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
164 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
165 \end{itemize} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
166 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
167 記号 $ \lor, \land, \Rightarrow $ の導入の除去規則について述べた。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
168 natural deduction には他にも $ \forall, \exists, \bot $ といった記号が存在するが、ここでは解説を省略する。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
169 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
170 それぞれの記号は以下のような意味を持つ |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
171 \begin{itemize} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
172 \item $ \land $ |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
173 conjunction。2つの命題が成り立つことを示す。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
174 $ A \land B $ と記述すると A かつ B と考えることができる。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
175 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
176 \item $ \lor $ |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
177 disjunction。2つの命題のうちどちらかが成り立つことを示す。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
178 $ A \lor B $ と記述すると A または B と考えることができる。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
179 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
180 \item $ \Rightarrow $ |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
181 implication。左側の命題が成り立つ時、右側の命題が成り立つことを示す。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
182 $ A \Rightarrow B $ と記述すると A ならば B と考えることができる。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
183 \end{itemize} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
184 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
185 例として、natural deduction で三段論法を証明する。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
186 なお、三段論法とは「A は B であり、 B は C である。よって A は C である」といった文を示すこととする。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
187 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
188 \begin{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
189 \AxiomC{ $ [A] $ $_{(1)}$} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
190 \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
191 \RightLabel{ $ \land 1 \mathcal{E} $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
192 \UnaryInfC{ $ (A \Rightarrow B) $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
193 \BinaryInfC{ $ B $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
194 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
195 \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
196 \RightLabel{ $ \land 2 \mathcal{E} $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
197 \UnaryInfC{ $ (B \Rightarrow C) $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
198 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
199 \BinaryInfC{ $ C $ } |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
200 \RightLabel{ $ \Rightarrow \mathcal{I} _{(1)}$} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
201 \UnaryInfC{ $ A \Rightarrow C $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
202 \RightLabel{ $ \Rightarrow \mathcal{I} _{(2)}$} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
203 \UnaryInfC{ $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
204 \end{prooftree} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
205 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
206 まず、三段論法を論理式で表す。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
207 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
208 「A は B であり、 B は C である。よって A は C である」 が証明するべき命題である。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
209 まず、「A は B であり」から、Aから性質Bが導けることが分かる。これが $ A \Rightarrow B $ となる。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
210 次に、「B は C である」から、Bから性質Cが導けることが分かる。これが $ B \Rightarrow C $ となる。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
211 そしてこの2つは同時に成り立つ。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
212 よって $ (A \Rightarrow B) \land (B \Rightarrow C)$ が前提となる。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
213 この条件2つが成り立つ時に「Aは Cである」が成りたつ。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
214 条件と同じように「A は C である」は、 $ A \Rightarrow C $ と書けるため、証明するべき論理式は $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ になる。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
215 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
216 証明の手順はこうである。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
217 まず条件$ (A \Rightarrow B) \land (B \Rightarrow C)$とAを2つ仮定する。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
218 条件を $ \land 1 \mathcal{E} $ $ \land 2 \mathcal{E} $ により分解する。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
219 A と $ A \Rightarrow B$ から B を、 B から $ B \Rightarrow C $ から C を導く。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
220 ここで $ \Rightarrow \mathcal{I} $ により $ A \Rightarrow C $ を導く。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
221 この際に dead にする仮定は A である。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
222 そのために $_{(1)} $ と対応する \verb/[]/の記号に数値を付けてある。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
223 これで残る仮定は $ (A \Rightarrow B) \land (B \Rightarrow C)$ となり、これから $ A \Rightarrow C $ を導くことができたためにさらに $ \Rightarrow \mathcal{I} $ を適用する。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
224 結果、証明すべき論理式$ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ が導けたために証明終了となる。 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
225 |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
226 % }}} |
|
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
227 |
|
24
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
228 % {{{ Curry-Howard Isomorphism |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
229 |
|
23
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
230 \section{Curry-Howard Isomorphism} |
|
24
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
231 \label{section:curry_howard_isomorphism} |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
232 \ref{section:natural_deduction}節では natural deduction における証明手法について述べた。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
233 natural deduction における証明は Curry-Howard Isomorphism により型付き $ \lambda $ 計算と対応している。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
234 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
235 $ \lambda $ 計算とは、計算モデルの1つであり、計算の実行を関数への適用としてモデル化したものである。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
236 関数は $ \lambda $ 式として表され、引数を1つ取りその引数を計算する関数は式\ref{exp:lambda_expression}のように記述される。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
237 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
238 \begin{equation} |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
239 \label{exp:lambda_expression} |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
240 \lambda x . x |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
241 \end{equation} |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
242 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
243 値と $ \lambda $ 式には型を付与することができ、その型の計算が natural deduction と対応している。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
244 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
245 例えば命題Aが成り立つためには A という型を持つ値が存在すれば良い。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
246 しかしこの命題は A という alive な仮定に依存している。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
247 natural deduction では A の仮定を dead にするために $ \Rightarrow \mathcal{I} $ により $ \Rightarrow $ を導入する。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
248 これが $ \lambda $ による抽象化に対応している。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
249 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
250 \begin{eqnarray} |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
251 x : A \\ \nonumber |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
252 \lambda x . x : A \rightarrow A |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
253 \end{eqnarray} |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
254 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
255 プログラムにおいて、変数 x は内部の値により型が決定される。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
256 特に、x の値が未定である場合は未定義の変数としてエラーが発生する。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
257 しかし、 x を取って x を返す関数は定義することはできる。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
258 これは natural deduction の $ \Rightarrow \mathcal{I} $ により仮定を discharge することに相当する。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
259 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
260 このように、 natural deduction における証明はそのまま 型付き $ \lambda $ 計算にエンコードすることができる。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
261 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
262 それぞれの詳細な対応は省略するが、表\ref{tbl:curry_howard_isomorphism} のような対応が存在する。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
263 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
264 \begin{center} |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
265 \begin{table}[htbp] |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
266 \begin{tabular}{|c||c|c|} \hline |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
267 & natural deduction & 型付き $ \lambda $ 計算 \\ \hline \hline |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
268 hypothesis & $ A $ & 型 A を持つ変数 x \\ \hline |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
269 conjunction & $ A \land B $ & 型 A と型 B の直積型 を持つ変数 x \\ \hline |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
270 disjunction & $ A \lor B $ & 型 A と型 B の直和型 を持つ変数 x \\ \hline |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
271 implication & $ A \Rightarrow B $ & 型 A を取り型 B の変数を返す関数 f \\ \hline |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
272 \end{tabular} |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
273 \caption{natural deuction と 型付き $ \lambda $ 計算との対応} |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
274 \label{tbl:curry_howard_isomorphism} |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
275 \end{table} |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
276 \end{center} |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
277 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
278 \ref{section:natural_deduction}節でも行なった三段論法の証明を Haskell により行なうとリスト\ref{src:modus_ponens} |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
279 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
280 \begin{table}[html] |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
281 \lstinputlisting[label=src:modus_ponens, caption=Haskell における三段論法の証明] {src/modus_ponens.txt} |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
282 \end{table} |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
283 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
284 証明は $ \lambda $ 式の型として表現される。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
285 Haskell における $ \lambda $ 式は \verb| \x -> x| のように表される。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
286 \verb/\/ と \verb/->/ の間が引数であり、 \verb/->/ の後に処理を記述する。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
287 また、$ \land $ に対応する直積型は tuple として提供される。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
288 A と B の直積型は $ (A, B) $ として表現される。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
289 そして、 $ \land 1 \mathcal{E} $ に対応する処理は関数 fst 、 $ \land 2 \mathcal{E} $ に対応する処理は関数 snd として提供される。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
290 fst と snd が $ \land $ の除去に対応しているのは型を見ることで分かる。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
291 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
292 そして三段論法の証明の解説を行なう。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
293 三段論法の仮定は、$ (A \Rightarrow B) \land (B \Rightarrow C) $ であった。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
294 この仮定を変数 cond として受けとる。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
295 cond に対して fst を行なうことで $ (A \Rightarrow B) $ を、snd を行なうことで $ (B \Rightarrow C) $ を証明する。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
296 ここでさらに仮定 a を導入し、$ (A \Rightarrow B) $ と$ (B \Rightarrow C) $ に適用することで C を得る。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
297 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
298 結果、 \verb/\cond -> (\a -> (snd cond ((fst cond) a)))/のような式が得られ、この型を確認すると正しく三段論法の証明となっている。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
299 なお、型推論の際に A はt2 に、 B は t1 に、 C は t という型名になっている。 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
300 |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
301 % }}} |
|
13affa3e65a2
Add curry-howad isomorphism
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
302 |
|
25
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
303 % {{{ Agda による証明 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
304 |
|
23
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
305 \section{Agda による証明} |
| 26 | 306 \label{section:agda} |
|
25
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
307 \ref{section:curry_howard_isomorphism}節において型を用いて証明を行なう手法を述べた。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
308 しかし、Haskell における型システムは証明を記述するために用いるものではない。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
309 よって、依存型を持つ証明支援言語 Agda を用いて証明を記述していく。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
310 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
311 依存型とは値に依存した型を作ることができる型であり、非常に表現能力が高い。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
312 値に型を使うことができるために証明に基づいた証明を記述することができる。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
313 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
314 $ \Rightarrow \mathcal{E} $ に対応する関数適用を Agda で記述するとリスト\ref{src:apply_function_in_agda}のようになる。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
315 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
316 \begin{table}[html] |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
317 \lstinputlisting[label=src:apply_function_in_agda, caption=Agda における $ \Rightarrow \mathcal{E} $ ] {src/apply_function.agda} |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
318 \end{table} |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
319 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
320 Agda による型注釈は \verb/ term : type/ と記述する。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
321 postulate とすると alive な証明を記述することができる。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
322 まずは alive な A を仮定している。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
323 なお、Set 型は型の型として組込みで用意されている型である。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
324 そのため詳細は省略するが、 A は型であると考える。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
325 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
326 次に関数 f を仮定する。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
327 仮定に用いられている記号 \verb/{}/ の内部の式は implicit な paramter である。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
328 任意の B の対してこの型が成り立つことを記述している。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
329 implicit な parameter は可能であれば Agda が推論する。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
330 そのため、f の見掛け上の型は \verb/A -> B/のようになる。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
331 ここで、 B に明示的に値を代入することで f の型を変更することもできる。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
332 このように Agda では型における引数のようなものが存在し、型の表現能力が高い。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
333 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
334 A と f の2つを仮定したところで、証明である \verb/->E/を定義する。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
335 証明するべき式は \verb/->E/ の型として与えられ、証明は \verb/->E/ の式として記述する。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
336 式の型に対する定義を正しく行なうことで証明を与える。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
337 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
338 $ \Rightarrow \mathcal{E} $ に対応する \verb/->E/ は関数の適用なので、値a と関数 f を受けとって適用することで B が得られる。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
339 なお、仮定を alive のまま証明を記述するのは依存した仮定を残すことになるため、必要な仮定を引数として受けとったり、implicit な parameter として指定して証明するのが良い。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
340 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
341 また、Agda は証明に用いる規則なども Agda 内部で定義することができる。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
342 例えば、直積型の定義はリスト\ref{src:product}のようなものがある。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
343 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
344 \begin{table}[html] |
|
41
8fc2ac1f901f
Add delta definition in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
40
diff
changeset
|
345 \lstinputlisting[label=src:product, caption=Agdaにおける直積型の例] {src/product.agda.replaced} |
|
25
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
346 \end{table} |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
347 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
348 関数の定義時に \verb/_/ とした部分には項を入れることで関数が適用される。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
349 つまり \verb/_x_/ とすれば中置関数を作成することができる。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
350 データ型 \verb/_x_/ は型 A と B を持つ型である。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
351 データ型 \verb/_x_/ はコンストラクタ \verb/<_,_>/ により構成され、コンストラクタは A と B を取ることで \verb/A x B/ 型を返す。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
352 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
353 例えば型A と B から 直積型 $ A \times B $ が作成できる証明は constructProduct である。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
354 任意の型AとBを受けとり、コンストラクタ \verb/<_,_>/を用いて $ A \times B $ に相当する \verb/A x B/を返す。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
355 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
356 また、型に対応するコンストラクタはパターンマッチにより分解することができる。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
357 その例が patternMatchProduct である。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
358 受けとる引数の型は \verb/ A x B/ であるため、ありえるコンストラクタは \verb/<_,_>/のみである。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
359 よって引数を取る際に \verb/< a , b >/ のように対応するコンストラクタと変数を用意することで、コンストラクタに基づいて型を分解することができる。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
360 \verb/A x B/ 型から B を取るため、\verb/A x B/ 型の変数を直接束縛せずにコンストラクタで分解し、a と b に束縛することで A と B が得られる。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
361 そのため、 patternMathProduct は $ \land 2 \mathcal{E} $ そのものである。 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
362 |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
363 % }}} |
|
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
364 |
| 28 | 365 % {{{ Reasoning |
| 366 | |
| 26 | 367 \section{Reasoning} |
| 368 \label{section:reasoning} | |
| 369 \ref{section:agda} 節ではAgdaにおける証明の手法について解説した。 | |
| 370 \ref{section:reasoning}節では Agda における証明の例として、自然数の加法の交換法則を証明する。 | |
|
25
a0d91fbf4876
Add description prove method in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
371 |
| 26 | 372 まずは自然数を定義する。 |
| 373 今回用いる自然数の定義は以下のようなものである。 | |
| 374 | |
| 375 \begin{itemize} | |
| 376 \item 0 は自然数である | |
| 377 \item 任意の自然数には後続数が存在する | |
| 378 \item 0 はいかなる自然数の後続数でもない | |
| 379 \item 異なる自然数どうしの後続数は異なる ($ n \neq m \rightarrow S n \neq S m $) | |
| 380 \item 0がある性質を満たし、aがある性質を満たせばその後続数 S(n) も自然数である | |
| 381 \end{itemize} | |
| 382 | |
| 383 この定義は peano arithmetic における自然数の定義である。 | |
| 384 | |
| 385 Agda で自然数型 Nat を定義するとリスト \ref{src:nat} のようになる。 | |
| 386 | |
| 387 \begin{table}[html] | |
| 388 \lstinputlisting[label=src:nat, caption=Agda における自然数型 Nat の定義] {src/nat.agda} | |
| 389 \end{table} | |
| 390 | |
| 391 自然数型 Nat は2つのコンストラクタを持つ。 | |
| 392 | |
| 393 \begin{itemize} | |
| 394 \item O | |
| 395 | |
| 396 引数を持たないコンストラクタ。これが0に相当する。 | |
| 397 | |
| 398 \item S | |
| 399 | |
| 400 Nat を引数に取るコンストラクタ。これが後続数に相当する。 | |
| 401 | |
| 402 \end{itemize} | |
| 403 | |
| 404 よって、数値の 3 は \verb/S (S (S O))/ のように表現される。 | |
| 405 Sの個数が数値に対応する。 | |
| 406 | |
| 407 次に加算を定義する(リスト\ref{src:nat_add})。 | |
| 408 | |
| 409 \begin{table}[html] | |
| 410 \lstinputlisting[label=src:nat_add, caption=Agdaにおける自然数型に対する加算の定義] {src/nat_add.agda} | |
| 411 \end{table} | |
| 412 | |
| 413 加算は中置関数 \verb/_+_/ として定義する。 | |
| 414 2つの Nat を取り、Natを返す。 | |
| 415 パターンマッチにより処理を変える。 | |
| 416 0に対して m 加算する場合は m であり、 n の後続数に対して m 加算する場合は n に m 加算した数の後続数とする。 | |
| 417 S を左の数から右の数へ1つずつ再帰的に移していくような加算である。 | |
| 418 | |
| 419 例えば 3 + 1 といった計算は (S (S (S O))) + (S O) のように記述される。 | |
| 420 ここで 3 + 1 が 4と等しいことの証明を行なう。 | |
| 421 | |
| 422 等式の証明には agda の standard library における Relation.Binary.Core の定義を用いる。 | |
| 423 | |
| 424 \begin{table}[html] | |
| 44 | 425 \lstinputlisting[label=src:equiv, caption= Relation.Binary.Core による等式を示す型 $ \equiv $] {src/equiv.agda.replaced} |
| 26 | 426 \end{table} |
| 427 等式は等式を示すデータ型 $ \equiv $ により定義される。 | |
| 428 $ \equiv $ は同じ両辺が同じ項に簡約される時にコンストラクタ refl で構築できる。 | |
| 429 | |
| 430 実際に 3 + 1 = 4 の証明は refl で構成できる(リスト\ref{src:three_plus_one})。 | |
| 431 | |
| 432 \begin{table}[html] | |
| 433 \lstinputlisting[label=src:three_plus_one, caption= Agda における 3 + 1 の結果が 4 と等しい証明] {src/three_plus_one.agda} | |
| 434 \end{table} | |
|
23
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
435 |
| 26 | 436 3+1 という1つの関数を定義し、その型として証明すべき式 \verb/(S (S (S O))) + (S O)≡(S (S (S (S O))))/ を記述する。 |
| 437 そして証明を関数の定義として記述する。 | |
| 438 今回は \verb/_+_/ 関数の定義により \verb/ (S (S (S (S O)))) / に簡約されるためにコンストラクタ refl が証明となる。 | |
| 439 | |
| 440 $ \equiv $ によって証明する際、必ず同じ式に簡約されるとは限らないため、いくつかの操作が Relation.Binary.PropositionalEquality に定義されている。 | |
| 441 | |
| 442 \begin{itemize} | |
| 443 \item sym : $ x \equiv y \rightarrow y \equiv x $ | |
| 444 | |
| 445 等式が証明できればその等式の左辺と右辺を反転しても等しい。 | |
| 446 | |
| 447 \item cong : $ f \rightarrow x \equiv y \rightarrow f x \equiv f y $ | |
| 448 | |
| 449 証明した等式に同じ関数を与えても等式は保たれる。 | |
| 450 | |
| 451 \item trans : $ x \equiv y \rightarrow y \equiv z \rightarrow x \equiv z $ | |
| 452 | |
| 453 2つの等式に表れた同じ項を用いて2つの等式を繋げた等式は等しい。 | |
| 454 \end{itemize} | |
| 455 | |
| 456 ではこれから nat の加法の交換法則を証明していく(リスト\ref{src:nat_add_sym})。 | |
| 457 | |
| 458 \begin{table}[html] | |
| 459 \lstinputlisting[label=src:nat_add_sym, caption= Agda における加法の交換法則の証明] {src/nat_add_sym.agda} | |
| 460 \end{table} | |
| 461 | |
| 462 証明する式は $ n + m \equiv m + n $ である。 | |
| 463 n と m は Nat であるため、それぞれがコンストラクタ O か S により構成される。 | |
| 464 そのためにパターンは4通りある。 | |
| 465 | |
| 466 \begin{itemize} | |
| 467 \item n = O, m = O | |
| 468 | |
| 469 + の定義により、 O に簡約されるため refl で証明できる。 | |
| 470 | |
| 471 \item n = O, m = S m | |
| 472 | |
| 473 $ O + (S m) \equiv (S m) + O $ を証明することになる。 | |
| 474 この等式は + の定義により $ O + (S m) \equiv S (m + O) $ と変形できる。 | |
| 27 | 475 $ S (m + O) $ は $ m + O $ に S を加えたものであるため、 cong を用いて再帰的に \verb/addSym/ を実行することで証明できる。 |
| 26 | 476 |
| 477 この2つの証明はこのような意味を持つ。 | |
| 478 n が 0 であるとき、 m も 0 なら簡約により等式が成立する。 | |
| 479 n が 0 であるとき、 m が 0 でないとき、 m は後続数である。 | |
| 480 よって m が (S x) と書かれる時、 x は m の前の値である。 | |
| 481 前の値による交換法則を用いてからその結果の後続数も + の定義により等しい。 | |
| 27 | 482 ここで、 \verb/addSym/ に渡される m は1つ値が減っているため、最終的には n = 0, m = 0 である refl にまで簡約され、等式が得られる。 |
| 26 | 483 |
| 484 \item n = S n, m = O | |
| 485 | |
| 486 $ (S n) + O \equiv O + (S n) $ を証明する。 | |
| 487 この等式は + の定義により $ S (n + O) \equiv (S n) $ と変形できる。 | |
| 488 さらに変形すれば $ S (n + O) \equiv S (O + n) $ となる。 | |
| 27 | 489 よって \verb/addSym/ により O と n を変換した後に cong で S を加えることで証明ができる。 |
| 26 | 490 |
| 491 ここで、 $ O + n \equiv n $ は + の定義により自明であるが、$ n + O \equiv n $ をそのまま導出できないことに注意して欲しい。 | |
| 492 + の定義は左側の項から S を右側の項への移すだけであるため、右側の項への演算はしない。 | |
| 493 | |
| 494 \item n = S n, m = S m | |
| 495 | |
| 496 3つのパターンは証明したが、このパターンは少々長くなるため別に解説することとする。 | |
| 497 \end{itemize} | |
| 498 | |
| 499 3 つのパターンにおいては refl や cong といった単純な項で証明を行なうことができた。 | |
| 500 しかし長い証明になると refl や cong といった式を trans で大量に繋げていく必要性がある。 | |
| 501 長い証明を分かりやすく記述するために $ \equiv $-Reasoning を用いる。 | |
| 28 | 502 |
| 503 $ \equiv $-Reasoning では等式の左辺を begin の後に記述し、等式の変形を $ \equiv \langle expression \rangle $ に記述することで変形していく。 | |
| 504 最終的に等式の左辺を $ \blacksquare $ の項へと変形することで等式の証明が得られる。 | |
| 505 | |
| 506 自然数の加法の交換法則を $ \equiv $-Reasoning を用いて証明した例がリスト\ref{src:nat_add_sym_reasoning}である。 | |
| 507 特に n と m が1以上である時の証明に注目する。 | |
| 508 | |
| 509 \begin{table}[html] | |
| 36 | 510 \lstinputlisting[label=src:nat_add_sym_reasoning, caption= $ \equiv $ - Reasoning を用いた証明の例] {src/nat_add_sym_reasoning.agda.replaced} |
| 28 | 511 \end{table} |
| 512 | |
| 513 まず \verb/ (S n) + (S m)/ は + の定義により \verb/ S (n + (S m)) / に等しい。 | |
| 514 よって refl で導かれる。 | |
| 515 なお、基本的に定義などで同じ項に簡約される時は refl によって記述することが多い。 | |
| 516 | |
| 517 次に \verb/S (n + (S m)) / に対して addSym を用いて交換し、 cong によって S を追加することで \verb/ S ((S m) + n) / を得る。 | |
| 518 これは、前3パターンにおいて + の右辺の項が 1以上であっても上手く交換法則が定義できたことを利用して項を変形している。 | |
| 519 このように同じ法則の中でも、違うパターンで証明できた部分を用いて別パターンの証明を行なうこともある。 | |
| 520 | |
| 521 最後に \verb/S ((S m) + n)/ から \verb/(S m) + (S n)/を得なくてはならない。 | |
| 522 しかし、 + の定義には右辺に対して S を移動する演算が含まれていない。 | |
| 523 よってこのままでは証明することができない。 | |
| 524 そのため、等式 $ S (m + n) \equiv m + (S n) $ を addToRight として定義する。 | |
| 525 addToRight の証明の解説は省略する。 | |
| 526 addToRight を用いることで \verb/S ((S m) + n)/ から \verb/(S m) + (S n)/を得られた。 | |
| 527 これで等式 $ (S m) + (S n) \equiv (S n) + (S m) $ の証明が完了した。 | |
| 528 | |
| 529 自然数に対する + の演算を考えた時にありえるコンストラクタの組み合せ4パターンのいずれかでも交換法則の等式が成り立つことが分かった。 | |
| 530 また、定義した + の演算のみでは加法の交換法則は証明できず、さらに等式を証明する必要があった。 | |
| 531 | |
| 532 このように、Agda における等式の証明は、定義や等式を用いて右辺と左辺を同じ項に変形することで行なわれる。 | |
| 533 | |
| 534 % }}} |