--- a/paper/agda.tex	Fri Feb 03 11:59:41 2017 +0900
+++ b/paper/agda.tex	Fri Feb 03 14:49:58 2017 +0900
@@ -9,8 +9,7 @@
 \label{section:natural_deduction}
 まず始めに証明を行なうためにNatural Deduction(自然演繹)を示す。
 
-証明には natural deduction(自然演繹)を用いる。
-natural deduction は Gentzen によって作られた論理と、その証明システムである~\cite{Girard:1989:PT:64805}。
+Natural Deduction は Gentzen によって作られた論理と、その証明システムである~\cite{Girard:1989:PT:64805}。
 命題変数と記号を用いた論理式で論理を記述し、推論規則により変形することで求める論理式を導く。
 
 natural deduction において
@@ -226,8 +225,9 @@
 \ref{section:natural_deduction}節では natural deduction における証明手法について述べた。
 natural deduction における証明はほとんど型付き $ \lambda $ 計算のような形をしている。
 実際、Curry-Howard Isomorphism により Natural Deduction と型付き $ \lambda $ 計算は対応している。% ref TaPL 104
+Curry-Howard Isomorphism の概要を~\ref{section:curry_howard_isomorphism} 節に述べる。
 
-型構築子 $ \rightarrow $ のみに注目した時
+関数型 $ \rightarrow $ のみに注目した時
 
 \begin{enumerate}
     \item 導入規則(T-ABS) は、その型の要素がどのように作られるかを記述する
@@ -272,7 +272,7 @@
             disjunction & $ A \lor B $        & 型 A と型 B の直和型 を持つ変数 x \\ \hline
             implication & $ A \Rightarrow B $ & 型 A を取り型 B の変数を返す関数 f \\ \hline
         \end{tabular}
-        \caption{natural deuction と 型付き $ \lambda $ 計算との対応}
+        \caption{natural deuction と 型付き $ \lambda $ 計算との対応(Curry-Howard Isomorphism)}
         \label{tbl:curry_howard_isomorphism}
     \end{table}
 \end{center}
@@ -284,7 +284,7 @@
 型システムを用いて証明を行なうことができる言語に Agda が存在する。% ref Agda のref
 Agda は依存型という強力な型システムを持っている。
 依存型とは型も第一級オブジェクトとする型であり、型を引数に取る関数や値を取って型を返す関数、型の型などが記述できる。
-この節では Agda の文法的な紹介を行なう~\cite{agda-documentation}。 % ref pdf のアレ
+この節では Agda の文法的な紹介を行なう~\cite{agda-documetation}。 % ref pdf のアレ
 
 まず Agda のプログラムは全てモジュールの内部に記述されるため、まずはトップレベルにモジュールを定義する必要がある。
 トップレベルのモジュールはファイル名と同一となる。
@@ -330,7 +330,7 @@
 
 単純型で利用した自然数もデータ型として定義できる(リスト~\ref{src:agda-nat})。
 自然数のコンストラクタは2つあり、片方は自然数ゼロ、片方は自然数を取って後続数を返すものである。
-例えば3は \verb/suc (suc (suc zero))/ となる。
+例えば0 は \verb/zero/ であり、1 は \verb/suc zero/に、3は \verb/suc (suc (suc zero))/ に対応する。
 
 \lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda}
 
@@ -340,7 +340,7 @@
 この二項演算子は正確には中置関数である。
 前置や後置で定義できる部分を関数名に \verb/_/ として埋め込んでおくことで、関数を呼ぶ時にあたかも前置演算子のように振る舞う。
 また、Agda は関数が停止するかを判定できる。
-この加算の二項演算子は左側がゼロに対しては明かに停止する。
+この加算の二項演算子は左側がゼロに対しては明らかに停止する。
 左側が1以上の時の再帰時には \verb/suc n/ から \verb/n/へと減っているため、再帰で繰り返し減らすことでいつかは停止する。
 
 \lstinputlisting[label=src:agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda}
@@ -356,17 +356,17 @@
 \lstinputlisting[label=src:agda-id, caption=依存型を持つ関数の定義] {src/AgdaId.agda}
 
 この恒等関数 \verb/identitiy/ は任意の型に適用可能である。
