Binary file paper/final_thesis.pdf has changed

--- a/paper/final_thesis.tex	Thu Feb 11 23:36:12 2021 +0900
+++ b/paper/final_thesis.tex	Fri Feb 12 18:02:24 2021 +0900
@@ -53,6 +53,7 @@
   lineskip=-0.1\zw,
   escapechar={@},
 }
+\def\lstlistingname{ソースコード}
 
 % bibtex
 \usepackage[backend=biber, style=numeric, bibstyle=ieee]{biblatex}

--- a/paper/tex/.#cbc.tex	Thu Feb 11 23:36:12 2021 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-soto@Szeleta.local.353
\ No newline at end of file

--- a/paper/tex/.#rbt_intro.tex	Thu Feb 11 23:36:12 2021 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-soto@Szeleta.local.353
\ No newline at end of file

--- a/paper/tex/agda.tex	Thu Feb 11 23:36:12 2021 +0900
+++ b/paper/tex/agda.tex	Fri Feb 12 18:02:24 2021 +0900
@@ -9,10 +9,10 @@
 は記述したプログラムを証明することができる。
 
 \section{Agdaの基本}
+本節ではAgdaの基本事項についてソースコードを例に出しながら説明を行う。
 
 \subsection{関数の実装}
-本節ではAgdaの基本事項について \coderef{plus} を例として解説する。
-
+Agdaでの関数の 定義方法について \coderef{plus} を例として解説する。
 基本事項として、$ \mathbb{N} $ というのは自然数 (Natulal Number) のことである。
 また - (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、
 ここでは関数を実行した際の例を記述している。
@@ -24,10 +24,10 @@
 この : の前が関数名になり、その後ろがその関数の定義となる。
 : 以降の (x y : $ \mathbb{N} $) は関数は x, y の自然数2つを受けとるという意味になる。
 $ \rightarrow $ 以降は関数が返す型を記述している。
-まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、
+まとめると、この関数 plus は、型が自然数である2つの変数 x, y を受け取り、
 自然数を返すという定義になる。
 
-関数の定義をしたコードの直下で実装を行うのが常である。
+Agda では関数の定義をしたコードの直下で実装を行うのが常である。
 関数名を記述した後に引数を記述して受け取り、= (イコール) 以降で
 引数に対応した実装をする。
 
@@ -51,15 +51,17 @@
 利点としては、直感的な記号論理の記述ができる。
 以下、記号論理は基本的に三項演算子を使用して記述する。
 
+\begin{comment}
 \subsection{Agdaにおけるラムダ計算}
 \lambda
+\end{comment}
 
 \subsection{Data 型の実装}
 Deta 型とは分岐のことである。
 そのため、それぞれの動作について実装する必要がある。
-例として既出で Data 型である $ \mathbb{N} $ の実装を \coderef{Nat} に示す。
+例として既出の Data 型である $ \mathbb{N} $ の実装を \coderef{Nat} に示す。
 
-\lstinputlisting[label=Nat, caption=Nat] {src/agda/Nat.agda}
+\lstinputlisting[label=Nat, caption=Natural の定義] {src/agda/Nat.agda}
 
 実装から、$ \mathbb{N} $ という型は zero と suc の2つのコンストラクタを持っていることが分かる。
 それぞれの仕様を見てみると、zeroは $ \mathbb{N} $ のみであるが、
@@ -72,13 +74,13 @@
 言い換えればパターンマッチをする必要があると言える。
 これは puls 関数で suc 同士の場合と、zeroが含まれる場合の両方を実装していることの説明となる。
 
-\subsection{パターンマッチ}
+% \subsection{パターンマッチ}
 
 \subsection{Record 型の実装}
 Record 型とはオブジェクトあるいは構造体ののようなものである。
 \coderef{And}は AND の関数となる。p1で前方部分が取得でき、p2で後方部分が取得できる。
 
-\lstinputlisting[label=And, caption=And] {src/agda/And.agda}
+\lstinputlisting[label=And の定義, caption=And] {src/agda/And.agda}
 
 また、Agda の関数定義では\_(アンダースコア)で囲むことで三項演算子を定義することができる。
 
@@ -86,7 +88,7 @@
 定義は「AならばB」かつ「BならばC」なら「AならばC」となる。
 \coderef{syllogism}を以下に示す。
 
-\lstinputlisting[label=syllogism, caption=syllogism] {src/agda/syllogism.agda}
+\lstinputlisting[label=syllogism の実装, caption=syllogism] {src/agda/syllogism.agda}
 
 コードの解説をすると、引数として x と a が関数に与えられている。
 引数 x の中身は ((A $ \rightarrow $ B) ∧ (B $ \rightarrow $ C)) 、引数 a の中身
@@ -94,7 +96,9 @@
 \_∧\_.p2 x で (B $ \rightarrow $ C) であるため、これに B を与えると C が取得できる。
 よって A を与えて C を取得することができたため、三段論法を定義できた。
 
-\section{Agdaで使用するもの}
+\section{本論で使用する Agda の記法}
+本論では、ソースコードを出しながら実施内容について述べるが、
+特殊な記法を用いている場合があるので、前もって解説をする。
 
 \subsection{Agdaの省略記法}
 Recode が入力された場合のことを考える。この際、入力時に record を展開してしまうと、

--- a/paper/tex/cbc.tex	Thu Feb 11 23:36:12 2021 +0900
+++ b/paper/tex/cbc.tex	Fri Feb 12 18:02:24 2021 +0900
@@ -1,9 +1,8 @@
 \chapter{Continuetion based C}
 
-\section{Continuation based C}
 CbC とはC言語からループ制御構造とサブルーチンコールを取り除き、
 継続を導入したC言語の下位言語である。継続呼び出しは引数付き goto 文で表現される。
-また、CodeGear を処理の単位、DataGear をデータの単位として記述するプログラミング言語である。
+また、処理の単位を Code Gear , データの単位を DataGear として記述するプログラミング言語である。
 CbC のプログラミングでは DataGear を CodeGear で変更し、その変更を次の CodeGear に渡して処理を行う。
 
 \section{Code Gear / Data Gear}
@@ -33,12 +32,28 @@
 
 \section{CbC と C言語の違い}
 同じ仕様でCbCとC言語で実装した際の違いを、実際のコードを元に比較する。
-以下はフィボナッチ数列の n 番目を求める CbC と C言語のソースコードである。
+比較するにあたり、再起処理が含まれるコードの例として、
+フィボナッチ数列の n 番目を求めるコードを挙げる。
+C言語で記述したものが\coderef{fib_c}。CbCで記述したものが\coderef{fib_cbc}になる。
+CbCは実行を継続するため、 return を行えない。そのためC言語での実装も return を書
+かず関数呼び出しを行い、最後にexitをして実行終了するように記述している。
 
-\lstinputlisting[label=plus, caption=plus, firstline=5] {src/cbc/fib.c}
-\lstinputlisting[label=plus, caption=plus, firstline=5] {src/cbc/fib.cbc}
+\lstinputlisting[label=fib_c, caption=C言語で記述した フィボナッチ数列の n 番目
+を求めるコード, firstline=5] {src/cbc/fib.c}
+\lstinputlisting[label=fib_cbc, caption=CbCで記述した フィボナッチ数列の n 番目
+を求めるコード, firstline=5] {src/cbc/fib.cbc}
 
 軽量実装になっているのか、上記のコードをアセンブラ変換した結果を見て確認する。
+全てを記載すると長くなるので、アセンブラ変換した際のfib関数のみを記載する。
+C言語で記述した\coderef{fib_c}をアセンブラ変換した結果が\coderef{c-ass}。
+CbCで記述した\coderef{fib_cbc}をアセンブラ変換した結果が\coderef{cbc-ass}になる。
 
-\lstinputlisting[label=c-ass, caption=cで記述した際のfib()のアセンブラ] {src/cbc/c.out}
-\lstinputlisting[label=cbc-ass, caption=cbcで記述した際のfib()のアセンブラ] {src/cbc/cbc.out}
+比較すると、fib 関数の内部で再度 fib 関数を呼び出す際、
+C言語で実装した\coderef{c-ass}の30行目では callq で fib 関数を呼び出している。
+対して CbC で実装した\coderef{cbc-ass}の32行目では、 jmp により fib 関数に移動
+している。
+
+\lstinputlisting[label=c-ass, caption=cで記述した際の fib 関数のアセンブラ] {src/cbc/c.out}
+\lstinputlisting[label=cbc-ass, caption=cbcで記述した際の fib 関数のアセンブラ] {src/cbc/cbc.out}
+
+以上のことから CbCが軽量継続を行っていると言える。

--- a/paper/tex/intro.tex	Thu Feb 11 23:36:12 2021 +0900
+++ b/paper/tex/intro.tex	Fri Feb 12 18:02:24 2021 +0900
@@ -32,6 +32,7 @@
 これらのことから、CbC に対応するように Agda で RedBlackTree を記述し、
 Hoare Logic により検証を行うことを目指す。
 
+\begin{comment}
 \section{論文の構成}
 本論文は以下の流れで構成されている。
 
@@ -47,6 +48,8 @@
 \item 第9章は, 本研究におけるまとめと今後の課題について述べる
 \end{itemize}
 
+\end{comment}
 
 
 
+

--- a/paper/tex/rbt_intro.tex	Thu Feb 11 23:36:12 2021 +0900
+++ b/paper/tex/rbt_intro.tex	Fri Feb 12 18:02:24 2021 +0900
@@ -1,29 +1,36 @@
 \chapter{Red Black Tree}
 
+実装を行う Red Black Tree の説明を行う。
+Red Black Tree は 木構造の基本操作である Insert(挿入)、Delete(削除)、Search(検索)の
+いずれに置いても最悪実行時間が $O(log \: n)$であり、データ構造のうちで最善のものの一つである。
+そのため、実用的なデータ構造として知られている。
+
 \section{Tree}
 Tree (木構造)とは、非常に有用なデータ構造である。
-下図の○の部分を node (節) と呼び、top node を root(根) と呼ぶ。
+\figref{tree}の○の部分を node (節) と呼び、top node を root(根) と呼ぶ。
 特に、根を持つ木構造のことを強調して、Rooted Tree (根付き木) と呼ぶ事がある。
 
-\begin{figure}[H]
-  \begin{center}
-    \includegraphics[height=4.5cm]{pic/rbt/tree.pdf}
-  \end{center}
-  \caption{RedBlackTree の一例}
-  \label{rbtree}
-\end{figure}
+\section{Binary Tree}
+各 node からすぐ下に辺で結ばれている node を
+その node の child またはson (子あるいは子供)と呼ぶ。
+child 側から上の辺を parent (親) と呼ぶ。
+\figref{bt}のように、各 node が持つ child が高々2つである Tree を Binary Tree (2分木)と呼ぶ。
 
-\section{Binary Tree}
-各 node からすぐ下に辺で結ばれている node をその node の child またはson (子ある
-いは子供)と呼ぶ。 child 側から上の辺を parent (親) と呼ぶ。
-下図のように、各 node が持つ child が高々2つである Tree を Binary Tree (2分木)と呼ぶ。
-
-\begin{figure}[H]
-  \begin{center}
-    \includegraphics[height=4.5cm]{pic/rbt/bt.pdf}
-  \end{center}
-  \caption{RedBlackTree の一例}
-  \label{rbtree}
+\begin{figure}[htbp]
+  \begin{minipage}{0.5\hsize}
+    \begin{center}
+      \includegraphics[height=4.5cm]{pic/rbt/tree.pdf}
+    \end{center}
+  \caption{Tree の例}
+  \label{tree}
+  \end{minipage}
+  \begin{minipage}{0.5\hsize}
+    \begin{center}
+      \includegraphics[height=4.5cm]{pic/rbt/bt.pdf}
+    \end{center}
+    \caption{Binary Tree の例}
+    \label{bt}
+  \end{minipage}
 \end{figure}
 
 \section{Binary Search Tree}
@@ -31,19 +38,22 @@
 
 $左側の子孫にある要素 < 親 < 右側の子孫にある要素$
 
+例を以下\figref{bst}に示す
+
 \begin{figure}[H]
   \begin{center}
     \includegraphics[height=7.5cm]{pic/rbt/bst.pdf}
   \end{center}
-  \caption{RedBlackTree の一例}
-  \label{rbtree}
+  \caption{Binary Search Tree の一例}
+  \label{bst}
 \end{figure}
 
-
 \section{RedBlackTree}
 RedBlackTree (または赤黒木)とは平衡2分探索木の一つである。
-2分探索木の点にランクという概念を追加し、そのランクの違いを赤と黒の色で分け、以下の定義に基づくように
-木を構成した物である。図では省略しているが、値を持っている点の下に黒色の空の葉があり、それが外点となる。
+2分探索木の点にランクという概念を追加し、そのランクの違いを赤と黒の色で分け、
+以下の定義に基づくように
+木を構成した物である。図では省略しているが、値を持っている点の下に黒色の空の葉があり、
+それが外点となる。
 
 \begin{enumerate}
   \item 各点は赤か黒の色である。
@@ -51,33 +61,36 @@
   \item 外点(葉。つまり一番下の点)は黒である。
   \item 任意の点から外点までの黒色の点はいずれも同数となる。
 \end{enumerate}
-参考となる\figref{rbtree}を以下に示す。上記の定義を満たしていることが分かる。
+参考となる\figref{rbt}を以下に示す。上記の定義を満たしていることが分かる。
 
 \begin{figure}[H]
   \begin{center}
-    \includegraphics[height=7.5cm]{pic/rbt/rbt.pdf}
+    \includegraphics[height=6.5cm]{pic/rbt/rbt.pdf}
   \end{center}
-  \caption{RedBlackTree の一例}
-  \label{rbtree}
+  \caption{Red Black Tree の一例}
+  \label{rbt}
 \end{figure}
 
-\section{Left Learing Red Black Tree}
+\section{Left Learning Red Black Tree}
 Left Learing Red Black Tree とは Red Black Tree の変形である。
 Red Black Tree の 仕様を満たしながら、実装が容易である。
 
-以下の図のように、
-赤色の node は parent から見て左の node にしか 現れない Red Black Tree となる。
+\figref{rbt}に入っていた値を Left Learning Red Black Tree に適応した場合を
+\figref{llrbt}に示す。
+Left Learning Red Black Tree では赤色の node は parent から見て
+左の node にしか 現れない Red Black Tree となる。
 これにより、パターンマッチの分岐を減らす事ができ、実装が容易になる。
 
-本来の Red Black Tree の実装は困難であるため、本論では Red Black Tree の仕様を満たしている
+本来の Red Black Tree の実装は困難であるため、
+本論では Red Black Tree の仕様を満たしている
 Left Learning Red Black Tree を検証する。
 
 \begin{figure}[H]
   \begin{center}
     \includegraphics[height=7.5cm]{pic/rbt/llrbt.pdf}
   \end{center}
-  \caption{RedBlackTree の一例}
-  \label{rbtree}
+  \caption{Left Learning Red Black Tree の一例}
+  \label{llrbt}
 \end{figure}