微分計算、ラムダ計算、型推論 - 檜山正幸のキマイラ飼育記 (はてなBlog)

微分の計算は色々な場面で必要です。が、微分の記号である $\frac{d}{dx}$ や $\frac{\partial}{\partial x}$ が入った式の解釈って難しいですね。式の型〈type〉が分かりにくいのです。実際、原理的に型が判断できない式が使われることがあります。にもかかわらず、「分かる人には分かる」のは、暗黙のお約束や習慣的手順が駆使されるからです。

僕は、暗黙のお約束や習慣的手順が嫌いなので、ハッキリした計算方法を示したいと思います。現状の記法の問題点と対処法を知りたい方は、前半をテキトーに読み飛ばして、後半の3つの節を読めばいいと思います。

事前にラムダ計算について少し知っているほうがいいでしょう。JavaScriptや絵を使って説明した記事は：

ラムダ計算をJavaScript側に寄せるとどうなるかは（興味があれば）：

JavaScriptに近いラムダ計算系

もっと詳しい構文論（今回はそこまで必要ないけど）は：

内容：

微分計算の構文
型システム
型判断と型推論
解釈不可能／困難な式の例
何がダメなのか
どうすればいいのか

微分計算の構文

この記事の目的は、ちゃんとした形式的体系を構成することではなくて、普通の微分計算の手順を明確化することです。なので、構文に関しては大雑把に記します*1。

出てくる基本記号は：

特定の値を表す定数記号： 0, 1, -10.2, π（円周率）など
特定の関数を表す関数記号： sin, cos, exp, log など
変数記号（関数を表す変数もある）： x, y, a, f, k など

演算子記号も関数記号の一種だとみなします。例えば、足し算の'+'、掛け算の'×'なども関数記号です。演算子記号は、書き方として中置を許す関数記号です。サイン関数の'sin'、対数関数の'log'などは、語（文字の並び）全体でひとつの関数記号です。

基本記号から出発して式（項）を組み立てるやり方は：

適用： E, F が式のとき EF または E(F) は式になる。
タプル： E₁, ..., E_n がn個の式のとき、(E₁, ..., E_n) は式になる。
ラムダ抽象： Eが式で、ξ₁, ..., ξ_n がn個の変数のとき、λ(ξ₁, ..., ξ_n).E は式になる。

適用 EF とは、Eを関数（を表す式）とみなして、Fでの値を表します。ラムダ計算では、併置（単に並べる）で表しますが、日常的な記法では E(F) が多いでしょう。例を幾つか挙げます。なお、常識的に使っている略記は許すことにします、2×x + 1 を 2x + 1 、x×x + y×y を x² + y² とか。

関数	引数	括弧なし適用	括弧あり適用
sin	x	sin x	sin(x)
sin	2x + 1	sin 2x + 1 解釈困難	sin(2x + 1)
f	(x, y)	f(x, y)	f((x, y)) くどい感じ
λ(x, y).(x² + y²)	(1, -1)	λ(x, y).(x² + y²)(1, -1)	λ(x, y).(x² + y²)((1, -1))

[追記][補足]「ニ変数関数と、ペアの一変数関数は違うのではないか？」という疑問はもっともなものであり、実際違います。ただし、これらを区別しなくても問題がない場合が多い、ということです。

いつでも問題がないかというと、そうではありません。「ニ変数関数と、ペアの一変数関数を区別しないとダメ」な状況はあります。そんなときは、n変数関数とn-タプルの1変数関数を区別する計算システムの構文論と意味論を組み立てて使います。今回はその労力をはらっていません。[/補足][/追記]

ここで、構文を論じるときのカナメでありながら混乱しがちな“メタ変数”について注意しておきます。

今話題にしている計算体系で使う変数は、x, y, a, f, k などのラテン文字小文字だとしました。変数が足りなくなったら、x1, x2, x3 のような番号付けもしていいとします。一方、変数を表す変数（メタ変数）には、ξ, η などのギリシャ文字小文字を使用します。ξ₁, ξ₂ などの下付き添字も使います。変数を表すメタ変数以外に、式〈項〉を表すメタ変数として、E, F, E₁, E₂ などのラテン文字大文字（と下付き添字）を使います。

メタ変数ξの具体的な値として変数xや変数fがあります。メタ変数Eの具体的な値として式 sin(2x + 1) や式 x² + y² があります。実際に使う“構文”と、構文を記述する“メタ構文”はゴッチャになりがちだし、面倒なのであまり区別しないこともありますが、概念的には別物です。

これから微分計算をする心積もりなので、通常のラムダ計算に次の構文要素を付け加えます。

