|
2
|
1 \section{GearsAgda 形式で書く agda}
|
|
5
|
2 CbC の継続の概念を取り入れた Agda の記法を説明する．
|
|
|
3 Agdaでは関数の再帰呼び出しが可能であるが，CbCでは値が 帰って来ない．そのためAgda
|
|
|
4 で実装を行う際には再帰呼び出しを行わないようにする．
|
|
2
|
5
|
|
5
|
6 以下で Gears Agda の記述方法を足し算を行うプログラムを用いて説明する．
|
|
0
|
7
|
|
2
|
8 \lstinputlisting[caption= Agdaでの Data Gear の定義, label=agda-dg, firstline=6, lastline=11]{src/agda/cbc-agda.agda.replaced}
|
|
|
9
|
|
|
10 \lstinputlisting[caption= Agdaでの Code Gear の定義, label=agda-cg, firstline=12, lastline=16]{src/agda/cbc-agda.agda.replaced}
|
|
|
11
|
|
|
12 \lstinputlisting[caption= Agdaでの 停止性が示せない CodeGear の例, label=agda-not-cg, firstline=18, lastline=22]{src/agda/cbc-agda.agda.replaced}
|
|
0
|
13
|
|
2
|
14 \lstinputlisting[caption= Agdaでの CodeGear の初期化, label=agda-exec-cg, firstline=24]{src/agda/cbc-agda.agda.replaced}
|
|
|
15
|
|
5
|
16 Code \ref{agda-dg}が Data Gear の定義をしている．
|
|
|
17 今回は足し算を実装するので，varx に vary を足すことを考える．
|
|
|
18 そのためそれらが2つの自然数を持つようにしている．
|
|
0
|
19
|
|
5
|
20 Code \ref{agda-cg}では Code Gear の定義になる．
|
|
|
21 最初に Data Gear となる env を受け取ったあと，そのまま次の関数に遷移させている．
|
|
0
|
22
|
|
5
|
23 Agda の記述は Curry-Howard 対応になっていて，
|
|
|
24 最初に関数名のあとに:（コロン）の後ろに命題を記述し，
|
|
|
25 そのあとに関数名のあとに引数を書き，=（イコール）の後ろに定義を記述しています．
|
|
0
|
26
|
|
5
|
27 Gears Agda での Code Gear の命題は必ず （Env $\rightarrow$ t） $\rightarrow$ t で
|
|
|
28 終了するようになっている．この （Env $\rightarrow$ t） は引数で受け取る型で Env を
|
|
|
29 受け取ってtを返すという意味になる．これが Code Gear を実行したあとの末尾関数呼び出しを
|
|
|
30 行う次の Code Gear となる． 最後にtを返すとなっているのは，これ自体が Code Gear であることを
|
|
|
31 示している．
|
|
0
|
32
|
|
5
|
33 受け取ったあとに別の関数に再度渡している．
|
|
|
34 これは後述するが，Agdaの繰り返し処理を行う際に停止性を
|
|
|
35 見失うために減少列を引数に取っている．
|
|
2
|
36
|
|
5
|
37 内部の処理はreducerを減らしながらvarxを増やすことで
|
|
|
38 varyの値をvarxに与えていくことで足し算を定義している．
|
|
2
|
39
|
|
|
40 基本的に繰り返し実行するコードを実装する場合には
|
|
5
|
41 実行時に減少し，その関数がいずれ停止することを示す
|
|
|
42 reducerを含めるようにしている．
|
|
0
|
43
|
|
5
|
44 reducerを含めなかった際の Code Gear を Code \ref{agda-not-cg}に示す．
|
|
|
45 agdaではパターンマッチを行うことで場合分けを考えることができるが，
|
|
|
46 受け取った Code Gear であるenvを with を使用してパターンマッチを試みている．
|
|
|
47 パターンマッチ自体は可能だが，この方法だとAgdaが関数が停止することを認識できない．
|
|
|
48 そのため，\{-$\#$ TERMINATING $\#$-\} を関数定義の前にアノテーションし
|
|
|
49 この関数が停止することを記述してコンパイルが通るようにしている．
|
|
0
|
50
|
|
2
|
51 Code \ref{agda-exec-cg} は受け取った引数で Data Gear を初期化して
|
|
5
|
52 それを Code Gear に与えることで実行を行っている．
|
|
0
|
53
|
|
2
|
54 今回の例では 引数から Data Gear を作成するのは
|
|
5
|
55 複雑ではないため，一度で Data Gear を作成してそれを Code Gear に渡している
|
|
2
|
56 引数から Data Gear を作成するのが複雑な場合は一度 入力から
|
|
5
|
57 Data Gear を作成する Code Gear を用いる．
|
|
2
|
58
|
|
5
|
59 加えて，実行なので命題の部分の最後が Env になっている．
|
|
0
|
60
|
|
|
61 \subsection{agda による Meta Gears}
|
|
5
|
62 通常の Meta Gears はノーマルレベルの CodeGear， DataGear では扱えないメタレベルの計算を扱う単位である．
|
|
2
|
63 今回はモデル検査を行う際に使用する
|
|
0
|
64
|
|
|
65 \begin{itemize}
|
|
|
66 \item Meta DataGear \mbox{}\\
|
|
5
|
67 Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる．
|
|
|
68 通常の Data Gear を wraping している．今回はこれを用いることで，モデル検査の状態を保存する
|
|
0
|
69
|
|
|
70 \item Meta CodeGear\mbox{}\\
|
|
|
71 Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear
|
|
5
|
72 である．Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返
|
|
|
73 す CodeGear である．今回はここでモデル検査を行う
|
|
0
|
74 \end{itemize}
|
|
|
75
|
