# HG changeset patch
# User ryokka
# Date 1580984672 -32400
# Node ID 8ef64db6349795407dfd0cd8fc2cca4f629b5a54
# Parent  d30593612a38cb08f71affdc52a94554dc9d774c
fix agda.tex

diff -r d30593612a38 -r 8ef64db63497 paper/Makefile
--- a/paper/Makefile	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/Makefile	Thu Feb 06 19:24:32 2020 +0900
@@ -19,7 +19,6 @@
 	platex  $(TARGET).tex
 	$(BIBTEX) $(TARGET)
 	platex  $(TARGET).tex
-	platex  $(TARGET).tex
 
 %.xbb: %.pdf
 	$(BB) $<
diff -r d30593612a38 -r 8ef64db63497 paper/agda.tex
--- a/paper/agda.tex	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/agda.tex	Thu Feb 06 19:24:32 2020 +0900
@@ -1,4 +1,4 @@
-\chapter{Agda}
+\chapter{定理証明支援系言語 Agda}
 \label{c:agda}
 Agda \cite{agda} とは定理証明支援器であり、関数型言語である。
 Agda は依存型という型システムを持ち、型を第一級オブジェクトとして扱うことが可能である。
@@ -8,77 +8,89 @@
 本章では Agda で証明をするために必要な要素を示し。
 また、Agda での証明について説明する。
 
-\section{Agda の文法}
-
-Agdaはインデントが意味を持ち、スペースの有無もチェックされる。
-コメントは \verb/-- comment/ や \verb/{-- comment --}/ のように記述される。
+\section{関数型言語としての Agda}
+Agda \cite{agda} は純粋関数型言語である。
+Agda は依存型という型システムを持ち、型を第一級オブジェクトとして扱う。
 
-Agda のプログラムは全てモジュール内部に記述されるため、各ファイルのトップレベルにモ
-ジュールを定義する必要がある。トップレベルのモジュールはファイル名と同一である。
+Agda の記述ではインデントが
+意味を持ち、スペースの有無もチェックされる。
+コメントは \verb/-- comment/ か \verb/{-- comment --}/ のように記述される。
+また、\verb/_/でそこに入りうるすべての値を示すことができ、
+\verb/?/でそこに入る値や型を不明瞭なままにしておくことができる。
 
-通常のモジュールをインポートする時は \verb/import/ キーワードを指定する。
+Agda のプログラムは全てモジュール内部に記述される。
+そのため、各ファイルのトップレベルにモジュールを定義する必要がある。
+トップレベルのモジュールはファイル名と同一になる。
+
+モジュール内で異なるモジュールをインポートする時は \verb/import/ キーワードを指定する。
 インポートを行なう際、モジュール内部の関数を別名に変更するには \verb/as/ キーワードを用いる。
 他にも、モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワード、
 関数名を、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠
 す場合は \verb/hiding/ キーワードを用いる。
 なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/open import/ キーワードを使うことで展開できる。
-モジュールをインポートする例をリスト~\ref{src:agda-import}に示す。
+モジュールをインポートする例を\coderef{src:agda-import}に示す。
 
-\lstinputlisting[label=src:agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda.replaced}
+\lstinputlisting[label=src:agda-import, caption=モジュールのインポートとオプション] {src/AgdaImport.agda.replaced}
 
 
 \section{Agda のデータ}
-Agda における型指定は : を用いて行う。 変数 x が型 A を持つ、ということを表すには x : A と記述する。
-データ型は、代数的なデータ構造で、その定義には data キーワードを用いる。
-data キーワードの後に data の名前と、型、 where 句を書きインデントを深くした後、
+Agda 型をデータや関数に記述する必要がある。
+Agda における型指定は \verb/:/ を用いて \verb/name : type/ のように記述する。
+データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。
+\verb/data/ キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くし、
 値にコンストラクタとその型を列挙する。
 
-例えば Bool 型を定義するとリスト~\ref{src:agda-bool}のようになる。
-Bool はコンストラクタ \verb/true/ と \verb/false/ を持つデータ型である。
-Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。
-Set は階層構造を持ち、型集合の集合の型を指定するには Set1 と書く
+\coderef{src:agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)を例である。
+
+\lstinputlisting[label=src:agda-nat, caption=自然数を表すデータ型 Nat の定義] {src/nat.agda.replaced}
 
-\lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda.replaced}
+\verb/Nat/ では \verb/zero/ と \verb/suc/ の2つのコンストラクタを持つデータ型である。
+\verb/suc/ は $\mathbb{N}$ を受け取って $\mathbb{N}$ を表す再帰的なデータになっており、
+\verb/suc/ を連ねることで自然数全体を表現することができる。
 
+$\mathbb{N}$ 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。
+\verb/Set/ は階層構造を持ち、型集合の集合の型を指定するには \verb/Set1/ と書く。
+%% \verb/Level/ を用いることで異なる \verb/Set/ を表現できる。
 
-Agda には C における構造体に相当するレコード型というデータも存在する、
-例えば x と y の二つの自然数からなるレコード \verb/Point/ を定義するとリスト~\ref{src:agda-record}のようになる。
-レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。
-複数の値を列挙する際は \verb/;/ で区切る。
-
+Agda には C 言語における構造体に相当するレコード型というデータも存在する、
+例えば \verb/x/ と \verb/y/ の二つの自然数からなるレコード \verb/Point/ を定義する。\coderef{src:agda-record}のようになる。
 \lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda.replaced}
