これは型 Advent Calendar 2019 15日目の記事です．交差型についてのよく知られた事実——交差型を持つ単純型付きλ計算において，強正規化する項は型付け可能であることを解説します．

はじめに

交差型 $T_{1} \land T_{2}$ とは，読んで字のごとく型 $T_{1}$ と型 $T_{2}$ の共通部分を表す型です．すなわち，型 $T_{1} \land T_{2}$ を持つ項e（つまり $e : T_{1} \land T_{2}$ ）とは，型 $T_{1}$ を持ち（ $e : T_{1}$ ），なおかつ型 $T_{2}$ も持つ項（ $e : T_{2}$ ）を指します．交差型のある体系では，SMLの+のようなアドホックな多相性¹を $(int \to int \to int) \land (real \to real \to real)$ のように表現できる嬉しさが知られています．しかし，真にヤバい点と言えば後述する性質でしょう．

交差型を含むある種の言語——交差型を持つ単純型付きλ計算——において，任意の項の型付け可能性と強正規化性は一致することが知られています．確かに左の性質から右の性質は導けそうです．単純型付きλ計算，System F，CoC等々，多くの言語において，型付けできる項は強正規化する²ことが知られています．しかし右——ある項が強正規化すること——から左——その項が型付け可能であること——も導けるとはどういう事でしょう？もうそれを聞いただけでヤバそうです．与えられた項が型付け可能かどうか判定するプログラムが存在すれば停止性問題が解けてしまうので，無制限に交差型を入れてしまうと型推論が決定不能になってしまいます．³

この記事ではその右から左への性質，すなわち交差型を持つ単純型付きλ計算において，強正規化する項は型付け可能であることをふわっと解説します．左から右への性質，型付け可能な項は強正規化する事については，論理関係（logical relation）を使えば単純型付きλ計算の時と同じノリで証明できるので割愛します．

性質が成り立つ直感

この性質が成り立つ直感を得るには，この論文による証明を追うのが良いでしょう．この論文では，肝心の定理は大きく分けて以下の二つの性質から証明しています．

正規形が型付け可能であること
主部展開定理（subject expansion）

正規形が型付け可能であること

交差型を持つ単純型付きλ計算においては，全ての正規形——これ以上簡約できない項——は適当な型環境を持って来れば型を付けられます．

これは明らかに単純型付きλ計算では成り立たなかった性質です．例えば，正規形 $λ x . x x$ に型を付けられるかどうか考えてみましょう．この項に型を付けようと思うと，引数 $x$ の型 $X$ は，型 $X$ の値を受け取って適当な型 $A$ の値を返す関数の型 $X \to A$ と一致しなくてはなりません． $X = X \to A$ を満たす型なんて単純型では表現できないので， $λ x . x x$ に型は付けられません．

一方で，交差型を認めれば $λ x . x x$ に型を付けられるようになります．これは， $X$ 型の値としても使えるし， $X \to A$ 型の値としても使える値の型を， $X \land (X \to A)$ として表現できるためです．型注釈を補ってやれば $λ (x : X \land (X \to A)) . x x$ みたいな感じですね．

主部展開定理

主部展開定理（subject expansion）とは，簡約後の項 $N$ が型付け可能ならば簡約前の項 $M$ も型付け可能になる性質です．良く知られた主部簡約定理（subject reduction）⁴の逆ですね．

単純型付きλ計算ではもちろん，主部展開定理は成り立ちません．説明のために $i n t$ ， $b o o l$ ，二つ組とかがあると仮定して，項 $M = (λ f . (f 0, f t r u e)) (λ x . x)$ に型を付けられるかどうか考えてみましょう．この項 $M$ に型を付けるためには， $f$ が $i n t$ を受け取る関数であり，なおかつ $b o o l$ を受け取る関数でもあると表現できなくてはなりません．単純型ではそのような多相性を表現できないので，簡約結果 $N = ((λ x . x) 0, (λ x . x) t r u e)$ に型が付くにもかかわらず，簡約前の項 $M$ には型が付きません．

一方，交差型があれば簡約前の項 $M$ にも型を付けられます．これは， $f$ が $i n t$ を受け取る関数であり， $b o o l$ を受け取る関数でもあることを $f : (i n t \to A) \land (b o o l \to B)$ のように表現できるためです．

つまるところ，評価結果 $M [x \mapsto N]$ に型が付く⁵なら評価前の $(λ x . M) N$ にも型が付く主な理由は，交差型がアドホックな多相性を表現できるからに他なりません． $M [x \mapsto N]$ に型が付くなら，項 $M$ の変数 $x$ の出現に代入された $N$ それぞれに適当な型 $T_{i}$ が付いているはずなので，その型付けを集めて $(λ (x : T_{1} \land \dots \land T_{n}) . M) N$ みたいな感じに交差型で結んでやる感じです．

厳密に言うと $M$ に $x$ が出現しない場合， $M [x \mapsto N]$ に型が付いたからと言って $N$ に型が付くとは限らないので，論文で扱う主部展開定理のステートメントでは $N$ に少なくとも何かしらの型が付くことを仮定しています． $M = λ y . y$ ， $N = (λ z . z z) (λ z . z z)$ とか明らかにアウトですもんね．

主定理の証明

以上二つの性質を用いると，直感的には以下の手順で強正規化する項は型付け可能であることを示せます．

正規形まで簡約し，正規形が型付け可能であることを用いる
簡約を遡りながら主部展開定理を用い，簡約後の項が型付け可能であることから簡約前の項型付け可能であることを示していく

論文では，強正規化する項 $M$ の考えうる簡約列の長さの和についての完全帰納法で証明しています．論文で用いている主部展開定理は $M [x \mapsto N]$ に型が付くことに加えて $N$ に型が付くことも仮定していますが，これも帰納法の仮定から手に入ります．

SMLの四則演算ってクッソアドホックにオーバーロードされていて，文脈によって勝手にint上の二項演算になったりreal上の二項演算になったりするんですよね．マイナー言語で例えてしまったので，この辺りは各自お好きな言語で脳内補完して下さい…↩
どう計算を進めたところで必ず評価が停止する，みたいな性質．とりあえず計算が停止するかどうかみたいに思っておけばよろしい．↩
流石にそれでは実用上不便なので，実際には初期の篩型（refinement types）みたいに，制限された形の交差型が使われがち．今の篩型って依存型っぽい雰囲気出してるけど，最初は制限された交差型だったんすよ ↩
TaPLで言うところの型保存（preservation）↩
後述するように，厳密には $N$ に型が付くことも必要↩

fetburner.core

コアダンプ

交差型を持つ単純型付きλ計算の型付け可能性について

はじめに

性質が成り立つ直感

正規形が型付け可能であること

主部展開定理

主定理の証明