D₁, D₂, .... という無限個の作用素記号
Dλ という束縛子〈binder〉記号。

D_i（i = 1, 2, ...）の意味は偏微分作用素です。Dλは2文字でひとつの記号です。直後に変数を伴って、変数を束縛します。微分ラムダ束縛子〈differential lambda binder〉と呼んでおきましょう。偏微分作用素と微分ラムダ束縛子が使えるようになったので、式（項）を組み立てるやり方も追加します。

偏微分： E が式のとき D_iE は式になる。
微分ラムダ： E が式、ξが変数のとき、Dλξ.E は式になる。

例えば、D₁λx.(x²)、D₂λ(x, y).(x² + y²)、Dλt.(r×sin(at + b)) + 1 などは、すぐ上のルールで作られた式です。一変数関数の微分作用素も、偏微分作用素D₁を使います。つまり、d/dx と ∂/∂x は特に区別しない流儀です*2。

微分ラムダ束縛子Dλの変数束縛のルールは、通常のラムダ束縛子λと同じです。λまたはDλで束縛された変数を束縛変数〈bound variable〉と呼び、束縛されてない変数を自由変数〈free variable〉と呼びます*3。

型システム

前節では型に触れませんでしたが、変数は、すべて型が指定されているとします。変数の型を宣言した形 ξ₁:α₁, ..., ξ_N:α_N を型コンテキスト〈type context〉、混乱がなければ単にコンテキスト〈context〉と呼びます。ここで、ξ₁, ..., ξ_N はN個の変数、α₁, ..., α_N はN個の型項（後述）です。

式〈項〉は、常に型コンテキスト付きだとします。式の内部で型が指定されなくても、型コンテキストには型情報が必須です。型が不明の変数は絶対に許しません。束縛変数の型指定は注意が必要です。束縛変数では、(λx.x(0))(λx.(2x + 1)) のように、違った型で同名の変数が使えます。こんなときは、型コンテキストでxの型を指定することはできません。束縛変数をリネーム（アルファ変換〈α-conversion〉ともいう）するか、ラムダ束縛内で型指定をします*4。

(λx:(R->R).(x(0)))(λx:R.(2x + 1)) （Rは実数の型を表す型記号とする）

型を表す式を型項〈type term〉と呼びます（型式〈かたしき〉でもいいんだけど、「けいしき」と読まれそうなので）。型項を作るための基本記号は：

特定の型を表すための型定数〈型名〉：実数型を表すR、ユニット型〈シングルトン型〉を表すI〈大文字アイ〉は入れておきます。他にも適宜追加してかまいません。
型構成子記号： ,〈カンマ〉, ->〈アロー〉, ⊗〈テンソル積記号〉, ^*〈上付きアスタリスク〉, [,]〈ブラケットとカンマ〉, vec〈ベクトル型構成子〉
補助記号：丸括弧

型項は、型定数をベースに、型構成子を施して作っていきます。⊗〈テンソル積記号〉, ^*〈上付きアスタリスク〉が分かりにくいなら無視してしまってかまいません。今回は使いませんから。A, B を追加した型定数だとして型項の例を挙げれば：

R
(A, R)
(A, R)->B
((A, R)->B)->R
I->(A, B)
vec(A)⊗(R, R)^*
A->[vec(A), vec(B)]

型項の意味を記述するために、スコットブラケット〚〛を使うことにします。まず、

〚R〛 = R
〚I〛 = 1 = {0}

これは、記号'R'の意味は実数の集合R、記号'I'の意味はシングルトン集合 {0} だということです。型項を表すメタ変数にギリシャ文字小文字（の初めのほう）を使うとして、型構成子の意味は：

〚α, β〛 = 〚α〛×〚β〛（直積）
〚α->β〛 = Map(〚α〛, 〚β〛) （写像の集合）
〚α⊗β〛 = 〚α〛 $\otimes$ 〚β〛（ベクトル空間のテンソル積空間）
〚α^*〛 = 〚α〛^* （ベクトル空間の双対空間）
〚[α, β]〛 = LinMap(〚α〛, 〚β〛) （ベクトル空間のあいだの線形写像の空間）
〚vec(α)〛 = vec(〚α〛) （後述）

これだけでは分かりにくいでしょうね。追加の説明をします。まず、型のなかにベクトル型〈vector type〉と呼ばれる型があります。型構成子 ⊗（テンソル積空間）、^*（双対空間）、[.]（線形写像空間）は、ベクトル型に対してしか使えません。組み込みの型定数 R, I はベクトル型（の記号）だとします。他に、ベクトル型（の記号）もベクトル型ではない型（の記号）も必要に応じて追加してかまいません。

