このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

型推論のための定理

cathand 論理 型検査

たいした内容ではないけど、名前を付けておこう。

  1. タグ排他性の原理：α≠β ⇒ (@α A)∩(@β B) = 0
  2. 単調性の原理：S ⊆T ⇒ tags(S)⊆tags(T)
  3. ハテナ定理：正規形の式なら、一番外側の'?'で確定型か不確定型か判断できる。
  4. ν（nu）定理：ν(T) ≧ 1、ν(T) = n なら、Tはn成分のユニオンとして書ける。
  5. 排他的包含の原理：(α=>A) ⊆ (β1=>B1 | ... |βn=>Bn) ⇔ α = βi で (α=>A) ⊆ (βi=>Bi)

タグ排他性の原理は、もっともベーシックな事実。単調性の原理と排他的包含の原理は、そうなるように作りましょう、という指導原理。ν定理も指導原理に近い。が、ハテナ定理は定理だ。