Mercurial > hg > Papers > 2018 > ryokka-thesis
view final_main/chapter4.tex @ 4:12204a2c2eda
add .pdf and some section.
author | ryokka |
---|---|
date | Sun, 18 Feb 2018 21:43:41 +0900 |
parents | 2155c6ff589f |
children | eafc166804f3 |
line wrap: on
line source
%% Natural Deduction の説明をして、 Agda が命題を証明することができることを示す %% 章? 要る。。。かどうかは微妙な気がする。 「こういう話で Agda では証明ができます。」 %% で勝手に証明して証明できたね!はありだけど読み手があんまり嬉しくないかも。 %% ソレだとやっぱり自然演繹の話しして~同型対応でちゃんとつながってるね~じゃあ %% Agda で表現できるし証明できるねでいい感じかも \chapter{Agda における CbC の表現} % ツッコミどころさん % どうするのかは書けるけどなんでAgdaなの?みたいな話が飛んでくる 前章では Agda の文法について説明した。 本章では CbC と対応して CodeGear、 DataGear、 継続を Agda で表現する。 また、 Agda で継続を記述することで得た知見を示す。 \section{Agda での CodeGear 、 DataGear 、 継続の表現} %% 書くこと % CodeGearとDataGearのAgda上での定義 DataGear はレコード型で表現できるため、 Agda のレコード型をそのまま利用して定義 してく。 記述は~\ref{src:agda-ds}のようになる。 \lstinputlisting[label=src:agda-ds, caption=Agda における DataGear の定義] {src/DataSegment.agda.replaced} CodeGear は DataGear を受け取って DataGear を返すという定義であるため、 $ I \rightarrow O $ を内包する CodeGear 型のデータ型(~\ref{src:agda-cs})を定義する。 \lstinputlisting[label=src:agda-cs, caption= Agda における CodeGear 型の定義] {src/CodeSegment.agda.replaced} CodeGear 型を定義することで、 Agda での CodeGear の本体は Agda での関数そのもの と対応する。 % しかし、そのままだと再帰呼び出しの点で CbC との対応が失われてしまう。 % そのため、 Agda では \verb/goto/を利用できるのは関数の末尾のみという制約を設ける % 必要がある。 % この制約さえ満たせば、 CodeGear の実行は CodeGear 型から関数本体を取り出し、レコード型を持つ値を適用す ることに相当する。 CbC での軽量継続は \begin{itemize} \item 次に実行する CodeGear を指定する \item CodeGear に渡す DataGear を指定する \item 現在実行している CodeGear から制御を指定された CodeGear へと移す \end{itemize} の機能を持っている。 この機能を満たす関数はソースコード\ref{src:agda-goto} として定義されている。 \lstinputlisting[label=src:agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda.replaced} goto は CodeGear よりも一つ Level が上の Meta CodeGear にあたり、次に実行する CodeGear 型を受け取り、Input DataGear、 Output DataGear を返す。型になっている。 \section{Agda での Stack、 Tree の実装} \section{Agda における Interface の実装} %% 書くこと % stack の Interface部分と redBlackTree の Interface部分。 % interfaceとは?->cbcのとこに突っ込んでこっちは同様に〜で済ませたい Agda 側でも CbC 側と同様に interface を実装した。 interface は record で列挙し、ソースコード~\ref{src:agda-interface}のように紐付けることができる。 CbC とは異なり、 Agda では型を明記する必要があるため record 内に型を記述している。 例として Agda で実装した Stack 上の interface (ソースコード\ref{agda-interface})を見る。 Stack の実装は SingleLinkedStack(ソースコード\ref{agda-single-linked-stack}) として書かれている。それを Stack 側から interface を通して呼び出している。 ここでの interface の型は Stack の record 内にある pushStack や popStack などで、 実際に使われる Stack の操作は StackMethods にある push や popである。この push や pop は SingleLinkedStack で実装されている。 \lstinputlisting[label=src:agda-single-linked-stack, caption=Agda における Stack の実装] {src/AgdaSingleLinkedStack.agda.replaced} \lstinputlisting[label=src:agda-interface, caption=Agda における Interface の定義] {src/AgdaInterface.agda.replaced} interface を通すことで、実際には Stack の push では stackImpl と何らかのデータ a を取 り、 stack を変更し、継続を返す型であったのが、 pushStack では 何らかのデータ a を取り stack を変更 して継続を返す型に変わっている。 また、 Tree でも interface を記述した。 \lstinputlisting[label=src:agda-tree, caption=Tree Interface の定義]{src/AgdaTree.agda.replaced} interface を記述することによって、データを push する際に予め決まっている引数を省 略することができた。 また、 Agda で interface を記述することで CbC 側では意識していなかった型が、明確 化された。 % 元の push では 送り先の stack を関数に書く必要があり、異なる stack に push % する可能性があったが、 pushStack では紐付けた Stack に push することになり \section{継続を使った Agda における Test , Debug} Agda ではプログラムのコンパイルが通ると型の整合性が取れていることは保証できるが、必ず しも期待した動作をするとは限らない。そのため、本研究中に書いたプログラムが正しい動 作をしているかを確認するために行なった手法を幾つか示す。 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 今回は実験中にソースコード~\ref{src:agda-stack-test}のような Test を書いた。 この Test では Stack をターゲットにしていて、 Stack に1、 2の二つの$ \mathbb{N} $型のデー タを push した後、 pop2 Interface を使って Stack に入っている 1、 2 が Stack の FILO の定義通り 2、 1 の順で取り出せるかを確認するために作成した。 \lstinputlisting[label=agda-stack-test, caption=Agdaにおけるテスト]{src/AgdaStackTest.agda.replaced} 上の Test では、02 が 2つのデータを push し、 03 で 二つのデータを pop する pop2 を行っている。それらをまとめて記述したものが 04 で 2 回 push し、 2つのデータを pop する動 作が正しく行われていれば 04 は True を返し、 05 で記述された型通りに互いに等しくなる ため 05 が refl でコンパイルが通るようになる。 今回は、 pop2 で取れた値を確認するため 03 の後に 031、 032 の二つの作成した。 032 では 03 で扱っている値が Maybe であるため、 031 のような比較をする前に値が確 実に存在していることを示す補題である。 032 を通すことで 031 では 2つの値があり、 かつ$\mathbb{N}$型である事がわかる。 031 では直接取れた値が 2、 1 の順番で入って いるかを確認している。 この Test でエラーが出なかったことから、 Stack に1、2の二つのデータを pushする と、 push した値が Stack 上から消えることなく push した順番に取り出せることが分 かる。 また、継続を用いて記述することで関数の Test を書くことで計算途中のデータ内部をチェックするこ とができた。 ここでの \$ は \( \) をまとめる糖衣構文で、 \$ が書かれた一行を\(\)でくくること ができる。 % \ref{sintax}のようなコードを % \begin{lstlisting}[frame=lrbt,label=sintax,caption={\footnotesize 通常の継続の % コード}] % \end{lstlisting} % \begin{lstlisting}[frame=lrbt,label=sintax-sugar,caption={\footnotesize 糖衣構文 % を用いた継続のコード}] % \end{lstlisting} ソースコード~\ref{src:agda-tree-debug}のように関数本体に記述してデータを返し、C-c C-n (Compute normal form) で関数を評価すると関数で扱っているデータを見ることができる。 また、途中の計算で受ける変数名を変更し、 Return 時にその変更した変数名に変えるこ とで、計算途中のデータの中身を確認することができる。評価結果はソースコード内にコメントで記述した。 \lstinputlisting[label=src:agda-tree-debug, caption=Agdaにおけるテスト]{src/AgdaTreeDebug.agda.replaced} 今回、この手法を用いることで複数の関数を組み合わせた findNode 関数内に異常があるこ とが分かった。 %getRedBlackTree の関数に % \lstinputlisting[label=agda-Debug, caption=Agdaにおけるデバッグ]{src/AgdaTreeDebug.agda.replaced} % Tree全然載せてないけどどうしよ。。。どこに書こうかは考えておきましょう