Mercurial > hg > Papers > 2015 > atton-thesis

changeset 75:0286bbcb59af

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mini fixes
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 17 Feb 2015 17:41:32 +0900
parents 3bfbf78cf502
children 3562c274db60
files paper/bibliography.tex paper/delta.tex paper/introduction.tex paper/main.pdf paper/main.tex paper/original_sources.tex paper/proof_deltaM.tex paper/reference.bib prepaper/reference.bib
diffstat 9 files changed, 59 insertions(+), 35 deletions(-) [+]
line wrap: on
line diff
--- a/paper/bibliography.tex	Tue Feb 17 16:56:18 2015 +0900
+++ b/paper/bibliography.tex	Tue Feb 17 17:41:32 2015 +0900
@@ -1,5 +1,7 @@
 % 参考文献
 \def\line{−\hspace*{-.7zw}−}
 
+\nocite{git, hg, agdawiki}
+
 \bibliographystyle{jplain}
 \bibliography{reference}
--- a/paper/delta.tex	Tue Feb 17 16:56:18 2015 +0900
+++ b/paper/delta.tex	Tue Feb 17 17:41:32 2015 +0900
@@ -11,9 +11,8 @@
 
 まずはプログラムを定義する。
 プログラムは型付けされた値と、値を値へと写像する関数のみで構成される。
-プログラムの実行は関数の値への適用とする。
-入出力といった、値や関数のみで表現できない計算はメタ計算とする。
-メタ計算を特定のデータ構造に対応させ、メタ計算が必要な関数は値をデータ構造へと写像することで入出力といった処理を実現する。
+プログラムの実行は関数の値への適用とし、入出力といった、値や関数で表現できない計算はメタ計算とする。
+メタ計算を特定のデータ構造に対応させ、メタ計算が必要な関数は値をデータ構造へと写像することで入出力処理を実現する。
 メタ計算とデータ構造の対応に用いる性質が Monad である。
 
 例えば、失敗する可能性があるメタ計算 T は式\ref{exp:partiality}のように定義できる。
@@ -23,8 +22,8 @@
     \label{exp:partiality}
 \end{equation}
 
-型 A の値に対応するメタ計算 T は、A と $ \bot $ の論理和として表現できる。
-計算に成功した際は A を返し、失敗した場合は $ \bot $ を返す。
+型 A の値に対応するメタ計算 T A は、A と $ \bot $ の論理和として表現できる。
+計算に成功した際は型 A の値を返し、失敗した場合は $ \bot $ を返す。
 
 ここで、失敗しない前提で作成されたプログラムに対して、失敗する可能性を表現するメタ計算を対応させる。
 プログラムは型 A の値x と、型 A の値を取り型 B の値を返す関数f, 型B の値を取り型Cの値を返す関数g によって構成されるとする(式\ref{exp:non_failure_program})。
@@ -34,16 +33,11 @@
     \label{exp:non_failure_program}
 \end{equation}
 
-ここで関数f は失敗する可能性があるとする。
-その時、f が失敗した場合の計算を考える必要がある。
-この計算の実現方法はいくつか存在する。
-計算g に失敗の判断を追加したり、例外機構により失敗を補足することで呼び出し元の関数で判断するなどがある。
+ここで関数f は失敗する可能性がある時、f をメタ計算によって拡張することで失敗を実現する。
 
-実現方法の1つとして、 Monad を用いたメタ計算がある。
-Monad により失敗した際の計算をメタ計算としてデータ構造に紐付ける。
 式\ref{exp:partiality} で定義したように、計算の成功は型 A 値を返し、失敗は $ \bot $ を返す。
+$ \bot $ となった時点で計算を中断するメタ計算を定義すれば、失敗を含めた関数を表現できる。
 計算に失敗した際に対応するメタ計算を定義し、関数をそのメタ計算で拡張することで失敗に対する処理が実現できる。
