Mercurial > hg > Papers > 2017 > atton-master
annotate paper/cbc-type.tex @ 64:10a550bf7e4a
Mini fixes with ryokka-san
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 03 Feb 2017 14:49:58 +0900 |
| parents | 6d8825f3b051 |
| children | c0693ad89f04 |
| rev | line source |
|---|---|
| 57 | 1 \chapter{Agda における Continuation based C の表現} |
| 2 \label{chapter:cbc-type} | |
| 58 | 3 CbC の項を部分型を用いて Agda 上に記述していく。 |
| 4 DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、 Agda 上で実行できることを確認する。 | |
| 5 また、Agda上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda 上で証明していく。 | |
| 6 | |
| 59 | 7 % {{{ DataSegment の定義 |
| 58 | 8 \section{DataSegment の定義} |
| 9 まず DataSegment から定義していく。 | |
| 10 DataSegment はレコード型で表現できるため、Agda のレコードをそのまま利用できる。 | |
| 11 例えは~\ref{src:goto} に示していた a と b を加算して c を出力するプログラムに必要な DataSegment を記述すると~\ref{src:agda-ds}のようになる。 | |
| 12 cs0 は a と b の二つの Int 型の変数を利用するため、対応する ds0 は a と b のフィールドを持つ。 | |
| 13 cs1 は計算結果を格納する c という名前の変数のみを持つので、同様にds1もcのみを持つ。 | |
| 14 | |
| 15 \lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda} | |
| 59 | 16 % }}} |
| 58 | 17 |
| 59 | 18 % {{{ CodeSegment の定義 |
| 57 | 19 \section{CodeSegment の定義} |
| 58 | 20 次に CodeSegment を定義する。 |
| 21 CodeSegment は DataSegment を取って DataSegment を返すものである。 | |
| 22 よって $ I \rightarrow O $ を内包するデータ型を定義する。 | |
| 23 | |
| 24 レコード型の型は Set なので、Set 型を持つ変数 I と O を型変数に持ったデータ型 CodeSegment を定義する。 | |
| 25 I は Input DataSegment の型であり、 O は Output DataSegment である。 | |
| 26 | |
| 27 CodeSegment 型のコンストラクタには \verb/cs/ があり、Input DataSegment を取って Output DataSegment を返す関数を取る。 | |
| 28 具体的なデータ型の定義はリスト ~\ref{src:agda-cs} のようになる。 | |
| 29 | |
| 59 | 30 \lstinputlisting[label=src:agda-cs, caption= Agda における CodeSegment 型の定義] {src/CodeSegment.agda.replaced} |
| 58 | 31 |
| 32 この CodeSegment 型を用いて CodeSegment の処理本体を記述する。 | |
| 33 | |
| 34 まず計算の本体となる cs0 に注目する。 | |
| 35 cs0 は二つのInt型変数を持つ ds0 を取り、一つのInt型変数を作った上で cs1 に軽量継続を行なう。 | |
| 36 DataSegment はレコードなので、a と b のフィールドから値を取り出した上で加算を行ない、cを持つレコードを生成する。 | |
| 37 そのレコードを引き連れたまま cs1 へと goto する。 | |
| 38 | |
| 39 次に cs1 に注目する。 | |
| 40 cs1 は値に触れず cs2 へと goto するだけである。 | |
| 41 よって何もせずにそのまま goto する関数をコンストラクタ\verb/cs/ に渡すだけで良い。 | |
| 42 | |
| 43 最後に cs2 である。 | |
| 44 cs2 はリスト~\ref{src:goto}では省略していたが、今回は計算を終了させる CodeSegment として定義する。 | |
| 45 どの CodeSegment にも軽量継続せずに値を持ったまま計算を終了させる。 | |
| 46 コンストラクタ \verb/cs/ には関数を与えなくては値を構成できないため、何もしない関数である id を渡している。 | |
| 47 | |
| 48 最後に計算をする cs0 へと軽量継続する main を定義する。 | |
| 49 例として、 a の値を 100 とし、 b の値を50としている。 | |
| 59 | 50 |
| 51 cs0, cs1, cs2, main をAgda で定義するとリスト~\ref{src:agda-css}のようになる。 | |
| 52 | |
| 53 \lstinputlisting[label=src:agda-css, caption= Agda における CodeSegment の定義] {src/CodeSegments.agda} | |
| 54 | |
| 55 正しく計算が行なえたなら値150が得られるはずである。 | |
| 56 % }}} | |
| 58 | 57 |
| 60 | 58 % {{{ ノーマルレベル計算の実行 |
| 57 | 59 \section{ノーマルレベル計算の実行} |
| 60 | 60 プログラムを実行することは \verb/goto/ を定義することと同義である。 |
| 61 軽量継続\verb/goto/ の性質としては | |
| 62 | |
| 63 \begin{itemize} | |
| 64 \item 次に実行する CodeSegment を指定する | |
| 65 \item CodeSegment に渡すべき DataSegment を指定する | |
|
61
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
66 \item 現在実行している CodeSegment から制御を指定された CodeSegment へと移動させる |
| 60 | 67 \end{itemize} |
| 68 | |
| 69 がある。 | |
| 70 Agda における CodeSegment の本体は関数である。 | |
| 71 関数をそのまま使用すると再帰を許してしまうために CbC との対応が失われてしまう。 | |
| 72 よって、\verb/goto/を利用できるのは関数の末尾のみである、という制約を関数に付け加える必要がある。 | |
| 73 | |
| 74 この制約さえ満たせば、CodeSegment の実行は CodeSegment 型から関数本体を取り出し、レコード型を持つ値を適用することに相当する。 | |
| 75 具体的に \verb/goto/ を関数として適用するとリスト~\ref{src:agda-goto}のようになる。 | |
| 76 | |
| 77 \lstinputlisting[label=src:agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda} | |
| 78 | |
| 79 この \verb/goto/ の定義を用いることで main などの関数が評価できるようになり、値150が得られる。 | |
| 80 本文中での CodeSegment の定義は一部を抜粋している。 | |
| 81 実行可能な Agda のソースコードは付録に載せる。% TODO: Appendix | |
| 82 | |
| 83 % }}} | |
| 84 | |
|
61
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
85 % {{{ Meta DataSegment の定義 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
86 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
87 \section{Meta DataSegment の定義} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
88 ノーマルレベルの CbC を Agda 上で記述し、実行することができた。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
89 次にメタレベルの計算を Agda 上で記述していく。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
90 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
91 Meta DataSegment はノーマルレベルの DataSegment の集合として定義できるものであり、全ての DataSegment の部分型であった。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
92 ノーマルレベルの DataSegment はプログラムによって変更されるので、事前に定義できるものではない。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
93 ここで、Agda の Parameterized Module を利用して、「Meta DataSegment の上位型は DataSegment である」のように DataSegment を定義する。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
94 こうすることにより、全てのプログラムは一つ以上の Meta DataSegment を持ち、任意の個数の DataSegment を持つ。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
95 また、Meta DataSegment をメタレベルの DataSegment として扱うことにより、「Meta DataSegment の部分型である Meta Meta DataSegment」を定義できるようになる。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
96 階層構造でメタレベルを表現することにより、計算の拡張を自在に行なうことができる。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
97 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
98 具体的な Meta DataSegment の定義はリスト~\ref{src:agda-mds}のようになる。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
99 型システム \verb/subtype/ は、Meta DataSegment である \verb/Context/ を受けとることにより構築される。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
100 Context を Meta DataSegment とするプログラム上では DataSegment は Meta CodeSegment の上位型となる。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
101 その制約を \verb/DataSegment/ 型は表わしている。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
102 |
|
62
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
103 \lstinputlisting[label=src:agda-mds, caption=Agda における Meta DataSegment の定義] {src/MetaDataSegment.agda.replaced} |
|
61
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
104 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
105 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
106 ここで、関数を部分型に拡張する S-ARROW をもう一度示す。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
107 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
108 \begin{align*} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
109 \AxiomC{$ T_1 <: S_1$} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
110 \AxiomC{$ S_2 <: T_2$} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
111 \BinaryInfC{$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
112 \DisplayProof && \text{S-ARROW} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
113 \end{align*} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
114 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
115 S-ARROW は、前提である部分型関係 $ T_1 <: S_1 $ と $ S_2 <: T_2 $ が成り立つ時に、 上位型 $ S_1 \rightarrow S_2 $ の関数を、部分型 $ T_1 \rightarrow T_2 $ に拡張できた。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
116 ここでの上位型は DataSegment であり、部分型は Meta DataSegment である。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
117 制約\verb/DataSegment/ の \verb/get/ は、 Meta DataSegment から DataSegment が生成できることを表す。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
118 これは前提 $ T_1 <: S_1 $ に相当する。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
119 そして、\verb/set/ は $ S_2 <: T_2 $ に相当する。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
120 しかし、任意の DataSegment が Meta DataSegment の部分型となるには、 DataSegment が Meta DataSegment よりも多くの情報を必ず持たなくてはならないが、これは通常では成り立たない。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
121 だが、メタ計算を行なう際には常に Meta DataSegment を一つ以上持っていると仮定するならば成り立つ。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
122 実際、GearsOS における赤黒木では Meta DataSegment に相当する \verb/Context/ を常に持ち歩いている。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
123 GearsOS における計算結果はその持ち歩いている Meta DataSegment の更新に相当するため、常に Meta DataSegment を引き連れていることを無視すれば DataSegment から Meta DataSegment を導出できる。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
124 よって $ S_2 <: T_2 $ が成り立つ。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
125 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
126 なお、 $ S_2 <: T_2 $ は Output DataSegment を Meta DataSegment を格納する作業に相当し、 $ T_1 <: S_1 $ は Meta DataSegment から Input DataSegment を取り出す作業であるため、これは明らかに \verb/stub/ である。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
127 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
128 % }}} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
129 |
|
62
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
130 % {{{ Meta CodeSegment の定義 |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
131 |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
132 \section{Meta CodeSegment の定義} |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
133 Meta DataSegment が定義できたので Meta CodeSegment を定義する。 |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
134 実際、DataSegment が Meta DataSegment に拡張できたため、Meta CodeSegment の定義には比較的変更は無い。 |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
135 ノーマルレベルの \verb/CodeSegment/ 型に、DataSegment を取って DataSegment を返す、という制約を明示的に付けるだけである(リスト~\ref{src:agda-mcs}) |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
136 |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
137 \lstinputlisting[label=src:agda-mcs, caption=Agda における Meta CodeSegment の定義] {src/MetaCodeSegment.agda.replaced} |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
138 |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
139 % }}} |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
140 |
|
63
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
141 % {{{ メタレベル計算の実行 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
142 |
| 57 | 143 \section{メタレベル計算の実行} |
|
63
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
144 Meta DataSegment と Meta CodeSegment の定義を行なったので、残るは実行である。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
145 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
146 実行はノーマルレベルにおいては軽量継続 \verb/goto/ を定義することによって表せた。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
147 メタレベル実行ではそれを Meta CodeSegment と Meta DataSegment を扱えるように拡張する。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
148 Meta DataSegment は Parameterized Module の引数 \verb/Context/ に相当するため、Meta CodeSegment は Context を取って Context を返す CodeSegment となる。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
149 軽量継続 \verb/goto/ と区別するために名前を \verb/exec/ とするリスト~\ref{src:agda-exec}のように定義できる。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
150 行なっていることは Meta CodeSegment の本体部分に Meta DataSegment を渡す、という \verb/goto/ と変わらないが、\verb/set/ と \verb/get/ を用いることで上位型である任意の DataSegment を実行する CodeSegment も Meta CodeSegment として一様に実行できる。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
151 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
152 \lstinputlisting[label=src:agda-exec, caption=Agda におけるメタレベル実行の定義] {src/Exec.agda.replaced} |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
153 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
154 実行例として、リスト~\ref{src:goto} に示していた a と b の値を加算して c に代入するプログラムを考える。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
155 実行する際に c の値を \verb/c'/ に保存してから加算ようなメタ計算を考える。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
156 c の値を \verb/c'/ に保存するタイミングは軽量継続時にユーザが指定する。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
157 よって軽量継続を行なうのと同等の情報を保持してなくてはならない。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
158 そのために Meta Meta DataSegment \verb/Meta/ には制御を移す対象であるノーマルレベル CodeSegment を持つ。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
159 値を格納する \verb/c'/ の位置は Meta DataSegment でも Meta Meta DataSegment でも構わないが、今回は Meta Meta DataSegemnt に格納するものとする。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
160 それらを踏まえた上での Meta Meta DataSegment の Agda 上での定義は~\ref{src:agda-mmds}のようになる。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
161 なお、\verb/goto/ などの名前の衝突を避けるためにノーマルレベルの定義は \verb/N/ に、メタレベルの定義は \verb/M/ へと名前を付けかえている。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
162 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
163 \lstinputlisting[label=src:agda-mmds, caption=Agda における Meta Meta DataSegment の定義例] {src/MetaMetaDataSegment.agda} |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
164 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
165 定義した \verb/Meta/ を利用して、c を \verb/c'/に保存するメタ計算 \verb/push/ を定義する。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
166 より構文が CbC に似るように \verb/gotoMeta/ を糖衣構文的に定義する。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
167 \verb/gotoMeta/ や \verb/push/ で利用している \verb/liftContext/ や \verb/liftMeta/ はノーマルレベル計算をメタ計算レベルとするように型を明示的に変更するものである。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
168 結果的に \verb/main/ の \verb/goto/ を \verb/gotoMeta/ に置き換えることにより、c の値を計算しながら保存できる。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
169 リスト~\ref{src:agda-mmcs} に示したプログラムでは、通常レベルのコードセグメントを全く変更せずにメタ計算を含む形に拡張している。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
170 加算を行なう前の \verb/c/ の値が \verb/70/ であったとした時、計算結果 \verb/150/ は \verb/c/ に格納されるが、\verb/c'/には\verb/70/に保存されている。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
171 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
172 \lstinputlisting[label=src:agda-mmcs, caption=Agda における Meta Meta CodeSegment の定義と実行例] {src/MetaMetaCodeSegment.agda} |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
173 |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
174 なお、CbC におけるメタ計算を含む軽量継続\verb/goto meta/とAgda におけるメタ計算実行の比較はリスト~\ref{src:goto-meta}のようになる |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
175 % TODO: cbc と agda の diff |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
176 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
177 CodeSegment や Meta CodeSegment などの定義が多かっため、どの処理やデータがどのレベルに属するか複雑になったため、一度図にてまとめる。 |
|
63
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
178 Meta DataSegment を含む任意の DataSegment は Meta DataSegment になりえるので、この階層構造は任意の段数定義することが可能である。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
179 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
180 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
181 % TODO: メタの階層構造の図 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
182 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
183 % }}} |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
184 |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
185 \section{Agda を用いた Continuation based C の検証} |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
186 Agda において CbC の CodeSegment と DataSegment を定義することができた。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
187 実際の CbC のコードを Agda に変換し、それらの性質を証明していく。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
188 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
189 ここでは赤黒木の実装に用いられているスタックの性質について注目する。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
190 この時のスタックはポインタを利用した片方向リストを用いる。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
191 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
192 CbC における構造体 \verb/stack/ の定義はリスト~\ref{src:cbc-stack}のようになっている。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
193 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
194 \lstinputlisting[label=src:cbc-stack, caption=CbC における構造体 stack の定義] {src/stack.h} |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
195 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
196 Agda にはポインタが無いため、メモリ確保や\verb/NULL/の定義は存在しない。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
197 CbC におけるメモリ確保部分はノーマルレベルには出現しないと仮定して、\verb/NULL/の表現にはAgda の標準ライブラリに存在する \verb/Data.Maybe/ を用いる。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
198 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
199 \verb/Data.Maybe/ の \verb/maybe/ 型は、コンストラクタを二つ持つ。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
200 片方のコンストラクタ \verb/just/ は値を持つ。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
201 これは計算を行なうことができる値であり、ポインタの先に値があることに対応している。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
202 一方のコンストラツア \verb/nothing/ は値を持たない。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
203 これは値が存在せず、ポインタの先が確保されていない(\verb/NULL/ ポインタである)ことを表現できる。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
204 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
205 \lstinputlisting[label=src:agda-maybe, caption=Agda における Maybe の定義] {src/Maybe.agda.replaced} |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
206 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
207 |
| 57 | 208 \section{スタックの実装の検証} |