檜山正幸のキマイラ飼育記

Catyと型推論

雑記／備忘 | 16:18 |

Catyは、トラブルの原因になりそうなことは、事前になるべく取り除こうという方針で作っています。

データのバリデーションは当然の事として、ハイパーリンクがちゃんと繋がることを保証しよう（ハイパーバリデーション）とか、リクエスト処理の途中で失敗しても被害を抑えるためにトランザクションをしっかりやろうとか、テストが負担にならない環境を作ろうとか、文書と実装の乖離をなくすために、自動描画や自動文書化のメカニズムを入れようとか、そんなことです。

当然に、リクエスト処理が“正しく”行われることも、できるだけ実行前に保証したいわけです。とは言っても「正しさ」とは何であるかの定義は難しいし、仮に定義が出来てもそれを完璧に保証するのは困難です。せめて型安全性くらいは保証したい、というのが我々の希望です。

最近、僕が論理と型推論の記事を書き始めたり、Kuwataさんも型システムに関するノートを書いたりしているのは、Catyに型安全性の判定系を付けるための準備みたいなものです。

型安全性の判定系は、その作業の一環としていわゆる「型推論」も行います。スクリプトコードを解析して、型の観点（型に注目するだけ）からそのコードを実行していいかどうかを調べます。「どうすれば型安全性の判定ができるか」は随分と前から（だいたいは）分かっていました。そもそも、型推論機能は、Catyプロジェクトの一番最初から予定されていた機能です。

予定はしてても手が回らないという事情は常にあるのですが、それよりネックになっていたのは、一箇所どうしても分からない事があったことです。「型安全かどうか？」にYES/NOで答えられても、実行時にチェックすべき型が決まらないのです。解がないから決まらないのではなくて、妥当な解がイッパイあり過ぎてどれを選んでいいか分からない、という状況でした。

型安全性が静的に分かるなら実行時型チェックは不要ではないか？ と思うでしょ。原理的には不要なんです。が、型に関する演繹をするとき、公理に相当する型宣言、例えば、foo :: string -> integer; はプログラマやアプリケーション設計者の自己申告なんです。開発中は（あるいは運用中でも）、自己申告と演繹に基づいたい名目上の安全性と実際の挙動に食い違いがあるかもしれません。そこで、静的に型安全と判定されても実行時型チェクを併用します。実行時チェック以外でも、型変数の具体化がないと困る箇所があります。

そのような型の具体化が決まらない問題があったのですが、比較的最近、どうやらうまくいきそうな気がしてきました。コロンブスの卵というか、僕に思い込みがあったようです。実は、苦し紛れにやってみた強引な方法がマトモな結果を出すので「えーーっ、こんなんで良かったん？」という状態なんですけどね。

ともかく、アルゴリズムはだいたい出来ていたし、引っかかっていた点は解決したみたい（たぶん）なので、自己流じゃない標準的な用語と記法で書き下そうと思い始めたのが1月末で、調べてみたら「標準的な用語と記法」と呼べるものはないし、山のような同義語／類義語でウンザリした、と ←今ココ。

それはそうと、以前、Catyの処理をCatyScriptで書いたことがあります（「REPL方式のWeb処理」とそこからのリンク先）。型推論の一部である単一化（ユニフィケーション）は、今のCatyScriptで書けそうです。実用にはなりませんが、説明には好都合です。CatyScriptのちょっと不便（非力）な部分をKuwataさんが修正してくれたので、単一化を書いてみようと思っています。

型推論に関わる論理の概念と用語 その5：型付けの簡単な例から型判断へ

雑記／備忘 | 17:01 |

このシリーズの「その2」で不平不満を言い、「その3」で実例を挙げたことですが、型推論に関わる用語法は混乱を招くものです。論理をある程度知っているが型推論の用語を知らない人と、型推論に詳しいが普通の論理に馴染みがない人が話をしたら、ほとんど話が通じないでしょう。外国語にようにまったく通じないならまだいいのですが、お互いに自分の知識で解釈しようとしたら、とんでもないカオスになるでしょう。

プログラミング言語の常識からの類推も通用しません。「型宣言」なら知っていても、型注釈や型コンテキストと言われたら何のことかわかりません。多相型という言葉にしても、オブジェクト指向の人々が持っている多相のイメージとは（無関係とは言わないにしても）かけ離れているでしょう。

