圏論的指数の定義 - 檜山正幸のキマイラ飼育記 (はてなBlog)

背景の説明に労力を使って疲れたので、Exerciseの解は示しません（今日のところは）。

解を示します、明白・露骨・丁寧に。

問題の記述

次の図式を便宜上Dとおきます。id_Aを単にAと書いています。B^AはB^A（指数）のことです。



         f

 C×A -----→ B

  ｜        ／

  ｜m×A  ／eval

  ｜    ／

  ↓  ／

B^A×A

それで、以下のような3つの命題を考えます；ただし、f:C×A→B, m:C→B^A, eval:B^A×A→B であることは前提とします。Λは集合論的関数C(C×A, B)→C(C, B^A)であり、Λ(f)∈C(C, B^A)なので、圏C内で Λ(f):C→B^Aです。

[β] ∀f. (Λ(f)×A);eval = f
[η] ∀m. Λ((m×A);eval) = m
[exp] ∀f.∃!m. Comm[D]

記号「∀f.」は「任意のfに対して…」を意味し、記号「∃!m.」は「…であるmがただ1つだけ存在する」を意味します。Comm[D]は、「図式Dが可換になる」ということ。

今回示すべきことは：

[β]かつ[η] ならば [exp]
[exp] ならば [β]
[exp] ならば [η]

の3つです。まとめて書けば：

[β]かつ[η] ⇔ [exp]

ですね。

[β]かつ[η] ならば [exp]

Comm[D]を等式に書き換えれば、(m×A);eval = f なので、示すべきは、

[exp'] ∀f.∃!m. (m×A);eval = f

です。

mの存在に関しては、与えられたfに対して m = Λ(f) と置けば、[β]から (m×A);eval = f が言えるのでOK。

次に一意性。m と m' が当該の等式を満たす射だとします。つまり、

(m×A);eval = f
(m'×A);eval = f

この2つの等式の両辺にΛを作用させると、

Λ((m×A);eval) = Λ(f)
Λ((m'×A);eval) = Λ(f)

[η]から、Λ((m×A);eval) = m と Λ((m'×A);eval) = m' が言えるので、

m = Λ(f)
m' = Λ(f)

したがって、m = m'。

[exp] ならば [β]

[exp]は、fを受け取りmを返す関数（一意的対応）の存在を主張しているので、その関数をΛと置きます。すると、m = Λ(f)。Λ(f)を使って[exp']を書き換えれば、

∀f. (Λ(f)×A);eval = f

これは[β]に他なりません。

Λが双射であること

[β]と[η]では、集合論的関数Λが最初から与えられてましたが、[exp]にはΛが登場しません。しかし、[exp]の主張は、C(C×A, B)→C(C, B^A)という集合論的関数を定義しているので、これをΛと書くことにします。このΛは、双射（可逆）になります。ここでそれを示しておきましょう。

任意のm∈(C, B^A)に対して、Γ(m) = (m×A);eval とすれば、Γ(m)∈C(C×A, B)なので、Γ:C(C, B^A)→C(C×A, B) という集合論的関数が定義できます。

f = Γ(m) と置くと、Γの定義よりただちに、

(m×A);eval = f

ところが[exp]より、上の等式を満たすmは一意的に決まり、m = Λ(f) なのでした。m = Λ(f) と f = Γ(m) より、

m = Λ(Γ(m))

次に、Γ(Λ(f)) をΓの定義にしたがって計算すると、(Λ(f)×A);eval ですが、[β]（[β]は[exp]から出ます）より、(Λ(f)×A);eval = f。これより、

Γ(Λ(f)) = f

以上から、Γ = Λ^-1 であり、Λが双射であることがわかりました。

[exp] ならば [η]

[exp]から定義されるΛは双射なので、全射（上射）でもあり、次が成立します。

[surj] ∀m.∃f. m = Λ(f)

[surj]が成立しているので、適当なf（実は一意的に決まる）を選んで、mをΛ(f)と書きます。すると、示すべき等式 Λ((m×A);eval) = m は、Λ((Λ(f)×A);eval) = Λ(f) だと思ってもいいことになります。ところが、[β]を使えば、等式 Λ((Λ(f)×A);eval) = Λ(f) は出ます。[exp]から[β]が出るのはもうわかっているので、[exp]から[η]が導かれました。

逆コンパイラ＝インタプリタ＝アンカリー化

「圏論的指数の周辺：ラムダ計算、デカルト閉圏、ノイマン型コンピュータ」において、Λをコンパイラに例えました。コンパイラの逆関数は逆コンパイラと呼んでもいいでしょう。ただし通常の用語法では、逆コンパイラは、関数のコンパイル済みコードから関数のソースコード（記述）を生成しますが、この場合は関数そのものを生成します。

関数そのものとはつまり、引数を渡して値を返す機能性ですから、コンパイル済みコードのインタプリタ（実行系）と同じことになります。我々人間は、関数の記述を通してしか関数を把握できないので、インタプリタを逆コンパイラだとは認識しにくいのですが、記述無しでも関数そのものを把握できる者なら、インタプリタの機能を「コンパイル済みコードから関数を再現する装置」とみなすでしょう。

ところでコンパイラΛ:C(C×A, B)→C(C, B^A)は、カリー化を与えているので、逆コンパイラΛ^-1:C(C, B^A)→C(C×A, B) はアンカリー化です。結局、「逆コンパイラ＝インタプリタ＝アンカリー化」ってわけです。