Mercurial > hg > Papers > 2017 > atton-master

comparison paper/cbc-type.tex @ 83:c0199291c58e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add simple/sub type description
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 09 Feb 2017 12:56:22 +0900
parents 39a27b704f0c
children e437746d6038
comparison
equal deleted inserted replaced
82:39a27b704f0c 83:c0199291c58e
4 加えて、証明支援系言語 Agda を用いてデータの定義とそれを扱う関数の性質の証明が行なえることを確認した。 4 加えて、証明支援系言語 Agda を用いてデータの定義とそれを扱う関数の性質の証明が行なえることを確認した。
5 5
6 CbC で自身を証明するために依存型を利用したいが、CbC には専用の型システムが存在しない。 6 CbC で自身を証明するために依存型を利用したいが、CbC には専用の型システムが存在しない。
7 依存型をCbCコンパイラで扱うためにもまず現状の CbC を型付けする必要がある。 7 依存型をCbCコンパイラで扱うためにもまず現状の CbC を型付けする必要がある。
8 8
9 ~\ref{chapter:cbc-type}では CbC の型システムを部分型を利用して定義する。 9 ~\ref{chapter:cbc-type}では CbC の項が部分型で型付けできることを示す。
10 定義した型システムを用いて、Agda 上に DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、それらが型付けされることを確認する。 10 定義した型システムを用いて、Agda 上に DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、それらが型付けされることを確認する。
11 また、Agda 上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda で証明する。 11 また、Agda 上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda で証明する。
12
13 % {{{ 部分型付け
14
15 \section{部分型付け}
16 TODO: なおす
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 % }}}
287 12
288 % {{{ DataSegment の定義 13 % {{{ DataSegment の定義
289 \section{DataSegment の定義} 14 \section{DataSegment の定義}
290 まず DataSegment から定義していく。 15 まず DataSegment から定義していく。
291 DataSegment はレコード型で表現できるため、Agda のレコードをそのまま利用できる。 16 DataSegment はレコード型で表現できるため、Agda のレコードをそのまま利用できる。