そんな事情でして、「型推論」の「推論」がそもそも論理で言う「推論」とは違ったりしています。論理で推論というと、演繹系の推論規則、またはその推論規則を適用して証明のステップを進める行為です。型演繹系内で行われる（論理の意味の）推論や証明は、型推論でなくて型付け（typing）と呼んでいるようです。今日は、型付けの簡単な例を調べてみます。

内容：

1. ラムダ式を型付けする規則
2. 型付け規則を使ってみる
3. 型理論／型推論の言葉では

• その1

ラムダ式を型付けする規則

カリー／ハワード対応の一番簡単な例は、「タプルを持つ型付きラムダ計算」と「含意と連言を持つ命題論理」の対応です。この対応を復習しながら、ラムダ式（ラムダ項）の型付けを説明します。

まず、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 です。上端になっている命題はいくつかあります。

1. x: array
2. length: array->number
3. 1: number
4. 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）といった呼称も使われるのでしょう。

というわけで、同義語・類義語が生じるにはそれなりの事情と経緯があるとは言えるのですが、… …、やっぱりイヤになる。

おつかれさま

日常 | 18:44 |

電話をかけると「はい、おつかれさまです」。朝、某オフィスを訪問するといきなり「檜山さん、どうもおつかれさまです」。朝からそんなに疲れてないよ、と思ってしまいます。

僕の感覚では、ひと仕事終えて実際に疲れているのをねぎらう、って言うか、まーそこまで文字通りじゃなくても、開口一番、会っていきなりの「おつかれさま」は違和感あるのですが、皆さんいかがでしょう。

そういえば最近、女子高生達が別れ際に「おつかれさん」と挨拶してるのを目撃しました。夕方の別れ際だから状況としては自然だけど、女子高生ってところがナンカね、「さよなら」とか「じゃーねー」ではなくて「おつかれさん」ですか。学校でひと仕事終えてきたって感覚なのかな。あるいは、「おつかれさま」は極めて汎用的な挨拶の地位を獲得しているのか。

型推論に関わる論理の概念と用語 その4：JavaScript風の擬似言語

雑記／備忘 | 18:17 |

与えられた項（term）に片付け（typing）することは、型に関わる基本的行為ですが、なにかしら項の書き方（構文）を決めておかないと例を出せません。普通はラムダ項が使われるのですが、もっと馴染みがある構文を定義しておきましょう。以下で、項（term）と式（expression）は同じ意味で使います（使い分けの基準はありません）。

内容：

1. ラムダ項をJavaScript風に書く
2. let式
3. 型let式

• その1

ラムダ項をJavaScript風に書く

ラムダ計算の説明にJavaScriptは好都合です（「JavaScriptで学ぶ・プログラマのためのラムダ計算」を参照）。λ(x, y).(x + y) を function (x, y){return (x + y);} と書けます。だけど、return がいかにも邪魔ですね（「returnも嫌いな理由」も参照）。returnは書かなくてもいいことにしましょう。つまり、function (x, y){x + y} でいい、と。これならもう、ほとんどラムダ項そのもの。

関数の引数と戻り値の型を次の形で宣言できるとします。

• function (x:integer, y:integer):integer {x + y}

これは型付きラムダ項に対応します。ただし、型宣言は必須ではなくて、あってもなくてもいいとします。

引数変数だけでなく、どこに出現した変数にも型を添えていいとします。例えば、

• function (x, y):integer {x:integer + y:integer}

出現位置のその場で型宣言をするようなものです。このような形での、変数への型情報付与を型注釈（type annotation）と言います。最初に出した、引数と戻り値の型宣言も型注釈とみなして差し支えありません。

let式

変数を束縛しておいてから式を評価することを表すためにlet式がよく使われます。次の形を使います。

• let ＜変数束縛＞ in ＜式＞

JavaScript風構文でもlet式を使っていいとします。

• let {var x=2; var y=3} in {x + y}

この例では、x + y は 2 + 3 となり、全体の値は5です。すべての変数が束縛される必要はありません。

• let {var x=2} in {x + y}

これだと、x + y が 2 + y になりますが、それ以上は評価できません。

• let {var y=3} in {function (x) {x + y}}

これは、function (x) {x + 3} が値となります。

• let {var x=2} in {(let {var y=3} in {function (x) {x + y}})(x)}

少し複雑ですが、注意深く順番に見ていけば、次と同じことがわかると思います。

• (function (x) {x + 3})(2)

次はどうでしょうか？ 考えてみてください。

