Mercurial > hg > Papers > 2018 > nozomi-master
view paper/cbc-type.tex @ 60:ecd3a1e40921
Add normal level goto
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 01 Feb 2017 15:37:11 +0900 |
parents | 5450e7ae5fa5 |
children | 3981580ece72 |
line wrap: on
line source
\chapter{Agda における Continuation based C の表現} \label{chapter:cbc-type} CbC の項を部分型を用いて Agda 上に記述していく。 DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、 Agda 上で実行できることを確認する。 また、Agda上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda 上で証明していく。 % {{{ DataSegment の定義 \section{DataSegment の定義} まず DataSegment から定義していく。 DataSegment はレコード型で表現できるため、Agda のレコードをそのまま利用できる。 例えは~\ref{src:goto} に示していた a と b を加算して c を出力するプログラムに必要な DataSegment を記述すると~\ref{src:agda-ds}のようになる。 cs0 は a と b の二つの Int 型の変数を利用するため、対応する ds0 は a と b のフィールドを持つ。 cs1 は計算結果を格納する c という名前の変数のみを持つので、同様にds1もcのみを持つ。 \lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda} % }}} % {{{ CodeSegment の定義 \section{CodeSegment の定義} 次に CodeSegment を定義する。 CodeSegment は DataSegment を取って DataSegment を返すものである。 よって $ I \rightarrow O $ を内包するデータ型を定義する。 レコード型の型は Set なので、Set 型を持つ変数 I と O を型変数に持ったデータ型 CodeSegment を定義する。 I は Input DataSegment の型であり、 O は Output DataSegment である。 CodeSegment 型のコンストラクタには \verb/cs/ があり、Input DataSegment を取って Output DataSegment を返す関数を取る。 具体的なデータ型の定義はリスト ~\ref{src:agda-cs} のようになる。 \lstinputlisting[label=src:agda-cs, caption= Agda における CodeSegment 型の定義] {src/CodeSegment.agda.replaced} この CodeSegment 型を用いて CodeSegment の処理本体を記述する。 まず計算の本体となる cs0 に注目する。 cs0 は二つのInt型変数を持つ ds0 を取り、一つのInt型変数を作った上で cs1 に軽量継続を行なう。 DataSegment はレコードなので、a と b のフィールドから値を取り出した上で加算を行ない、cを持つレコードを生成する。 そのレコードを引き連れたまま cs1 へと goto する。 次に cs1 に注目する。 cs1 は値に触れず cs2 へと goto するだけである。 よって何もせずにそのまま goto する関数をコンストラクタ\verb/cs/ に渡すだけで良い。 最後に cs2 である。 cs2 はリスト~\ref{src:goto}では省略していたが、今回は計算を終了させる CodeSegment として定義する。 どの CodeSegment にも軽量継続せずに値を持ったまま計算を終了させる。 コンストラクタ \verb/cs/ には関数を与えなくては値を構成できないため、何もしない関数である id を渡している。 最後に計算をする cs0 へと軽量継続する main を定義する。 例として、 a の値を 100 とし、 b の値を50としている。 cs0, cs1, cs2, main をAgda で定義するとリスト~\ref{src:agda-css}のようになる。 \lstinputlisting[label=src:agda-css, caption= Agda における CodeSegment の定義] {src/CodeSegments.agda} 正しく計算が行なえたなら値150が得られるはずである。 % }}} % {{{ ノーマルレベル計算の実行 \section{ノーマルレベル計算の実行} プログラムを実行することは \verb/goto/ を定義することと同義である。 軽量継続\verb/goto/ の性質としては \begin{itemize} \item 次に実行する CodeSegment を指定する \item CodeSegment に渡すべき DataSegment を指定する \item 現在実行している CodeSegment から制御を指定されて CodeSegment へと移動させる \end{itemize} がある。 Agda における CodeSegment の本体は関数である。 関数をそのまま使用すると再帰を許してしまうために CbC との対応が失われてしまう。 よって、\verb/goto/を利用できるのは関数の末尾のみである、という制約を関数に付け加える必要がある。 この制約さえ満たせば、CodeSegment の実行は CodeSegment 型から関数本体を取り出し、レコード型を持つ値を適用することに相当する。 具体的に \verb/goto/ を関数として適用するとリスト~\ref{src:agda-goto}のようになる。 \lstinputlisting[label=src:agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda} この \verb/goto/ の定義を用いることで main などの関数が評価できるようになり、値150が得られる。 本文中での CodeSegment の定義は一部を抜粋している。 実行可能な Agda のソースコードは付録に載せる。% TODO: Appendix % }}} \section{MetaDataSegment の定義} \section{MetaCodeSegment の定義} \section{メタレベル計算の実行} \section{Agda を用いたContinuation based C の検証} \section{スタックの実装の検証}