今話題にしている計算システム／型システムでは、型の意味はベクトル空間の開集合だとします*5。例えば、追加した型（の記号）Aの意味は次だとしましょう。

〚A〛 = {(x, y)∈R² | 0 < x < 1, 0 < y < 1}

vec(A) の意味は、Aが含まれる外のベクトル空間のことです*6。つまり、

〚vec(A)〛 = R²

型項αが、もともとベクトル型（ベクトル空間を意味する型）であるなら vec(α) = α です。

他に注意すべきことをザッと述べると：

3個以上の型項をカンマ区切りで並べたもの（タプル形式）は、3個以上の集合の直積を表します。
型がベクトル型ならば、カンマをベクトル空間の直和と解釈できます。〚α, β〛 = 〚α〛 $\oplus$ 〚β〛。最初から構文に直和記号 ⊕ を入れておいてもかまいません。
アローを使った型項 α->β は写像の集合を表しますが、単なる（なんでもいい）写像ではなくて、微分可能性などの条件が付きます。
ベクトル型から、型構成子 ,（直積または直和）、⊗（テンソル積空間）、^*（双対空間）、[,]（線形写像空間）で作られた型は再びベクトル型になります。

型判断と型推論

型コンテキストを Γ, Δ などのギリシャ文字大文字で表します（これもメタ変数です）。Eを式、αを型項として、Γ ⇒ E :α という形（構文的対象）を型判断〈type judgement〉といいます。論理のシーケントと類似しているので、僕は型シーケント〈type sequent〉とも呼びます。型判断 Γ ⇒ E:α の意味は：

型コンテキストΓのもとで、式Eの型はαである。

例えば、

t:R ⇒ (cos(t), sin(t)) : (R, R)
解釈：変数tの型がR（tは実数変数）ならば、式 (cos(t), sin(t)) の型は (R, R)（実数のペア）である。

ただし、こういう判断ができるためには、cos:R->R, sin:R->R という型宣言も必要です。これもちゃんと書けば：

cos:R->R, sin:R->R, t:R ⇒ (cos(t), sin(t)) : (R, R)

この型判断がいきなり出るのではなくて、次のような型判断の推論過程があります。横線の上段にある型判断（複数でもよい）を仮定して、下段の型判断が結論されます。

  cos:R->R, sin:R->R, t:R ⇒ cos:R->R
  cos:R->R, sin:R->R, t:R ⇒ t:R
 ------------------------------------[適用]
  cos:R->R, sin:R->R, t:R ⇒ cos(t):R


  cos:R->R, sin:R->R, t:R ⇒ sin:R->R
  cos:R->R, sin:R->R, t:R ⇒ t:R
 ------------------------------------[適用]
  cos:R->R, sin:R->R, t:R ⇒ sin(t):R


  cos:R->R, sin:R->R, t:R ⇒ cos(t):R
  cos:R->R, sin:R->R, t:R ⇒ sin(t):R
 ----------------------------------------------------[ペア]
  cos:R->R, sin:R->R, t:R ⇒ (cos(t), sin(t)) :(R, R)

上のように横線の上段から下段を導くことを型推論〈type inference〉といいます。型推論の積み重ねは型証明〈type proof〉ですが、型推論と型証明はあまり区別してないようです。我々が「型について考える」とき、頭のなかで型推論／型証明が行われています。

[補足][追記]ここで言っている型推論は、型コンテキストの情報をもとにして、ラムダ式〈ラムダ項〉の型を計算することです。プログラミング言語における型推論では、逆向きの推論をすることがあります -- 型が未知の記号を含む式を見て、その記号の型宣言を生成することです。

プログラミング言語の機能として話題にのぼる「型推論」は逆向きの推論のほうでしょう。コンパイラが型宣言を生成してくれるなら、プログラマの負担が減ります。順方向の型推論だけだと、事前に型宣言が必要なので、プログラマが型宣言を書かなくてはなりません。[/追記][/補足]

基本となる型推論ルールは、式の構成と並行に定義されます。

  Γ ⇒ E :(α->β)
  Γ ⇒ F :α
 ------------------[適用]
  Γ ⇒ E(F) :β


  Γ ⇒ E :α
  Γ ⇒ F :β
 -----------------------[ペア]
  Γ ⇒ (E, F) :(α, β)


  Γ ⇒ ξ :α
  Γ ⇒ E :β
 ---------------------[ラムダ抽象]
  Γ ⇒ λξ.E :α->β

