このシリーズの「その2」で不平不満を言い、「その3」で実例を挙げたことですが、型推論に関わる用語法は混乱を招くものです。論理をある程度知っているが型推論の用語を知らない人と、型推論に詳しいが普通の論理に馴染みがない人が話をしたら、ほとんど話が通じないでしょう。外国語にようにまったく通じないならまだいいのですが、お互いに自分の知識で解釈しようとしたら、とんでもないカオスになるでしょう。
プログラミング言語の常識からの類推も通用しません。「型宣言」なら知っていても、型注釈や型コンテキストと言われたら何のことかわかりません。多相型という言葉にしても、オブジェクト指向の人々が持っている多相のイメージとは（無関係とは言わないにしても）かけ離れているでしょう。
そんな事情でして、「型推論」の「推論」がそもそも論理で言う「推論」とは違ったりしています。論理で推論というと、演繹系の推論規則、またはその推論規則を適用して証明のステップを進める行為です。型演繹系内で行われる（論理の意味の）推論や証明は、型推論でなくて型付け（typing）と呼んでいるようです。今日は、型付けの簡単な例を調べてみます。
内容：
シリーズ目次：
ラムダ式を型付けする規則
カリー／ハワード対応の一番簡単な例は、「タプルを持つ型付きラムダ計算」と「含意と連言を持つ命題論理」の対応です。この対応を復習しながら、ラムダ式（ラムダ項）の型付けを説明します。
まず、A、Bなどは命題として、以下の（論理の意味の）推論規則（推論図）を考えましょう。
A A⊃B
----------
B
A B
--------
A∧B
A、Bなどは集合だと解釈してみます。集合は、Sets-as-Typesの立場なら型だと言えます。論理の含意記号「⊃」を関数集合を作る演算子「->」に置き換え、論理の連言（AND）記号「∧」を直積集合を作る演算子「×」に置き換えてみます。
A A->B
----------
B
A B
--------
A×B
A、Bなどの集合（＝型）の左側に、値（集合の要素）を表す項を添えてみます。
s:A t:(A->B)
---------------
t(s):B
s:A t:B
-------------
[s, t]:A×B
ここで、t(s) は関数適用、[s, t]はタプルの構成です。
項と型に関する推論規則（推論図）を型付け規則（typing rule）と呼びます。型付け規則は、論理の意味の推論規則ですが、型推論規則とは（混乱が生じるので）呼ばないようです。
型付け規則を使ってみる
項の構文は「その4」で述べたJavaScript風構文とします。JavaScript風なので、タプルは [x, y] の形で書いて、配列（array）と呼びます。
lengthは配列の長さを求める関数、sumは数値（number）の足し算だとして、sum(length(x), 1) の型を求めてみましょう。足し算を「+」じゃなくて「sum」と書いたのは、関数形式のほうが扱いやすいのと、記号「+」はオーバーロードされていることが多くて厄介だからです。
もういきなり（論理の意味の）推論図を積み重ねた証明図を出してしまいますね。
x: array length: array->number
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- -
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
length(x): number 1: number
-------------------------------------
[length(x), 1]: number×number sum: number×number -> number
----------------------------------------------------------------
sum(length(x), 1): number
この証明図の一番下は結論である型命題 sum(length(x), 1): number です。上端になっている命題はいくつかあります。
- x: array
- length: array->number
- 1: number
- sum: number×number -> number
上記の証明図は自然演繹風です。自然演繹風の証明を外から眺めて、「こんな証明ができたよ」というメタな言明を書いてみると：
- x: array, length: array->number, 1: number, sum: number×number -> number |- sum(length(x), 1): number
ここで、ターンスタイル記号「|-」はメタな言明を構成する記号で、左側の命題群を仮定すると右側の命題を証明できる、という意味です。
自然演繹風の証明に関するメタな言明を再び形式化したものがシーケントだと解釈できます（そう思ってもいい、という程度）。そのことは、「シーケント計算と例外処理コード」でも書きました。
上のメタな言明を、シーケントらしく矢印を「⇒」として書き換えれば以下のようです。
- x: array, length: array->number, 1: number, sum: number×number -> number ⇒ sum(length(x), 1): number
型付け規則をシーケント計算の形に書き換えれば、型命題に関するシーケント計算の体系ができます。
型理論／型推論の言葉では
型理論／型推論では、なぜか「シーケント」という言葉は使いません。型判断（typing judgement）、型ステートメント（typing statement）、型表明（typing assertion）*1などと呼ばれます。シーケントの矢印も「⇒」や「→」ではなくて、ターンスタイルをそのまま使うのが習慣のようです。しかしメタ記号なのではなくて、シーケント計算風の演繹系のなかの記号です。
これから先、型理論／型推論におけるシーケントを型判断と呼ぶことにします。型判断は次の形をしています。
- 型命題1, 型命題2, ..., 型命題n |- 型命題
形の上では直観主義論理のシーケントと同じです。
型判断の左右辺に出現する型命題は、「名前 : 型」という形の基本型命題です。これはまた、名前に対する型割り当て（type assignment）ともみなせます。名前に対する型割り当てを型環境、型コンテキストとか呼ぶので、型判断（シーケント）の左辺を型環境、型コンテキストとも呼ぶわけです。
一方、型判断の左辺は演繹の仮定としての意味もあるので、型仮定（type assumuption）とか型仮説（type hypothesis）といった呼称も使われるのでしょう。
というわけで、同義語・類義語が生じるにはそれなりの事情と経緯があるとは言えるのですが、… …、やっぱりイヤになる。
*1:シーケントの成分である型命題を型表明と呼んでいる例もあります。