• let {var x=2} in {let {var y=3} in {let {var f = function (x) {x + y}} in {f(x)}}}

型let式

let式は、変数に値を束縛します。値には関数も含まれます（let {var f = function (x) {x + y}} がその例）。式の評価のための環境を整えていることになります。一方、式の型を知りたいときは、型付け（typing）の環境が必要です。それは、変数や関数の戻り値に型注釈を付けることになります。

型注釈を付けるための専用の構文、例えば lettype {var x:integer; var t:boolean} を導入してもいいのですが、めんどうだからletをそのまま使ってしまいましょう。

• let {var x:integer; var t:boolean} in {function (y:integer) {if (t) {x} else {y}}}

function (y:integer) {if (t) {x} else {y}} だけだと、yの型しかわかりませんが、外側のletにおいて、x:integer; var t:boolean と型注釈（型宣言）されているので、x, y, tの型がハッキリとわかります。

let内では、変数の型注釈と値の束縛を一緒にやってもいいとします。

• let {var x:integer=2; var t:boolean} in {function (y:integer) {if (t) {x} else {y}}}

if (t) {x} else {y} のような式だけだと、変数の型も値も不明です。let式によって、型情報や値情報を準備してあげることができます。すべての情報を明示的に与えなくても、与えられた情報をもとに計算や推論ができます。できるだけ少ない型注釈から、式やその部分式の型を決定することが、「型推論」のひとつの解釈です。

喫茶店とは何か

日常 | 18:14 |

長男：「俺、喫茶店行ってみたいな」
父親：「一緒にスターバックス行ってるじゃん」
長男：「スターバックスは喫茶店と違うよ」
父親：「じゃ、どんなんが喫茶店なんだ？」
長男：「えーとね、大人の人がタバコ吸ってるの」
父親：「禁煙じゃないってことね」
長男：「そう、それでコーヒー以外に食べ物がある」
父親：「スターバックスだって、スコーンとかサンドイッチとか売ってるぞ」
長男：「そうじゃなくて、ピラフとかスパゲッティとか」
父親：「あー、ランチセットとかね」
長男：「そうそう、スパゲッティの具はソーセージ」

確かに、昭和の「喫茶店」ってそんなイメージだな。

型推論に関わる論理の概念と用語 その3

雑記／備忘 | 11:19 |

「型推論に関わる論理の概念と用語 その1」で、「『型推論』て言葉が何を意味するかはそれほど明らかじゃない」と言いました。その2では、「同義語／類義語が無闇に多くて、人によって言葉の使い方が違う」と注意しました。僕の目論見としては、何種類かの文脈における「型推論」の意味を明らかにしたいのですが、その前に同義語／類義語を整理していきたいと思います。

「型推論」は「型に関する推論」という文字通りの意味で使われているわけじゃないですが、なにはともあれ、演繹系（deduction system, deductive system）は必要になります。そしてその演繹系は「型」という概念を持ちます。詳細はともかくとして、型概念を持つ演繹系を型演繹系と呼ぶことにします。型演繹系は、論理における演繹系の特別なものとみなすので、論理の通常の概念と言葉は使います。

「論理の通常の概念と言葉」の例として、「その1」で項と論理式を説明しました。「その2」では、0階、1階、2階の対象物について紹介しました（下の表）。

今回は、もう少し話を先に進めましょう。

内容：

1. シーケント
2. 型の原子論理式
3. 割り当てと環境
4. 値、型ってなんなの？

シーケント

項と論理式に加えて、シーケントと呼ばれる構文要素を導入するとなにかと便利です。シーケントは、矢印（→、⇒、|- などが使われる）の左右に、論理式をカンマで区切って並べた図形です。矢印記号に「⇒」を使うことにすると、x ≧ 0, y ≧ 0 ⇒ x + y ≧ 0 はシーケントの例です。

矢印に左右に、何個の論理式を並べることができるかを制限することがあります。

• 特に制限なし： 古典論理のシーケント
• 右側の論理式は高々1個： 直観主義論理のシーケント
• 左側の論理式は0個： 右片側シーケント
• 右側の論理式は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 という部分写像
• Var→Type という部分写像
• 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は、構文領域の存在物としてキチンと定義されたとしましょう。構文としての項、型項（型表現）も厳密に定義されたとしましょう。しかしそれでも、変数に割り当てるべき「値」や「型」はまったくハッキリしません。

