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

comparison agda.tex @ 26:de3397af1f8d

Temporary save

author	Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date	Tue, 10 Feb 2015 15:30:01 +0900
parents	a0d91fbf4876
children	e30a02baba55

comparison

equal deleted inserted replaced

-:a0d91fbf4876
+:de3397af1f8d
 % }}}
 % {{{ Agda による証明
 \section{Agda による証明}
+\label{section:agda}
 \ref{section:curry_howard_isomorphism}節において型を用いて証明を行なう手法を述べた。
 しかし、Haskell における型システムは証明を記述するために用いるものではない。
 よって、依存型を持つ証明支援言語 Agda を用いて証明を記述していく。
 依存型とは値に依存した型を作ることができる型であり、非常に表現能力が高い。
 \verb/A x B/ 型から B を取るため、\verb/A x B/ 型の変数を直接束縛せずにコンストラクタで分解し、a と b に束縛することで A と B が得られる。
 そのため、 patternMathProduct は $ \land 2 \mathcal{E} $ そのものである。
 % }}}
 \section{Reasoning}
+\label{section:reasoning}
-% TODO: nat かなー
+\ref{section:agda} 節ではAgdaにおける証明の手法について解説した。
+\ref{section:reasoning}節では Agda における証明の例として、自然数の加法の交換法則を証明する。
+まずは自然数を定義する。
+今回用いる自然数の定義は以下のようなものである。
+\begin{itemize}
+\item 0 は自然数である
+\item 任意の自然数には後続数が存在する
+\item 0 はいかなる自然数の後続数でもない
+\item 異なる自然数どうしの後続数は異なる ($ n \neq m \rightarrow S n \neq S m $)
+\item 0がある性質を満たし、aがある性質を満たせばその後続数 S(n) も自然数である
+\end{itemize}
+この定義は peano arithmetic における自然数の定義である。
+Agda で自然数型 Nat を定義するとリスト \ref{src:nat} のようになる。
+\begin{table}[html]
+\lstinputlisting[label=src:nat, caption=Agda における自然数型 Nat の定義] {src/nat.agda}
+\end{table}
+自然数型 Nat は2つのコンストラクタを持つ。
+\begin{itemize}
+\item O
+引数を持たないコンストラクタ。これが0に相当する。
+\item S
+Nat を引数に取るコンストラクタ。これが後続数に相当する。
+\end{itemize}
+よって、数値の 3 は \verb/S (S (S O))/ のように表現される。
+Sの個数が数値に対応する。
+次に加算を定義する(リスト\ref{src:nat_add})。
+\begin{table}[html]
+\lstinputlisting[label=src:nat_add, caption=Agdaにおける自然数型に対する加算の定義] {src/nat_add.agda}
+\end{table}
+加算は中置関数 \verb/_+_/ として定義する。
+2つの Nat を取り、Natを返す。
+パターンマッチにより処理を変える。
+0に対して m 加算する場合は m であり、 n の後続数に対して m 加算する場合は n に m 加算した数の後続数とする。
+S を左の数から右の数へ1つずつ再帰的に移していくような加算である。
+例えば 3 + 1 といった計算は (S (S (S O))) + (S O) のように記述される。
+ここで 3 + 1 が 4と等しいことの証明を行なう。
+等式の証明には agda の standard library における Relation.Binary.Core の定義を用いる。
+\begin{table}[html]
+\lstinputlisting[label=src:equiv, caption= Relation.Binary.Core による等式を示す型 $ \equiv $] {src/equiv.agda}
+\end{table}
+等式は等式を示すデータ型 $ \equiv $ により定義される。
+$ \equiv $ は同じ両辺が同じ項に簡約される時にコンストラクタ refl で構築できる。
+実際に 3 + 1 = 4 の証明は refl で構成できる(リスト\ref{src:three_plus_one})。
+\begin{table}[html]
+\lstinputlisting[label=src:three_plus_one, caption= Agda における 3 + 1 の結果が 4 と等しい証明] {src/three_plus_one.agda}
+\end{table}
+3+1 という1つの関数を定義し、その型として証明すべき式 \verb/(S (S (S O))) + (S O)≡(S (S (S (S O))))/ を記述する。
+そして証明を関数の定義として記述する。
+今回は \verb/_+_/ 関数の定義により \verb/ (S (S (S (S O)))) / に簡約されるためにコンストラクタ refl が証明となる。
+$ \equiv $ によって証明する際、必ず同じ式に簡約されるとは限らないため、いくつかの操作が Relation.Binary.PropositionalEquality に定義されている。
+\begin{itemize}
+\item sym  : $ x \equiv y \rightarrow y \equiv x $
+等式が証明できればその等式の左辺と右辺を反転しても等しい。
+\item cong : $ f \rightarrow x \equiv y \rightarrow f x \equiv f y $
+証明した等式に同じ関数を与えても等式は保たれる。
+\item trans : $ x \equiv y \rightarrow y \equiv z \rightarrow x \equiv z $
+2つの等式に表れた同じ項を用いて2つの等式を繋げた等式は等しい。
+\end{itemize}
+ではこれから nat の加法の交換法則を証明していく(リスト\ref{src:nat_add_sym})。
+\begin{table}[html]
+\lstinputlisting[label=src:nat_add_sym, caption= Agda における加法の交換法則の証明] {src/nat_add_sym.agda}
+\end{table}
+証明する式は $ n + m \equiv m + n $ である。
+n と m は Nat であるため、それぞれがコンストラクタ O か S により構成される。
+そのためにパターンは4通りある。
+\begin{itemize}
+\item n = O, m = O
++ の定義により、 O に簡約されるため refl で証明できる。
+\item n = O, m = S m
+$ O + (S m) \equiv (S m) + O $  を証明することになる。
+この等式は + の定義により $ O + (S m) \equiv S (m + O) $ と変形できる。
+$ S (m + O) $ は $ m + O $ に S を加えたものであるため、 cong を用いて再帰的に \verb/add_sym/ を実行することで証明できる。
+この2つの証明はこのような意味を持つ。
+n が 0 であるとき、 m も 0 なら簡約により等式が成立する。
+n が 0 であるとき、 m が 0 でないとき、 m は後続数である。
+よって m が (S x) と書かれる時、 x は m の前の値である。
+前の値による交換法則を用いてからその結果の後続数も + の定義により等しい。
+ここで、 \verb/add_sym/ に渡される m は1つ値が減っているため、最終的には n = 0, m = 0 である refl にまで簡約され、等式が得られる。
+\item n = S n, m = O
+$ (S n) + O \equiv O + (S n) $ を証明する。
+この等式は + の定義により $ S (n + O) \equiv (S n) $ と変形できる。
+さらに変形すれば $ S (n + O) \equiv S (O + n) $ となる。
+よって \verb/add_sym/ により O と n を変換した後に cong で S を加えることで証明ができる。
+ここで、 $ O + n  \equiv n $ は + の定義により自明であるが、$ n + O \equiv n $ をそのまま導出できないことに注意して欲しい。
++ の定義は左側の項から S を右側の項への移すだけであるため、右側の項への演算はしない。
+\item n = S n, m = S m
+3つのパターンは証明したが、このパターンは少々長くなるため別に解説することとする。
+\end{itemize}
+3 つのパターンにおいては refl や cong といった単純な項で証明を行なうことができた。
+しかし長い証明になると refl や cong といった式を trans で大量に繋げていく必要性がある。
+長い証明を分かりやすく記述するために $ \equiv $-Reasoning を用いる。

Mercurial > hg > Papers > 2015 > atton-thesis

comparison agda.tex @ 26:de3397af1f8d