積分を入れたラムダ計算状況編 - 檜山正幸のキマイラ飼育記 (はてなBlog)

今回のラムダ期の課題は、デカルト閉とは限らない非標準な状況でのセマンティック駆動なラムダ計算かな。

セマンティック駆動なラムダ計算とは、まず意味領域があって、その意味領域における計算をするためにラムダ式やシーケントを手段として使う計算法のことです。構文には必ず意味が付いていて、記号計算の体系が主役ではありません。

「ラムダ計算と積分計算」で述べた“積分を入れたラムダ計算”は、セマンティック駆動なラムダ計算の良い事例となり、プレイグラウンド／練習場を提供します。ラムダ計算にとって、何が必要なのかを調べる素材にもなります。

積分付きのラムダ計算は、通常のラムダ計算からすると変わった状況での計算になります：

計算の舞台がデカルト閉圏ではない。
複数の圏を行ったり来たりして計算する。

このような状況について説明します。ある程度はself-containedになるように、「ラムダ計算と積分計算」との重複を厭わずに記します。一風変わった状況でもラムダ計算が成立することは、ラムダ計算の守備範囲の広大さを示唆します。

内容：

コンパクト領域の圏
コンパクト領域の、バナッハ空間への指数作用
指数対象と評価射
カリー化と反カリー化
バナッハ空間へのコード化と脱コード化エンジン

コンパクト領域の圏

ユークリッド空間としてのRⁿの部分集合Xで、次の性質を持つものを考えます。

Xはコンパクトである。
値が1である定数関数のX上でのn次元積分が値を持ち、正である*1。

このようなXをコンパクト領域と呼ぶことにします。コンパクト領域は、Rⁿから受け継いだ距離で距離空間になります。コンパクト領域を対象として、コンパクト領域のあいだの連続写像を射とする圏をCompRgnとします。

X⊆Rⁿ、Y⊆R^m のとき、直積 X×Y⊆R^n+m は再びコンパクト領域になります。圏CompRgnは、この直積によりデカルト圏になります。1点からなる集合は、0次元ユークリッド空間R⁰の部分集合なのでコンパクト領域です（1点空間の0次元体積は1です）。1点からなるコンパクト領域をI（大文字アイ）で表しましょう。Iは、圏CompRgnの終対象であり、直積の単位対象でもあります。

コンパクト領域XからYへの連続写像の全体であるホムセットCompRgn(X, Y)に距離を入れようと思えばできます。しかし、作った距離空間が有限次元ユークリッド空間に埋め込めるとは限らないので、距離化はやりません。つまり、圏CompRgnはデカルト圏ですが、デカルト閉圏にはなりません。

距離空間と（距離に関する）連続写像の圏をMetとすると、CompRgnはMetの充満部分圏になります。Metも直積と終対象を持つデカルト圏ですが、微妙な違いがあります。Metにおいては、直積に入れる距離は一意には決まりません。CompRgnでは、X×Y⊆R^n+m と考えるので、直積上の距離はユークリッド距離として確定します。

直積上の距離を用途により（同値な範囲で）変更したいこともあるので、Met全体で「直積上の標準的な距離」を決めることはしません。同値な範囲で距離を取り替えても、連続写像の概念に差は出ないので困ることはないでしょう。

コンパクト領域の、バナッハ空間への指数作用

Banはバナッハ空間と有界線形写像の圏だとします。Banの対象をV, Wなどで表します。Banの射を表すには、φ、ψなどのギリシャ小文字を使います。

Xをコンパクト領域、VをR上のバナッハ空間とします。XもVも距離空間なので、両方とも距離空間とみなして、そのあいだの連続写像の全体 Met(X, V) を考えることができます。より正確に言えば、包含（標準埋め込み）関手を J:CompRgn→Met、忘却関手を U:Ban→Met として、Met(J(X), U(V)) が連続写像の空間です。正確に書いていると長ったらしいので、C(X, V) := Met(J(X), U(V)) とします。C(X, V)という記法において、XとVが別の圏に由来する点には注意してください。

集合 C(X, V) には一様ノルム（最大値ノルム）を入れてバナッハ空間にすることが出来ます。こうして作ったバナッハ空間を [X, V]、または V^X と書きます。次の同型が成立するので、[X, V] は指数と言えます。

[Y, [X, V]] $\stackrel{\sim}{=}$ [Y×X, V] $\stackrel{\sim}{=}$ [X×Y, V] in Ban
[I, V] $\stackrel{\sim}{=}$ V in Ban

空な領域と直和を考えれば次も成立します。

[ $\emptyset$ , V] $\stackrel{\sim}{=}$ {0} in Ban
[X + Y, V] $\stackrel{\sim}{=}$ [X, V] $\oplus$ [Y, V] in Ban

ただし、今回は空な領域 $\emptyset$ や直和+は考えません。