+レコードを構築する際は \verb/record/ キーワード後の \verb/{}/ の内部に \verb/FieldName = value/ の形で値を列挙する。
+複数の値を列挙するには \verb/;/ で区切る必要がある。
 
 
 \section{Agda の関数}
-
-Agda での関数の定義は、関数名と型を記述した後に関数の本体を \verb/=/ の後に記述する。
-関数の型には $ \rightarrow $ 、 または\verb/->/ を用いる。
+Agda での関数は型の定義と、関数の定義をする必要がある。
+関数の型はデータと同様に \verb/:/ を用いて \verb/name : type/ に記述するが、入力を受け取り出力返す型として記述される。$\rightarrow$ 、 または\verb/→/ を用いて \verb/input → output/ のように記述される。
+関数の定義は型の定義より下の行に、\verb/=/ を使い \verb/name input = output/ のように記述される。
 
-例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A -> B/ のように書くことができる。
-また、複数の引数を取る関数の型は \verb/A -> A -> B/ のように書ける。この
-時の型は \verb/A -> (A -> B)/のように考えられる。
-Bool 変数 \verb/x/ を取って true を返す関数 \verb/f/はリスト~\ref{src:agda-function}のようになる。
+例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A → B/ のように書くことができる。
+また、複数の引数を取る関数の型は \verb/A → A → B/ のように書ける。
+この時の型は \verb/A → (A → B)/のように考えられる。
+%% 変数 \verb/x/ を取って true を返す関数 \verb/f/は\tabref{src:agda-function}のようになる。
+例として任意の自然数$mathbb{N}$を受け取り、\verb/+1/した値を返す関数は\coderef{src:agda-function}のように定義できる。
+\lstinputlisting[label=src:agda-function, caption=Agda における関数定義] {src/agda-func.agda.replaced}
 
-\lstinputlisting[label=src:agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda.replaced}
 
 引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
-これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなもので
-例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。
+これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。
+例として自然数$mathbb{N}$の加算を関数で書くと\coderef{agda-plus}のようになる。
 
-\lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced}
+\lstinputlisting[label=src:agda-plus, caption=自然数での加算の定義] {src/agda-plus.agda.replaced}
+%% \lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced}
+\verb/_+_/のように関数名で\verb/_/を使用すると引数がその位置にあることを意味する。
 
-パターンマッチでは全てのコンストラクタのパターンを含まなくてはならない。
-例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。
-なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。
-例えばリスト~\ref{src:agda-pattern}の not は x には true しか入ることは無い。
-なお、マッチした値以外の挙動をまとめて書く際には \verb/_/ を用いることもできる。
+パターンマッチでは全てのコンストラクタのパターンを含む必要がある。
+例えば、自然数$mathbb{N}$を受け取る関数では \verb/zero/ と \verb/suc/ の2つのパターンが存在する必要がある。
+なお、コンストラクタをいくつか指定した後に変数で受けることもでき、その変数では指定されたもの以外を受けることができる。
+例えば\coderef{src:agda-pattern}の減算では初めのパターンで2つ目の引数が\verb/zero/のすべてのパターンが入る。
+
 
-\lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda.replaced}
+\lstinputlisting[label=src:agda-pattern, caption=自然数の減算によるパターンマッチの例] {src/agda-pattern.agda.replaced}
 
-Agda にはラムダ計算が存在している。ラムダ計算とは関数内で生成できる無名の関数であり、
-\verb/\arg1 arg2 -> function body/ のように書くことができる。
-例えば Bool 型の引数 \verb/b/ を取って not を適用する \verb/not-apply/ をラムダ計算で書くとリスト~\ref{src:agda-lambda}のようになる。
-関数 \verb/not-apply/ をラムダ計算を使わずに定義すると \verb/not-apply-2/ になるが、この二つの関数は同一の動作をする。
+Agda には$\lambda$計算が存在している。$\lambda$計算とは関数内で生成できる無名の関数であり、
+\verb/\arg1 arg2 → function/ のように書くことができる。
+\coderef{agda-function} で例とした \verb/+1/ をラムダ計算で書くと\coderef{src:agda-lambda}の\verb/$\lambda$+1/ように書くことができる。この二つの関数は同一の動作をする。
 
 \lstinputlisting[label=src:agda-lambda, caption=Agda におけるラムダ計算] {src/AgdaLambda.agda.replaced}
 
@@ -92,13 +104,13 @@
 
 
 \section{定理証明支援器としての Agda}
-Agda での証明では型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明が完成する。
-証明の例として Code \ref{proof} を見る。
-ここでの $+zero$ は右から zero を足しても $\equiv$ の両辺は等しいことを証明している。
-これは、引数として受けている y が Nat なので、 zero の時と suc y の二つの場合を証明する必要がある。
+Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である。
+証明の例として Code \coderef{proof} を見る。
+ここでの \verb/+zero/ は右から \verb/zero/ を足しても $\equiv$ の両辺は等しいことを証明している。
+これは、引数として受けている \verb/y/ が \verb/Nat/ なので、 \verb/zero/ の時と \verb/suc y/ の二つの場合を証明する必要がある。
 