値の候補として次があります：

1. 意味領域である集合の要素
2. 定数記号
3. 変数を含まない項

同様に、割り当てるべき型の候補として次があります：

1. 意味領域である集合やその部分集合
2. 型定数記号
3. 型変数を含まない型項

意味論が決まっているなら意味領域を持ちだしてもいいでしょうが、意味論が未定の場合は、割り当てるべき値／型として、“定数／型定数”か“変数／型変数を含まない項／型項”を取ることになります。“定数／型定数”が十分にあることは一般に保証できないので、“変数／型変数を含まない項／型項”で考えるのがよさそうです。

変数を含まない項を基礎項（ground term）とか閉じた項（closed term）と呼びます。基礎型項、閉じた型項の意味も同じこと。値の意味領域として基礎項の集合を使う意味論があります。エルブラン・モデル（Herbrand model）と呼ばれる意味論ですね。変数／型変数を含まない基本型命題 t∈T の真偽が型演繹系で決定可能なら*3、型項にも意味を与えたエルブラン・モデルが構成可能です（細部を詰めてないけど）。

閉じた（変数／型変数を含まない）基本型命題の真偽が型演繹系で決定可能という条件を満たすなら、特別な意味論が事前にないときはエルブラン・モデルを意味論として採用することができます。

割り当てる値／型についてハッキリとさせたいなら、次のどちらかを前提にする必要があるでしょう。

1. 型演繹系に対する意味論が事前に定義されている。
2. 型演繹系に対するエルブラン・モデルが構成可能である。

まだ触れてませんが、型理論独特の用語として、typing judgement、typing statement、typing rule、type derivation、subtype assertion、type constraints なんてのがあります。これらはどれも、論理と集合論の普通の言葉で定義も説明もできるのですが、あえて独自語彙の世界を作りたいのでしょうかねぇ？ 学習と記憶の負担が増すだけでいいこと無いと思うのですが、既に独自な（そして混沌とした）用語法が使われているので、まー、しょうがないです。

と、愚痴を言いながらもたぶん続きます。

型推論に関わる論理の概念と用語 その2

雑記／備忘 | 11:53 |

話が前後しますが、なんで僕がこんなエントリー（のシリーズかな？）を書こうと思ったかを述べます。その後、高階述語論理に少し触れます。

• 前回のエントリー：型推論に関わる論理の概念と用語 その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階の対象物が次のように定義できます。

要素、インスタンスという言葉を表に入れてないのは、「要素」、「インスタンス」次のように使うことがあるからです。

• 型はカインドのインスタンスである。
• 集合は族の要素である。

階数（order, rank）を指定して、「0階の対象」のように言うのが間違いが少ないでしょう。ところで、0階、1階、2階のような番号では味気ないので、各階に名前を付けることがあります。例えば：

この表に出現した名前（valueとかsetとか）をときに「型」と呼ぶことがあります。「typeという型」 -- ウーン、紛らわしい！ ヒドすぎるのでソート（sort）と呼びましょう。対象物を階数という番号で分類しても、ソートという名前で分類しても本質は何も変わりません。が、雰囲気は変わります。分類にソートを使う論理を多ソート論理（many-sorted logic）と呼びます。

ここでは、階数（番号）の別名ラベルとしてソートを使うだけですが、ソートのあいだになんらかの関係性を仮定するようなこともあります。ソートが複雑な階層構造を持つケースとかも考えることができますが、あまりうまく扱えないようです。現在主流の集合論では階数やソートは使いません*1。value, type, kind（あるいは、atom, set, family）のような単純な階層に抑えておくのが無難なようです。

チョビチョビと書くことにしますので、今日はここまで。

型推論に関わる論理の概念と用語 その1

雑記／備忘 | 18:51 |

寒いのがホントに苦手。寒いと活動レベルが下がって、なんもやる気が出ないわ。

これ、一回のエントリーで書こうとした内容なんだけど、途中までなので「その1」を付けました。中途半端なところでブチッと終りますが、続きをたぶん書きます。

[追記 date="2012-01-27"]「論理式の構成法」と「型の論理式」はこのエントリー内に続きを書きました。さらに続きは別なエントリーになるでしょう。[/追記] [追記 date="2012-01-30"]後に続く記事とツジツマをあわせるため、文言をわずかに修正。[/追記]

型推論を備えるプログラミング言語が増えてきましたね。そのうちに、型推論はプログラミング言語の「普通の機能」になるのかもしれません。