E(X, V) := [X, V] = V^X として、E:CompRgn^op×Ban→Ban という関手を定義できます。つまり、射に対して対応を拡張できて、CompRgnに関しては反変、Banに関しては共変の二項関手Eを定義できます。この二項関手Eは前述の“指数法則”を満たすので、底と指数（右肩のパラメータ）が異なる圏を走る“指数関手”です。しかし、これは圏Banの内部ホムではありません。

独白補足：バナッハ空間圏の内部ホム

V, Wをバナッハ空間として、圏BanのホムセットBan(V, W) は、VからWへの有界線形写像の全体です。ψ∈Ban(V, W) には、作用素ノルム（単位ノルム球の伸縮率の上限） $||\psi||$ を定義できて、このノルムを使ってBan(V, W)をバナッハ空間に出来ます。出来たバナッハ空間を [V, W] とします。Xがコンパクト領域のときの [X, V] と同じ記号ですが、文脈で区別してください。

今定義した [V, W] においては、VもWもBanの対象なので、Banの内部ホムと言っていいと思います。しかし、Banをデカルト閉圏にするためには、次の等式を成り立たせるテンソル積が必要です。

Ban(V $\otimes$ W, S) $\stackrel{\sim}{=}$ Ban(V, [W, S])

テンソル積の代数的な特徴付けは有限次元ベクトル空間のときと同じで、V×W→S という双線形写像を線形化するような空間でしょう。問題はノルムと完備性で、難しそうです。

おそらく、頑張ればBanをデカルト閉圏にできるのでしょうが、今回は圏Banのなかでラムダ計算をするわけではないので、Banがデカルト閉圏である必要はありません。

指数対象と評価射

通常、ラムダ計算のモデルとしてはデカルト閉圏を考えます。今の状況では、CompRgnもMetもBanもデカルト閉圏ではありません。

ラムダ計算では、指数対象と評価射（適用射）がとても重要な役割を担っていて、デカルト閉圏にはそれらが作り付けになっています。見方を変えると、指数対象と評価射が存在すれば、計算の舞台が必ずしもデカルト閉圏である必要はないとも言えます。

今の状況では、指数対象はBan内に存在する [X, V] です。ここで、Xはコンパクト領域なので、Banの対象ではありません。[X, V]×X を作るために、忘却関手 U:Ban→Met を使って、[X, V] をMetに持ってきます。コンパクト領域XはもともとMetに入っているので、Met内で評価射 ev_X,V:U([X, V])×X→U(V) を作ることができます。

評価射evは、「関数に引数を渡して値を求めること」で、Met内で定義するのは簡単です。ただし、Metのなかで考えているので、evが距離に関する連続写像であることを確認する必要はあります。evの連続性は次のことを意味します。

引数であるXの値を少し動かしたら、関数値も少し動くだけ。
関数コードであるバナッハ空間[X, V]のベクトルを少し動かしたら、関数値も少し動くだけ。

「関数コード」という言葉を使ったのは、連続関数の情報をバナッハ空間のベクトルにコード化しているからです（後でまたコード化に触れます）。

カリー化と反カリー化

カリー化／反カリー化がないと、さすがにラムダ計算は無理でしょう。カリー化は、関数の独立変数の個数を減らして、代わりに値を関数空間に取るようにすることです。反カリー化はその逆、高階関数から多変数関数にする操作です。カリー化／反カリー化こそ、ラムダ計算のキモなんだろうと思います。

今の状況で、カリー化／反カリー化は次の形で存在します。

C(X×Y, V) $\stackrel{\sim}{=}$ C(X, [Y, V])

ここで、C(-, -) はホムセットではないので、(-)×Y と [Y, -] の随伴としての解釈がそのままでは通用しません。よくわからないので、この点はほっておきます。

上記の（集合としての）同型を与える写像を大文字ラムダで書いて Λ_X,Y,V:C(X×Y, V)→C(X, [Y, V]) in Set とします。f∈C(X×Y, V) のとき、fは2変数のV値関数です。Λ(f)は、1変数の[Y, V]値関数です。[Y, V]はBanの対象なので、x∈X に対する Λ(f)(x) はバナッハ空間のベクトルです。w = Λ(f)(x)、w∈[Y, V] と置いたときに、

ev(w, y) = f(x, y)

が成立します。これは、ラムダ計算を成立させている根本となる最重要公式です。構文的ラムダ計算におけるベータ変換の、意味論的な対応物です。圏論の記法で正確に書けば：

(Λ_X,Y,V(f)×id_Y);ev_Y,V = f

さてここで、g∈C(X, [Y, Y]) に対して、Γ(g) := (g×id_Y);ev_Y,V と定義すると、Γ:C(X, [Y, V])→C(X×Y, V) となり、次が成立します（上の等式の書き換え）。

Γ(Λ(f)) = f

