Mercurial > hg > Papers > 2015 > atton-thesis

--- a/agda.tex	Tue Feb 10 12:48:02 2015 +0900
+++ b/agda.tex	Tue Feb 10 15:30:01 2015 +0900
@@ -302,6 +302,7 @@
 % {{{ Agda による証明

 \section{Agda による証明}
+\label{section:agda}
 \ref{section:curry_howard_isomorphism}節において型を用いて証明を行なう手法を述べた。
 しかし、Haskell における型システムは証明を記述するために用いるものではない。
 よって、依存型を持つ証明支援言語 Agda を用いて証明を記述していく。
@@ -360,7 +361,138 @@

 % }}}

+\section{Reasoning}
+\label{section:reasoning}
+\ref{section:agda} 節ではAgdaにおける証明の手法について解説した。
+\ref{section:reasoning}節では Agda における証明の例として、自然数の加法の交換法則を証明する。

-\section{Reasoning}
+まずは自然数を定義する。
+今回用いる自然数の定義は以下のようなものである。
+
+\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}

-% TODO: nat かなー
+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 を用いる。
--- a/bibliography.tex	Tue Feb 10 12:48:02 2015 +0900
+++ b/bibliography.tex	Tue Feb 10 15:30:01 2015 +0900
@@ -8,6 +8,17 @@
 %書籍、論文、URLによって若干書き方が異なる。
 %URLを載せる人は参考にした年月日を最後に記入すること。

