Mercurial > hg > Papers > 2017 > atton-master
annotate paper/cbc-type.tex @ 144:060202b21724 default tip
Bookbinding
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 27 Feb 2017 20:29:43 +0900 |
| parents | 5ad74fb83f72 |
| children |
| rev | line source |
|---|---|
| 110 | 1 \chapter{Agda による Continuation based C の表現} |
| 57 | 2 \label{chapter:cbc-type} |
| 78 | 3 ~\ref{chapter:agda}章では Curry-Howard 同型対応により、型付きラムダ計算を用いて命題が証明できることを示した。 |
| 4 加えて、証明支援系言語 Agda を用いてデータの定義とそれを扱う関数の性質の証明が行なえることを確認した。 | |
| 5 | |
| 81 | 6 CbC で自身を証明するために依存型を利用したいが、CbC には専用の型システムが存在しない。 |
| 82 | 7 依存型をCbCコンパイラで扱うためにもまず現状の CbC を型付けする必要がある。 |
| 81 | 8 |
| 110 | 9 ~\ref{chapter:cbc-type}章では CbC の項が部分型で型付けできることを示す。 |
| 81 | 10 定義した型システムを用いて、Agda 上に DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、それらが型付けされることを確認する。 |
| 11 また、Agda 上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda で証明する。 | |
| 78 | 12 |
| 59 | 13 % {{{ DataSegment の定義 |
| 58 | 14 \section{DataSegment の定義} |
| 15 まず DataSegment から定義していく。 | |
| 16 DataSegment はレコード型で表現できるため、Agda のレコードをそのまま利用できる。 | |
| 17 例えは~\ref{src:goto} に示していた a と b を加算して c を出力するプログラムに必要な DataSegment を記述すると~\ref{src:agda-ds}のようになる。 | |
| 18 cs0 は a と b の二つの Int 型の変数を利用するため、対応する ds0 は a と b のフィールドを持つ。 | |
| 19 cs1 は計算結果を格納する c という名前の変数のみを持つので、同様にds1もcのみを持つ。 | |
| 20 | |
| 86 | 21 \lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda.replaced} |
| 59 | 22 % }}} |
| 58 | 23 |
| 59 | 24 % {{{ CodeSegment の定義 |
| 57 | 25 \section{CodeSegment の定義} |
| 58 | 26 次に CodeSegment を定義する。 |
| 27 CodeSegment は DataSegment を取って DataSegment を返すものである。 | |
| 28 よって $ I \rightarrow O $ を内包するデータ型を定義する。 | |
| 29 | |
| 30 レコード型の型は Set なので、Set 型を持つ変数 I と O を型変数に持ったデータ型 CodeSegment を定義する。 | |
| 31 I は Input DataSegment の型であり、 O は Output DataSegment である。 | |
| 32 | |
| 33 CodeSegment 型のコンストラクタには \verb/cs/ があり、Input DataSegment を取って Output DataSegment を返す関数を取る。 | |
| 34 具体的なデータ型の定義はリスト ~\ref{src:agda-cs} のようになる。 | |
| 35 | |
| 59 | 36 \lstinputlisting[label=src:agda-cs, caption= Agda における CodeSegment 型の定義] {src/CodeSegment.agda.replaced} |
| 58 | 37 |
| 38 この CodeSegment 型を用いて CodeSegment の処理本体を記述する。 | |
| 39 | |
| 40 まず計算の本体となる cs0 に注目する。 | |
| 41 cs0 は二つのInt型変数を持つ ds0 を取り、一つのInt型変数を作った上で cs1 に軽量継続を行なう。 | |
| 42 DataSegment はレコードなので、a と b のフィールドから値を取り出した上で加算を行ない、cを持つレコードを生成する。 | |
| 43 そのレコードを引き連れたまま cs1 へと goto する。 | |
| 44 | |
| 45 次に cs1 に注目する。 | |
| 46 cs1 は値に触れず cs2 へと goto するだけである。 | |
| 47 よって何もせずにそのまま goto する関数をコンストラクタ\verb/cs/ に渡すだけで良い。 | |
| 48 | |
| 49 最後に cs2 である。 | |
| 50 cs2 はリスト~\ref{src:goto}では省略していたが、今回は計算を終了させる CodeSegment として定義する。 | |
| 51 どの CodeSegment にも軽量継続せずに値を持ったまま計算を終了させる。 | |
| 52 コンストラクタ \verb/cs/ には関数を与えなくては値を構成できないため、何もしない関数である id を渡している。 | |
| 53 | |
| 54 最後に計算をする cs0 へと軽量継続する main を定義する。 | |
| 55 例として、 a の値を 100 とし、 b の値を50としている。 | |
| 59 | 56 |
| 57 cs0, cs1, cs2, main をAgda で定義するとリスト~\ref{src:agda-css}のようになる。 | |
| 58 | |
| 86 | 59 \lstinputlisting[label=src:agda-css, caption= Agda における CodeSegment の定義] {src/CodeSegments.agda.replaced} |
| 59 | 60 |
| 61 正しく計算が行なえたなら値150が得られるはずである。 | |
| 62 % }}} | |
| 58 | 63 |
| 60 | 64 % {{{ ノーマルレベル計算の実行 |
| 57 | 65 \section{ノーマルレベル計算の実行} |
| 71 | 66 \label{section:normal-level-exec} |
| 60 | 67 プログラムを実行することは \verb/goto/ を定義することと同義である。 |
| 68 軽量継続\verb/goto/ の性質としては | |
| 69 | |
| 70 \begin{itemize} | |
| 71 \item 次に実行する CodeSegment を指定する | |
| 72 \item CodeSegment に渡すべき DataSegment を指定する | |
|
61
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
73 \item 現在実行している CodeSegment から制御を指定された CodeSegment へと移動させる |
| 60 | 74 \end{itemize} |
| 75 | |
| 76 がある。 | |
| 77 Agda における CodeSegment の本体は関数である。 | |
| 78 関数をそのまま使用すると再帰を許してしまうために CbC との対応が失われてしまう。 | |
| 79 よって、\verb/goto/を利用できるのは関数の末尾のみである、という制約を関数に付け加える必要がある。 | |
| 80 | |
| 81 この制約さえ満たせば、CodeSegment の実行は CodeSegment 型から関数本体を取り出し、レコード型を持つ値を適用することに相当する。 | |
| 82 具体的に \verb/goto/ を関数として適用するとリスト~\ref{src:agda-goto}のようになる。 | |
| 83 | |
| 86 | 84 \lstinputlisting[label=src:agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda.replaced} |
| 60 | 85 |
| 86 この \verb/goto/ の定義を用いることで main などの関数が評価できるようになり、値150が得られる。 | |
| 87 本文中での CodeSegment の定義は一部を抜粋している。 | |
| 71 | 88 実行可能な Agda のソースコードは付録に載せる。 |
| 60 | 89 |
| 90 % }}} | |
| 91 | |
|
61
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
92 % {{{ Meta DataSegment の定義 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
93 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
94 \section{Meta DataSegment の定義} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
95 ノーマルレベルの CbC を Agda 上で記述し、実行することができた。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
96 次にメタレベルの計算を Agda 上で記述していく。 |
|
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 はノーマルレベルの DataSegment の集合として定義できるものであり、全ての DataSegment の部分型であった。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
99 ノーマルレベルの DataSegment はプログラムによって変更されるので、事前に定義できるものではない。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
100 ここで、Agda の Parameterized Module を利用して、「Meta DataSegment の上位型は DataSegment である」のように DataSegment を定義する。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
101 こうすることにより、全てのプログラムは一つ以上の Meta DataSegment を持ち、任意の個数の DataSegment を持つ。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
102 また、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
|
103 階層構造でメタレベルを表現することにより、計算の拡張を自在に行なうことができる。 |
|
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 具体的な Meta DataSegment の定義はリスト~\ref{src:agda-mds}のようになる。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
106 型システム \verb/subtype/ は、Meta DataSegment である \verb/Context/ を受けとることにより構築される。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
107 Context を Meta DataSegment とするプログラム上では DataSegment は Meta CodeSegment の上位型となる。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
108 その制約を \verb/DataSegment/ 型は表わしている。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
109 |
|
62
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
110 \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
|
111 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
112 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
113 ここで、関数を部分型に拡張する S-ARROW をもう一度示す。 |
|
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 \begin{align*} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
116 \AxiomC{$ T_1 <: S_1$} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
117 \AxiomC{$ S_2 <: T_2$} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
118 \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
|
119 \DisplayProof && \text{S-ARROW} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
120 \end{align*} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
121 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
122 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
|
123 ここでの上位型は DataSegment であり、部分型は Meta DataSegment である。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
124 制約\verb/DataSegment/ の \verb/get/ は、 Meta DataSegment から DataSegment が生成できることを表す。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
125 これは前提 $ T_1 <: S_1 $ に相当する。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
126 そして、\verb/set/ は $ S_2 <: T_2 $ に相当する。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
127 しかし、任意の DataSegment が Meta DataSegment の部分型となるには、 DataSegment が Meta DataSegment よりも多くの情報を必ず持たなくてはならないが、これは通常では成り立たない。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
128 だが、メタ計算を行なう際には常に Meta DataSegment を一つ以上持っていると仮定するならば成り立つ。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
129 実際、GearsOS における赤黒木では Meta DataSegment に相当する \verb/Context/ を常に持ち歩いている。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
130 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
|
131 よって $ S_2 <: T_2 $ が成り立つ。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
132 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
133 なお、 $ 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
|
134 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
135 % }}} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
136 |
|
62
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
137 % {{{ Meta CodeSegment の定義 |
|
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 \section{Meta CodeSegment の定義} |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
140 Meta DataSegment が定義できたので Meta CodeSegment を定義する。 |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
141 実際、DataSegment が Meta DataSegment に拡張できたため、Meta CodeSegment の定義には比較的変更は無い。 |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
142 ノーマルレベルの \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
|
143 |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
144 \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
|
145 |
| 100 | 146 メタレベルの定義を部分型で行なって分かったことには以下のようなものがある。 |
| 147 | |
| 148 \begin{itemize} | |
| 149 \item メタ計算は階層構造化できる | |
| 150 | |
| 151 メタ計算は階層構造を取ることができるため、組み合わせることも可能である。 | |
| 152 | |
| 153 \item 継続先が不定の場合は型を一様に扱う必要がある | |
| 154 | |
| 155 メタ計算がノーマルレベルの具体的な型を知ることができるのはコンパイル時のみである。 | |
| 156 よってメタ計算を定義する時は部分型制約しか記述できない。 | |
| 157 逆に言えばノーマルレベル計算のみであれば部分型は解決され、レコード型で型付けができる。 | |
| 158 | |
| 159 \item \verb/stub/ は部分型付けにおいても必要である | |
| 160 | |
| 161 GearsOS では Meta DataSegment から DataSegment を取り出すための処理として \verb/stub/ が存在していた。 | |
| 162 これは Meta DataSegment で一様に扱っていた DataSegment に型を戻す処理として、型システムにおいても必要なものである。' | |
| 163 また、型システム経由で \verb/stub/ を生成することも可能であると考えられる。 | |
| 164 | |
| 165 \end{itemize} | |
| 166 | |
|
62
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
167 % }}} |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
168 |
|
63
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
169 % {{{ メタレベル計算の実行 |
| 57 | 170 \section{メタレベル計算の実行} |
| 72 | 171 \label{section:meta-level-exec} |
|
63
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
172 Meta DataSegment と Meta CodeSegment の定義を行なったので、残るは実行である。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
173 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
174 実行はノーマルレベルにおいては軽量継続 \verb/goto/ を定義することによって表せた。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
175 メタレベル実行ではそれを Meta CodeSegment と Meta DataSegment を扱えるように拡張する。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
176 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
|
177 軽量継続 \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
|
178 行なっていることは 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
|
179 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
180 \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
|
181 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
182 実行例として、リスト~\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
|
183 実行する際に c の値を \verb/c'/ に保存してから加算ようなメタ計算を考える。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
184 c の値を \verb/c'/ に保存するタイミングは軽量継続時にユーザが指定する。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
185 よって軽量継続を行なうのと同等の情報を保持してなくてはならない。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
186 そのために 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
|
187 値を格納する \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
|
188 それらを踏まえた上での 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
|
189 なお、\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
|
190 |
| 86 | 191 \lstinputlisting[label=src:agda-mmds, caption=Agda における Meta Meta DataSegment の定義例] {src/MetaMetaDataSegment.agda.replaced} |
|
63
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
192 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
193 定義した \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
|
194 より構文が CbC に似るように \verb/gotoMeta/ を糖衣構文的に定義する。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
195 \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
|
196 結果的に \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
|
197 リスト~\ref{src:agda-mmcs} に示したプログラムでは、通常レベルのコードセグメントを全く変更せずにメタ計算を含む形に拡張している。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
198 加算を行なう前の \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
|
199 |
| 86 | 200 \lstinputlisting[label=src:agda-mmcs, caption=Agda における Meta Meta CodeSegment の定義と実行例] {src/MetaMetaCodeSegment.agda.replaced} |
|
63
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
201 |
|
90
f535393e4043
Add figure meta-hierarchy
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
86
diff
changeset
|
202 CodeSegment や Meta CodeSegment などの定義が多かっため、どの処理やデータがどのレベルに属するか複雑になったため、一度図~\ref{fig:meta-hierarchy}にてまとめる。 |
|
63
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
203 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
|
204 |
|
90
f535393e4043
Add figure meta-hierarchy
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
86
diff
changeset
|
205 \begin{figure}[htbp] |
|
f535393e4043
Add figure meta-hierarchy
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
86
diff
changeset
|
206 \begin{center} |
| 91 | 207 \includegraphics[width=450pt]{fig/meta-hierarchy.pdf} |
| 94 | 208 \caption{メタの階層構造} |
| 209 \label{fig:meta-hierarchy} | |
|
90
f535393e4043
Add figure meta-hierarchy
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
86
diff
changeset
|
210 \end{center} |
|
f535393e4043
Add figure meta-hierarchy
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
86
diff
changeset
|
211 \end{figure} |
|
63
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
212 |
| 72 | 213 また、この節で取り扱ったソースコードは付録に付す。 |
| 214 | |
|
63
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
215 % }}} |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
216 |
| 99 | 217 % {{{ Agda を用いた Continuation based C の証明 |
| 65 | 218 |
| 99 | 219 \section{Agda を用いた Continuation based C の証明} |
| 72 | 220 \label{section:cbc-proof} |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
221 Agda において CbC の CodeSegment と DataSegment を定義することができた。 |
| 100 | 222 実際の CbC のコードを Agda で記述し、それらの性質を証明していく。 |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
223 |
| 65 | 224 ここではGearsOS が持つ DataSegment \verb/SingleLinkedStack/ を証明していく。 |
| 225 この\verb/SingleLinkedStack/はポインタを利用した片方向リストを用いて実装されている。 | |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
226 |
| 65 | 227 CbC における DataSegment \verb/SingleLinkedStack/ の定義はリスト~\ref{src:cbc-stack}のようになっている。 |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
228 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
229 \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
|
230 |
| 65 | 231 次に Agda における \verb/SingleLinkedStack/の定義について触れるが、Agda にはポインタが無いため、メモリ確保や\verb/NULL/の定義は存在しない。 |
| 232 CbC におけるメモリ確保部分はノーマルレベルには出現しないと仮定し、\verb/NULL/の表現にはAgda の標準ライブラリに存在する \verb/Data.Maybe/ を用いる。 | |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
233 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
234 \verb/Data.Maybe/ の \verb/maybe/ 型は、コンストラクタを二つ持つ。 |
| 65 | 235 片方のコンストラクタ \verb/just/ は値を持ったデータであり、ポインタの先に値があることに対応している。 |
| 236 一方のコンストラクタ \verb/nothing/ は値を持たない。 | |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
237 これは値が存在せず、ポインタの先が確保されていない(\verb/NULL/ ポインタである)ことを表現できる。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
238 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
239 \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
|
240 |
| 65 | 241 Maybe を用いて片方向リストを Agda 上に定義するとリスト~\ref{src:agda-stack}のようになる。 |
| 242 CbC とほぼ同様の定義ができている。 | |
| 243 CbC、 Agda 共に\verb/SingleLinkedStack/ は \verb/Element/ 型の \verb/top/ を持っている。 | |
| 244 \verb/Element/ 型は値と次の \verb/Element/ を持つ。 | |
| 245 CbC ではポインタで表現していた部分が Agda では Maybe で表現されているが、\verb/Element/ 型の持つ情報は変わっていない。 | |
| 246 | |
| 86 | 247 \lstinputlisting[label=src:agda-stack, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaStack.agda.replaced} |
| 65 | 248 |
| 249 Agda で片方向リストを利用する DataSegment の定義をリスト~\ref{src:agda-stack-ds}に示す。 | |
| 250 ノーマルレベルからアクセス可能な場所として \verb/Context/ に \verb/element/ フィールドを追加する。 | |
| 251 そしてノーマルレベルからアクセスできないよう分離した Meta Meta DataSegment である \verb/Meta/ にスタックの本体を格納する。 | |
| 252 CbC における実装では \verb/.../ で不定であった \verb/next/ も、agda ではメタレベルのコードセグメント \verb/nextCS/ となり、きちんと型付けされている。 | |
| 253 | |
| 86 | 254 \lstinputlisting[label=src:agda-stack-ds, caption=スタックを利用するための DataSegment の定義] {src/AgdaStackDS.agda.replaced} |
| 65 | 255 |
| 256 次にスタックへの操作に注目する。 | |
| 257 スタックへと値を積む \verb/pushSingleLinkedStack/ と値を取り出す \verb/popSingleLinkedStack/ の CbC 実装をリスト~\ref{src:cbc-push-pop}に示す。 | |
| 258 \verb/SingleLinkedStack/ は Meta CodeSegment であり、メタ計算を実行した後には通常の CodeSegment へと操作を移す。 | |
| 259 そのために \verb/next/ という名前で次のコードセグメントを保持している。 | |
| 260 具体的な \verb/next/ はコンパイル時にしか分からないため、\verb/.../ 構文を用いて不定としている。 | |
| 261 | |
| 262 \verb/pushSingleLinkedStack/ は \verb/element/ を新しく確保し、値を入れた後に \verb/next/ へと繋げ、 \verb/top/ を更新して軽量継続する。 | |
| 263 \verb/popSingleLinkedStack/ は先頭が空でなければ先頭の値を \verb/top/ から取得し、\verb/element/を一つ進める。 | |
| 264 値が空であれば \verb/data/ を \verb/NULL/ にしたまま軽量継続を行なう。 | |
| 265 | |
| 266 \lstinputlisting[label=src:cbc-push-pop, caption= CbC における SingleLinkedStack を操作する Meta CodeSegment] {src/singleLinkedStack.c} | |
| 267 | |
| 268 次に Agda における定義をリスト~\ref{src:agda-push-pop}に示す。 | |
| 269 同様に \verb/pushSingleLinkedStack/ と \verb/popSingleLinkedStack/ を定義している。 | |
| 270 \verb/pushsinglelinkedstack/ では、スタックの値を更新したのちにノーマルレベルの CodeSegment である \verb/n/ を \verb/exec/ している。 | |
| 271 なお、 \verb/liftMeta/ はノーマルレベルの計算をメタレベルとする関数である。 | |
| 272 | |
| 273 実際に値を追加する部分は where 句に定義された関数 \verb/push/ である。 | |
| 274 これはスタックへと積む値が空であれば追加を行なわず、値がある時は新たに element を作成して top を更新している。 | |
| 275 本来の CbC の実装では空かチェックはしていないが、値が空であるかに関わらずにスタックに積んでいるために挙動は同じである。 | |
| 276 | |
| 277 次に \verb/popSingleLinkedStack/ に注目する。 | |
| 278 こちらも操作後に \verb/nextCS/ へと継続を移すようになっている。 | |
| 279 | |
| 280 実際に値を取り出す操作はノーマルレベルからアクセスできる \verb/element/ の値の確定と、アクセスできない \verb/stack/ の更新である。 | |
| 281 | |
| 282 \verb/element/については、 \verb/top/ が空なら取り出した後の値は無いので \verb/element/ は \verb/nothing/ である。 | |
| 283 \verb/top/ が空でなければ \verb/element/ は \verb/top/ の値となる。 | |
| 284 | |
| 285 \verb/stack/ は空なら空のままであり、\verb/top/ に値があればその先頭を捨てる。 | |
| 286 ここで、\verb/pop/ の実装はスタックが空であっても、例外を送出したり停止したりせずに処理を続行できることが分かる。 | |
| 287 | |
| 86 | 288 \lstinputlisting[label=src:agda-push-pop, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaPushPop.agda.replaced} |
| 65 | 289 |
| 74 | 290 また、この章で取り上げた CbC と Agda の動作するソースコードは付録に載せる。 |
| 65 | 291 |
| 292 % }}} | |
| 293 | |
| 99 | 294 % {{{ スタックの実装の証明 |
| 295 \section{スタックの実装の証明} | |
| 72 | 296 \label{section:stack-proof} |
| 66 | 297 定義した SingleLinkedStack に対して証明を行なっていく。 |
| 298 ここでの証明は SingleLinkedStack の処理が特定の性質を持つことを保証することである。 | |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
299 |
| 66 | 300 例えば |
| 301 | |
| 302 \begin{itemize} | |
| 303 \item スタックに積んだ値は取り出せる | |
| 304 \item 値は複数積むことができる | |
| 305 \item スタックから値を取り出すことができる | |
| 306 \item スタックから取り出す値は積んだ値である | |
| 307 \item スタックから値を取り出したらその値は無くなる | |
| 308 \item スタックに値を積んで取り出すとスタックの内容は変わらない | |
| 309 \end{itemize} | |
| 310 | |
| 311 といった多くの性質がある。 | |
| 312 | |
| 313 ここでは、最後に示した「スタックに値を積んで取り出すとスタックの内容は変わらない」ことについて示していく。 | |
| 314 この性質を具体的に書き下すと以下のようになる。 | |
| 315 | |
| 316 \begin{definition} | |
| 317 任意のスタック s に対して | |
| 318 | |
| 319 \begin{itemize} | |
| 320 \item 任意の値n | |
| 321 \item 値xを積む操作 push(x, s) | |
| 322 \item 値を一つスタックから取り出す操作 pop(s) | |
| 323 \end{itemize} | |
| 324 | |
| 325 がある時、 | |
| 326 | |
| 327 pop . push(n) s = s | |
| 328 | |
| 329 である。 | |
| 330 \end{definition} | |
| 331 | |
| 332 これを Agda 上で定義するとリスト~\ref{src:agda-push-pop-type-1} のようになる。 | |
| 333 Agda 上の定義ではスタックそのものではなく、スタックを含む任意の \verb/Meta/ に対してこの性質を証明する。 | |
| 334 この定義が \verb/Meta/ の値によらず成り立つことを、自然数の加算の交換法則と同様に等式変形を用いて証明していく。 | |
| 335 | |
| 336 \lstinputlisting[label=src:agda-push-pop-type-1, caption=Agda におけるスタックの性質の定義(1)] {src/PushPopType.agda.replaced} | |
| 337 | |
| 338 今回注目する条件分けは、スタック本体である \verb/stack/ と、push や pop を行なうための値を格納する \verb/element/ である。 | |
| 339 それぞれが持ち得る値を場合分けして考えていく。 | |
| 340 | |
| 341 \begin{itemize} | |
| 342 \item スタックが空である場合 | |
| 343 | |
| 344 \begin{itemize} | |
| 345 \item element が存在する場合 | |
| 346 | |
| 347 値が存在するため、 push は実行される。 | |
| 348 push が実行されたためスタックに値があるため、pop が成功する。 | |
| 349 pop が成功した結果スタックは空となるため元のスタックと同一となり成り立つ。 | |
| 350 | |
| 351 \item element が存在しない場合 | |
| 352 | |
| 353 値が存在しないため、 push が実行されない。 | |
| 354 push が実行されなかったため、スタックは空のままであり、pop も実行されない。 | |
| 355 結果スタックは空のままであり、元のスタックと一致する。 | |
| 356 \end{itemize} | |
| 357 | |
| 358 \item スタックが空でない場合 | |
| 359 | |
| 360 \begin{itemize} | |
| 361 \item element が存在する場合 | |
| 362 | |
| 363 element に設定された値 n が push され、スタックに一つ値が積まれる。 | |
| 364 スタックの先頭は n であるため、pop が実行されて n は無くなる。 | |
| 365 結果、スタックは実行する前の状態に戻る。 | |
| 366 | |
| 367 \item element が存在しない場合 | |
| 368 | |
| 369 element に値が存在しないため、push は実行されない。 | |
| 370 スタックは空ではないため、popが実行され、先頭の値が無くなる。 | |
| 371 実行後、スタックは一つ値を失なっているため、これは成りたたない。 | |
| 372 \end{itemize} | |
| 373 \end{itemize} | |
| 374 | |
| 375 スタックが空でなく、push する値が存在しないときにこの性質は成り立たないことが分かった。 | |
| 376 また、\verb/element/ が空でない制約を仮定に加えることでこの命題は成り立つようになる。 | |
| 377 | |
| 378 push 操作と pop 操作を連続して行なうとスタックが元に復元されることは分かった。 | |
| 379 ここで SingleLinkedStack よりも範囲を広げて \verb/Meta/ も復元されるかを考える。 | |
| 380 一見これも自明に成り立ちそうだが、push 操作と pop 操作は操作後に実行される CodeSegment を持っている。 | |
| 381 この CodeSegment は任意に設定できるため、\verb/Meta/ 内部の DataSegement が書き換えられる可能性がある。 | |
| 382 よってこれも制約無しでは成り立たない。 | |
| 383 | |
| 384 逆にいえば、CodeSegment を指定してしまえば \verb/Meta/ に関しても push/pop の影響を受けないことを保証できる。 | |
| 385 全く値を変更しない CodeSegment \verb/id/ を指定した際には自明にこの性質が導ける。 | |
| 386 実際、 Agda 上でも等式変形を明示的に指定せず、定義からの推論でこの証明を導ける(リスト~\ref{src:agda-push-pop-proof})。 | |
| 387 | |
| 99 | 388 なお、今回 SingleLinkedStack に積むことができる値は Agda の標準ライブラリの(\verb/Data.Nat/)モジュールにおける自然数型 $ \mathbb{N} $ としている。 |
| 389 これはスタックを利用する際に具体的な値があると証明に有用であるからである。 | |
| 66 | 390 push/pop 操作の後の継続が \verb/Meta/ に影響を与えない制約は \verb/id-meta/ に表れている。 |
| 391 これは \verb/Meta/ を構成する要素を受け取り、継続先の CodeSegment に恒等関数 \verb/id/ を指定している。 | |
| 392 加えて、スタックが空で無い制約 where 句の \verb/meta/ に表れている。 | |
| 393 必ずスタックの先頭 \verb/top/ には値xが入っており、それ以降の値は任意としている。 | |
| 394 よってスタックは必ず一つ以上の値を持ち、空でないという制約を表わせる。 | |
| 395 証明は refl によって与えられる。 | |
| 396 つまり定義から自明に推論可能となっている。 | |
| 397 | |
| 398 \lstinputlisting[label=src:agda-push-pop-proof, caption=Agdaにおけるスタックの性質の証明(1)] {src/AgdaPushPopProof.agda.replaced} | |
| 399 | |
| 400 ここで興味深い点は、 SingleLinkedStack の実装から証明に仮定が必要なことが証明途中でに分かった点にある。 | |
| 401 例えば、CbC の SingleLinkedStack 実装の push/pop 操作は失敗しても成功しても指定された CodeSegment に軽量継続する。 | |
| 402 この性質により、指定された CodeSegment によっては、スタックの操作に関係なく \verb/Meta/ の内部の DataSegemnt が書き換えられる可能性があることが分かった。 | |
| 403 スタックの操作の際に行なわれる軽量継続の利用方法は複数考えられる。 | |
| 404 例えば、スタックが空である際に pop を行なった時はエラー処理用の継続を行なう、といった実装も可能である。 | |
| 405 実装が異なれば、同様の性質でも証明は異なるものとなる。 | |
| 406 このように、実装そのものを適切に型システムで定義できれば、明示されていない実装依存の仕様も証明時に確定させることができる。 | |
| 407 | |
| 67 | 408 証明した定理をより一般的な「任意の自然数回だけスタックへ値を積み、その後同じ回数スタックから値を取り出すとスタックは操作前と変わらない」という形に拡張する。 |
| 409 この性質を Agda で定義するとリスト~\ref{src:agda-n-push-n-pop}のようになる。 | |
| 410 自然数n回だけ push/pop することを記述するために Agda 上に \verb/n-push/ 関数と \verb/n-pop/ 関数を定義している。 | |
| 411 それぞれ一度操作を行なった後に再帰的に自身を呼び出す再帰関数である。 | |
| 412 | |
| 413 \lstinputlisting[label=src:agda-n-push-n-pop, caption=Agda におけるスタックの性質の定義(2)] {src/AgdaNPushNPop.agda.replaced} | |
| 414 | |
| 415 この性質の証明は少々複雑である。 | |
| 416 結論から先に示すとリスト~\ref{src:agda-n-push-n-pop-proof}のように証明できる。 | |
| 417 | |
| 418 \lstinputlisting[label=src:agda-n-push-n-pop-proof, caption=Agda におけるスタックの性質の証明(2)] {src/AgdaNPushNPopProof.agda.replaced} | |
| 419 | |
| 420 これは以下のような形の証明になっている。 | |
| 421 | |
| 422 \begin{itemize} | |
| 423 \item 「n回pushした後にn回popしても同様になる」という定理を \verb/n-push-pop/ とおく。 | |
| 99 | 424 \item \verb/n-push-pop/ は自然数nと特定の \verb/Meta/ に対して \\ |
| 425 \verb/exec (n-pop (suc n)) . (n-push (suc n))) m = m/ が成り立つことである | |
| 67 | 426 \item 特定の \verb/Meta/ とは、 push/pop 操作の後の継続が DataSegment を変更しない \verb/Meta/ である。 |
| 427 \item また、簡略化のために \verb/csComp/ による CodeSegment の合成を二項演算子 \verb/./ とおく | |
| 428 \begin{itemize} | |
| 429 \item 例えば \verb/exec (csComp f g) x/ は \verb/exec (f . g) x/ となる。 | |
| 430 \end{itemize} | |
| 431 | |
| 432 \item \verb/n-push-pop/ を証明するための補題 \verb/pop-n-push/ を定義する | |
| 433 \item \verb/n-push-pop/ とは「n+1回push して1回 pop することは、n回pushすることと等しい」という補題である。 | |
| 434 \item \verb/n-push-pop/ は \verb/exec (pop . n-push (suc n)) m = exec (n-push n) m/ と表現できる。 | |
| 435 \item \verb/n-push-pop/ の n が zero の時は直ちに成り立つ。 | |
| 436 \item \verb/n-push-pop/ の n が zero でない時(suc n である時)は以下のように証明できる。 | |
| 437 | |
| 438 \begin{itemize} | |
| 439 \item \verb/exec (n-push (suc n)) m/ を \verb/X/ とおく | |
| 440 \item \verb/exec (pop . n-push (suc (suc n))) m = X/ | |
| 441 \item n-push の定義より \verb/exec (pop . (n-push (suc n) . push)) m = X/ | |
| 442 \item 補題 exec-comp より \verb/exec (pop (exec (n-push (suc n) . push) m)) = X/ | |
| 443 \item 補題 exec-comp より \verb/exec (pop (exec (n-push (suc n) (exec push m)))) = X/ | |
| 444 \item 一度pushした結果を \verb/m'/とおくと \verb/exec (pop (exec (n-push (suc n) m'))) = X/ | |
| 445 \item \verb/n-push-pop/ より \verb/exec (exec (n-push n m')) = X/ | |
| 446 \item push の定義より \verb/exec (exec (n-push n (exec push m))) = X/ | |
| 447 \item n-push の定義より \verb/exec (exec (n-push (suc n) m) = X/ となる | |
| 448 \item 全く同一の項に変更できたので証明終了 | |
| 449 \end{itemize} | |
| 450 | |
| 451 | |
| 452 \item 次に \verb/n-push-pop/ の証明を示す。 | |
| 453 \item \verb/n-push-pop/ の n が zero の時は、 \verb/suc zero/ 回の push/pop が行なわれるため、\verb/push-pop/より成り立つ。 | |
| 454 \item \verb/n-push-pop/ の n が zero でない時は以下により証明できる。 | |
| 455 | |
| 456 \begin{itemize} | |
| 457 \item \verb/exec ((n-pop (suc n)) . (n-push (suc n))) m = m / を示せれば良い。 | |
| 458 \item \verb/X/ に注目した時 n-pop の定義より \verb/exec (n-pop n) . pop . (n-push (suc n)) m = m/ | |
| 459 \item exec-comp より \verb/exec (n-pop n) (exec pop (n-push (suc n)) m) = m/ | |
| 460 \item exec-comp より \verb/exec (n-pop n) (exec pop (exec (n-push (suc n)) m)) = m/ | |
| 461 \item exec-comp より \verb/exec (n-pop n) (exec pop . (n-push (suc n)) m) = m/ | |
| 462 \item pop-n-push より \verb/exec (n-pop n) (exec (n-push n) m) = m/ | |
| 463 \item n-push-pop より \verb/m = m/ となり証明終了。 | |
| 464 \item なお、n-push-pop は (suc n) が n に減少するため、確実に停止することから自身を自身の証明に適用している。 | |
| 465 \end{itemize} | |
| 466 \end{itemize} | |
| 467 | |
| 468 push-pop を一般化した n-push-pop を証明することができた。 | |
| 469 n-push-pop は証明の途中で補題 pop-n-push と push-pop を利用した定理である。 | |
| 470 このように、CbC で記述されたプログラムを Agda 上に記述することで、データ構造の性質を定理として証明することができた。 | |
| 471 これらの証明機構を CbC のコンパイラやランタイム、モデルチェッカなどに組み込むことにより CbC は CbC で記述されたコードを証明することができるようになる。 | |
| 100 | 472 なお、本論文で取り扱っている Agda のソースコードは可読性の向上のために暗黙的な引数を省略している。 |
| 473 完全なコードは付録に付す。 | |
| 67 | 474 |
| 475 % }}} | |
| 100 | 476 |