--- a/Paper/tex/tree_desc.tex	Thu May 05 17:38:06 2022 +0900
+++ b/Paper/tex/tree_desc.tex	Thu May 05 22:32:45 2022 +0900
@@ -1,13 +1,13 @@
 \section{Gears Agda における木構造の設計}
 
-本研究では、Gears Agda にて Red Black Tree の検証を行うにあたり、
-Agda が変数に対して再代入を許していないことが問題になってくる。
+本研究では，Gears Agda にて Red Black Tree の検証を行うにあたり，
+Agda が変数に対して再代入を許していないことが問題になってくる．
 
-そのため下図 \ref{rbt-stack} のように、木構造の root から leaf　に 辿る際に見ているnodeから
-下の　tree をそのまま stack に持つようにする。
+そのため下図 \ref{rbt-stack} のように，木構造の root から leaf　に 辿る際に見ているnodeから
+下の　tree をそのまま stack に持つようにする．
 
-そして insert や delete を行った後に stack から tree を取り出し、
-元の木構造を再構築 していきながら　rootへ戻る。
+そして insert や delete を行った後に stack から tree を取り出し，
+元の木構造を再構築 していきながら　rootへ戻る．
 
 \begin{figure}[H]
   \begin{center}
@@ -18,91 +18,91 @@
 \end{figure}
 
 
-このようにして Gears Agda にて Red Black Tree を実装していく。
+このようにして Gears Agda にて Red Black Tree を実装していく．
 
 \section{Gears Agda における Binary Tree の実装}
 
-Red Black Tree を実装しそれを検証する前段階として、
-実装が簡単な Binary Tree の実装から行う。
+Red Black Tree を実装しそれを検証する前段階として，
+実装が簡単な Binary Tree の実装から行う．
 
-まず Binary Tree と 遷移させる Data Gear となる Env の定義は Code \ref{bt_env} のようになる。
+まず Binary Tree と 遷移させる Data Gear となる Env の定義は Code \ref{bt_env} のようになる．
 
 \lstinputlisting[label=bt_env, caption=Binary Tree の Data Gear] {src/bt_impl/bt_env.agda.replaced}
 
-bt は、木での順序としての意味を持つ key とその中身 value はどのような型でも入れられるように
-「A : Set n」となっている。
-そして left, right には bt A を持つようにし、木構造を構築している。
+bt は，木での順序としての意味を持つ key とその中身 value はどのような型でも入れられるように
+「A : Set n」となっている．
+そして left, right には bt A を持つようにし，木構造を構築している．
 
-Env では、 find, insert, delete の対象となる値を保存し、 Code Gear に与えられるようにするために
-varn, varv を持っている。
-加えて変更を加える bt を持つ vart と、章Nで前述した木構造を持っておくための List である
-varl を Env に設定している。
+Env では， find, insert, delete の対象となる値を保存し， Code Gear に与えられるようにするために
+varn, varv を持っている．
+加えて変更を加える bt を持つ vart と，章Nで前述した木構造を持っておくための List である
+varl を Env に設定している．
 
 7章で述べた Gears Agda での木構造を保ったまま root から目的のnodeまで辿る Code Gear が
-Code \ref{bt_find_impl} になる。
+Code \ref{bt_find_impl} になる．
 
 \lstinputlisting[label=bt_find_impl, caption=root から目的のnodeまで辿る Code Gear] {src/bt_impl/find.agda.replaced}
 
