集合の不等式系と等式系
ここ何ヶ月か（ひょっとして何年？）悩んでいる問題がある。うまくいけば解決するかもしれない。
細部の定式化はいくらでもバリエーションがあるのだけど、次のような事実がある。
- プログラムの型安全性と集合の連立不等式系の可解性が同値となる。
集合の包含関係「⊆」を不等号とみなして、「⊆」と集合演算（∪、∩、＼）を含む論理式を「不等式」と呼んでいる。コゥゼン（Kozen）は集合制約系（set contsraints）という言葉を使っている。
束縛されてない（開いた）型変数を含むプログラムがある時、次の問を考える。
- そのプログラムは型安全か？
- そのプログラムの型変数にどのような具体型を割り当てれば型安全か？
これは、実際は1つの問とも言えて：
- そのプログラムを型安全とする型変数への型割り当てを求めよ。
集合の連立不等式系に持って行くと：
- その不等式系は可解か？
- その不等式系の未知変数にどのような値を割り当てれば不等式系は満たされるか？
非可解のときはそれでオシマイだが、可解のとき、不等式系の解は一意に決まらない。どの解を選ぶべきかがわからない、これが問題。いわゆる最適解が欲しいのだが、最適性の条件が特にないのだ。テキトーに解を選べばいいのだが、テキトーに選ぶアルゴリズムが難しい。
ふと気づくと、不等式系Eが与えられると、これから閉じた（変数を含まない）不等式命題Cと等式系E'を作れる。そして、次の関係がある。
- 命題Cが真である ⇔ 等式系E'が可解である
さらに、
- 不等式系Eが可解である ⇔ 等式系E'が可解である
つまり、もとの不等式系Eの可解性も閉じた命題Cの真偽で決定できる。命題Cの作り方は知っていたし、それが可解性条件を与えることも知っていたが、等式系E'のほうは全然意識してなかった。
等式系E'は、もとの不等式系Eに比べてはるかに自由度が少ない。E'の解が（あるとして）一意かどうかわからないが、ずっと絞り込めることは確かだ。実例では、変数の数も劇的に減る。仮に変数が未定で生き残るにしても、それは少数だろう。
不等式系EからCとE'を作って、その後はCの真偽判定と等式系Eの解を求めることに集中すればいいのではないか、と（今は）思っている。
[追記] このテの問題は、http://d.hatena.ne.jp/m-hiyama-memo/20110507 にだいたいまとまっている。「型検査と制約解決：制約解決＝連立不等式系の解を求める」（http://d.hatena.ne.jp/m-hiyama-memo/20110507/1304756310）では等式を併用しているのだが、このときは制約の伝搬という考え方をしている。不等式の一部を等式に置き換えているけど、「可解性が変わらない」という意識はなかったと思う。[/追記]
[さらに追記]
集合の連立不等式系Eから、閉じた命題Cと連立等式系E'が得られると言ったが、実際のアルゴリズムを考えると、命題Cの真偽は不等式系Eを作る段階で分かってしまう。つまり、次が成立する。
- 不等式系Eが作れる ⇔ 命題Cが真である。
等式系の構成もほぼ同じ手順なので、
- 等式系E'が作れる ⇔ 命題Cが真である。
最終的な型具体化を、等式系E'のほうから作るのだとしたら、不等式系Eは不要となる。ただし、ほんとに等式を考えるのかと言うとそうではなくて、命題Cは不等式命題。不等式命題Cの真偽を確認しつつ、ついでに等式系E'を作っていくようにすればいい。
処理が失敗したときは、
- 不等式命題Cが偽だった。
- したがって、等式系E'（不等式系Eでも）を作ることはできなかった。
処理が成功すると：
- 不等式命題Cが真だった。
- 等式系E'が作れた。
となる。「不等式命題Cが真 ⇔ 等式系E'が可解」なので、得られたE'には解がある。一意解とは限らないが、不等式系Eに比べてずっと扱いやすいはずだ。
[/さらに追記]
