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