Mercurial > hg > Papers > 2018 > nozomi-master
annotate paper/cbc-type.tex @ 81:3f63f697ed3a
Update
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 08 Feb 2017 17:37:08 +0900 |
| parents | 897fda8e39c5 |
| children | 39a27b704f0c |
| rev | line source |
|---|---|
| 57 | 1 \chapter{Agda における Continuation based C の表現} |
| 2 \label{chapter:cbc-type} | |
| 78 | 3 ~\ref{chapter:agda}章では Curry-Howard 同型対応により、型付きラムダ計算を用いて命題が証明できることを示した。 |
| 4 加えて、証明支援系言語 Agda を用いてデータの定義とそれを扱う関数の性質の証明が行なえることを確認した。 | |
| 5 | |
| 81 | 6 CbC で自身を証明するために依存型を利用したいが、CbC には専用の型システムが存在しない。 |
| 7 依存型を定義するためにもまず現状の CbC を型付けする必要がある。 | |
| 8 | |
| 78 | 9 この章では CbC の型システムを部分型を利用して定義する。 |
| 81 | 10 定義した型システムを用いて、Agda 上に DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、それらが型付けされることを確認する。 |
| 11 また、Agda 上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda で証明する。 | |
| 78 | 12 |
| 13 % {{{ 部分型付け | |
| 14 | |
| 15 \section{部分型付け} | |
| 81 | 16 TODO: なおす |
| 78 | 17 単純型付きラムダ計算では、ラムダ計算の項が型付けされることを確認した。 |
| 18 ここで、 単純型の拡張として、レコードを導入する。 | |
| 19 | |
| 20 レコードとは名前の付いた複数の値を保持するデータである。 | |
| 21 C 言語における構造体などがレコードに相当する。 | |
| 22 値を保持する各フィールド $ t_1 $ はあらかじめ定められた集合 L からラベル $ l_i$ を名前として持つ。 | |
| 23 例えば $ { x : Nat } $ や $ {no : 100, point 33}$ などがこれに相当する。 | |
| 24 なお、あるレコードの項や値に表れるラベルはすべて相異なるとする。 | |
| 25 レコードから値を取り出す際にはラベルを指定して値を射影する。 | |
| 26 | |
| 27 レコードの拡張の定義は以下である。 | |
| 28 | |
| 29 \begin{definition} | |
| 30 レコードの拡張に用いる新しい構文形式 | |
| 31 | |
| 32 \begin{align*} | |
| 33 t :: = ... && \text{項 :} \\ | |
| 34 \{l_i = t_i^{\; i \in 1 .. n}\} && \text{レコード} \\ | |
| 35 t.l && \text{射影} \\ | |
| 36 \end{align*} | |
| 37 | |
| 38 \begin{align*} | |
| 39 v :: = ... && \text{値 :} \\ | |
| 40 {l_i : v_i^{\; i \in 1..n}} && \text{レコードの値} | |
| 41 \end{align*} | |
| 42 | |
| 43 \begin{align*} | |
| 44 T :: = ... && \text{型 :} \\ | |
| 45 \{l_i : T_i^{\; i \in 1..n}\} && \text{レコードの型} | |
| 46 \end{align*} | |
| 47 \end{definition} | |
| 48 | |
| 49 \begin{definition} | |
| 50 レコードの拡張に用いる新しい評価規則 | |
| 51 | |
| 52 \begin{align*} | |
| 53 \{l_i = v_i^{\; i \in 1..n}.l_j \rightarrow v_j\} && \text{E-PROJRCD} \\ | |
| 54 \AxiomC{$t_1 \rightarrow t_1'$} | |
| 55 \UnaryInfC{$t_1.l \rightarrow t_1'.l$} | |
| 56 \DisplayProof && \text{E-PROJ} \\ | |
| 57 \AxiomC{$ t_j \rightarrow t_j'$} | |
| 58 \UnaryInfC{$ \{l_i = v_i^{i \in 1..j-1}, l_j = t_j, l_k = t_k^{k \in j+1 .. n}\} | |
| 59 \rightarrow | |
| 60 \{l_i = v_i^{i \in 1..j-1}, l_j = t_j', l_k = t_k^{k \in j+1 .. n}\} | |
| 61 $} | |
| 62 \DisplayProof && \text{E-RCD} \\ | |
| 63 \end{align*} | |
| 64 \end{definition} | |
| 65 | |
| 66 \begin{definition} | |
| 67 レコードの拡張に用いる新しい型付け規則 | |
| 68 | |
| 69 \begin{align*} | |
| 70 \AxiomC{各iに対して$ \Gamma \vdash t_i : T_i$} | |
| 71 \UnaryInfC{$ \Gamma \vdash \{ l_i = t_i^{\; i \in 1..n} : \{l_i : T_i^{\; i \in 1..n}\}$} | |
| 72 \DisplayProof && \text{T-RCD} \\ | |
| 73 \AxiomC{$ \Gamma \vdash t_1 : \{ l_i : T_i^{\; i \in 1.. n}\}$} | |
| 74 \UnaryInfC{$\Gamma \vdash t_1.lj : T_j$} | |
| 75 \DisplayProof && \text{T-PROJ} | |
| 76 \end{align*} | |
| 77 \end{definition} | |
| 78 | |
| 79 レコードを用いることで複数の値を一つの値としてまとめて扱うことができる。 | |
| 80 しかし、引数にレコードを取る場合、その型と完全に一致させる必要がある。 | |
| 81 例えば $ \{ x : Nat \} $ を引数に取る関数に対して $ \{ x : Nat , y : Bool\}$ といった値を適用することができない。 | |
| 82 しかし、直感的には関数の要求はフィールド $x $ が型 $Nat$を持つことのみであり、その部分にのみ注目すると$ \{ x : Nat , y : Bool\}$ も要求に沿っている。 | |
| 83 | |
| 84 部分型付けの目標は上記のような場合の項を許すように型付けを改良することにある。 | |
| 85 つまり型 $ S $ の任意の項が、型 $ T $ の項が期待される文脈において安全に利用できることを示す。 | |
| 86 この時、$ S $ を $ T $ の部分型と呼び、 $ S <: T $ と書く。 | |
| 87 これは型 $ S $ が型 $ T $よりも情報を多く持っていることを示しており、$S$は$T$の部分型である、と読む。 | |
| 88 $ S <: T $ の別の読み方として、型 $ T $ は型 $ S $ の上位型である、という読み方も存在する。 | |
| 89 | |
| 90 型付け関係と部分型関係をつなぐための新しい型付け規則を考える。 | |
| 91 | |
| 92 \begin{align*} | |
| 93 \AxiomC{$\Gamma \vdash t : S $} | |
| 94 \AxiomC{$ S <: T $} | |
| 95 \BinaryInfC{$ \Gamma \vdash t : T$} | |
| 96 \DisplayProof && \text {T-SUB} | |
| 97 \end{align*} | |
| 98 | |
| 99 この規則は $ S <: T $ ならば $ S $ 型の要素 $ t$はすべて $ T $の要素であると言っている。 | |
| 100 例えば、先程の $ \{ x : Nat \} $ と $ \{ x : Nat , y : Bool\}$ が $ \{ x : Nat , y : Bool\} <: \{ x : Nat \}$ となるように部分型関係を定義した時に $ \Gamma \vdash \{x=0, y=1\} : \{ x : Nat \}$ を導ける。 | |
| 101 | |
| 102 部分型関係は $ S <: T $ という形式の部分型付け式を導入するための推論規則の集まりとして定式化される。 | |
| 103 始めに、部分型付けの一般的な規定から考える。 | |
| 104 部分型は反射的であり、推移的である。 | |
| 105 | |
| 106 \begin{align*} | |
| 107 S <: S && \text{S-REFL} \\ | |
| 108 \AxiomC{$S <: U$} | |
| 109 \AxiomC{$U <: T$} | |
| 110 \BinaryInfC{$ S <: T $} | |
| 111 \DisplayProof && \text{S-TRANS} | |
| 112 \end{align*} | |
| 113 | |
| 114 これらの規則は安全代入に対する直感より正しい。 | |
| 115 次に、基本型や関数型、レコード型などの型それぞれに対して、その形の型の要素が期待される部分に対して上位型の要素を利用しても安全である、という規則を導入していく。 | |
| 116 | |
| 117 レコード型については型 $ T = \{ l_i : T_1 ... l_n : T_n\} $が持つフィールドが型 $ S = \{ k_1 : S_1 ... k_n : T_n\} $のものよりも少なければ $S$ を $T$の部分型とする。 | |
| 118 つまりレコードの終端フィールドのいくつかを忘れてしまっても安全である、ということを意味する。 | |
| 119 この直感は幅部分型付け規則となる。 | |
| 120 | |
| 121 \begin{align*} | |
| 122 \{l_i : T_i^{\; i \in 1..n+k} \} <: \{l_i : T_i^{\; i \in 1..n}\} | |
| 123 && \text{S-RCDWIDTH} | |
| 124 \end{align*} | |
| 125 | |
| 126 フィールドの多い方が部分型となるのは名前に反するように思える。 | |
| 127 しかし、フィールドが多いレコードほど制約が多くなり表すことのできる集合の範囲は小さくなる。 | |
| 128 集合の大きさで見ると明かにフィールドの多い方が小さいのである。 | |
| 129 | |
| 130 幅部分型付け規則が適用可能なのは、共通のフィールドの型が全く同じな場合のみである。 | |
| 131 しかし、その場合フィールドの型に部分型を導入できず、フィールドの型の扱いで同じ問題を抱えることとなる。 | |
| 132 そのために導入するのが深さ部分型付けである。 | |
| 133 二つのレコードの中で対応するフィールドの型が部分型付け関係にある時に個々のフィールドの型が異なることを許す。 | |
| 134 これは具体的には以下の規則となる。 | |
| 135 | |
| 136 \begin{align*} | |
| 137 \AxiomC{各iに対して $S_i <: T_i$} | |
| 138 \UnaryInfC{$\{ l_i : S_i^{\; i \in 1..n}\} <: \{l_i : T_i^{\; i \in 1..n}\}$} | |
| 139 \DisplayProof && \text{S-RCDDEPTH} | |
| 140 \end{align*} | |
| 141 | |
| 142 これらを用いて $ \{ x : \{a : Nat , b : Nat\}, y : \{m : Nat\}\}$ が $ \{x : \{ a : Nat\}, y : \{\}\}$の部分型であることは以下のように導出できる。 | |
| 143 | |
| 144 \begin{prooftree} | |
| 145 \AxiomC{} | |
| 146 \RightLabel{S-RCDWIDTH} | |
| 147 \UnaryInfC{$ \{a : Nat, b : Nat\} <: \{a : Nat\}$} | |
| 148 \AxiomC{} | |
| 149 \RightLabel{S-RCDWIDTH} | |
| 150 \UnaryInfC{$ \{m : Nat\} <: \{\}$} | |
| 151 \RightLabel{S-RCDDEPTH} | |
| 152 \BinaryInfC{$ \{ x : \{a : Nat , b : Nat\}, y : \{m : Nat\}\} <: \{x : \{ a : Nat\}, y : \{\}\}$} | |
| 153 \end{prooftree} | |
| 154 | |
| 155 最後に、レコードを利用する際はフィールドさえ揃っていれば順序は異なっても良いという規則を示す。 | |
| 156 | |
| 157 \begin{align*} | |
| 158 \AxiomC{$ \{ k_j : S_j^{\; i \in 1 .. n} \}$ は $ \{ l_i : T_i^{\; i \in 1 ..n}\} $ の並べ替えである} | |
| 159 \UnaryInfC{$ \{k_j : S_j^{\; j \in 1..n} \} <: \{l_i : T_i^{\; i \in 1..n }\}$} | |
| 160 \DisplayProof && \text{S-RCDPERM} | |
| 161 \end{align*} | |
| 162 | |
| 163 S-RCDPERM を用いることで、終端フィールドだけではなく任意の位置のフィールドを削ることができる。 | |
| 164 | |
| 165 レコードの部分型は定義できたので、次は関数の部分型を定義していく。 | |
| 166 関数の部分型は以下 S-ARROW として定義できる。 | |
| 167 | |
| 168 \begin{align*} | |
| 169 \AxiomC{$ T_1 <: S_1$} | |
| 170 \AxiomC{$ S_2 <: T_2$} | |
| 171 \BinaryInfC{$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $} | |
| 172 \DisplayProof && \text{S-ARROW} | |
| 173 \end{align*} | |
| 174 | |
| 175 前提の条件二つを見ると部分型の関係が逆転している。 | |
| 176 左側の条件は関数型自身の型と逆になっているため反変と言い、返り値の型は同じ向きであるため共変と言う。 | |
| 177 引数について考えた時、求める型よりも大きい型であれば明らかに安全に呼ぶことができるために関数の引数の型の方が上位型になる。 | |
| 178 返り値については関数が返す型が部分型であれば上位型を返すことができるため、関数の返り値の方が部分型になる。 | |
| 179 | |
| 180 別の見方をすると、型 $ S_1 \rightarrow S_2 $ の関数を別の型 $ T_1 \rightarrow T_2 $が期待される文脈で用いることが安全な時とは | |
| 181 | |
| 182 \begin{itemize} | |
| 183 \item 関数に渡される引数がその関数にとって想定外でない($ T_1 <: S_1$) | |
| 184 \item 関数が返す値も文脈にとって想定外でない($ S_2 <: T_2 $) | |
| 185 \end{itemize} | |
| 186 | |
| 187 という場合に限る。 | |
| 188 | |
| 189 % }}} | |
| 190 | |
| 191 % {{{ 部分型と Continuation based C | |
| 192 | |
| 193 \section{部分型と Continuation based C} | |
| 194 部分型を用いて Conituation based C の型システムを定義していく。 | |
| 195 | |
| 196 まず、DataSegment の型から定義してく。 | |
| 197 DataSegment 自体はCの構造体によって定義されているため、レコード型として考えることができる。 | |
| 198 例えばリスト~\ref{src:akasha-context}に示していた DataSegment の一つに注目する(リスト~\ref{src:type-ds})。 | |
| 199 | |
| 200 \lstinputlisting[label=src:type-ds, caption=akashaContext の DataSegment である AkashaInfo] {src/type-ds.h} | |
| 201 この AkashaInfo は $ \{ minHeight : unsigned\; int , maxHeight : unsigned \; int, akashaNode : AkashaNode*\}$ であると見なせる。 | |
| 202 CodeSegment は DataSegment を引数に取るため、DataSegment の型は CodeSegment が要求する最低限の制約をまとめたものと言える。 | |
| 203 | |
| 204 次に Meta DataSegment について考える。 | |
| 205 Meta DataSegment はプログラムに出現する DataSegment の共用体であった。 | |
| 206 これを DataSegment の構造体に変更する。 | |
| 207 こうすることにより、 Meta DataSegment はプログラム中に出現する DataSegment を必ず持つため、Meta DataSegment は任意の DataSegment の部分型となる。 | |
| 208 もしくは各 DataSegment の全てのフィールドを含むような1つの構造体でも良い。 | |
| 209 第~\ref{chapter:cbc-type}章における Meta DataSegment はそのように定義している。 | |
| 210 なお、GearsOSでは DataSegment の共用体をプログラムで必要な数だか持つ実装になっている。 | |
| 211 | |
| 212 具体的な CbC における Meta DataSegment であるContext (リスト~\ref{src:type-mds})は、 DataSegment の集合を値として持っているために明らかに DataSegment よりも多くの情報を持っている。 | |
| 213 \lstinputlisting[label=src:type-mds, caption=CbC の Meta DataSegment である Context] {src/type-mds.h} | |
| 214 | |
| 215 部分型として定義するなら以下のような定義となる。 | |
| 216 | |
| 217 \begin{definition} | |
| 218 Meta DataSegment の定義 | |
| 219 | |
| 220 \begin{align*} | |
| 221 Meta \; DataSegment <: DataSegment_i^{i \in N} && \text{S-MDS} | |
| 222 \end{align*} | |
| 223 \end{definition} | |
| 224 | |
| 225 なお、$N$はあるプログラムに出現するデータセグメントの名前の集合であるとする。 | |
| 226 | |
| 227 次に CodeSegment の型について考える。 | |
| 228 CodeSegment は DataSegment を DataSegment へと移す関数型とする。 | |
| 229 | |
| 230 \begin{definition} | |
| 231 CodeSegment の定義 | |
| 232 | |
| 233 \begin{align*} | |
| 234 DataSegment \rightarrow DataSegment && \text{T-CS} | |
| 235 \end{align*} | |
| 236 \end{definition} | |
| 237 | |
| 238 そして Meta CodeSegmentは Meta DataSegment を Meta DataSegment へと移す関数となる。 | |
| 239 | |
| 240 \begin{definition} | |
| 241 Meta CodeSegment の定義 | |
| 242 | |
| 243 \begin{align*} | |
| 244 Meta \; DataSegment \rightarrow Meta \; DataSegment && \text{T-MCS} | |
| 245 \end{align*} | |
| 246 \end{definition} | |
| 247 | |
| 248 ここで具体的なコード(リスト~\ref{src:type-cs})と比較してみる。 | |
| 249 | |
| 250 \lstinputlisting[label=src:type-cs, caption=具体的なCbCにおける CodeSegment] {src/type-cs.c} | |
| 251 | |
| 252 CodeSegment \verb/getMinHeight/ は DataSegment \verb/Allocate/ と \verb/AkashaInfo/ を引数に取っている。 | |
| 253 現状は \verb/Context/ も継続のために渡しているが、本来ノーマルレベルからはアクセスできないために隠れているとする。 | |
| 254 その場合、引数の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} $ となる。 | |
| 255 また、返り値は構文的には存在していないが、軽量継続で渡す値は $ Context $ である。 | |
| 256 よって \verb/getMinHeight/ の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} \rightarrow Context $ となる。 | |
| 257 $ Context $ の型は Meta DataSegment なので、 subtype の S-ARROW より $Context $の上位型への変更ができる。 | |
| 258 | |
| 259 $ \{ allocat; : Allocate , akashaInfo : AkahsaInfo\} $ を $X$と置いて、\verb/getMinHeignt/ を $ X \rightarrow X $ とする際の導出木は以下である。 | |
| 260 | |
| 261 \begin{prooftree} | |
| 262 \AxiomC{} | |
| 263 \RightLabel{S-REFL} | |
| 264 \UnaryInfC{$ X <: X $} | |
| 265 \AxiomC{} | |
| 266 \RightLabel{S-MDS} | |
| 267 \UnaryInfC{$ Conttext <: X$} | |
| 268 \RightLabel{S-ARROW} | |
| 269 \BinaryInfC{$ X \rightarrow Context <: X \rightarrow X$} | |
| 270 \end{prooftree} | |
| 271 | |
| 272 返り値部分を部分型として定義することにより、軽量継続先が上位型であればどの CodeSegment へと遷移しても良い。 | |
| 273 プログラムによっては遷移先は確定しているために部分型にする必要性は無いが、メタ計算やライブラリなどの遷移先が不定の場合は一度部分型として確定し、その後コンパイル時やランタイム時に包摂関係から具体型を導けば良い。 | |
| 274 例えばコンパイル時に解決すればライブラリの静的リンク時実行コード生成が行なえ、ランタイム時に解決すればネットワークを経由するプログラムとの接続初期化に利用できる。 | |
| 275 例えば、プロトコルがバージョンを持つ場合に接続先のプログラムが利用しているプロトコルと互換性があるかの判断を Context どうしの部分型関係で判断できる。 | |
| 276 | |
| 277 また、stub のみに注目すると、stub は Context から具体的なDataSegment X を取り出す操作に相当し、S-ARROWの左側の前提のような振舞いをする。 | |
| 278 加えて、軽量継続する際に X の計算結果を Context に格納してから goto する部分を別の Meta CodeSegment として分離すると、S-ARROWの右側の前提のような振舞いを行なう。 | |
| 279 このようにノーマルレベルの CodeSegment の先頭と末尾にメタ計算を接続することによってノーマルレベルの CodeSegment が型付けできる。 | |
| 280 型付けにDataSegment の集合としての Meta DataSegment が必須になるが、これは構造体として定義可能なためコンパイル時に生成することで CbC に組み込むことができる。 | |
| 281 | |
| 282 なお、メタ計算に利用する Meta DataSegment と Meta DataSegment も同様に型付けできる。 | |
| 283 ここで興味深いのはあるレベルの CodeSegment は同レベルの DataSegment において型付けされるが、一つ上の階層から見ると、下の階層のDataSegmentとして一貫して扱えることにある。 | |
| 284 このようにメタ計算を階層化することにより、メタ計算で拡張された計算に対しても他のメタ計算が容易に適用できる。 | |
| 285 | |
| 286 % }}} | |
| 58 | 287 |
| 59 | 288 % {{{ DataSegment の定義 |
| 58 | 289 \section{DataSegment の定義} |
| 290 まず DataSegment から定義していく。 | |
| 291 DataSegment はレコード型で表現できるため、Agda のレコードをそのまま利用できる。 | |
| 292 例えは~\ref{src:goto} に示していた a と b を加算して c を出力するプログラムに必要な DataSegment を記述すると~\ref{src:agda-ds}のようになる。 | |
| 293 cs0 は a と b の二つの Int 型の変数を利用するため、対応する ds0 は a と b のフィールドを持つ。 | |
| 294 cs1 は計算結果を格納する c という名前の変数のみを持つので、同様にds1もcのみを持つ。 | |
| 295 | |
| 296 \lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda} | |
| 59 | 297 % }}} |
| 58 | 298 |
| 59 | 299 % {{{ CodeSegment の定義 |
| 57 | 300 \section{CodeSegment の定義} |
| 58 | 301 次に CodeSegment を定義する。 |
| 302 CodeSegment は DataSegment を取って DataSegment を返すものである。 | |
| 303 よって $ I \rightarrow O $ を内包するデータ型を定義する。 | |
| 304 | |
| 305 レコード型の型は Set なので、Set 型を持つ変数 I と O を型変数に持ったデータ型 CodeSegment を定義する。 | |
| 306 I は Input DataSegment の型であり、 O は Output DataSegment である。 | |
| 307 | |
| 308 CodeSegment 型のコンストラクタには \verb/cs/ があり、Input DataSegment を取って Output DataSegment を返す関数を取る。 | |
| 309 具体的なデータ型の定義はリスト ~\ref{src:agda-cs} のようになる。 | |
| 310 | |
| 59 | 311 \lstinputlisting[label=src:agda-cs, caption= Agda における CodeSegment 型の定義] {src/CodeSegment.agda.replaced} |
| 58 | 312 |
| 313 この CodeSegment 型を用いて CodeSegment の処理本体を記述する。 | |
| 314 | |
| 315 まず計算の本体となる cs0 に注目する。 | |
| 316 cs0 は二つのInt型変数を持つ ds0 を取り、一つのInt型変数を作った上で cs1 に軽量継続を行なう。 | |
| 317 DataSegment はレコードなので、a と b のフィールドから値を取り出した上で加算を行ない、cを持つレコードを生成する。 | |
| 318 そのレコードを引き連れたまま cs1 へと goto する。 | |
| 319 | |
| 320 次に cs1 に注目する。 | |
| 321 cs1 は値に触れず cs2 へと goto するだけである。 | |
| 322 よって何もせずにそのまま goto する関数をコンストラクタ\verb/cs/ に渡すだけで良い。 | |
| 323 | |
| 324 最後に cs2 である。 | |
| 325 cs2 はリスト~\ref{src:goto}では省略していたが、今回は計算を終了させる CodeSegment として定義する。 | |
| 326 どの CodeSegment にも軽量継続せずに値を持ったまま計算を終了させる。 | |
| 327 コンストラクタ \verb/cs/ には関数を与えなくては値を構成できないため、何もしない関数である id を渡している。 | |
| 328 | |
| 329 最後に計算をする cs0 へと軽量継続する main を定義する。 | |
| 330 例として、 a の値を 100 とし、 b の値を50としている。 | |
| 59 | 331 |
| 332 cs0, cs1, cs2, main をAgda で定義するとリスト~\ref{src:agda-css}のようになる。 | |
| 333 | |
| 334 \lstinputlisting[label=src:agda-css, caption= Agda における CodeSegment の定義] {src/CodeSegments.agda} | |
| 335 | |
| 336 正しく計算が行なえたなら値150が得られるはずである。 | |
| 337 % }}} | |
| 58 | 338 |
| 60 | 339 % {{{ ノーマルレベル計算の実行 |
| 57 | 340 \section{ノーマルレベル計算の実行} |
| 71 | 341 \label{section:normal-level-exec} |
| 60 | 342 プログラムを実行することは \verb/goto/ を定義することと同義である。 |
| 343 軽量継続\verb/goto/ の性質としては | |
| 344 | |
| 345 \begin{itemize} | |
| 346 \item 次に実行する CodeSegment を指定する | |
| 347 \item CodeSegment に渡すべき DataSegment を指定する | |
|
61
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
348 \item 現在実行している CodeSegment から制御を指定された CodeSegment へと移動させる |
| 60 | 349 \end{itemize} |
| 350 | |
| 351 がある。 | |
| 352 Agda における CodeSegment の本体は関数である。 | |
| 353 関数をそのまま使用すると再帰を許してしまうために CbC との対応が失われてしまう。 | |
| 354 よって、\verb/goto/を利用できるのは関数の末尾のみである、という制約を関数に付け加える必要がある。 | |
| 355 | |
| 356 この制約さえ満たせば、CodeSegment の実行は CodeSegment 型から関数本体を取り出し、レコード型を持つ値を適用することに相当する。 | |
| 357 具体的に \verb/goto/ を関数として適用するとリスト~\ref{src:agda-goto}のようになる。 | |
| 358 | |
| 359 \lstinputlisting[label=src:agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda} | |
| 360 | |
| 361 この \verb/goto/ の定義を用いることで main などの関数が評価できるようになり、値150が得られる。 | |
| 362 本文中での CodeSegment の定義は一部を抜粋している。 | |
| 71 | 363 実行可能な Agda のソースコードは付録に載せる。 |
| 60 | 364 |
| 365 % }}} | |
| 366 | |
|
61
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
367 % {{{ Meta DataSegment の定義 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
368 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
369 \section{Meta DataSegment の定義} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
370 ノーマルレベルの CbC を Agda 上で記述し、実行することができた。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
371 次にメタレベルの計算を Agda 上で記述していく。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
372 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
373 Meta DataSegment はノーマルレベルの DataSegment の集合として定義できるものであり、全ての DataSegment の部分型であった。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
374 ノーマルレベルの DataSegment はプログラムによって変更されるので、事前に定義できるものではない。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
375 ここで、Agda の Parameterized Module を利用して、「Meta DataSegment の上位型は DataSegment である」のように DataSegment を定義する。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
376 こうすることにより、全てのプログラムは一つ以上の Meta DataSegment を持ち、任意の個数の DataSegment を持つ。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
377 また、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
|
378 階層構造でメタレベルを表現することにより、計算の拡張を自在に行なうことができる。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
379 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
380 具体的な Meta DataSegment の定義はリスト~\ref{src:agda-mds}のようになる。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
381 型システム \verb/subtype/ は、Meta DataSegment である \verb/Context/ を受けとることにより構築される。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
382 Context を Meta DataSegment とするプログラム上では DataSegment は Meta CodeSegment の上位型となる。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
383 その制約を \verb/DataSegment/ 型は表わしている。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
384 |
|
62
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
385 \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
|
386 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
387 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
388 ここで、関数を部分型に拡張する S-ARROW をもう一度示す。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
389 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
390 \begin{align*} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
391 \AxiomC{$ T_1 <: S_1$} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
392 \AxiomC{$ S_2 <: T_2$} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
393 \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
|
394 \DisplayProof && \text{S-ARROW} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
395 \end{align*} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
396 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
397 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
|
398 ここでの上位型は DataSegment であり、部分型は Meta DataSegment である。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
399 制約\verb/DataSegment/ の \verb/get/ は、 Meta DataSegment から DataSegment が生成できることを表す。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
400 これは前提 $ T_1 <: S_1 $ に相当する。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
401 そして、\verb/set/ は $ S_2 <: T_2 $ に相当する。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
402 しかし、任意の DataSegment が Meta DataSegment の部分型となるには、 DataSegment が Meta DataSegment よりも多くの情報を必ず持たなくてはならないが、これは通常では成り立たない。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
403 だが、メタ計算を行なう際には常に Meta DataSegment を一つ以上持っていると仮定するならば成り立つ。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
404 実際、GearsOS における赤黒木では Meta DataSegment に相当する \verb/Context/ を常に持ち歩いている。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
405 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
|
406 よって $ S_2 <: T_2 $ が成り立つ。 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
407 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
408 なお、 $ 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
|
409 |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
410 % }}} |
|
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
60
diff
changeset
|
411 |
|
62
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
412 % {{{ Meta CodeSegment の定義 |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
413 |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
414 \section{Meta CodeSegment の定義} |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
415 Meta DataSegment が定義できたので Meta CodeSegment を定義する。 |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
416 実際、DataSegment が Meta DataSegment に拡張できたため、Meta CodeSegment の定義には比較的変更は無い。 |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
417 ノーマルレベルの \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
|
418 |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
419 \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
|
420 |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
421 % }}} |
|
a40033d3e10f
Add Meta CodeSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
422 |
|
63
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
423 % {{{ メタレベル計算の実行 |
| 57 | 424 \section{メタレベル計算の実行} |
| 72 | 425 \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
|
426 Meta DataSegment と Meta CodeSegment の定義を行なったので、残るは実行である。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
427 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
428 実行はノーマルレベルにおいては軽量継続 \verb/goto/ を定義することによって表せた。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
429 メタレベル実行ではそれを Meta CodeSegment と Meta DataSegment を扱えるように拡張する。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
430 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
|
431 軽量継続 \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
|
432 行なっていることは 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
|
433 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
434 \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
|
435 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
436 実行例として、リスト~\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
|
437 実行する際に c の値を \verb/c'/ に保存してから加算ようなメタ計算を考える。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
438 c の値を \verb/c'/ に保存するタイミングは軽量継続時にユーザが指定する。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
439 よって軽量継続を行なうのと同等の情報を保持してなくてはならない。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
440 そのために 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
|
441 値を格納する \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
|
442 それらを踏まえた上での 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
|
443 なお、\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
|
444 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
445 \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
|
446 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
447 定義した \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
|
448 より構文が CbC に似るように \verb/gotoMeta/ を糖衣構文的に定義する。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
449 \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
|
450 結果的に \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
|
451 リスト~\ref{src:agda-mmcs} に示したプログラムでは、通常レベルのコードセグメントを全く変更せずにメタ計算を含む形に拡張している。 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
452 加算を行なう前の \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
|
453 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
454 \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
|
455 |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
456 なお、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
|
457 % TODO: cbc と agda の diff |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
458 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
459 CodeSegment や Meta CodeSegment などの定義が多かっため、どの処理やデータがどのレベルに属するか複雑になったため、一度図にてまとめる。 |
|
63
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
460 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
|
461 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
462 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
463 % TODO: メタの階層構造の図 |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
464 |
| 72 | 465 また、この節で取り扱ったソースコードは付録に付す。 |
| 466 | |
|
63
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
467 % }}} |
|
6d8825f3b051
Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
62
diff
changeset
|
468 |
| 65 | 469 % {{{ Agda を用いた Continuation based C の検証 |
| 470 | |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
471 \section{Agda を用いた Continuation based C の検証} |
| 72 | 472 \label{section:cbc-proof} |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
473 Agda において CbC の CodeSegment と DataSegment を定義することができた。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
474 実際の CbC のコードを Agda に変換し、それらの性質を証明していく。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
475 |
| 65 | 476 ここではGearsOS が持つ DataSegment \verb/SingleLinkedStack/ を証明していく。 |
| 477 この\verb/SingleLinkedStack/はポインタを利用した片方向リストを用いて実装されている。 | |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
478 |
| 65 | 479 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
|
480 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
481 \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
|
482 |
| 65 | 483 次に Agda における \verb/SingleLinkedStack/の定義について触れるが、Agda にはポインタが無いため、メモリ確保や\verb/NULL/の定義は存在しない。 |
| 484 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
|
485 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
486 \verb/Data.Maybe/ の \verb/maybe/ 型は、コンストラクタを二つ持つ。 |
| 65 | 487 片方のコンストラクタ \verb/just/ は値を持ったデータであり、ポインタの先に値があることに対応している。 |
| 488 一方のコンストラクタ \verb/nothing/ は値を持たない。 | |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
489 これは値が存在せず、ポインタの先が確保されていない(\verb/NULL/ ポインタである)ことを表現できる。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
490 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
491 \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
|
492 |
| 65 | 493 Maybe を用いて片方向リストを Agda 上に定義するとリスト~\ref{src:agda-stack}のようになる。 |
| 494 CbC とほぼ同様の定義ができている。 | |
| 495 CbC、 Agda 共に\verb/SingleLinkedStack/ は \verb/Element/ 型の \verb/top/ を持っている。 | |
| 496 \verb/Element/ 型は値と次の \verb/Element/ を持つ。 | |
| 497 CbC ではポインタで表現していた部分が Agda では Maybe で表現されているが、\verb/Element/ 型の持つ情報は変わっていない。 | |
| 498 | |
| 499 \lstinputlisting[label=src:agda-stack, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaStack.agda} | |
| 500 | |
| 501 Agda で片方向リストを利用する DataSegment の定義をリスト~\ref{src:agda-stack-ds}に示す。 | |
| 502 ノーマルレベルからアクセス可能な場所として \verb/Context/ に \verb/element/ フィールドを追加する。 | |
| 503 そしてノーマルレベルからアクセスできないよう分離した Meta Meta DataSegment である \verb/Meta/ にスタックの本体を格納する。 | |
| 504 CbC における実装では \verb/.../ で不定であった \verb/next/ も、agda ではメタレベルのコードセグメント \verb/nextCS/ となり、きちんと型付けされている。 | |
| 505 | |
| 74 | 506 \lstinputlisting[label=src:agda-stack-ds, caption=スタックを利用するための DataSegment の定義] {src/AgdaStackDS.agda} |
| 65 | 507 |
| 508 次にスタックへの操作に注目する。 | |
| 509 スタックへと値を積む \verb/pushSingleLinkedStack/ と値を取り出す \verb/popSingleLinkedStack/ の CbC 実装をリスト~\ref{src:cbc-push-pop}に示す。 | |
| 510 \verb/SingleLinkedStack/ は Meta CodeSegment であり、メタ計算を実行した後には通常の CodeSegment へと操作を移す。 | |
| 511 そのために \verb/next/ という名前で次のコードセグメントを保持している。 | |
| 512 具体的な \verb/next/ はコンパイル時にしか分からないため、\verb/.../ 構文を用いて不定としている。 | |
| 513 | |
| 514 \verb/pushSingleLinkedStack/ は \verb/element/ を新しく確保し、値を入れた後に \verb/next/ へと繋げ、 \verb/top/ を更新して軽量継続する。 | |
| 515 \verb/popSingleLinkedStack/ は先頭が空でなければ先頭の値を \verb/top/ から取得し、\verb/element/を一つ進める。 | |
| 516 値が空であれば \verb/data/ を \verb/NULL/ にしたまま軽量継続を行なう。 | |
| 517 | |
| 518 \lstinputlisting[label=src:cbc-push-pop, caption= CbC における SingleLinkedStack を操作する Meta CodeSegment] {src/singleLinkedStack.c} | |
| 519 | |
| 520 次に Agda における定義をリスト~\ref{src:agda-push-pop}に示す。 | |
| 521 同様に \verb/pushSingleLinkedStack/ と \verb/popSingleLinkedStack/ を定義している。 | |
| 522 \verb/pushsinglelinkedstack/ では、スタックの値を更新したのちにノーマルレベルの CodeSegment である \verb/n/ を \verb/exec/ している。 | |
| 523 なお、 \verb/liftMeta/ はノーマルレベルの計算をメタレベルとする関数である。 | |
| 524 | |
| 525 実際に値を追加する部分は where 句に定義された関数 \verb/push/ である。 | |
| 526 これはスタックへと積む値が空であれば追加を行なわず、値がある時は新たに element を作成して top を更新している。 | |
| 527 本来の CbC の実装では空かチェックはしていないが、値が空であるかに関わらずにスタックに積んでいるために挙動は同じである。 | |
| 528 | |
| 529 次に \verb/popSingleLinkedStack/ に注目する。 | |
| 530 こちらも操作後に \verb/nextCS/ へと継続を移すようになっている。 | |
| 531 | |
| 532 実際に値を取り出す操作はノーマルレベルからアクセスできる \verb/element/ の値の確定と、アクセスできない \verb/stack/ の更新である。 | |
| 533 | |
| 534 \verb/element/については、 \verb/top/ が空なら取り出した後の値は無いので \verb/element/ は \verb/nothing/ である。 | |
| 535 \verb/top/ が空でなければ \verb/element/ は \verb/top/ の値となる。 | |
| 536 | |
| 537 \verb/stack/ は空なら空のままであり、\verb/top/ に値があればその先頭を捨てる。 | |
| 538 ここで、\verb/pop/ の実装はスタックが空であっても、例外を送出したり停止したりせずに処理を続行できることが分かる。 | |
| 539 | |
| 540 \lstinputlisting[label=src:agda-push-pop, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaPushPop.agda} | |
| 541 | |
| 74 | 542 また、この章で取り上げた CbC と Agda の動作するソースコードは付録に載せる。 |
| 65 | 543 |
| 544 % }}} | |
| 545 | |
| 67 | 546 % {{{ スタックの実装の検証 |
| 66 | 547 \section{スタックの実装の検証} |
| 72 | 548 \label{section:stack-proof} |
| 66 | 549 定義した SingleLinkedStack に対して証明を行なっていく。 |
| 550 ここでの証明は SingleLinkedStack の処理が特定の性質を持つことを保証することである。 | |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
551 |
| 66 | 552 例えば |
| 553 | |
| 554 \begin{itemize} | |
| 555 \item スタックに積んだ値は取り出せる | |
| 556 \item 値は複数積むことができる | |
| 557 \item スタックから値を取り出すことができる | |
| 558 \item スタックから取り出す値は積んだ値である | |
| 559 \item スタックから値を取り出したらその値は無くなる | |
| 560 \item スタックに値を積んで取り出すとスタックの内容は変わらない | |
| 561 \end{itemize} | |
| 562 | |
| 563 といった多くの性質がある。 | |
| 564 | |
| 565 ここでは、最後に示した「スタックに値を積んで取り出すとスタックの内容は変わらない」ことについて示していく。 | |
| 566 この性質を具体的に書き下すと以下のようになる。 | |
| 567 | |
| 568 \begin{definition} | |
| 569 任意のスタック s に対して | |
| 570 | |
| 571 \begin{itemize} | |
| 572 \item 任意の値n | |
| 573 \item 値xを積む操作 push(x, s) | |
| 574 \item 値を一つスタックから取り出す操作 pop(s) | |
| 575 \end{itemize} | |
| 576 | |
| 577 がある時、 | |
| 578 | |
| 579 pop . push(n) s = s | |
| 580 | |
| 581 である。 | |
| 582 \end{definition} | |
| 583 | |
| 584 これを Agda 上で定義するとリスト~\ref{src:agda-push-pop-type-1} のようになる。 | |
| 585 Agda 上の定義ではスタックそのものではなく、スタックを含む任意の \verb/Meta/ に対してこの性質を証明する。 | |
| 586 この定義が \verb/Meta/ の値によらず成り立つことを、自然数の加算の交換法則と同様に等式変形を用いて証明していく。 | |
| 587 | |
| 588 \lstinputlisting[label=src:agda-push-pop-type-1, caption=Agda におけるスタックの性質の定義(1)] {src/PushPopType.agda.replaced} | |
| 589 | |
| 590 今回注目する条件分けは、スタック本体である \verb/stack/ と、push や pop を行なうための値を格納する \verb/element/ である。 | |
| 591 それぞれが持ち得る値を場合分けして考えていく。 | |
| 592 | |
| 593 \begin{itemize} | |
| 594 \item スタックが空である場合 | |
| 595 | |
| 596 \begin{itemize} | |
| 597 \item element が存在する場合 | |
| 598 | |
| 599 値が存在するため、 push は実行される。 | |
| 600 push が実行されたためスタックに値があるため、pop が成功する。 | |
| 601 pop が成功した結果スタックは空となるため元のスタックと同一となり成り立つ。 | |
| 602 | |
| 603 \item element が存在しない場合 | |
| 604 | |
| 605 値が存在しないため、 push が実行されない。 | |
| 606 push が実行されなかったため、スタックは空のままであり、pop も実行されない。 | |
| 607 結果スタックは空のままであり、元のスタックと一致する。 | |
| 608 \end{itemize} | |
| 609 | |
| 610 \item スタックが空でない場合 | |
| 611 | |
| 612 \begin{itemize} | |
| 613 \item element が存在する場合 | |
| 614 | |
| 615 element に設定された値 n が push され、スタックに一つ値が積まれる。 | |
| 616 スタックの先頭は n であるため、pop が実行されて n は無くなる。 | |
| 617 結果、スタックは実行する前の状態に戻る。 | |
| 618 | |
| 619 \item element が存在しない場合 | |
| 620 | |
| 621 element に値が存在しないため、push は実行されない。 | |
| 622 スタックは空ではないため、popが実行され、先頭の値が無くなる。 | |
| 623 実行後、スタックは一つ値を失なっているため、これは成りたたない。 | |
| 624 \end{itemize} | |
| 625 \end{itemize} | |
| 626 | |
| 627 スタックが空でなく、push する値が存在しないときにこの性質は成り立たないことが分かった。 | |
| 628 また、\verb/element/ が空でない制約を仮定に加えることでこの命題は成り立つようになる。 | |
| 629 | |
| 630 push 操作と pop 操作を連続して行なうとスタックが元に復元されることは分かった。 | |
| 631 ここで SingleLinkedStack よりも範囲を広げて \verb/Meta/ も復元されるかを考える。 | |
| 632 一見これも自明に成り立ちそうだが、push 操作と pop 操作は操作後に実行される CodeSegment を持っている。 | |
| 633 この CodeSegment は任意に設定できるため、\verb/Meta/ 内部の DataSegement が書き換えられる可能性がある。 | |
| 634 よってこれも制約無しでは成り立たない。 | |
| 635 | |
| 636 逆にいえば、CodeSegment を指定してしまえば \verb/Meta/ に関しても push/pop の影響を受けないことを保証できる。 | |
| 637 全く値を変更しない CodeSegment \verb/id/ を指定した際には自明にこの性質が導ける。 | |
| 638 実際、 Agda 上でも等式変形を明示的に指定せず、定義からの推論でこの証明を導ける(リスト~\ref{src:agda-push-pop-proof})。 | |
| 639 | |
| 640 なお、今回 SingleLinkedStack に積むことができる値は Agda の標準ライブラリ(\verb/Data.Nat/)における自然数型 $ \mathbb{N} $ としている。 | |
| 641 push/pop 操作の後の継続が \verb/Meta/ に影響を与えない制約は \verb/id-meta/ に表れている。 | |
| 642 これは \verb/Meta/ を構成する要素を受け取り、継続先の CodeSegment に恒等関数 \verb/id/ を指定している。 | |
| 643 加えて、スタックが空で無い制約 where 句の \verb/meta/ に表れている。 | |
| 644 必ずスタックの先頭 \verb/top/ には値xが入っており、それ以降の値は任意としている。 | |
| 645 よってスタックは必ず一つ以上の値を持ち、空でないという制約を表わせる。 | |
| 646 証明は refl によって与えられる。 | |
| 647 つまり定義から自明に推論可能となっている。 | |
| 648 | |
| 649 \lstinputlisting[label=src:agda-push-pop-proof, caption=Agdaにおけるスタックの性質の証明(1)] {src/AgdaPushPopProof.agda.replaced} | |
| 650 | |
| 651 ここで興味深い点は、 SingleLinkedStack の実装から証明に仮定が必要なことが証明途中でに分かった点にある。 | |
| 652 例えば、CbC の SingleLinkedStack 実装の push/pop 操作は失敗しても成功しても指定された CodeSegment に軽量継続する。 | |
| 653 この性質により、指定された CodeSegment によっては、スタックの操作に関係なく \verb/Meta/ の内部の DataSegemnt が書き換えられる可能性があることが分かった。 | |
| 654 スタックの操作の際に行なわれる軽量継続の利用方法は複数考えられる。 | |
| 655 例えば、スタックが空である際に pop を行なった時はエラー処理用の継続を行なう、といった実装も可能である。 | |
| 656 実装が異なれば、同様の性質でも証明は異なるものとなる。 | |
| 657 このように、実装そのものを適切に型システムで定義できれば、明示されていない実装依存の仕様も証明時に確定させることができる。 | |
| 658 | |
| 67 | 659 証明した定理をより一般的な「任意の自然数回だけスタックへ値を積み、その後同じ回数スタックから値を取り出すとスタックは操作前と変わらない」という形に拡張する。 |
| 660 この性質を Agda で定義するとリスト~\ref{src:agda-n-push-n-pop}のようになる。 | |
| 661 自然数n回だけ push/pop することを記述するために Agda 上に \verb/n-push/ 関数と \verb/n-pop/ 関数を定義している。 | |
| 662 それぞれ一度操作を行なった後に再帰的に自身を呼び出す再帰関数である。 | |
| 663 | |
| 664 \lstinputlisting[label=src:agda-n-push-n-pop, caption=Agda におけるスタックの性質の定義(2)] {src/AgdaNPushNPop.agda.replaced} | |
| 665 | |
| 666 この性質の証明は少々複雑である。 | |
| 667 結論から先に示すとリスト~\ref{src:agda-n-push-n-pop-proof}のように証明できる。 | |
| 668 | |
| 669 \lstinputlisting[label=src:agda-n-push-n-pop-proof, caption=Agda におけるスタックの性質の証明(2)] {src/AgdaNPushNPopProof.agda.replaced} | |
| 670 | |
| 671 これは以下のような形の証明になっている。 | |
| 672 | |
| 673 \begin{itemize} | |
| 674 \item 「n回pushした後にn回popしても同様になる」という定理を \verb/n-push-pop/ とおく。 | |
| 675 \item \verb/n-push-pop/ は自然数nと特定の \verb/Meta/ に対して \verb/exec (n-pop (suc n)) . (n-push (suc n))) m = m/ が成り立つことである | |
| 676 \item 特定の \verb/Meta/ とは、 push/pop 操作の後の継続が DataSegment を変更しない \verb/Meta/ である。 | |
| 677 \item また、簡略化のために \verb/csComp/ による CodeSegment の合成を二項演算子 \verb/./ とおく | |
| 678 \begin{itemize} | |
| 679 \item 例えば \verb/exec (csComp f g) x/ は \verb/exec (f . g) x/ となる。 | |
| 680 \end{itemize} | |
| 681 | |
| 682 \item \verb/n-push-pop/ を証明するための補題 \verb/pop-n-push/ を定義する | |
| 683 \item \verb/n-push-pop/ とは「n+1回push して1回 pop することは、n回pushすることと等しい」という補題である。 | |
| 684 \item \verb/n-push-pop/ は \verb/exec (pop . n-push (suc n)) m = exec (n-push n) m/ と表現できる。 | |
| 685 \item \verb/n-push-pop/ の n が zero の時は直ちに成り立つ。 | |
| 686 \item \verb/n-push-pop/ の n が zero でない時(suc n である時)は以下のように証明できる。 | |
| 687 | |
| 688 \begin{itemize} | |
| 689 \item \verb/exec (n-push (suc n)) m/ を \verb/X/ とおく | |
| 690 \item \verb/exec (pop . n-push (suc (suc n))) m = X/ | |
| 691 \item n-push の定義より \verb/exec (pop . (n-push (suc n) . push)) m = X/ | |
| 692 \item 補題 exec-comp より \verb/exec (pop (exec (n-push (suc n) . push) m)) = X/ | |
| 693 \item 補題 exec-comp より \verb/exec (pop (exec (n-push (suc n) (exec push m)))) = X/ | |
| 694 \item 一度pushした結果を \verb/m'/とおくと \verb/exec (pop (exec (n-push (suc n) m'))) = X/ | |
| 695 \item \verb/n-push-pop/ より \verb/exec (exec (n-push n m')) = X/ | |
| 696 \item push の定義より \verb/exec (exec (n-push n (exec push m))) = X/ | |
| 697 \item n-push の定義より \verb/exec (exec (n-push (suc n) m) = X/ となる | |
| 698 \item 全く同一の項に変更できたので証明終了 | |
| 699 \end{itemize} | |
| 700 | |
| 701 | |
| 702 \item 次に \verb/n-push-pop/ の証明を示す。 | |
| 703 \item \verb/n-push-pop/ の n が zero の時は、 \verb/suc zero/ 回の push/pop が行なわれるため、\verb/push-pop/より成り立つ。 | |
| 704 \item \verb/n-push-pop/ の n が zero でない時は以下により証明できる。 | |
| 705 | |
| 706 \begin{itemize} | |
| 707 \item \verb/exec ((n-pop (suc n)) . (n-push (suc n))) m = m / を示せれば良い。 | |
| 708 \item \verb/X/ に注目した時 n-pop の定義より \verb/exec (n-pop n) . pop . (n-push (suc n)) m = m/ | |
| 709 \item exec-comp より \verb/exec (n-pop n) (exec pop (n-push (suc n)) m) = m/ | |
| 710 \item exec-comp より \verb/exec (n-pop n) (exec pop (exec (n-push (suc n)) m)) = m/ | |
| 711 \item exec-comp より \verb/exec (n-pop n) (exec pop . (n-push (suc n)) m) = m/ | |
| 712 \item pop-n-push より \verb/exec (n-pop n) (exec (n-push n) m) = m/ | |
| 713 \item n-push-pop より \verb/m = m/ となり証明終了。 | |
| 714 \item なお、n-push-pop は (suc n) が n に減少するため、確実に停止することから自身を自身の証明に適用している。 | |
| 715 \end{itemize} | |
| 716 \end{itemize} | |
| 717 | |
| 718 push-pop を一般化した n-push-pop を証明することができた。 | |
| 719 n-push-pop は証明の途中で補題 pop-n-push と push-pop を利用した定理である。 | |
| 720 このように、CbC で記述されたプログラムを Agda 上に記述することで、データ構造の性質を定理として証明することができた。 | |
| 721 これらの証明機構を CbC のコンパイラやランタイム、モデルチェッカなどに組み込むことにより CbC は CbC で記述されたコードを証明することができるようになる。 | |
| 722 なお、本論文で取り扱っている Agda のソースコードは視認性の向上のために暗黙的な引数を省略して記述している。 | |
| 72 | 723 動作する完全なコードは付録に付す。 |
| 67 | 724 |
| 725 % }}} |