+% TODO: List
+
+% books
+% proofs and types
+% Introduction to higher order categorical logic
+% category theory for the computiong science
+
+% papers
+% notion of computations and monads
+% composing monads
+

 \bibitem{hoge}
 hoge
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/jlisting.sty	Tue Feb 10 15:30:01 2015 +0900
@@ -0,0 +1,216 @@
+\NeedsTeXFormat{LaTeX2e}
+\def\filedate{2006/02/20}
+\def\fileversion{0.2}
+\ProvidesPackage{jlisting}[\filedate\space\fileversion\space(Thor)]
+%
+\newcount\lst@nextchar
+\let\lst@@ProcessSpace\lst@ProcessSpace
+\def\lst@ProcessSpace#1{%
+   \lst@check@chartype{#1}%
+      \lst@@ProcessSpace
+      \lst@whitespacetrue}
+\let\lst@@ProcessLetter\lst@ProcessLetter
+\def\lst@ProcessLetter#1#2{%
+   \lst@check@chartype{#2}%
+      {\lst@@ProcessLetter{#1}}%
+      \relax}
+\let\lst@@ProcessDigit\lst@ProcessDigit
+\def\lst@ProcessDigit#1#2{%
+   \lst@check@chartype{#2}%
+      {\lst@@ProcessDigit{#1}}%
+      \relax}
+\let\lst@@ProcessOther\lst@ProcessOther
+\def\lst@ProcessOther#1#2{%
+   \lst@check@chartype{#2}%
+      {\lst@@ProcessOther{#1}}%
+      \relax}
+\let\lst@@ProcessTabulator\lst@ProcessTabulator
+\def\lst@ProcessTabulator#1{%
+   \lst@check@chartype{#1}%
+      \lst@@ProcessTabulator
+      \relax}
+\def\lst@check@chartype#1#2#3{%
+   \edef\@tempa{\lst@nextchar=`\string#1\relax}%
+   \afterassignment\remove@to@nnil
+   \@tempa\@nnil
+   #2%
+   \ifnum\lst@nextchar<\@cclvi
+      #3%
+   \else
+      \lst@ifletter \else \lst@OutputOther \fi
+      \lst@whitespacefalse
+      \expandafter\lst@AppendJchar
+   \fi
+   #1}
+\def\lst@AppendJchar#1#2{%
+   \lst@check@chartype{#2}%
+      {\advance\lst@length\@ne\lst@Append{#1}}%
+      \relax}
+\def\lst@check@chartype@BOL#1{%
+   \edef\@tempa{\lst@nextchar=`\string#1\relax}%
+   \afterassignment\remove@to@nnil
+   \@tempa\@nnil
+   \ifnum\lst@nextchar<\@cclvi\else
+      \lst@whitespacefalse
+      \expandafter\lst@AppendJchar
+   \fi
+   #1}
+\def\lst@InputListing#1{%
+   \begingroup
+      \lsthk@PreSet \gdef\lst@intname{#1}%
+      \expandafter\lstset\expandafter{\lst@set}%
+      \lsthk@DisplayStyle
+      \catcode\active=\active
+      \lst@Init\relax \let\lst@gobble\z@
+      \lst@SkipToFirst
+      \lst@ifprint \def\lst@next{\lst@get@filecontents{#1}}%
+      \else        \let\lst@next\@empty
+      \fi
+      \lst@next
+      \lst@DeInit
+   \endgroup}
+\newread\lst@inputfile
+\def\lst@get@filecontents#1{%
+   \let\lst@filecontents\@empty
+   \openin\lst@inputfile=#1\relax
+   \let\@lst@get@filecontents@prevline\relax
+   \lst@get@filecontents@loop
+   \closein\lst@inputfile
+   \lst@filecontents\empty}
+\def\lst@get@filecontents@loop{%
+   \read\lst@inputfile to\@lst@get@filecontents@currline
+   \ifx\@lst@get@filecontents@prevline\relax\else
+      \expandafter\expandafter\expandafter\def
+      \expandafter\expandafter\expandafter\lst@filecontents
+      \expandafter\expandafter\expandafter{%
+         \expandafter\lst@filecontents\@lst@get@filecontents@prevline}%
+   \fi
+   \let\@lst@get@filecontents@prevline\@lst@get@filecontents@currline
+   \ifeof\lst@inputfile\else
+      \expandafter\lst@get@filecontents@loop
+   \fi}
+%%% [$B$3$N=hM}$b!$AjEv6/0z$G$9!%(B]
+\def\lst@BOLGobble{%
+   \ifnum\lst@gobble>\z@
+      \@tempcnta\lst@gobble\relax
+      \expandafter\lst@BOLGobble@
+   \else
+      \expandafter\lst@check@chartype@BOL
+   \fi}
+\def\lst@BOLGobble@#1{%
+   \let\lst@next#1%
+   \ifx \lst@next\relax\else
+   \ifx \lst@next\lst@MProcessListing\else
+   \ifx \lst@next\lst@ProcessFormFeed\else
+   \ifx \lst@next\lstenv@backslash
+      \let\lst@next\lstenv@BOLGobble@@
+   \else
+      \let\lst@next\lst@BOLGobble@@
+      \ifx #1\lst@ProcessTabulator
+         \advance\@tempcnta-\lst@tabsize\relax
+         \ifnum\@tempcnta<\z@
+            \lst@length-\@tempcnta \lst@PreGotoTabStop
+         \fi
+      \else
+         \edef\@tempa{\lst@nextchar=`\string#1\relax}%
+         \@tempa
+         \ifnum\lst@nextchar<\@cclvi\else
+            \advance\@tempcnta\m@ne
+         \fi
+         \advance\@tempcnta\m@ne
+      \fi
+   \fi \fi \fi \fi
+   \lst@next}
+\def\lst@BOLGobble@@{%
+   \ifnum\@tempcnta>\z@
+      \expandafter\lst@BOLGobble@
+   \else
+      \expandafter\lst@check@chartype@BOL
+   \fi
+}
+%
+%    \begin{$B=$@5;v9`(B}{1.3}
+% $B$A$g$C$H$7$?=$@5(B
+\gdef\lst@breakProcessOther#1{\lst@ProcessOther#1}
+% $B%=!<%9%3!<%IL\<!$K$*$1$kJ8;z$HHV9f$N6u$-(B
+\let \l@lstlisting = \l@figure
+% $B%-%c%W%7%g%s$H%=!<%9%3!<%IL\<!$KBP$9$kF|K\8lBP1~(B
+\def\lstlistingname{$B%=!<%9%3!<%I(B}
+\def\lstlistlistingname{$B%=!<%9%3!<%IL\<!(B}
+%    \end{$B=$@5;v9`(B}
+\endinput
+%
+%#!platex
+\documentclass[papersize]{jsarticle}
+% Macros
+\IfFileExists{dvipdfmx.def}{%
+  \usepackage[dvipdfmx]{color,graphicx}%
+}{%
+  \usepackage[dvipdfm]{color,graphicx}%
+}
+\usepackage{listings}[2004/09/07]
+\usepackage{jlisting}[2006/02/20]
+\usepackage{url}
+\usepackage{verbatim}
+
+\makeatletter
+% Original Macros
+\def\email#1{\gdef\@email{\texttt{#1}}}
+\def\homepage#1{\gdef\@homepage{\texttt{#1}}}
+\def\mac#1{\textsf{#1}}
+\def\URL#1{\texttt{#1}}
+\def\src#1{\texttt{#1}}
+
+% Dvipdfmx.def
+\def\dvipdfmxDefi{http://tex.dante.jp/ok/dvipdfmx/}
+\def\dvipdfmxDefii{http://ftp.ktug.or.kr/KTUG/dvipdfmx/contrib/latex/}
+
+\IfFileExists{dvipdfmx.def}{%
+   \let \IfDvipdfmxDef = \empty \relax}{%
+   \typeout{^^Jget dvipdfmx.def at \dvipdfmxDefi^^J
+            or \dvipdfmxDefii^^J}%
+   \def\IfDvipdfmxDef{Get \src{dvipdfmx.def} at \URL \dvipdfmxDefii \\
+      or \URL \dvipdfmxDefi.}%
+}
+
+% Author Info
+\author   {Th\'or Watanabe\thanks \@email \space \thanks \@homepage}
+\title    {\mac{jlisting.sty}\\
+          ---Japanese Localized Patch File of \mac{listings}---}
+\email    {thor@tex.dante.jp}
+\homepage {http://tex.dante.jp/typo/}
+\date     {2006/02/20}
+
+\makeatother
+
+\begin{document}
+\maketitle
+%\IfDvipdfmxDef
+
+\section{$B$A$g$C$H$7$?@bL@(B}% Short Description
+
+$B1|B<@2I';a$N7G<(HD$N!VHFMQE*$JIbF0BN!W$H$$$&0lO"$N=q$-9~$_$+$i(B
+$BE>:\$7$^$7$?!#(B
+
+\begin{quote}
+ \url{http://http://cise.edu.mie-u.ac.jp/~okumura/texfaq/qa/21172.html}\\
+ \url{http://http://cise.edu.mie-u.ac.jp/~okumura/texfaq/qa/21184.html}\\
+ \url{http://http://cise.edu.mie-u.ac.jp/~okumura/texfaq/qa/21189.html}\\
+ \url{http://http://cise.edu.mie-u.ac.jp/~okumura/texfaq/qa/21197.html}
+\end{quote}
+
+ Copyright $B$O5H1JE/H~;a$K$"$k$N$@$H;W$$$^$9!%(B
+
+\section{$B99?7MzNr(B}% ChageLogs
+
+\begin{description}
+ \item[ver.~0.1 (2004/03/24)]
+   $B$H$j$"$($:8x3+!%(B
+ \item[ver.~0.2 (2006/02/20)]
+   \verb|\lst@breakProcessOther| $BL?Na$NDj5A$NDI2C!%(B
+\end{description}
+
+\section{$B%=!<%9%3!<%I(B}
+\par\narrowbaselines
+\verbatiminput{jlisting.sty}
+\end{document}
--- a/main.tex	Tue Feb 10 12:48:02 2015 +0900
+++ b/main.tex	Tue Feb 10 15:30:01 2015 +0900
@@ -3,7 +3,7 @@
 \usepackage{mythesis}
 \usepackage{multirow}
 \usepackage{here}
-\usepackage{listings}
+\usepackage{listings, jlisting}
 \usepackage{bussproofs}

 \setlength{\itemsep}{-1zh}
@@ -30,6 +30,7 @@

 \lstset{
   frame=single,
+  keepspaces=true,
   stringstyle={\ttfamily},
   commentstyle={\ttfamily},
   identifierstyle={\ttfamily},
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/equiv.agda	Tue Feb 10 15:30:01 2015 +0900
@@ -0,0 +1,1 @@
+data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/nat.agda	Tue Feb 10 15:30:01 2015 +0900
@@ -0,0 +1,5 @@
+module nat where
+
+data Nat : Set where
+  O : Nat
+  S : Nat -> Nat
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/nat_add.agda	Tue Feb 10 15:30:01 2015 +0900
@@ -0,0 +1,6 @@
+open import nat
+module nat_add where
+
+_+_ : Nat -> Nat -> Nat
+O + m     = m
+(S n) + m = S (n + m)
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/nat_add_sym.agda	Tue Feb 10 15:30:01 2015 +0900
@@ -0,0 +1,14 @@
+open import Relation.Binary.PropositionalEquality
+open import nat
+open import nat_add
+open ≡-Reasoning
+
+module nat_add_sym where
+
+add_sym : (n m : Nat) -> n + m ≡ m + n
+add_sym O       O   = refl
+add_sym O    (S m)  = cong S (add_sym O m)
+add_sym (S n)   O   = cong S (add_sym n O)
+add_sym (S n) (S m) = {!!}
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/nat_add_sym_reasoning.agda	Tue Feb 10 15:30:01 2015 +0900
@@ -0,0 +1,22 @@
+open import Relation.Binary.PropositionalEquality
+open import nat
+open import nat_add
+open ≡-Reasoning
+
+module nat_add_sym_reasoning where
+
+add_to_right : (n m : Nat) -> S (n + m) ≡ n + (S m)
+add_to_right n m = {!!}
+
+addSym : (n m : Nat) -> n + m ≡ m + n
+addSym O       O   = refl
+addSym O    (S m)  = cong S (add_sym O m)
+addSym (S n)   O   = cong S (add_sym n O)
+add_sym (S n) (S m) = begin
+  S (n + S m)    ≡⟨ cong S (add_sym n (S m)) ⟩
+  S (S (m + n))  ≡⟨ refl ⟩
+  S ((S m) + n)  ≡⟨ {!!} ⟩
+  S (m + S n)
+  ∎
+
+
--- a/src/product.agda	Tue Feb 10 12:48:02 2015 +0900
+++ b/src/product.agda	Tue Feb 10 15:30:01 2015 +0900
@@ -1,10 +1,10 @@
 module product where

-data _x_ (A B : Set) : Set where
-  <_,_> : A -> B -> A x B
+data _×_ (A B : Set) : Set where
+  <_,_> : A -> B -> A × B

-constructProduct : {A B : Set} -> A -> B -> A x B
+constructProduct : {A B : Set} -> A -> B -> A × B
 constructProduct a b = < a , b >

-patternMatchProduct : {A B : Set} -> A x B -> B
+patternMatchProduct : {A B : Set} -> A × B -> B
 patternMatchProduct (< a , b >) = b
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/three_plus_one.agda	Tue Feb 10 15:30:01 2015 +0900
@@ -0,0 +1,8 @@
+open import Relation.Binary.PropositionalEquality
+open import nat
+open import nat_add
+
+module three_plus_one where
+
+3+1 : (S (S (S O)))  +  (S O) ≡ (S (S (S (S O))))
+3+1 = refl
\ No newline at end of file