部分構造的型システム
普通の型システムは順番だったり使われる回数だったりを制限できない ファイルなどのリソースアクセスで問題になってくる
部分構造的型システム (Substructural Type System) なるものを導入してどうにかする Structural properties
ふつうのλ計算は文脈内の変数を何回でも使える → Structural Property
勝手に文脈の順番を入れ替えたり(exchange)、追加したり(weakening)、同じ型の変数をまとめたり(contraction)できる
contraction: $ \Gamma_1, x_2:T_1, x_3:T_1, \Gamma_2 \vdash t: T_2 ならば $ \Gamma_1, x_1:T_1, \Gamma_2 \vdash t: [x_1/x_2][x_1/x_3]T_2
Substructural type system
Structural propertiesのうち一つ以上が成立しないようなもののこと
線形型システム (Linear-): weakeningとcontractionができない すべての変数をちょうど1回使う
アフィン型システム (Affine- ): contractionができない
すべての変数をたかだか1回使う
関連型システム? (Relevant-): weakeningができない
全ての変数を少なくとも1回使う
なんて訳すんだろう
順序付き型システム? (Ordered-): 全て使えない
全ての変数をちょうど1回使い、その使用順も制限される
こうしてみると使える規則で束をなしているように見える
そうだね