--- a/paper/Makefile	Fri Feb 03 16:34:30 2017 +0900
+++ b/paper/Makefile	Sat Feb 04 12:23:25 2017 +0900
@@ -32,7 +32,7 @@
 .PHONY : clean all open remake
 
 clean:
-	rm -f *.dvi *.aux *.log *.pdf *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol *.bbl *.blg *.idx
+	rm -f *.dvi *.aux *.log *.pdf *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol *.bbl *.blg *.idx src/*.replaced
 
 all: $(TARGET).pdf
 

Binary file paper/atton-master.pdf has changed

--- a/paper/atton-master.tex	Fri Feb 03 16:34:30 2017 +0900
+++ b/paper/atton-master.tex	Sat Feb 04 12:23:25 2017 +0900
@@ -8,6 +8,7 @@
 %    gears and monad
 %    delta monad
 %    副査名修正
+%    csComp の解説
 
 
 \documentclass[a4j,12pt]{jreport}

--- a/paper/cbc-type.tex	Fri Feb 03 16:34:30 2017 +0900
+++ b/paper/cbc-type.tex	Sat Feb 04 12:23:25 2017 +0900
@@ -258,5 +258,115 @@
 
 % }}}
 
+\section{スタックの実装の検証}
+定義した SingleLinkedStack に対して証明を行なっていく。
+ここでの証明は SingleLinkedStack の処理が特定の性質を持つことを保証することである。
 
-\section{スタックの実装の検証}
+例えば
+
+\begin{itemize}
+    \item スタックに積んだ値は取り出せる
+    \item 値は複数積むことができる
+    \item スタックから値を取り出すことができる
+    \item スタックから取り出す値は積んだ値である
+    \item スタックから値を取り出したらその値は無くなる
+    \item スタックに値を積んで取り出すとスタックの内容は変わらない
+\end{itemize}
+
+といった多くの性質がある。
+
+ここでは、最後に示した「スタックに値を積んで取り出すとスタックの内容は変わらない」ことについて示していく。
+この性質を具体的に書き下すと以下のようになる。
+
+\begin{definition}
+    任意のスタック s に対して
+
+    \begin{itemize}
+        \item 任意の値n
+        \item 値xを積む操作 push(x, s)
+        \item 値を一つスタックから取り出す操作 pop(s)
+    \end{itemize}
+
+    がある時、
+
+    pop . push(n) s = s
+
+    である。
+\end{definition}
+
+これを Agda 上で定義するとリスト~\ref{src:agda-push-pop-type-1} のようになる。
+Agda 上の定義ではスタックそのものではなく、スタックを含む任意の \verb/Meta/ に対してこの性質を証明する。
+この定義が \verb/Meta/ の値によらず成り立つことを、自然数の加算の交換法則と同様に等式変形を用いて証明していく。
+
+\lstinputlisting[label=src:agda-push-pop-type-1, caption=Agda におけるスタックの性質の定義(1)] {src/PushPopType.agda.replaced}
+
+今回注目する条件分けは、スタック本体である \verb/stack/ と、push や pop を行なうための値を格納する \verb/element/ である。
+それぞれが持ち得る値を場合分けして考えていく。
+
+\begin{itemize}
+    \item スタックが空である場合
+
+        \begin{itemize}
+            \item element が存在する場合
+
+                値が存在するため、 push は実行される。
+                push が実行されたためスタックに値があるため、pop が成功する。
+                pop が成功した結果スタックは空となるため元のスタックと同一となり成り立つ。
+
+            \item element が存在しない場合
+
+                値が存在しないため、 push が実行されない。
+                push が実行されなかったため、スタックは空のままであり、pop も実行されない。
+                結果スタックは空のままであり、元のスタックと一致する。
+        \end{itemize}
+
+    \item スタックが空でない場合
+
+        \begin{itemize}
+            \item element が存在する場合
+
+                element に設定された値 n が push され、スタックに一つ値が積まれる。
+                スタックの先頭は n であるため、pop が実行されて n は無くなる。
+                結果、スタックは実行する前の状態に戻る。
+
+            \item element が存在しない場合
+
+                element に値が存在しないため、push は実行されない。
+                スタックは空ではないため、popが実行され、先頭の値が無くなる。
+                実行後、スタックは一つ値を失なっているため、これは成りたたない。
+        \end{itemize}
+\end{itemize}
+
+スタックが空でなく、push する値が存在しないときにこの性質は成り立たないことが分かった。
+また、\verb/element/ が空でない制約を仮定に加えることでこの命題は成り立つようになる。
+
+push 操作と pop 操作を連続して行なうとスタックが元に復元されることは分かった。
+ここで SingleLinkedStack よりも範囲を広げて \verb/Meta/ も復元されるかを考える。
+一見これも自明に成り立ちそうだが、push 操作と pop 操作は操作後に実行される CodeSegment を持っている。
+この CodeSegment は任意に設定できるため、\verb/Meta/ 内部の DataSegement が書き換えられる可能性がある。
+よってこれも制約無しでは成り立たない。
+
+逆にいえば、CodeSegment を指定してしまえば \verb/Meta/ に関しても push/pop の影響を受けないことを保証できる。
+全く値を変更しない CodeSegment \verb/id/ を指定した際には自明にこの性質が導ける。
+実際、 Agda 上でも等式変形を明示的に指定せず、定義からの推論でこの証明を導ける(リスト~\ref{src:agda-push-pop-proof})。
+
+なお、今回 SingleLinkedStack に積むことができる値は Agda の標準ライブラリ(\verb/Data.Nat/)における自然数型 $ \mathbb{N} $ としている。
+push/pop 操作の後の継続が \verb/Meta/ に影響を与えない制約は \verb/id-meta/ に表れている。
+これは \verb/Meta/ を構成する要素を受け取り、継続先の CodeSegment に恒等関数 \verb/id/ を指定している。
+加えて、スタックが空で無い制約 where 句の \verb/meta/ に表れている。
+必ずスタックの先頭 \verb/top/ には値xが入っており、それ以降の値は任意としている。
+よってスタックは必ず一つ以上の値を持ち、空でないという制約を表わせる。
+証明は refl によって与えられる。
+つまり定義から自明に推論可能となっている。
+
+\lstinputlisting[label=src:agda-push-pop-proof, caption=Agdaにおけるスタックの性質の証明(1)] {src/AgdaPushPopProof.agda.replaced}
+
+ここで興味深い点は、 SingleLinkedStack の実装から証明に仮定が必要なことが証明途中でに分かった点にある。
+例えば、CbC の SingleLinkedStack 実装の push/pop 操作は失敗しても成功しても指定された CodeSegment に軽量継続する。
+この性質により、指定された CodeSegment によっては、スタックの操作に関係なく \verb/Meta/ の内部の DataSegemnt が書き換えられる可能性があることが分かった。
+スタックの操作の際に行なわれる軽量継続の利用方法は複数考えられる。
+例えば、スタックが空である際に pop を行なった時はエラー処理用の継続を行なう、といった実装も可能である。
+実装が異なれば、同様の性質でも証明は異なるものとなる。
+このように、実装そのものを適切に型システムで定義できれば、明示されていない実装依存の仕様も証明時に確定させることができる。
+
+// n-pop / n-push

--- a/paper/escape_agda.rb	Fri Feb 03 16:34:30 2017 +0900
+++ b/paper/escape_agda.rb	Sat Feb 04 12:23:25 2017 +0900
@@ -13,6 +13,8 @@
   '×' => 'times',
   '⟨'  => 'langle',
   '⟩'  => 'rangle',
+  '₁' => 'text{1}',
+  'ℕ' => 'mathbb{N}',
   '∎'  => 'blacksquare'
 }
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaPushPopProof.agda	Sat Feb 04 12:23:25 2017 +0900
@@ -0,0 +1,11 @@
+id-meta : ℕ -> ℕ -> SingleLinkedStack ℕ -> Meta
+id-meta n e s = record { context = record {n = n ; element = just e}
+                       ; nextCS = (N.cs id) ; stack = s}
+
+push-pop-type : ℕ -> ℕ  -> ℕ -> Element ℕ -> Set₁
+push-pop-type n e x s = M.exec (M.csComp {meta} (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta
+  where
+    meta = id-meta n e record {top = just (cons x (just s))}
+
+push-pop : (n e x : ℕ) -> (s : Element ℕ) ->  push-pop-type n e x s
+push-pop n e x s = refl

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/PushPopType.agda	Sat Feb 04 12:23:25 2017 +0900
@@ -0,0 +1,9 @@
+pushOnce : Meta -> Meta
+pushOnce m = M.exec pushSingleLinkedStackCS m
+
+popOnce : Meta -> Meta
+popOnce m = M.exec popSingleLinkedStackCS m
+
+push-pop-type : Meta -> Set₁
+push-pop-type meta =
+    M.exec (M.csComp  (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta