「型推論に関わる論理の概念と用語 その1」で、「『型推論』て言葉が何を意味するかはそれほど明らかじゃない」と言いました。その2では、「同義語／類義語が無闇に多くて、人によって言葉の使い方が違う」と注意しました。僕の目論見としては、何種類かの文脈における「型推論」の意味を明らかにしたいのですが、その前に同義語／類義語を整理していきたいと思います。
「型推論」は「型に関する推論」という文字通りの意味で使われているわけじゃないですが、なにはともあれ、演繹系（deduction system, deductive system）は必要になります。そしてその演繹系は「型」という概念を持ちます。詳細はともかくとして、型概念を持つ演繹系を型演繹系と呼ぶことにします。型演繹系は、論理における演繹系の特別なものとみなすので、論理の通常の概念と言葉は使います。
「論理の通常の概念と言葉」の例として、「その1」で項と論理式を説明しました。「その2」では、0階、1階、2階の対象物について紹介しました（下の表）。
| - | 0階の対象物 | 1階の対象物 | 2階の対象物 |
|---|---|---|---|
| 型理論 | value | type | kind |
| 集合論 | atom | set | family |
今回は、もう少し話を先に進めましょう。
内容：
- シーケント
- 型の原子論理式
- 割り当てと環境
- 値、型ってなんなの？
シリーズ目次：
シーケント
項と論理式に加えて、シーケントと呼ばれる構文要素を導入するとなにかと便利です。シーケントは、矢印（→、⇒、|- などが使われる）の左右に、論理式をカンマで区切って並べた図形です。矢印記号に「⇒」を使うことにすると、x ≧ 0, y ≧ 0 ⇒ x + y ≧ 0 はシーケントの例です。
矢印に左右に、何個の論理式を並べることができるかを制限することがあります。
片側シーケントなんて意味がなさそうですが、そうでもありません。「演繹系とお絵描き圏論」とか「コンパクト閉圏と絵算で理解する線形代数とシーケント計算（入り口だけ）」を参照してみてください。
シーケントの形による分類に「古典論理」とか「直観主義論理」とか出てきますが、気にする必要はありません。ある形状のシーケントを利用する典型的なケースが「古典論理」「直観主義論理」てだけで、矢印の左右の論理式の個数だけを根拠に分類しています。
後で出てくるシーケントは、矢印の右に論理式が1個だけのものですが、直観主義論理と関係があるわけじゃないです。
論理式はなんらかの「主張や判断を表す式」ですが、シーケントもやはり「主張や判断を表す式」です。古典論理の A, B ⇒ C, D というシーケントは、(A∧B)⊃(C∨D) という単一の論理式と事実上同じ意味です。それでも、主張や判断をシーケントの形に書いておいたほうが扱いやすいのです。
型の原子論理式
「その1」の「論理式の構成法」で述べたように、論理式を作るには、述語記号や関係記号を決める必要があります。型の議論では、「値がある型を持つ／値がある型に所属する」という主張が基本的なので、所属関係を表す記号「∈」を導入します。
「∈」は集合に関して使う記号ですが、Sets-as-Typesの立場なので、型と集合は同一視してもかまいません。気になるようでしたら「:」に置き換えて読んでください。
述語・関係記号が二項関係記号「∈」だけで、左に項（値の項）、右に型項を置く規則（構文的な制限）なら、原子論理式は、「項∈型項」という形になります。例えば：
- 3∈integer
- (2 + 3×4)∈integer
- x∈boolean
- (x + 1)∈boolean
型変数や型関数（総称型）があるなら、Tを型変数として次も原子論理式です。
- 3∈T
- (x + 1)∈T
- p∈Pair<integer, boolean>
- q∈Pair<T, integer>
このような、型に関する原子論理式を型表明（typing assertion）と呼ぶことがあるようです。でも、原子論理式とは別な意味で「型表明」を使っている例もありますね。これといった定番用語もないようなので、型の原子論理式とか基本型命題とか呼ぶことにします。「その1」で注意したように、型論理式と型命題を区別しません。
一番単純な形でよく使う基本型命題は、「変数∈型定数」という形でしょう。例えば、x∈integer 。この形の型命題は、普通に言えば、変数の型宣言（type declaration）ですね。しかし、型理論のなかでは型宣言という言い方はあまりしないようです。変数の型宣言や初期化は、項の一部とみなすことがあるからでしょう。
割り当てと環境
型演繹系の形式言語には、値変数（0階の変数）と型変数（1階の変数）が登場します。変数とは未知のナニカを表す記号ですが、これに既知のナニカを対応付けることを割り当て（assignment）と呼びます。何種類かの割り当てがあります。
- 値変数に値を割り当てる
- 値変数に型を割り当てる
- 型変数に型を割り当てる
値変数に値を割り当てること（value assignment）は、付値（valuation）とか、束縛（binding）ということもあります。また、assignment の訳語に代入を使うこともあります。束縛と代入はニュアンスの違いがありますが、広く合意された使い分けの基準はないと思います*1。
話をハッキリさせるために、値変数の集合をVar、値の集合をVal、型変数の集合をTVar、型の集合をTypeとします。すると、上の各種の割り当ては次のように言い直せるでしょう。
「Var→Val という部分写像」は環境（environment）と呼ばれます。特にクロージャの一部として現れるときは環境部分（environment part）といいます。環境は、評価（evaluation）のときに効いてくるので、その意味を込めて評価環境（evaluation environment）とも呼びます。
「Var→Type という部分写像」は型環境（typing environment）と呼ぶようですが、「TVar→Type という部分写像」のほうを型環境と呼んでいる例もあります。型コンテキスト（typing context）という言葉を導入して、「Var→Type」が型コンテキスト、「TVar→Type」が型環境と区別するとかもあります。「TVar→Type」のほうを型置換（type substitution）と呼んでいる例もありますね。でも、型置換は型単一化（type unification）との絡みでちょっと別な定義をすることもあります*2。
さらにややこしいことには、「Var→Type という部分写像」は、文脈により型仮定（type assumuption）とか型仮説（type hypothesis）と呼ばれたりもします。形容詞としての「型」はtypeだったりtypingだったり（まー、どっちでもいいのでしょう）、ひとつの基本型命題を type assumption と呼ぶこともあれば、基本型命題のセットをまとめて type assumption と（単数形で）指していることもあります。
矢鱈に色々な言葉があるのは分かりましたが、どれが標準的な言い回しか？とかはさっぱりワカリマセンでした。以下では、「型環境」も「型コンテキスト」もその他の用語も使わずに、面倒でも「値変数への型の割り当て」「型変数への型の割り当て」と言うことにします。いずれ述べるつもりですが、これらの概念は、型命題（型の論理式）とシーケントがあれば、それだけでシンプルに構成と説明ができるものです。そんなにイッパイ用語を作り出す必要性なんて全然ないと思うのですが…。
値、型ってなんなの？
「値変数に値を割り当てる」「値変数、または型変数に型を割り当てる」と言えば曖昧性はないような気がしますが、残念、まだまだ曖昧です。
値変数と型変数（の記号）の集合VarとTVarは、構文領域の存在物としてキチンと定義されたとしましょう。構文としての項、型項（型表現）も厳密に定義されたとしましょう。しかしそれでも、変数に割り当てるべき「値」や「型」はまったくハッキリしません。
値の候補として次があります：
- 意味領域である集合の要素
- 定数記号
- 変数を含まない項
同様に、割り当てるべき型の候補として次があります：
- 意味領域である集合やその部分集合
- 型定数記号
- 型変数を含まない型項
意味論が決まっているなら意味領域を持ちだしてもいいでしょうが、意味論が未定の場合は、割り当てるべき値／型として、“定数／型定数”か“変数／型変数を含まない項／型項”を取ることになります。“定数／型定数”が十分にあることは一般に保証できないので、“変数／型変数を含まない項／型項”で考えるのがよさそうです。
変数を含まない項を基礎項（ground term）とか閉じた項（closed term）と呼びます。基礎型項、閉じた型項の意味も同じこと。値の意味領域として基礎項の集合を使う意味論があります。エルブラン・モデル（Herbrand model）と呼ばれる意味論ですね。変数／型変数を含まない基本型命題 t∈T の真偽が型演繹系で決定可能なら*3、型項にも意味を与えたエルブラン・モデルが構成可能です（細部を詰めてないけど）。
閉じた（変数／型変数を含まない）基本型命題の真偽が型演繹系で決定可能という条件を満たすなら、特別な意味論が事前にないときはエルブラン・モデルを意味論として採用することができます。
割り当てる値／型についてハッキリとさせたいなら、次のどちらかを前提にする必要があるでしょう。
- 型演繹系に対する意味論が事前に定義されている。
- 型演繹系に対するエルブラン・モデルが構成可能である。
まだ触れてませんが、型理論独特の用語として、typing judgement、typing statement、typing rule、type derivation、subtype assertion、type constraints なんてのがあります。これらはどれも、論理と集合論の普通の言葉で定義も説明もできるのですが、あえて独自語彙の世界を作りたいのでしょうかねぇ？ 学習と記憶の負担が増すだけでいいこと無いと思うのですが、既に独自な（そして混沌とした）用語法が使われているので、まー、しょうがないです。
と、愚痴を言いながらもたぶん続きます。