型推論と一口にいっても、型システムとか計算モデルによって色々と違いが出るでしょうし、そもそも「型推論」て言葉が何を意味するかもそれほど明らかじゃないです。人によって使い方が違うのではないでしょうか。僕自身は、「型推論」は「型の演繹系の理論」と捉えています*1。同語反復みたいですけど(苦笑)。

演繹とは、論理的な推論・証明のことです。論理で使っている一般的な概念と用語に、形容詞「型」を付けると、それで型理論の対応する概念・用語になります。それで、論理の説明をするついでに型理論に触れるようなスタイルで、型推論の周辺を軽く紹介します。型概念としては、一番簡単な Sets-as-Types（型とは集合なり）を採用します。

内容：

1. 項と論理式
2. 項の構成法
3. 論理式の構成法
4. 型の論理式

1. その1 （この記事）
2. その2
3. その3
4. その4
5. その5

項と論理式

論理では、式（expression）を二種類に分けるのが慣例です*2。例として、算術（小学校で習う数の四則計算）を考えます。2 + 3×4 のように「数を表す式」と、2 + 3×4 > 10 のような「主張や判断を表す式」に分けます。「数（に限らず対象物）を表す式」を項（term）、「主張や判断を表す式」を論理式（formula）と呼びます。

論理式を命題（proposition）と呼ぶこともあります。本来、論理式は構文的な概念で、命題だと意味も考えるのでしょうが、まーあんまり神経質にならずに、論理式と命題は同じと思っていいでしょう。僕は論理式と命題をほとんど区別していません。ついでに言うと、命題論理と述語論理の境界を引くのもあまり意味がないと思います（「論理とはなにか？」も参照）。

型理論では型が対象物なので、型を表す式が型項、型に関する主張や判断を表す式が型論理式、または型命題ということになります。

型項（type term）を type expression と呼ぶことは多いのですが、これを直訳すると「型式」、「ケイシキ」と読まれちゃうので、僕は「型表現」を使うことがあります。型表現と型項は同義語です。

項の構成法

項は次のような素材から組み立てます。

1. 定数記号
2. 変数記号
3. 演算子記号
4. 関数記号
5. 補助記号（括弧類）

ここではいちいち「記号」と付けてますが、「定数記号」を単に「定数」のように呼ぶことが多いです。「○○記号」と「○○」は、ホントは違うのですが、これも神経質になると鬱陶しいので意図的に混同します。

例えば、(1 + sqrt(x))/2 という項の素材は：

1. 定数記号： 1, 2
2. 変数記号： x
3. 演算子記号： +, /
4. 関数記号： sqrt()
5. 補助記号（括弧類）： (, )

型に関しても、+ が直和、* が直積、string, boolean は基本的な型、Tが型変数とするなら、型項 string + string*boolean + list<T> の素材は：

1. 型定数記号： string, boolean
2. 型変数記号： T
3. 型演算子記号： +, *
4. 型関数記号： list<>
5. 補助記号（括弧類）： 使ってない

演算子記号と関数記号の違いは書き方のスタイルだけなので、1 + 2 を sum(1, 2) に直すようにすると、関数記号だけにすることができます。この事情は型項のときも同じで、string + string*boolean + list<T> を型関数記号を使って、次のように書いてもかまいません。

• sum<sum<string, prod<string, boolean>>, list<T>>

型関数の引数を囲むのに山形括弧（不等号の対）を使うのも単なる習慣で、丸括弧でも問題はありません。

• sum(sum(string, prod(string, boolean)), list(T))

論理式の構成法

今日（2012-01-26）はここまで：たぶん、続く。

算術の 2 + 3×4 とか、変数を含んだ x + 1 とかは項です。それに対して、通常、方程式とか不等式とか呼ばれている式は論理式（formula）です。論理式を作るには、今までに出てきた記号類（定数記号、…、関数記号）とは別な種類の記号が必要です。それは関係記号です。例えば、等号「=」とか不等号「≦」なんかが関係記号です。

2 + 3×4 = 14 とか x + 1 ≦ 5 とかは関係記号を含んだ論理式です。関係記号は A = B とか A ≦ B のような中置（infix notation）にすることが多いですが、Eq(2 + 3×4, 14)、Le(x + 1, 5) のような関数っぽい書き方でもかまいません。