-$y = zero$ の時は両辺が zero とできて、左右の項が等しいということを表す refl で証明することができる。
-$y = suc y$ の時は x == y の時 fx == fy が成り立つという cong を使って、y の値を 1 減らしたのちに再帰的に $+zero y$
+\verb/y = zero/ の時は両辺が \verb/zero/ とできて、左右の項が等しいということを表す \verb/refl/ で証明することができる。
+\verb/y = suc y/ の時は $x \equiv y$ の時 $fx \equiv fy$ が成り立つという \verb/cong/ を使って、y の値を 1 減らしたのちに再帰的に \verb/+zero y/
 を用いて証明している。
 
 \lstinputlisting[caption=等式変形の例,label=proof]{src/zero.agda.replaced}
@@ -108,59 +120,85 @@
 %% +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
 %% \end{lstlisting}
 
-また、他にも $\lambda$ 項部分で等式を変形する構文が存在している。
- Code \ref{agda-term-pre}、 \ref{agda-term-post} は等式変形の例である。
-始めに等式変形を始めたいところで $let open \equiv-Reasoning  in begin$と記述する。
-Agda 上では分からないところを ? と置いておくことができるので、残りを ? としておく。
-$--$ は Agda 上ではコメントである。
+また、他にも $\lambda$ 項部分で等式を変形する構文がいくつか存在している。
+ここでは \verb/rewrite/ と $\equiv$\verb/-Reasoning/ の構文を説明するとともに、等式を変形する構文の例として加算の交換則について示す。
+
+\verb/rewrite/ では 関数の \verb/=/ 前に \verb/rewrite 変形規則/ の形で記述し、複数の規則を使う場合は \verb/rewrite/ 変形規則1 \verb/|/ 変形規則2 のように \verb/|/を用いて記述する。
+\coderef{agda-rewrite} にある \verb/+-comm/ で \verb/x/ が \verb/zero/ のパターンが良い例である。
+ここでは、\verb/+zero/ を利用し、 \verb/zero + y/ を \verb/y/ に変形することで $y \equiv y$となり、左右の項が等しいことを示す \verb/refl/ になっている。
 
-\lstinputlisting[caption=等式変形の例1/2,label=agda-term-pre]{src/term1.agda.replaced}
-%% \begin{lstlisting}[caption=等式変形の例1/3,label=agda-term-pre]
-%% stmt2Cond : {c10 : ℕ} → Cond
-%% stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
+\lstinputlisting[caption=rewrite での等式変形の例,label=agda-rewrite]{src/agda-rewrite.agda.replaced}
+
+\coderef{agda-term-pre}、\coderef{agda-term-mid}、 \coderef{agda-term-post} は$\equiv$\verb/-Reasoning/を用いた等式変形の流れである。
+始めに等式変形を始めたいところで \verb/let open/ $\equiv$ \verb/-Reasoning in begin/と記述し、
+\verb/変形前/ $\equiv$ $\langle$ \verb/変形規則/ $\rangle$ \verb/変形後/ の形で記述して、
+最後に $\blacksquare$ をつけて変形を終える。
+この \verb/let open/ から $\blacksquare$ までの流れは1行で記述しても良いし、改行やインデントを含めても良い。
+\coderef{agda-term-pre}の例では分からないところを \verb/?/ と置いておき、
+\verb/?/ の中で示されている値は下にコメントで示しておく。
 
-%% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\
-%% 10})
-%% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
+\lstinputlisting[caption=等式変形の例1/3,label=agda-term-pre]{src/agda-term1.agda.replaced}
+%% \begin{lstlisting}[caption=等式変形の例1/3,label=agda-term-pre]
+%% +-suc : {x y : ℕ} → x + suc y ≡ suc (x + y)
+%% +-suc {zero} {y} = refl
+%% +-suc {suc x} {y} = cong suc (+-suc {x} {y})
+
+%% +-comm : (x y : ℕ) → x + y ≡ y + x
+%% +-comm zero y rewrite (+zero {y}) = refl
+%% +-comm (suc x) y = let open ≡-Reasoning in
 %%   begin
-%%     ?      -- ?0
-%%   ≡⟨ ? ⟩  -- ?1
-%%     ?      -- ?2
-%%   ∎ )
+%%   ?0 ≡⟨ ?1 ⟩
+%%   ?2 ∎
 
-%% -- ?0 : Bool
-%% -- ?1 : stmt2Cond (record { varn = varn env ; vari = 0 }) ≡ true
-%% -- ?2 : Bool
+%% -- ?0 : (suc x) + y
+%% -- ?1 : suc x + y ≡ y + suc x
+%% -- ?2 : y + (suc x)
 %% \end{lstlisting}  
 
-この状態で実行すると  ? 部分に入る型を Agda が示してくれる。
-始めに変形する等式を ?0 に記述し、?1 の中に $x == y$ のような変形規則を入れることで等式を変形して証明することができる。
-
-ここでは \ref{agda-term-mid} の Bool 値 x を受け取って $x \wedge true$ の時必ず x であるという証明 $\wedge$true と 値と Env を受け取って Bool 値を返す stmt1Cond を使って等式変形を行う。
-\lstinputlisting[caption=使っている等式変形規則,label=agda-term-mid]{src/term2.agda.replaced}
-%% \begin{lstlisting}[caption=等式変形の例2/3,label=agda-term-mid]
-%% ∧true : { x : Bool } →  x  ∧  true  ≡ x
-%% ∧true {x} with x
-%% ∧true {x} | false = refl
-%% ∧true {x} | true = refl
+この状態で実行すると \verb/?/ 部分に入る型を Agda が示してくれる。
+始めに変形する等式を ?0 に記述し、?1 の中に変形規則を使用することで等式を変形できる。
+ここでの方針は \verb/(suc x) + y/ を \verb/suc (x + y)/ 変形してやり、
+\verb/y + (suc x)/ も同様に \verb/ suc (x + y)/ の形に変形することで等しさを証明する。
+Agda の加算では左側に \verb/suc/ がついていた場合外に \verb/suc/ を出して再帰的に中身と足し算を行うため、
+何もせずに \verb/(suc x) + y/ は \verb/suc (x + y)/ に変換できる。
+\coderef{agda-term-mid} では \verb/suc (x + y)/ に対して \verb/cong/ で \verb/suc/ を外に出し　\verb/+comm/ を再帰的に利用することで \verb/suc (y + x)/ へ変換している。
 
