このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

圏論的指数の周辺：ラムダ計算、デカルト閉圏、ノイマン型コンピュータ

雑記／備忘

圏論勉強会は、コーヒーがなんと160円で飲めるベローチェで実施されました（参考→http://www.sampou.org/cgi-bin/haskell.cgi?CategoryTheory%3a%b7%f7%cf%c0%ca%d9%b6%af%b2%f1&l=jp、→http://d.hatena.ne.jp/bonotake/20070812/1186947754）。

僕が参加していた時間（1時間ほど）内にできた唯一の問題（2.3.2 Exercise）について述べてみます。問題自体は簡単なので、周辺事情とかも入れて、雰囲気やココロが伝わるように書くつもり。で、書いてみたら長くなっちゃったよ。

内容：

ベータ変換とイータ変換

ラムダ計算の“適用（apply）演算”をナカグロ記号「・」で明示的に示すと、

  • (λx.f(x))・a = f(a)

が成立します。これは、左から右へとみればベータ変換です。（上の等式では、f(x)、f(a) の意味が曖昧ですが、非形式的な話なので神経質に気にしないでください。）


適用にはナカグロ記号「・」を使っているので、f(a)の意味はfの適用ではありません。f(x)の構文的な解釈は、変数xを含むかも知れない項Eをf(x)と書いていて、f(a)はEに出現するxをaに置き換えたE[a/x]のことだ、となります。意味的に解釈するなら（後述することですが）、f:A×1→B に対するカリー化 Λ(f):1→BA がλx.f(x)で、a:X→A に対する (Λ(f)×a);eval = a;f が等式の意味です。

関数の外延性＜がいえんせい＞、つまり「関数hは、任意の（ただし考え得る）xに対するh・xによって決定される」*1をラムダ計算のなかで表現すると、

  • λx.(h・x) = h

となります。これを左から右への変形（書き換え）規則とみたものはイータ変換と呼ばれます。

今ここでは、λx.f(x) = f ではなくて、λx.(h・x) = h であることに注意してください。適用「・」が出現しているのがミソです。後で説明しますが、hは関数そのものではなくて、“関数を表すデータ”なのです。

ラムダ計算とデカルト閉圏

このエントリーの主題はデカルト閉圏（しばしばしCCCと略記される）ですが、厳密な定義はしないで話を進めます。そのなかでデカルト閉圏のイメージが描ければいいとします。

デカルト閉圏は、ラムダ計算のモデルなので、ラムダ計算と対比して理解するのは良い方法です。ただし、静的にチェックされる型システムを持ち、タプル構成を許すようなラムダ計算を考えます（型無しラムダ計算もCCCでモデル化できますが細工が必要です）。

丸括弧のオーバーロード（多義的使用）が激しいので、タプル（ペア）は <a, b>で表現します。そして、f(a, b)は、f(<a, b>)の略記と考えます。f |→ λx.f(x) を、引数fの関数と考えて、ラムダの大文字Λで表現します；つまり、λx.f(x) = Λ(f)。また、適用演算（「・」で表したもの）は圏論の習慣に従い、applyではなくてevalとします。（applyとevalの用法は分野／人により違うので注意してください。）

以上のように記号の約束をして、先に出したベータ変換とイータ変換の等式を書き換えると：

  • eval(Λ(f), a) = f(a)
  • Λ(eval(h, x)) = h

同じことですが、二変数関数がタプルの関数であることを明示すれば：

  • eval(<Λ(f), a>) = f(a)
  • Λ(eval(<h, x>)) = h

ベータ変換とイータ変換に相当する2つの等式（の若干の一般化）が、デカルト閉圏の公理となります。このことから、デカルト閉圏は、外延的型付き高階関数計算の体系であることが予想できますね。

指数をコンピュータの言葉で語れば

「型→対象、関数→射、関数結合→射の結合、タプル→直積」と対応させれば、多変数（ただし、多変数をタプルの一変数で表す）関数計算をデカルト圏で定式化できます。しかし、ラムダ計算では、引数／戻り値として関数が使えるので、関数型＝“データとみなした関数の型”が必要です。関数型も型なので、圏論的には対象となります。

対象（つまり型）Aから対象Bへの関数を表す対象（つまり関数型）は、圏論では指数、ベキ、累乗などと呼ばれ、BA、[A, B]、(A→B)などと書かれます。コンピュータとのアナロジーで言えば、指数対象BAは、引数データ型Aで戻り値データ型Bである関数に対する機械語コードを格納する領域に与えられる型です。コード領域にも、静的に強く詳細に型が付けられている状況を想定してください。

コード領域のデータを関数とみなすには、ハードウェアまたはソフトウェアによるインタプリタが必要です。また、（抽象的／数学的な）関数をコード領域のデータに直すにはコンパイラが必要です。実は、抽象的／数学的な関数をソースコードとして記述する人間も必要ですが、その人もコンパイラの一部と考えます。

機械語コード（データです！）と引数データを受け取って解釈実行するインタプリタがeval、抽象的関数を受け取ってコンパイルするコンパイラがΛです。

