--- a/Paper/sigos.tex	Thu Apr 19 20:28:12 2018 +0900
+++ b/Paper/sigos.tex	Sun Apr 22 18:42:34 2018 +0900
@@ -94,7 +94,7 @@
 
 % 信頼性の高いOS
 
-\section{ソフトウェアの信頼性の保証}
+\section{定理証明系Agda を用いた GearsOS の検証}
 
 動作するソフトウェアは高い信頼性を持つことが望ましい。
 そのためにはソフトウェアが期待される動作をすることを保証する必要がある。
@@ -105,10 +105,9 @@
 記述する手法を提案しており、 CodeGear 、 DataGear という単位を用いてプログラミン
 グする言語として Countinuation based C\cite{kaito:2015} (以下CbC)を開発している。
 CbC はC言語と似た構文を持つ言語である。
-また、 CodeGear、DataGear を用いて信頼性と拡張性をメタレベルで保証する GearsOS
- CbC で開発している。
+また、 CodeGear、DataGear を用いて信頼性と拡張性をメタレベルで保証する GearsOS を CbC で開発している。
 
- 本研究では検証を行うために証明支援系言語 Agda を使用している。
+本研究では検証を行うために証明支援系言語 Agda を使用している。
 Agda では型で証明したい論理式を書き、その型に合った実装を記述することで証明を記
 述することができる。
  
@@ -124,16 +123,13 @@
  は並列実行の単位、データ分割、 Gear 間の接続等になる。
 CodeGear はプログラムの処理そのもので、図\ref{cgdg}で示しているように任意の数の
 Input DataGear を参照し、処理が完了すると任意の数の Output DataGear に書き込む。
-また、CodeGear は接続された DataGear 意外には参照を行わない。
 
 CodeGear 間の移動は継続を用いて行われる。継続は関数呼び出しとは異なり、呼び出し
-た後に元のコードに戻らず、 CodeGear ないで次の CodeGear へ継続を行う。その為、
- CodeGear 、 DataGear を使ったプログラミングは末尾再帰を強制したスタイルになる。
+た後に元のコードに戻らず、次の CodeGear へ継続を行う。これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当する。
 
- Gear の特徴として処理やデータ構造が CodeGear、 DataGear に閉じている。このため、
- 実行時間、メモリ使用量等を予測可能にできると考えている。
- また、 GearsOS 自体もこの CodeGear、 DataGear を用いた CbC(Continuation based C
-) によって実装されている。
+Gear では処理やデータ構造が CodeGear、 DataGear に閉じている。したがって、
+DataGear は Agda のデータ構造(data と record)で表現できる。
+CodeGear は Agda の CPS (Continuation Passing Style) で関数として表現することができる。
  
 \begin{figure}[htpb]
  \begin{center}
@@ -143,92 +139,62 @@
  \label{fig:cgdg}
 \end{figure}
 
-% \section{メタ計算}
-% % メタ計算の論文引用どうするかな…
-% % メタプログラミング~系の本とかもいれていいのかな
-
-% メタ計算(リフレクション)とは、対象とするレベルとメタなレベルを分離し、対象レベルでの推論や計算に
-% 関するメタな情報をメタレベルで明示的に記述し操作する。
+CodeGear は Agda では継続を用いた末尾呼び出しを行う関数として表現される。
+継続は不定の型 (\verb+t+) を返す関数で表される。
+CodeGear 自体も同じ型 \verb+t+ を返す関数となる。
+例えば、 Stack への push を行う関数 pushStack は以下のような型を持つ。
 
-% メタ計算(自己反映計算)\cite{weko_5056_1} とはプログラムを記述する際に通常の処理
-% と分離し、他に記述しなければならない処理である。例えばプログラム実行時のメモリ管
-% 理やスレッド管理、資源管理等の計算がこれに当たる。
+\begin{verbatime}
+   pushStack : a -> (Stack a si -> t) -> t
+\end{verbatime}
 
-% GearsOS では継続の前にメタ計算を埋め込むことで CodeGear の中身を変更することなく
-% 検証を行うことができる。
+\verb+pushStack+ が関数名で、コロンの後ろに型を記述する。
+最初の引数は Stack に格納される型\verb+a+ を持つ。
+二つ目の引数は継続であり、\verb+Stack a si+ (\verb+si+という実装を持つ\verb+a+を格納するStack)を受け取り不定の型\verb+t+を返す関数である。
+この CodeGear 自体は不定の型\verb+t+を返す。
 