等号「=」と不等号「≦」は二項関係記号ですが、三項以上の関係記号や単項の関係記号があってもかまいません。例えば、「m は a と b の平均である」ということを Mean(m, a, b) と書けばMeanは三項関係記号です。「x は偶数である」を Even(x) と書けばEvenは単項関係記号です。

単項の関係は述語（predicate）と呼ぶことが多いので、単項関係記号は述語記号ともいいます。述語を関係と同義語として使う人もいます -- そのときは二項述語とか三項述語とかも出てきます。ここでは、単項のときは述語記号、二項以上なら関係記号と呼ぶことにします。また、関係記号／述語記号も、Eq(2 + 3×4, 14) のような関数っぽい書き方を標準とします。

論理式（命題）の一般的な作り方は次のようになります。

• 述語記号(項)、二項関係記号(項1, 項2)、三項関係記号(項1, 項2, 項3) などを原子論理式と呼ぶ。
• 原子論理式をベースに、論理結合記号により組み立てた式が論理式となる。

論理結合記号の選び方は目的や趣味により色々ですが、古典論理の標準的な論理結合記号である ∧（連言、かつ）、∨（選言、または）、¬（否定、ではない）、⊃（含意、ならば）としておきます。「論理記号のいろいろ」と「さまざまな「ならば」達」も参考にしてください。

2 + 3×4 = 14 と x + 1 ≦ 5 は原子論理式なので、(2 + 3×4 = 14) ∧ ¬(x + 1 ≦ 5) は原子論理式から組み立てられた論理式の例となります。

型の論理式

型に関する議論でも、項と論理式（命題）が出てきます。しかし、型の場合は、各種の記号類を2セット用意するのが普通です。なぜかというと、議論の対象物が二種類あるからです。ひとつはもちろん型、もうひとつの対象物は型に属するインスタンスデータです。Sets-as-Typesの立場なら、集合とその要素と言っても同じことです。

各種の記号類を2セット用意するなら、次のモノが必要です。

項もインスタンス項と型項（型表現）があり、インスタンスに関する論理式と型に関する、あるいはインスタンスと型の両方に関する論理式があります。でも、論理結合子は共通に使えます。上の表では、「型○○」という単純な名称を使ってますが、型理論特有の言い回しがあります。例えば、型演算子とか型関数とか言うよりは、型構成子とか総称型と呼ぶことが多いでしょう。

型を含む論理式（命題）で一番よく使うのは、「インスタンス項 ∈ 型項」という形のものです。ここでは集合の所属関係の記号「∈」を使いましたが、コロン「:」のほうが利用例は多いでしょう。例えば、3∈integer （あるいは 3 : integer）とか、f(2, x)∈(integer + string) とかです（+ は直和、つまりユニオン型のつもり）。

インスタンスと型の二種類の対象物を扱う点と、論理とは違った固有の言葉使いがある点で、型推論は難しい印象があるのですが、普通の論理と違ったことをやるわけではありません。

今日（2012-01-27）はここまで：たぶん、続く。

少年隊は遠くなりにけり

日常 | 15:34 |

長男は、昔のアイドルとか古い歌謡曲をよく知ってます。

長男：「東山って、少年隊のメンバーだったんだよね」
父親：「うん、今でも少年隊なんじゃないの」
長男：「それと、ニシコリっていう人も少年隊だよね」

テニスのニシコリ選手が大活躍ですからね。少年隊の「錦織」はニシキオリだとは長男も知らなかったようです。

“少年”隊つっても、もう四十代中盤ですよね、彼ら。東山紀之さんは取締役だそうですし。

ラベル付き有向グラフが関手であること

雑記／備忘 | 15:48 |

ラベル付き有向グラフは関手とみなせます。

有向グラフの基本的概念

Gを有向グラフとします。Gには特に制限を設けず、多重辺もループ（同じ頂点に戻る有向辺）も許しましょう。Gの頂点の集合をNode(G)、辺の集合をEdge(G)とします。e∈Edge(G) に対して、辺eの始点（source）を src(e)、辺eの終点（target）を trg(e) と書くことにします。

A, Bはなんらかの集合だとして、写像 a:Node(G)→A を頂点ラベリング、b:Edge(G)→B を辺ラベリングと呼びます。有向グラフGと頂点ラベリングaを一緒にした構造 (G, a) を頂点ラベル付き有向グラフ、辺ラベリングbを付けた (G, b) を辺ラベル付き有向グラフと呼びます。もちろん、頂点にも辺にもラベルが付いた (G, a, b) もあります。

