型に関するアルゴリズム
実行すべきプログラムを式と呼ぶ。Catyでは、式＝スクリプトコード。型を表す構文的対象を型項とする。型項を項として、包含関係 t⊆s を原子論理式とする論理系を考える。これはデクスター・コゥゼンのset constraintsと同じ。ただし、型変数が含まれて、全称記号も使う。
式Fが与えられたとき、Consis(F)という論理式が作れる。Consis(F)は自由変数を含む式で、その全称閉包を∀[Consis(F)] とする。論理式Aが当該の論理系で証明可能なことを |- A と書く。|- ∀[Consis(F)] とは限らない。が、Consis(F)と同じ自由変数を含んだ論理式Wがあって、|- ∀[W⇒Consis(F)] とはできる。WをFの事前条件と呼ぶ。
UがFの事前条件ならば、U⇒W が成立するとき、Wを最弱事前条件（最汎妥当性制約）と呼ぶ。もし false が最弱事前条件なら、任意の事前条件Uは U ⇒ false （Uは矛盾する、¬U が成立する）となるから、Uの外延は空となる。Consis(F)が空の外延でしか成立しないとは、Consis(F)がまったく成立する見込みがないことだから、Fはまったくダメな式（実行してはいけないプログラム）となる。
最弱事前条件がtrueなら、任意のUに対して U⇒Consis(F) が成立し、任意の外延でConsis(F)が成立するから、Fは無条件で安全なプログラムとなる。
「まったくダメ」と「常に安全」の中間に、条件付きで安全なプログラムがある。そのようなプログラムの最弱条件、つまり最大の外延を計算で求める方法がある。ただし、式Fにある程度の制限を加えないと実効的ではないが、その制限は実用性を奪うほどではない。
てなことは、1年以上前にだいたい書いているのか。フムフム。
[追記]「だいたい書いている」けど、カインドがなかったから、カインド計算を前提にしてなくて、その意味で曖昧つうか、暗黙の制約に頼っている。型の代数系、あるいはさらにカインドから構成される代数系の計算を背景にしないと、キチンとしたアルゴリズムは書き下せない。
最近の進歩は、すべての変数（型変数になる）をカインド付きにして、型制約を明示的にしたことだな。型の集合をTとして、Tの部分集合だけではなくて、Tn の部分集合（型関係、型制約）も使う。型関数は型関係の特殊なものとも言える。型集合を対象として、型関係を射とする圏で考えることになる。
デカルト半環圏は「値の計算」のモデルにはなるが、「型の計算」のモデルではない。型の計算のモデルは、1レベル上がった、別な圏が必要だった。[/追記]