-%% stmt1Cond : {c10 : ℕ} → Cond
-%% stmt1Cond {c10} env = Equal (varn env) c10
-%% \end{lstlisting}
+\lstinputlisting[caption=等式変形の例2/3,label=agda-term-mid]{src/agda-term2.agda.replaced}
+%% \begin{lstlisting}[caption=等式変形の例2/3,label=agda-term-mid]
+%% +-comm : (x y : ℕ) → x + y ≡ y + x
+%% +-comm zero y rewrite (+zero {y}) = refl
+%% +-comm (suc x) y = let open ≡-Reasoning in
+%%   begin
+%%   (suc x) + y ≡⟨⟩
+%%   suc (x + y) ≡⟨ cong suc (+-comm x y) ⟩
+%%   suc (y + x) ≡⟨ ?0 ⟩
+%%   ?1 ∎
 
-最終的な証明は\ref{agda-term-post} のようになる。
-\lstinputlisting[caption=等式変形の例2/2,label=agda-term-post]{src/term3.agda.replaced}
-%% \begin{lstlisting}[caption=等式変形の例2/2,label=agda-term-post]
-%% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\
-%% 10})
-%% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
-%%   begin
-%%     (Equal (varn env) c10 ) ∧ true
-%%   ≡⟨ ∧true ⟩
-%%     Equal (varn env) c10
-%%   ≡⟨ cond ⟩
-%%     true
-%%   ∎ )
+%% -- ?0 : suc (y + x) ≡ y + suc x
+%% -- ?1 : y + suc x
+
 %% \end{lstlisting}
 
 
+
+\coderef{agda-term-post} では \verb/suc (y + x)/ $equiv$ \verb/y + (suc x)/ という等式に対して $equiv$ の対称律 \verb/sym/ を使って左右の項を反転させ\verb/y + (suc x)/ $equiv$ \verb/suc (y + x)/の形にし、\verb/y + (suc x)/が\verb/suc (y + x)/ に変形できることを \verb/+-suc/ を用いて示した。
+これにより等式の左右の項が等しくなったため \verb/+-comm/ が示せた。
+\lstinputlisting[caption=等式変形の例3/3,label=agda-term-post]{src/agda-term3.agda.replaced}
+%% \begin{lstlisting}[caption=等式変形の例2/2,label=agda-term-post]
+%% +-comm : (x y : ℕ) → x + y ≡ y + x
+%% +-comm zero y rewrite (+zero {y}) = refl
+%% +-comm (suc x) y = let open ≡-Reasoning in
+%%   begin
+%%   suc (x + y) ≡⟨⟩
+%%   suc (x + y) ≡⟨ cong suc (+-comm x y) ⟩
+%%   suc (y + x) ≡⟨ sym (+-suc {y} {x}) ⟩
+%%   y + suc x ∎
+
+%% -- +-suc : {x y : ℕ} → x + suc y ≡ suc (x + y)
+%% -- +-suc {zero} {y} = refl
+%% -- +-suc {suc x} {y} = cong suc (+-suc {x} {y})
+%% \end{lstlisting}
+Agda ではこのような形で等式を変形しながら証明を行う事ができる。
+
+%% 例として先程の \verb/+-comm/ を rewrite で証明した \verb/rewrite-+-comm/ を \coderef{agda-rewrite} を載せる。
+
diff -r d30593612a38 -r 8ef64db63497 paper/cbc.tex
--- a/paper/cbc.tex	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/cbc.tex	Thu Feb 06 19:24:32 2020 +0900
@@ -15,22 +15,19 @@
 CodeGear の入力となる DataGear を Input DataGear と呼び、
 出力は Output DataGear と呼ぶ。
 
-CodeGear はプログラムの処理そのもので、図 Code \ref{fig:cgdg}で示しているように任意の数の
+CodeGear はプログラムの処理そのもので、\figref{fig:cgdg}で示しているように任意の数の
 Input DataGear を参照し、処理が完了すると任意の数の Output DataGear に書き込む。
 
 CodeGear 間の移動は継続を用いて行われる。継続は関数呼び出しとは異なり、呼び出し
 た後に元のコードに戻らず、次の CodeGear へ継続を行う。
 これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当する。
 
-図\ref{fig:csds}のように Input DataGear を受け取り、 CodeGear で処理を行い、
-Output DataGear に変更を加え、プログラム全体を記述する。
-
 \begin{figure}[htpb]
  \begin{center}
-  \scalebox{0.50}{\includegraphics{fig/cgdg.pdf}}
+  \scalebox{0.6}{\includegraphics{fig/cgdg.pdf}}
  \end{center}
  \caption{CodeGear と DataGear}
