Catyの型解析
最近考えている手順：
- スクリプトから有向グラフを作る。あるいは最初から有向グラフが与えられる。
- すべてのワイヤー（有向辺＝パイプ）に型注釈を付ける。このとき型付け規則（typing rules）を使う。
- 限量子で束縛されていた型変数を名前を変えて自由変数にする。このとき、名前の捕捉が起きないようにする。
- ワイヤーごとに不等式を作り、連立不等式系を構成する。この段階で不等式の個数はワイヤー＝パイプの数と同じ。
- 非対称単一化を行い、不等式を既約な形にする。変数を含まない不等式か、xを変数として、A⊆x、x⊆B が規約な形。
- 変数を含まない不等式を分離して、可解性条件とする。非可解ならオシマイ。
- 残った不等式（変数を含む規約形）から付随等式系を構成する（詳細はいずれ）。
- 付随等式系を代入法で解く（詳細はいずれ）。
- 付随等式系の解を使って型注釈の変数を具体化する。