-実際に Nat へ適用した例が \verb/id-zero/ である。
+実際に関数 \verb/identitiy/ を Nat へ適用した例が \verb/identitiy-zero/ である。
+
+多相の恒等関数では型を明示的に指定せずとも \verb/zero/ に適用した場合の型は自明に \verb/Nat -> Nat/である。
+Agda はこのような推論をサポートしており、推論可能な引数は省略できる。
+推論によって解決される引数を暗黙的な引数(implicit arguments) と言い、記号 \verb/{}/ でくくる。
 
-依存型を用いることで任意の型に適用可能な多相の恒等関数を定義した。
-しかし型を明示的に指定せずとも \verb/zero/ を渡された場合は恒等関数の型は自明に \verb/Nat -> Nat/である。
-その場合、型を推論することで実際に引数として渡さないようにできる。
-これを暗黙的な引数(implicit arguments) と言い、記号 \verb/{}/ でくくる。
-
-例えば恒等関数の型を暗黙的な引数にするとリスト~\ref{src:agda-implicit-id}のようになる。
-この恒等関数を利用する際は値を渡すだけで型が自動的に推論される。
-よって関数を利用する際は \verb/id-true/ のように記述できる。
-なお、関数の本体で暗黙的な引数を利用したい場合は \verb/{variableName}/ で束縛することもできる。
+例えば、\verb/identitiy/ の対象とする型\verb/A/を暗黙的な引数として省略するとリスト~\ref{src:agda-implicit-id}のようになる。
+この恒等関数を利用する際は特定の型に属する値を渡すだけでその型が自動的に推論される。
+よって関数を利用する際は \verb/id-zero/ のように型を省略して良い。
+なお、関数の本体で暗黙的な引数を利用したい場合は \verb/{variableName}/ で束縛することもできる(\verb/id'/ 関数)。
+適用する場合も \verb/{}/でくくり、\verb/id-true/のように使用する。
 
 \lstinputlisting[label=src:agda-implicit-id, caption=Agdaにおける暗黙的な引数を持つ関数] {src/AgdaImplicitId.agda}
 
@@ -386,8 +386,7 @@
 \lstinputlisting[label=src:agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda}
 
 Agda における部分型のように振る舞う機能として Instance Arguments が存在する。
-とあるデータ型が、ある型と名前を持つ関数を持つことを保証する。
-これは Haskell における型クラスや Java におけるインターフェースに相当する。
+これはとあるデータ型が、ある型と名前を持つ関数を持つことを保証する機能であり、Haskell における型クラスや Java におけるインターフェースに相当する。
 Agda における部分型の制約は、必要な関数を定義した record に相当し、その制約を保証するにはその record を instance として登録することになる。
 例えば、同じ型と比較することができる、という性質を表すとリスト~\ref{src:agda-type-class}のようになる。
 具体的にはとある型 A における中置関数 \verb/_==_/ を定義することに相当する。
@@ -529,31 +528,31 @@
 \begin{itemize}
     \item n = O, m = O
 
-        + の定義により、 O に簡約されるため refl で証明できる。
+        \verb/_+_/ の定義により、 O に簡約されるため refl で証明できる。
 
     \item n = O, m = S m
 
         $ O + (S m) \equiv (S m) + O $  を証明することになる。
-        この等式は + の定義により $ O + (S m) \equiv S (m + O) $ と変形できる。
+        この等式は \verb/_+_/ の定義により $ O + (S m) \equiv S (m + O) $ と変形できる。
         $ S (m + O) $ は $ m + O $ に S を加えたものであるため、 cong を用いて再帰的に \verb/addSym/ を実行することで証明できる。
 
         この2つの証明はこのような意味を持つ。
         n が 0 であるとき、 m も 0 なら簡約により等式が成立する。
         n が 0 であり、 m が 0 でないとき、 m は後続数である。
         よって m が (S x) と書かれる時、 x は m の前の値である。
-        前の値による交換法則を用いてからその結果の後続数も + の定義により等しい。
+        前の値による交換法則を用いてからその結果の後続数も \verb/_+_/ の定義により等しい。
 
         ここで、 \verb/addSym/ に渡される m は1つ値が減っているため、最終的には n = 0, m = 0 である refl にまで簡約され、等式が得られる。
 
     \item n = S n, m = O
 
         $ (S n) + O \equiv O + (S n) $ を証明する。
-        この等式は + の定義により $ S (n + O) \equiv (S n) $ と変形できる。
+        この等式は \verb/_+_/ の定義により $ S (n + O) \equiv (S n) $ と変形できる。
         さらに変形すれば $ S (n + O) \equiv S (O + n) $ となる。
         よって \verb/addSym/ により O と n を変換した後に cong で S を加えることで証明ができる。
 
-        ここで、 $ O + n  \equiv n $ は + の定義により自明であるが、$ n + O \equiv n $ をそのまま導出できないことに注意して欲しい。
-        + の定義は左側の項から S を右側の項への移すだけであるため、右側の項への演算はしない。
+        ここで、 $ O + n  \equiv n $ は \verb/_+_/ の定義により自明であるが、$ n + O \equiv n $ をそのまま導出できないことに注意して欲しい。
+        \verb/_+_/ の定義は左側の項から S を右側の項への移すだけであるため、右側の項への演算はしない。
 
     \item n = S n, m = S m
 
@@ -572,7 +571,7 @@
 
 \lstinputlisting[label=src:agda-reasoning, caption= $ \equiv $ - Reasoning を用いた証明の例] {src/Reasoning.agda.replaced}
 
-まず \verb/ (S n) + (S m)/ は + の定義により \verb/ S (n + (S m)) / に等しい。
+まず \verb/ (S n) + (S m)/ は \verb/_+_/ の定義により \verb/ S (n + (S m)) / に等しい。
 よって refl で導かれる。
 なお、基本的に定義などで同じ項に簡約される時は refl によって記述することが多い。
 
@@ -581,10 +580,11 @@
 このように同じ法則の中でも、違うパターンで証明できた部分を用いて別パターンの証明を行なうこともある。
 
 最後に \verb/S ((S m) + n)/ から \verb/(S m) + (S n)/を得なくてはならない。
-しかし、 + の定義には右辺に対して S を移動する演算が含まれていない。
+しかし、 \verb/_+_/ の定義には右辺に対して S を移動する演算が含まれていない。
 よってこのままでは証明することができない。
 そのため、等式 $ S (m + n) \equiv m + (S n) $ を addToRight として定義する。
-addToRight の証明の解説は省略する。
+addToRight はコンストラクタによる分岐を用いて証明できる。
+値が0であれば自明に成り立ち、1以上であれば再帰的に addToRight を適用することで任意の数に対して成り立つ。
 addToRight を用いることで \verb/S ((S m) + n)/ から \verb/(S m) + (S n)/を得られた。
 これで等式 $ (S m) + (S n) \equiv (S n) + (S m) $  の証明が完了した。
 

Binary file paper/atton-master.pdf has changed

--- a/paper/atton-master.tex	Fri Feb 03 11:59:41 2017 +0900
+++ b/paper/atton-master.tex	Fri Feb 03 14:49:58 2017 +0900
@@ -116,9 +116,9 @@
 %chapters
 \input{introduction.tex}
 
-%\input{cbc.tex}
-%\input{type.tex}
-%\input{agda.tex}
+\input{cbc.tex}
+\input{type.tex}
+\input{agda.tex}
 \input{cbc-type.tex}
 
 \chapter{まとめ}

--- a/paper/cbc-type.tex	Fri Feb 03 11:59:41 2017 +0900
+++ b/paper/cbc-type.tex	Fri Feb 03 14:49:58 2017 +0900
@@ -171,7 +171,10 @@
 
 \lstinputlisting[label=src:agda-mmcs, caption=Agda における Meta Meta CodeSegment の定義と実行例] {src/MetaMetaCodeSegment.agda}
 
-メタの階層構造を表すと図のようになる。
+なお、CbC におけるメタ計算を含む軽量継続\verb/goto meta/とAgda におけるメタ計算実行の比較はリスト~\ref{src:goto-meta}のようになる
+% TODO: cbc と agda の diff
+
+CodeSegment や Meta CodeSegment などの定義が多かっため、どの処理やデータがどのレベルに属するか複雑になったため、一度図にてまとめる。
 Meta DataSegment を含む任意の DataSegment は Meta DataSegment になりえるので、この階層構造は任意の段数定義することが可能である。
 
 
@@ -179,5 +182,27 @@
 
 % }}}
 