- \label{fig:csds}
+ \label{fig:cgdg}
 \end{figure}
 
 
@@ -42,17 +39,20 @@
 そのため、 CbC ではメタ計算を分離するために Meta CodeGear、 Meta DataGear を定義している。
 
 Meta CodeGear は CbC 上でのメタ計算で、通常の CodeGear を実行する際に必要なメタ計算を分離するための単位である。
+\figref{fig:meta-cgdg} のように CodeGear を実行する前後や DataGear の大枠として Meta Gear が存在している。
 
-例えば、 CbC では CodeGear を実行する際、ノーマルレベルの計算からは見えないが必要な DataGear を Context と呼ばれる Meta DataGear を通して取得することになる。これはユーザーが直接データを扱える状態では信頼性が高いとは言えないと考えるからである。
+\begin{figure}[htpb]
+ \begin{center}
+  \scalebox{0.5}{\includegraphics{fig/meta-cg-dg.pdf}}
+ \end{center}
+ \caption{メタ計算を可視化した CodeGear と DataGear}
+ \label{fig:meta-cgdg}
+\end{figure}
+
+
+例として CodeGear が DataGear から値を取得する際に使われる Meta CodeGear である stub CodeGear について説明する。
+CbC では CodeGear を実行する際、ノーマルレベルの計算からは見えないが必要な DataGear を Context と呼ばれる Meta DataGear を通して取得することになる。これはユーザーが直接データを扱える状態では信頼性が高いとは言えないと考えるからである。
 そのために、 Meta CodeGear を用いて Context から必要な DataGear を取り出し、 CodeGear に接続する stub CodeGear という Meta CodeGear が定義されている。
 
 Meta DataGear は CbC 上のメタ計算で扱われる DataGear である。
 例えば stub CodeGear では Context と呼ばれる接続可能な CodeGear、 DataGear のリストや、DataGear のメモリ空間等を持った Meta DataGear を扱っている。
-
-\begin{figure}[htpb]
- \begin{center}
-  \scalebox{0.55}{\includegraphics{fig/meta_cg_dg.pdf}}
- \end{center}
- \caption{メタ計算を可視化した CodeGear と DataGear}
- \label{fig:meta-cgdg}
-\end{figure}
diff -r d30593612a38 -r 8ef64db63497 paper/fig/WorkerRun.xbb
--- a/paper/fig/WorkerRun.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/WorkerRun.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/workerRun.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 824 309
 %%HiResBoundingBox: 0.000000 0.000000 824.000000 309.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Tue Feb 13 05:26:03 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/bitonicNetwork.xbb
--- a/paper/fig/bitonicNetwork.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/bitonicNetwork.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/bitonicNetwork.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 591 422
 %%HiResBoundingBox: 0.000000 0.000000 591.000000 422.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Sat Feb  3 19:57:43 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/bitonicSort.xbb
--- a/paper/fig/bitonicSort.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/bitonicSort.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/bitonicSort.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 600 480
 %%HiResBoundingBox: 0.000000 0.000000 600.000000 480.000000
 %%PDFVersion: 1.5
 %%Pages: 1
-%%CreationDate: Sat Feb  3 22:27:55 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/cbc-hoare.xbb
--- a/paper/fig/cbc-hoare.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/cbc-hoare.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 580.000000 175.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 20 14:41:03 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/cbc-subtype.xbb
--- a/paper/fig/cbc-subtype.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/cbc-subtype.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 1084.000000 281.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 20 14:41:03 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/cgdg.xbb
--- a/paper/fig/cgdg.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/cgdg.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 535.000000 427.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Wed Feb  5 01:55:59 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/codegear-datagear.xbb
--- a/paper/fig/codegear-datagear.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/codegear-datagear.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/codegear-datagear.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 535 427
 %%HiResBoundingBox: 0.000000 0.000000 535.000000 427.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Tue Feb 13 00:39:37 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/codesegment.xbb
--- a/paper/fig/codesegment.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/codesegment.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 305.000000 85.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 20 14:41:03 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/codesegment2.xbb
--- a/paper/fig/codesegment2.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/codesegment2.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 393.000000 201.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 20 14:41:03 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/csds.xbb
--- a/paper/fig/csds.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/csds.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 580.000000 76.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 20 14:41:04 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/cudaArchitecture.xbb
--- a/paper/fig/cudaArchitecture.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/cudaArchitecture.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/cudaArchitecture.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 446 488
 %%HiResBoundingBox: 0.000000 0.000000 446.000000 488.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Thu Feb  1 07:03:30 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/cudaDataArchitecture.xbb
--- a/paper/fig/cudaDataArchitecture.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/cudaDataArchitecture.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/cudaDataArchitecture.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 448 598
 %%HiResBoundingBox: 0.000000 0.000000 448.000000 598.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Tue Feb 13 04:47:33 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/dependency.xbb
--- a/paper/fig/dependency.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/dependency.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/dependency.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 573 273
 %%HiResBoundingBox: 0.000000 0.000000 573.000000 273.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Tue Feb 13 05:27:27 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/factorial.xbb
