ラムダ計算と積分計算 - 檜山正幸のキマイラ飼育記 (はてなBlog)

ラムダ抽象と定積分を混ぜた計算をしていたら、次の公式が欲しくなったのです。

$\lambda x. \int_{y\in Y} f(x, y) dy = \int_{y\in Y} \lambda x. f(x, y)\, dy$

見た目の上では、「ラムダ束縛と積分記号を交換してもいいよ」という形で覚えやすいんですが、これが何を意味しているかハッキリしない。なんだこれは？と思って考えたら、思いのほか事情は複雑でした。

内容：

連続関数の空間
ラムダ計算
定積分
カリー化と定積分
解釈
なんで「偏積分」はないの？

連続関数の空間

Xをコンパクト距離空間、Vはバナッハ空間として、C(X, V) をXからVへの連続関数の全体とします。こう書くと、C(X, Y) がなんかの圏のホムセットのように見えますが、そうではないのです。距離空間とバナッハ空間という概念が出てくるので、距離空間の圏とバナッハ空間の圏を考えてみると、C(X, V) は異なる圏の対象をパラメータに持っています。何だか奇妙です。

事情をハッキリさせるために、状況設定をします。距離空間の圏をMet、バナッハ空間の圏をBanとしましょう。Metの射は、距離空間のあいだの連続写像、Banの射は有界線形写像だとします。Metの部分圏CompMetは、コンパクト距離空間を対象とする充満部分圏とします。

先に定義した C(X, V) のXとVを動かすなら、C(-, -):|CompMet|×|Ban|→|Set| という対応が出来て、C(-, -) は異なる圏にまたがったホムセットもどきです。BanからMetへの忘却関手があるので、それをUとすると、C(X, V) = Met(X, U(V)) とは書けます。

Met(X, U(V)) として定義した C(X, V) は単なる集合ですが、XとVの構造を利用すると、集合 C(X, V) にバナッハ空間の構造を与えることができます。出来たバナッハ空間は、C(X, V) とは区別して [X, V] と書くことにします。C(X, V)∈|Set|、[X, V]∈|Ban| です。

XとYをコンパクト距離空間として、次の集合は意味を持ちます。

C(X×Y, V) = Met(X×Y, U(V))
C(X, [Y, V]) = Met(X, U([Y, V]))

集合の同型 C(X×Y, V) $\stackrel{\sim}{=}$ C(X, [Y, V]) は示せるので、この同型を使ってラムダ計算ができます（後でやります）。

しかし、C(X×Y, V) $\stackrel{\sim}{=}$ C(X, [Y, V]) が、(-)×Y と [Y, -] の随伴を表しているわけではありません。C(-, -) は略記で、実際は Met(X×Y, U(V)) $\stackrel{\sim}{=}$ Met(X, U([Y, V])) です。しかも、X, Yに制限が付くし、Vは他の圏の対象だし。

C(-, -)を CompMet^op×Ban→Set の関手と考えることはできるので、Cはプロ関手になります。これを利用して気が利いた定式化ができるのでしょうか？ウーン、よく分かりません。

ラムダ計算

ともかく、集合の同型 C(X×Y, V) $\stackrel{\sim}{=}$ C(X, [Y, V]) はあるので、カリー化は定義できます。Λ_X,Y,V:C(X×Y, V)→C(X, [Y, V]) としましょう。このΛがカリー化です。Λは集合のあいだの双射となり、逆写像があります； Λ^-1_X,Y,V:C(X, [Y, V])→C(X×Y, V)。Λ^-1 のほうは反カリー化 と呼びます。

記号的な計算をするために、f:X×Y→V を (x:X, y:Y |→ f(x, y)) と書きます。変数x, yの変域X, Yが了解されていれば、(x, y |→ f(x, y)) でもかまいません。さらに、誤解がないなら単に f(x, y) とも書きます。ただし、ほんとに f = f(x, y) なのではありません。記号の乱用です。(x:X, y:Y |→ f(x, y)) は、大きなラムダ式（型判断、型シーケント）で、まじめに形式的計算をするなら絶対に必要ですが、普通は記号の乱用で済ませています。

f:X×Y→V に対する Λ_X,Y,V(f) を (x:X |→ λy:Y.f(x, y)) と書きます。矢印の右に現れる項 λy:Y.f(x, y) を、f(x, y)のラムダ抽象と呼びます。変域Yの変数yは束縛されますが、変数xは自由変数として残ります。ラムダ項（小さなラムダ式）では自由なxも、外側の大きなラムダ式により束縛されています。

カリー化のオペレータ Λ_X,Y,V:C(X×Y, V)→C(X, [Y, V]) は、ラムダ抽象とだいたい同じことです。ここでは（異なる用語法もありますけど）、カリー化が写像を意味するのに対して、ラムダ抽象は記号の操作のことです。カリー化は意味領域の存在、ラムダ抽象は構文領域の存在です、とりあえず。

3つのパラメータ（インデックス）を持つ Λ_X,Y,V に対して、2つのパラメータの Λ_X,V を次のように定義します。



  C(X, V)  C(I×X, V)   Λ_I,X,V:C(I×X, V)→C(I, [X, V])

  ------------------------------------------------------[ = ]

  Λ_X,V:C(X, V)→C(I, [X, V])