-\section{Agda を用いたContinuation based C の検証}
+\section{Agda を用いた Continuation based C の検証}
+Agda において CbC の CodeSegment と DataSegment を定義することができた。
+実際の CbC のコードを Agda に変換し、それらの性質を証明していく。
+
+ここでは赤黒木の実装に用いられているスタックの性質について注目する。
+この時のスタックはポインタを利用した片方向リストを用いる。
+
+CbC における構造体 \verb/stack/ の定義はリスト~\ref{src:cbc-stack}のようになっている。
+
+\lstinputlisting[label=src:cbc-stack, caption=CbC における構造体 stack の定義] {src/stack.h}
+
+Agda にはポインタが無いため、メモリ確保や\verb/NULL/の定義は存在しない。
+CbC におけるメモリ確保部分はノーマルレベルには出現しないと仮定して、\verb/NULL/の表現にはAgda の標準ライブラリに存在する \verb/Data.Maybe/ を用いる。
+
+\verb/Data.Maybe/ の \verb/maybe/ 型は、コンストラクタを二つ持つ。
+片方のコンストラクタ \verb/just/ は値を持つ。
+これは計算を行なうことができる値であり、ポインタの先に値があることに対応している。
+一方のコンストラツア \verb/nothing/ は値を持たない。
+これは値が存在せず、ポインタの先が確保されていない(\verb/NULL/ ポインタである)ことを表現できる。
+
+\lstinputlisting[label=src:agda-maybe, caption=Agda における Maybe の定義] {src/Maybe.agda.replaced}
+
+
 \section{スタックの実装の検証}

