# HG changeset patch # User soto # Date 1613120544 -32400 # Node ID bb7e9eaf9df86c37981d7487c705424f826921ab # Parent 9d7e993dadbd1445e95d769144f3eb48b34012c9 FIN chapter 2,3,6 diff -r 9d7e993dadbd -r bb7e9eaf9df8 paper/final_thesis.pdf Binary file paper/final_thesis.pdf has changed diff -r 9d7e993dadbd -r bb7e9eaf9df8 paper/final_thesis.tex --- 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} diff -r 9d7e993dadbd -r bb7e9eaf9df8 paper/tex/.#cbc.tex --- 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 diff -r 9d7e993dadbd -r bb7e9eaf9df8 paper/tex/.#rbt_intro.tex --- 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 diff -r 9d7e993dadbd -r bb7e9eaf9df8 paper/tex/agda.tex --- 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 を展開してしまうと、 diff -r 9d7e993dadbd -r bb7e9eaf9df8 paper/tex/cbc.tex --- 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が軽量継続を行っていると言える。 diff -r 9d7e993dadbd -r bb7e9eaf9df8 paper/tex/intro.tex --- 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} + diff -r 9d7e993dadbd -r bb7e9eaf9df8 paper/tex/rbt_intro.tex --- 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}