-まず、関数の実装が始まってすぐに Env の vartを指定したものと引数をそのまま find-c の関数に遷移している。
-ここで展開しているのは Env の vart で、そのまま Env から展開した vart をパターンマッチすると
-Agda が追えなくなってしまい、\{-$\#$ TERMINATING $\#$-\} を使用することになってしまう。
+まず，関数の実装が始まってすぐに Env の vartを指定したものと引数をそのまま find-c の関数に遷移している．
+ここで展開しているのは Env の vart で，そのまま Env から展開した vart をパターンマッチすると
+Agda が追えなくなってしまい，\{-$\#$ TERMINATING $\#$-\} を使用することになってしまう．
 
-そのため関数を新たに定義し、展開したものを受け取り、パターンマッチすることで
+そのため関数を新たに定義し，展開したものを受け取り，パターンマッチすることで
 \{-$\#$ TERMINATING $\#$-\} を使用せずに loopを定義できるようになる
 
-木を stack に入れるのは単純で、操作の対象の key となる varn と
-node のkeyを比較を行う。
-そこからは本来の木構造と同じで、操作の対象の key が小さいなら
-left の tree を次の node として遷移する。
-大きいなら right の tree を次の node として遷移していく。
+木を stack に入れるのは単純で，操作の対象の key となる varn と
+node のkeyを比較を行う．
+そこからは本来の木構造と同じで，操作の対象の key が小さいなら
+left の tree を次の node として遷移する．
+大きいなら right の tree を次の node として遷移していく．
 
-操作の対象となる node に辿り着き、操作を行った後、
-Stack に持っている tree から再構築を行う。
+操作の対象となる node に辿り着き，操作を行った後，
+Stack に持っている tree から再構築を行う．
 
 そのコードが Code \ref{bt_replace_impl} となる
 
 \lstinputlisting[label=bt_replace_impl, caption=Stack から tree を再構築する Code Gear] {src/bt_impl/replace.agda.replaced}
 
-これも Code \ref{bt_find_impl} と同じように構成されており、
-varn と node の key を比較し、 vart を List から持ってきた node の どこに加えるかを決めるようになっている。
+これも Code \ref{bt_find_impl} と同じように構成されており，
+varn と node の key を比較し， vart を List から持ってきた node の どこに加えるかを決めるようになっている．
 
-以上の流れを繋げることで、 Binary Tree の insert と find を実装できた。
-delete は insert の値を消すようにすると実装ができる。
+以上の流れを繋げることで， Binary Tree の insert と find を実装できた．
+delete は insert の値を消すようにすると実装ができる．
 
 \section{Gears Agda における Binary Tree の検証}
 
-検証も前述した While Loop の 検証と同じようにしていく。
-しかし、 Binary Tree の不変条件は2つ以上あるため、これを関数定義の際に全て書くと
-煩雑になってしまうため、事前に記述して関数化しておく。
-それが Code \ref{bt_invariant} になる。
+検証も前述した While Loop の 検証と同じようにしていく．
+しかし， Binary Tree の不変条件は2つ以上あるため，これを関数定義の際に全て書くと
+煩雑になってしまうため，事前に記述して関数化しておく．
+それが Code \ref{bt_invariant} になる．
 
 \lstinputlisting[label=bt_invariant, caption=Binary Tree の 不変条件] {src/bt_verif/invariant.agda.replaced}
 
-この不変条件は、 treeInvariant が　tree の 左にある node の key が小さく、
-右にある node の方が大きいことを条件としている。
+この不変条件は， treeInvariant が　tree の 左にある node の key が小さく，
+右にある node の方が大きいことを条件としている．
 
-stackInvariant は Stack にある tree が、次に取り出す Tree の一部であることを
-条件としている。
+stackInvariant は Stack にある tree が，次に取り出す Tree の一部であることを
+条件としている．
 
-これを先ほど実装した Code Gear に対して加えることで検証していく。
-先ほど実装した Code \ref{bt_find_impl} に対して加えると Code ref のようになる。
+これを先ほど実装した Code Gear に対して加えることで検証していく．
+先ほど実装した Code \ref{bt_find_impl} に対して加えると Code ref のようになる．
 
 
 \lstinputlisting[label=bt_invariant, caption=Binary Tree の 不変条件] {src/bt_verif/find.agda.replaced}
 
 現時点では条件を満たしていることの証明まで行っていないが
-コード中の {!!} に記述を行い、前述した While Loop と同じように中身を記述することで検証を行える。
+コード中の {!!} に記述を行い，前述した While Loop と同じように中身を記述することで検証を行える．
 
 \section{まとめと今後の課題}
-本論文では、Gears Agda にて Hoare Logic を用いて While Loop の検証を行えた。
-これはプログラムが Code Gear という単位で分かれているため、
-一つ一つの Code Gear に対して検証を行いながら実装を行っていくことも可能である。
-そのため、従来の検証手法よりもスコープが小さく、簡単に検証と実装を行えると考える。
+本論文では，Gears Agda にて Hoare Logic を用いて While Loop の検証を行えた．
+これはプログラムが Code Gear という単位で分かれているため，
+一つ一つの Code Gear に対して検証を行いながら実装を行っていくことも可能である．
+そのため，従来の検証手法よりもスコープが小さく，簡単に検証と実装を行えると考える．
 
-今後の課題として、Gears Agda による Red Black Tree の実装と検証を行う必要がある。
-While Loop と同じように検証を行えると考えているが、研究目的である
-「ループが存在し、かつ再代入がプログラムに含まれるデータ構造」を
-Gaers Agda を実装することが難しく、それをさらに検証しなければならない。
+今後の課題として，Gears Agda による Red Black Tree の実装と検証を行う必要がある．
+While Loop と同じように検証を行えると考えているが，研究目的である
+「ループが存在し，かつ再代入がプログラムに含まれるデータ構造」を
+Gaers Agda を実装することが難しく，それをさらに検証しなければならない．