型宣言と型判定

変数xと型記号（ソート）Aに対して、x::A （普通はx:A）を変数の型宣言と呼ぶことにする。型宣言の集合を型環境と呼びΔ、Γなどで表す。型環境には、同じ変数の宣言が2回以上は登場しないとする。型環境に登場する変数の集合をVar(Δ)と書く。Var(Δ)とΔは同じ基数で、標準的な1：1対応を持つ。

Eを式（項）だとして、E::B も型宣言と呼ぶ。型環境Δと式の型宣言E::Bの組を、Δ |- E::B と書いて型判定と呼ぶ。上江州計算を仮定すると、型環境Δは、Var(Δ)上の型割り当てだから、Δは型付き変数集合に他ならない。モノイド閉圏Cに対して、上江州変数拡張C[Δ]が定義できる。

式Eに上江州流の解釈をすれば、E:[Δ]→B というC[Δ]の射が対応する。つまり、意味論は、(Δ |- E::B) |→ E in C[Δ] として与えられる。Eから大きなラムダ式<x₁, ..., x_n | E>を作れば、これはCの射となる。

問題は型推論。推論規則の意味はどこに求めるべきだろう？