ペアだけではなく、3個以上のタプルも同様な型推論ルールがあります。ラムダ抽象は、複数の変数を使った抽象 λ(ξ₁, ..., ξ_n).E もあり、1変数の抽象と同様な型推論ルールを持ちます。

（単一の変数の）型宣言 ξ:α が型コンテキストΓに入っているとき、

Γ ⇒ ξ:α

は、無条件に使ってよい型判断（公理型判断）です。

さて、偏微分と微分ラムダ束縛子による抽象の型推論ルールは次のようです。

  Γ ⇒ E :(α_1, ..., α_n)->β
 --------------------------------------------------[偏微分作用素]
  Γ ⇒ D_iE : (α_1, ..., α_n)->[vec(α_i), vec(β)]


  Γ ⇒ ξ :α
  Γ ⇒ E :β
 ----------------------------------[微分ラムダ抽象]
  Γ ⇒ Dλξ.E :α->[vec(α), vec(β)]

偏微分作用素 D_i は、（多変数でもよい）関数型の式にしか作用させることはできません。ルールには書いてないですが、i ≦ n という制限もあります。微分λ抽象は、任意の式に対して使ってよいですが、束縛できる変数は1つだけです（その変数がタプル型のときはあるけど）。Dλξ.E は、D₁(λξ.E) と同値です。なので、微分ラムダ束縛子はなくてもなんとかなるのですが、入れたほうが断然便利です。

解釈不可能／困難な式の例

通常の微積分に出てくる式で、意味がハッキリしない式の例を挙げましょう。f(x, y) = x² + xy だとして、 $\frac{\partial f}{\partial y}(x, y)$ はどのように解釈可能かを見てみましょう。

fの型は f:(R, R)->R となります。変数 x, y の型は x:R, y:R です。この前提で、意味のある型判断の例を複数挙げます。（下に出てくる [R, R]は、実数から実数への線形写像の空間の型なので、実数の型Rと同一視してもかまいません。）

f:(R, R)->R, x:R, y:R ⇒ D₂f :(R, R)->[R, R]
f:(R, R)->R, x:R, y:R ⇒ (D₂f)(x, y) :[R, R]
f:(R, R)->R, x:R, y:R ⇒ Dλy.f(x, y) : R->[R, R]

それぞれの式の意味は：

2変数関数fを、第2変数に関して偏微分した導関数 λ(x, y).(x) :(R, R)->[R, R]
導関数 D₂f の値（を表す式） x :[R, R]
xを自由変数として（あるいはxを止めて）、1変数関数とみなしたfの導関数 λy.(x) :R->[R, R]

$\frac{\partial f}{\partial y}(x, y)$ は、この3つのどれを意味するか判断できません。前後の文脈やその他なんらかの“お察し”を駆使しないと、解釈不能です。こういう解釈不能／解釈困難が何段階も重なると、読む者に負担を強いるストレスフルな式になります。

何がダメなのか

$\frac{\partial f}{\partial y}(x, y)$ という書き方に馴染んでいて使いこなしている人も多いでしょう。しかし、この書き方は本質的にダメなところがあります。fが関数だとすれば、f(x, y) は関数値（この例では実数値）です。関数値に偏微分作用素を作用させることはできない*7ので、 $\frac{\partial }{\partial y}(f(x, y))$ は型エラーで無意味です。では、 $(\frac{\partial f}{\partial y})(x, y)$ なら合理的かというと、そうではありません。

$\frac{\partial f}{\partial y}$ は関数fの導関数（偏導関数）ですが、fは λ(x, y).(x² + xy) と同じです。であるなら、次の等式が成立します。

$\frac{\partial f}{\partial y} = \frac{\partial }{\partial y}(\lambda(x, y).(x^2 + xy) )$

ラムダ束縛した変数名はリネームしてもかまいません。例えば、

$\lambda(x, y).(x^2 + xy) = \lambda(y, x).(y^2 + yx) = \lambda(s, t).(s^2 + st)$

となると、偏微分作用素 $\frac{\partial }{\partial y}$ の分母のyって何よ!? となりますよね。

$\frac{\partial f}{\partial y} = \frac{\partial }{\partial y}(\lambda(x, y).(x^2 + xy) )$ ←これはいい
$\frac{\partial f}{\partial y} = \frac{\partial }{\partial y}(\lambda(y, x).(y^2 + yx) )$ ←あれっ？
$\frac{\partial f}{\partial y} = \frac{\partial }{\partial y}(\lambda(s, t).(s^2 + st) )$ ←えっ？?

記号 $\frac{\partial }{\partial y}$ は、事前に「変数名と変数の順番が固定的に決まっている」という前提で使っているのです。つまり、「yは2番目を意味する」ので $\frac{\partial }{\partial y} = D_2$ です。