-例えば、 A に対してはそのまま関数の適用を行ない、 $ \bot $ に対しては $ \bot $ を返すようなメタ計算を定義することで、計算が失敗した時に計算を終了することができる。
 
 型A を持つx の値をメタ計算と対応して型 T A とした値を x' 、メタ計算による関数の拡張を * と記述すると、式\ref{exp:non_failure_program} の式は式\ref{exp:failure_program} のように書ける。
 
@@ -85,9 +79,7 @@
 
 \section{Haskell における Delta Monad の実装例}
 
-式\ref{exp:meta_computation_definition}のメタ計算をMonadで実現する。
-
-実装例としてプログラミング言語 Haskell を用いる。
+式\ref{exp:meta_computation_definition}のメタ計算をプログラミング言語 Haskell を実装し、プログラムの変更が表現できることを示す。
 
 まずは全てのプログラムのバージョンを表わすデータ型 Delta を考える。
 Delta の定義はリスト\ref{src:delta_constructor} とする。
@@ -99,6 +91,7 @@
 データ型 Delta はコンストラクタ Delta もしくは Mono によって構成される。
 バージョンが1である値は Mono によって構成される。
 プログラムを変更する際には、コンストラクタ Delta を用いて記述し、変更後の値と前のバージョンを持つ。
+Delta で記述することで、プログラムの変更に沿った長さ1以上のリスト構造が構築される。
 なお、a とは任意の型であり、Delta が任意の型の値に対してもデータ型を構築できることを示す。
 
 Haskell においてメタ計算とデータ型の対応は Monad によって行なうため、 Monad という型クラスが用意されている。
--- a/paper/introduction.tex	Tue Feb 17 16:56:18 2015 +0900
+++ b/paper/introduction.tex	Tue Feb 17 17:41:32 2015 +0900
@@ -15,4 +15,4 @@
 例えば、プログラムが変更された際に変更前と変更後のプログラムの挙動を比較する機構を提供できる。
 もし挙動の変化が望ましくない場合、信頼性が損なわれる変更だと変更時に判定できる。
 このように、プログラムの変更に対するメタ計算を定義することで信頼性を保ちながら開発することが可能となる。
-本研究ではプログラムの変更をメタ計算として定義し、それがMonad則を満たすことを証明する。
+本研究ではプログラムの変更をメタ計算として定義し、それがMonad則を満たすこと証明支援系Agda~\cite{agda}により証明する。
Binary file paper/main.pdf has changed
--- a/paper/main.tex	Tue Feb 17 16:56:18 2015 +0900
+++ b/paper/main.tex	Tue Feb 17 17:41:32 2015 +0900
@@ -3,6 +3,7 @@
 \usepackage{mythesis}
 \usepackage{multirow}
 \usepackage{here}
+\usepackage{url}
 \usepackage{cite}
 \usepackage{listings}
 \usepackage{bussproofs}
@@ -20,14 +21,8 @@
 
 % TODO
 %   卒論の修正点
-%       T Aの A の解説
-%           A が未定義
-%       式2.1 が未定義式っぽい
 %       実行例で Delta を使わないのも出す
 %       可能な変更の一覧
-%       bibliograph
-%           agda, hg, git
-%       ソフトウェアのバージョンにする
 %       where の解説が欲しい
 
 
--- a/paper/original_sources.tex	Tue Feb 17 16:56:18 2015 +0900
+++ b/paper/original_sources.tex	Tue Feb 17 17:41:32 2015 +0900
@@ -1,18 +1,19 @@
 \chapter{Haskell による Delta と DeltaM の定義と使用例のプログラム}
 \label{chapter:original_sources}
 
-\section{実験環境}
+\section{ソフトウェアのバージョン一覧}
 
-表\ref{table:environment}に実験環境におけるプログラムやライブラリのバージョンを示す。
+本論文で用いたプログラムやライブラリのバージョンを表\ref{table:environment}に示す。
 
 \begin{table}[htbp]
     \begin{center}
         \begin{tabular}{|c||c|} \hline