関数fをコンパイルしたコードをインタプリタで走らせれば、もとの関数fを機能的に再現できることは、

  • eval(Λ(f), a) = f(a)

と表せます。これ、ベータ変換の等式。

コード領域のデータ（機械語コード）hをインタプリタで解釈することにより定義される関数f(x) = eval(h, x)をコンパイルすると、（理想的状況では）hに戻ることが

  • Λ(eval(h, x)) = h

ですね。これ、イータ変換の等式。

インタプリタとコンパイラを分類する

いままでの話は、直感的でおおざっぱな説明です。圏論化の準備として、もう少し精密に定式化します。とはいえ、暗黙に集合と関数の概念を使うし、ラムダ記法も非形式的（つまり、けっこうイイカゲン）なままで話を続けますけどね。

実際のCPUや仮想機械は汎用、あるいは万能ですが、以下では、関数のインタープリタを、扱えるデータ型ごとに細かく分類します。コードのデータ型がBAで、引数のデータ型がAである適用を計算するインタプリタをevalA,Bとします。evalA,Bに、いま述べた以外の引数が渡されれば型エラーとなります。このことは、evalA,B:BA×A→B と記述できます。

コンパイラΛは、二変数関数f:C×A→Bを部分的にコンパイルできるように拡張しましょう。部分的にコンパイルするとは、二変数関数f(t, x)の変数xに対するラムダ抽象（あるいはカリー化）λx.f(t, x) を、tの特定の値ごとにコンパイルすることです。全体として、tでパラメータ付けられた機械語コードの族を生成します。型Cの特定の値tごとに機械語コードが対応しているので、パラメータtは当該関数コードの名前や番号（エントリーポイント、最終的にはコードアドレスに解決される）とみなせます。このときCは、「関数の名前／番号の集合＝コンパイル済み関数のエントリーポイント群＝ライブラリモジュールのAPI」とみなせます。

“Cをエントリーポイント・パラメータとする、A→Bである関数のコンパイル済みモジュール”を作り出すコンパイラをΛC,A,Bと書きます。コンパイラΛC,A,Bの入力は、C×A→Bの関数です。その他の入力はエラーです。コンパイラΛC,A,Bの出力は、型がBAである機械語コードの族なので、C→BAという関数と見なせます。これをモジュールだと解釈するなら、Cはモジュールからエクスポートされる関数の名前／番号の集合で、C→BAは、名前と対応する機械語コード本体とのマップ（ディスパッチテーブル）を与えます。

データ型BAは「A→B という関数をコンパイルしたデータの型である」と主張するには、次の2つが必要です。

  • 抽象的関数をデータへとエンコードするコンパイラΛC,A,B達（Cを色々と動かす）。
  • 型ABのコンパイル済み関数コードと型Aの引数データを受け取って適用計算を実行するインタプリタevalA,B。

機械語コードをただそれだけで眺めている限り、ビット模様に過ぎません。ビット模様を関数だとみなすには、抽象的（あるいはホントの）関数とビット模様の双方向の変換機構が必要なのです。「ホントの関数→ビット模様」がコンパイラ、「ビット模様→ホントの関数」がインタプリタです。

モジュールの実行環境

コンパイラΛC,A,Bは、現実世界のコンパイラに比べてずっと高機能です。まず、抽象的・理念的な機能実体であるホントの関数をソースコードに記述する能力を内蔵しています（プログラマ付きコンパイラ）。それだけでなく、二変数関数f(t, x)の形をした関数の族を全部コンパイルして、tの各値をエントリーポイント群とするローダブル・モジュールを生成します。

コンパイラが出力としてモジュールを生成するなら、インタプリタもモジュールの実行機能を持つべきですよね。そこで、インタプリタevalA,Bを拡張して、単一の関数コードではなくて、エントリーポイントを持った関数コードの集まりであるモジュールを引数に取ることにします。拡張されたインタプリタ（モジュール実行環境）をEvalとすると、

  • Eval(m, c, a) = f(c, a)

となります。ここで、mはコンパイル済みモジュールで m = ΛC,A,B(f)です。cはCの特定値なので、モジュールからエクスポートされた特定関数を示す名前とか番号です。aは関数への引数。それでこの等式は、実行環境Evalにモジュールmがロードされた状況で、名前がcである関数に引数aを渡して実行したら、期待された結果が得られることを述べています。

モジュールmは、C→BAという関数ですが、ディスパッチテーブルのイメージを尊重して、m(c)の代わりにm[c]と書くことにします。m[c]は、名前cに対応する機械語コードです。この記法を使えば、evalとEvalの関係は、

  • Eval(m, c, a) = eval(m[c], a)

と書けます。つまり、モジュール実行環境Evalは、ディスパッチテーブルを引いた結果m[c]を単純なインタプリタevalに渡しているだけなんですね。念のために、上のEvalを含む等式をevalだけで書いておけば：

  • eval(m[c], a) = f(c, a) （ただし、m = ΛC,A,B(f)）

ノイマン／ゲーデルの箱庭風景

コンパイラΛとインタプリタevalの関係式 eval(Λ(f)[c], a) = f(c, a) は、圏論的指数、そしてデカルト閉圏の定義を与えるものですが、現状のノイマン型コンピュータの特徴をよく表しています。