--- a/paper/fig/factorial.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/factorial.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 296.000000 220.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 20 14:41:04 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/gears-meta.xbb
--- a/paper/fig/gears-meta.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/gears-meta.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 653.000000 243.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 20 14:41:04 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/goto.xbb
--- a/paper/fig/goto.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/goto.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 305.000000 85.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 20 14:41:04 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/gotoInterface.xbb
--- a/paper/fig/gotoInterface.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/gotoInterface.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/gotoInterface.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 793 724
 %%HiResBoundingBox: 0.000000 0.000000 793.000000 724.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Sun Feb  4 21:45:54 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/hoare-logic.xbb
--- a/paper/fig/hoare-logic.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/hoare-logic.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 580.000000 76.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 20 14:41:04 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/iterateTaskExec.xbb
--- a/paper/fig/iterateTaskExec.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/iterateTaskExec.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/iterateTaskExec.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 749 310
 %%HiResBoundingBox: 0.000000 0.000000 749.000000 310.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Wed Jan 31 20:11:02 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/meta-cg-dg.xbb
--- a/paper/fig/meta-cg-dg.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/meta-cg-dg.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
-%%Title: fig/meta-cg-dg.pdf
+%%Title: meta-cg-dg.pdf
 %%Creator: extractbb 20190225
 %%BoundingBox: 0 0 608 202
 %%HiResBoundingBox: 0.000000 0.000000 608.000000 202.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Wed Feb  5 02:00:05 2020
+%%CreationDate: Wed Feb  5 19:14:51 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/meta-hierarchy.xbb
--- a/paper/fig/meta-hierarchy.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/meta-hierarchy.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 832.000000 283.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 20 14:41:04 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/meta.xbb
--- a/paper/fig/meta.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/meta.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 958.000000 148.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 20 14:41:05 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/meta_cg_dg.xbb
--- a/paper/fig/meta_cg_dg.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/meta_cg_dg.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/meta_cg_dg.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 608 202
 %%HiResBoundingBox: 0.000000 0.000000 608.000000 202.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Tue Feb 13 00:36:02 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/metameta.xbb
--- a/paper/fig/metameta.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/metameta.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 472.000000 184.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 20 14:41:05 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/non-destructive-rbtree.xbb
--- a/paper/fig/non-destructive-rbtree.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/non-destructive-rbtree.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 559.000000 248.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 20 14:41:05 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/put.xbb
--- a/paper/fig/put.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/put.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 868.000000 130.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 20 14:41:05 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/putSynchronizedQueue1.xbb
--- a/paper/fig/putSynchronizedQueue1.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/putSynchronizedQueue1.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/putSynchronizedQueue1.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 746 301
 %%HiResBoundingBox: 0.000000 0.000000 746.000000 301.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Wed Jan 24 02:45:08 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/putSynchronizedQueue2.xbb
--- a/paper/fig/putSynchronizedQueue2.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/putSynchronizedQueue2.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/putSynchronizedQueue2.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 825 391
 %%HiResBoundingBox: 0.000000 0.000000 825.000000 391.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 29 20:29:39 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/rbtree.xbb
--- a/paper/fig/rbtree.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/rbtree.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 562.000000 274.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 20 14:41:05 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/ryukyu.xbb
--- a/paper/fig/ryukyu.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/ryukyu.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/ryukyu.pdf
-%%Creator: extractbb 20160307
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 595 842
 %%HiResBoundingBox: 0.000000 0.000000 595.000000 842.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Sun Jan 28 19:06:39 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/semaphoreSequence.xbb
--- a/paper/fig/semaphoreSequence.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/semaphoreSequence.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/semaphoreSequence.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 1120 869
 %%HiResBoundingBox: 0.000000 0.000000 1120.000000 869.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Sun Feb  4 15:57:13 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/sendTask.xbb
--- a/paper/fig/sendTask.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/sendTask.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/sendTask.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 722 374
 %%HiResBoundingBox: 0.000000 0.000000 722.000000 374.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Tue Feb 13 05:26:03 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/subtype-arg.xbb
--- a/paper/fig/subtype-arg.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/subtype-arg.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 1084.000000 281.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 20 14:41:05 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/subtype-return.xbb
--- a/paper/fig/subtype-return.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/subtype-return.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 1084.000000 281.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Jan 20 14:41:06 2020
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/takeSynchronizedQueue1.xbb
--- a/paper/fig/takeSynchronizedQueue1.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/takeSynchronizedQueue1.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/takeSynchronizedQueue1.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 571 202
 %%HiResBoundingBox: 0.000000 0.000000 571.000000 202.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Wed Jan 24 02:45:08 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/takeSynchronizedQueue2.xbb
--- a/paper/fig/takeSynchronizedQueue2.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/takeSynchronizedQueue2.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/takeSynchronizedQueue2.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 561 202
 %%HiResBoundingBox: 0.000000 0.000000 561.000000 202.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Wed Jan 24 02:45:08 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/twice.xbb
--- a/paper/fig/twice.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/twice.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/twice.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 600 480
 %%HiResBoundingBox: 0.000000 0.000000 600.000000 480.000000
 %%PDFVersion: 1.5
 %%Pages: 1
-%%CreationDate: Tue Feb  6 04:08:41 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/vsgo.xbb
--- a/paper/fig/vsgo.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/vsgo.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/vsgo.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 600 480
 %%HiResBoundingBox: 0.000000 0.000000 600.000000 480.000000
 %%PDFVersion: 1.5
 %%Pages: 1
-%%CreationDate: Wed Feb 28 23:36:32 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/fig/vsopenmp.xbb
--- a/paper/fig/vsopenmp.xbb	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/fig/vsopenmp.xbb	Thu Feb 06 19:24:32 2020 +0900
@@ -1,8 +1,8 @@
 %%Title: fig/vsopenmp.pdf