$\frac{\partial }{\partial y}$ は、ラムダ変数（関数の引数変数）の名前を固定して、リネーム〈アルファ変換〉を許さない、という約束のもとでしか意味を持たないのです*8。

[補足]念の為に注意しておくと、多様体上の偏微分作用素（むしろ方向微分作用素） $\frac{\partial }{\partial x^i}$ では、名前xは固有名詞的意味を持ちます。xは使っている局所座標〈チャート〉を識別する名前なのです。 $\frac{\partial }{\partial x^i}$ の意味は「局所座標xに関するD_i」です。リネームした $\frac{\partial }{\partial y^i}$ なら「別な局所座標yに関するD_i」です。このリネームはアルファ変換ではなくて、別なものを指す名前に置き換えたのです。
（[追記 date="2019-10-20"]「局所座標xに関するDi」に関して書きました。「接ベクトル場の定義：補遺」を参照。[/追記]）

困ったことに、ユークリッド空間の微分計算と多様体の微分計算では、同じ記号でも意味と運用ルールがまったく違うのです。[/補足]

どうすればいいのか

多変数関数の型は、(α₁, ..., α_n)->β のような形をしています。関数の型がハッキリしているなら、偏微分作用素 D_i の意味もハッキリします。この偏微分作用素の意味と計算は信用できます。微分作用素に変数名を添えたいなら微分ラムダ束縛子が使えます。

$\frac{\partial }{\partial y}$ のような偏微分作用素は、直後に関数（関数値ではない！）が置かれたら、適当な番号iに関する D_i と解釈し、式が置かれたら、微分ラムダ束縛子として計算します。例：

$\frac{\partial }{\partial y}(f) = D_2(f)$
$\frac{\partial }{\partial y}(x^2 + xy) = D\lambda y.(x^2 + xy) = D_1(\lambda y.(x^2 + xy))$

さらに、外側をラムダ束縛した意味を持つ場合もあります（これが一番多いかも）。

$\frac{\partial }{\partial y}(x^2 + xy) = \lambda(x, y).( (D\lambda y.(x^2 + xy))(y)) = \lambda(x, y).(D_1(\lambda y.(x^2 + xy))(y))$

見やすくするためラムダ変数をリネーム〈アルファ変換〉してみると：

$\frac{\partial }{\partial y}(x^2 + xy) = \lambda(x, y).( (D\lambda t.(x^2 + xt))(y)) = \lambda(x, y).(D_1(\lambda t.(x^2 + xt))(y))$

関数と関数値の区別／自由変数と束縛変数の区別をちゃんとして、ラムダ抽象／適用／カリー化／反カリー化の操作に沿って式の型を追跡しましょう。そのとき、各種の型推論ルールを使います。型を意識しながら計算すれば、間違いは少なくなります*9。

微分公式（ライプニッツの法則とかチェーン法則とか）については触れてないし、計算の具体例もあまり出してませんが、それはまた（いつになるか分からんけど）。

*1:多変数関数とタプル1変数関数の違いなどは、あまり気にしてません。このテの問題は絵（ストリング図）を描かないと説明しにくいですね。

*2:区別することによるメリットより、区別することによる弊害のほうが大きいと思います。「dか∂かは別にどうでもいい」と割り切ったほうがいいでしょう。

*3:変数が束縛なのか自由なのかは、変数名で決まるのではくて、個別の出現〈occurence〉ごとに、束縛出現と自由出現があります。同名の変数が、束縛出現したり自由出現したりすることがあります。変数出現の束縛・自由は、その変数を支配している（スコーピングしている）束縛子がどれか（ないときもある）で決まります。束縛子がなければ自由出現です。

*4:型付きラムダ計算では、束縛変数の型指定はラムダ束縛内で行います。つまり、λ(x, y) ではなくて、λ(x:X, y:Y) のようなラムダ束縛子を使います。型コンテキスト内で束縛変数の型を指定できるようにしているのは、現実的習慣に合わせた変更です。

*5:正確に言うと、型の意味はアフィン線形空間の開集合です。

*6:正確に言うと、外のアフィン線形空間に付随するベクトル空間です。

*7:関数値が関数のときは偏微分できます。が、この例では関数値が実数なので、単一の実数の偏微分は定義できません。

*8:当然ながら、「変数リネームを許さない」なんてルールは破綻します。実際には、「ある範囲では変数リネームを許さない」ですが、「ある範囲」は明示されず、暗黙の範囲を察する能力を要求されます。

*9:プログラミング言語のコンパイラが、プログラマの間違いを検出するために型チェックをするのと同じことです。