最近、Meta Object Protocol (MOP) を扱わなきゃ、とか思ってます。使いやすい枠組みがないかな? と、ありますね。以前(去年の正月)、「プログラミング言語の処理系と、デカルト圏の部分閉構造」という記事を書いたのですが、この「部分閉構造」が使えそうです*1。
デカルト圏の部分閉構造
デカルト圏の部分閉構造は、構文とソースコードという概念は無視しての言語処理系の定式化です。以下、「プログラミング言語の処理系と、デカルト圏の部分閉構造」と同じ記号・記法を使います
C = (C, ×, 1) を十分に大きなデカルト圏とします。「プログラミング言語の処理系と、デカルト圏の部分閉構造」では、C上の部分閉構造の定義域を部分圏とは仮定してないのですが、それだと話が煩雑になりキレイにまとまらないので、Cの部分デカルト圏を使うように定義を変更します。
C上の部分閉構造は次の構成要素からなります。
- Cの部分デカルト圏D
- A, B∈|D| に対して、 [A, B]∈|C| という割り当て。
- A, B, C∈|D| に対して、ΛA,B,C : D(A×B, C) → C(A, [B, C]) という集合の同型写像。Λは同型なので、Λ-1 が存在する。
- A, B∈|D| に対して、evA,B : [A, B]×A→B in C という射。
次の点には注意してください。
- [A, B]∈|C| だが、[A, B]∈|D| とは限らない。つまり、指数を作る演算は|D|内に閉じているとは限らない。
- したがって、D(A, [B, C]) は意味を持たないかもしれない。
- A, B∈|D| であっても、(A×[A, B])∈|D| は保証できないので、evA,B : [A, B]×A→B in がDの射とは限らない。
evのプロファイル(域と余域) evA,B : [A, B]×A→B は「プログラミング言語の処理系と、デカルト圏の部分閉構造」に合わせたもので、evA,B : A×[A, B]→B でもかまいません(最近の僕は、A×[A, B]→B を使うことが多いです)。
さて、部分閉構造であるための条件は、次のカリー化に対する基本公式です。
- f:A×B→C in D に対して、(ΛA,B,C(f)×idB);evB,C = f
簡略に書くなら: ev(f^(a), b) = f(a, b) 。
これらの構成要素のインフォーマルな意味を、「プログラミング言語の処理系と、デカルト圏の部分閉構造」から再掲すると:
部分閉構造のあいだの関係:模倣可能性
複数の部分閉構造を同時に扱うので、部分閉構造自体をΦ、Ψなどのギリシャ文字大文字で示します。(D, [-, -], Λ, ev) のそれぞれにΦ, Ψなどを添えた記号法を使います。Φ = (Φ.D, Φ[-, -], Φ.Λ, Φ.ev) のようです*2。部分閉構造は言語処理系と解釈できるので、次のように思えばいいでしょう。
- Φ.D -- 言語処理系Φが扱えるデータ型と関数の圏(デカルト構造を持つのでタプルを作れる)
- Φ[-, -] -- 言語処理系Φの実行可能形式のデータ(2つの型でインデックスされる)
- Φ.Λ -- 言語処理系Φのコンパイラ
- Φ.ev -- 言語処理系Φの実行エンジン
Φ = (Φ.D, Φ[-, -], Φ.Λ, Φ.ev) と Ψ = (Ψ.D, Ψ[-, -], Ψ.Λ, Ψ.ev) がデカルト圏C上の2つの部分閉構造だとします。ΦとΨのあいだの準同型を定義します。「プログラミング言語の処理系と、デカルト圏の部分閉構造」において、「コンパイル結果を変換するトランスレータ」と言ったものと事実上は同じ概念です。
次の状況を考えます。
- Cの部分圏として、Φ.D⊆Ψ.D である。
- A, B∈|Φ.D| に対して、TA,B:Φ[A, B]→Ψ[A, B] というCの射が割り当てられている。
- f∈Φ.D(A, B) に対して、Ψ.evA,B(TA,B(Φ.ΛA,B(f)), idB) が成立する。
このとき、(記号を乱用して)T:Φ→Ψ と書き、TをΦからΨへの準同型と呼ぶことにします。もっと洒落た呼び名を付けたいのですが思いつきません。「変換(トランスレータ)」が良さそうですが、後で自然変換が出てくるので混乱しそうです。とりあえず、味も素っ気もない「準同型」で。
部分閉構造のあいだの準同型は関手と似てますが、実際、デカルト積による対称モノイド圏Cによる豊饒圏のあいだの豊饒関手となっています。部分圏としての埋め込みが豊饒関手の対象部分、Tが豊饒関手の射部分を与えます。
2つの部分閉構造Φ、Ψのあいだに準同型 T:Φ→Ψ が存在するとき、ΨはΦを模倣可能だと言うことにします。ΦとΨを言語処理系だと考えると、Φで出来ることは何でも(Tを通して)Ψでも出来ることです。ΨのほうがΦより計算能力が高いとも言えます。
状態遷移系のあいだの模倣(simular)関係という概念があります。ここの模倣も似たようなものですが、simulationよりemulationという言葉を使ってemulatableがふさわしいかと; ある機械の上で別の機械を真似るソフトウエアはエミュレータと呼びますからね。
デカルト圏C上の部分閉構造(partially closed structure)の全体を PartiallyCS(C) とすると、準同型を射とみなして PartiallyCS(C) は圏となります。先に注意したように、部分閉構造は、C-豊饒圏の特殊なものなので、PartiallyCS(C)⊆C-Cat となります。ここで、C-Cat はC-豊饒圏の圏です。
PartiallyCS(C) は“豊饒圏の圏”の構造を持つことから、自然変換に相当する概念を定義すれば、PartiallyCS(C) を2-圏となります。そして圏同値の概念を定義できます。これは、模倣可能性に関連する同値関係となります。
続きの予定
今日は時間と気力がなくなったので、ここまでにします。
部分閉構造を豊饒圏とみなして比較する方法はなかなかに便利で良いなー、と思ってます。詳しい状況をチェックしてないところがあるので、もう少し調べてみます。
いま、2つの部分閉構造Φ、Ψのあいだに模倣可能性という関係を定義したのですが、それとは別に記述可能性という概念を導入します(次回に)。ΨがΦを記述可能なら、ΨはΦを模倣可能です。
部分閉構造のあいだの模倣可能性と記述可能性を使うと、メタ巡回構造の定式化ができます。この定式化は、僕としては納得感があるし、現実への適用もしやすいと感じています。