話が前後しますが、なんで僕がこんなエントリー（のシリーズかな？）を書こうと思ったかを述べます。その後、高階述語論理に少し触れます。
- 前回のエントリー：型推論に関わる論理の概念と用語 その1
シリーズ目次：
型推論の話についていけない事情
型推論について調べたり勉強したりしようとすると、ゴチャゴチャしていてメンドクサイんですよ。同義語／類義語が無闇に多くて、人によって言葉の使い方が違うのです。そうなると、書かれたモノを読むときの負担が大きくてイヤになっちゃう。
きちんとした教科書なら定義もちゃんと書いてあるのでしょうが、僕は教科書は苦手。短めの論説・論文を拾い読みしていると、用語法が錯綜していてなんだかワカラナイ。ウゲウゲ。といった状況なんです。
なんでこうなの？ と考えてみると、まずは「型とはなにか？」に対する考え方・方針が色々あることがひとつの理由でしょう。Sets-as-Types、 Propositions-as-Types、Algebras-as-Types、Colgebras-as-Typesでは状況がだいぶ違うでしょう。インスティチューション・ベースならCategories-as-Typesと考えるべきかもしれません。とりあえずここでは、Sets-as-Types（型とは集合なり）に限定することにします。
「型とはなにか？」を固定してもまだ問題があります。型に関する議論には、プログラミング言語の概念、論理の概念、集合論の概念（Sets-as-Typesのとき）、そして型理論固有の概念が登場します。同じ、またはほとんど同じ概念にたくさんの用語が対応しています。同義語なのか、微妙に違うのか、趣味的な問題なのか判断に苦しみます。例えば、次のような言葉の違いを説明できますか？（説明できなくていいのですけど）
- 割り当て
- 代入
- 束縛
- 具体化
- 環境
- コンテキスト
同義語／類義語を整理したとしても、構造的な複雑さは残ります。Sets-as-Typesの立場で議論するとして、少なくとも二種類の対象物を扱うことになります。それは「その1」でも述べました -- 値（データインスタンス）と型です。各種の記号類を2セット用意する必要があり、項と論理式も、「値の項」、「値の論理式」、「型の項」、「型の論理式」が定義できます。それだけではなくて、「値と型を混ぜて作った項／論理式」だって出てきます。
高階述語論理の利用
「二種類（以上）の対象物を扱う」枠組みとして、高階述語論理が思い浮かびます。特に、Sets-as-Typesの立場なら、要素（原子、個体）と集合を扱うので二階述語論理が使えそうな感じがします。しかし、型推論の高階述語論理による説明を僕は見たことがありません（あるのでしょうけど）。直接的に定式化したほうが手っ取り早いという事情があるのでしょう。
型について云々する前に、高階述語論理をお勉強するのは遠回りだし、無駄な労力と思えるかもしれません。ですが、論理のついでに型理論も、あるいは型理論のついでに論理も、ということであれば無駄とも言えないでしょう。
値と型、それと“型の型”まで考えると、0階、1階、2階の対象物が次のように定義できます。
| - | 0階の対象物 | 1階の対象物 | 2階の対象物 |
|---|---|---|---|
| 型理論 | 値、データ | 型 | 型の型、カインド |
| 集合論 | 原子、個体 | 集合 | 集合の集合、族 |
要素、インスタンスという言葉を表に入れてないのは、「要素」、「インスタンス」次のように使うことがあるからです。
- 型はカインドのインスタンスである。
- 集合は族の要素である。
階数（order, rank）を指定して、「0階の対象」のように言うのが間違いが少ないでしょう。ところで、0階、1階、2階のような番号では味気ないので、各階に名前を付けることがあります。例えば：
| - | 0階の対象物 | 1階の対象物 | 2階の対象物 |
|---|---|---|---|
| 型理論 | value | type | kind |
| 集合論 | atom | set | family |
この表に出現した名前（valueとかsetとか）をときに「型」と呼ぶことがあります。「typeという型」 -- ウーン、紛らわしい！ ヒドすぎるのでソート（sort）と呼びましょう。対象物を階数という番号で分類しても、ソートという名前で分類しても本質は何も変わりません。が、雰囲気は変わります。分類にソートを使う論理を多ソート論理（many-sorted logic）と呼びます。
ここでは、階数（番号）の別名ラベルとしてソートを使うだけですが、ソートのあいだになんらかの関係性を仮定するようなこともあります。ソートが複雑な階層構造を持つケースとかも考えることができますが、あまりうまく扱えないようです。現在主流の集合論では階数やソートは使いません*1。value, type, kind（あるいは、atom, set, family）のような単純な階層に抑えておくのが無難なようです。
チョビチョビと書くことにしますので、今日はここまで。