-            & version   \\ \hline \hline
-            Mac OS X & 10.9.5    \\ \hline
-            ghc      & 7.8.4     \\ \hline
-            Agda     & 2.4.2.2   \\ \hline
-            cabal    & 1.22.0.0  \\ \hline
+                        & version   \\ \hline \hline
+            Mac OS X    & 10.9.5    \\ \hline
+            ghc         & 7.8.4     \\ \hline
+            Agda        & 2.4.2.2   \\ \hline
+            agda-stdlib & 0.9       \\ \hline
+            cabal       & 1.22.0.0  \\ \hline
         \end{tabular}
         \label{table:environment}
         \caption{実験環境}
--- a/paper/proof_deltaM.tex	Tue Feb 17 16:56:18 2015 +0900
+++ b/paper/proof_deltaM.tex	Tue Feb 17 17:41:32 2015 +0900
@@ -1,15 +1,16 @@
 \chapter{DeltaM が Monad 則を満たす証明}
 \label{section:proof_deltaM}
 DeltaM に対する Monad 則の証明も Agda によって行なう。
-プログラム内部のDeltaのバージョン数は全て同じであるとし、1以上とする。
 
-内部に持つ型引数を持つ型M は Functor と Monad であるとする。
-基本的に同じ法則を用いて証明していくことになる。
-例えば $ \eta $ が natural transformation である証明には、 M の $ \eta $ が natural transformation である証明を用いる。
-また、同じ値に対して同じ振舞いをする関数を fmap しても同じであるという fmap-equiv という等式を導入している。
-これは高階関数に対する等式が定義できなかったためである。
+内部に持つ型 M は型引数を持ち、 Functor と Monad の制約を持つ。
+ある法則を証明する時は内部の M の証明を使って証明することになる。
+例えば DeltaM の$ \eta $ が natural transformation である証明には、 M の $ \eta $ が natural transformation である証明を用いる。
+
+また、証明に辺り fmap-equiv という等式を定義している。
+この等式は同じ値に対して同じ振舞いをする関数を fmap しても同じである等式である。
 
 DeltaM に対する Monad 則の証明がリスト\ref{src:deltaM_is_monad}である。
+プログラム内部のDeltaのバージョン数は全て同じであるとし、1以上とする。
 なお、Functor則に対する証明も行なったが省略する。
 
 
--- a/paper/reference.bib	Tue Feb 17 16:56:18 2015 +0900
+++ b/paper/reference.bib	Tue Feb 17 17:41:32 2015 +0900
@@ -59,3 +59,22 @@
   ftp         = {ftp://ftp.cs.nott.ac.uk/nott-fp/reports/yale/RR-1004.ps}
 }
 
+@misc{agda,
+    title = {The Agda wiki},
+    howpublished = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}},
+    note = {Accessed: 2015/02/17(Tue)}
+}
+
+
+@misc{git,
+    title = {Git},
+    howpublished = {\url{http://git-scm.com/}},
+    note = {Accessed: 2015/02/17(Tue)}
+}
+
+
+@misc{hg,
+    title = {Mercurial SCM},
+    howpublished = {\url{http://mercurial.selenic.com/}},
+    note = {Accessed: 2015/02/17(Tue)}
+}
--- a/prepaper/reference.bib	Tue Feb 17 16:56:18 2015 +0900
+++ b/prepaper/reference.bib	Tue Feb 17 17:41:32 2015 +0900
@@ -66,3 +66,16 @@
     note = {Accessed: 2015/02/17(Tue)}
 }
 
+
+@misc{git,
+    title = {Git},
+    howpublished = {\url{http://git-scm.com/}},
+    note = {Accessed: 2015/02/17(Tue)}
+}
+
+
+@misc{hg,
+    title = {Mercurial SCM},
+    howpublished = {\url{http://mercurial.selenic.com/}},
+    note = {Accessed: 2015/02/17(Tue)}
+}