--- a/paper/src/AgdaId.agda	Fri Feb 03 11:59:41 2017 +0900
+++ b/paper/src/AgdaId.agda	Fri Feb 03 14:49:58 2017 +0900
@@ -1,5 +1,5 @@
 identity : (A : Set) -> A -> A
 identity A x = x
 
-id-zero : Nat
-id-zero = identity Nat zero
+identity-zero : Nat
+identity-zero = identity Nat zero

--- a/paper/src/AgdaImplicitId.agda	Fri Feb 03 11:59:41 2017 +0900
+++ b/paper/src/AgdaImplicitId.agda	Fri Feb 03 14:49:58 2017 +0900
@@ -1,5 +1,11 @@
 id : {A : Set} -> A -> A
 id x = x
 
+id-zero : Nat
+id-zero = id zero
+
+id' : {A : Set} -> A -> A
+id' {A} x = x
+
 id-true : Bool
-id-true = id true
+id-true = id {Bool} true

--- a/paper/src/AgdaRecordProj.agda	Fri Feb 03 11:59:41 2017 +0900
+++ b/paper/src/AgdaRecordProj.agda	Fri Feb 03 14:49:58 2017 +0900
@@ -1,5 +1,5 @@
 getX : Point -> Nat
-getX p = Point.get p
+getX p = Point.x p
 
 getY : Point -> Nat
 getY record { x = a ; y = b} = b

--- a/paper/src/NatAddSym.agda	Fri Feb 03 11:59:41 2017 +0900
+++ b/paper/src/NatAddSym.agda	Fri Feb 03 14:49:58 2017 +0900
@@ -8,7 +8,5 @@
 addSym : (n m : Nat) -> n + m ≡ m + n
 addSym O       O   = refl
 addSym O    (S m)  = cong S (addSym O m)
-addSym (S n)   O   = cong S (addSym n O)
-addSym (S n) (S m) = {!!}
-
-
+addSym (S n)   O   = cong S (addSym n O) 
+addSym (S n) (S m) = {!!} -- 後述