「ラベル」というと“文字列”のような印象がありますが、値の集合A, Bは何でもかまいません。数値でも複雑なデータ構造でもラベルの値に使えます。「ラベル」という言葉の代わりに、習慣や応用により「色」「重さ」「コスト」「属性」「流量」「電圧」などと呼ぶこともあります。

GとHが有向グラフとして、f_node:Node(G)→Node(H)、f_edge:Edge(G)→Edge(H) の組 f = (f_node, f_edge) が次の条件を満たすとき、fは有向グラフの準同型写像と呼びます。

• 任意の e∈Edge(G) に対して、f_node(src(e)) = src(f_edge(e)) かつ f_node(trg(e)) = src(f_trg(e)) 。

辺ラベリングから作る関手

b:Edge(G)→B を、有向グラフGの辺ラベリングとします。頂点ラベリングは定義されてない状況で、1 = {*} = (単元集合) として、a:Node(G)→1 という自明な写像を頂点ラベリングだとします。こうすると、Gには頂点ラベリングaと辺ラベリングbが付いていることになります。

ここで、辺ラベルの集合Bから有向グラフHを作ります。

• Node(H) = 1 = {*} （頂点は1つだけ）
• Edge(H) = B
• e∈Edge(H) に対して、src(e) = *、trg(e) = * 。

a:Node(G)→1、b:Edge(G)→B は、a:Node(G)→Node(H)、b:Edge(G)→Edge(H) なので、(a, b) は有向グラフの準同型写像となります。準同型である条件を満たすことはほぼ自明でしょう（が要確認）。

有向グラフGとHから自由生成により自由圏（（パスの圏）を作ると、グラフ準同型写像 (a, b) は、FreeCat(G)→FreeCat(H) という関手に持ち上がります。

有向グラフHには頂点が1つしかなかったので、FreeCat(H)はBから生成された自由モノイドになります。形式言語理論の言葉では、アルファベットBから生成された語（文、列）の連接モノイドです。Bでラベルされた有向グラフGは、オートマトンの表現とみなせるので、関手 FreeCat(G)→FreeCat(H) はオートマトンから形式言語（語の集合）を作るメカニズムを与えています。

頂点ラベリングから作る関手

今度は、頂点ラベリング a:Node(G)→A があって、辺ラベリングは定義されてない状況を考えましょう。ここでもまた、GもAも圏と考えたいのです。

単なる集合Aを圏と考える標準的な方法は離散圏を作ることです； 集合Aを圏の対象類とみて、射は恒等射だけとします。それとは別な方法として、余離散圏（codiscrete category）を作ることもできます。集合Aに対する余離散圏とは次のような圏Cです。以下では、A×Aの要素を [x, y]（x, y∈A）のように書くことにします。

1. Obj(C) = |C| = A
2. Mor(C) = A×A
3. dom([x, y]) = x、cod([x, y]) = y
4. [x, y];[y, z] = [x, z]

別な言い方をすると、圏Cは、集合Aを頂点集合とする完全有向グラフを作って、射の結合を経路のバイバスで定義した圏です。集合Aに対する余離散圏を Codisc(A) と書くことにします。

頂点ラベリング a:Node(G)→A があると、e∈Edge(G) に対して b(e) = (src(e), trg(e)) と定義すると、b:Edge(G)→A×A となります。A×A は Codisc(A) の射の集合なので、a:Node(G)→|Codisc(A)|、b:Edge(G)→Mor(Codisc(A)) となります。ちょっと定義を付け足せば、FreeCat(G)→Codisc(A) という関手ができます。

つまり、頂点ラベリング a:Node(G)→A から出発しても、関手が構成できるわけです。

ラベル付き有向グラフは関手

頂点ラベリング a:Node(G)→A と、辺ラベリング b:Edge(G)→B があるときも、自由圏と余離散圏の手法を組み合わせると適切な圏Cが作れて、FreeCat(G)→C という関手が自然に構成できます。自由生成関手FreeCatと忘却関手Uとの随伴性から、FreeCat(G)→C は G→U(C) という有向グラフ準同型写像だと思っても同じことです。

ラベル付き有向グラフが関手なのだと分かれば、ラベル付き有向グラフによって表現される状態遷移系や回路図も関手だということになります。関手だからウレシイとは限りませんが、新しい視点を提供する可能性もあるでしょう。