Catyのtyping rulesと制約の可解性を少し

次のようなtyping rulesを設けたとする。

  Γ ⇒ f:: A->B

  Γ ⇒ g:: C->D

  Γ ⇒ B⊆C

  ------------------------[パイプ]

  Γ ⇒ (f | g):: A -> D


  Γ ⇒ x∈B

  Γ ⇒ f:: A-> B

  ------------------------[変数生成]

  Γ ⇒ (f > x) :: A-> B


  Γ ⇒ x∈B

  ------------------------[変数参照]

  Γ ⇒ %x :: null -> B

次の証明があるはず。イコール並べたのは証明がそこにあることを意味する。

  Γ ⇒ f:: A->B

  Γ ⇒ x∈B

  Γ ⇒ g:: C->D

  Γ ⇒ B⊆C

  ===========================

  Γ ⇒ (f > x | g) :: A -> D

A, B, C, Dの代わりに X, Y, Z, W を未知変数とする（これは単に気分の問題）。Y⊆Z, Y≠0 が可解なら、型命題 (f > x | g) :: X -> W も可解となる。つまり、式 (f > x | g) のtypabilityは、4変数 X, Y, Z, Wの制約系の可解性に翻訳され、可解性条件は Y, Z だけの制約にまで落とせる（X, W は自由に決めてよい変数）。

解集合は、集合の空間を4個直積した空間のなかの図形（領域）だが、X, W方向への射影は全射になる。Yでは0だけは例外、Y, Zでは半空間みたいな感じ。