デカルト閉圏は計算（computations）のモデルとして大変に使いやすいものです。しかし、どうもデカルト閉圏が矮小化されて理解され、応用範囲を狭めているような印象も持ちます。デカルト閉圏が型付きラムダ計算のモデルであるのは事実ですが、このことが強調されすぎて、デカルト閉圏は「型付きラムダ計算にしか適用できない」という誤解があるのかもしれません。
静的に強く型付けされるプログラミング言語処理系は、デカルト閉圏でうまくモデル化できます。いま、「プログラミング言語」ではなくて、「プログラミング言語処理系」と言ったのに注意してください。プログラミング言語の構文に意味を付与する話ではなくて、コンパイラやランタイムを含んだメカニズム全体の定式化にもデカルト閉圏が使えます。
デカルト閉圏とプログラミング言語処理系
デカルト閉圏の特徴は、C(A×B, C) ＝ C(A, [B, C]) という同型があることです。ここで、A×B はデカルト積（直積）、[A, C] は指数（CA）です。「＝」は「等しい」ではなくて同型を意味します。この同型を与える写像（カリー化、ラムダ抽象）を ΛA,B;C:C(A×B, C) → C(A, [B, C]) と書くことにします。
さらに、デカルト閉圏には評価射 evB,C:[B, C]×B → C があり、次の等式を満たします。
- ev(Λ(f), id) = f
図式順記法を使ってもう少し正確に書くと：
- (ΛA,B;C(f)×idB);evB,C = f
デカルト閉圏の構成素と現実の言語処理系との対応関係は次のようになります。
- [B, C] の要素 -- 実行可能ファイルのフォーマット仕様に基づくバイナリデータ
- C(A×B, C) の要素 -- 同じ型の関数の名前付きの集まり
- C(A, [B, C]) の要素 -- 関数コードの名前解決とローディング
- Λ -- コンパイラとリンカー
- ev -- インタプリタ、仮想マシン、ハードウェアのようなランタイムシステム
この対応関係は一例に過ぎませんが、次のような事実をうまく表しています。
このようなことは何度も書いたことがあります。次のエントリー群も参考にしてください。
デカルト圏の部分閉構造
デカルト圏Cがデカルト閉（closed）になるには、任意の対象の対(A, B)に対して指数 [A, B] を作れる必要があります。応用によってはこの条件がきつすぎるので、閉になる条件をゆるめることにします。
指数[-, -]、カリー化Λ、評価射evは、圏の対象を添字に持ちます。添字を引数と考えると、指数、カリー化、評価射は、次のような対応とみなせます。
- [-, -] : |C|×|C| → |C|
- Λ : |C|×|C|×|C| → Set（集合圏の射＝写像）
- ev : |C|×|C| → C
この見方において、定義域が全域であることを要求しないことにします。つまり、上の対応を部分写像でいいと考えます。このゆるい条件で考えた3つ組 ([-, -], Λ, ev) をC上の部分閉構造と呼ぶことにします。
デカルト圏の部分閉構造は、チューリング完全とは限らないプログラミング言語（スクリプティング言語）処理系の定式化に使えます。例えば、基本データ型は整数と真偽値だけで、[integer, boolean] のような関数型（指数対象）は持つが、もっと高階の関数型は一切サポートしないような簡易言語の処理系を定義できます。
部分閉構造が通常の（全域的）閉構造と同じように扱えるために、次の条件は要求します。
- ΛA,B;C が定義されるなら、[B, C] も定義される。
- [B, C] が定義されるなら、適当なAに対するΛA,B;C が定義されている。
- [B, C] が定義されるなら、evB,C も定義される。
- evB,C が定義されるなら、[B, C] が定義される。
これらは、次のような現実的な状況や要求に対応します。
- コンパイラを使って、ちゃんとした実行可能バイナリデータを作れるべき。
- 実行可能バイナリデータを手で作るなんてイヤだよね、コンパイラが吐き出すべき。
- 仕様に従った実行可能バイナリデータは、仮想マシンで実行可能であるべき。
- 仮想マシンがあるなら、そのマシンが実行すべき（任意の）バイナリデータを作れるべき。
部分閉構造とプログラム変換
Cがデカルト閉圏で、Dもデカルト閉圏のとき、デカルト閉構造を保つ関手 F:C→D を考えることができて、デカルト閉圏とデカルト閉構造を保つ関手（デカルト閉関手と呼ぶのか？）の全体は圏の圏CCCを作るでしょう（細部まで確認してないですが、たぶんそういうこと）。
全域的なデカルト閉構造の代わりに部分デカルト閉構造を考えても同様に、圏の圏PartialCCCは作れそうです（たぶん）。が、もう少し単純化した状況； ベースとなるデカルト圏Cを固定して、その上の部分閉構造をたくさん考えることにします。
([-, -], Λ, ev) をC上のデカルト部分閉構造、([-, -]', Λ', ev') を同じベース圏C上の別なデカルト部分閉構造とします。[-, -]の定義域に入るA, Bに対して定義された TA,B :[A, B]→[A, B]' という射の族で次を満たすものを考えましょう。
- ΛA,B;C;TB,C = Λ'A,B;C
Tは、コンパイルの出力をバイナリレベルで変換するトランスレータ（あるいはコンバータ）になっています。コンパイラΛの出力であるデータをTに通すと、別なコンパイラΛ'の出力と同じになり、次の等式が成立します。
- ev'(T(Λ(f)), id) = ev'(Λ'(f), id) = f = ev(Λ(f), id)
今までの話ではソースコードという概念が出てきませんが、evをソースコード・テキストを入力としてそのまま実行してしまうインタプリタと考えると、ソースコードレベルのトランスレートも定式化できます。
このようなプログラム変換Tを射とすれば、デカルト圏C上の部分閉構造の全体が圏となります。
何の役に立つか
型システムが1つあって、それはデカルト圏Cを定義するとします。これは、データ型 A,B ごとに計算処理の集合 C(A, B) があり、計算の結合（順次合成）が定義されていることです。デカルト性は、タプル型 A×B が定義できるという条件です。
この型システム上に、複数の簡易言語処理系が載っている状況を考えましょう。それぞれの言語処理系は、可能な計算処理 A→B に対する実行可能フォーマットの仕様 [-, -]、コンパイラΛ、ランタイムevを持っているとします。プログラム変換Tは、2つの処理系のあいだを繋ぐ役割を持ちます。
このような定式化は、単一の型システム上に相互に関連する複数言語が載っている状況を記述し整理するには役立つと思います。実際のところ、そのような状況を記述し整理する必要性に迫られて、こんなことを考えたのです。
