先週の土曜に、「晩に渋谷でパスタの会：双対編」を開催しました。例外処理の話をする予定ではいたのですが、当日の朝になって突然シーケント計算と絡めようと思ってしまいました。ところが、シーケント計算の話は最後の15分くらい。ちょっと残念。
ここでは、(コ)パスタの会の文脈は特に仮定しないで、古典論理のシーケント計算が、プログラムの合成や変換と対応付けられることを説明します。包括的な説明ではなくて、二、三の例を出すだけですけどね。でも、その例に関しては詳しく説明します。
内容：
- とても重要な注意
- シーケントと推論図
- シーケントと推論図とは何なのか
- カリー／ハワード対応
- 例外処理のコードパターン
- 例外コンバーターをパラメータとする例外処理
- どこかで見たような推論規則
- それにしても不思議だ
とても重要な注意
土曜の晩に、口汚く差別用語を使ってまで強調したことがあります。それは、圏の射を、プログラミング言語の関数や手続きだと思い込むのはやめてくれ、ということです。集合と写像の圏をモデルに使う場合でも、写像によりモデル化されるものが「プログラミング言語の関数や手続き」ってことではありません。プログラム全体のなかで、任意の部分計算を抜き出して、それを射だとみなしていいのです。
このことを理解しないで、プログラミング言語の構文構成素と圏の対象／射を素朴に対応させようとするから、バカバカしくもトンチンカンなことになるのです*1。素朴な対応がうまくいかないのは当たり前です。うまくいけばラッキーなだけ*2。http://d.hatena.ne.jp/m-hiyama-memo/19991128 の太字強調の直後のC言語風に書いた例をみてください。変数の参照と代入をするようなコード断片を射だとみなす例です。素朴な対応が一番うまくいくのは機械語でしょう。
僕が、「関数f」と言ったり書いたりしたとき、fは、プログラム全体のなかの何らかの計算単位のことです。その入力は計算開始前の資源状況、その出力は計算終了後の資源状況です。
シーケントと推論図
記号「⇒」の左右に、論理式をカンマで区切って並べた列を配置した記号的図形をシーケントと呼びます。A, B, C, D を論理式として、A, B ⇒ C, D はシーケントの例です。A, B ⇒ C とか、A ⇒ B, C とか A ⇒ B のように、1個だけ論理式を置いてもかまいません。実は0個の論理式でもいいのですが、今は触れません。
シーケントの記法は、竹内外史・著『層・圏・トポス』（P.134あたり）に原則あわせますが、含意記号は「⊃」にします。矢印「→」が多用されすぎだと思うからです。また、通常は、ギリシャ大文字Γ、Δなどで論理式の列を表現しますが、この記法は採用せずに、一番簡単な例を出すにとどめます。
横棒の上下にシーケントを配置した図形を推論図といいます。上段には、0個、1個、2個のシーケントを置けますが、下段は1個に限ります。以下に推論図の例を2つだけあげます。意味の解説はすぐ後でします。
右 含意導入規則
A, B ⇒ C
--------------[⊃右]
A ⇒ B⊃C左 含意導入規則
A ⇒ B, E C ⇒ D
----------------------[⊃左]
A, E⊃C ⇒ B, D
シーケントと推論図とは何なのか
シーケントの計算体系は、機械的な記号処理の規則集に過ぎません。意味など考えなくてもシーケント計算はできます。でもそれは辛いので、精神衛生上の説明をしておきます。
まず、いま目の前に、ヒルベルト方式演繹系とか自然演繹系とかがあって、その演繹系で A, B |- C だっとします。この事実を、記号的に「A, B ⇒C」と記します。つまり、「⇒」は対象演繹系の証明可能性です。対象演繹系の証明可能性を形式的に議論するメタな体系がシーケント計算だと思ってください。シーケントの推論規則は、対象演繹系に対するメタ推論を形式化したものです。
例えば、
右 含意導入規則
A, B ⇒ C
--------------[⊃右]
A ⇒ B⊃C
これは、A, B |- C （AとBを仮定して、Cが証明できる）ならば、A |- B⊃C （Aを仮定して、B⊃C を証明できる） ということ、つまりは演繹定理です。
日常的な言い回しで書くと：
- 「AとBを仮定して、Cが証明できる」ならば、「Aを仮定して、『BならばC』を証明できる」
もう少し簡略に言えば：
- 「AとBを仮定してC」ならば、「Aを仮定して『BならばC』」
あるいは：
- 「A, BならばC」ならば、「Aならば『BならばC』」
うえー、「ならば」だらけ！ このへんの事情は、「さまざまな「ならば」達」を参照してください。
さて、もうひとつの推論規則（基本的な推論図）も見ておきましょう。
左 含意導入規則
A ⇒ B, E C ⇒ D
----------------------[⊃左]
A, E⊃C ⇒ B, D
これは、
- 「Aを仮定してBまたはE」かつ「Cを仮定してD」ならば、「Aと『EならばC』を仮定して、BまたはD」
となります。Aを仮定したときの結論が、「BまたはE」と2つの場合があります。特にEのとき、もし「EならばC」があれば、上段の「Cを仮定してD」と組み合わせてDを結論できます。それがこの推論規則が言っている内容です。
カリー／ハワード対応
もう一度「右 含意導入規則」を：
A, B ⇒ C
--------------[⊃右]
A ⇒ B⊃C
これを次のように書き換えてみます。
A×B → C
--------------
A → [B->C]
適当な圏Cのなかで解釈するとして、A×BからCへの射（上段）があると、Aから[B->C]への射（下段）が作れることを意味します。ここで、[B->C]はベキCBの別表記です。
このような解釈ができるためには、圏Cにベキ（指数）がなくてはなりません。さらに、上段・下段を逆にした推論も導出できる必要がありますが、もしそうなっていれば：
C(A×B, C)
--------------[上段下段のホムセットが同型]
C(A, [B->C])
つまりは、積とベキ（指数）に関する随伴性です。これはカリー化（ラムダ抽象）と反カリー化の議論ですね。圏論では、デカルト閉圏の話になります。
で結局、「右 含意導入規則」は型付きラムダ計算で解釈可能だということになります。このへんのことは次のエントリーでも書いています。
例外処理のコードパターン
ふー、やっと例外処理の話ができる。例外処理の構成要素を次の3つとします。
- 危ない処理 ： 例外を引き起こすかも知れない処理で、tryスコープに入れて実行します。
- 例外ハンドラー ： 例外が起きたときに起動される処理です。話を複雑にしないために、例外ハンドラーは例外を出さないとします。
- 例外コンバーター ： 危ない処理で投げられた例外データを、例外ハンドラーが扱いやすいデータに変換します。
危ない処理をf、例外ハンドラーをg、例外コンバーターをγとすると、例外処理全体は次のようになります。
- try { f } catch(e) { g(γ(e)) }
例外コンバーターだけギリシャ文字（小文字ガンマ）を使ったのは多少の意味があるのですが、今は気にする必要はありません。念のためJavaScriptでも書いてみますが、冒頭の重要な注意を忘れないでくださいね。（γの代わりに、c_ を使います。）
try {
// 危ない処理、うまくいけばfの戻り値がそのまま返る
return f(a);
} catch (e) {
// キャッチされた例外データeを変換する
var c = c_(e);
// 変換されたcをハンドルして返す
return g(c);
}
例外コンバーターをパラメータとする例外処理
fとgが与えられたとき、次のような関数hを考えます。
function h(a, c_) {
try {
// 危ない処理、うまくいけばfの戻り値がそのまま返る
return f(a);
} catch (e) {
// キャッチされた例外データeを変換する
var c = c_(e);
// 変換されたcで例外をハンドルして返す
return g(c);
}
}
このhは、f（危ない処理）に渡すべき引数aと、例外コンバーターc_を引数に取るような関数です。第二引数が関数なので高階関数です。最初にγ（ギリシャ小文字）を使ったのは、「データとしての関数」という気分からです。
さらに、もとの2つの関数f, gを引数として、hを作り出すような高階関数は次のように書けます。
function makeExceptionHandling(f, g) {
return function (a, c_) {
try {
return f(a);
} catch (e) {
var c = c_(e);
return g(c);
}
};
}
Firebugでの実行例：
>>> function f(x) {if (x === 0) {throw "0"} return x;}
>>> function g(x) {return x + 1;}
>>> var h = makeExceptionHandling(f, g)
>>> h(0, function(e){return Number(e);})
1
>>> h(1, function(e){return Number(e);})
1
>>> h(2, function(e){return Number(e);})
2
JavaSriptは型宣言不要ですが、次のような型を想定しておきます。c_はγに戻します。
- f:A→B throws E
- g:C→D
- γ:E→C
γ:E→C と γ∈[E->C] は同じ意味ですが、γ∈[E->C] と書いたときは、「働きとしてのγ」よりは「関数データとしてのγ」の解釈が強調されます。B+D は「BまたはD」というユニオン型（ただし排他的ユニオン）だとして、もう一度型を記述してみると：
- f:A→B throws E
- g:C→D
- γ∈[E->C]
- fが成功するとき h:A×[E->C]→B
- fが失敗するとき h:A×[E->C]→D
- まとめて書くと h:A×[E->C]→B+D
makeExceptionHandlingは普通の関数より上位の存在と考えて別な記法を導入してみると、次のように書けます。
f:A→B throws E g:C→D
----------------------------[↓makeExceptionHandling]
h:A×[E->C]→B+D
どこかで見たような推論規則
ここでもう一度「左 含意導入規則」を：
A ⇒ B, E C ⇒ D
----------------------[⊃左]
A, E⊃C ⇒ B, D
あんれーー、なにかに似てる。って、すぐ上のmakeExceptionHandlingとソックリ。
カリー化の場合と同様に、適当な圏C（集合圏でかまいません）で解釈しましょう。シーケントの右辺のカンマは場合分けなので、圏Cに直和が必要です。つまり、解釈の舞台は直和を持つデカルト閉圏です。
「左 含意導入規則」をCのホムセットのあいだの対応だとして書き直すと：
C(A, B+E) C(C, D)
----------------------
C(A×[E->C], B+D)
上段と下段を繋ぐのは、 C(A, B+E)×C(C, D) → C(A×[E->C], B+D) という、ホムセット間の集合論的写像ですが、それがmakeExceptionHandlingです。makeExceptionHandlingは一種のプログラム合成です。どんな合成かというと：
- 危ない処理fと例外ハンドラーgが入力に与えられる。
- fの入力と例外コンバーターγを入力とするエラー処理付き関数hを出力する。
推論規則からは離れて、演繹定理＝デカルト閉圏の随伴性を仮定すれば、次のようなプログラム合成でもかまいません。
C(A, B+E) C(C, D) C(E, C)
-------------------------
C(A, B+D)
これは、危ない処理、例外ハンドラー、（射とみなした）例外コンバータの3者から、例外処理付き関数を合成します。
ところで、A ⇒ B, E というシーケントを A→B throws E の表現だとみなすには、正常終了のときの型Bと、例外データの型Eを区別する必要があります。例えば、throwsに相当する区切り記号としてセミコロンを使うと約束します。この約束で推論図をもう一度書くと次のとおり。
A ⇒ B; E C ⇒ D
----------------------[⊃左]
A, E⊃C ⇒ B, D
なお、絵算のときは、E; B と例外型を左に書いたほうが便利みたいです*3。
それにしても不思議だ
僕がいま述べたことに気付いたのは、例外処理の絵算をしていて、ワイヤーを上向きにひん曲げたときです。（絵を描く向きによりますが、上から下に描くとして）カリー化では、ワイヤーを下向き（∩という形）にひん曲げます。双対的に上向き（∪という形）にひん曲げて、留め金（バエズのclasp）でとめたり、となりのボックスと繋いだりしているうちに、シーケントの推論図と同じ図形になることを発見しました。
ゲンツェンがシーケント計算を創案したのは1930年代です。7,80年前ですよ。その推論規則が、なんで現在のプログラミング言語の例外機構と同じ形なんでしょう？ 単なる偶然かも知れません。あるいは、本質的な概念は時代や分野を超えている、といえばそれまでのこと。でも、気分としては不思議でなりませんね。
さらに、例外処理と同じ絵は、テンソル計算（の絵算版）でもしょっちゅう出会います。テンソル計算のほうは、コンパクト閉圏なので、×と＋が一致しちゃうのですが、絵（図形）としては似たものです。これも、「どっちも、ワイヤーひん曲げ操作が可能なモノイド圏だから」とアッサリ説明はできるのですが、「なんでや？」という感じは残ります。
僕は、この不思議さを味わうだけでもけっこう満足しちゃうのだけど、例外を含む（実は副作用も含む）計算の静的解析がシーケント計算で出来る可能性があるんで、現実的な余録もあるわけ。まーお得だこと。
