コゥゼンを勉強しなきゃ

• http://www.cs.cornell.edu/~kozen/papers/papers_collapsed.htm

ここからいろいろな論文が取れる。

set expressionはtype expressionで、set constraintsはtype constraintsだから、そのまま型推論に使える。しかし、termset代数が、エルブラン方式理論であってタルスキー方式理論じゃないのは問題だ。ちなみに、エルブラン方式（Hrbrand -）、タルスキー方式（Tarskian -）ってのもコゥゼン先生の造語だと思う。エルブラン方式は、ようするに構文的なコンストラクタしか考えない理論。集合は、項の集合に限るし、関数は型構成子に対応するものだけ。