人間とコンパイラが協力することにより、理念的な世界の存在である関数を、アルゴリズムを経由してビット模様へとエンコードできます。ビット模様はまさにコンピュータが扱うデータなのでメモリに格納できます；そう、プログラム内蔵方式コンピュータの原理そのものです。メモリに格納されたプログラムを実行するには、最低でも1個のエントリーポイントが必要です。であるなら、エントリーポイント（の識別子）と関数の引数を2つの変数とする2変数関数をプログラムの“ソース”とみなすが妥当でしょう*2。コンパイル結果は、1変数関数の機械語コードの1パラメータ族（コンパイル済みモジュール）です。

関数を、アルゴリズムを経由してビット模様にエンコードできることは、「計算可能関数に番号を付けて列挙できる」ことと事実上同じことです。ゲーデルが使った番号付けも同じ発想です。

共通する手法は、理念的な世界の存在（ただし、計算可能関数のようなたちの良い存在）を、具象的なデータのなかにエンコードしてしまうことです。具象的なデータは、目の前にあり手で触れるモノです。よって、理念的な外部世界を、目の前にある具象的対象物に投影して閉じ込めることができます。世界全体がスノーグローブ（和風の表現なら、箱庭の小世界）と同型になるわけです。

世界が箱庭に忠実に投影されているなら、当のその箱庭に対応する存在も箱庭内に見つかるはずです。こうして世界は再帰的なマトリョーシカ人形の構造を持つことになります。

であるとするなら、この世界が一番外側の世界である保証もなく、我々は無限入れ子の箱庭階層のどこかにいるのかも知れません。が、実際にどこにいるかを知る手段はありません。

Exercise

既に述べたように、インタプリタ（機械または仮想機械）evalとローダブル・モジュールを作るコンパイラΛの関係は次の等式で表現できます。

  • evalA,B(m[c], a) = f(c, a) （ただし、m = ΛC,A,B(f)）
  • ΛC,A,B(f) = m （ただし、f(c, a) = evalA,B(m[c], a)）

この等式は、集合と関数の概念／記法を使ってますが、一般のデカルト圏では、次のように書くことができます。f:C×A→B、m:C→BA、evalA,B:BA×A→B に対して：

  • (m×A);evalA,B = f （ただし、m = ΛC,A,B(f)）
  • ΛC,A,B(f) = m （ただし、f = (m×A);evalA,B）

（もとのテキストの記法ではなくて、ふだん僕が使っている記法です。idAを単にAと書いています。）

インタプリタevalA,Bは、（A、Bが何であっても）圏Cの射ですが、コンパイラΛC,A,Bは圏Cの射ではなくて、C(C×A, B) → C(C, AB) という集合論的関数です。これは何故でしょう？ 圏Cはデータと計算の世界です。evalも所詮は計算機構なので圏の射です。しかし、計算をデータにエンコードするには、人間の知性のような圏の外にある超越的な能力*3を介在させる必要があるのかもしれません（よくワカランのですけど）。

さて、件のExerciseですが、デカルト圏の等式によるevalとΛの関係の記述は、次のような記述と同値であることを示しなさい、というものです。

  • 任意の射f:C×A→Bに対して、m:C→BAであって (m×A);eval = f であるmが一意的に存在する。

fからmが一意的に決まるので、そのmをΛ(f)として、等式と可換図式をいじっていれば出てきます。背景の説明に労力を使って疲れたので、Exerciseの解は示しません（今日のところは）。（[追記]http://d.hatena.ne.jp/m-hiyama/20070816/1187250855に書きました。[/追記]）

それからまた

コンパイラに例えたΛC,A,Bは、C(C×A, B)→C(C, BA) という集合論的関数（写像）ですが、逆コンパイラΛ-1*4が存在するので、C(C×A, B)とC(C, BA) の同型を与えます。さらに、この同型は自然同型になるので、F(X) = X×A と G(X) = XA *5で定義される関手が随伴になります。

一方、ΛとΛ-1は、2変数関数と1変数高階関数の対応を与えるカリー化、アンカリー化でもあります。ただし、1変数高階関数は、データ化された関数を値とするので、なんらかのゲーデル化（実はコンパイル操作の本質）が内包されています。

ノイマンのプログラム内蔵方式、コンパイラとインタプリタの関係、ラムダ計算の意味論、圏論の随伴、カリー化、ゲーデル化などがデカルト閉圏と圏論的指数の周辺で絡まりあいながら調和しています。うーん、不思議だなー。

*1:これから、「どんなxに関しても f・x = g・x ならば、 f = g」が出ます。

*2:実はここ、コジツケっぽいと思いながら書いている。

*3:圏Cの“なかの人”から見て超越的なのであって、神様の能力を要求しているのではありません。

*4:逆コンパイラとはいっても、コンパイル済みモジュールからソースコード（関数の記述）を再現するのではなくて、関数そのもの（の集まり）を再現します。よって、この逆コンパイラはインタプリタのことです。

*5:対象だけではなくて、射に対しても適切に拡張する必要がありますが。