--- a/Paper/Makefile	Wed Feb 01 20:27:04 2023 +0900
+++ b/Paper/Makefile	Wed Feb 01 22:16:45 2023 +0900
@@ -36,7 +36,7 @@
 	open $(TARGET).pdf
 
 clean:
-	rm -f *.dvi *.aux *.log *.ilg *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol *.bbl *.blg *.idx src/**/*.replaced *.fdb_latexmk *.fls
+	rm -f *.dvi *.aux *.log *.ilg *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol *.bbl *.blg *.idx ./**/*.replaced *.fdb_latexmk *.fls
 
 remake:
 	make clean

Binary file Paper/fig/dpp-model.jpg has changed

--- a/Paper/info.toml	Wed Feb 01 20:27:04 2023 +0900
+++ b/Paper/info.toml	Wed Feb 01 22:16:45 2023 +0900
@@ -5,11 +5,11 @@
 title_en = "the neural pulse signals of memories stored in the temporal lobe and the theory of turning analog memories into digital patterns"
 
 abstract = """
-人間の記憶は大脳皮質の側頭葉に記録される。
-その記憶の書き込みや読み込みをする部位が側頭葉の海馬傍回である。
-脳は電気信号の伝達により働いており、実は記憶も電気信号の伝わりの一つである。
-その働きを制御しているのも海馬傍回である。つまり、電気信号が海馬傍回を出入することで記憶が作られる。
-そこで、海馬傍回を出入りする電気信号のパターンが、大脳皮質のどの記憶と対応しているか解析を行い、記憶を電気信号のパターンの組み合わせとして理論立てた。
+人間の記憶は大脳皮質の側頭葉に記録される.
+その記憶の書き込みや読み込みをする部位が側頭葉の海馬傍回である.
+脳は電気信号の伝達により働いており,実は記憶も電気信号の伝わりの一つである.
+その働きを制御しているのも海馬傍回である.つまり,電気信号が海馬傍回を出入することで記憶が作られる.
+そこで,海馬傍回を出入りする電気信号のパターンが,大脳皮質のどの記憶と対応しているか解析を行い,記憶を電気信号のパターンの組み合わせとして理論立てた.
 """
 
 abstract_en = """

Binary file Paper/master_paper.pdf has changed

--- a/Paper/master_paper.sty	Wed Feb 01 20:27:04 2023 +0900
+++ b/Paper/master_paper.sty	Wed Feb 01 22:16:45 2023 +0900
@@ -41,8 +41,8 @@
 %
 %%第一章
 %\input{chapter1.tex}
-%%chapter1.texの\chapter{}の後ろに次のコマンドを追加してください。
-%%ページカウントがリセットされ、ページ数がアラビア文字になります。
+%%chapter1.texの\chapter{}の後ろに次のコマンドを追加してください.
+%%ページカウントがリセットされ,ページ数がアラビア文字になります.
 %%  \pagenumbering{arabic}
 %%第二章
 %\input{chapter2.tex}
@@ -197,7 +197,7 @@
   氏\hspace{4ex}名: 上地 悠斗
   \vspace*{4.5cm}
   \begin{center}
-    本論文は、修士(工学)の学位論文として適切であると認める。
+    本論文は,修士(工学)の学位論文として適切であると認める.
   \end{center}
   \vskip 10 em
   \begin{minipage}{0.5\hsize}
@@ -367,7 +367,7 @@
 % ヘディング
 % c.f. 奥村晴彦,''LaTeX2e 美文書作成入門,'' 技術評論社, pp207--231, 1997.
 
-%ヘッダ、フッタに追加するもの
+%ヘッダ,フッタに追加するもの
 \def\@lefthead{}
 \def\marklefthead#1{\gdef\@lefthead{\small #1}}
 \def\@leftfoot{}
@@ -485,7 +485,7 @@
 % \prebreakpenalty\jis`．=10000 % ．
 %\prebreakpenalty\jis"2124=10000 % ，
 %\prebreakpenalty\jis"2125=10000 % ．
-%\prebreakpenalty\jis`、=10000 % 、
-%\prebreakpenalty\jis`。=10000 % 。
-%%\prebreakpenalty\jis"2124=10000 % 、
-%%\prebreakpenalty\jis"2125=10000 % 。
+%\prebreakpenalty\jis`,=10000 % ,
+%\prebreakpenalty\jis`.=10000 % .
+%%\prebreakpenalty\jis"2124=10000 % ,
+%%\prebreakpenalty\jis"2125=10000 % .

--- a/Paper/master_paper.tex	Wed Feb 01 20:27:04 2023 +0900
+++ b/Paper/master_paper.tex	Wed Feb 01 22:16:45 2023 +0900
@@ -119,11 +119,6 @@
 \input{tex/agda.tex}
 \input{tex/cbc_agda.tex}
 
-\chapter{Gears Agda による定理証明}
-先行研究では、Hoare Logic を 使用して while loop の検証を行っていた。
-本研究では、invariant というプログラムの不変条件を定義し、それを検証することで、比較的容易に検証を行うことができるようになった(本章2節)
-本章では Gears Agda による定理証明の方法について説明する。
-
 \input{tex/hoare.tex}
 \input{tex/while_loop.tex} % while loop の実装と検証(簡単に)
 \input{tex/tree_desc.tex}% Gears Agda における木構造の設計
@@ -132,26 +127,26 @@
 \input{tex/dpp_impl.tex}% Gears Agda の記法　loopのやつやる
 
 \chapter{まとめと今後の展望}
-本論文では Gears Agda による形式手法を用いたプログラムの検証について述べた。そこで、定理証明については Invariant を用いて定理証明を行った。モデル検査については Gears Agda にて dead lock を検知できるようになった。
+本論文では Gears Agda による形式手法を用いたプログラムの検証について述べた.そこで,定理証明については Invariant を用いて定理証明を行った.モデル検査については Gears Agda にて dead lock を検知できるようになった.
 
-実際に Invariant を用いることで、プログラムに与える入力とその出力に対して条件を与え、Hoare Logic による検証を行えるようになった。
-これにより、いままでより容易に Gears Agda にて検証が進められるようになった。
+実際に Invariant を用いることで,プログラムに与える入力とその出力に対して条件を与え,Hoare Logic による検証を行えるようになった.
+これにより,いままでより容易に Gears Agda にて検証が進められるようになった.
 
-また、先行研究での課題にて、CbCで開発、検証を行いたいと考えている Gears OSの並列並列動作の検証があった。これもモデル検査により、Gears Agda 内で並列動作に対する検証も行えるようになった。
+また,先行研究での課題にて,CbCで開発,検証を行いたいと考えている Gears OS\cite{mitsuki-prosym}の並列並列動作の検証があった.これもモデル検査により,Gears Agda 内で並列動作に対する検証も行えるようになった.
 
 
 \section{今後の課題}
-今後の課題としてモデル検査による検証、定理証明による検証、Gears Agda の今後の展望について述べる。
-モデル検査においては、有効オートマトンによるプログラムの遷移を全自動探索することと、live lockやアサーションの検証を行いたい。
-加えて、State List のデータ構造を brunced tree にすることで、並列にモデル検査が行えるようになると考えられる。
-これにより、状態が膨大になるモデル検査に対応できる。
+今後の課題としてモデル検査による検証,定理証明による検証,Gears Agda の今後の展望について述べる.
+モデル検査においては,有向グラフからなる有限オートマトンの遷移を全自動探索することと,live lockやLTTLも用いたアサーションなどの検証\cite{model}を行いたい.
+加えて,State List のデータ構造を brunced tree にすることで,並列にモデル検査が行えるようになると考えられる.
+これにより,状態が膨大になるモデル検査に対応できる.
 
-定理証明においては、Red Black Tree の検証を行いたいと思っている。
-これで検証を行ったものをモデル検査や Gears OS のファイルシステムなどに転用できると考えている。
+定理証明においては,Red Black Tree の検証を行いたいと思っている.
+これで検証を行ったものをモデル検査や Gears OS のファイルシステムなどに転用できると考えている.
 
-Gears Agda の展望について、CbC に変換することが挙げられる。
-CbC はアセンブラに近いため記述が複雑かつ困難であるが、Gears Agda で記述したものを CbC に変換できるようになれば、その点を解決できる。更に、Gears Agda で検証を行ったプログラムであるため、プログラムの信頼性もある。
-加えて、モデル検査の実行には速度が求められるが、CbCで高速に実行できるようになることが期待される。
+Gears Agda の展望について,CbC に変換することが挙げられる.
+CbC はアセンブラに近いため記述が複雑かつ困難であるが,Gears Agda で記述したものを CbC に変換できるようになれば,その点を解決できる.更に,Gears Agda で検証を行ったプログラムであるため,プログラムの信頼性もある.
+加えて,モデル検査の実行には速度が求められるが,CbCで高速に実行できるようになることが期待される.
 
 % %謝辞
 \input{tex/thanks.tex}

--- a/Paper/reference.bib	Wed Feb 01 20:27:04 2023 +0900
+++ b/Paper/reference.bib	Wed Feb 01 22:16:45 2023 +0900
@@ -86,12 +86,6 @@
     note = {Accessed: 2020/2/9(Sun)},
 }
 
-@misc{coq,
-    title = {Coq Source},
-    howpublished = {\url{https://github.com/coq/coq}},
-    note = {Accessed: 2020/2/9(Sun)},
-}
-
 @misc{cr-ryukyu,
     title = {Hoare Logic - 並列信頼研 mercurial repository},
     howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/}},
@@ -147,13 +141,6 @@
   publisher={共立出版}
 }
 
-@misc{article-intro,
-  title={記号論理入門},
-  author={金子洋之},
-  year={1994},
-  publisher={東京: 産業図書}
-}
-
 @misc{model,
   title={コンピュータ基礎理論ハンドブック 形式的モデルと意味論},
   author={広瀬健},

--- a/Paper/src/dpp-verif/ModelChecking.agda	Wed Feb 01 20:27:04 2023 +0900
+++ b/Paper/src/dpp-verif/ModelChecking.agda	Wed Feb 01 22:16:45 2023 +0900
@@ -126,7 +126,7 @@
     bit-force-search zero f l env envl exit = exit envl
     bit-force-search (suc redu) f [] env envl exit = exit envl
     bit-force-search (suc redu) f (true ∷ bs) env envl exit = bit-force-search (suc redu) (f ++ (false ∷ [])) bs env envl exit -- 今回の対象をfalseにしてfに追加,bを次の対象にする
-    bit-force-search (suc redu) f (false ∷ bs) env envl exit = set-state redu (f ++ (true ∷ bs)) (f ++ (true ∷ bs)) [] (ph env) env envl exit where -- 今回の対象をtrueにし、fとbを結合してそのListを代入する。かつそれをbに入れfをinitしてloopさせる
+    bit-force-search (suc redu) f (false ∷ bs) env envl exit = set-state redu (f ++ (true ∷ bs)) (f ++ (true ∷ bs)) [] (ph env) env envl exit where -- 今回の対象をtrueにし,fとbを結合してそのListを代入する.かつそれをbに入れfをinitしてloopさせる
       set-state : {n : Level} {t : Set n} → ℕ → (origin state : List Bool ) → (f b : List Phi) → Env → (List Env) → (exit : List Env → t) → t -- 入れ替える必要のあるやつはphaseがThinkingのやつのみ
       set-state redu origin [] f b env envl exit = bit-force-search redu [] origin env (record env{ph = (f ++ b)} ∷ envl) exit -- Stateが先に尽きる
       set-state redu origin state@(s ∷ ss) f b env envl exit with b
@@ -835,8 +835,8 @@
 -- いきなりsearchしないで実行結果を持つ感じに
 -- stubを使うとCodeの引数がスマートになるのでやる
 
--- 実行結果をListでもっているので、stepをじっこうしても変化がなかった場合をdeadlockとして検出したい
--- 東恩納先輩とおなじように、waitに入れて評価する
+-- 実行結果をListでもっているので,stepをじっこうしても変化がなかった場合をdeadlockとして検出したい
+-- 東恩納先輩とおなじように,waitに入れて評価する
 
 -- 余裕があったらassertにLTLの話をいれる
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/dpp-verif/dpp-metacode.agda	Wed Feb 01 22:16:45 2023 +0900
@@ -0,0 +1,7 @@
+check-deadlock-metaenv : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
+check-deadlock-metaenv meta2 exit = search-brute-force-envll-p [] (metal meta2) (λ e → exit record meta2{metal = e}) where
+  search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t
+  search-brute-force-envll-p f [] exit = exit f
+  search-brute-force-envll-p f b@(metaenv ∷ bs) exit with DG metaenv
+  ... | [] = search-brute-force-envll-p f bs exit
+  ... | (env ∷ envs) =  brute-force-search env (λ e0 → search-brute-force-envll-p (f ++ ( record metaenv{meta = record (meta metaenv){num-branch = (length e0)} } ∷ [])) bs exit )
\ No newline at end of file

--- a/Paper/tex/abst.tex	Wed Feb 01 20:27:04 2023 +0900
+++ b/Paper/tex/abst.tex	Wed Feb 01 22:16:45 2023 +0900
@@ -6,7 +6,7 @@
 
 形式手法で開発したプログラムは数学的に正しいことが証明されている，
 そのため高い安全性が必要とされる鉄道や電力などのインフラ分野に使用されている．
-しかし、一見完璧な手法であるように思えるが欠点として，膨大なコストを要する．
+しかし,一見完璧な手法であるように思えるが欠点として，膨大なコストを要する．
 シンプルな実装であれば仕様の形式化が容易に行えるが，そうであれば形式手法を使用せずとも良いとなる．
 
 そのため，他のプログラミング言語と比べて検証に適しているGears Agdaを使用する．
@@ -14,13 +14,13 @@
 取り入れた記法で記述された Agdaのことである．
 
 定理証明によるプログラムの検証は一般的に難易度が高いが，
-Gears Agda では検証をプログラム単位に分割することができ，比較的容易に検証を行えるようになっている．\cite{ryokka-sigos}
+Gears Agda では検証をプログラム単位に分割することができ，比較的容易に検証を行えるようになっている．
 
-先行研究では implies を用いて Hoare Logic での定理証明を行っていた。
-しかしそれでは記述が長く、かつ複雑になってしまっていた。
-そこで今回は Invariant というプログラムの不変条件を新たに取り入れた。これを検証しながら実行を行うことで、Hoare Logic を用いた定理証明を比較的簡単に行えるようになった。
+先行研究では implies を用いて Hoare Logic での定理証明を行っていた.
+しかしそれでは記述が長く,かつ複雑になってしまっていた.
+そこで今回は Invariant というプログラムの不変条件を新たに取り入れた.これを検証しながら実行を行うことで,Hoare Logic を用いた定理証明を比較的簡単に行えるようになった.
 
-また，定理証明では並行処理の検証は困難である。
+また，定理証明では並行処理の検証は困難である.
 そのため，もう一つの代表的な検証手法であるモデル検査を Gears Agda にて行えるようにした．
 
 これらのことから，本論文では Gears Agda の定理証明とモデル検査での検証手法について述べる
@@ -41,7 +41,7 @@
 Gears Agda is an Agda written in a notation that incorporates the concept of Continuation based C (CbC), which is being developed in our laboratory.
 
 Verification of programs by theorem proving is generally difficult.
-Gears Agda can be divided into program units, making verification relatively easy. \cite{ryokka-sigos}
+Gears Agda can be divided into program units, making verification relatively easy.
 
 In previous research, implies were used for theorem proving in Hoare Logic.
 However, this made the description long and complicated.

--- a/Paper/tex/agda.tex	Wed Feb 01 20:27:04 2023 +0900
+++ b/Paper/tex/agda.tex	Wed Feb 01 22:16:45 2023 +0900
@@ -2,7 +2,10 @@
 Agda \cite{agda-wiki} \cite{Stump:2016:VFP:2841316} は純粋関数型言語である．
 Agda は依存型という型システムを持ち，型を第一級オブジェクトとして扱う．
 
-本章ではAgdaの基本とAgdaによる定理証明の方法について述べる。
+また,もともとの Agda には自然数などの定義すら存在しない.
+その実装ができることも本章で取り扱っているが,一般的には standard-libralies \cite{agda-stdlib} を使用する.
+
+本章ではAgdaの基本とAgdaによる定理証明の方法について述べる.
 
 \section{Agdaの基本}
 Agda の記述ではインデントが意味を持ち，スペースの有無もチェックされる．

--- a/Paper/tex/cbc.tex	Wed Feb 01 20:27:04 2023 +0900
+++ b/Paper/tex/cbc.tex	Wed Feb 01 22:16:45 2023 +0900
@@ -13,53 +13,53 @@
 したがって，Code Gear に Deta Gear を与え，それをもとに処理を行い，
 出力として Data Gear を返し，また次の Code Gearに遷移していく流れとなる．
 
-本章ではCbCの概要について説明する。
+本章ではCbCの概要について説明する.
 
 \section{Code Gear / Data Gear}
-CbCでは、検証しやすいプログラムの単位として DataGear と CodeGear という単位を用いる。
+CbCでは,検証しやすいプログラムの単位として DataGear と CodeGear という単位を用いる.
 
-CodeGear はプログラムの処理そのものであり、一般的なプログラム言語における関数と同じ役割である。
-DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータである。
-CodeGear の入力となる DataGear を Input DataGear と呼び、出力は Output DataGear と呼ぶ。
+CodeGear はプログラムの処理そのものであり,一般的なプログラム言語における関数と同じ役割である.
+DataGear は CodeGear で扱うデータの単位であり,処理に必要なデータである.
+CodeGear の入力となる DataGear を Input DataGear と呼び,出力は Output DataGear と呼ぶ.
 
-CodeGear 間の移動は継続を用いて行われる。
-継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻れず、次の CodeGear へ継続を行う。
-これは、関数型プログラミングでは末尾再帰をしていることと同義である。
+CodeGear 間の移動は継続を用いて行われる.
+継続は関数呼び出しとは異なり,呼び出した後に元のコードに戻れず,次の CodeGear へ継続を行う.
+これは,関数型プログラミングでは末尾再帰をしていることと同義である.
 
 
 \section{CbC と C言語の違い}
-同じ仕様でCbCとC言語で実装した際の違いを、実際のコードを元に比較する。
-比較するにあたり、再起処理が含まれるコードの例として、
-フィボナッチ数列の n 番目を求めるコードを挙げる。
-C言語で記述したものが\coderef{fib_c}。CbCで記述したものが\coderef{fib_cbc}になる。
-CbCは実行を継続するため、 return を行えない。そのためC言語での実装も return を書
-かず関数呼び出しを行い、最後にexitをして実行終了するように記述している。
+同じ仕様でCbCとC言語で実装した際の違いを,実際のコードを元に比較する.
+比較するにあたり,再起処理が含まれるコードの例として,
+フィボナッチ数列の n 番目を求めるコードを挙げる.
+C言語で記述したものが\coderef{fib_c}.CbCで記述したものが\coderef{fib_cbc}になる.
+CbCは実行を継続するため, return を行えない.そのためC言語での実装も return を書
+かず関数呼び出しを行い,最後にexitをして実行終了するように記述している.
 
 \lstinputlisting[label=code:fib_c, caption=C言語で記述した フィボナッチ数列の n 番目
 を求めるコード, firstline=5] {src/cbc/fib.c}
 \lstinputlisting[label=code:fib_cbc, caption=CbCで記述した フィボナッチ数列の n 番目
 を求めるコード, firstline=5] {src/cbc/fib.cbc}
 
-軽量実装になっているのか、上記のコードをアセンブラ変換した結果を見て確認する。
-全てを記載すると長くなるので、アセンブラ変換した際のfib関数のみを記載する。
-C言語で記述した\coderef{fib_c}をアセンブラ変換した結果が\coderef{c-ass}。
-CbCで記述した\coderef{fib_cbc}をアセンブラ変換した結果が\coderef{cbc-ass}になる。
+軽量実装になっているのか,上記のコードをアセンブラ変換した結果を見て確認する.
+全てを記載すると長くなるので,アセンブラ変換した際のfib関数のみを記載する.
+C言語で記述した\coderef{fib_c}をアセンブラ変換した結果が\coderef{c-ass}.
+CbCで記述した\coderef{fib_cbc}をアセンブラ変換した結果が\coderef{cbc-ass}になる.
 
-比較すると、fib 関数の内部で再度 fib 関数を呼び出す際、
-C言語で実装した\coderef{c-ass}の30行目では callq で fib 関数を呼び出している。
-対して CbC で実装した\coderef{cbc-ass}の32行目では、 jmp により fib 関数に移動
-している。
+比較すると,fib 関数の内部で再度 fib 関数を呼び出す際,
+C言語で実装した\coderef{c-ass}の30行目では callq で fib 関数を呼び出している.
+対して CbC で実装した\coderef{cbc-ass}の32行目では, jmp により fib 関数に移動
+している.
 
 \lstinputlisting[label=code:c-ass, caption=cで記述した際の fib 関数のアセンブラ] {src/cbc/c.txt}
 \lstinputlisting[label=code:cbc-ass, caption=cbcで記述した際の fib 関数のアセンブラ] {src/cbc/cbc.txt}
 
-以上のことから CbCが軽量継続を行っていると言える。
+以上のことから CbCが軽量継続を行っていると言える.
 
 
 \section{Meta Code Gear / Meta Data Gear}
-Meta DataGear は CbC 上のメタ計算で扱われる DataGear である。例えば stub
-CodeGear では Context と呼ばれる接続可能な CodeGear、DataGear のリストや、DataGear
-のメモリ空間等を持った Meta DataGear を扱っている。
+Meta DataGear は CbC 上のメタ計算で扱われる DataGear である.例えば stub
+CodeGear では Context と呼ばれる接続可能な CodeGear,DataGear のリストや,DataGear
+のメモリ空間等を持った Meta DataGear を扱っている.
 
 また，プログラムを記述する際は，ノーマルレベルの計算の他に，メモリ管理，スレッド管理，資源管理等を記述しなければならない処理が存在する．
 これらの計算はノーマルレベルの計算と区別してメタ計算と呼ぶ．

--- a/Paper/tex/conclusion.tex	Wed Feb 01 20:27:04 2023 +0900
+++ b/Paper/tex/conclusion.tex	Wed Feb 01 22:16:45 2023 +0900
@@ -1,10 +1,10 @@
 \section{まとめ}
-本稿では、Gears Agda を用いてAI研究への適応方法について述べた。
-手法として、Gears Agda によりプログラムの内部にアルゴリズムを使用したコードで
-置き換えられる部分が存在するかをモデル検査で探索する。
-これをニューラルネットワークの中間層の最適化に使用する。
-したがって、中間層を別の少ないレイヤーで置き換えられないかを探索する。
-加えて、考慮するレイヤーの中に新規で計算式を加えることで新しいレイヤーを
-開発できるのではないかとも考えている。
+本稿では,Gears Agda を用いてAI研究への適応方法について述べた.
+手法として,Gears Agda によりプログラムの内部にアルゴリズムを使用したコードで
+置き換えられる部分が存在するかをモデル検査で探索する.
+これをニューラルネットワークの中間層の最適化に使用する.
+したがって,中間層を別の少ないレイヤーで置き換えられないかを探索する.
+加えて,考慮するレイヤーの中に新規で計算式を加えることで新しいレイヤーを
+開発できるのではないかとも考えている.
 
 

--- a/Paper/tex/dpp_impl.tex	Wed Feb 01 20:27:04 2023 +0900
+++ b/Paper/tex/dpp_impl.tex	Wed Feb 01 22:16:45 2023 +0900
@@ -1,24 +1,24 @@
 \section{Gears Agdaによるモデル検査の流れ}
-今回作成した Gears Agda による DPP のモデル検査の流れは以下のようになっている。
+今回作成した Gears Agda による DPP のモデル検査の流れは以下のようになっている.
 
 - Gears Agda にてモデル検査を実装を行う
-  - step実行を行う Code Gear や、場合によっては分岐を行うCode Gearが必要になる
+  - step実行を行う Code Gear や,場合によっては分岐を行うCode Gearが必要になる
 
-- プログラムが実行中に取りうる状態の網羅をする State List を作成する。
+- プログラムが実行中に取りうる状態の網羅をする State List を作成する.
 
-- 上で実装したものを使用しつつ、meta データである プロセスが実行するための wait list を定義する Meta Data Gear や分岐の数を保存する Meta Data Gear を定義する。
+- 上で実装したものを使用しつつ,meta データである プロセスが実行するための wait list を定義する Meta Data Gear や分岐の数を保存する Meta Data Gear を定義する.
 
-- 上記 Meta Code Gear で作成された meta data を元に、dead lockを判定する Meta Code Gear を記述する
+- 上記 Meta Code Gear で作成された meta data を元に,dead lockを判定する Meta Code Gear を記述する
 
 
-- 状態を網羅した State List にある State を一つづつ Meta Code Gear に実行させて、dead lockしている状態がないか確認する
+- 状態を網羅した State List にある State を一つずつ Meta Code Gear に実行させて,dead lockしている状態がないか確認する
 
-先行研究では網羅した状態データを State DB に格納していた。しかし今回の Gears Agda では State List にて代替とした。これは List で行った方が Agda での実装がしやすい点にある。本来は branced tree をデータ構造に持って State を作成するほう正しい。
+先行研究では網羅した状態データを State DB に格納していた.しかし今回の Gears Agda では State List にて代替とした.これは List で行った方が Agda での実装がしやすい点にある.本来は branced tree をデータ構造に持って State を作成するほう正しい.
 
-dead lock の定義として、全てのプロセスが他のプロセスの実行終了待ちをしている。かつ新たに状態の分岐が作成できないものとした。
-そこでstep実行してもプロセスがすべて変動がなく、かつStateの分岐が作成されなかったものを dead lock としている。
+dead lock の定義として,全てのプロセスが他のプロセスの実行終了待ちをしている.かつ新たに状態の分岐が作成できないものとした.
+そこでstep実行してもプロセスがすべて変動がなく,かつStateの分岐が作成されなかったものを dead lock としている.
 
-最後について、今回は状態の網羅を一度終了してから dead lock の有無を検証している。しかし、これは今回のプログラムが有限オートマトンであることは事前に明らかであるためにできたことである。検証したいプログラムが無限の状態を作成する場合は、Stateを作成するたびにそれに対して dead lock や live lock などのモデル検査をすることもできる。モデル検査中に意図しない動きがあった場合に停止するようにすることで、無限の状態を作成するプログラムであっても、モデル検査ができると考える。他にも、プログラムが取る状態を制限することで有限な状態を作成するようにし、モデル検査をすることもできる。 (bounded model checking)
+最後について,今回は状態の網羅を一度終了してから dead lock の有無を検証している.しかし,これは今回のプログラムが有限オートマトンであることは事前に明らかであるためにできたことである.検証したいプログラムが無限の状態を作成する場合は,Stateを作成するたびにそれに対して dead lock や live lock などのモデル検査をすることもできる.モデル検査中に意図しない動きがあった場合に停止するようにすることで,無限の状態を作成するプログラムであっても,モデル検査ができると考える.他にも,プログラムが取る状態を制限することで有限な状態を作成するようにし,モデル検査をすることもできる. (bounded model checking)
 
 \section{Gears Agda によるDPPの実装}
 
@@ -55,15 +55,15 @@
 \lstinputlisting[caption= Gears Agdaでの DPP の Data Gear のinit, label=agda-dpp-init, firstline=23, lastline=30]{src/agda-dpp-impl.agda.replaced}
 
 Code \ref{agda-dpp-init}が入力から Data Gear を作成する Code Gear になる．
-ここでは哲学者の人数を自然数で受け取り，人数分の List Phi と table を一つづつ作成し env を作成している．
+ここでは哲学者の人数を自然数で受け取り，人数分の List Phi と table を一つずつ作成し env を作成している．
 また，最初の哲学者の状態は思考することであるため，next-code には C\_thinking を格納している．
 
 \lstinputlisting[caption= Gears Agdaでの DPP の step 実行, label=agda-dpp-step, firstline=31, lastline=37]{src/agda-dpp-impl.agda.replaced}
 
-Agda では並列実行を行うことができない．そのため step 単位の実行を一つづつ行うことで
+Agda では並列実行を行うことができない．そのため step 単位の実行を一つずつ行うことで
 並列実行をしていることとする．
 
-この際に Env にある List Phi の中身を展開しながら一つづつ行動を処理していく．
+この際に Env にある List Phi の中身を展開しながら一つずつ行動を処理していく．
 
 \lstinputlisting[caption=Gears Agdaでの DPP の左のフォークを取る記述, label=agda-dpp-lfork, firstline=39]{src/agda-dpp-impl.agda.replaced}
 
@@ -89,27 +89,27 @@
 
 \section{Gears Agda によるDPPの検証}
 
-これまでの実装は一般的なDPPの実装であったため、
-Code / Data Gear の実装であった。
-ここからは、モデル検査を行うため、Meta Data Gear の定義をし、
-それの操作を行う Meta Code Gear の実装を行っていく。
+これまでの実装は一般的なDPPの実装であったため,
+Code / Data Gear の実装であった.
+ここからは,モデル検査を行うため,Meta Data Gear の定義をし,
+それの操作を行う Meta Code Gear の実装を行っていく.
 
 以下\coderef{dpp-mdg}がMeta Code Gear の定義になる
 
 % ここにmetadata MetaEnv MetaEnv2のソースコードを貼り付ける
 \lstinputlisting[caption=Gears Agdaでの DPP モデル検査を行うための Meta Data Gear の定義, label=code:dpp-mdg]{src/dpp-verif/dpp-metadata.agda.replaced}
 
-この Meta Data Gear の説明をすると、
-metadataは状態の分岐数を持っておくnum-brunchがある。
+この Meta Data Gear の説明をすると,
+metadataは状態の分岐数を持っておくnum-brunchがある.
 MetaEnv はもとの DataGear を保持するDG(Data Gearの省略)
-meta に 前述したmetadataを持っており、
-他には、deadlockしているかのフラグである deadlock 、
-最後の2つは後述する際に必要になる。
-そのstate が step 実行済みなのかのフラグであるis-step、
-そのstateがモデル検査済なのかのフラグであるis-doneフラグを持っている。
+meta に 前述したmetadataを持っており,
+他には,deadlockしているかのフラグである deadlock ,
+最後の2つは後述する際に必要になる.
+そのstate が step 実行済みなのかのフラグであるis-step,
+そのstateがモデル検査済なのかのフラグであるis-doneフラグを持っている.
 
-MetaEnv2 は1つのstate である MetaEnv の Listを meta で持てる。
-加えて今まで実行していた Data Gear  を DG で持てる。
+MetaEnv2 は1つのstate である MetaEnv の Listを meta で持てる.
+加えて今まで実行していた Data Gear  を DG で持てる.
 
 次に Meta Data Gear を作成する Meta Code Gear の説明をすると
 
@@ -123,85 +123,85 @@
 \lstinputlisting[caption=状態の分岐数をカウントする Meta Data Gear の定義, label=code:dpp-mcg-branch]{src/dpp-verif/dpp-metacode.agda.replaced}
 
 
-実際にやっていることは、MetaEnv2 から state を取り出し、分岐を見る関数に遷移させている。その結果の List の length を meta データとしている。
+実際にやっていることは,MetaEnv2 から state を取り出し,分岐を見る関数に遷移させている.その結果の List の length を meta データとしている.
 
-つまり、この Meta Code Gear の実装にあたって新しい実装はほとんど行っていない。
+つまり,この Meta Code Gear の実装にあたって新しい実装はほとんど行っていない.
 
-Wait List の 作成も同じように、取り出した state を step させて、そこで一致するnext-codeを状態が変わっていないとし、Wait Listに入れている。
+Wait List の 作成も同じように,取り出した state を step させて,そこで一致するnext-codeを状態が変わっていないとし,Wait Listに入れている.
 
 %いちおうコード載せようかな？←棄却されました%
 
-Wait List について、Thinking と Eathing の状態に関しては状態が変わる可能性がある。
-これを Wait List に入れなければ Wait List のみで dead lock が検知できると考えられる。しかし、DPP以外の他のプログラムをモデル検査する際に、一つ一つ next-code の設定を行うのは煩雑であると考えた。そのため、step した際に状態が変化しないものを Wait List にいれた。これと分岐がない場合という条件にて、dead lock を検知する。これにより Meta Code Gear の作成が簡易化された。そのため、Thinking と Eathing のプロセスも Waithing List に入るようになっている。
+Wait List について,Thinking と Eathing の状態に関しては状態が変わる可能性がある.
+これを Wait List に入れなければ Wait List のみで dead lock が検知できると考えられる.しかし,DPP以外の他のプログラムをモデル検査する際に,一つ一つ next-code の設定を行うのは煩雑であると考えた.そのため,step した際に状態が変化しないものを Wait List にいれた.これと分岐がない場合という条件にて,dead lock を検知する.これにより Meta Code Gear の作成が簡易化された.そのため,Thinking と Eathing のプロセスも Waithing List に入るようになっている.
 
-deadlockの検出方法として、上記の2つのMeta Code Gear で作成したmeta データを使用する。
+deadlockの検出方法として,上記の2つのMeta Code Gear で作成したmeta データを使用する.
 
-そして「num-brunchの値が1であり、wait Listの数がプロセス数と一致する」ということは、「その状態から別の状態に遷移することができない」として、この状態をdead lockであると定義した。
+そして「num-brunchの値が1であり,wait Listの数がプロセス数と一致する」ということは,「その状態から別の状態に遷移することができない」として,この状態をdead lockであると定義した.
 
 以下の\coderef{dpp-judge-mcg}がdead-lockを検知する関数となる
 
-複雑なことは何もしておらず、単純にstate毎のnum-brunchの値を見て、wait-listの数がプロセス数と一致していた場合に
-deadlockのフラグを立ち上げている。これが、Gears Agda におけるアサーションになっている。
+複雑なことは何もしておらず,単純にstate毎のnum-brunchの値を見て,wait-listの数がプロセス数と一致していた場合に
+deadlockのフラグを立ち上げている.これが,Gears Agda におけるアサーションになっている.
 
 % judge-dead-lock-pのソースコードを貼り付ける
 \lstinputlisting[caption=DPP での dead lock を検知する Meta Code Gear, label=code:dpp-judge-mcg]{src/dpp-verif/judge-deadlock.agda.replaced}
 % こいつはmetaEnv2を受け取れるように変えないと行けない
 
-ここから前述した通り、State Listを作成する。
+ここから前述した通り,State Listを作成する.
 
-そのまま実行するだけでは無限に実行されるのみで停止しないと思われる。
-しかし、分岐後に step 実行後の state を保存している State List に同じ State が存在しないかを確かめる。
-存在していた場合はそれを追加せず、存在しなかった場合にのみ State を追加する。
+そのまま実行するだけでは無限に実行されるのみで停止しないと思われる.
+しかし,分岐後に step 実行後の state を保存している State List に同じ State が存在しないかを確かめる.
+存在していた場合はそれを追加せず,存在しなかった場合にのみ State を追加する.
 
-Agdaには2つの record が等しい場合の分岐など存在しないため、
-\coderef{dpp-exclude-state-mcg} のようにrecordの中身を一つづつ一致しているか確認する。
-こちらはそのまま掲載すると長いので、実際のコードに手を加えて省略している。実際のコードは付録にて参照できる。
+Agdaには2つの record が等しい場合の分岐など存在しないため,
+\coderef{dpp-exclude-state-mcg} のようにrecordの中身を一つずつ一致しているか確認する.
+こちらはそのまま掲載すると長いので,実際のコードに手を加えて省略している.実際のコードは付録にて参照できる.
 
 \lstinputlisting[caption=重複しているstateを除外する Meta Code Gear, label=code:dpp-exclude-state-mcg]{src/dpp-verif/exclude-same-env.agda.replaced}
 % 手を加えているので詳細は付録を参照するように促す
 
-MetaEnv2 を受け取ってその中身の state を比較するが、そこまで展開する必要がある。
- loop-metaenv と loop-target-metaenv, eq-env にてそれを行っている。
+MetaEnv2 を受け取ってその中身の state を比較するが,そこまで展開する必要がある.
+ loop-metaenv と loop-target-metaenv, eq-env にてそれを行っている.
 
-更に15行目の loop-metaenv では State List 内に見つからなかった場合に State List に Stateを追加し、次のstateの一致を探索するように記述されている。
+更に15行目の loop-metaenv では State List 内に見つからなかった場合に State List に Stateを追加し,次のstateの一致を探索するように記述されている.
 
-実際にstateの一致を見ているのは22行目のeq-env関数で、一致している State が見つかった場合には追加せずにこちらも次の State を探索するように記述されている
+実際にstateの一致を見ているのは22行目のeq-env関数で,一致している State が見つかった場合には追加せずにこちらも次の State を探索するように記述されている
 
-State が保持している値がそれぞれ正しいのかは eq-pid のように一致を見て分岐させている。
-その値が一致している場合には別の値を見て、一致していない場合はeq-envに遷移して State List にある次の State との一致を見るようにしている。
-他の値である、lhandやrhandなども同じように記述している。
+State が保持している値がそれぞれ正しいのかは eq-pid のように一致を見て分岐させている.
+その値が一致している場合には別の値を見て,一致していない場合はeq-envに遷移して State List にある次の State との一致を見るようにしている.
+他の値である,lhandやrhandなども同じように記述している.
 
 
-これらにて、まだ分岐を見ていない1つのStateの分岐を確かめる。
-発生した分岐を step 実行させる。
-step実行して作成された state が State Listに存在していないかを確かめる。
-これを繰り返すことで State Listを作る。
-State List に存在している全ての state の分岐を見たということは、
-出現するStateを全て網羅することができたと言える。
+これらにて,まだ分岐を見ていない1つのStateの分岐を確かめる.
+発生した分岐を step 実行させる.
+step実行して作成された state が State Listに存在していないかを確かめる.
+これを繰り返すことで State Listを作る.
+State List に存在している全ての state の分岐を見たということは,
+出現するStateを全て網羅することができたと言える.
 
 あとは State List を dead lock の検査を行う Meta Code Gear に与えるとどの state が dead lockしているかを検証することができる
 
 \section{Gears Agda による live lockの検証方法について}
-live lockとは、状態が変動しているが、その状態はループしており、実行が進んでいないことを指す。
+live lockとは,状態が変動しているが,その状態はループしており,実行が進んでいないことを指す.
 
-DPPにて例を上げると、(上の哲学者のフローだと) dead lock が発生するため、フローを変更したとする。それは以下のような動作を追加する。
-「右手にフォークを持っているが、左手のフォークがすでに取られている場合に右手のフォークを即座に置いて固定時間待つ」
-とする。これで解決すると思われるが、全員が同時に食事をしようとした場合、右手のフォークを取ったり置いたりを永遠に繰り返すことになる。
+DPPにて例を上げると,(上の哲学者のフローだと) dead lock が発生するため,フローを変更したとする.それは以下のような動作を追加する.
+「右手にフォークを持っているが,左手のフォークがすでに取られている場合に右手のフォークを即座に置いて固定時間待つ」
+とする.これで解決すると思われるが,全員が同時に食事をしようとした場合,右手のフォークを取ったり置いたりを永遠に繰り返すことになる.
 これを live lock という
 
-つまり、この状態を検知するなら、そのstateが持っているhistoryまで考慮する必要がある。つまり、今回の場合だとstateのloopができた際にコマンドが一巡しているかを確認すると良い。
+つまり,この状態を検知するなら,そのstateが持っているhistoryまで考慮する必要がある.つまり,今回の場合だとstateのloopができた際にコマンドが一巡しているかを確認すると良い.
 
-history がloopしていた際に、誰もeathingしていない場合を live lock していると定義する。
+history がloopしていた際に,誰もeathingしていない場合を live lock していると定義する.
 
-今回のはDPPであるためEatingが挙げられているが、他の実装であれば、どのコマンドが実行されるのが正常な動きなのかを決める。それがloop中に存在いしているかを見れば live lock を検知できる。
+今回のはDPPであるためEatingが挙げられているが,他の実装であれば,どのコマンドが実行されるのが正常な動きなのかを決める.それがloop中に存在いしているかを見れば live lock を検知できる.
 
 
 \section{Gears Agda でのモデル検査の評価}
 
-SPINで行ったDPPのモデル検査に比べると、Gears Agdaの方が制約が多いため難解に思える。しかし、Gears Agda ではプログラムの実装も含んでいる。
+SPINで行ったDPPのモデル検査に比べると,Gears Agdaの方が制約が多いため難解に思える.しかし,Gears Agda ではプログラムの実装も含んでいる.
 
-さらに、Gears Agda での実装をしたあとのモデル検査を行う際の Meta Code Gear の流れは変化しないため、比較的容易であると言える。
+さらに,Gears Agda での実装をしたあとのモデル検査を行う際の Meta Code Gear の流れは変化しないため,比較的容易であると言える.
 
-加えて、Gears Agda は CbC へコンパイルされ、高速に実行されることを踏まえると、いかに Gears Agda が検証に向いたプログラムであるか理解できる。
+加えて,Gears Agda は CbC へコンパイルされ,高速に実行されることを踏まえると,いかに Gears Agda が検証に向いたプログラムであるか理解できる.
 
 % この評価の話はまとめでしたほうがいいかもね？

--- a/Paper/tex/hoare.tex	Wed Feb 01 20:27:04 2023 +0900
+++ b/Paper/tex/hoare.tex	Wed Feb 01 22:16:45 2023 +0900
@@ -1,3 +1,7 @@
+\chapter{Gears Agda による定理証明}
+先行研究\cite{ryokka-sigos}では,Gears Agda ではないプログラムの Hoare Logic による検証\cite{agda2-hoare}を参考にそれを Gears Agda に適応して while loop の検証を行っていた\cite{cr-ryukyu}.
+本研究では,invariant というプログラムの不変条件を定義し,それを検証することで,比較的容易に検証を行うことができるようになった(本章2節)
+本章では Gears Agda による定理証明の方法について説明する.
 
 \section{Hoare Logic}
 Hoare Logic\cite{hoare} とは C.A.R Hoare，

--- a/Paper/tex/intro.tex	Wed Feb 01 20:27:04 2023 +0900
+++ b/Paper/tex/intro.tex	Wed Feb 01 22:16:45 2023 +0900
@@ -1,13 +1,13 @@
 \chapter{Gears Agda でのプログラムの検証}
 
 OSやアプリケーションの信頼性の向上は重要である
-信頼性を向上するための手段として、プログラムを検証する事が挙げられる。
+信頼性を向上するための手段として,プログラムを検証する事が挙げられる.
 
 
-しかし、検証には仕様の形式化とその検証には膨大なコストを要する．
+しかし,検証には仕様の形式化とその検証には膨大なコストを要する．
 そのため，他のプログラミング言語と比べて検証に適しているGears Agdaを使用する．
-Gears Agdaとは当研究室で開発している Continuation based C (CbC) の概念を
-取り入れた記法で記述された Agdaのことである．
+Gears Agdaとは当研究室で開発している Continuation based C \cite{cbc-gcc}(以下CbC) の概念を
+取り入れた記法で記述された Agda \cite{agda} のことである．
 
 通常のプログラミング言語では関数を実行する際にメインルーチンからサブルーチンに遷移する．
 この際メインルーチンで使用していた変数などの環境はスタックされ，サブルーチンが終了し，
@@ -18,12 +18,12 @@
 
 これにより検証を Code Gear 単位に分割することができ，比較的容易に検証を行えるようになっている．
 
-先行研究では、Gears Agda での並列実行の検証について課題が残っていた。
-並列実行の検証を定理証明で行うには、考慮する状態の数が膨大になり困難である。
-そのため、Gears Agda でモデル検査を行うことでこの課題に対応する。
+先行研究\cite{ryokka-sigos}では,Gears Agda での並列実行の検証について課題が残っていた.
+並列実行の検証を定理証明で行うには,考慮する状態の数が膨大になり困難である.
+そのため,Gears Agda でモデル検査\cite{EdmundM}を行うことでこの課題に対応する.
 
-CbCの継続の概念はモデル検査とも相性がよい．
+CbCの継続の概念はモデル検査とも相性がよい．\cite{ikkun-master}
 CbCが末尾関数呼び出しであるため Code Gear をそのまま
 モデルの edge として定義することができるためである．
 
-これらのことから、本論文では、Gears Agda での定理証明とモデル検査について述べる
\ No newline at end of file
+これらのことから,本論文では,Gears Agda での定理証明とモデル検査について述べる
\ No newline at end of file

--- a/Paper/tex/main.tex	Wed Feb 01 20:27:04 2023 +0900
+++ b/Paper/tex/main.tex	Wed Feb 01 22:16:45 2023 +0900
@@ -1,30 +1,30 @@
 \section{AI分野への適応}
-ここまでで Gears Agda を用いたアルゴリズム適用可否探索の方法を示した。
-これのアルゴリズムに当たる部分をニューラルネットワークの中間層の計算式に置き換えて考える。
+ここまでで Gears Agda を用いたアルゴリズム適用可否探索の方法を示した.
+これのアルゴリズムに当たる部分をニューラルネットワークの中間層の計算式に置き換えて考える.
 
-現在、ハードウェア技術、機械学習技術の両方の進歩により
+現在,ハードウェア技術,機械学習技術の両方の進歩により
 ニューラルネットワークの中間層が増加しても
 Residual Block や Dense Block などの勾配を伝搬する経路を確保することで
-勾配消失問題は発生しなくなった。\cite{DBLP:journals/corr/HeZRS15}\cite{DBLP:journals/corr/HuangLW16a}
-しかし、中間層が増加していることによるモデルサイズの肥大化や計算量の増加からは逃れられない。
+勾配消失問題は発生しなくなった.\cite{DBLP:journals/corr/HeZRS15}\cite{DBLP:journals/corr/HuangLW16a}
+しかし,中間層が増加していることによるモデルサイズの肥大化や計算量の増加からは逃れられない.
 
-この問題に対して、複数の中間層をより少ない数の中間層で置き換えることができないか探索を行う。
-加えて、考案した新規の計算式を考慮するようにし、その妥当性を考慮したり、
-現在扱っていない数式自体を組み合わせの全探索によって構築し模索することもできると考える。
+この問題に対して,複数の中間層をより少ない数の中間層で置き換えることができないか探索を行う.
+加えて,考案した新規の計算式を考慮するようにし,その妥当性を考慮したり,
+現在扱っていない数式自体を組み合わせの全探索によって構築し模索することもできると考える.
 
 \subsection{中間層の圧縮と新しいレイヤー計算式の開発}
-2章で述べた手法について、
-アルゴリズム群を中間層の計算式と置き換える。
-これはレイヤーの計算式１つずつのみを格納しているのではなく、
-その組み合わせも保持しておく。
+2章で述べた手法について,
+アルゴリズム群を中間層の計算式と置き換える.
+これはレイヤーの計算式１つずつのみを格納しているのではなく,
+その組み合わせも保持しておく.
 これにより複数のレイヤーの組み合わせと等しい計算をしている
-それ以下の組み合わせで実現できないかを探索する。
+それ以下の組み合わせで実現できないかを探索する.
 
-完全に等しい計算式を探索するのが難しい場合は、ある程度一致している
-計算を出せるようにしてもよいと考えている。
+完全に等しい計算式を探索するのが難しい場合は,ある程度一致している
+計算を出せるようにしてもよいと考えている.
 
-また、レイヤーの計算式を格納している部分に、新しい計算式を
-加えることで、新しいレイヤーの計算式を開発できるとも考えている。
+また,レイヤーの計算式を格納している部分に,新しい計算式を
+加えることで,新しいレイヤーの計算式を開発できるとも考えている.
 
-さらに、その新規で追加する計算式も探索により作成することも
-できると想定している。
+さらに,その新規で追加する計算式も探索により作成することも
+できると想定している.

--- a/Paper/tex/spin_dpp.tex	Wed Feb 01 20:27:04 2023 +0900
+++ b/Paper/tex/spin_dpp.tex	Wed Feb 01 22:16:45 2023 +0900
@@ -1,17 +1,17 @@
 \chapter{Gears Agda によるモデル検査}
 定理証明では数学的な証明をするため状態爆発を起こさず検証を行うことが
 できるが，専門的な知識が多く難易度が高いという欠点がある．
-加えて、CbCでは並列処理も実行できる\cite{parusu-master}が、
-並列処理を定理証明するには検証する状態が膨大になり困難である。
-そのため、並列処理はモデル検査にて検証する方が良い。
+加えて,CbCでは並列処理も実行できる\cite{parusu-master}が,
+並列処理を定理証明するには検証する状態が膨大になり困難である.
+そのため,並列処理はモデル検査にて検証する方が良い.
 
 \section{モデル検査とは}
-モデル検査 (Model Cheking) とは、検証手法のひとつである。
+モデル検査 (Model Cheking) とは,検証手法のひとつである.
 モデル検査はプログラムが入力に対して仕様を満たした動作を
 行うことを網羅的に検証することを指す．
-しかし、モデル検査と定理証明を比較した際に，モデル検査は入力が無限になる
+しかし,モデル検査と定理証明を比較した際に，モデル検査は入力が無限になる
 状態爆発が起こり得るという問題がある．
-実際にモデル検査で行うことは、検証したい内容の時相理論式 $\varphi$  を作り、対象のシステムの初期状態 s のモデル M があるとき、M, s が $\varphi$ を満たすかを調べる。
+実際にモデル検査で行うことは,検証したい内容の時相理論式 $\varphi$  を作り,対象のシステムの初期状態 s のモデル M があるとき,M, s が $\varphi$ を満たすかを調べる.
 
 \section{Dining Philosophers Problem}
 今回はモデル検査を行う対象として Dining Philosophers Problem (以下DPP)
@@ -50,20 +50,20 @@
 
 \section{SPINによるモデル検査}% 内容にそぐわない場合は使わない
 
-SPIN(Simple Promela INterpreter) とは一般的にモデル検査に使用されるツールである。これは使用記述言語 PROMELA(Process Meta Language) による記述を元にプログラムが取る状態を網羅し、モデル検査を行うことができる。
+SPIN(Simple Promela INterpreter) \cite{spin}とは一般的にモデル検査に使用されるツールである.これは使用記述言語 PROMELA(Process Meta Language) による記述を元にプログラムが取る状態を網羅し,モデル検査を行うことができる.
 
-今回 Gears Agda でのモデル検査と比較するために、SPINでのDPPプログラムのモデル検査に必要なコードの一部を\coderef{spin-dpp}に載せる。
+今回 Gears Agda でのモデル検査と比較するために,SPINでのDPPプログラムのモデル検査に必要なコードの一部を\coderef{spin-dpp}に載せる.
 
 \lstinputlisting[caption= SPINにてDPPをモデル検査する際のコードの一部 , label=code:spin-dpp]{src/dpp-verif/spin.pml}
 
-コードを簡単に説明する。哲学者がThinkの状態から食事をしようとしだした際の状態の変化が4行目と5行目になっている。
-forkの状態を配列で管理している。0 である状態が誰もそのforkを持っていない状態である。ここでは、5人目の人が右手にあるフォークを取ろうとした際に配列の最初を取ることが5行目に記述されている。
+コードを簡単に説明する.哲学者がThinkの状態から食事をしようとしだした際の状態の変化が4行目と5行目になっている.
+forkの状態を配列で管理している.0 である状態が誰もそのforkを持っていない状態である.ここでは,5人目の人が右手にあるフォークを取ろうとした際に配列の最初を取ることが5行目に記述されている.
 
-左手のフォークを取る動作も同じように記述する。
-SPINではこのコードを元にプログラムが取りうる状態全てを網羅し、モデル検査を行うことができる。
+左手のフォークを取る動作も同じように記述する.
+SPINではこのコードを元にプログラムが取りうる状態全てを網羅し,モデル検査を行うことができる.
 
-\figref{DPP-model}はこのPromelaから作成された状態遷移図になる。
-SPINではコードからプログラムの状態遷移図を出力することができる他、プログラムのstep実行など幅広くモデル検査を行うことができる。
+\figref{DPP-model}はこのPromelaから作成された状態遷移図になる.
+SPINではコードからプログラムの状態遷移図を出力することができる他,プログラムのstep実行など幅広くモデル検査を行うことができる.
 
 \begin{figure}[htpb]
     \begin{center}

--- a/Paper/tex/thanks.tex	Wed Feb 01 20:27:04 2023 +0900
+++ b/Paper/tex/thanks.tex	Wed Feb 01 22:16:45 2023 +0900
@@ -1,11 +1,11 @@
 \chapter*{謝辞}
 \addcontentsline{toc}{chapter}{謝辞}
 
-本研究の遂行、本論文の作成にあたり、御多忙にも関わらず終始懇切なる御指導と御教授を賜わりました河野真治准教授に心より感謝致します。
-共に研究を行い暖かな気遣いと励ましをもって支えてくれた並列信頼研究室の全てのメンバーに感謝致します。
-私の研究において苦楽を共にした Manjaro Linux とその開発者には頭が上がりません。
-さらに、ゼミの前においしいご飯で元気づけてくれた Hally's Cafe に感謝しております。
-最後に、 有意義な時間を共に過ごした理工学研究科工学専攻の学友、並びに物心両面で支えてくれた家族に深く感謝致します。
+本研究の遂行,本論文の作成にあたり,御多忙にも関わらず終始懇切なる御指導と御教授を賜わりました河野真治准教授に心より感謝致します.
+共に研究を行い暖かな気遣いと励ましをもって支えてくれた並列信頼研究室の全てのメンバーに感謝致します.
+私の研究において苦楽を共にした Manjaro Linux とその開発者には頭が上がりません.
+さらに,ゼミの前においしいご飯で元気づけてくれた Hally's Cafe に感謝しております.
+最後に, 有意義な時間を共に過ごした理工学研究科工学専攻の学友,並びに物心両面で支えてくれた家族に深く感謝致します.
 
 \begin{flushright}
     2023年 3月 \\ 上地悠斗

--- a/Paper/tex/tree_desc.tex	Wed Feb 01 20:27:04 2023 +0900
+++ b/Paper/tex/tree_desc.tex	Wed Feb 01 22:16:45 2023 +0900
@@ -1,11 +1,11 @@
 \section{Gears Agda における Binary Tree の検証}
 
 ここでは Gears Agda にて 再帰的なデータ構造を検証する例として，
-Binary Tree を実装・検証する．
+Binary Tree \cite{rbtree} を実装・検証する．
 
 \subsection{Gears Agda における木構造の設計}
 
-本研究では，Gears Agda にて Red Black Tree の検証を行うにあたり，
+本研究では，Gears Agda にて Binary Tree の検証を行うにあたり，
 Agda が変数に対して再代入を許していないことが問題になってくる．
 
 そのため下図 \ref{fig:rbt-stack} のように，木構造の root から leaf　に 辿る際に見ているnodeから
@@ -23,14 +23,11 @@
 \end{figure}
  
 
-このようにして Gears Agda にて Red Black Tree を実装していく．
+このようにして Gears Agda にて Binary Tree を実装していく．
 
 \subsection{Gears Agda における 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}