Mercurial > hg > Papers > 2017 > atton-master

comparison paper/cbc-type.tex @ 64:10a550bf7e4a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
63:6d8825f3b051 64:10a550bf7e4a
169 リスト~\ref{src:agda-mmcs} に示したプログラムでは、通常レベルのコードセグメントを全く変更せずにメタ計算を含む形に拡張している。 169 リスト~\ref{src:agda-mmcs} に示したプログラムでは、通常レベルのコードセグメントを全く変更せずにメタ計算を含む形に拡張している。
170 加算を行なう前の \verb/c/ の値が \verb/70/ であったとした時、計算結果 \verb/150/ は \verb/c/ に格納されるが、\verb/c'/には\verb/70/に保存されている。 170 加算を行なう前の \verb/c/ の値が \verb/70/ であったとした時、計算結果 \verb/150/ は \verb/c/ に格納されるが、\verb/c'/には\verb/70/に保存されている。
171 171
172 \lstinputlisting[label=src:agda-mmcs, caption=Agda における Meta Meta CodeSegment の定義と実行例] {src/MetaMetaCodeSegment.agda} 172 \lstinputlisting[label=src:agda-mmcs, caption=Agda における Meta Meta CodeSegment の定義と実行例] {src/MetaMetaCodeSegment.agda}
173 173
174 メタの階層構造を表すと図のようになる。 174 なお、CbC におけるメタ計算を含む軽量継続\verb/goto meta/とAgda におけるメタ計算実行の比較はリスト~\ref{src:goto-meta}のようになる
175 % TODO: cbc と agda の diff
176
177 CodeSegment や Meta CodeSegment などの定義が多かっため、どの処理やデータがどのレベルに属するか複雑になったため、一度図にてまとめる。
175 Meta DataSegment を含む任意の DataSegment は Meta DataSegment になりえるので、この階層構造は任意の段数定義することが可能である。 178 Meta DataSegment を含む任意の DataSegment は Meta DataSegment になりえるので、この階層構造は任意の段数定義することが可能である。
176 179
177 180
178 % TODO: メタの階層構造の図 181 % TODO: メタの階層構造の図
179 182
180 % }}} 183 % }}}
181 184
182 \section{Agda を用いたContinuation based C の検証} 185 \section{Agda を用いた Continuation based C の検証}
186 Agda において CbC の CodeSegment と DataSegment を定義することができた。
187 実際の CbC のコードを Agda に変換し、それらの性質を証明していく。
188
189 ここでは赤黒木の実装に用いられているスタックの性質について注目する。
190 この時のスタックはポインタを利用した片方向リストを用いる。
191
192 CbC における構造体 \verb/stack/ の定義はリスト~\ref{src:cbc-stack}のようになっている。
193
194 \lstinputlisting[label=src:cbc-stack, caption=CbC における構造体 stack の定義] {src/stack.h}
195
196 Agda にはポインタが無いため、メモリ確保や\verb/NULL/の定義は存在しない。
197 CbC におけるメモリ確保部分はノーマルレベルには出現しないと仮定して、\verb/NULL/の表現にはAgda の標準ライブラリに存在する \verb/Data.Maybe/ を用いる。
198
199 \verb/Data.Maybe/ の \verb/maybe/ 型は、コンストラクタを二つ持つ。
200 片方のコンストラクタ \verb/just/ は値を持つ。
201 これは計算を行なうことができる値であり、ポインタの先に値があることに対応している。
202 一方のコンストラツア \verb/nothing/ は値を持たない。
203 これは値が存在せず、ポインタの先が確保されていない(\verb/NULL/ ポインタである)ことを表現できる。
204
205 \lstinputlisting[label=src:agda-maybe, caption=Agda における Maybe の定義] {src/Maybe.agda.replaced}
206
207
183 \section{スタックの実装の検証} 208 \section{スタックの実装の検証}