-\section{Meta Gear}
-Gears OS の Code Gear は関数に比べて細かく分割されているため、メタ計算をより
-柔軟に記述できる。Code Gear と Data Gear にはそれぞれメタ計算の区分として
-Meta Code Gear、Meta Data Gear が存在し、これらを用いてメタ計算を実装する。
-Meta Gear は 制限された Monad に相当し、型付きアセンブラよりは大きな表現単位を
-提供する。 Haskell などの関数型プログラミング言語では実行環境が複雑て
-゙あり、実行時の資源使用 を明確にすることができないが、Gears OS を記述して
-いる CbC はスタック上に隠され た環境を持たないので、メタ計算で使用する資源を
-明確にできる利点がある。Meta Code Gear は図\ref{fig:meta-cgdg} に示すように通常の Code Gear
-の直後に遷移され、メタ計算を実行する。 また、Meta Code Gear は、その階層からさら
-にメタ計算を記述することが可能である。
+GearsOS で CodeGear の性質を証明するには、 Agda で記述された CodeGear と DataGear に対してメタ計算として証明を行う。証明すべき性質は、不定の型を持つ継続 \verb+t+ に記述することができる。例えば、 Stack にある値\verb+x+をpushして、popすると \verb+ x'+ が取れてくる。Just x とJust x' は等しい必要がある。これはAgdaでは(Just x ≡ x' ) と記述される。
+ここでJustとはAgdaの以下のデータ構造である。
 
-\begin{figure}[htpb]
- \begin{center}
-  \scalebox{0.3}{\includegraphics{pic/meta_cg_dg.pdf}}
- \end{center}
- \caption{Meta CodeGear}
- \label{fig:meta-cgdg}
-\end{figure}
+\begin{verbtim}
+data Maybe {n : Level } (a : Set n) : Set n where
+  Nothing : Maybe a
+  Just    : a -> Maybe a
+\end{verbtim}
+
+これはDataGearに相当し、Nothing と Just の二つの状態を保つ。
+popした時に、Stackが空であればNothing を返し、そうでなければJust のついた返り値を返す。
+
+この性質をAgda で表すと、以下のような型になる。
+Agda では証明すべき論理式は型で表される。
+継続部分に直接証明すべき性質を型として記述できる。
+Agda ではこの型に対応する$\lambda$項を与えると証明が完了したことになる。
 
 
-% \section{Context}
-% CbC で DataGear を扱う際、 Context と呼ばれる接続可能な CodeGear、 DataGear のリ
-% スト、Temporal DataGear のためのメモリ空間等を持っている Meta DataGearである。
-% CbC で必要な CodeGear 、 DataGear を参照する際は Context を通してアクセスする必
-% 要がある。
-
-% \section{stub CodeGear}
-% CodeGear が必要とする DataGear を取り出す際、 Context を通す必要がある。
-% しかし、 Context を直接扱えるようにするのは信頼性を損なう。そのため CbC では
-% Context を通して必要なデータを取り出して次の Code Gear に接続する stub CodeGear
-% を定義している。CodeGear は stub CodeGear を介してのみ必要な DataGear へアクセス
-% することができる。 stub CodeGear は CodeGear 毎に生成され、次の CodeGear へと接
-% 続される。
-% stub CodeGear は CodeGear の Meta CodeGear に当たる。
-
-% \section{CbCによる Interface の記述と継続}
-
-% CodeGear は通常の関数と比べ、細かく分割されるためメタ計算をより柔軟に記述でき
-% る。 CodeGear 、 DataGear にはそれぞれメタレベルとして、 Meta CodeGear
-% 、 Meta DataGear が存在する。
+\begin{verbtim}
+   push->pop : {l : Level } {D : Set l} (x : D ) (s : SingleLinkedStack D ) ->
+       pushStack ( stackInSomeState s )  x (\s -> popStack s ( \s3 x1 -> (Just x ≡ x1 )  ))
+\end{verbtim}
 
-% CbC で実装していくうちに、stub CodeGear の記述が煩雑になることが分かった。
-% そのため 既存の実装を モジュールとして扱うため Interface を導入した。
-
-% Interface は DataGear に対して何らかの操作(API)を行う CodeGear とその
-% CodeGear で使われる DataGear の集合を抽象化した メタレベルの DataGear
-% として定義される。
+このように、CodeGear を Agda で記述し、継続部分に証明すべき性質をAgda で記述する。
 
-% 例として CbC による Stack Interface \ref{interface-define},
-% \ref{interface}がある。Stack への push 操作に注目すると、
-% 実態は SingleLinkedStack の push であることが\ref{interface}で分
-% かる。実際の SingleLinkedStack の push では Stack を指定する必要があるが、
-% Interface で実装した Stack では push 先の Stack が stackImpl として扱
-% われている。この stackImpl は$ Stack->push $で呼ばれた時の Stack と同じになる。
-% これにより、 ユーザーは実行時に Stack を指定する必要がなくなる。
+GearsOS での記述は interface によってモジュール化される。
+このモジュール化もAgda により記述する必要がある。
+CbC で記述された任意の CodeGear と Meta CodeGear が Agda にそのまま変換されるわけではないが、変換可能なように記述されると仮定する。
 
-% このように Interface 記述をすることで CbC で通常記述する必要がある一定の部分を省略し呼び出
-% しが容易になる。
-
-% \lstinputlisting[label=interface-define, caption=CbCでのStack-Interfaceの定義] {src/interface.cbc}
-
-% \lstinputlisting[label=interface, caption=CbCでのStack-Interfaceの実装] {src/singleLinkedStackInterface.cbc}
+以下の節では、Agda の基本について復習を行う。
 
 \section{定理証明支援器 Agda での証明}
 
+
 型システムを用いて証明を行うことができる言語として Agda \cite{agda}が存在する。
 Agda は依存型という型システムを持つ。依存型とは型も第一級オブジェクトとする型シ
 ステムで、依存型を持っている言語では型を基本的な操作に制限なしに使用できる
 。
 型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応する。
 
+
+
 \section{Agda の文法}
 
 Agda はインデントに意味を持つため、きちんと揃える必要がある。
@@ -240,12 +206,8 @@
 
 データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。
 \verb/data/キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くした後、値にコンストラクタとその型を列挙する。
-例えば Bool 型を定義するとリスト~\ref{agda-bool}のようになる。
-Bool はコンストラクタ \verb/true/ と \verb/false/ を持つデータ型である。
-Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。
-Set は階層構造を持ち、型集合の集合の型を指定するには Set1 と書く。
+Maybe はこのdata型の例である。
 
-\lstinputlisting[label=agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda}
 
 関数の定義は、関数名と型を記述した後に関数の本体を \verb/=/ の後に記述する。
 関数の型には $ \rightarrow $ 、 または\verb/->/ を用いる。
@@ -261,8 +223,9 @@
 引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
 これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなもので
 例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{agda-not}のようになる。
+% element の定義、縦棒　| の定義
+% SingleLinkedStack の説明に必要なものだけ
 
-\lstinputlisting[label=agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda}
 
 パターンマッチでは全てのコンストラクタのパターンを含まなくてはならない。
 例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。
@@ -287,54 +250,7 @@
 
 \lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda}
 