この図の意味は、上段と下段が等しいことで、上段により下段が定義されていることになります。上段を見ると、C(X, V) と C(I×X, V) の同型がありますが、ここで、Iは単元集合（を距離空間とみなしたもの）です。横に並んだ、C(X, V)→C(I×X, V) （同型）と C(I×X, V)→C(I, [X, V]) （カリー化、これも同型）を繋いだものが下段の写像を与えます。

以上で定義された2パラメータのΛは、「0引数関数と定数は同じなのか？：圏的ラムダ計算の立場から考える」で出したフルカリー化です。必要があれば、Λ^fullという記法で3パラメータのΛと区別します。

定積分

今まで、X, Yなどはコンパクト距離空間としてきましたが、定積分をしたいので、X, Yなどはユークリッド空間Rⁿに埋め込まれていて、タチのよい図形になっているとします。バナッハ空間Vに対する f:X→V は、Xを含むRⁿの開集合上で定義された連続関数のXへの制限で定義すればいいでしょう。具体的な詳細は別にどうでもよくて、要するに、関数fのX上での積分が定義できればそれでいいのです。

カリー化Λ_X,Y,Vと似た感じに、3パラメータのオペレータ ∫_X,Y,V:C(X×Y, V)→C(X, V) を定義します。f∈C(X×Y, V) に対して、∫_X,Y,V(f) は次の式で定義される関数です。

$x \in X \mapsto \int_{y\in Y} f(x, y) dy$

変数yは積分変数（一種の束縛変数）なので結果からは消えますが、xは積分の項内では自由変数で、yに関する積分実行のときには定数扱いされます。その後でxを動かせば、X→V という関数が得られるので、それを ∫_X,Y,V(f) とします。

また、フルカリー化Λ^full_X,Vに似た感じのフル積分オペレータ ∫^full_X,V:C(X, V)→C(I, V) は、X上でのfの積分の値（Vの定数）を、一点Iからのポインティング関数とみなしたものです。集合としては C(I, V) $\stackrel{\sim}{=}$ V なので、フル積分オペレータは、X上の定積分です。

二種類の積分オペレータを使うと、フビニの定理は次の形に述べられます。

∫_X,Y,V;∫^full_X,[Y,V] = ∫^full_X×Y,V

カリー化と定積分

二種類のカリー化と二種類の積分オペレータが準備できたので、これらのあいだの関係を述べることができます。矢印の可換図式の代わりに、上段と下段が等しいことを示す図を使います。



  Λ_X,Y,V:C(X×Y, V)→C(X, [Y, V])  ∫^full_X,[Y,V]:C(X, [Y, V])→C(I, [Y, V])

  --------------------------------------------------------------------[ = ]

  C(X×Y, V)  C(Y×X, V)  ∫_Y,X,V:C(Y×X, V)→C(Y, V)

  Λ^full_Y,V:C(Y, V)→C(I, [Y, V])

C(I, [Y, V]) $\stackrel{\sim}{=}$ [Y, V] の同一視のもとで、上段は次の式で表現できます。被積分関数は、連続関数のバナッハ空間に値を取る1変数関数です。

$f \mapsto \int_{x\in X} \lambda y. f(x, y) dx$

下段は次のよう。ラムダ抽象した結果はバナッハ空間のベクトルだとみなします。

$f \mapsto \lambda y. \int_{x\in X} f(x, y) dx$

通常の式で表すと、下段にある変数のスワップ C(X×Y, V) $\stackrel{\sim}{=}$ C(Y×X, V) は陽には見えなくなります。結局、次の等式になります。この等式は、バナッハ空間[Y, V]のなかでの比較です。

$\int_{x\in X} \lambda y. f(x, y) dx = \lambda y. \int_{x\in X} f(x, y) dx$

xとyの役割を入れ替えれば、冒頭に挙げた公式です。

解釈

記号の意味が分かってしまえば、解析の知識がある人なら（適当な前提を付けて）等式を証明できるでしょう。僕は解析の知識がないのでよく分かりません。しかし、変数yを離散化すれば：

$\lambda x.(\sum_{j \in J} f_{j}(x)) \:=\: \sum_{j \in J}(\lambda x. f_{j}(x))$

これは、「パラメータ付き値列の総和を、そのパラメータの関数とみなしたものは、関数列の総和を与える」と読めるので、番号jをなんとかして連続変数yに持っていけば、和を積分に変えた等式も成立するでしょう。

なんで「偏積分」はないの？

以下、余談。

"partial differential"の訳語は「偏微分」で、"partial integral"の訳語は「部分積分」です。partial differential と partial integral に直接的な関係はないので、この訳語の選択は適切だと思います。結果的に、「偏積分」という言葉は使われずに残っています。

先に定義した∫_X,Y,Vというオペレータは、Y方向にだけ積分を実行して、Xはパラメータとして残るものです。2つの変数のうちの片一方についてだけ積分するので、「偏積分」という言葉ば∫_X,Y,Vにピッタリな気がします。

この「偏積分と呼びたい操作」は、普通は何と呼ぶのだろう？ひょっとして呼び名がない？多重積分は、むしろフル積分の意味だし、逐次積分は繰り返しやる行為っぽいし、線積分はパラメータで束ねることはしないし。