分解還元法による演繹系
Catyの型推論のために、分解還元法というのを考えた。シーケント計算とタブローの中間のような感じのもの。推論は逆向きに（結論から仮定へと）行われるので、次の用語を導入する。
- 分解図 -- 推論図（1ステップ）の逆
- 還元図 -- 証明図（nステップ）の逆
シーケントに対応するのは、有限個(n≧0)の原子論理式をカンマで区切った列。列式、または単に式と呼ぶ。列式のなかの原子論理式は次のいずれか：
- 真であるとすぐに判断できる。
- 偽であるとすぐに判断できる。
- 分解できる。
「真であるとすぐに判断できる」原子論理式は、aを基本型記号（basic type symbol）だとして、a⊆a か a⊆any のどちらかの形。あきらかに偽の論理式は色々ある。
分解とは、列式のなかの1個の原子論理式に注目して、それを1個以上の別な原子論理式の集合（構文的にはカンマ区切り列）に置き換えること。分解が p→q1, ..., qk のとき、次の性質が成立している。
- |= p ⇔ |= (q1∧...∧qk)
- rank(p) ＞ rank({q1, ..., qk})
上の主張が確認できるためには、原子論理式に対する意味論が定義されていることと、rankが定義されていることが必要。
意味論は意味領域がないとしょうがないが、rank関数は構文的に定義される。
- 基本型記号のrankは0
- 型項（型表現）のrankは、含まれる型関数記号、型演算子記号の総数。
- 原子論理式のrankは、左右のrankの和
- 列式のrankは、原子論理式rankの最大値
分解図では、上の式と下の式が意味論的には等価で、下の式のほうが確実にランクが下がっていることになる。常に分解可能性が保証できれば、ランクはゼロに落ちるから、列式の決定可能性が（メタ）証明できる。
意味論を適切に構成すれば、完全性（complete = sound and adequate）が成立する。完全になるように意味論を組み立てる、ってのがホントウのところだけど。
以上の話は、述語pに対する λx:A.p というラムダ式の定義域Aの議論。領域計算と呼びたいが、領域が多用されているから、台領域（キャリア；carrier）計算とでもするか。台の計算をもとにして、その上のラムダ式の計算が可能となる。ラムダ式の計算のほうが制限（restriction）計算となる。制限の実体はスキーマ属性だから属性計算と呼んでもいいかもしれない。
