Papers/2018/nozomi-master: paper/agda.tex annotate

annotate paper/agda.tex @ 51:6318c8f4bb8c

Writing Agda description

author	atton <atton@cr.ie.u-ryukyu.ac.jp>
date	Tue, 31 Jan 2017 11:57:12 +0900
parents	451c510825de
children	fb42478e4c96

rev	line source
49 7f1b5c33b282 Add agda.tex atton <atton@cr.ie.u-ryukyu.ac.jp> parents: diff changeset	1 \chapter{証明支援系言語 Agda による証明手法}
7f1b5c33b282 Add agda.tex atton <atton@cr.ie.u-ryukyu.ac.jp> parents: diff changeset	2 \label{chapter:agda}
50 451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	3 第~\ref{chapter:type}章では形無し算術式と型付き算術式による型システムの定義、ラムダ計算によるプログラミング言語の抽象化、部分型の導入とCbCの型が部分型で示せることを確認した。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	4 部分型を用いて具体的なCbCの型システムを定義する前に、型システムの一方のメリットである証明について触れる。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	5 依存型という型を持つ証明支援系言語 Agda を用いて証明が行なえることを示す。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	6
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	7 % {{{ Natural Deduction
49 7f1b5c33b282 Add agda.tex atton <atton@cr.ie.u-ryukyu.ac.jp> parents: diff changeset	8 \section{Natural Deduction}
50 451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	9 まず始めに証明を行なうためにNatural Deduction(自然演繹)を示す。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	10
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	11 証明には natural deduction(自然演繹)を用いる。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	12 natural deduction は Gentzen によって作られた論理と、その証明システムである~\cite{Girard:1989:PT:64805}。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	13 命題変数と記号を用いた論理式で論理を記述し、推論規則により変形することで求める論理式を導く。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	14
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	15 natural deduction において
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	16
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	17 \begin{eqnarray}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	18 \vdots \\ \nonumber
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	19 A \\ \nonumber
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	20 \end{eqnarray}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	21
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	22 と書いた時、最終的に命題Aを証明したことを意味する。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	23 証明は木構造で表わされ、葉の命題は仮定となる。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	24 仮定には dead か alive の2つの状態が存在する。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	25
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	26 \begin{eqnarray}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	27 \label{exp:a_implies_b}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	28 A \\ \nonumber
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	29 \vdots \\ \nonumber
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	30 B \\ \nonumber
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	31 \end{eqnarray}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	32
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	33 式\ref{exp:a_implies_b}のように A を仮定して B を導いたとする。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	34 この時 A は alive な仮定であり、証明された B は A の仮定に依存していることを意味する。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	35
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	36 ここで、推論規則により記号 $ \Rightarrow $ を導入する。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	37
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	38 \begin{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	39 \AxiomC{[$ A $]}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	40 \noLine
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	41 \UnaryInfC{ $ \vdots $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	42 \noLine
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	43 \UnaryInfC{ $ B $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	44 \RightLabel{ $ \Rightarrow \mathcal{I} $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	45 \UnaryInfC{$ A \Rightarrow B $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	46 \end{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	47
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	48 $ \Rightarrow \mathcal{I} $ を適用することで仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	49 A という仮定に依存して B を導く証明から、「A が存在すれば B が存在する」という証明を導いたこととなる。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	50 このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導ける。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	51 なお、dead な仮定は \verb/[A]/ のように \verb/[]/ で囲んで書く。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	52
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	53 alive な仮定を dead にすることができるのは $ \Rightarrow \mathcal{I} $ 規則のみである。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	54 それを踏まえ、 natural deduction には以下のような規則が存在する。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	55
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	56 \begin{itemize}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	57 \item Hypothesis
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	58
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	59 仮定。葉にある式が仮定となるため、論理式A を仮定する場合に以下のように書く。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	60
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	61 $ A $
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	62
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	63 \item Introductions
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	64
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	65 導入。証明された論理式に対して記号を導入することで新たな証明を導く。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	66
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	67
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	68 \begin{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	69 \AxiomC{ $ \vdots $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	70 \noLine
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	71 \UnaryInfC{ $ A $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	72 \AxiomC{ $ \vdots $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	73 \noLine
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	74 \UnaryInfC{ $ B $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	75 \RightLabel{ $ \land \mathcal{I} $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	76 \BinaryInfC{$ A \land B $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	77 \end{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	78
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	79 \begin{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	80 \AxiomC{ $ \vdots $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	81 \noLine
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	82 \UnaryInfC{ $ A $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	83 \RightLabel{ $ \lor 1 \mathcal{I} $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	84 \UnaryInfC{$ A \lor B $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	85 \end{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	86
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	87 \begin{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	88 \AxiomC{ $ \vdots $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	89 \noLine
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	90 \UnaryInfC{ $ B $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	91 \RightLabel{ $ \lor 2 \mathcal{I} $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	92 \UnaryInfC{$ A \lor B $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	93 \end{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	94
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	95 \begin{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	96 \AxiomC{[$ A $]}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	97 \noLine
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	98 \UnaryInfC{ $ \vdots $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	99 \noLine
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	100 \UnaryInfC{ $ B $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	101 \RightLabel{ $ \Rightarrow \mathcal{I} $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	102 \UnaryInfC{$ A \Rightarrow B $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	103 \end{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	104
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	105 \item Eliminations
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	106
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	107 除去。ある論理記号で構成された証明から別の証明を導く。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	108
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	109 \begin{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	110 \AxiomC{ $ \vdots $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	111 \noLine
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	112 \UnaryInfC{ $ A \land B $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	113 \RightLabel{ $ \land 1 \mathcal{E} $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	114 \UnaryInfC{$ A $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	115 \end{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	116
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	117 \begin{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	118 \AxiomC{ $ \vdots $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	119 \noLine
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	120 \UnaryInfC{ $ A \land B $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	121 \RightLabel{ $ \land 2 \mathcal{E} $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	122 \UnaryInfC{$ B $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	123 \end{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	124
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	125 \begin{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	126 \AxiomC{ $ \vdots $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	127 \noLine
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	128 \UnaryInfC{ $ A \lor B $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	129
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	130 \AxiomC{[$A$]}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	131 \noLine
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	132 \UnaryInfC{ $ \vdots $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	133 \noLine
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	134 \UnaryInfC{ $ C $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	135
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	136 \AxiomC{[$B$]}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	137 \noLine
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	138 \UnaryInfC{ $ \vdots $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	139 \noLine
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	140 \UnaryInfC{ $ C $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	141
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	142 \RightLabel{ $ \lor \mathcal{E} $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	143 \TrinaryInfC{ $ C $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	144 \end{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	145
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	146 \begin{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	147 \AxiomC{ $ \vdots $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	148 \noLine
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	149 \UnaryInfC{ $ A $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	150
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	151 \AxiomC{ $ \vdots $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	152 \noLine
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	153 \UnaryInfC{ $ A \Rightarrow B $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	154
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	155 \RightLabel{ $ \Rightarrow \mathcal{E} $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	156 \BinaryInfC{$ B $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	157 \end{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	158
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	159 \end{itemize}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	160
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	161 記号 $ \lor, \land, \Rightarrow $ の導入の除去規則について述べた。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	162 natural deduction には他にも $ \forall, \exists, \bot $ といった記号が存在するが、ここでは解説を省略する。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	163
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	164 それぞれの記号は以下のような意味を持つ
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	165 \begin{itemize}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	166 \item $ \land $
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	167 conjunction。2つの命題が成り立つことを示す。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	168 $ A \land B $ と記述すると A かつ B と考えることができる。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	169
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	170 \item $ \lor $
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	171 disjunction。2つの命題のうちどちらかが成り立つことを示す。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	172 $ A \lor B $ と記述すると A または B と考えることができる。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	173
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	174 \item $ \Rightarrow $
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	175 implication。左側の命題が成り立つ時、右側の命題が成り立つことを示す。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	176 $ A \Rightarrow B $ と記述すると A ならば B と考えることができる。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	177 \end{itemize}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	178
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	179 例として、natural deduction で三段論法を証明する。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	180 なお、三段論法とは「A は B であり、 B は C である。よって A は C である」といった文を示す。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	181
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	182 \begin{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	183 \AxiomC{ $ [A] $ $_{(1)}$}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	184 \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	185 \RightLabel{ $ \land 1 \mathcal{E} $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	186 \UnaryInfC{ $ (A \Rightarrow B) $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	187 \BinaryInfC{ $ B $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	188
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	189 \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	190 \RightLabel{ $ \land 2 \mathcal{E} $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	191 \UnaryInfC{ $ (B \Rightarrow C) $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	192
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	193 \BinaryInfC{ $ C $ }
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	194 \RightLabel{ $ \Rightarrow \mathcal{I} _{(1)}$}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	195 \UnaryInfC{ $ A \Rightarrow C $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	196 \RightLabel{ $ \Rightarrow \mathcal{I} _{(2)}$}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	197 \UnaryInfC{ $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	198 \end{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	199
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	200 まず、三段論法を論理式で表す。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	201
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	202 「A は B であり、 B は C である。よって A は C である」が証明するべき命題である。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	203 まず、「A は B であり」から、Aから性質Bが導けることが分かる。これが $ A \Rightarrow B $ となる。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	204 次に、「B は C である」から、Bから性質Cが導けることが分かる。これが $ B \Rightarrow C $ となる。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	205 そしてこの2つは同時に成り立つ。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	206 よって $ (A \Rightarrow B) \land (B \Rightarrow C)$ が仮定となる。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	207 この仮定が成り立つ時に「Aは Cである」を示せば良い。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	208 仮定と同じように「A は C である」は、 $ A \Rightarrow C $ と書けるため、証明するべき論理式は $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ となる。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	209
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	210 証明の手順はこうである。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	211 まず条件$ (A \Rightarrow B) \land (B \Rightarrow C)$とAの2つを仮定する。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	212 条件を $ \land 1 \mathcal{E} $ $ \land 2 \mathcal{E} $ により分解する。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	213 A と $ A \Rightarrow B$ から B を、 B と $ B \Rightarrow C $ から C を導く。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	214 ここで $ \Rightarrow \mathcal{I} $ により $ A \Rightarrow C $ を導く。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	215 この際に dead にする仮定は A である。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	216 数回仮定を dead にする際は $_{(1)} $ のように対応する \verb/[]/の記号に数値を付ける。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	217 これで残る alive な仮定は $ (A \Rightarrow B) \land (B \Rightarrow C)$ となり、これから $ A \Rightarrow C $ を導くことができたためにさらに $ \Rightarrow \mathcal{I} $ を適用する。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	218 結果、証明すべき論理式$ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ が導けたために証明終了となる。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	219
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	220 % }}}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	221
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	222 % {{{ Curry-Howard Isomorphism
49 7f1b5c33b282 Add agda.tex atton <atton@cr.ie.u-ryukyu.ac.jp> parents: diff changeset	223 \section{Curry-Howard Isomorphism}
50 451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	224 \label{section:curry_howard_isomorphism}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	225 \ref{section:natural_deduction}節では natural deduction における証明手法について述べた。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	226 natural deduction における証明はほとんど型付き $ \lambda $ 計算のような形をしている。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	227 実際、Curry-Howard Isomorphism により Natural Deduction と型付き $ \lambda $ 計算は対応している。% ref TaPL 104
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	228
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	229 型構築子 $ \rightarrow $ のみに注目した時
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	230
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	231 \begin{enumerate}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	232 \item 導入規則(T-ABS) は、その型の要素がどのように作られるかを記述する
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	233 \item 除去規則(T-APP) は、その型の要素がどのように作られるかを記述する
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	234 \end{enumerate}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	235
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	236
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	237 例えば命題Aが成り立つためには A という型を持つ値が存在すれば良い。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	238 しかしこの命題は A という alive な仮定に依存している。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	239 natural deduction では A の仮定を dead にするために $ \Rightarrow \mathcal{I} $ により $ \Rightarrow $ を導入する。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	240 これが $ \lambda $ による抽象化(T-ABS)に対応している。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	241
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	242 \begin{eqnarray*}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	243 x : A \\
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	244 \lambda x . x : A \rightarrow A
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	245 \end{eqnarray*}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	246
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	247 プログラムにおいて、変数 x は内部の値により型が決定される。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	248 特に、x の値が未定である場合は未定義の変数としてエラーが発生する。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	249 しかし、 x を取って x を返す関数は定義することはできる。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	250 これは natural deduction の $ \Rightarrow \mathcal{I} $ により仮定を discharge することに相当する。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	251
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	252 また、仮定Aが成り立つ時に結論Bを得ることは、関数適用(T-APP)に相当している。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	253
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	254 \begin{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	255 \AxiomC{$A$}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	256 \AxiomC{$A \rightarrow B $}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	257 \RightLabel{T-APP}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	258 \BinaryInfC{$B$}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	259 \end{prooftree}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	260
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	261 このように、 natural deduction における証明はそのまま型付き $ \lambda $ 計算に変換することができる。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	262
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	263 それぞれの詳細な対応は省略するが、表\ref{tbl:curry_howard_isomorphism} のような対応が存在する。
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	264
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	265 \begin{center}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	266 \begin{table}[htbp]
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	267 \begin{tabular}{\|c\|\|c\|c\|} \hline
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	268 & natural deduction & 型付き $ \lambda $ 計算 \\ \hline \hline
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	269 hypothesis & $ A $ & 型 A を持つ変数 x \\ \hline
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	270 conjunction & $ A \land B $ & 型 A と型 B の直積型を持つ変数 x \\ \hline
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	271 disjunction & $ A \lor B $ & 型 A と型 B の直和型を持つ変数 x \\ \hline
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	272 implication & $ A \Rightarrow B $ & 型 A を取り型 B の変数を返す関数 f \\ \hline
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	273 \end{tabular}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	274 \caption{natural deuction と型付き $ \lambda $ 計算との対応}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	275 \label{tbl:curry_howard_isomorphism}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	276 \end{table}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	277 \end{center}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	278 % }}}
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	279
451c510825de Add natural deduction and curry-howard isomorphism atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 49 diff changeset	280 \section{依存型を持つ証明支援系言語 Agda}
51 6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	281 型システムを用いて証明を行なうことができる言語に Agda が存在する。% ref Agda のref
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	282 Agda は依存型という強力な型システムを持っている。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	283 依存型とは型も第一級オブジェクトとする型であり、型を引数に取る関数や値を取って型を返す関数、型の型などが記述できる。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	284 この節では Agda の文法的な紹介を行なう。 % ref pdf のアレ
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	285
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	286 まず Agda のプログラムは全てモジュールの内部に記述されるため、まずはトップレベルにモジュールを定義する必要がある。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	287 トップレベルのモジュールはファイル名と同一となる。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	288 例えば \verb/AgdaBasics.agda/ のモジュール名定義はリスト~\ref{src:agda-module}のようになる。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	289
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	290 \lstinputlisting[label=src:agda-module, caption=Agdaのモジュールの定義する] {src/AgdaBasics.agda}
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	291
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	292 また、Agda はインデントに意味を持つ言語であるため、インデントはきちんと揃える必要がある。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	293
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	294 まず Agda におけるデータ型について触れていく。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	295 Agda における型指定は $:$ を用いて行なう。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	296 例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	297
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	298 データ型は Haskell や ML に似て代数的なデータ構造のパターンマッチを扱うことができる
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	299 データ型の定義は \verb/data/ キーワードを用いる。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	300 \verb/data/キーワードの後に \verb/where/ 句を書きインデントを深くした後、値にコンストラクタとその型を列挙する。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	301 例えば Bool 型を定義するとリスト~\ref{src:agda-bool}のようになる。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	302
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	303 \lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda}
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	304
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	305 Bool はコンストラクタ \verb/true/ か \verb/false/ を持つデータ型である。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	306 Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型の型」である。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	307 Set は階層構造を持ち、型の型の型を指定するには Set1 と書く。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	308
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	309 関数の定義は Haskell に近い。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	310 関数名と型を記述した後に関数の本体を \verb/=/ の後に指定する。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	311 関数の型は単純型付き $ \lambda$ 計算と同様に $ \rightarrow $ を用いる。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	312 なお、$\rightarrow$に対しては糖衣構文 \verb/->/ も用意されている。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	313 引数は変数名で受けることもできるが、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	314 これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	315 例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	316
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	317 \lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda}
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	318
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	319 パターンマッチは全てのコンストラクタのパターンを含まなくてはならない。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	320 パターンマッチは上からマッチされていくため、優先順位が存在する。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	321 なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定したコンストラクタ以外となる。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	322 例えばリスト~\ref{src:agda-pattern}のnot は x には true しか入ることは無い。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	323
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	324 \lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda}
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	325
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	326 なお、マッチした値を変数として利用しない場合は \verb/_/ を用いて捨てることもできる。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	327
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	328 単純型で利用した自然数もデータ型として定義できる(リスト~\ref{src:agda-nat})。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	329 自然数のコンストラクタは2つあり、片方は自然数ゼロ、片方は自然数を取って後続数を返すものである。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	330 例えば3は \verb/suc (suc (suc zero))/ となる。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	331
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	332 \lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda}
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	333
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	334 自然数に対する演算は再帰関数として定義できる。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	335 例えば自然数どうしの加算は二項演算子\verb/+/としてリスト~\ref{src:agda-plus}のように書ける。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	336
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	337 この二項演算子は正確には中置関数である。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	338 前置や後置で定義できる部分を関数名に \verb/_/ として埋め込んでおくことで、関数を呼ぶ時にあたかも前置演算子のように振る舞う。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	339 また、Agda は関数が停止するかを判定できる。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	340 この加算の二項演算子は左側がゼロに対しては明かに停止する。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	341 左側が1以上の時の再帰時には \verb/suc n/ から \verb/n/へと減っているため、再帰で繰り返し減らすことでいつかは停止する。
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	342
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	343 \lstinputlisting[label=src:agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda}
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	344
6318c8f4bb8c Writing Agda description atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 50 diff changeset	345
49 7f1b5c33b282 Add agda.tex atton <atton@cr.ie.u-ryukyu.ac.jp> parents: diff changeset	346 \section{Reasoning}
7f1b5c33b282 Add agda.tex atton <atton@cr.ie.u-ryukyu.ac.jp> parents: diff changeset	347

Mercurial > hg > Papers > 2018 > nozomi-master

annotate paper/agda.tex @ 51:6318c8f4bb8c