# HG changeset patch # User ryokka # Date 1524474706 -32400 # Node ID 4312a27022d10b5f951aeb12ca9b826f5a32eb4f # Parent 341b4c04597f646e238236c30d200a40b31fdc3b fix diff -r 341b4c04597f -r 4312a27022d1 Paper/auto/sigos.el --- a/Paper/auto/sigos.el Sun Apr 22 20:53:49 2018 +0900 +++ b/Paper/auto/sigos.el Mon Apr 23 18:11:46 2018 +0900 @@ -4,7 +4,7 @@ (TeX-add-to-alist 'LaTeX-provided-class-options '(("ipsjpapers" "techrep"))) (TeX-add-to-alist 'LaTeX-provided-package-options - '(("graphicx" "dvipdfmx"))) + '(("graphicx" "dvipdfmx") ("otf" "deluxe" "multi") ("inputenc" "utf8x"))) (add-to-list 'LaTeX-verbatim-environments-local "lstlisting") (add-to-list 'LaTeX-verbatim-macros-with-braces-local "path") (add-to-list 'LaTeX-verbatim-macros-with-braces-local "url") @@ -14,20 +14,24 @@ (add-to-list 'LaTeX-verbatim-macros-with-delims-local "lstinline") (TeX-run-style-hooks "latex2e" - "dummy" "ipsjpapers" "ipsjpapers10" "graphicx" - "url" "listings" - "jlisting" "enumitem" - "bussproofs" - "amsmath" "multirow" "here" + "ucs" + "autofe" + "fancyvrb" + "ascmac" + "otf" + "url" "cite" "amssymb" + "amsmath" + "colonequals" + "inputenc" "caption") (LaTeX-add-labels "fig:cgdg" diff -r 341b4c04597f -r 4312a27022d1 Paper/sigos.pdf Binary file Paper/sigos.pdf has changed diff -r 341b4c04597f -r 4312a27022d1 Paper/sigos.tex --- a/Paper/sigos.tex Sun Apr 22 20:53:49 2018 +0900 +++ b/Paper/sigos.tex Mon Apr 23 18:11:46 2018 +0900 @@ -1,17 +1,28 @@ \documentclass[techrep]{ipsjpapers} \usepackage[dvipdfmx]{graphicx} -\usepackage{url} -\usepackage{listings,jlisting} + +\usepackage{listings} \usepackage{enumitem} -\usepackage{bussproofs} -\usepackage{amsmath} +% \usepackage{bussproofs} \usepackage{multirow} \usepackage{here} +\usepackage{ucs} +\usepackage{autofe} +\usepackage{fancyvrb} +\usepackage{ascmac} +\usepackage[deluxe, multi]{otf} +\usepackage{url} \usepackage{cite} \usepackage{listings} \usepackage{amssymb} -%\usepackage{ucs} -%\usepackage[utf8x]{inputenc} +\usepackage{amsmath} +\usepackage{colonequals} +\usepackage[utf8x]{inputenc} + +\DeclareUnicodeCharacter{8852}{$\sqcup$} +\DeclareUnicodeCharacter{8909}{$\simeq$} + +% \uc@dclc{8852}{default}{\ensuremath{\sqcup}} \lstset{ language=C, @@ -38,10 +49,11 @@ \usepackage{caption} \captionsetup[lstlisting]{font={small,tt}} -\input{dummy.tex} %% Font +% \input{dummy.tex} %% Font % ユーザが定義したマクロなど． \makeatletter +% \def<\UTF{2294}>{$\sqcup$} \begin{document} @@ -90,7 +102,7 @@ % 本文はここから始まる % Introduce -% Code Gear は関数に比べて細かく分割されているのでメタ計算をより柔軟に記述できる。 +% Code Gear は関数に比べて細かく分割されているのでメタ計算をより柔軟に記述できる。 % 研究目的 @@ -222,6 +234,10 @@ 時の型は \verb+A -> (A -> B)+ のように考えられる。 前節に出てきた pushStack の型(Code \ref{push-stack})はこの例である。 pushStack の型の本体は Code \ref{push-stack-func}のようになる。 +Code \ref{push-stack-funk} では\verb+\+の表記が出ている。これは$\lambda$式で初め +の pushStack で返した stack である s1 を受け取り、次の関数へ渡している。 Agda の +$\lambda$式では\verb+\+の他に\verb+λ+で表記することもできる。 +\verb++ \begin{lstlisting}[caption=pushStack の関数定義,label=push-stack-func] pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } )) @@ -236,8 +252,8 @@ \verb+record+ の定義の例として Stack のデータを操作する際に必要なレコード型のデータ \verb+Element+ (Code \ref{element-impl})を例とする。 -\verb+Element+ は単方向のリスト構造になっており、 \verb+datum+ に格納するデータ、 -\verb+next+ に次のデータを持っている。 +\verb+Element+ は単方向のリスト構造になっており、 \verb+datum+ に格納する任意の +型のデータ、\verb+next+ に次のElement型のデータを持っている。 \begin{lstlisting}[caption=Element の定義,label=element-impl] record Element {l : Level} (a : Set l) : Set l where @@ -248,94 +264,130 @@ next : Maybe (Element a) \end{lstlisting} -% 引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。 -% これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなもので - %% element の定義、縦棒　| の定義 %% SingleLinkedStack の説明に必要なものだけ +% パターンマッチの説明、 | の定義、説明用のあれ。 %% push と pop だけ書いて必要なものだけ説明する %% testStack08 を説明する。 -パターンマッチの説明、 | の定義、説明用のあれ。 +引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。 +これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。 +例として、 popStack の実装である popSingleLinkedStack を使う。 + +popSingleLinkedStack では \verb+stack+、 \verb+cs+ の2つの引数を取り、 +\verb+with+キーワードの後に\verb+Maybe+型の\verb+top+でパターンマッチしている。 +\verb+Maybe+型は\verb+nothing+と\verb+Just+のどちらかを返す。そのため、両方のパ +ターンにマッチしている必要がある。 +パターンマッチの記述では関数名、引数、を列挙して\verb+|+の後に \verb+パターン名 =+ +で挙動を書く場合と、 Code \ref{pattern-match}のように、\verb+... |+で関数名、引数 +を省略して\verb+パターン名 =+で挙動を書く方法がある。 + +また、Agda では特定の関数内のみで利用できる関数を \verb+where+ 句で記述できる。 +スコープは \verb+where+ 句が存在する関数内部のみであるため、名前空間が汚染させる +ことも無い。 +\verb+where+ 句は利用したい関数の末尾にインデント付きで \verb+where+ キーワード +を記述し、改行の後インデントをして関数内部で利用する関数を定義する。 + +\begin{lstlisting}[caption=パターンマッチの例,label=pattern-match] +popSingleLinkedStack stack cs with (top stack) +... | Nothing = cs stack Nothing +... | Just d = cs stack1 (Just data1) + where + data1 = datum d + stack1 = record { top = (next d) } +\end{lstlisting} -\begin{lstlisting}[caption=test8,label=test8] +pushStack と popStack を使った証明の例は Code\ref{push-pop}のようになる。 +ここでは、stack に対し push を行なった直後に pop を行うと取れるデータは push し +たものと同じになるという論理式を型に書き、証明を行なった。 + +\begin{lstlisting}[caption=pushとpopを使った証明,label=push-pop] +push->pop : {l : Level } {D : Set l} (x : D ) (s : SingleLinkedStack D ) -> pushStack ( stackInSomeState s ) x ( \s1 -> popStack s1 ( \s3 x1 -> (Just x ≡ x1))) +push->pop {l} {D} x s = refl +\end{lstlisting} + +証明の関数部分に出てきた\verb+refl+は左右の項が等しいことを表す$x \equiv x$を生 +成する項であり、$x \equiv x$を証明したい場合には\verb+refl+と書く事ができる。 + +\begin{lstlisting}[caption=reflectionの定義,label=refl] +data _≡_ {a} {A : Set a} (x : A) : A → Set a where + refl : x ≡ x +\end{lstlisting} + +また、Code \ref{test08}のように継続を用いて記述することで関数の中で計算途中のデー +タ内部を確認することができた。ここでは$\lambda$式のネストになり見づらいため、 +\verb+()+をまとめる糖衣構文\verb+$+を使っている。\verb+$+を先頭に書くことで後ろ +の一行を\verb+()+でくくることができる。 + +Code \ref{test08} のように記述し、\verb+C-c C-n+(Compute nomal form)で関数を評価 +すると最後に返している stack の top を確認することができる。top の中身は +Code\ref{test08} の中にコメントとして記述した。 +\begin{lstlisting}[caption=継続によるテスト,label=test08] testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1 $ \s -> pushSingleLinkedStack s 2 $ \s -> pushSingleLinkedStack s 3 $ \s -> pushSingleLinkedStack s 4 $ \s -> pushSingleLinkedStack s 5 $ \s -> top s + +-- Just (cons 5 (Just (cons 4 (Just (cons 3 (Just (cons 2 (Just (cons 1 Nothing))))))))) \end{lstlisting} -% パターンマッチでは全てのコンストラクタのパターンを含まなくてはならない。 -% 例えば、Bool 型を受け取る関数で \verb+true+ の時の挙動のみを書くことはできない。 -% なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。 -% 例えばリスト~\ref{agda-pattern}の not は x には true しか入ることは無い。 -% なお、マッチした値以外の挙動をまとめて書く際には \verb+_+ を用いることもできる。 -% \lstinputlisting[label=agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda} - -% Agda にはラムダ式が存在している。ラムダ式とは関数内で生成できる無名の関数であり、 -% \verb+\arg1 arg2 -> function body+ のように書くことができる。 -% 例えば Bool 型の引数 \verb+b+ を取って not を適用する \verb+not-apply+ をラムダ式で書くとリスト~\ref{agda-lambda}のようになる。 -% 関数 \verb+not-apply+ をラムダ式を使わずに定義すると \verb+not-apply-2+ になるが、この二つの関数は同一の動作をする。 - -% \lstinputlisting[label=agda-lambda, caption=Agda におけるラムダ式] {src/AgdaLambda.agda} - -% Agda では特定の関数内のみで利用できる関数を \verb+where+ 句で記述できる。 -% スコープは \verb+where+ 句が存在する関数内部のみであるため、名前空間が汚染させることも無い。 -% 例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb+f+ を定義するとき、 \verb+where+ を使うとリスト~\ref{agda-where} のように書ける。 -% これは \verb+f'+ と同様の動作をする。 -% \verb+where+ 句は利用したい関数の末尾にインデント付きで \verb+where+ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。 - -% \lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda} - -% % Stackのinterface 部分を使ってrecord の説明をする -% Agda のデータには C における構造体に相当するレコード型も存在する。 -% 定義を行なう際は \verb+record+キーワードの後にレコード名、型、\verb+where+ の後に \verb+field+ キーワードを入れた後、フィールド名と型名を列挙する。 -% 例えば x と y の二つの自然数からなるレコpード \verb+Point+ を定義するとリスト~\ref{agda-record}のようになる。 -% レコードを構築する際は \verb+record+ キーワードの後の \verb+{}+ の内部に \verb+fieldName = value+ の形で値を列挙していく。 -% 複数の値を列挙する際は \verb+;+ で区切る。 - -% \lstinputlisting[label=agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda} - -% 構築されたレコードから値を取得する際には \verb+RecordName.fieldName+ という名前の関数を適用する(リスト~\ref{agda-record-proj} 内2行目) 。 -% なお、レコードにもパターンマッチが利用できる(リスト~\ref{agda-record-proj} 内5行目)。 -% レコード内の値は \verb+record oldRecord {field = value ; ... }+ という構文を利用し更新することができる。 -% Point の中の x の値を5増やす関数 \verb+xPlus5+ はリスト~\ref{agda-record-proj}の 7,8行目のように書ける。 - -% \lstinputlisting[label=agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda} \section{Agda での Stack、 Binary Tree の実装} -ここでは Agda での Stack 、 Tree の実装を示す。 +ここでは Agda での Stack 、 Binary Tree の実装を示す。 -Stack の実装を以下のソースコード\ref{stack-impl}で示す。 -実装は SingleLinkedStack という名前で定義されている。 -定義されている API は一部を書き、残りは省略する。 +Stack の実装を以下の Code \ref{stack-impl}で示す。 +実装は SingleLinkedStack という名前の\verb+record+で定義されている。 \lstinputlisting[label=stack-impl, caption=Agdaにおける Stack の実装の一部] {src/AgdaStackImpl.agda} -Element は SingleLinkedStack で扱われる要素の定義で、現在のデータ datum と次のデー -タを Maybe 型という値の存在が不確かな場合の型で包み、自身で再帰的に定義している。 -Maybe 型では値が存在する場合は Just 、 存在しない場合は　Nothing を返す。 - +% Element は SingleLinkedStack で扱われる要素の定義で、現在のデータ datum と次のデー +% タを Maybe 型という値の存在が不確かな場合の型で包み、自身で再帰的に定義している。 +% Maybe 型では値が存在する場合は Just、 存在しない場合は　Nothing を返す。 SingleLinkedStack 型では、この Element の top 部分のみを定義している。 Stack に対する push 操作では stack と push する element 型の datum を受け取り、 datum の next に現在の top を入れ、 stack の top を受け取った datum に切り替え、新しい stack を返すというような実装をしている。 -Tree の実装(以下のソースコード\ref{tree-impl})は RedBlackTree という名前で定義されている。 -定義されている API は put 以後省略する。残りのの実装は付録に示す。 %~\ +Tree の実装(以下の Code \ref{tree-impl})は Tree という\verb+record+で定義されている。 + +% \lstinputlisting[label=tree-impl, caption=Agdaにおける Tree の実装]{src/AgdaTreeImpl.agda} -\lstinputlisting[label=tree-impl, caption=Agdaにおける Tree の実装] {src/AgdaTreeImpl.agda} +\begin{lstlisting}[caption=Treeの実装,label=tree-impl] +record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where + field + putImpl : treeImpl -> a -> (treeImpl -> t) -> t + getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t -Node 型は key と value 、 Color と Node の rihgt 、 left の情報を持っている。 -Tree を構成する末端の Node は leafNode 型で定義されている。 +record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where + field + tree : treeImpl + treeMethods : TreeMethods {n} {m} {a} {t} treeImpl + putTree : a -> (Tree treeImpl -> t) -> t + putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} )) + getTree : (Tree treeImpl -> Maybe a -> t) -> t + getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d ) -RedBlackTree 型は root の Node 情報と Tree に関する計算をする際に、そこまでの -Node の経路情報を保持するための nodeStack と 比較するための compare を持っている。 +record Node {n : Level } (a k : Set n) : Set n where + inductive + field + key : k + value : a + right : Maybe (Node a k) + left : Maybe (Node a k) + color : Color {n} +\end{lstlisting} + +Tree を構成する Node の型は \verb+Node+型で定義され key、 value、 Color、rihgt、 +left などの情報を持っている。 +Tree を構成する末端の Node は \verb+leafNode+ 型で定義されている。 + +Tree 型の実装では root の Node 情報と Tree に関する計算をする際に、そこまでの +Node の経路情報を保持するための Stack を持っている。 Tree の put 操作では tree 、 put するノードのキーと値(k1、value)を引数として受け 取り、Tree の root に Node が存在しているかどうかで場合分けしている。 @@ -349,13 +401,13 @@ Agda で GearsOS のモジュール化の仕組みである interface を実装した。 interface とは、実装と仕様を分ける記述でここでは Stack の実装を -SingleLinkedStack 、 Stack の仕様を Stack とする。 -interface は record で列挙し、ソースコード~\ref{agda-interface}のように紐付けることができる。 +SingleLinkedStack 、 Stack の仕様を Stack とした。 +interface は record で列挙し、Code~\ref{agda-interface}のように紐付けることができる。 Agda では型を明記する必要があるため record 内に型を記述している。 -例として Agda で実装した Stack 上の interface (ソースコード\ref{agda-interface}) +例として Agda で実装した Stack 上の interface ( Code \ref{agda-interface}) の一部を見る。 -Stack の実装は SingleLinkedStack(ソースコード\ref{agda-single-linked-stack}) として書かれている。それを Stack 側からinterface を通して呼び出している。 +Stack の実装は SingleLinkedStack( Code \ref{agda-single-linked-stack}) として書かれている。それを Stack 側からinterface を通して呼び出している。 ここでの interface の型は Stack の record 内にある pushStack や popStack などで、 実際に使われる Stack の操作は StackMethods にある push や popである。この push @@ -380,71 +432,12 @@ % 元の push では 送り先の stack を関数に書く必要があり、異なる stack に push % する可能性があったが、 pushStack では紐付けた Stack に push することになり -\section{継続を使った Agda における Test , Debug} -Agda ではプログラムのコンパイルが通ると型の整合性が取れていることは保証できるが、必ず -しも期待した動作をするとは限らない。そのため、本研究中に書いたプログラムが正しい動 -作をしているかを確認するために行なった手法を幾つか示す。 - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -今回は実験中にソースコード\ref{agda-stack-test}のような Test を書いた。 -この Test では Stack をターゲットにしていて、 Stack に1、 2の二つの$ \mathbb{N} $型のデー -タを push した後、 pop2 Interface を使って Stack に入っている 1、 2 が Stack の -定義である First in Last out の通りに 2、 1 の順で取り出せるかを確認するために作成した。 - -%\lstinputlisting[label=agda-stack-test, caption=Agdaにおけるテスト]{src/} - -上の 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={ 通常の継続の -% コード}] - -% \end{lstlisting} - -% \begin{lstlisting}[frame=lrbt,label=sintax-sugar,caption={ 糖衣構文 -% を用いた継続のコード}] - -% \end{lstlisting} - -ソースコード~\ref{agda-tree-debug}のように関数本体に記述してデータを返し、C-c C-n -(Compute normal form) で関数を評価すると関数で扱っているデータを見ることができる。 -また、途中の計算で受ける変数名を変更し、 Return 時にその変更した変数名に変えるこ -とで、計算途中のデータの中身を確認することができる。評価結果はソースコード内にコメントで記述した。 - - \lstinputlisting[label=agda-tree-debug, caption=Agdaにおけるテスト]{src/AgdaTreeDebug.agda} - -今回、この手法を用いることで複数の関数を組み合わせた findNode 関数内に異常があるこ -とが分かった。 - - -%getRedBlackTree の関数に -% \lstinputlisting[label=agda-Debug, caption=Agdaにおけるデバッグ]{src/AgdaTreeDebug.agda} -% Tree全然載せてないけどどうしよ。。。どこに書こうかは考えておきましょう - \section{Agda による Interface 部分を含めた Stack の部分的な証明} \label{agda-interface-stack} % Stack の仕様記述 -Stack や Tree の Interface を使い、 Agda で Interface を 経由した証明が可能であ -ることを示す。 +Stack の Interface を使い、 Agda で Interface を 経由した証明を行なった。 ここでの証明とは Stack の処理が特定の性質を持つことを保証することである。 Stack の処理として様々な性質が存在する。例えば、 @@ -462,13 +455,13 @@ ここでは「どのような状態の Stack でも、値を push した後 pop した値は直前 に入れた値と一致する」という性質を証明する。 -まず始めに不定状態の Stack を定義する。ソースコード~\ref{agda-in-some-state} -の stackInSomeState 型は中身の分からない抽象的な Stack を表現している。ソースコー -ド~\ref{agda-in-some-state}の証明ではこのstackInSomeState に対して、 push を -2回行い、 pop2 をして取れたデータは push したデータと同じものになることを証明す -る。 - - \lstinputlisting[label=agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda} +まず始めに不定状態の Stack を定義する。 Code~\ref{agda-in-some-state} +の stackInSomeState 型は引数として \verb+SingleLinkedStack+ 型の \verb+s+を受け +取り新しいレコードを返す関数である。 +この関数により、中身の分からない抽象的な Stack を表現している。ソースコー +ド~\ref{agda-in-some-state}の証明ではこの \verb+stackInSomeState+ に対して、 +\verb+push+ 操作を2回行い、 \verb+pop+を2回行なって取れたデータは push したデー +タと同じものになることを証明している。 この証明では stackInSomeState 型の s が抽象的な Stack で、そこに x 、 y の２つのデー タを push している。また、 pop2 で取れたデータは y1 、 x1 となっていて両方が @@ -480,42 +473,11 @@ これにより、抽象化した Stack に対して push 、 pop を行うと push したものと同じも のを受け取れることが証明できた。 - -% \lstinputlisting[label=agda-Test, caption=]{src/AgdaStackTest.agda} - -% \section{Agda による Interface 部分を含めた Binary Tree の部分的な証明と課題} -% ここでは Binary Tree の性質の一部に対して証明を行う。 -% Binary Tree の性質として挙げられるのは次のようなものである -% % 上の２つはデータ構造として最低限守られるべき部分ではあるがとりあえず書いてる - -% \begin{itemize} -% \item Tree に対して Node を Put することができる。 -% \item Tree に Put された Node は Delete されるまでなくならない。 -% \item Tree に 存在する Node とその子の関係は必ず「右の子 $>$ Node」かつ「Node $>$ 左の子」の関係になっている。 -% \item どのような状態の Tree に値を put しても Node と子の関係は保たれる -% \item どのような状態の Tree でも値を Put した後、その値を Get すると値が取れる。 -% \end{itemize} - -% ここで証明する性質は + \lstinputlisting[label=agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda} -% ${!!}$ と書かれているところはまだ記述できていない部分で $?$ としている部分である。 - -% \lstinputlisting[label=agda-tree-proof, caption=Tree Interface の証 -% 明]{src/AgdaTreeProof.agda} - -% この Tree の証明では、不定状態の Tree を redBlackInSomeState で作成し、その状態の Tree -% に一つ Node を Put し、その Node を Get することができるかを証明しようとしたもの -% である。 - -% しかし、この証明は Node を取得する際に Put した Node が存在するか、 Get した -% Node が存在するのか、などの条件や、 Get した Node と Put した Node が合同なのか、 -% key の値が等しい場合の eq は合同と同義であるのか等の様々な補題を証明する必要が -% あった。今回この証明では Put した Node と Get した -% Node が合同であることを記述しようとしていたがそれまでの計算が異なるため完全に合 -% 同であることを示すことが困難であった。 - -% 今後の研究では\ref{hoare-logic} で説明する Hoare Logic を元に証明を -% 行おうと考えている。 +しかし、同様の証明を Tree 側で記述した際、 Agda 側で等しいことを認識できず記述が +複雑になっていったため、今後の証明は Hoare Logic をベースにしたものを取り入れて +行きたいと考えている。 \section{Hoare Logic} \label{hoare-logic} @@ -549,8 +511,8 @@ \end{figure} この状態を当研究室で提案している CodeGear、 DataGear の単位で考えると -Pre Condition は CodeGear に入力として与えられる Input DataGear として、 - Command は処理の単位である CodeGear、 Post Condition を Output DataGear として当てはめることができると考える。 +PreCondition は CodeGear に入力として与えられる Input DataGear として、 + Command は処理の単位である CodeGear、 PostCondition を Output DataGear として当てはめることができると考える。 ここでは binary tree での findNode、 replaceNode、 getRedBlackTree の流れを図 \ref{fig:tree-hoare} で示す。 diff -r 341b4c04597f -r 4312a27022d1 Paper/src/AgdaInterface.agda --- a/Paper/src/AgdaInterface.agda Sun Apr 22 20:53:49 2018 +0900 +++ b/Paper/src/AgdaInterface.agda Mon Apr 23 18:11:46 2018 +0900 @@ -1,12 +1,7 @@ -data Maybe {n : Level } (a : Set n) : Set n where - Nothing : Maybe a - Just : a -> Maybe a - record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where field push : stackImpl -> a -> (stackImpl -> t) -> t pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t - get : stackImpl -> (stackImpl -> Maybe a -> t) -> t open StackMethods record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where @@ -17,6 +12,4 @@ pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } )) popStack : (Stack a si -> Maybe a -> t) -> t popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - getStack : (Stack a si -> Maybe a -> t) -> t - getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) open Stack diff -r 341b4c04597f -r 4312a27022d1 Paper/src/AgdaTreeImpl.agda --- a/Paper/src/AgdaTreeImpl.agda Sun Apr 22 20:53:49 2018 +0900 +++ b/Paper/src/AgdaTreeImpl.agda Mon Apr 23 18:11:46 2018 +0900 @@ -1,32 +1,14 @@ -record Node {n : Level } (a k : Set n) : Set n where - inductive +record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where field - key : k - value : a - right : Maybe (Node a k) - left : Maybe (Node a k) - color : Color {n} -open Node + putImpl : treeImpl -> a -> (treeImpl -> t) -> t + getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t -leafNode : {n : Level } {a k : Set n} -> k -> a -> Node a k -leafNode k1 value = record { - key = k1 ; - value = value ; - right = Nothing ; - left = Nothing ; - color = Red - } -open leafNode +record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where + field + tree : treeImpl + treeMethods : TreeMethods {n} {m} {a} {t} treeImpl + putTree : a -> (Tree treeImpl -> t) -> t + putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} )) + getTree : (Tree treeImpl -> Maybe a -> t) -> t + getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d ) -record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.⊔ n) where - field - root : Maybe (Node a k) - nodeStack : SingleLinkedStack (Node a k) - compare : k -> k -> CompareResult {n} -open RedBlackTree - -putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t -putRedBlackTree {n} {m} {a} {k} {t} tree k1 value next with (root tree) -... | Nothing = next (record tree {root = Just (leafNode k1 value) }) -... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)) - diff -r 341b4c04597f -r 4312a27022d1 Paper/src/AgdaTreeImpl.agda.replaced --- a/Paper/src/AgdaTreeImpl.agda.replaced Sun Apr 22 20:53:49 2018 +0900 +++ b/Paper/src/AgdaTreeImpl.agda.replaced Mon Apr 23 18:11:46 2018 +0900 @@ -1,47 +1,13 @@ -record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where +record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.$\sqcup$ n) where field - putImpl : treeImpl @$\rightarrow$@ a @$\rightarrow$@ (treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t - getImpl : treeImpl @$\rightarrow$@ (treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t -open TreeMethods + putImpl : treeImpl $\rightarrow$ a $\rightarrow$ (treeImpl $\rightarrow$ t) $\rightarrow$ t + getImpl : treeImpl $\rightarrow$ (treeImpl $\rightarrow$ Maybe a $\rightarrow$ t) $\rightarrow$ t -record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where +record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.$\sqcup$ n) where field tree : treeImpl treeMethods : TreeMethods {n} {m} {a} {t} treeImpl - putTree : a @$\rightarrow$@ (Tree treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t - putTree d next = putImpl (treeMethods ) tree d (\t1 @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} )) - getTree : (Tree treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - getTree next = getImpl (treeMethods ) tree (\t1 d @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ) d ) -open Tree - -record Node {n : Level } (a k : Set n) : Set n where - inductive - field - key : k - value : a - right : Maybe (Node a k) - left : Maybe (Node a k) - color : Color {n} -open Node - -leafNode : {n : Level } {a k : Set n} @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ Node a k -leafNode k1 value = record { - key = k1 ; - value = value ; - right = Nothing ; - left = Nothing ; - color = Red - } -record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.@$\sqcup$@ n) where - field - root : Maybe (Node a k) - nodeStack : SingleLinkedStack (Node a k) - compare : k @$\rightarrow$@ k @$\rightarrow$@ CompareResult {n} -open RedBlackTree - -putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t -putRedBlackTree {n} {m} {a} {k} {t} tree k1 value next with (root tree) -... | Nothing = next (record tree {root = Just (leafNode k1 value) }) -... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s @$\rightarrow$@ findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 @$\rightarrow$@ insertNode tree1 s n1 next)) - --- 以下省略 + putTree : a $\rightarrow$ (Tree treeImpl $\rightarrow$ t) $\rightarrow$ t + putTree d next = putImpl (treeMethods ) tree d (\t1 $\rightarrow$ next (record {tree = t1 ; treeMethods = treeMethods} )) + getTree : (Tree treeImpl $\rightarrow$ Maybe a $\rightarrow$ t) $\rightarrow$ t + getTree next = getImpl (treeMethods ) tree (\t1 d $\rightarrow$ next (record {tree = t1 ; treeMethods = treeMethods} ) d )