型解析がだんだんわかってきた
100年前の日付を付けてなんだかんだ書いている（例えば、http://d.hatena.ne.jp/m-hiyama-memo/19100110）。
コゥゼンの集合制約（set constraints）を参考にしているが、types as sets の立場の型理論なので、type constraintsといったほうが実情にあっている。関係記号が⊆だから、type inclusion または type inequality（どっちも略称はTI）の連言的コレクション（conjunctive collection）なので、CCTIとか呼ぼうかとも思ったが、アクロニムは覚えにくいので type constraints でもいいか。
がしかし、別なところで用語法で困った。コゥゼンに従えば、S⊆T が正の制約で、¬(S⊆T) が負の制約になる。原子論理式とその否定を、正リテラル／負リテラルと呼ぶ習慣があるから、まー当然。だけど、僕の用途では：
- 正の命題 S⊆T
- 否定命題 ¬(S⊆T)
- 負の命題 S∩T = 0
となる。ここで、0は空集合。S∩T = 0 は S⊥T と書き、¬(S⊆T) は S!⊆T と書くと短く書ける。
あくまでCatyと僕の状況での話だが、正の命題 S⊆T を否定した命題 S!⊆T だけでは不十分で、より強い負の命題 S⊥T が必要。この意味（コゥゼンじゃなくて僕の意味）での負の命題は、正の命題とほとんど排他的になる。S⊆T と S⊥T を仮定して：
- S∩S ⊆ T∩S
- S ⊆ T∩S
- S ⊆ 0
- S = 0
となるので、正の命題と負の命題が両立するのは S = 0 のときに限られて、空でないSを考えれば、どちらか一方しか成立しない。互いに否定の関係ではないのだが、排他的となる。
正の命題、負の命題、それぞれの否定の現実的な意味は：
- S⊆T 何の問題もない、素晴らしい。
- ¬(S⊆T) 問題がある、要注意だ。
- S∩T = 0 全然ダメ。ハナシにならない。絶望的。
- S∩T ≠ 0 なんともいえないが、望みはある。試してみよう。
Catyの型解析では、証明ターゲットは S⊆T なんだが、この正の命題を証明するのがほんとの目的ではなくて、負の命題の成否のほうが重要。もし、全然ダメが分かったら実行してはいけないのだから。正の命題の証明が失敗しても、実は希望があって、負の命題の否定「望みはある」ならば、実行時チェック条件を付けて実行に回せる。
自分で言うのもなんだが、Catyの型システムとそれに伴う演繹系（SILと呼んでいる）はよく出来ていて、帰納的構成の基底の部分では：
- 正の命題の否定が負の命題と一致する。
この性質はモデル論からいえることだが、公理に入れてしまえばいい。すると、ボトムアップな構成から正の命題も負の命題も証明できる。
正の命題と負の命題を別々に証明する必要はなくて、正の命題が証明できないことから負の命題の成立を帰結できる。基底部分では、「正の命題の否定が負の命題」なんだが、さらにSIL演繹系はあるモデルに対して完全なので、
- 正の命題の証明がない
- 正の命題は成立しない
- 負の命題が成立する
と言える。基底部分から（ボトムアップに）ステップを踏むアルゴリズムもある。
問題は2つあって：
- 都合のよいモデルを作ること
- 「証明できない」ことを判定するメタアルゴリズムを作ること
モデルは、とある論理系（SILとは別）によりdefinableな集合の全体を取ればいいことが分かっている。メタアルゴリズムも目星は付いているのだが、最初は手作業と目視しか手段がないので、作業的にシンドイ。ハッキリ言って疲れている。