いま定義したΓはΛの逆写像を与えていて、Λ(Γ(g)) = g も成立します。詳しく書けば：

Λ_X,Y,V((g×id_Y);ev_Y,V) = g

こちらのほうはイータ変換に対応します。ここらへんの話は次の記事にも書いてあります。

評価射（適用射）が重要なのは、カリー化の逆写像＝反カリー化Γ＝Λ^-1を具体的に与える道具だからです。構文的なラムダ計算で重要なベータ変換／イータ変換はそれぞれ、Λ^-1(Λ(f)) = f と Λ(Λ^-1(g)) = g という、Λの同型（双射）性の主張に対応します。

独白補足：積分を知らないので一般化がよく分からない

とりあえず、距離に関する連続関数の集合C(X, V)を基本に据えます。これは、関数の積分を考えるとき、C(X, V)→V という形の積分なら普通に定義できるだろう、と思ってです。Vはバナッハ空間ですが、バナッハ空間値関数の（ルベーグ流）積分はボッホナー積分（Bochner integral）と呼ぶそうです（知らなかった）。

C(X, V)→V とか C(X, [Y, V])→[Y, V] という積分はボッホナー積分になるでしょうが、なんであれ積分て、単関数による近似を使うんですよね。単関数は連続とは限らないので、C(X, V)より広い空間で近似操作を行うことになります。だったら最初から C(X, V) より広い空間をホムセットに採用すればいいのかな、と思ったりするのですが、広い空間がハッキリしません。

「Xがコンパクト」という条件も外したいので、なにか適切な空間H(X, V)があって、非コンパクトXでも定義できて、積分 H(X, V)→V もある、となると具合がいいんですけど。なんだったら、外の圏Metからして取り替えてもいいし。

バナッハ空間へのコード化と脱コード化エンジン

以下、バナッハ空間の要素はバナッハベクトルと呼ぶことにします。

我々の今の立場では、“関数”とは集合C(X, V)の要素のことです。C(X, V) := Met(J(X), U(V)) なので、定義域XはCompRgnの対象、値域VはBanの対象です*2。“関数”はMetの射、距離空間のあいだの連続写像ですね。

f∈C(X, V) に対して、fのフルカリー化Λ^full_X,V(f)は C(I, [X, V]) に入りますが、集合の同型 C(I, [X, V]) $\stackrel{\sim}{=}$ [X, V] を経由して、fのフルカリー化をバナッハベクトルとみなせます。

コンピュータがらみでセマンティックなラムダ計算を考える場合は、Λ(f) は「関数fのコード」になっています。例えば、計算可能関数fに対してfを実現（理想的コンパイル）した実行可能バイナリデータがΛ(f)です*3。ゲーデル符号化も同じことです。“働き”としての関数をコード化／データ化することがカリー化であり、指数対象がコード空間を与えます。

コード化／データ化された関数を“働き”として再現する機構が評価射で、ハードウェア／仮想マシン／インタープリタ／eval関数などに相当します。評価射は、“コード化された関数”（データ）と関数への“引数データ”の2つのデータを受け取ってもとの関数の値を計算します。この脱コード化エンジンが反カリー化の実体であることは納得できるでしょう。

若干比喩的な表現ではありますが、“働き”としての連続関数（C(X, V)の要素）をコード化／データ化したモノがバナッハベクトル（[X, V]の要素）と言えます。バナッハベクトルという“コード化された関数”（データ）と、コンパクト領域の点という関数への“引数データ”を受け取ってもとの連続関数の“働き”を再現するのがMetにいるevです。

今の状況に関して言えば、カリー化はバナッハ化であり、反カリー化は反バナッハ化＝バナッハ構造の忘却です。3パラメータのカリー化 Λ_X,Y,V:C(X×Y, V)→C(X, [Y, V]) の場合は、f∈C(X×Y, Y) をY方向にバナッハ化するので、独立変数はコンパクト領域Xを走る変数だけとなり、点xでのΛ(f)の値はバナッハ化されたy変数関数＝バナッハベクトルとなります。

以上の状況で計算を遂行するための半形式的体系を準備するのが次のステップです。「半」なのは、スタンドアロンの記号計算系が目的ではないので、セマンティックに依存したインフォーマル計算も許していいと思うからです。もちろん、物事が曖昧にならない程度の形式性は求めます。

*1:Xは正の体積を持つわけですが、他の条件も付けておいたほうが便利かも知れません。例えば、X⊆(Xの内部の閉包）とすると、毛が生えたような図形を除外できます。

*2:値域という言葉は注意が必要かも知れません。写像の像（イメージ）を値域と言うこともあるからです。始域／終域という言葉もあります。

*3:この説明で注意すべきは、バイナリデータをバイト比較すると、イータ変換が成立しない可能性があることです。現実世界では、関数の外延性の確認や保証は困難です。