-%%Creator: extractbb 20170318
+%%Creator: extractbb 20190225
 %%BoundingBox: 0 0 600 480
 %%HiResBoundingBox: 0.000000 0.000000 600.000000 480.000000
 %%PDFVersion: 1.5
 %%Pages: 1
-%%CreationDate: Wed Feb 28 23:36:32 2018
+%%CreationDate: Wed Feb  5 17:52:45 2020
 
diff -r d30593612a38 -r 8ef64db63497 paper/master_paper.pdf
Binary file paper/master_paper.pdf has changed
diff -r d30593612a38 -r 8ef64db63497 paper/master_paper.tex
--- a/paper/master_paper.tex	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/master_paper.tex	Thu Feb 06 19:24:32 2020 +0900
@@ -37,9 +37,9 @@
 %    Gears OS の並列処理
 %\end{minipage}}
 
-\newcommand\figref[1]{図 \ref{fig:#1}}
-\newcommand\tabref[1]{表 \ref{tab:#1}}
-\newcommand\coderef[1]{ソースコード \ref{code:#1}}
+\newcommand\figref[1]{図 \ref{#1}}
+\newcommand\tabref[1]{表 \ref{#1}}
+\newcommand\coderef[1]{ソースコード \ref{#1}}
 
 \lstset{
   frame=single,
diff -r d30593612a38 -r 8ef64db63497 paper/src/AgdaLambda.agda
--- a/paper/src/AgdaLambda.agda	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/src/AgdaLambda.agda	Thu Feb 06 19:24:32 2020 +0900
@@ -1,5 +1,5 @@
-not-apply : Bool -> Bool
-not-apply = (\b -> not b)   -- use lambda
++1 : ℕ → ℕ
++1 n = suc n -- not use lambda
 
-not-apply : Bool -> Bool
-not-appy b = not b          -- not use lambda
+λ+1 : ℕ → ℕ
+λ+1 = (\n -> suc n)   -- use lambda
diff -r d30593612a38 -r 8ef64db63497 paper/src/AgdaLambda.agda.replaced
--- a/paper/src/AgdaLambda.agda.replaced	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/src/AgdaLambda.agda.replaced	Thu Feb 06 19:24:32 2020 +0900
@@ -1,5 +1,5 @@
-not-apply : Bool @$\rightarrow$@ Bool
-not-apply = (\b @$\rightarrow$@ not b)   -- use lambda
++1 : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@
++1 n = suc n -- not use lambda
 
-not-apply : Bool @$\rightarrow$@ Bool
-not-appy b = not b          -- not use lambda
+@$\lambda$@+1 : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@
+@$\lambda$@+1 = (\n @$\rightarrow$@ suc n)   -- use lambda
diff -r d30593612a38 -r 8ef64db63497 paper/src/Nat.agda
--- a/paper/src/Nat.agda	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/src/Nat.agda	Thu Feb 06 19:24:32 2020 +0900
@@ -1,5 +1,5 @@
-module nat where
-  
-data Nat : Set where
-  O : Nat
-  S : Nat -> Nat
\ No newline at end of file
+data ℕ : Set where
+  zero : ℕ
+  suc  : ℕ → ℕ
+
+
diff -r d30593612a38 -r 8ef64db63497 paper/src/Nat.agda.replaced
--- a/paper/src/Nat.agda.replaced	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/src/Nat.agda.replaced	Thu Feb 06 19:24:32 2020 +0900
@@ -1,5 +1,5 @@
-module nat where
-  
-data Nat : Set where
-  O : Nat
-  S : Nat @$\rightarrow$@ Nat
\ No newline at end of file
+data @$\mathbb{N}$@ : Set where
+  zero : @$\mathbb{N}$@
+  suc  : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@
+
+
diff -r d30593612a38 -r 8ef64db63497 paper/src/agda-func.agda.replaced
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/agda-func.agda.replaced	Thu Feb 06 19:24:32 2020 +0900
@@ -0,0 +1,5 @@
++1 : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@
++1 m = suc m
+
+-- eval +1 zero
+-- return suc zero
diff -r d30593612a38 -r 8ef64db63497 paper/src/agda-pattern.agda.replaced
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/agda-pattern.agda.replaced	Thu Feb 06 19:24:32 2020 +0900
@@ -0,0 +1,4 @@
+_-_ : Nat @$\rightarrow$@ Nat @$\rightarrow$@ Nat
+n     - zero = n      -- "n - zero" have 2-pattern, "zero - zero" "suc n - zero"
+zero  - suc m = zero
+suc n - suc m = n - m
diff -r d30593612a38 -r 8ef64db63497 paper/src/agda-plus.agda.replaced
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/agda-plus.agda.replaced	Thu Feb 06 19:24:32 2020 +0900
@@ -0,0 +1,3 @@
+_+_ : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@
+zero  + m = m
+suc n + m = suc (n + m)
diff -r d30593612a38 -r 8ef64db63497 paper/src/agda-term.agda.replaced
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/agda-term.agda.replaced	Thu Feb 06 19:24:32 2020 +0900
@@ -0,0 +1,28 @@
+module agda-term where
+
+open import Data.Nat.Base
+open import Relation.Binary.PropositionalEquality
+
++zero : {y : @$\mathbb{N}$@} @$\rightarrow$@ y + zero @$\equiv$@ y
++zero {zero} = refl
++zero {suc y} = cong (@$\lambda$@ yy @$\rightarrow$@ suc yy) (+zero {y})
+
++-suc : {x y : @$\mathbb{N}$@} @$\rightarrow$@ x + suc y @$\equiv$@ suc (x + y)
++-suc {zero} {y} = refl
++-suc {suc x} {y} = cong suc (+-suc {x} {y})
+
++-comm : (x y : @$\mathbb{N}$@) @$\rightarrow$@ x + y @$\equiv$@ y + x
++-comm zero y rewrite (+zero {y}) = refl
++-comm (suc x) y = let open @$\equiv$@-Reasoning in
+  begin
+  suc (x + y) @$\equiv$@@$\langle$@@$\rangle$@
+  suc (x + y) @$\equiv$@@$\langle$@ cong suc (+-comm x y) @$\rangle$@
+  suc (y + x) @$\equiv$@@$\langle$@ sym (+-suc {y} {x}) @$\rangle$@
+  y + suc x @$\blacksquare$@
+
++-come : (x y : @$\mathbb{N}$@) @$\rightarrow$@ x + y @$\equiv$@ y + x
++-come zero y rewrite (+zero {y}) = refl
++-come (suc x) y
+  rewrite (cong suc (+-come x y)) | sym (+-suc {y} {x}) = refl
+
+
diff -r d30593612a38 -r 8ef64db63497 paper/src/agda-term1.agda.replaced
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/agda-term1.agda.replaced	Thu Feb 06 19:24:32 2020 +0900
@@ -0,0 +1,10 @@
++-comm : (x y : @$\mathbb{N}$@) @$\rightarrow$@ x + y @$\equiv$@ y + x
++-comm zero y rewrite (+zero {y}) = refl
++-comm (suc x) y = let open @$\equiv$@-Reasoning in
+  begin
+  ?0 @$\equiv$@@$\langle$@ ?1 @$\rangle$@
+  ?2 @$\blacksquare$@
+
+-- ?0 : @$\mathbb{N}$@ {(suc x) + y}
+-- ?1 : suc x + y @$\equiv$@ y + suc x
+-- ?2 : @$\mathbb{N}$@
diff -r d30593612a38 -r 8ef64db63497 paper/src/agda-term2.agda.replaced
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/agda-term2.agda.replaced	Thu Feb 06 19:24:32 2020 +0900
@@ -0,0 +1,11 @@
++-comm : (x y : @$\mathbb{N}$@) @$\rightarrow$@ x + y @$\equiv$@ y + x
++-comm zero y rewrite (+zero {y}) = refl
++-comm (suc x) y = let open @$\equiv$@-Reasoning in
+  begin
+  (suc x) + y @$\equiv$@@$\langle$@@$\rangle$@
+  suc (x + y) @$\equiv$@@$\langle$@ cong suc (+-comm x y) @$\rangle$@
+  suc (y + x) @$\equiv$@@$\langle$@ ?0 @$\rangle$@
+  ?1 @$\blacksquare$@
+
+-- ?0 : suc (y + x) @$\equiv$@ y + suc x
+-- ?1 : y + suc x
diff -r d30593612a38 -r 8ef64db63497 paper/src/term1.agda
--- a/paper/src/term1.agda	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/src/term1.agda	Thu Feb 06 19:24:32 2020 +0900
@@ -1,14 +1,14 @@
 stmt2Cond : {c10 :ℕ} → Cond
 stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
 
-lemma1 : {c10 :ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\
-10})
+lemma1 : {c10 :ℕ} → Axiom (stmt1Cond {c10})
+       (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
 lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
-begin
-?      -- ?0
-≡⟨ ? ⟩  -- ?1
-?      -- ?2
-∎ )
+  begin
+    ?      -- ?0
+  ≡⟨ ? ⟩    -- ?1
+    ?      -- ?2
+  ∎ )
 
 -- ?0 : Bool
 -- ?1 : stmt2Cond (record { varn = varn env ; vari = 0 }) ≡ true
diff -r d30593612a38 -r 8ef64db63497 paper/src/term1.agda.replaced
--- a/paper/src/term1.agda.replaced	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/src/term1.agda.replaced	Thu Feb 06 19:24:32 2020 +0900
@@ -1,14 +1,14 @@
 stmt2Cond : {c10 :@$\mathbb{N}$@} @$\rightarrow$@ Cond
 stmt2Cond {c10} env = (Equal (varn env) c10) @$\wedge$@ (Equal (vari env) 0)
 
-lemma1 : {c10 :@$\mathbb{N}$@} @$\rightarrow$@ Axiom (stmt1Cond {c10}) (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env ; vari = 0 }) (stmt2Cond {c\
-10})
+lemma1 : {c10 :@$\mathbb{N}$@} @$\rightarrow$@ Axiom (stmt1Cond {c10})
+       (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
 lemma1 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning  in
-begin
-?      -- ?0
-@$\equiv$@@$\langle$@ ? @$\rangle$@  -- ?1
-?      -- ?2
-@$\blacksquare$@ )
+  begin
+    ?      -- ?0
+  @$\equiv$@@$\langle$@ ? @$\rangle$@    -- ?1
+    ?      -- ?2
+  @$\blacksquare$@ )
 
 -- ?0 : Bool
 -- ?1 : stmt2Cond (record { varn = varn env ; vari = 0 }) @$\equiv$@ true