ここ何ヶ月か（ひょっとして何年？）悩んでいる問題がある。うまくいけば解決するかもしれない。細部の定式化はいくらでもバリエーションがあるのだけど、次のような事実がある。 プログラムの型安全性と集合の連立不等式系の可解性が同値となる。 集合の包…

Aを型項、αを型変数として、多相型を ∀α.A と表すのは定着した習慣になっている。∀をfor allなりfor anyと読み下すとそれなりに意味が通るので、まーいいかと思っていたが、論理の全称記号（全称限量子）が一緒に出てくる文脈だと混乱する。それと、論理の全…