Papers/2015/atton-thesis: agda.tex annotate

annotate agda.tex @ 41:8fc2ac1f901f

Add delta definition in agda

author	Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date	Fri, 13 Feb 2015 11:48:40 +0900
parents	470d99799398
children	4f1107f1f6aa

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

Mercurial > hg > Papers > 2015 > atton-thesis

annotate agda.tex @ 41:8fc2ac1f901f