-データ型のコンストラクタには自分自身の型を引数に取ることもできる(リスト~\ref{agda-nat})。
-自然数のコンストラクタは2つあり、片方は自然数ゼロ、片方は自然数を取って後続数を返すものである。
-例えば0 は \verb/zero/ であり、1 は \verb/suc zero/に、3は \verb/suc (suc (suc zero))/ に対応する。
-
-\lstinputlisting[label=agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda}
-
-自然数に対する演算は再帰関数として定義できる。
-例えば自然数どうしの加算は二項演算子\verb/+/としてリスト~\ref{agda-plus}のように書ける。
-
-この二項演算子は中置関数として振る舞う。
-前置や後置で定義できる部分を関数名に \verb/_/ として埋め込んでおくと、関数を呼ぶ
-時にあたかも前置や後置演算子のように振る舞うことができる。
-例えば \verb/!_/ を定義すると \verb/! true/ のように利用でき、\verb/_~/ を定義すると \verb/false ~/ のように利用できる。
-
-また、Agda は再帰関数が停止するかを判別できる。
-この加算の二項演算子は左側がゼロに対しては明らかに停止する。
-左側が1以上の時の再帰時には \verb/suc n/ から \verb/n/へと減っているため、再帰で繰り返し減らすことでいつかは停止する。
-もし \verb/suc n/ のまま自分自身へと再帰した場合、Agda は警告を出す。
-
-\lstinputlisting[label=agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda}
-
-次に依存型について見ていく。
-依存型で最も基本的なものは関数型である。
-依存型を利用した関数は引数の型に依存して返す型を決定できる。
-なお、依存型の解決はモジュールのインポート時に行なわれる。
-
-Agda で \verb/(x : A) -> B/ と書くと関数は型 A を持つ x を受け取り、Bを返す。
-ここで B の中で x を扱っても良い。
-例えば任意の型に対する恒等関数はリスト~\ref{agda-id}のように書ける。
-
-\lstinputlisting[label=agda-id, caption=依存型を持つ関数の定義] {src/AgdaId.agda}
-
-この恒等関数 \verb/identitiy/ は任意の型に適用可能である。
-実際に関数 \verb/identitiy/ を Nat へ適用した例が \verb/identitiy-zero/ である。
-
-多相の恒等関数では型を明示的に指定せずとも \verb/zero/ に適用した場合の型は自明に \verb/Nat -> Nat/である。
-Agda はこのような推論をサポートしており、推論可能な引数は省略できる。
-推論によって解決される引数を暗黙的な引数(implicit arguments) と言い、変数を
-\verb/{}/ でくくることで表す。
-
-例えば、\verb/identitiy/ の対象とする型\verb/A/を暗黙的な引数として省略するとリスト~\ref{agda-implicit-id}のようになる。
-この恒等関数を利用する際は特定の型に属する値を渡すだけでその型が自動的に推論される。
-よって関数を利用する際は \verb/id-zero/ のように型を省略して良い。
-なお、関数の本体で暗黙的な引数を利用したい場合は \verb/{variableName}/ で束縛することもできる(\verb/id'/ 関数)。
-適用する場合も \verb/{}/でくくり、\verb/id-true/のように使用する。
-
-\lstinputlisting[label=agda-implicit-id, caption=Agdaにおける暗黙的な引数を持つ関数] {src/AgdaImplicitId.agda}
-
+% Stackのinterface 部分を使ってrecord の説明をする
 Agda のデータには C における構造体に相当するレコード型も存在する。
 定義を行なう際は \verb/record/キーワードの後にレコード名、型、\verb/where/ の後に \verb/field/ キーワードを入れた後、フィールド名と型名を列挙する。
 例えば x と y の二つの自然数からなるレコード \verb/Point/ を定義するとリスト~\ref{agda-record}のようになる。
@@ -350,29 +266,8 @@
 
 \lstinputlisting[label=agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda}
 
-\section{Agda での CodeGear 、 DataGear 、 継続の表現}
-Agda と CbC を対応して CodeGear、 DataGear、 継続を Agda で表現する。
-また、 Agda で継続を記述することで得た知見を示す。
-
-DataGear はレコード型で表現できるため、 Agda のレコード型をそのまま利用して定義
-していく。記述は~\ref{agda-ds}のようになる。
-
-% stack の DataGear の例を持ってくる
-\lstinputlisting[label=agda-ds, caption=Agda における DataGear の定義]
-{src/DataSegment.agda}
-
-CodeGear は DataGear を受け取って DataGear を返すという定義であるため、
-$ I \rightarrow O $ を内包する CodeGear 型のデータ型(~\ref{agda-cs})を定義する。
-
-\lstinputlisting[label=agda-cs, caption= Agda における CodeGear 型の定義] {src/CodeSegment.agda}
-
-CodeGear 型を定義することで、 Agda での CodeGear の本体は Agda での関数そのもの
-と対応する。
-
-CodeGear の実行は CodeGear 型から関数本体を取り出し、レコード型を持つ値を適用す
-ることに相当する。
-
-CbC での軽量継続は
+% push と pop だけ書いて必要なものだけ説明する
+% testStack08 を説明する。
 
 \begin{itemize}
  \item 次に実行する CodeGear を指定する