# HG changeset patch # User ryokka # Date 1509091575 -32400 # Node ID c0a6124f436b31f341f622c8b2eb253ad1dc204e # Parent 3be2444dacc59640df14bc39038110a553d3fb8a delete natural deduction. add CbC,Agda more description diff -r 3be2444dacc5 -r c0a6124f436b midterm/midterm.pdf Binary file midterm/midterm.pdf has changed diff -r 3be2444dacc5 -r c0a6124f436b midterm/midterm.tex --- a/midterm/midterm.tex Thu Oct 26 15:04:10 2017 +0900 +++ b/midterm/midterm.tex Fri Oct 27 17:06:15 2017 +0900 @@ -47,7 +47,7 @@ \section{研究目的} -%% Agdaのお勉強のこと、Agdaに直したRedBlackTreeのこと、CbC側のDeletionのこと +%% Agdaのお勉強のこと、CbCをAgdaに直したこと、CbC側のDeletionのこと %% CbC でソフトウェアを検証できるかを CbCで書いた RBTree と Agda で同様に書いた RBTree を検証することで示す @@ -62,16 +62,15 @@ % CbC検証と実装が同一の言語で行える言語である。 % CbCの特徴はだいじょうぶ？完全じゃなくていいけどある程度は乗せなきゃ駄目だよね -ソフトウェアの信頼性を保証することは重要だ。 -現在ソフトウェアの信頼性を保証する方法として代表的なものはモデル検査と、定理証明が存在している。 - +ソフトウェアの信頼性を保証することは重要である。現在ソフトウェアの信頼性を保証する方法として代表的なものはモデル検査と、定理証明が存在している。 モデル検査はソフトウェアの状態をすべて数え上げ、すべての状態で仕様が正しいことを確認する方法である。 定理証明はソフトウェアが満たすべき仕様を論理式で記述し、その論理式が恒真であることを証明することである。%% atton-master papar より -モデル検査や、証明でソフトウェアを検証する際、検証に使われる言語と実装に使う言語が異なるという問題がある。 -そのため、二重で同じソフトウェアを記述する必要があるうえ、検証に用いるソースコードは状態が遷移する形で記述する必要があるなど実装されているコードに比べて記述が困難である。 -検証されたコードから実行可能なコードを生成可能な検証系もあるが、生成されたコードが検証のコードと別の言語であったり、既存の実際に対する検証は行えないなどの問題がある。 +%% モデル検査や、証明でソフトウェアを検証する際、検証に使われる言語と実装に使う言語が異なるという問題がある。 +%% そのため、二重で同じソフトウェアを記述する必要があるうえ、検証に用いるソースコードは状態が遷移する形で記述する必要があるなど実装されているコードに比べて記述が困難である。 +%% 検証されたコードから実行可能なコードを生成可能な検証系もあるが、生成されたコードが検証のコードと別の言語であったり、既存の実際に対する検証は行えないなどの問題がある。 -この問題を解決する為に当研究室では検証と実装を同一の言語で行える Continuation based C ( CbC )言語を開発している。 +% この問題を解決する為に +当研究室では検証と実装を同一の言語で行える Continuation based C ( CbC )言語を開発している。 本研究では、検証や証明に直接使用できる言語として CbC を用いる。 %% CbC 上に構築されたプログラムが持つ状態を数え挙げ、仕様を満たすか調べるモデル検査的手法は、比嘉(2016)\cite{Yasutaka:2016}により提案、実装されている。 @@ -83,7 +82,7 @@ %% 部分型を用いて CbC の項を型付けすることで、CbC の形式的定義を型システムより相似的に得る。 -本研究では CbC を用いて RedBlackTree を実装し、 Insert、Delete などの操作の際に RedBlackTree が常にその仕様を満たせているかを検査、証明することで、 CbC 上で動くプログラムが正しく検証できることを示す。 +本研究では CbC を用いて RedBlackTree を実装し、 Insert、Delete などの操作の際に RedBlackTree が常にその仕様を満たせているかを検証、証明する。 %%検証と証明の話書かないとAgda出せなくない？ @@ -93,7 +92,9 @@ CbC は C 言語とほぼおなじ構文を持ち、よりアセンブラに近い形でプログラムを記述する。 CbC では C の関数の代わりに CodeSegment を用いて処理を記述する。 -CodeSegment は値を入力として受取り、出力を行う処理で、それらの状態を goto で遷移して記述する。この goto による処理の遷移を継続と呼ぶ。 +CodeSegment は値を入力として受取り、出力を行う処理の単位で、それらの状態を goto で遷移して記述する。この goto による処理の遷移を継続と呼ぶ。 +CbC の CodeSegment を定義するには C とは少し異なり関数定義のの先頭に \_\_code が付く。 +DataSegment は CodeSegment が扱うデータの単位であり、処理に必要なデータが全て入っている。CodeSegment の入力となる DataSegment は Input DataSegment　出力 を Input DataSegment は関数の引数として定義する。次の CodeSegment に処理を移す際は、 goto の後に CodeSegment 名と Input DataDataSegment を指定する。 % 図\ref{fig:CSContinuation}は CodeSegment 感の処理の流れを表している。 %%% figure @@ -105,98 +106,129 @@ %% \label{fig:CSContinuation} %% \end{figure} - %% CbC ではこの継続処理にをメタ計算として定義されていて、実装や環境によって切り替えることできる。検証を行うメタ計算を定義することで、 CodeSegment の仕様を変更せずソフトウェアの検証を行う事ができる。 -例として CbC による Stack のコード示す。 +CbC ではこの継続処理にをメタ計算として定義されていて、実装や環境によって切り替えることできる。検証を行うメタ計算を定義することで、 CodeSegment の仕様を変更せずソフトウェアの検証を行う事ができる。 +例として CbC による Stack に対する操作のコード示す。 +\newpage \lstinputlisting[label=src:singlelinked, caption=CbCによるStack]{./src/SingleLinkedStack.cbc.replace} +このコードでは Stack に対する push と pop を定義している。 -%CbC で Fanctional に書かれた CodeSegment は等価な Agda のコードに置き換えることが可能だと考えている。 +push や pop は必要があるときに外から呼ばれる。 + +push では element で新しい要素を作って、次の要素との関係、 push する要素を入れ、Stack の top を書き換えて次のCodeSegmentに飛ぶ。 -現状の CbC では CbC 自身を証明する事ができない。 +pop では Stack の top に data があればその data を next に入れ、次のCodeSegmentに飛ぶ。 top に data が無ければ NULL を next の Input Data に入れて次のCodeSegmentに飛ぶ。 + +%% また CbC で Functional に書かれた CodeSegment は等価な Agda のコードに置き換えることが可能だと考えている。 + 比嘉(2016)\cite{Yasutaka:2016}では CbC における CodeSegment 、 DataSegment が部分型で定義できることが示されている。 -これより、 CbC で Fanctional に書かれたプログラムは等価な Agda のコードの置き換えることができる。 -本研究では代わりに等価なAgdaのコードに変換することで証明を行う。 +これより、 CbC で Functional に書かれたプログラムは等価な Agda のコードの置き換えることができる。 +本研究では CbC の代わりに等価なAgdaのコードに変換することで証明を行う。 \section{Agda} Agda\cite{agda} とは定理証明支援器であり依存型を関数プログラミング言語である。 依存型とは型も第一級オブジェクトとする型システムであり、型の型や型を引数に取る関数、値を取って型を返す関数などが記述することができる。 -例として 前項で示した CbC で書かれた Stack をAgda に変換したコードを示す。 + +CbC を Agda に変換する場合 DataSegment をレコード型、 CodeSegment は関数型となる。 + +前項で示した CbC で書かれた Stack の操作をAgda に変換したコードを示す。 \lstinputlisting[label=src:stack-agda, caption=AgdaによるStack]{./src/stack.agda.replace} + %CbC で書かれた Stack の CodeSegment が要素、Tree、 -Agda のコードに変換した後証明を行う。 +Agda のコードで関数を定義するときは関数名、型を記述した後に関数本体を指定する。関数の型では → または \verb/->/ を使い定義する。 +%% 引数は変数で受けることもできるが、具体的な型構築子を渡された時の挙動を定義することができる。これはパターンマッチと呼ばれ、型構築子で case 文を行っているようなものである。 +%% パターンマッチはすべての場合を含む必要があり、特定のものだけ異なる挙動にしたい場合は構築子を幾つか指定した後に変数で受けることで解決できる。なお、マッチした値を変数として利用しない場合は _ で値を捨てることもできる。 -%% 証明を行う前に自然演繹について説明 -自然演繹とは Gentzen によって作られた論理とその証明システムである。命題変数と記号を用いた論理式で論理を記述し、推論規則を使って変形することで求める論理式を導く。 +関数にはリテラルが存在し、関数を定義せずにその場で値を生成することもできる。これは ラムダ式と呼ばれ、 \verb/\arg1 arg2 -> function body/ または $ \lambda $ arg1 arg2 → function body のように記述できる。上の例では pushStack の \verb/\s1 -> next (record {stack = s1})/ や、 popStack の \verb/\s1 -> next s0/ が ラムダ式である。 + + +%%%%%%%% + Agda のレコード型も存在する。定義をする際は record キーワードのあとにレコード名、型、 where の後に field キーワードを入れ、フィールド名 : 型名 と列挙する。レコードを構築する際は record キーワードの後に {} 内部に fileName = value の形で列挙していく。複数の値を列挙する際は ; で区切る。上の例では \verb/record {stack = s1}/ がそれにあたる。 -始めに、自然演繹と型付き$ \lambda $ 計算の対応を定義する。 -\begin{center} -\begin{table}[htbp] -\scalebox{0.75}{ -\begin{tabular}{|c|c|} \hline - Natural Deduction & 型付き $ \lambda $ 計算 \\ \hline \hline - $ A $ & 型 A を持つ変数 x \\ \hline - $ A \Rightarrow B $ & 型 A を取り型 B の変数を返す関数 f \\ \hline - $ \Rightarrow \mathcal{I} $ & ラムダの抽象化 \\ \hline - $ \Rightarrow \mathcal{E} $ & 関数適用 \\ \hline - $ A \land B $ & 型 A と型 B の直積型 を持つ変数 x \\ \hline - $ \land \mathcal{I} $ & 型A,Bを持つ値から直積型へのコンストラクタ \\ \hline - $ \land 1 \mathcal{E} $ & 直積型からの型Aを取り出す射影fst \\ \hline - $ \land 2 \mathcal{E} $ & 直積型からの型Bを取り出す射影snd \\ \hline -\end{tabular} -} -\caption{natural deuction と 型付き $ \lambda $ 計算との対応(Curry-Howard Isomorphism)} -\label{table:curry} -\end{table} -\end{center} + + +%% リテラル is 何 + -ここでは例として ((A ならば B) かつ (B ならば C)) ならば (A ならば C) が成り立つという三段論法を証明をする。 - -この三段論法を自然演繹による証明木にすると次のようになる。 +%% このコードでは push 、 pop の関数を定義をしている。 +%% push では要素を追加した新しいStackを返す。 +%% pop では data があればそのデータを pop し、しない場合はそもそも -\begin{figure}[htpb] - \begin{center} - \includegraphics[width=95mm]{../pic/modus-ponens.pdf} - \end{center} - \caption{自然演繹での三段論法の証明} - \label{fig:modus-ponens} -\end{figure} +このように CbC のコードを Agda に変換し、証明を行う。 -この証明木に対応するAgdaによる証明は次のようになる。 - -\begin{lstlisting}[basicstyle=\ttfamily\footnotesize, frame=single] -data _×_ (A B : Set) : Set where - <_,_> : A → B → A × B +% 証明を行う前に自然演繹について説明 +%% 自然演繹とは Gentzen によって作られた論理とその証明システムである。命題変数と記号を用いた論理式で論理を記述し、推論規則を使って変形することで求める論理式を導く。 -fst : {A B : Set} → A × B → A -fst < a , _ > = a +%% 始めに、自然演繹と型付き$ \lambda $ 計算の対応を定義する。 +%% \begin{center} +%% \begin{table}[htbp] +%% \scalebox{0.75}{ +%% \begin{tabular}{|c|c|} \hline +%% Natural Deduction & 型付き $ \lambda $ 計算 \\ \hline \hline +%% $ A $ & 型 A を持つ変数 x \\ \hline +%% $ A \Rightarrow B $ & 型 A を取り型 B の変数を返す関数 f \\ \hline +%% $ \Rightarrow \mathcal{I} $ & ラムダの抽象化 \\ \hline +%% $ \Rightarrow \mathcal{E} $ & 関数適用 \\ \hline +%% $ A \land B $ & 型 A と型 B の直積型 を持つ変数 x \\ \hline +%% $ \land \mathcal{I} $ & 型A,Bを持つ値から直積型へのコンストラクタ \\ \hline +%% $ \land 1 \mathcal{E} $ & 直積型からの型Aを取り出す射影fst \\ \hline +%% $ \land 2 \mathcal{E} $ & 直積型からの型Bを取り出す射影snd \\ \hline +%% \end{tabular} +%% } +%% \caption{natural deuction と 型付き $ \lambda $ 計算との対応(Curry-Howard Isomorphism)} +%% \label{table:curry} +%% \end{table} +%% \end{center} -snd : {A B : Set} → A × B → B -snd < _ , b > = b +%% ここでは例として ((A ならば B) かつ (B ならば C)) ならば (A ならば C) が成り立つという三段論法を証明をする。 + +%% この三段論法を自然演繹による証明木にすると次のようになる。 + +%% \begin{figure}[htpb] +%% \begin{center} +%% \includegraphics[width=95mm]{../pic/modus-ponens.pdf} +%% \end{center} +%% \caption{自然演繹での三段論法の証明} +%% \label{fig:modus-ponens} +%% \end{figure} -f : {A B C : Set} → ((A → B) × (B → C)) → (A → C) -f = λ p x → (snd p) ((fst p) x) -\end{lstlisting} +%% この証明木に対応するAgdaによる証明は次のようになる。 + +%% \begin{lstlisting}[basicstyle=\ttfamily\footnotesize, frame=single] +%% data _×_ (A B : Set) : Set where +%% <_,_> : A → B → A × B -三段論法の証明は、1つの仮定から $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ を用いて仮定を二つ取り出し、それぞれに $ \Rightarrow \mathcal{E} $ を適用した後に仮定を $ \Rightarrow \mathcal{I}$ して導出していた。 +%% fst : {A B : Set} → A × B → A +%% fst < a , _ > = a + +%% snd : {A B : Set} → A × B → B +%% snd < _ , b > = b + -$ \Rightarrow \mathcal{I}$ に対応するのは関数適用である。 -よってこの証明は「一つの変数から fst と snd を使って関数を二つ取り出し、それぞれを関数適用する」という形になる。 -%% これをラムダ式で書くとリスト~\ref{src:agda-modus-ponens}のようになる。 -仮定 $ (A \rightarrow B) \times (B \rightarrow C) $ と仮定 A から A $ \rightarrow $ C を導いている。 +%% f : {A B C : Set} → ((A → B) × (B → C)) → (A → C) +%% f = λ p x → (snd p) ((fst p) x) +%% \end{lstlisting} + +%% 三段論法の証明は、1つの仮定から $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ を用いて仮定を二つ取り出し、それぞれに $ \Rightarrow \mathcal{E} $ を適用した後に仮定を $ \Rightarrow \mathcal{I}$ して導出していた。 -仮定に相当する変数 p の型は$ (A \rightarrow B) \times (B \rightarrow C) $ であり、p からそれぞれの命題を取り出す操作が fst と snd に相当する。 -fst p の型は $ (A \rightarrow B) $ であり、snd p の型は $ (B \rightarrow C) $ である。 -もう一つの仮定xの型は A なので、fst p を関数適用することで B が導ける。 -得られた B を snd p に適用することで最終的に C が導ける。 +%% $ \Rightarrow \mathcal{I}$ に対応するのは関数適用である。 +%% よってこの証明は「一つの変数から fst と snd を使って関数を二つ取り出し、それぞれを関数適用する」という形になる。 +%% %% これをラムダ式で書くとリスト~\ref{src:agda-modus-ponens}のようになる。 +%% 仮定 $ (A \rightarrow B) \times (B \rightarrow C) $ と仮定 A から A $ \rightarrow $ C を導いている。 + +%% 仮定に相当する変数 p の型は$ (A \rightarrow B) \times (B \rightarrow C) $ であり、p からそれぞれの命題を取り出す操作が fst と snd に相当する。 +%% fst p の型は $ (A \rightarrow B) $ であり、snd p の型は $ (B \rightarrow C) $ である。 +%% もう一つの仮定xの型は A なので、fst p を関数適用することで B が導ける。 +%% 得られた B を snd p に適用することで最終的に C が導ける。 %% \lstinputlisting[label=src:agda-modus-ponens, caption=Agda における三段論法の証明] {src/AgdaModusPonens.agda.replaced} -このように Agda では証明を記述することができる。 +%% このように Agda では証明を記述することができる。 % Agdaの知識ってどう出す？ @@ -250,7 +282,7 @@ %% pushStack {a} {t} s0 d next = (push s0) (stack s0) d (\s1 -> next (record {stack = s1} )) %% \end{lstlisting} - +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{RedBlackTree} @@ -281,6 +313,8 @@ \end{figure} 本研究で検証する RedBlackTree は非破壊であり、一度構築した木構造は破壊される操作ごとに新しい木が生成される。非破壊である理由は並列実行時のデータ保存である。 + + %% atton-master@13p %% figure @@ -298,7 +332,7 @@ 現段階では CbC で書かれた RedBlackTree の一部を Agda のコードに変換した。 今後は CbC での RedBlackTree の Deletion 、Agda での証明を実装していく。また、依存型を導入することで CbC で自身を証明できるようにするなどの課題があるため、今後はこれらの課題に着手していく。 -%\nocite{*} +\nocite{*} \bibliographystyle{junsrt} \bibliography{reference} \end{document} diff -r 3be2444dacc5 -r c0a6124f436b midterm/src/stack.agda.replace --- a/midterm/src/stack.agda.replace Thu Oct 26 15:04:10 2017 +0900 +++ b/midterm/src/stack.agda.replace Fri Oct 27 17:06:15 2017 +0900 @@ -1,5 +1,12 @@ +record Stack {a t : Set} (stackImpl : Set) : Set where +field +stack : stackImpl +push : stackImpl -> a -> (stackImpl -> t) -> t +pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t +open Stack + pushStack : {a t : Set} -> Stack a -> a -> (Stack t -> t) -> t pushStack {a} {t} s0 d next = (push s0) (stack s0) d (\s1 -> next (record {stack = s1} )) popStack : {a t : Set} -> Stack a -> (Stack t -> t) -> t -popStack {a} {t} s0 next = (pop s0) (stack s0) (\s1 -> next s0) \ No newline at end of file +popStack {a} {t} s0 next = (pop s0) (stack s0) (\s1 -> next s0)