キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。
2018-07-02 (月)
古典的微分幾何・ベクトル解析のモダン化: ラムダ記法の利用
雑記/備忘 | |
微分幾何・ベクトル解析の古い教科書、あるいは古いスタイルで書かれた説明は、とても分かりにくいものです。記法の説明や計算の仕方はちゃんと書いてあるのですが、その記法が何を表すのか? 計算によって何をしてるのか? 実体/実状が把握できないんです。
今でも古いスタイルの説明はよく見かけます。それに文句を言うのはやめて(過去、文句を言いましたが(笑))、古い(古典的/古式)スタイルの記述に、モダンな解釈を与えるにはどうするか、を解説します。
古典的/古式なスタイルは、微分幾何・ベクトル解析に限らず、例えば中学・高校の教育でも使われているので、それを避けるのは難しいでしょう。モダンな解釈、モダンな再定式化を知っておいて損はないと思います。
今回だけでなく、2,3回は書くと思います(たぶん)。とりあえず今回は、関数〈写像〉に関する曖昧な記述をハッキリさせるために型付きラムダ記法を導入します。
内容:
- 古典的/古式なスタイルの記述とは
- 入力型と出力型を持つ型付きラムダ記法
- 入力制約と出力変数
- 非独立入力変数と多出力変数
- 出力制約
- 部分写像とそのプロファイル
- 関数への名前付け
- 座標ラベル
- ヤコビ行列の表現
- おわりに
古典的/古式なスタイルの記述とは
現代の記号的記述/記号的計算では、次の三者は区別されます。
- 変数記号 x
- 関数記号 f、関数を表す項 E
- 関数値を表す項 f(x), E(x)
関数を表す項としては、λx∈R.(x2 - x + 2) のような型付きラムダ項〈typed lambda term〉がよく使われます。
しかし、古典的/古式なスタイルでは、変数と関数の区別は曖昧です。例えば、多変数写像を微分したヤコビ行列は次のように書きます。
変数(のタプル) y = (y1, ..., ym) は、変数(のタプル) x = (x1, ..., xn) の“関数”だ、という言い方をします。で、“関数”yを変数xで微分したわけです。
関数(あるいは写像)yが可逆(逆写像を持つ)場合は、xがyの“関数”となるので、xをyで微分すれば、
これは、先のヤコビ行列の逆行列になるので、次の等式が成立します。
ここで、添字(インデックス)jに関する総和記号は省略してあり、δはクロネッカーのデルタです。
と、これが古典的/古式な言い方/書き方の例です。わかりますか? まー、分かる人には分かるでしょうが、僕はサッパリ分かりませんでした。
記号の約束(上下の添字、総和記号の省略)はともかくとして、関数〈写像〉に関する暗黙の前提が多すぎるんですよ。その前提を自力で補うことが、僕には困難でした。
入力型と出力型を持つ型付きラムダ記法
関数〈写像〉の記述を明確にする書き方として、型付きラムダ記法〈typed lambda notation〉があります。例えば、2次関数 y = x2 は次のように書きます。
- λx∈R.x2
だいぶ明確になります。しかし、これだと関数〈写像〉の余域〈codomain | 終域〉がハッキリしません。次の書き方にします。
- λx∈R.(x2 : R)
いわゆる“型推論”には頼らず、必ず明示的に入力型と出力型を書くことにします。次の3つの関数は別なものです。
- λx∈R.(x2 : R)
- λx∈Z.(x2 : R)
- λx∈Z.(x2 : Z)
入力制約と出力変数
入力型の記述に、集合の内包記法〈intentional notation/definition〉を使っていいとしましょう。例えば:
- λx∈{t∈R| t ≧ 0}.(√x : R)
内包記法で使われた変数tは束縛変数なので、自由にリネームできます。
- λx∈{x∈R| x ≧ 0}.(√x : R)
同名の変数xが、異なる束縛スコープで使われています。束縛変数はそのスコープ内で自由にリネームできるので、次に挙げるラムダ項は全部同じ関数を表します。
- λx∈{t∈R| t ≧ 0}.(√x : R)
- λy∈{x∈R| x ≧ 0}.(√y : R)
- λx∈{y∈R| y ≧ 0}.(√x : R)
- λx∈{x∈R| x ≧ 0}.(√x : R)
- λy∈{y∈R| y ≧ 0}.(√y : R)
同じ名前を異なるスコープで使うことは許されることですが、混乱するのは確かです。古式スタイルが分かりにくい理由のひとつは、同じ名前を様々な意味でオーバーロード(多義的使用)するからです。モダン化するには、明確にスコープを切って、異なるスコープで解釈してあげます。
さて、λx∈{x∈R| x ≧ 0}.(√x : R) に問題はないのですが、混乱の危険だけではなくて、束縛変数xを二度導入しているので冗長です。次の書き方を採用しましょう。
- λx∈(R| x ≧ 0).(√x : R)
ちょっとだけコンパクトな書き方になりました。x ≧ 0 のような、入力変数に関する条件を入力制約〈input constraint〉と呼びます。プログラマには、事前条件〈precondition〉と言うとピンと来るでしょう。
古式スタイルでは、関数の定義に y = x2 のように出力変数も指定するのが普通です。この習慣を尊重して、次の書き方を許します。
- λx∈R.(y := x2 : y∈R)
さらに、出力変数に入力変数と同じ名前を使うのも許します。
- λx∈R.(x := x2 : x∈R)
これまた混乱しますが、構文的には(出現位置で)入力変数と出力変数を区別できるので大丈夫です。プログラミングでは x = x + 1 と書いたりするし、恒等関数を λx∈R(x := x : x∈R) と書くのはさほど変ではないでしょう。
出力変数もラムダ項のなかに閉じ込められているので、リネームは自由に行なえます。次はすべて同じ関数を表します。
- λx∈R.(x := x2 : x∈R)
- λx∈R.(y := x2 : y∈R)
- λx∈R.(z := x2 : z∈R)
非独立入力変数と多出力変数
円周S1は、2次元平面の部分集合として定義する場合が多いですね。
- S1 := {(x, y)∈R2| x2 + y2 = 1}
円周S1上で定義された関数を、2変数関数で表すことがあります。
- λ(x, y)∈(R2| x2 + y2 = 1).(x + y : R)
入力制約 x2 + y2 = 1 があるので、この関数はR2全体で定義されてません。関数の域〈domain | 始域〉は1次元ですが、変数はxとyを使っています。
入力変数を独立変数とも呼ぶ習慣がありますが、この例では、xとyは独立ではありません。入力制約で縛られるので非独立〈non-independent〉あるいは従属〈dependent〉な関係になります。このようなことがあるので、次の提案をしておきます。
- 入力変数を独立変数と呼ぶのはやめよう。非独立な入力変数もある。
- 出力変数を従属変数と呼ぶのはやめよう。入力変数でも従属変数がある。
非独立な入力変数があるとき、状況によっては「入力変数を減らして独立な入力変数に出来るよ」と主張しているのが陰関数定理です。
出力変数は2つ以上あってもかまいません。
- λθ∈R.(x := cos(θ), y := sin(θ) : (x, y)∈R2)
- λ(r, θ)∈(R2| r≧0, 0≦θ≦2π).(x := r cos(θ), y := r sin(θ) : (x, y)∈R2)
- λ(x, y)∈(R2| x > 0).(r := √(x2 + y2), θ := arctan(y/x) : (r, θ)∈R2)
入力変数と出力変数に同じ名前が登場してもいいので:
- λ(x, y)∈R2.(x := y, y := x : (x, y)∈R2)
これは、第一座標と第二座標を入れ替える写像です。分かりにくいのなら、出力変数もリネームしていいので:
- λ(x, y)∈R2.(s := y, t := x : (s, t)∈R2)
出力制約
入力変数(のタプル)に入力制約で条件付けできます。同様に出力側にも制約を課していいとしましょう。
- λx∈R.(y := x2 : y∈(R| y > -1))
- λ(x, y)∈(R2| x2 + y2 = 1).(z := x + y : z∈(R| -√2 ≦ z ≦ √2))
- λ(x, y)∈(R2| x > 0).(r := √(x2 + y2), θ := arctan(y/x) : (r, θ)∈(R2| -π < θ < π))
出力制約〈output constraint〉は勝手に付けられるわけではありません。ラムダ項が関数を表すことを担保するためには、値が出力制約の範囲内にあることを示す必要があります。上の3つのそれぞれに対して、次の命題を示す義務が生じます。
- ∀x∈R.(y = x2 ⇒ y > -1)
- ∀(x, y)∈R2.(x2 + y2 = 1 ∧ z = x + y ⇒ -√2 ≦ z ≦ √2)
- ∀(x, y)∈R2.(x > 0 ∧ r = √(x2 + y2) ∧ θ = arctan(y/x) ⇒ -π < θ < π)
「ラムダ記法とイプシロン記法を組み合わせて関数を定義する」で述べことですが、関数定義に伴って要求される正当性の証明を(Mizarでは)justificationと呼びます。今の例では、上記の命題の証明がjustificationとなります。
関数を定義する際や、関数に何らかの操作を加える際には、justificationが要求されることがあるのですが、古式スタイルはそこらへんを曖昧に済ませてしまいます。そもそも、入力制約や出力制約がちゃんとは言及されないこと(空気読めよ方式)があります。曖昧な部分は自力で明確化するしかないです。
部分写像とそのプロファイル
現代風の関数〈写像〉の定義では:
- 域〈始域〉Xと余域〈終域〉Yがハッキリと決まっている。
- 域Xのすべての要素xに、余域Yの要素f(x)が一意的に(1つだけ)定まる。
古式スタイルでは、これらは守られません。古式スタイルの関数〈写像〉とは、部分写像〈partial mapping〉と思ったほうがいいでしょう。
部分写像は、次の素材から構成されます。
- 集合X
- Xの部分集合A
- 集合Y
- AからYへの通常の写像 f:A→Y
これらをまとめて次のように書きます。
- f:X⊇A→Y
X⊇A→Y の部分を、部分写像fのプロファイルと呼びます。集合Aはfの定義域〈domain of definition〉です。通常、域と定義域は同義語と解釈しますが、部分写像では違います。次の記法を使いましょう。
- dom(f) = X
- ddef(f) = A
- cod(f) = Y
2つの部分写像fとgが結合可能〈composable | 合成可能〉である条件は、通常の写像と同じで cod(f) = dom(g) です。f:X⊇A→Y と g:Y⊇B→Z の結合 h = f;g = gf は次のように定義されます。
- f(a)∈B のとき、 h(a) = g(f(a))
- そうでないとき、h(a)は未定義
h = f;g = gh の定義域(域ではない)は、fの定義域とは変わるかもしれません。fによる集合Bの逆像がhの定義域です。hの定義域が空になってしまこともあります。
上記のように部分写像とその結合を定義すると、だいたい普通の写像と同じように扱えることは分かっています。なので、古式スタイルの“関数”を部分写像として扱いたいと思うのですが … ですが、けっこう深刻な問題があります。
型付きラムダ記法で書かれた関数定義から、部分写像としてのプロファイルを取り出すことがうまくできないのです。例えば:
- λ(x, y)∈(R2| x2 + y2 = 1).(x + y : R)
この関数のプロファイルは何でしょうか? S1を円周として、R2⊇S1→R が自然のように思えますが、S1⊇S1→R (つまり全域写像)のつもりだったかも知れません。次はどうでしょう?
- λ(x, y)∈(R2| x2 + y2 = 1, y > 0).(x : R)
U = {(x, y)∈R2| x2 + y2 = 1, y > 0} として、この関数のプロファイル候補は:
- R2⊇U→R
- S1⊇U→R
- U⊇U→R
どれなのか? これといって決め手はありません。部分写像としてのプロファイルを決定できないので、古式スタイルの関数を部分写像と解釈することは難しく、部分写像としての整合的な定式化も頓挫します。
以前僕は、部分写像プロファイルを少し一般化した f:X⊇A→B⊆Y というプロファイルを考えて、fの使用状況からXとYを、ソフトウェアにより“型推論”することを試みたことがあります。難しくてうまくいきませんでした。
ソフトウェアによる実装が難しいということは、人間にとっても難しい、ってことです。古式スタイルの曖昧な域・定義域・余域を、アルゴリズム的に決定するのは無理だと思います。しかし、曖昧な域・定義域・余域がヘビーに使われる場面、具体的には局所座標の変換では、ハッキリとした定式化ができます。局所座標の変換については、次の機会に(たぶん)述べます。
関数への名前付け
冒頭でも述べたように、古式スタイルでは、関数と変数の区別がされないことがあります。これは、名前のスコープをハッキリさせることで、破綻しない定式化ができます。
関数の名前付けを次の形で行いましょう。
- mapping sqrt := λx∈(R| x ≧ 0).(√x : R)
次の名前付けは問題ありません。
- mapping y := λx∈R.(y := x2 : y∈R)
ラムダ項内の出力変数と関数名がたまたま同じですが、出力変数もラムダ項内に閉じ込められた束縛変数です。束縛変数はリネームしても何も変わりません。
- mapping y := λx∈R.(t := x2 : t∈R)
あるいは、出力変数なしでもいいでしょう。
- mapping y := λx∈R.(x2 : R)
この定義のもとで、次のような等式は成立します。
- y(a) = a2
- y(2) = 4
- y(a + b) = a2 + 2ab + b2
「出力変数名と関数名が同じ名前」というのは、たまたま選んだ束縛変数名が関数名と同じだけで、スコープが違うし、束縛変数のリネームもできるので問題にはなりません。
- mapping (x1, x2) := λθ∈R.(x1 := cos(θ), x2 := sin(θ) : (x1, x2)∈R2)
でも、外部に公開される関数名はx1とx2で、内部的な出力変数名とかぶっているのは単なる偶然だと言い張れます。
というわけで、関数名と出力変数名のかぶりは合理化できましたが、違う関数に同じ名前が付けられるのはどうでしょうか。
mapping y := λx∈R.(y := x2 : y∈R) mapping y := λx∈R.(y := 2x + 1 : y∈R)
こんなときは、後の関数定義(名前付け)が前の定義を上書きした、あるいは新しい環境(名前空間)に入って同名の別な関数を定義したと解釈しましょう。
座標ラベル
古式スタイルが分かりにくい大きな理由は、「同じ名前を様々な意味でオーバーロード(多義的使用)するからだ」と述べました。このような状況に対して、同じ名前でも、所属する名前空間〈namespace | namae partition〉が違うから別なものを表してもいい、という解釈で合理化できます。
前節では、出力変数名と関数名は違う名前空間(スコープ)に属するから同名でもかまわないとしました。ここで、また別な名前空間として、座標ラベル〈coordinate label〉の名前空間を導入しましょう。
Rnの部分集合(多くの場合は開集合)Aに対して、座標ラベルと呼ばれる記号の集合Sを用意します。Sはn個の要素を持つ有限集合です。例えば、S = {'x', 'y'}。シングルクォートで囲んだのは、変数名ではなくて単なるラベルだと強調するためです(この後はもう囲みません)。座標ラベルは、座標軸の名前と考えればいいでしょう。
座標ラベル集合は、集合Aごとに準備されるので、Aの座標ラベル集合とBの座標ラベル集合に同じ記号が入っていてもかまいません。座標ラベルは単なるラベルなので、変数名や関数名とは別な名前空間を構成します。
座標ラベルSが指定された集合Aは、A⊆Rn というより、A⊆RS と考えます。RS Rn ですが、RS では座標軸の呼び名が 1, 2, ..., n ではなくて、Sの要素(ラベル)で呼びます。
射影 RS→R は、Sの要素でラベルされます。例えば、R{x, y}ならば、
- πx:R{x, y}→R
- πy:R{x, y}→R
Rn = R{1, ..., n} とみなせば、πi:R{1, ..., n}→R という記法と整合します。
A⊆RS とみなすので、A上に制限された射影も、Sでラベルしたπs(s∈S)で表します。
S = {x, y} の例で、射影に関数名を与えることができます。例えば、
mapping x := πx mapping y := πy
あるいは、
mapping p := πx mapping q := πy
射影にどんな名前を付けるのも自由だし、名前を付けずにπsとして使ってもかまいません。
射影以外に、偏微分作用素も座標ラベルでラベルすることにします。Aは開集合として、C∞(A)を、A上で定義されたなめらかな(無限回微分可能な)実数値関数の全体だとします。A⊆Rn ならば、標準的な偏微分作用素は、1, ..., n という番号でラベルされます。
- D1:C∞(A)→C∞(A)
- D2:C∞(A)→C∞(A)
- …
- Dn:C∞(A)→C∞(A)
A⊆RSなら、偏微分作用素もSの要素sでラベルしてDsのように書きます。S = {x, y} の例なら:
- Dx:C∞(A)→C∞(A)
- Dy:C∞(A)→C∞(A)
繰り返しますが、座標ラベルは変数名でも関数名でもないので、同名の変数・関数があっても問題になりません。
ヤコビ行列の表現
次の例を考えましょう。
- λ(x, y)∈(R2| x > 0).(r := √(x2 + y2), θ := arctan(y/x) : (r, θ)∈R2)
- λ(r, θ)∈(R2| r > 0, -π < θ < π).(x := r cos(θ), y := r sin(θ) : (x, y)∈R2)
写像の成分関数に次のように名前を付けます。
mapping (r, θ) := λ(x, y)∈(R2| x > 0).(r = √(x2 + y2), θ = arctan(y/x) : (r, θ)∈R2) mapping (x, y) := λ(r, θ)∈(R2| r > 0, -π < θ < π).(x := r cos(θ), y := r sin(θ) : (x, y)∈R2)
既に述べた理由で、関数名 r, θ, x, y は問題ありません。
座標ラベル集合{x, y}に対して、開集合Aを次のように定義します。
- A := {{x:s, y:t}∈R{x, y}| s > 0}
{x:s, y:t}は、x座標成分の値がs、y座標成分がtという意味です。同様に、座標ラベル集合{r, θ}に対して、開集合Bを次のように定義します。
- B := {{r:s, θ:t}∈R{r, θ}| s > 0, -π < t < π}
R2 R{x, y}, R2
R{r, θ} により、関数 r, θ, x, y は次のようにみなせます。
- r:A→R
- θ:A→R
- x:B→R
- y:B→R
A, B上の偏微分作用素は、{x, y}, {r, θ} でラベルされるので、
- Dx:C∞(A)→C∞(A)
- Dy:C∞(A)→C∞(A)
- Dr:C∞(B)→C∞(B)
- Dθ:C∞(B)→C∞(B)
偏微分作用素を関数に作用させれば、次は意味を持ちます。
- Dxr ∈C∞(A)
- Dyr ∈C∞(A)
- Dxθ ∈C∞(A)
- Dyθ ∈C∞(A)
- Drx ∈C∞(B)
- Dθx ∈C∞(B)
- Dry ∈C∞(B)
- Dθy ∈C∞(B)
関数可換環C∞(A)またはC∞(B)を係数環とする次の行列も意味を持ちます。
のような書き換えをすれば:
これらは、関数係数〈関数成分〉の行列ですが、次の、簡単だがとても重要な同型により、実数係数行列を値とする関数〈写像〉ともみなせます。以下で、C∞(X, Y)は、XからYへのなめらかな写像の全体、Mat(n, m;R)は、R係数のm行n列の行列の集合です。
- C∞(A, Mat(n, m;R))
Mat(n, m;C∞(A))
- C∞(B, Mat(n, m;R))
Mat(n, m;C∞(B))
(r, θ):A→R2 と (x, y):B→R2 は、そのままでは(厳密に言えば)結合できませんし、逆写像にもなっていません。しかし、次のような部分写像とみなせば結合ができます。
- (r, θ):R{x, y}⊇A→R{r, θ}
- (x, y):R{r, θ}⊇B→R{x, y}
部分写像の意味で結合〈合成〉すれば:
- (x, y)
(r, θ) = idA
- (r, θ)
(x, y) = idB
が成立するので、互いに逆と言ってもいいでしょう。
添字付けや総和記号の省略の規則は述べてませんが、冒頭で述べたヤコビ行列の記法が、意味付け可能だろうと推察できるでしょう。
[追記]Maximaにヤコビ行列を計算させてみると、こんな(↓)感じでした。やはり、同じ名前を使うのはうまくなくて、関数のx, y、変数のr, θは大文字にしています。
[/追記]
おわりに
前節の議論では、集合や写像の名前付けやプロファイルの特定などが、細かすぎてうるさいなー、と感じたかもしれません。それはそのとおりで、煩雑になります。「話が簡単になるから、このくらいの曖昧さや非厳密さはいいだろう」という気持ちはわかりますが、それが何段階も積み重なると、全体がモヤンモヤンのワケわからないシロモノになります。
記号をイイカゲンに使った計算は実際に楽で便利なんで、使うのはおおいにけっこうですが、一方で、モヤンモヤンは晴らしておきたいなー、とも思います。
- 421 https://www.google.co.jp/
- 123 https://www.google.com/
- 116 https://t.co/xP6kPwg9Fw
- 92 https://t.co/ycLGhySm8g
- 25 http://search.yahoo.co.jp/
- 18 https://www.bing.com/
- 17 http://www.google.co.jp/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&ved=0ahUKEwj32NruuYDcAhVCTbwKHcyKDoEQFggoMAA&url=http://d.hatena.ne.jp/m-hiyama/20151215/1450140312&usg=AOvVaw1TQDTqBzQcwhh8ZxsS0BFs
- 16 https://t.co/ycLGhySm8g?amp=1
- 14 https://socialmediascanner.eset.com
- 12 https://t.co/xP6kPwg9Fw?amp=1