檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2018-06-18 (月)

二点しかない離散空間に長さ1の線分を描けるか?

| 15:41 | 二点しかない離散空間に長さ1の線分を描けるか?を含むブックマーク

a, bを実数の定数として、f(x) = ax + b は中学校で習った1次関数です。xの変域を単位閉区間 [0, 1] = {x∈R | 0 ≦ x ≦1} に制限します。ax + b = b(1 - x) + (a + b)x であることに注意して、s := b (sはstart点のs), t := a + b (tはtarget点のt)と置けば、f(x) を次のように書き換えられます。

  • f(x) = s(1 - x) + tx

xを時刻とみなせば、時刻0でスタート点s(出発地)にいて、時刻1でターゲット点t(目的地)に到着する等速直線運動(速度はa)の記述と解釈できます。0と1の中間の時刻(例えば x = 1/2)でも、必ず対応する位置 f(x) が存在します。

さて、いま二点だけの集合 {2, 3} を考えます。ホントに二点だけですよ! 中間の位置はありません。関数 f:[0, 1]→{2, 3} で、f(x) = 2(1 - x) + 3x と書けるものはあるでしょうか?

普通に考えると、x = 1/2 で f(1/2) = 2(1 - 1/2) + 3(1/2) = 5/2、しかし5/2は{2, 3}の要素ではないのでウマクないですよね。なにかしら普通ではない、しかし合理的で説得的な考え方により、f(x) = 2(1 - x) + 3x : [0, 1]→{2, 3} に意味を与えたいのです。さあ、どうしましょうか?

内容:

  1. カーク・スターツの論文
  2. ベクトル空間内の凸集合
  3. 凸結合の性質
  4. 凸空間の公理的定義
  5. 二元集合を台集合とする凸空間はあるのか?
  6. 二元集合上の凸構造の構成
  7. おわりに

カーク・スターツの論文

カーク・スターツ(Kirk Sturtz)は、2017年7月にarXiv.orgに投稿され、2018年4月に更新(ver.4)された論文により、ジリィモナド界隈の人々が成立するだろうと期待していた(しかし、証明はなかった)定理を証明しました。

新しい証明・理論には、新しいアイディアが必要です。スターツは、いくつもの新しいアイディアを駆使して証明・理論を組み立てていますが、そのなかに、小さな/ささいなアイディアかも知れませんが、僕には大きな驚きだったものがあります。

それが表題にある「二点しかない離散空間に長さ1の線分を描く方法」です。正確な言葉づかいをするなら、要素が2つだけの集合に凸構造〈convex structure〉を定義することです。

実は僕も、「二元集合(要素が2つだけの集合)に凸構造が入ったらいいなー」と思ったことがあります。しかし、「出来るわけないよな、こりゃ無理ムリ」と決めてかかっていました。なので、スターツが二元集合上の凸構造を作っているのを知って、もうビックリ! だったのです。

スターツのアイディア*1と共に、僕がどんな先入観に囚われていたかも説明します。

ベクトル空間内の凸集合

Vを実数体R上のベクトル空間とします*2。Vの部分集合Aが凸集合〈convex set〉だとは、次が成立することです。

  • x, y∈A ならば、0 ≦ τ ≦ 1 である実数τに対して、((1 - τ)x + τy)∈A

ここから先、閉区間 [0, 1] に所属する実数はギリシャ文字小文字で表すことにします。文字τ(タウ、ラテン文字tに相当)を選んだのは、時間パラメータの雰囲気(τ = time)を残したかったからです。

ベクトル空間Vの要素x, yを固定して、τを0から1へと動かした場合、(1 - τ)x + τy は、xからyへと至る線分〈segment〉(直線の一部)を描きます。この線分を [x, y] と書きます。

  • [x, y] := {v∈V | 0 ≦ τ ≦ 1 である実数τにより v = (1 - τ)x + τy と書ける}

V = R の場合を考えると、閉区間の記法 [0, 1] は、今定義した記法と整合します。

  • [0, 1] := {s∈R | 0 ≦ τ ≦ 1 である実数τにより s = (1 - τ)0 + τ1 と書ける}

線分を使って凸集合の定義を言い換えると:

  • A⊆V が凸集合 :⇔ (x, y∈A ⇒ [x, y]⊆A)

':⇔'は、定義であることを強調した論理的同値、'⇒'は「ならば」(論理的含意)です。

平面(2次元ベクトル空間)内の円板(円周ではない)や、内部を含む三角形などは凸集合です。平面全体や一点だけの集合も凸集合です。凸集合の例を作るときに役立つ定理があります。

  1. f:V→R が線形写像のとき、a∈R に対して、{v∈V | f(v) ≧ a} は凸集合である。
  2. Iはインデックス集合(無限集合でもよい)として、各 i∈I に対してAiが凸集合のとき、共通部分 ∩{Ai | i∈I} は凸集合である。

{v∈V | f(v) ≧ a} の形の集合は、アフィン半空間〈affine half-space〉*3と呼ばれるので、すぐ上の一番目の定理は、「アフィン半空間は凸集合である」と言い換えられます。

{v∈V | f(v) ≧ a}∩{v∈V | -f(v) ≧ a} = {v∈V | f(v) = a} なので、Vの超平面(アフィン超平面)は凸集合なのが分かります。{fi(v) ≧ ai | i = 1, 2, ..., k} という連立不等式で定義される多角形・多面体も凸集合です。円板のように、多角形とは呼べない図形でも、無限個の半空間の共通部分として書けます。

ハート形は凸集合ではありません。次の図のように、両端がハート形に入っているのに、ハート形からはみ出す線分が存在するからです。

[補足]

空集合は凸集合です。これは、そう約束したと思ってもいいですが、例外事項を付加したわけではなくて、定義だけから厳密に言えることです。最近、論理と証明の話を書いたばかりなので、論理的に確認してみましょう。

Pow(V)はベクトル空間(の台集合)Vのベキ集合だとして、Aが凸集合であることを、ちゃんと書いてみると:

  • for A∈Pow(V) (Aが凸集合 ⇔ ∀x, y∈V.(x, y∈A ⇒ [x, y]⊆A))

A = ∅ (空集合)と具体化してみると:

  • ∅が凸集合 ⇔ ∀x, y∈V.(x, y∈∅ ⇒ [x, y]⊆∅)

∅が凸集合であるかないかの判定は、x, y∈∅ ⇒ [x, y]⊆∅ という命題の真偽判定と同じことです。含意命題('⇒'を含む命題)の前件('⇒'の左側) x, y∈∅ は常に偽なので、含意命題全体は真です。つまり、∀x, y∈V.(x, y∈∅ ⇒ [x, y]⊆∅) が真であることから、「∅が凸集合」も真になります。

別な(逆な)発想として、「∅が凸集合でない」と言いたいなら、

  • ∃x, y∈V.(x, y∈∅ ∧ ¬([x, y]⊆∅))

を示す必要があります。x, y∈∅ が常に偽なので、この命題は絶対に成立しません(「∅が凸集合」に対する反例となる2点を見つけられない)。二重否定の原理から、「∅が凸集合でない」が成立し得ない、とは「∅は凸集合である」ことです。

[/補足]

凸結合の性質

前節の凸集合の定義で出てきた (1 - τ)x + τy を、xとyの凸結合〈convex combination〉と呼びます。凸結合を、τ, x, y の3引数を持つ関数〈写像〉ccと考えましょう。つまり、

  • cc:[0, 1]×V×V→V
  • cc(τ, x, y) := (1 - τ)x + τy

型付きのラムダ記法を使うなら:

  • cc := λ(τ, x, y)∈[0, 1]×V×V.( (1 - τ)x + τy :V )

A⊆V が凸集合であることは、ccをA上に制限した cc:[0, 1]×A×A→A がちゃんと定義できる(well-defined)ことと同じです。

cc(τ, x, y) を ccτ(x, y) とも書きます。ccは次の性質を持ちます。

  1. cc0(x, y) = x ---(始点条件)
  2. ccτ(x, x) = x ---(退化線分条件)
  3. cc1-τ(x, y) = ccτ(y, x) ---(反転対称性)
  4. ccτ(x, ccρ(y, z)) = ccτρ(ccσ(x, y), z) ただし τ(1 - ρ) = (1 - τρ)σ ---(パラメータ付き結合律)

これらの等式は、ccの定義に従って計算すれば出てきます(ぜひ、やってみてください)。それぞれの等式の意味を説明しましょう。

ccを等速直線運動のパラメータ表示と考えると、τ = 0 では始点xにいるはずです。それを表した等式が「始点条件」です。

始点と終点が一致している等速直線運動は、一点に退化した線分を描きます。一点に退化した線分とは定数写像になります。「退化線分条件」はそのことを表していますね。

パラメータτを τ' = 1 - τ に変更すると、時間を反転したことになり、終点から始点へと逆行する運動になります。時間反転が、空間的には線分の対称性を導きます。「反転対称性」です。

最後の「パラメータ付き結合律」は少し複雑です。一般に、二項演算(=ニ変数関数)fが f(x, f(y, z)) = f(f(x, y), z) を満たすなら、fは結合律を満たします。ccの場合、パラメータをうまく調整すると結合律を満たします。パラメータに関する条件も含めて結合律を述べたのが「パラメータ付き結合律」です。

μ = τσ と置くと、

  • ccτ(x, ccρ(y, z)) = ccμ(ccσ(x, y), z)

この結合律は、4つのパラメータ τ, ρ, μ, σ が次の連立方程式を満たすときだけ成立します。

  1. μ = τσ
  2. τ(1 - ρ) = (1 - μ)σ

連立方程式により定義される図形 {(τ, ρ, μ, σ)∈[0, 1]4 | μ = τσ かつ τ(1 - ρ) = (1 - μ)σ} が、ccの結合律を支配していると言ってもいいでしょう。

凸空間の公理的定義

凸集合の定義では、ベクトル空間Vがまずあり、その部分集合として凸集合が定義されました。凸結合も、ベクトル空間の足し算とスカラー倍から組み立てられた演算です。前節の凸結合の性質も、定理として示すべきものです。

ここで発想を変えて、ベクトル空間を想定せずに、とある集合Aとその上の演算のパラメータ族〈family of binary operations〉ccの組として「凸な構造」を定義しましょう。(A, cc) が満たすべき公理(定理ではない)は、前節の凸結合の性質です。凸結合の公理を満たす (A, cc) を凸空間〈convex space〉と呼びます。

ccτ(x, y) を、中置二項演算子 +τ として書くことにします。読みやすさはけっこう改善します。中置二項演算子を使って、凸結合の公理をもう一度書いてみます。

  1. x +0 y = x ---(始点条件)
  2. x +τ x = x ---(退化線分条件)
  3. x +1-τ y = y +τ x ---(反転対称性)
  4. x +τ (y +ρ z) = (x +σ y) +μ z ただし、μ = τρ, τ(1 - ρ) = (1 - μ)σ ---(パラメータ付き結合律)

こう書いてみると、凸結合は“パラメータ付きの和”に見えるので、凸結合を凸和〈convex sum〉と呼ぶこともあります。凸結合を二項演算だと見ると、それぞれの公理も若干違った見え方になるかも知れません。

  1. x +0 y = x は、τ = 0 のときの凸和が左自明演算になることです。左自明演算とは、x・y = x という演算です。同様に、τ = 1 のときの凸和は右自明演算です。
  2. x +τ x = x は、+τ がベキ等〈idempotent〉な演算であることを意味します。
  3. x +1-τ y = y +τ x は一種の交換律です。
  4. x +τ (y +ρ z) = (x +σ y) +μ z はもちろん、パラメータ条件に縛られた結合律です。

ここから先は、プラス記号'+'を凸和の意味でもオーバーロード(多義的使用)して、A = (A, +) のような記号の乱用もします。

(A, +) と (B, +) が2つの凸空間だとして、写像 f:A→B がアフィン凸写像〈affine convex map〉だとは、凸和を保存することです。つまり、次を満たすことですね。

  • f(x +τ y) = f(x) +τ f(y)

アフィン凸写像は、凸アフィン写像アフィン写像凸写像などとも呼ばれます。

凸空間を対象として、アフィン凸写像を射とする圏が構成できます。しかし、今回は圏論的考察はしません。

二元集合を台集合とする凸空間はあるのか?

いよいよ本題に入ります。二元集合(2つだけの要素を持つ集合)を凸空間にすることが出来るか? が問題です。

二元集合として、真偽値の集合 B = {F, T} をとります。BはBooleanから、F, T は False, True の略です。Bに対して凸和 +:[0, 1]×B×BB をうまいこと定義して、(B, +) を凸空間にしたいのです。

僕は即座に「無理」と判断しました。皆さんはどうでしょう? なぜ僕は「無理」と判断してしまったのでしょう? 後から考えてみました。

先入観・思い込みがあったのです。その先入観・思い込みは、凸空間にいだいた幾何的・物理的イメージによります。今まで使用していた用語「線分」には明らかに図形のイメージが伴います。その線分は等速直線運動の軌跡とみなしているので、物理的イメージもあります。凸空間の定義に使われる閉区間 [0, 1] は図形だろうし、凸空間の典型例である多角形・多面体、円板・球体なども図形です。

つまり、凸空間には、図形の(幾何的)イメージが非常に強く付着しています。このため、無意識に幾何的判断をしてしまうのです。

Bの二点、例えばFとTに対して F +τ T = ccτ(F, T) は、閉区間[0, 1]からBへの写像となります。Bは離散空間で2つの連結成分({F}と{T})を持ちます。ですから、連結で連続した[0, 1]からの写像は存在するはずがありません。B内の線分や等速直線運動なんて無理なんです。

これが僕の判断でした。しかし、公理的・抽象的に定義された凸空間の定義に、位相や連続性は一切入っていません。凸空間は代数的構造であって、代数的法則の成立が要請されているだけです*4

「無理だ」という判断は、凸空間の定義に照らし合わせて、まったく何の根拠もなかったのです。実際スターツは、凸空間 (B, +) を 構成しています。

二元集合上の凸構造の構成

B = {F, T} 上の凸和を次のように定義します。

  1. F +τ F := F
  2. F +τ T := if (τ = 1) then T else F
  3. T +τ F := F +1-τ T = if (τ = 0) then T else F
  4. T +τ T := T

このように定義された凸和が、凸空間の4つの公理(始点条件、退化線分条件、反転対称性、パラメータ付き結合律)を満たせば、(B, +) は凸空間になります。順番に確認していきましょう。

始点条件

始点条件を、∀(「任意の」を意味する記号)を使って書けば、∀x, y∈B.(x +0 y = x) となります。∀x, y∈B の部分は、4つの組み合わせに展開できるので:

  1. F +0 F = F
  2. F +0 T = F
  3. T +0 F = T
  4. T +0 T = T

これらは定義から明らかです。

退化線分条件

同じく∀を使って書けば、∀x∈B.∀τ∈[0, 1].(x +τ x = x)、展開すれば:

  1. ∀τ∈[0, 1].(F +τ F = F)
  2. ∀τ∈[0, 1].(T +τ T = T)

これらも定義から言えます。

反転対称性

∀x, y∈B.∀τ∈[0, 1].(x +1-τ y = y +τ x) が示すべきことです。∀x, y∈B を展開すれば4つの命題になります。

  1. ∀τ∈[0, 1].(F +1-τ F = F +τ F)
  2. ∀τ∈[0, 1].(F +1-τ T = T +τ F)
  3. ∀τ∈[0, 1].(T +1-τ F = F +τ T)
  4. ∀τ∈[0, 1].(T +1-τ T = T +τ T)

これも定義からすぐに言えますね。

パラメータ付き結合律

パラメータ付き結合律は、ちょっと複雑な論理式になって:

  • ∀x, y, z∈B.∀τ, ρ, μ, σ∈[0, 1].(μ = τρ かつ τ(1 - ρ) = (1 - μ)σ ⇒ x +τ (y +ρ z) = (x +σ y) +μ z)

∀x, y, z∈B を8つの場合に展開するのではなくて、パラメータτ, ρに関して場合分けすることにします。

(τ, ρ) = (1, 1) の場合とそれ以外です。それ以外をさらに2つに分けて:

  1. 場合1 : τ = 1 かつ ρ = 1
  2. 場合2 : τ ≠ 1 (ρは任意)
  3. 場合3 : ρ ≠ 1 (τは任意)

漏れない場合分けなので、「場合1または場合2または場合3」で、すべての(τ, ρ)をカバーしています。

場合2と場合3では、結合律の左辺のパラメータ(τ, ρ)で与えられたとき、右辺のパラメータ(μ, σ)を次のように計算できることに注意してください。

  • μ = τρ
  • σ = τ(1 - ρ)/(1 - μ) = τ(1 - ρ)/(1 - τρ)

場合1では、分母がゼロになるので二番目の式が使えません。

場合1 : τ = 1 かつ ρ = 1

この条件で、「μ = τρ かつ τ(1 - ρ) = (1 - μ)σ」を満たす μ, σ は、

  • μ = 1
  • σは任意

となります。目的の命題=結合律は、

  • x +1 (y +1 z) = (x +σ y) +1 z

です。σが何であっても、これは成立します。

場合2 : τ ≠ 1 (ρは任意)

この条件のもとでは、

  • μ ≠ 1 (τ ≠ 1, μ = τρ なので)

σ = τ(1 - ρ)/(1 - τρ) を、σ = 1 として解くと τ = 1 。つまり、σ = 1 ⇒ τ = 1 。対偶をとれば τ ≠ 1 ⇒ σ ≠ 1 ですが、τ ≠ 1 は今の仮定に入っているので、

  • σ ≠ 1

τ ≠ 1 から x +τ (y +ρ z) = x 。μ ≠ 1 から (x +σ y) +μ z = (x +σ y)、σ ≠ 1 から (x +σ y) = x 。

以上より、x +τ (y +ρ z) = x 、(x +σ y) +μ z = x だから、

  • x +τ (y +ρ z) = (x +σ y) +μ z

場合3 : ρ ≠ 1 (τは任意)

この条件のもとでも場合2と同じく次は成立します。

  • μ ≠ 1
  • σ = 1 ⇒ τ = 1

さらに、

  • τ = 1 ⇒ σ = 1

も、σ = τ(1 - ρ)/(1 - τρ) の計算から明らか。よって、

  • τ = 1 ⇔ σ = 1
  • τ ≠ 1 ⇔ σ ≠ 1

ρ ≠ 1, τ = 1 のときは、σ = 1 でもあって、

  • x +τ (y +ρ z) = y +ρ z = y
  • (x +σ y) +μ z = y +μ z = y (μ ≠ 1 だったから)

結合律は成立します。

ρ ≠ 1, τ ≠ 1 のときは、σ ≠ 1 でもあって、

  • x +τ (y +ρ z) = x
  • (x +σ y) +μ z = (x +σ y) = x

結合律は成立します。

おわりに

公理的・抽象的に定義された凸空間は、我々の幾何的・物理的イメージを裏切るような存在物(その例が (B, +))も包摂しているようです。お馴染みの例である有限次元ベクトル空間の凸部分集合は、必然的に幾何的(位相的)構造も持ってしまうのですが、凸部分集合の幾何的イメージに頼るのは危険です。

定義や前提に含まれない仮定を勝手に付けてしまう過ちは、けっこうやってしまいます。今回の例でも僕はやらかしました。余計なことを考えない境地に至るのは、だいぶ修行が必要そうです。

*1:既によく知られていたことを、スターツが採用しただけかも知れませんが、スターツ論文が自分にとっての初見だったので、「スターツの」とします。

*2:凸集合を定義する場所としては、ベクトル空間よりもアフィン空間のほうがふさわしいのですが、話を簡単にするためにベクトル空間を使います。

*3:アフィン半空間の定義も、アフィン空間をベースに行うべきですが、ベクトル空間でいいことにします。

*4:幾何的イメージを避けてかどうかは分かりませんが、凸空間の代わりに凸代数〈convex algebra〉、重心代数〈barycentric algebra〉という呼び名もあるようです。重心代数は微妙に違った定義かも知れません。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20180618

2018-06-15 (金)

論理の全称記号∀も存在記号∃もちゃんと使えるようになろう

| 12:24 | 論理の全称記号∀も存在記号∃もちゃんと使えるようになろうを含むブックマーク

論理の存在記号∃をちゃんと使えるようになろう」:

自然数の大小順序だけでも、まだネタはありますし、もう少し練習問題があったほうがいい気もします。全称記号∀に関する説明が不足してるし、∀と∃の関係も述べていません。が、長くなるので今回はこのくらいにしておきます。

ということで、そのまま続きを書きます。前回の記事を読んでいることを前提にするので、予備知識や記法の約束の繰り返しはしません。

内容:

  1. 全称記号と存在記号に関する推論規則
  2. 全称命題を準備するボックスを使ってみよう: 最小元の存在
  3. 背理法も使ってみる: 最大元の非存在
  4. おわりに

全称記号と存在記号に関する推論規則

全称記号∀を含む命題と存在記号∃を含む命題に対する推論規則は、それぞれに導入規則〈introduction rule〉と除去規則〈elimination rule〉があり、合計で4つの規則となります。論理の教科書によくあるスタイル(望ましいスタイルとは思ってない)で規則を書くと:

      P                    ∀x.P
 ------------[∀導入]    ----------[∀除去]
 ∀x.P[a:=x]              P[x:=t]

      P                    ∃x.P
 ------------[∃導入]    ----------[∃除去]
 ∃x.P[t:←x]             P[x:=a]

規則の記述のなかで使っている記号を説明します。

  • Pは命題です。正確に言えば、述語論理の論理式を表すメタ変数がPです。
  • xとaは変数(を表すメタ変数)ですが、xは束縛変数で、aは自由変数とします。実際に使う変数を'x', 'a'って決めてるわけじゃないですよ。メタ変数xが表す実際の変数がaのときもあります。
  • tは項(を表すメタ変数)です。定数、変数、関数(の記号)の組み合わせが項です。

ブラケット〈角括弧〉は置換を表します。4つのルールで、置換の仕方は微妙に違います。

  1. ∀導入 ∀x.P[a:=x] : 自由変数の束縛変数化 : Pに含まれていた自由変数aを束縛変数xに置き換える。
  2. ∀除去 P[x:=t] : 束縛変数の具体化 : Pに含まれていた束縛変数xを項tで置き換える。
  3. ∃導入 ∃x.P[t:←x] : 具体項の束縛変数化 : Pに含まれていた項tを束縛変数xで置き換える。これだけ特殊で(なので違う記号を使っている)、具体物を表す項に対して置き換えを行う。tが複数箇所に出現しても、出現箇所を特定して置き換える。つまり、置換しないままのtが残ってもかまわない。
  4. ∃除去 P[x:=a] : 束縛変数の条件付き自由変数化 : Pに含まれていた束縛変数xを自由変数aで置き換える。ただし、自由変数aには条件が付く(その意味で「自由」という呼び方は違和感があるかも)。

この節冒頭のスタイルで推論規則を書くのは望ましくない、と言ったのは、前回に述べたボックスの構造が全く含まれていないからです。∃除去で使うボックスが前回の主たる話題でした。∀導入にもボックスが付きます。ボックスなしでは実用的なテンプレートとしては不十分なので、推論バー(横棒)しか書かないスタイルは実用性に乏しいと思うのです。

全称命題を準備するボックスを使ってみよう: 最小元の存在

∀x∈N.(a ≦ x) という論理式は、「aがNの最小元である」という意味です。「Nに最小元が存在する」なら、次の論理式になります。

  • ∃a∈N.∀x∈N.(a ≦ x)

大小関係≦の定義は次のようであり、この定義は我々の暗黙の前提Γに入っているのでした。

  • ∀x, y∈N(x ≦ y ⇔ ∃z∈N.(x + z = y)) ---(大小順序の定義)

この定義を用いると、a ≦ x は ∃z∈N.(a + z = x) のことなので、「Nに最小元が存在する」は次のことです。

  • ∃a∈N.∀x∈N.∃z∈N.(a + z = x)

これをターゲットとする証明要求は:

  • Γ |-? ∃a∈N.∀x∈N.∃z∈N.(a + z = x)

我々は経験上、自然数の最小元といえば0だと知っています。実際、ターゲットを示す証明の出発点は、∀a∈N.(a + 0 = a) という命題で、これはΓに入っています。先に当該命題の証明を示して、後に説明を続けます。なお、ドルマーク('$')が付いたラベルは、既に前提Γに入っている命題の引用を示します。

証明要求: Γ |-?
         ∃a∈N.∀x∈N.∃z∈N.(a + z = x)

BEGIN ∀導入
  x∈N

  ∀a∈N.(a + 0 = a) ---$(ゼロの中立性)
    --[∀除去 a:=x]
  x + 0 = x
  // 交換律より
  0 + x = x
    --[∃導入 等式左辺のx:←z]
  ∃z∈N.(0 + z = x)
END
●∀x∈N.∃z∈N.(0 + z = x)
  --[∃導入 0:←a]
∃a∈N.∀x∈N.∃z∈N.(a + z = x)

前回既に、∃除去ボックスを出したので、∀導入ボックスにも違和感はないでしょう。∀導入ボックスを絵で描けば次のようです。

テキストと絵を混ぜるのは大変なので、∀導入ボックスをテキストで表現するには:

BEGIN ∀導入
  変数宣言

  :
  :
  ボックス内結論
END
●全称命題

∀導入ボックス内で使う変数を、ボックス冒頭で宣言します。ボックス内結論に∀を付けて(全称束縛して)ボックスの外に出します。黒丸'●'は全称命題を目立たせるマーカーで、特に意味はありません。

具体例である「最小元の存在」の証明では、∀導入ボックス内の変数はxで、ボックス内結論 ∃z∈N.(a + z = x) に自由変数xが入っています。この自由変数xを束縛変数に書き換えて外に出すのですが、

  • 慣れるまでは、自由変数と束縛変数に、別な名前を使うことを推奨。前回述べた推奨事項)

もうこの推奨を破っています。同じ変数名xをそのまま束縛変数にも使っています。破っておいて言うのもナンですが、自由変数と束縛変数は本来別物なんですよ。構文的に完全に区別している例もあります。が、実際には文字が足りなくなるので、同じ名前を使い回すことになっちゃうんですね。

しかしそれでも、∀導入ボックス内で宣言された変数xは、ボックスの外部に絶対に漏れないことには注意してください。ボックス外のxは、たまたま同名の束縛変数であって、ボックス内のxがボックス外まで有効な(生きている)わけじゃないです。プログラミング言語で、ブロック内の変数が外から見えるわけないでしょ、それと同じ。

背理法も使ってみる: 最大元の非存在

前節で最小元を扱ったので、最大元もみておきましょう。最大の自然数は存在しないので、そのことを表現すれば:

  • ¬∃a∈N.∀x∈N.(x ≦ a)

これを示すために次の命題を仮定します(後で証明します)。

  • ∀x∈N.(x ≦ x + 1) ---(a)
  • ∀x∈N.(x ≠ x + 1) ---(b)

この2つをまとめて書けば ∀x∈N.(x < x + 1) ですが、2つに分けた形にしておきます。

今度の証明要求は次のようになります。

  • Γ |-? ¬∃a∈N.∀x∈N.(x ≦ a)

背理法を使うことにすれば:

  • Γ, ∃a∈N.∀x∈N.(x ≦ a) |-? ⊥

'⊥'は矛盾を表す記号です。矛盾を出す証明は次のようになります。

証明要求: Γ, ∃a∈N.∀x∈N.(x ≦ a) |-? ⊥

●∃a∈N.∀x∈N.(x ≦ a)
BEGIN ∃除去
  m∈N
  ∀x∈N.(x ≦ m)
    --[∀除去 x:=m + 1]
  m + 1 ≦ m ---(1)

  ∀x∈N.(x ≦ x + 1) ---$(a)
    --[∀除去 x:=m]
  m ≦ m + 1 ---(2)

  // (1), (2)より
  m + 1 ≦ m ∧ m ≦ m + 1 ---(3)

  ∀x, y∈N.(x ≦ y ∧ y ≦ x ⇒ x = y) ---$(対称律)
    --[∀除去 x:=m, y:=m + 1]
  m ≦ m + 1 ∧ m + 1 ≦ m ⇒ m = m + 1 ---(4)

  // (3), (4)より
  m = m + 1 ---(5)

  ∀x∈N.(x ≠ x + 1) ---$(b)
    --[∀除去 x:=m]
  m ≠ m + 1 ---(6)

  // (5), (6)より
  ⊥
END
⊥

変形後の証明要求の前提(左側)に「最大元が存在する」があるので、その最大元をmと置いて証明を進めています。∃除去ボックス内で遂行される証明は、既に分かっている全称命題の具体化(∀除去)ばっかりです。全称命題の具体化(∀除去)は、通常は無意識に行われています。

さて、補題(a), (b)ですが、あまりに明らかですからこれを公理にしてもいいですが、大小順序の定義と消約律から証明できます。不等号≦を、定義から存在命題に置き換えた形を証明要求としましょう。

証明要求: Γ |-? ∀x∈N.∃z∈N.(x + z = x + 1)

BEGIN ∀導入
  n∈N
  ∀x∈N.(x = x) ---$(等式の反射律)
   --[∀除去 x:=n + 1]
  n + 1 = n + 1
   --[∃導入 左辺の1:←z]
  ∃z∈N.(n + z = n + 1)
END
●∀x∈N.∃z∈N.(x + z = x + 1)

補題(b)を示すには、0 ≠ 1 が公理にあるとします。背理法を使う形の証明要求とします。

証明要求: Γ, x∈N, x = x + 1 |-? ⊥

// 前提から
x = x + 1
// ゼロの中立性から
x + 0 = x + 1
// 消約律から
0 = 1
// 公理 0 ≠ 1 と矛盾するので
⊥

おわりに

前回と今回で、∀導入, ∀除去, ∃導入, ∃除去、これら4つの推論規則の例をある程度は出せたと思います。特に、∀導入と∃除去では、ボックスを使います。ボックスには、そのボックス内でだけ有効な(生きている)変数が伴い、ボックスの先頭で変数宣言します。ボックスの入り口、出口にも決まったお作法があります。念の為再掲すると:

変数リネームは、(あまり守られない)推奨事項です。こういったボックスを意識すると、全称命題/存在命題を間違いなく扱うことが出来ます。

2018-06-14 (木)

論理の存在記号∃をちゃんと使えるようになろう

| 11:09 | 論理の存在記号∃をちゃんと使えるようになろうを含むブックマーク

距離空間や一般の位相空間を勉強中のN君ですが、「任意の」や「存在する」の扱いには苦労しているようです。特に、「前提にある存在命題の使い方が分からない」と。うん、難しいですよね。「習うより慣れろ」と言われても、そう簡単に慣れるもんじゃないです。

∀と∃をちゃんと使うには、実用的なテンプレートを意識して、当座はそのテンプレートに沿って命題や証明を書いたほうがいいと思います。そのようなテンプレート、特に存在記号のためのテンプレートと、その使い方を紹介します。

内容:

  1. はじめに
  2. 例題と予備知識
  3. 自然数の大小順序と証明の例: 反射律
  4. 存在命題を料理するボックスを使ってみよう: 対称律
  5. もっとボックスを使ってみよう: 推移律
  6. おわりに
  1. 全称記号と存在記号に関する推論規則
  2. 全称命題を準備するボックスを使ってみよう: 最小元の存在
  3. 背理法も使ってみる: 最大元の非存在
  4. おわりに

はじめに

イプシロン-デルタ論法はなぜ難しいのか? どうしたら分かるのか? 分かる必要があるのか?」に、次のように書きました。

イプシロン-デルタ論法のために必要なスキルとして、次が要求されています。

  1. 点の集合だけでなく、集合の集合を扱うスキル(あるいは慣れ)。
  2. 「任意の」「存在する」という言葉を含む論理的な表現を扱うスキル(あるいは慣れ)。

これはもちろん、イプシロン-デルタ論法だけではなくて、空間やら構造やらを扱うときは常に必要になります。

「任意の」「存在する」の使い方は、述語論理の推論規則によって統制されているのですが、あまり分かりやすいものではありません。次の2つの記事で詳しく分析しています。が、ちょっと詳し過ぎたかも知れません。

命題の記述や証明がうまく出来ないと「論理的に考えていないから」と思いがちですが、そうとも限りません。単に技術的な問題、つまりノウハウが不足しているだけかもしれません。特に、∀と∃の取り扱いはノウハウが必要です。この記事は、ノウハウと事例の提供を目的にしています。

例題と予備知識

今回例題に使うのは、自然数の順序関係(大小順序関係)です。自然数の全体を N = {0, 1, 2, ...} とします。0も自然数に入れている点に注意してください。自然数の演算としては、足し算しか考えません。足し算は次の法則を満たします。

  • (a + b) + c = a + (b + c) ---(結合律)
  • a + b = b + a ---(交換律)
  • a + 0 = a ---(ゼロの中立性)

他にも必要な法則(公理)がありますが、必要になった時点で導入します。

いま述べた結合律などの法則は、実は全称記号〈全称限量子 | 全称量化子 | universal quantifier〉∀が付いています。

  • ∀a, b, c.( (a + b) + c = a + (b + c) )

法則には常に全称記号が付くので、「常に付くなら常に省略してもいいだろう」と省略されます。

変数 a, b, c は、今の場合は自然数を表します。変数の変域(変数の型)を明示するなら、

  • ∀a, b, c∈N.( (a + b) + c = a + (b + c) )

です。∀a, b, c∈N という書き方も略記で、ちゃんと書くなら:

  • ∀a∈N.∀b∈N.∀c∈N.( (a + b) + c = a + (b + c) )

単に命題をポンと出しても、それの真偽は不明です。「この命題は真だぞ」という主張を伴うなら、「真だぞ」を意味する判断〈judgement〉記号 '|-' を添えたほうが確実です*1

  • |- ∀a∈N.b∈N.c∈N.( (a + b) + c = a + (b + c) )

まーしかし、さすがに面倒くさいので、(a + b) + c = a + (b + c) とだけ書いて、結合律の提示とするのです。「毎回、真面目に律儀に書け」と言う気は無いですが、省略、省略、省略のあげくに簡潔な書き方をしていることは意識すべきです。省略された情報は文脈から補いますが、文脈に頼りすぎるとコミュニケーションが失敗します*2。明示的に書くか、暗黙の前提で済ますかは、よくよく考える必要があります。

「式」という言葉は多義・曖昧過ぎるので、この記事では「命題〈proposition〉」と「項〈term〉」を使います。命題は真偽判定が可能(だと想定されるよう)な文、項はなんかのモノ(例えば自然数)を表す(と想定される)記号表現です。(ただし、単項式/多項式の意味の項とは違います。単項式/多項式の項はサマンド〈summand〉*3のことです。)x や x + 1 は項で、∀x.(x = x + 1) は命題です。

命題を一般的に表すために P, Q などを使い、項を一般的に表すために s, t などを使います。これらはメタ変数なので、書体を変えるのが望ましいのですが、普通のローマン体で書きます。「普通の変数(今回は自然数を表す変数)か? メタ変数(命題や項を一般的に表す変数)なのか?」は、“文脈で”判断してください。

自然数の大小順序と証明の例: 反射律

自然数の大小は、足し算とは独立に理解されるでしょう。例えば、足し算が出来ない小さな子供でも、個数の大小は認識できるかもしれません。しかしここでは、足し算ありきで、大小の順序関係は足し算により定義される、と考えましょう。

  • x ≦ y :⇔ ∃z.(x + z = y) --(大小順序の定義)

':⇔'は、定義であることを強調した論理的同値です。全称記号や変数の型(所属する集合)までちゃんと書けば:

  • ∀x, y∈N(x ≦ y ⇔ ∃z∈N.(x + z = y)) --(大小順序の定義)

いま定義した x ≦ y が、ちゃんと順序関係になっているか、確認します。「x ≦ y が順序関係である」とは次が成立することです。

  • x ≦ x ---(反射律)
  • x ≦ y, y ≦ x ⇒ x = y ---(対称律)
  • x ≦ y, y ≦ z ⇒ x ≦ z ---(推移律)

順に証明を付けていきましょう。

まず反射律に対して次の証明要求を考えます。

  • Γ |-? ∀x∈N.(x ≦ x)

証明要求とは、その名の通り「この命題を証明してください」という依頼や指示のことです。'|-?'の左側が証明のときに使っていい前提で、'|-?'の右側が証明のターゲット命題(目的とする命題)です。大文字ガンマ'Γ'は、諸々の前提をまとめて書くときに使います。

証明要求について詳しくは、次の記事とそこからのリンク先を参照してください。

上記記事には、証明要求の変形についても書いてあり、それを証明の“お膳立て”と呼んでいます。次はお膳立ての例です。

 Γ |-? ∀x∈N.(x ≦ x)
 ----------------------[全称の変形]
 Γ, x∈N |-? x ≦ x

変形後の証明要求は次のようにして証明(契約が履行)されます。

証明要求: Γ, x∈N |-? x ≦ x

x + 0 = x ---(1)
 --[∃導入 0:←z]
∃z.(x + z = x) ---(2)
// 大小順序の定義より
x ≦ x ---(3)

こんな短い証明ですが、いつくもの約束が使われています。それらを説明していきます。

  • 証明の最後の命題は、証明要求のターゲット命題('|-?'の右側)と同じでなければならない。

上の例では、最後の命題(番号は(3))と、証明要求のターゲット命題は、どちらも x ≦ x ですからいいですね。

  • 証明内に出現するすべての命題は、その根拠がハッキリしてなくてはならない。

証明内に出現する命題には (1), (2), (3)と番号がふってあります。(1), (2), (3)すべてに根拠が必要ですが、根拠記述には次の3つの方法を適宜使い分けています。

  1. 根拠が明らかと思える場合は、特に何も書かない(省略)。
  2. 使っている推論規則を推論バー形式で書く。
  3. コメントとして短いヒントを書く。

(1)の x + 0 = 0 は、証明要求の前提('|-?'の左側)から容易に推論できるので、根拠は何も書いてません。(1)から(2)は、「∃導入」と呼ばれる推論規則を使っています。∃導入の一般的な形は次のようです。

     P
 --------------[∃導入 t:←v]
 ∃v.P[t:←v]

ここで、Pは何らかの命題(Pは命題を表すメタ変数)です。P[t:←t] は、Pのなかに含まれる項t(tは項を表すメタ変数)を、変数v(vは変数を表すメタ変数)で置き換えたものです。今の具体例では、

    x + 0 = x
 ------------------[∃導入 0:←z]
  ∃z.(x + z = x)

命題 x + 0 = x のなかに含まれる項 0 (0も項です)を、変数(具体的な実際の変数)zで置き換えた x + z = x に存在限量子 ∃z を付けて ∃z.(x + z = x) を出しています。

なお、推論バーのバー(横棒)の長さを調整するのがイヤになったので、長さは調整しません! ハイフン2,3個並べてバーを表現します。

先の具体例の(2)から(3)はコメントでヒントを書いています。

∃z.(x + z = x) ---(2)
// 大小順序の定義より
x ≦ x ---(3)

大小順序の定義は、x ≦ y ⇔ ∃z.(x + z = y) だったので、yをxに置き換えると、x ≦ x ⇔ ∃z.(x + z = x) 、これと(2)から、(3)が出るわけです。詳細に推論を積み重ねなくても、コメントで十分でしょう。

存在命題を料理するボックスを使ってみよう: 対称律

では次に、対称律の証明にいきましょう。

  • x ≦ y, y ≦ x ⇒ x = y ---(対称律)

この命題をちゃんと書けば:

  • ∀x, y∈N(x ≦ y ∧ y ≦ x ⇒ x = y)

その証明要求は、

  • Γ |-? ∀x, y∈N(x ≦ y ∧ y ≦ x ⇒ x = y)

変形して、

  • Γ, (x, y∈N) |-? x ≦ y ∧ y ≦ x ⇒ x = y

証明要求の左側(前提)に出現する (x, y∈N) は、一種の変数宣言だと思ってください。もう少し変形(お膳立て)しておきましょう。

  Γ, (x, y∈N) |-? x ≦ y ∧ y ≦ x ⇒ x = y
  ----------------------------------------------[含意の変形]
  Γ, (x, y∈N), (x ≦ y ∧ y ≦ x) |-? x = y
  ----------------------------------------------[前提の連言を分解]
  Γ, (x, y∈N), x ≦ y, y ≦ x |-? x = y

さらに、x ≦ y と y ≦ x を、大小順序の定義により書き換えれば:

  • Γ, (x, y∈N), ∃z∈N.(x + z = y), ∃z∈N.(y + z = x) |-? x = y

これでお膳立ては終わり。実際の証明にかかります。

前提(証明のときに使ってよい命題達)に∃が入っているので、これは「前提にある存在命題の使い方」を練習するチャンスです。存在命題を使うときは、専用のボックスを使いましょう

ボックスは、「全称記号の導入規則について考える」と「存在記号の除去規則について考える」で説明したもので、次のようなものです。

この絵がピンと来なくてもいいです。∀や∃の扱いでは、証明の一部分を囲むボックスが必要だ、と認識してください。存在記号∃の除去〈elimination〉に使うボックスは次のようです。

さっそく実際に使いたいのですが、テキストで書いた証明内でボックスをリアルに描くのは非常にめんどくさいので、次の記法を使います。

●存在命題
BEGIN ∃除去
  変数宣言
  変数の条件
  :
  :
  ボックス内結論
END
ボックス内結論

BEGIN/ENDとインデントを使います。黒丸'●'は、存在命題が目立つようにです。この形式で対称律の証明を行います。説明は後でします。

証明要求:  Γ, (x, y∈N), ∃z∈N.(x + z = y), ∃z∈N.(y + z = x)
          |-? x = y

●∃z∈N.(x + z = y)
BEGIN ∃除去
  a∈N
  x + a = y ---(1)
  ●∃z∈N.(y + z = x)
  BEGIN ∃除去
    b∈N
    y + b = x ---(2)
    // (1)と(2)から
    (x + a) + b = x
    // 結合律から
    x + (a + b) = x
    // ゼロの中立性から
    x + (a + b) = x + 0
    // 消約律(後述)から
    a + b = 0
    // ゼロ和自由性(後述)から
    a = 0 ∧ b = 0
    // 連言の左を取り出して
    a = 0 ---(3)
    // (1)と(3)から
    x = y
  END
  x = y
END
x = y

証明のなかで、まだ触れてない法則が出てくるので、それを述べておきます。消約律 〈cancellation property | cancellation law〉は次の形の法則です。

  • a + x = a + y ⇒ x = y

ちゃんと書けば:

  • ∀a, x, y∈N.(a + x = a + y ⇒ x = y)

ゼロ和自由性〈zerosumfree property〉は次の形。

  • a + b = 0 ⇒ a = 0 ∧ b = 0

ちゃんと書けば:

  • ∀a, b∈N.(a + b = 0 ⇒ a = 0 ∧ b = 0)

これらの法則については次の記事で述べています。興味があればどうぞ。

さて、問題の存在命題の扱い方ですが、この具体例では、∃除去ボックスを入れ子にして使っています。ほとんどの証明は内側の∃除去ボックスで遂行されているので、内側の∃除去ボックスだけ取り出します。

  ●∃z∈N.(y + z = x)
  BEGIN ∃除去
    b∈N
    y + b = x ---(2)
    :
    :
    x = y
  END
  x = y

存在命題 ∃z∈N.(y + z = x) をこの∃除去ボックス内で料理します。ボックスの1行目は、ボックス内だけで使う変数の宣言です。この変数*4の名前の選び方は次のとおり。

  1. ボックス内から、ボックス外の変数を参照することがあるので、外部の変数と違う名前を選ぶ。これは守るべし!
  2. 存在命題の束縛変数とは違う名前を選んだほうが事情がハッキリする。これは、あまり守られてないし、破っても実害はない。が、最初のうちは混乱を防ぐために違う名前を推奨。

上の具体例では、

  1. ボックスの外側で、x, y, aが既に使われているので、これと同じ名前はダメ。
  2. 存在命題の束縛変数がzだから、混乱を避ける意味でzと別な名前にする。

で、ボックス内で使う変数にbを選んでいます。変数名の衝突や、紛らわしい名前による混乱を避けるため、変数名の選択法は重要なスキルです。にも関わらず、明示的に述べられず、トレーニングの機会も少ないのは困ったことです。

∃除去ボックスの2行目は、今導入したボックス内変数(具体的にはb)に関する条件です。もとの存在命題の束縛変数(具体的にはz)を、ボックス内変数で置き換えた命題を書きます。y + z = x のzをbに置き換えるので、y + b = x となります。

あとは、ボックス内で証明を遂行して結論を出します。ボックス内の結論には、変数宣言で導入したボックス内変数が入っていてはダメです。ただし、束縛変数なら話が別です。例えば、∀b∈N.(...) のようにbを使うなら問題ありません。とはいえ、これも混乱のもとなので、自由変数(ボックス内変数も自由変数)と、∀, ∃の束縛変数は別な名前を使いましょう。慣れた人は同じ変数を平気で使い回す*5ので、それがまた初心者を困惑させたりします。

  • 慣れるまでは、自由変数と束縛変数に、別な名前を使うことを推奨。

ボックス内結論は、ボックスの外に取り出します。同じ命題を2回書くので冗長ですが、∃除去ボックスのスコープから結論をエクスポートしたことを確認する意味で、2回書きましょう*6。結論がボックス外に取り出せるために、ボックス内変数bが入っていてはダメなのです。

以上に述べたことが、前提である存在命題の使い方の決まり文句=テンプレートです。律儀に守ると、かなり冗長になりますが、慣れるまではテンプレート通りに書きましょう。

もっとボックスを使ってみよう: 推移律

推移律の証明もやってみましょう。証明要求は、次のようです。

  • Γ |-? ∀x, y, z∈N.(x ≦ y ∧ y ≦ z ⇒ x ≦ z)

前節と同じ要領で証明要求を変形すれば:

  • Γ, (x, y, z∈N), ∃z∈N.(x + z = y), ∃w∈N.(y + w = z) |-? ∃w∈N.(x + w = z)

(わざとに)自由変数と束縛変数を同じ名前にしているので、注意してください。紛らわしいだけで間違いではありません。この設定で推移律を証明してみましょう。

証明要求: Γ, (x, y, z∈N), ∃z∈N.(x + z = y), ∃w∈N.(y + w = z)
          |-? ∃w∈N.(x + w = z)

●∃z∈N.(x + z = y)
BEGIN ∃除去
  a∈N
  x + a = y ---(1)
  ●∃w∈N.(y + w = z)
  BEGIN ∃除去
    b∈N
    y + b = z ---(2)
    // (1), (2)より
    (x + a) + b = z
    // 結合律より
    x + (a + b) = z
     --[∃導入 (a + b):←w]
    ∃w∈N.(x + w = z)
  END
  ∃w∈N.(x + w = z)
END
∃w∈N.(x + w = z)

前節とほとんど同じなので、説明は要らないですね。

注意すべきは、やはり変数の使い方です。あえて、同名の自由変数と束縛変数を使っています。自由変数と同名の束縛変数を使うのはかまいません(でも、ときに混乱をまねきます)。異なる命題で同じ束縛変数を使うのも問題ありません(でも、ときに混乱をまねきます)。上の証明内に現れる変数は:

  1. 自由変数 x, y, z(前提で宣言されている)
  2. 束縛変数z(前提の命題)
  3. 束縛変数w(前提の命題)
  4. 自由変数a(外側の∃除去ボックスで宣言されている)
  5. 自由変数b(内側の∃除去ボックスで宣言されている)
  6. 束縛変数w(ターゲット命題、内側の∃除去ボックス内の∃導入で導入)

こういった変数の名前と型(変域、所属する集合)、そしてスコープ(有効範囲)の管理がとても大事です。変数に名前・型・スコープがあること、スコープは入れ子のブロック構造になること -- このへんはプログラミング言語と同じです。自然言語で適切に表現するのは難しいです。

だから、機械可読で、機械(ソフトウェア)でチェック可能な人工言語で証明を書くほうがいいと僕は思うのですが、残念ながら、広く実用に耐える証明支援系は存在しません。

こうすればCoqに入門できそうだ (誰も書かないCoq入門以前 5)」:

Coqに関する情報はけっこう多いのですが、ゲームとして遊び始めるための良い説明は少ないです。多くの人が入門的な解説を試みてはいますが、Coqの入門的な説明はとても困難だと思います。

Isabelleについて: 証明支援系は何を目指し、どこへ向かうのか」:

Isabelleが世の趨勢と離れるのか? という話をしてますが、有り体に言えば、もともとIsabelleは独特の文化を持った癖の強い処理系で、利用者は特殊な人々です。証明支援系を使いたくても、Isabelleを避ける人はいるでしょう。僕自身、Isabelleは「ダメだこりゃ」と思った1人です。

Mizar、嫌いじゃないんだけどな」:

僕はほんとに「もったいない」と思っています。システムとコミュニティがこのままだと、せっかく蓄積した膨大なライブラリもあまり活用されないままに朽ちていく懸念さえあります。それはあまりにも「もったいない」。

Globularの使い方 (1)」:

3次元ビュー、まともなアニメーション機能、5次元以上の正しい計算モデルなどは(ユーザーなら)誰でも欲しいでしょうが、実現するのは何年先でしょうか? このソフトウェアの性格からいって、10年、20年のスパンで進化と成長を見守るべきでしょう。

おわりに

自然数の大小順序だけでも、まだネタはありますし、もう少し練習問題があったほうがいい気もします。全称記号∀に関する説明が不足してるし、∀と∃の関係も述べていません。が、長くなるので今回はこのくらいにしておきます。

論理の教科書には、推論バーの積み重ねで証明が出来るかのごとくに書かれていますが、それだけでは不十分です(「自然演繹はちっとも自然じゃない -- 圏論による再考」参照)。ボックス(ブロック)の入れ子構造と、変数のライフタイム管理も必要です。

とりあえず、∃除去ボックスのテンプレートを使えるようにしましょう。慣れるまでは、変数のスコープに意識を向け、冗長でも律儀に変数をリネームしましょう。


続きがあるよ。

*1:記号'|-'は構文論的な真(公理か証明済み)を主張します。一方、記号'|='は意味論的な真を主張します。

*2:「何言ってるか(書いていあるか)よく分からない」ときは、文脈を共有できてないことが多いです。

*3:サマンドの訳語に「加数」というのがあるようですが、あんまり聞かないですね。

*4:固有変数〈eigenvariable〉、またはパラメータと呼ぶようですが、あまり使われない言葉なので、ボックス内変数にしておきます。

*5:同じ変数の使い回しをしないと、文字が足りなくなってしまうので、実際的には使い回しをせざるを得ない事情があります。

*6:変数水増しオペレーターの効果も考えると、まったく同じ命題を2回書いているのではありません。見た目は同じでも議論域〈domain of discourse〉は変わっています。変数水増しオペレーターについては、「存在記号の除去規則について考える」を参照。

hitotakuchanhitotakuchan 2018/06/14 12:02 私は最近一人だけですが数学の個別指導をしていて、この辺りの厳密な演繹ルールを教えるのに Coq を使いました。
彼は最終的には量化子も含めちゃんと使えるようになったので指導法としてよかったと考えています。

最終的には、演繹ルールの厳密な運用よりも教科書にある自然言語で書かれた定義を、論理式として正確に表現する能力の方が獲得が難しいという結論に至っていて、こちらの方はどうやって指導していけばいいのか解決策を見いだせていません。

m-hiyamam-hiyama 2018/06/14 12:12 hitotakuchanさん、
> 演繹ルールの厳密な運用よりも教科書にある自然言語で書かれた定義を、論理式として正確に表現する能力の方が獲得が難しいという結論に至っていて、

そう、そう、そう。まったくそのとおり!
だいたい僕自身が、日本語と形式言語の翻訳が出来ません。
この記事の半形式的証明を、日本語にエンコードすることも(不可能でないけど)難しいし、負担だと思います。

(一般の日本語ではなくて)論理的な内容を記述する日本語自体をフォーマルに構文定義しないとダメかな、とか思っています。

2018-06-12 (火)

謎の食券販売機@渋谷

| 14:59 | 謎の食券販売機@渋谷を含むブックマーク

以前、松屋の食券販売機を話題にしたことがあります。

上記記事は、対話的機械としての“ユーザーインターフェースの悪さ”を指摘したものです。

最近、見た目も振る舞いも謎な食券販売機を渋谷で見かけました。


渋谷の「大勝軒まるいち」は、本家「東池袋大勝軒」山岸氏の最後のお弟子さんのお店だそうです。僕は、東池袋大勝軒に行ったことはありますが、どんな味だったかハッキリとは覚えてないので、「まるいち」と本家を比較して云々はできません。が、つけ麺おいしかったです。

さて、その「まるいち」の食券販売機がこれです。

まず、最初のツッコミポイントは、お釣り出口(↓)です。いったい、どっちからお釣りが出るんじゃい?

結果を言うと、上のほうからお釣りが出ました。下の方の出口は変な突起がついていて、なんなんだか分かりません。

この自販機は、完全に明示的な指示をしないと動きません。例えば千円札を入れて、950円注文し、50円以下のメニュー項目がなくても、[発券]ボタン(↓)を押さないと食券が出てきません。無事に食券が出てきても、明示的に[おつり]ボタン(↓)を押さないとお釣りが出てきません。

僕は、発券したらお釣りは出てくるもんだと思い込んでいたいので、しばらく待ってしまいました。いつまでたってもお釣りが出てこないので[おつり]ボタンの存在に気付いた次第。

ソフトウェア部分(液晶パネル)には、キャンセルがなかったような気がします(記憶のみ)。そこで、存在感のあるこのキャンセルレバー

表示を見る限り、コインのキャンセル(返却)にしか使えない感じです。お札のキャンセルはどうしたらいいんでしょう。(今度行ったら、お札のキャンセルに挑戦してみます。)

トラックバック - http://d.hatena.ne.jp/m-hiyama/20180612

2018-06-07 (木)

確率空間の凸結合と分割

| 18:40 | 確率空間の凸結合と分割を含むブックマーク

確率空間に対して、直和に似た演算として凸結合を導入し、そこから見方を変えて確率空間の分割を定義します。

内容:

  1. 確率空間
  2. 確率空間の独立積
  3. 確率空間の直和類似物は?
  4. 確率空間の凸結合
  5. 確率空間の分割
  6. おわりに

確率空間

この記事は、もっと長い記事の前半部分を切り出したものです。ありていに言えば、息切れしたので、一区切りつけたものです。続き(後半)がそのうち出るかも(出ないかも)。

まずは確率空間の定義; 確率空間〈probability space〉は、(Ω, Σ, μ)という3つ組です。ここで:

  • Ωは集合。なんでもいい。
  • Σは、Ωのベキ集合Pow(Ω)の部分集合で、σ代数(完全加法族ともいう)であるもの。
  • μは、Σ上の測度で、μ(Ω) = 1 となるもの。

Ωを確率空間の台集合〈underlying set〉と呼びます。「標本空間」という言葉は混乱のもとなので使いません。台集合Ωはなんでもいいですが、Ωが空集合だと μ(Ω) = 1 となる測度μが作れないので、結果的には非空集合になります。

Σの要素を「事象」と呼ぶことがありますが、この言葉も使いません。代わりに可測集合〈measurable set〉といいます。

μ(Ω) = 1 という条件を満たす測度を確率測度〈probability measure〉と呼びます。確率測度を単に「確率」、あるいは単に「測度」というのは好ましくないので、なるべく使わないようにします(絶対に使わないとは言ってない)。

いくつかの確率空間を考えるとき、それらを区別するために、

  • X = (ΩX, ΣX, μX)
  • Y = (ΩY, ΣY, μY)

のように書きます。記号の乱用により、

  • X = (X, ΣX, μX)
  • Y = (Y, ΣY, μY)

のようにも書きます。ΣXをΣXと書くこともあります。

写像 f:ΩX→ΩY が次の条件を満たすとき、確率空間XからYへの準同型写像〈homomorphism〉と呼びます。

  1. B∈ΣY に対して、f*(B)∈ΣX、f*は逆像を対応させる写像。
  2. B∈ΣYに対して、μY(B) = μX(f*(B)) が成立する。

確率空間を対象として、確率空間のあいだの準同型写像を射とする圏ができるので、それをProbと書きます。圏Probの射である準同型写像は、確率保存写像〈probability preserving {map | mapping}〉と呼ぶことが多いです。

確率空間の独立積

X = (X, ΣX, μX), Y = (Y, ΣY, μY) が2つの確率空間のとき、台集合の直積 X×Y 上には、標準的〈canonical〉な確率空間構造が構成できます。実際に作ってみましょう。XとYをもとに(これから)作る確率空間をZとします。Z := X×Y です。

ΣZを作るために、矩形〈rectangle | 長方形〉の話からします。X, Yは単なる集合だとして、

  • rect:Pow(X)×Pow(Y)→Pow(X×Y)

を次のように定義します。

  • for A∈Pow(X), B∈Pow(Y), rect(A, B) := A×B ∈Pow(X×Y)

あるいはラムダ記法を使って、

  • rect := λA∈Pow(X), B∈Pow(Y).(A×B ∈Pow(X×Y))

要するに、“二辺”A, B から矩形を作り出す写像がrectです。

rectをΣX×ΣYに制限すると、

  • rect|ΣX×ΣY : ΣX×ΣY→Pow(X×Y)

ができます。この写像rect|ΣX×ΣYの像は、Pow(X×Y)の部分集合となるので、それをRect(ΣX, ΣY)とします。

  • C∈Rect(ΣX, ΣY) ⇔ A∈ΣX, B∈ΣY が存在して、C = A×B と書ける。

Rect(ΣX, ΣY)は、“二辺”がそれぞれΣX、ΣYに入るような矩形の集合です。

Rect(ΣX, ΣY)を含むような Z = X×Y 上のσ代数で最小のものが一意に決まる(可測空間に関する定理)ので、それをΣX¥otimesΣYとします。

  • ΣX¥otimesΣY := (Rect(ΣX, ΣY)から生成された、X×Y上のσ代数)

ここまでで、集合 Z = X×Y = ΩZ とZ上のσ代数 ΣZ = ΣX¥otimesΣY が構成できました。組み合わせた (Z, ΣZ) は可測空間です。

可測空間(Z, ΣZ)上の測度μZを、A×B∈Rect(ΣX, ΣY) に対して、

  • μZ(A×B) = μX(A)μY(B) (右辺は実数の掛け算)

が成立するように決めます。そのような測度は一意的に存在する(測度に関する定理)ので、μZ = μX¥otimesμY と書きます。

3つ組 (Z, ΣZ, μZ) が確率空間になることは容易に確認できます。Z = X×Y, ΣZ = ΣX¥otimesΣY, μZ = μX¥otimesμY だったので、確率空間としてのZをX¥otimesYと書きます。

  • X¥otimesY = (X×Y, ΣX¥otimesΣY, μX¥otimesμY)

このようにして作ったX¥otimesYを、XとYの直積と呼びたくなりますが、そうは呼びません! 理由は、¥otimesは圏Probの圏論的直積にはならないからです。f:X→Y, g:V→W in Prob に対しても f¥otimesg:X¥otimesV→Y¥otimesW を定義して、¥otimesProb上のモノイド積にすることは出来ますが、直積の条件は満たしません。

直積にはならないProb上のモノイド積¥otimesは、独立積〈independent product〉と呼びます。確率的独立性〈stochastic independence〉と関係するからです。

モノイド積としての独立積に関しては次の論文が詳しいです。ただし、「射影付き(または入射付き)テンソル積」という言葉が使われています。

独立性の一般論は次を参照。

確率空間の直和類似物は?

前節で述べた確率空間の独立積は、圏論的直積〈デカルト積〉にはなりませんが、台集合の直積の上に載っかる確率空間構造なので、直積に近いとは言えます。では、台集合の直和の上に載っかる確率空間構造はあるでしょうか? もしあるなら、それは、直和に近いモノイド積となるでしょう。

X = (X, ΣX, μX), Y = (Y, ΣY, μY) として、集合として Z = X + Y とします。集合としてのZ上に、なるべく自然な確率空間構造を定義することを目的にします。

まず Pow(X + Y) ¥stackrel{¥sim}{=} Pow(X)×Pow(Y) であることに注意します。Pow(X)×Pow(Y)→Pow(X + Y) 方向の同型(全単射)をsumとします。sum(A, B) := (A + B in X + Y) です。sumをΣX×ΣYに制限して像を取ると、それはPow(X + Y)の部分集合になるので、Sum(ΣX, ΣY) と置きましょう。

  • C∈Sum(ΣX, ΣY) ⇔ A∈ΣX, B∈ΣY が存在して、C = A + B と書ける。

Sum(ΣX, ΣY) ⊆ Pow(X + Y) から生成される最小のσ代数をΣZとします。すると、(Z, ΣZ)は可測空間になります。

(Z, ΣZ)上で定義される測度μZを、次が成立するように定義します。

  • μZ(A + B) = μX(A) + μY(B)

以上により、測度空間(Z, ΣZ, μZ) が構成できます。この定義は自然に思えます。が、しかし、μZは確率測度になっていません。μZ(Z) = μX(X) + μY(Y) = 2 だからです。

μZ(Z)を1にするために、μXとμYに1/2ずつの重みを付ける案がありますが、そうすると、モノイド積としての結合律が成立しません。

そもそも、2つの確率空間を常に対等な重さで扱うのは根拠がない気がします。そこで、p + q = 1 となる非負実数p, qを用意して、

  • μZ(A + B) = pμX(A) + qμY(B)

と定義してはどうでしょう。これなら確かに確率測度になります。この確率測度μZを持つ確率空間(Z, ΣZ, μZ)を、

  • Z = pX + qY

と書いてもいいでしょう。係数p, q付きの和は、モノイド積にはなりませんが、2つの確率空間を重み付きで足したもの、というハッキリした意味を持ちます。

確率空間の凸結合

ベクトルxとyの凸結合とは、p + q = 1 となる非負実数p, qを係数とした足し算 px + qy のことです。xとyがベクトル(ベクトル空間の要素)のときは、px + qy はそのまま意味を持ちますが、前もって足し算がなくても、凸結合を公理的に定義することができます。

Cを集合として、0≦ q ≦1 である実数qに対して、写像 γq:C×C→C が定義されていて、次の条件を満たすとします。

  1. γ0(x, y) = x
  2. γq(x, x) = x
  3. γ1-q(x, y) = γq(y, x)
  4. γq(x, γp(y, z)) = γpqr(x, y), z) ただし、q(1 - p) = (1 - pq)r

最後の条件がちょっと複雑ですが、一種の結合律だとみなせます。Cに足し算があるときは、γq(x, y) = (1 - q)x + qy と定義するとこれらの条件を満たします。

集合Cと上記の条件を満たすγの組(C, γ)を凸空間〈convex space〉と呼びます。γpは、パラメータqを持つ二項演算で、(公理的に定義された)凸結合〈convex combination〉と呼びます。(詳しくはnLab項目を参照。)

γ自体はパラメータ付き二項演算ですが、γを入れ子にすることにより、p1 + p2 + ... + pn = 1 であるような非負実数の列 p1, p2, ... ,pn に対する凸結合を定義できます。足し算がない場合でも、記法としては足し算を使って、

  • p1x1 + p2x2 + ... + pnxn

のように書きます。あたかも足し算があるかのように扱ってかまいません。

さて、前節で定義した pX + qY ですが、これを γq(X, Y) := (1 - q)X + qY とすると、(|Prob|, γ)は凸空間になります。|Prob|は普通の集合ではなくて大きな集合〈プロパークラス〉なので、(|Prob|, γ)は”大きな凸空間”と言うべきかもしれません。大きさを気にしなければ、凸空間の議論はすべて(|Prob|, γ)に対しても適用できます。

f:X→Y, g:V→W in Prob に、(pf + qg):(pX + qW)→(pV + qW) と重み付けできるので、対象だけでなく射の凸結合も定義できます。これにより、圏Probは凸空間としての構造を持つことになります。

僕は理解してないのですが、凸空間の構造を持つ圏は、エントロピーの定義と関係するようです。バエズ〈John Baez〉による次のページに色々書いてあります。

確率空間の分割

p1 + p2 + ... + pn = 1 であるような非負実数の列 p1, p2, ... ,pn と、n個の確率空間 X1, X2, ..., Xn があったとします。前節で述べたように、これらの凸結合が定義できます。

  • Z = p1X1 + p2X2 + ... + pnXn

各Xi(i = 1, 2, ..., n)は確率空間であり、それらを重み付きで寄せ集めたZもまた確率空間です。

ここで、発想を逆転させて、確率空間Zが最初にあって、それを小さな確率空間達 X1, X2, ..., Xn に分割したと考えましょう。凸結合と同じことではありますが、Zの分割〈partitioning | disjoint decomposition〉を定義すると:

  1. 台集合として、Z = X1∪X2∪...∪Xn である。
  2. i ≠ j ならば、Xi∩Xj は空集合である(互いに共通部分がない)*1
  3. 各Xiには、Zのσ代数/確率測度から“誘導された”σ代数/確率測度により、確率空間の構造が入る。詳細は割愛するが、条件付き確率になる。
  4. 各Xiに非負実数piが割り当てられていて、すべてのpiを足すと1になる。

μZ(Xi) ≠ 0 とか pi ≠ 0 を仮定しておいたほうが扱いやすそうですが、かえって邪魔になることもありそう … よく分かりません。

いずれにしても、確率空間達の凸結合(重み付きの和)と、確率空間の分割(これも重み付き)は事実上同じものです。複数の確率空間達を集約してひとつにするか、ひとつの確率空間を分割して複数の確率空間達を得るか -- 見方の違いがあるだけです。

集約/分割のときに使う重みの列 p1, p2, ..., pn を、積分して1になる関数 p(t)(t∈T)に置き換えたらどうなるんだろうな? と思ったりします。t∈T に対する各Xtが確率空間で、ZはXt達を重み付きで束ねた(バンドルした)確率空間になります。このような“確率バンドル”、あるいは“確率ファイブレーション”を、「分布から拡散へ: ミシェル・ジリィを巡って」で述べた拡散圏のなかで考えたら面白いかもしれません。よく分からんけど。

おわりに

冒頭に書いたように、この記事は、もっと長い記事の一部分になる予定のものでした。残る話題は何かというと、確率空間の凸結合/分割が、より一般的なメカニズムの事例ではないか、ということです。前節で、有限個の重みを連続化することを書きましたが、ソッチ方面への拡張ではありません。有限個のままでも、なんか面白いことがあるような気がします。

*1:Xi∩Xjが測度ゼロの集合になる、でもいいでしょうが、煩雑なので空集合にしておきます。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20180607

2018-06-06 (水)

分布から拡散へ: ミシェル・ジリィを巡って

| 12:34 | 分布から拡散へ: ミシェル・ジリィを巡ってを含むブックマーク

確率・統計の概念・用語には、不明瞭なものが多くて難儀します。こういった不明瞭さに対して、きわめてクリアな解釈を与えてくれる道具にジリィモナド〈Giry monad〉があります。

ところが、ジリィモナド周辺もかなりとっ散らかった印象があります。ジリィモナドには多様なバリエーションがあるのですが、それらを包括的に語る言葉が不足しています。

物理現象である“拡散”をメタファーにすると、ジリィモナドを直感的に把握できるようになり、用語法の整理にも寄与することになります。

内容:

  1. 分布を寄せ集めると
  2. ローヴェアとジリィの定式化
  3. 「拡散」がよくね
  4. ジリィの原典を眺めると
  5. ジリィ・スタイルのモナド
  6. ジリィモナドの相対化
  7. 資料

分布を寄せ集めると

以前、「確率分布」って言葉の意味が分からないなー、と嘆いていました。結果的に言えば、確率分布の意味は“確率測度または確率密度関数”です。そのどちらを意味するかは文脈によるし、ニュアンスを含めることもあります。

曖昧性やニュアンスがあることで分かりにくい言葉になっていますが、一方で、曖昧ゆえに使い勝手がいい言葉でもあります。

さて、分布のフォーマルな定義は一旦脇に置いて、分布という言葉の直感的な印象、あるいは雰囲気にについて語ります。

分布というからには、なにか空間的に広がっている印象がありますよね。Yが空間だとして、「yがYの点だ」とは、yが、点集合としてのYの要素ということです。一点yは分布していません。物理的に言えば、質量1の質点みたいなものです。

それに対して分布したモノは、一点ではなく、滲〈にじ〉んで広がっています。空間にモヤッと物質が存在する感じです。質点とは限らない物質は、その質量密度関数で記述できるでしょう。よって、分布を密度関数と同一視するのは悪くないと思えます。

Yの一点とは、単元集合〈singleton set〉 1 = {0} からYへの写像と言っても同じです。f:1→Y と f(0)∈Y は1:1に対応しますから。そうなると、分布は、写像 f:1→Y が滲んで広がってしまったモノとみなせます。

いま、別な空間Xを持ってきて、写像 f:X→Y を考えます。x∈X に対して f(x) はYの点です。確定した一点です、滲んでません。もし、f(x) が滲むと、Xの各点xに対して、Y上の滲み(あるいは物質)が対応することになります。点xに対応する滲みが F(x) です。

上の図では、Xの点が3つしか描いてありませんが、もっとたくさんの点があってもいいです。むしろ、Xに無限個の点があるほうが普通でしょう。無限かもしれないXの各点に、Y側の滲み(あるいは物質)が対応する状況です。各点ごとの分布が寄せ集まった状況とも言えます。

ローヴェアとジリィの定式化

Xの点でパラメトライズされた、Y上の滲み(あるいは物質)の集まり -- これをうまく定義する方法はウィリアム・ローヴェア*1〈William Lawvere〉により提案され、ミシェル・ジリィ〈Michèle Giry〉*2によりキチンと定義・調査されました。

空間Y上の確率分布〈probability distribution〉をすべて集めた集合をPDist(Y)と書きましょう。いま出た「確率分布」は雰囲気的なモノではなくて、確率論の意味での確率分布 -- つまり確率測度または確率密度関数のことです。

ローヴェア/ジリィのアイディアは、F:X→PDist(Y) という写像を使う、というものです。F:X→PDist(Y) は、Xの各点xに対して、Y上の確率分布 F(x) を対応させます。Y上の確率分布は、Y上に広がったモノ/滲んだモノ/物質(総質量は1)などの定式化になっています。

いま説明したような F:X→PDist(Y) を何と呼ぶか? これが実に困った状況でして、「ライプニッツの微分記法とアインシュタインの総和規約を測度に使ってみる」で言ったように、山のように呼び名があります。

  1. stochastic map
  2. stochastic kernel
  3. stochastic relation
  4. stochastic matrix (台集合が有限のとき)
  5. probabilistic mapping
  6. probabilistic relation
  7. probabilistic matrix (台集合が有限のとき)
  8. regular conditional probability
  9. conditional probability density
  10. Markov kernel
  11. Markov matrix (台集合が有限のとき)
  12. transition probability
  13. transition probability density
  14. transition kernel
  15. transition matrix (台集合が有限のとき)
  16. probabilistic channel
  17. stochastic channel

このブログ内で使ったことがある呼び名は:

  1. 確率写像〈probabilistic mapping〉
  2. 確率関係〈stochastic relation〉
  3. 測度的積分核〈measure-theoretic integral kernel〉
  4. マルコフ行列〈markov matrix〉

測度的積分核は、確率写像/確率関係より広い意味で使っています。マルコフ行列は、扱う空間が有限集合のときの言葉です。

ちなみに、ローヴェア/ジリィのアイディア/定式化に(ゆるく)関係する過去記事には次があります(古い順)。

  1. 何故にあえて確率を学ぶのか?
  2. 測度的積分核と随伴構造
  3. 合同を持つ圏と測度空間の圏
  4. 質量モナド
  5. ライプニッツの微分記法とアインシュタインの総和規約を測度に使ってみる
  6. 同時確率分布の圏
  7. 同時確率分布の圏の使用例:超具体的
  8. アブダクションと確率的推論
  9. 確率的推論・判断の計算法:マルコフ・テンソル絵算
  10. 余可換コモノイド・モダリティ事件の解説

話を戻して、F:X→PDist(Y) を何と呼ぶか? -- X = 1 = {0} のときはY上の分布なので、分布と関連する言葉/親和性がある言葉がいいんじゃないのかな、と僕は思いました。

「拡散」がよくね

分布と同様に、広がって滲む感じの言葉? 「余可換コモノイド・モダリティ事件の解説」で、分散〈dispersion〉という言葉は使ったことがあります(否定的に「非分散的」として)。溶解〈disolution〉も同じ雰囲気です。でも、拡散〈diffusion〉が一番よく使いそうです。

ローヴェア/ジリィの F:X→PDist(Y) を拡散〈diffusion〉、あるいは拡散写像〈diffusion {map | mapping}〉と呼んではどうでしょう。

雰囲気はあってますよね。でも、物理的現象として拡散現象があるし、拡散方程式なんて偏微分方程式もあります。そういう意味での拡散と、ローヴェア/ジリィのアレが乖離していると、「拡散」という言葉を割り当てるのはよろしくない気がします。

そこで、物理現象のモデルとしての拡散について調べてみました。ちら見しただけで、理解はできませんが、どうやら拡散過程〈diffusion process〉とはマルコフ過程〈Markov process〉の一種のようです。拡散過程を特徴付ける重要な等式として、チャップマン/コルモゴロフ方程式〈Chapman-Kolmogorov equation〉というものがあるようです。

その他に、遷移確率(密度)〈transition probability (density)〉、条件付き確率密度〈conditional probability density〉なんて言葉も拡散の話に出てきます。ローヴェア/ジリィと同じ用語が出てくるなー。なんか関連があると思っていいのかな。

ジリィの原典を眺めると

現在、ジリィの論文はインターネット上にもあります*3

最初の一文がイキナリ:

The aim of this paper is to give a categorical definition of random processes and provide tools for their study.


この論文の目的は、確率過程を圏論的に定義して、それらを調べる手段を提供することである。

random processって確率過程、それがジリィの目的だったのか。すぐにマルコフ過程の話になり、圏論的な結合〈composition〉を定義する等式はチャップマン/コルモゴロフ方程式だと述べています。

えっ、これは拡散過程の話とモロカブリじゃん。ジリィの本来の意図からしても、F:X→PDist(Y) は拡散過程の遷移記述だとみなしてよさそうです。ローヴェア/ジリィが定義した圏Pの射を拡散写像と呼ぶなら、確率過程は、順序構造により圏とみなしたNR≧0からPへの関手となります。もっとも単純(原子的)な遷移のステップがPの射=拡散写像となります。

ジリィはまた、次のようにも語っています。

As F. W. Lawvere already pointed out in an unpublished paper [3] in 1962, most problems in probability and statistics theory can be translated in terms of diagrams in these Kleisli categories.


ローヴェアが、1962年の未出版の論文で既に指摘しているように、確率や統計のほとんどの問題は、これらのクライスリ圏内の図式による表現へと翻訳できる。

うん、これはホントだと思う

で、上記引用内の未出版の論文とは、ローヴェアがおこなったセミナーの資料です。"the highly referenced seminar handout notes"ということで、カーク・スターツ(Kirk Sturtz)が、書き込みが入った紙資料をスキャンして公開しています。

スターツは、「確率変数」と言うのはやめようと言った人です。スターツ自身、ローヴェア/ジリィ路線の論文を何編も書いています。

ジリィ・スタイルのモナド

さて、既に山のように同義語があるのに、新しい言葉が欲しかった理由を説明しましょう。

既存の用語の多くには、stochastic, probabilistic, probability が含まれます。確率的ということですが、それは全空間の測度が1を意味します。しかし、全空間の測度が1でない状況も扱いたいのです。となると、残る言葉は(正規表現で書けば)、{Markov | transition} {kernel | matrix} です。{kernel | matrix}は、表現・表示の手段であり、圏の射そのものを表すには不適切な気がします。以前僕が使っていた測度的積分核も同じ理由でよくありません。

結局、既存用語はどれも不合格です。今後は、拡散写像〈diffusion {map | mapping}〉を採用します。拡散写像を射とする圏は、拡散写像の圏〈category of diffusion {maps | mappings}〉または単に拡散圏〈diffusion category〉と呼ぶことにします。

拡散圏を定義するには、ジリィ・スタイルのモナド〈Giry-style monad〉の説明が必要です。モナドが定義できれば、拡散圏はそのクライスリ圏として定義できます。

現在ジリィモナドと呼ばれているモノは、特定のモナドではなくて、一群のモナド達の総称です。ジリィ自身、可測空間をベースにするモナドとポーランド空間をベースにするモナドの二種類を定義しています。

まず、基礎となる圏Hを選びます*4Hは、可測空間と可測写像の圏Measへの忘却関手(忠実関手) U:HMeas を持つとします。ジリィは、H = MeasH = Polishボーランド空間と連続写像の圏)を扱っています*5H = (距離空間と連続写像の圏) とかでもいいでしょう*6

Hの対象Xは可測空間とみなせるので、X上のすべての測度の集合Meas(X)を考えることができます。Meas(X)の部分集合を次のように定義します。

  • Meas<∞(X) = (有限測度の全体)
  • Meas1(X) = (確率測度の全体)
  • Meas≦1(X) = (劣確率測度の全体)

劣確率測度〈subprobability measure〉とは、全空間の測度が1以下になる測度のことです。

これらの測度の集合に対して、構造を入れたり制限をしたりすることにより、圏H上の自己関手 G:HH を作ります。さらに、モナド単位とモナド乗法を定義して、モナド G = (G, η, μ) に仕立てます。もとにした測度の集合により、次のように分類します。

HやGの作り方は多様なので、今述べた枠組みで作られるモナドを総称してジリィ・スタイルのモナド〈Giry-style monad〉と呼ぶことにします。ジリィ・スタイルのモナドのサブ分類として、上記の三種のモナド種別があり、そのインスタンスとして具体的な個々のモナドがあります。

Hが基礎となる圏〈base category | ground category〉だとして、GがH上のジリィ・スタイルのモナドのとき、クライスリ圏Kl(H, G)が(H上の)拡散圏です。Gが確率ジリィモナドのときは、Kl(H, G)を確率圏〈{stochastic | probabilistic} category〉と呼ぶことがあります。

ジリィモナドの相対化

前節で述べた枠組みで、基礎となる圏Hとその上のジリィ・スタイルのモナドGの選び方・作り方を変えれば、色々な拡散圏・確率圏を定義できます。目的に応じてカスタムメイドの圏を構成できるでしょう。

しかし、重要な事例でも前述の枠内に収まらないものがあります。FinSetを有限集合と写像の圏として、H = FinSet とします。このとき、H上のジリィ・スタイルのモナドをうまく作れません。有限集合のあいだの拡散写像はとても重要なので、これは困ります。

こんなときは相対モナド〈relative monad〉の出番です。相対モナドでは、台関手が自己関手でなくてもモナド類似構造を作れます。有限集合FinSetの場合ならば、例えば距離空間の圏Metに対して、埋め込み J:FinSetMet を前提して、台関手Gを G:FinSetMet の形に構成できます。

H = FinSet は離散有限な場合になるので、一般の(連続無限を含む)場合と比較するのは有用です。([追記]縦と横を逆にしました。[/追記]

離散有限な場合 一般の場合
有限集合 可測空間/位相空間
写像 可測写像/ボレル写像/連続写像など
ベクトル 測度(分布)
ベクトル 非負実数値関数
行列 積分核
スカラー積 積分
非負実数係数行列 拡散写像の積分核
マルコフ行列 確率拡散写像の積分核

通常のモナドでは、台関手に自己関手が必要で、そのためにある程度の規模の圏が必要です。相対モナドでは、J:HC のような関手を仮定した上で、台関手は G:HC の形でよく、FinSetのような小規模の圏を基礎の圏に取れます。モナドとして相対モナドまで許せば、ジリィ・スタイルのモナドとそのクライスリ圏(それが拡散圏)の応用範囲はさらに広がるでしょう。

資料

先に挙げた2つの原典は古い資料なので、もう少し新しいものを紹介します。

パナンガデン〈Prakash Panangaden〉の論文は、計算科学を意識して書かれているので、読みやすいと思います。次の2つの論文は、用語法を変えているだけで内容はほとんど同じです。

拡散写像には、反転〈converse | 転置〉と双対性という重要な話題があります。それについては、次の2つの論文に書いてあります。それぞれ、計算科学と統計への応用が意図されています。

エフェクト論理の観点からジリィモナドや積分について語っているものとして:

確率拡散写像を各著者がどう呼んでいるかというと:

  • ローヴェアは probabilistic mapping
  • ジリィは transition probability
  • スターツは conditional probability
  • パナンガデンは probabilistic relation と Markov kernel
  • ドバーカット〈Doberkat〉は stochastic relation
  • ドールクゥイスト〈Dahlqvist〉達は kernel
  • ヤコブス〈Jacobs〉は特に呼び名を付けてないようです。

ところで、拡散というと、空気中に広がる煙とか、水に溶けるインクとかを思い出すのですが、実写とCGを組み合わせた次の動画がすごい。

D

*1:今まで、「ローヴェル」と表記してきたのですが、「ローヴェア」のほうがもとの音に近いようなので、「ローヴェア」にします → https://ja.forvo.com/word/william_lawvere/Wikipeia項目も「ローヴェア」ですし。

*2:名前から判断するに、フランス人の女性でしょう、たぶん。

*3:存在は知っていても読めなかった論文なのでありがたいのですが、当該サイトが公開の権利を持っているかどうかはあやしいです。

*4Hはジリィが使っていた記法です。

*5:ジリィの記号ではMesPol

*6:確率測度の空間上への距離の導入が必要になりますが、ハッチンソン距離〈Hutchinson {metric |distance}〉やワッサースタイン距離〈Wasserstein {metric |distance}〉が使えるでしょう。

2018-05-31 (木)

ラムダ記法とイプシロン記法を組み合わせて関数を定義する

| 12:32 | ラムダ記法とイプシロン記法を組み合わせて関数を定義するを含むブックマーク

イプシロン記号/イプシロン記法/イプシロン計算については何度か述べたことがあります。今回は、イプシロンを実用的に使うための補助構文について述べます。ここで述べるアイディアは、証明検証系Mizarから拝借しています。ただし、Mizarそのものには触れませんし、Mizarの知識も不要です。

内容:

  1. 関数の書き方
  2. イプシロン記法
  3. イプシロン項の基本性質
  4. イプシロン項の不定性
  5. イプシロン項による関数定義
  6. 関数の余域を制限する

関数の書き方

中学校で習う1次関数は、

  • y = 2x + 1

のような形で書かれます。このため、「関数とは、等式の書き方の一種だ」と思っている人もいます。 「y = 」の部分は、関数の定義としてはどうでもいい部分です。関数としてエッセンシャルな部分だけを書くにはラムダ記法が便利です。

  • λx.(2x + 1)

しかし、ラムダ記法にも制限があります。既にある定数、関数、演算子などを組み合わせて新しい関数を構成するにはラムダ記法で十分ですが、命題で条件付けて関数を定義するときはラムダ記法ではうまく表現できません。

例えば、非負平方根を求める関数sqrt(square root から)をラムダ記法で定義するにはどうしたらいいでしょうか。

  • sqrt := λx.(……)

(……) の部分をどう書きますか? -- うまく書けないでしょ。

非負平方根は、(通常は)値を求める式やアルゴリズムで定義されるのではなくて、次のような条件で定義されます。

  • xの非負平方根とは、y2 = x かつ y ≧0 であるようなyである。

このような定義を表現するにはイプシロン記法が必要です。

イプシロン記法

イプシロン記法〈epsilon notation〉とは、イプシロン記号'ε'を使った表現方法で、例えば“xの非負平方根”を表すなら、次のように書きます。

  • εy.(y2 = x ∧ y ≧ 0)

イプシロン記法で書かれた式は、英語の冠詞'a'と関係代名詞'such that'に読み替えると、だいたいの意味は解釈できます。

  • a y such that y2 = x and y ≧ 0

冠詞も関係代名詞も自然な日本語に訳すのが難しいのですが、自然でなくてもよいなら:

  • y2 = x かつ y ≧ 0 であるところの どれかひとつのy

'ε'を含んだ式〈expression | 表現〉をイプシロン〈epsilon term〉と呼び、イプシロン項を含む計算体系をイプシロン計算〈epsilon calculus〉といいます。イプシロン計算は、ヒルベルト〈David Hilbert〉によって始められたので、イプシロン計算で使う'ε'はヒルベルトのイプシロン記号〈Hilbert's epsilon〉とも呼ばれます。

以上の説明でだいたい大丈夫だとは思いますが、イプシロン記法/イプシロン計算についてもう少し詳しいことは、次の記事で説明しています。

イプシロン計算の利用例は次の記事にあります。

イプシロン項の基本性質

イプシロン項は、Pを(述語論理の)論理式として、εx.P の形です。ヒルベルトのイプシロン計算では、論理式Pに何の制限もありません。Pが変数xを含んでいなくてもかまいません。x以外の変数がPに出現しても、もちろんOKです。いくつか例を挙げると:

  • εx.(x = y)
  • εx.(x = x)
  • εx.(a ≦ y ∧ y ≦ b)
  • εa.(a ≦ y ∧ y ≦ b)
  • εy.(a ≦ y ∧ y ≦ b)

論理式Pに対して、Pに出現する変数xを項Eで置き換えたものを P[x := E] と書きます。角括弧は論理式の一部ではなくて、構文的オペレーターを表すメタ記号です。例を挙げましょう。以下で、記号'≡'は、構文的に等しい(同じ論理式である)ことを示す“メタな等号”です。

  • (x = y)[y := 1] ≡ (x = 1)
  • (x = y)[x := 2x + 1] ≡ (2x + 1 = y)
  • (x = y)[x := y] ≡ (y = y)
  • (a ≦ y ∧ y ≦ b)[a := x2] ≡ (x2 ≦ y ∧ y ≦ b)
  • (a ≦ y ∧ y ≦ b)[a := 1] ≡ (1 ≦ y ∧ y ≦ b)

イプシロン計算における基本的な公理は次のものです。

これは、単一の命題ではなくて、変数xと命題Pの組み合わせごとに作られる無限個の命題を表すパターンです。変数yと命題 (a ≦ y ∧ y ≦ b) の組み合わせだと:

  • ∃y.(a ≦ y ∧ y ≦ b) ⇒ (a ≦ εy.(a ≦ y ∧ y ≦ b) ∧ εy.(a ≦ y ∧ y ≦ b) ≦ b)

イプシロン記号は、ラム計算のラムダ記号や述語論理の限量子と同様に束縛子なので、εで束縛された変数のリネーム(アルファ変換)は自由にできます。以下の論理式では、すぐ上と比べて、y→z, y→w というリネームをしてます。意味は変わりません。

  • ∃y.(a ≦ y ∧ y ≦ b) ⇒ (a ≦ εz.(a ≦ z ∧ z ≦ b) ∧ εw.(a ≦ w ∧ w ≦ b) ≦ b)

イプシロン項の不定性

イプシロン項 εx.P の直感的な意味は:

  1. aが定数(あるいは値そのもの)で、P[x := a] が成立するなら、そのようなaを表す。
  2. P[x := a] が成立するaが存在しないとき、0を表す。

二番目は、「なんで0なんだ?」と突っ込まれそうです。実は何でもいいのです。何でもいいのなら、特に0に固定してもいいだろう、ということです。

一番目の状況では、P[x := a] が成立し、a = εx.P ですから、次の2つの命題が成立しています。

  • ∃x.P
  • P[x := εx.P]

イプシロン項の基本性質 ∃x.P ⇒ P[x := εx.P] は P[x := εx.P] と同値です(含意命題の前件が真だから後件だけと同じ)。もちろん、基本性質は成立します。

ニ番目の状況では、∃x.P は成立せず、0 = εx.P です。P[x := 0] も成立しません。しかし、∃x.P ⇒ P[x := 0] は真です。含意命題の前件が偽なので、後件が何であっても真なのです。結果として、基本性質が成立します。

以上の解釈から、イプシロン項の基本性質 ∃x.P ⇒ P[x := εx.P] は常に成立する感じがします。

さて、では次の命題は成立するでしょうか?

  • ∃x.(x = x) ⇒ εx.(x = x) = εx.(x = x)

これは、 変数xと命題 (x = x) に対するイプシロン項の基本性質です。残念ながら、これが真だとは断言できません。なぜなら、イプシロン項 εx.P は唯一の値を表すわけではなくて、「Pを満たすどれか」という不定性(非決定性)を持つからです。等式の左辺のイプシロン項の値と右辺のイプシロン項の値が同じである保証がないのです。

となると、等式の基本性質 E = E (反射律)が破綻してしまいます。これはとても困ります。対策として、イプシロン項の出現ごとに毎回値が偶発的に選ばれるのではなくて、一度だけ任意選択が発生し、一度決めた値はずっと使い続ける、と決めます。候補が複数あれば、どの値であるかはやはり分からないのですが、出現ごとに違う値という事態はなくなります。

別な考え方として、イプシロン項は不定(非決定的)だとしたまま、論理のほうを変える方法があります。εx.(x = x) = εx.(x = x) の真偽は決まらないので、第三の真偽値を割り当てます。使う論理は三値以上の真偽値を持つ論理になります。話はややこしくなります。

今説明したような事情があるので、イプシロン記法を、何の条件も付けずに使うのはちょっと厄介です。そこで、過去の記事では条件付きでイプシロン記法を使っています。

イプシロン計算ってなんですかぁ? こんなもんですよぉ」:

話を煩雑にしないために、∃x.P(x) が保証されているか、∃x.P(x) を前提とする場合にだけ、εx.P(x) を使っていいと約束しましょう。

論理式内の名前の消去とイプシロン項」:

イプシロン項εx.P(x)の使用条件をさらにきびしくして、次のようにしましょう。

  • ∃!x.P(x)が真であるときに限り、εx.P(x)を使ってよい。

ここで出てきた∃!は、一意的な存在を意味します。

イプシロン項による関数定義

前節最後に引用した「∃!x.P が真であるときに限り、εx.P を使ってよい」という規則は、イプシロン記法を簡単安全に使う良い方法です。この規則に従えば、イプシロン項は定数や関数として扱えます。特別に気を使う必要はありません。

この方法は証明検証系Mizarで採用されています。Mizarでは、イプシロン項が自由に使えるわけではなくて、関数定義の内部でだけ使えます。次のような感じです。

function sqrt := λx.εy.(y2 = x ∧ y ≧ 0)

実際のMizarでは、ユーザーにそれがイプシロン項だと意識させないようなシンタックスシュガーがかかっていますが、ここではイプシロン記号をそのまま使い続けます。

さて、上のような定義では「∃!x.P が真であるときに限り、εx.P を使ってよい」という条件を守っているかどうか分かりません。Mizarの方法は、関数定義と同時に ∃!x.P の証明を書かせるものです。次のような感じです。

function sqrt := λx.εy.(y2 = x ∧ y ≧ 0)
justification
  existence 存在命題
    存在の証明
  uniqueness 一意性命題
    一意性の証明
end

存在や一意性の命題と証明を書けるようにするには、変数に型が必要です。ここでは、型は集合のことだとして、「変数∈集合」の形で型を明示します。部分集合の型も必要になるので、次の書き方を認めます。

  • λx∈(R | x≧ 0).εy∈R.(y2 = x ∧ y ≧ 0)

ここで、λx∈(R | x≧ 0) は、λx∈{t∈R | t ≧ 0} の略記です。

これで、関数に付随する存在命題と一意性命題を書き下すことができます。

function sqrt := λx∈(R | x≧ 0).εy∈R.(y2 = x ∧ y ≧ 0)
justification
  existence ∀x∈(R | x≧ 0).∃y∈R.(y2 = x ∧ y ≧ 0)
    存在の証明
  uniqueness ∀x∈(R | x≧ 0).∀v, w∈R.((v2 = x ∧ v ≧ 0) ∧ (w2 = x ∧ w ≧ 0) ⇒ v = w)
    一意性の証明
end

存在命題と一意性命題は、関数定義の本体部分から機械的に作り出せます。関数定義本体が次のようだとします。

  • function f := λx∈(X | A).εy∈Y.P

ここで、Aはxを絞り込む条件を表す命題です。すると、存在命題と一意性命題は次の形です。

  • ∀x∈(X | A).∃y∈Y.P
  • ∀x∈(X | A).∀v, w∈Y.(P[y := v]∧P[y := w] ⇒ v = w)

∀x∈(X | A) という略記を用いなければ:

  • ∀x∈X.(A ⇒ ∃y∈Y.P)
  • ∀x∈X.(A ⇒ ∀v, w∈Y.(P[y := v]∧P[y := w] ⇒ v = w))

関数の余域を制限する

非負平方根の関数sqrtを定義する本体の式は λx∈(R | x≧ 0).εy∈R.(y2 = x ∧ y ≧ 0) です。この式を見れば、関数定義を正当化〈justify〉するための存在命題と一意性命題は自動的に書けます。それだけでなく、関数の域〈domain | source domain〉と余域〈codomain | target domain〉も自動的に分かります。この例では:

  • sqrt:{x∈R | x≧0}→R

関数の域と余域の組み合わせは関数のプロファイルというので、「関数定義の本体は、関数のプロファイル情報を持っている」とも言えます。

さて、関数sqrtの値は負にならないので、余域を非負の実数にしてもよいでしょう。つまり、sqrtのプロファイルを次のようにしよう、ということです。

  • sqrt:{x∈R | x≧0}→{y∈R | y≧0}

この状況を表現するために、次の書き方を許しましょう。

  • λx∈(R | x≧ 0).εy∈(R | y≧0).(y2 = x ∧ y ≧ 0)

これで関数の余域に関する条件も書けます。しかし勝手に条件を追加していいわけではありません。例えば次はどうでしょうか。

  • λx∈(R | x≧ 0).εy∈(R | y≦0).(y2 = x ∧ y ≧ 0)

関数sqrtの余域を非正の実数に制限しています。こうすると、値の行き場所がなくなり、もはや関数とはいえません。

関数がちゃんと定義される〈well-defined〉ためには、「値が余域内に収まる」という条件も必要です。一般的に言えば、λx∈(X | A).εy∈(Y | B).P の形の定義があれば、次の条件です。

  • ∀x∈(X | A).(P ⇒ B)

sqrtの例では:

  • ∀x∈(R | x≧0).((y2 = x ∧ y ≧ 0) ⇒ y≧0)

うまくいかない例では:

  • ∀x∈(R | x≧0).((y2 = x ∧ y ≧ 0) ⇒ y≦0)

余域の条件も付けたsqrtの定義をあらためて書けば次のようです。

function sqrt := λx∈(R | x≧ 0).εy∈(R | y≧0).(y2 = x ∧ y ≧ 0)
justification
  existence ∀x∈(R | x≧ 0).∃y∈R.(y2 = x ∧ y ≧ 0)
    存在の証明
  uniqueness ∀x∈(R | x≧ 0).∀v, w∈R.((v2 = x ∧ v ≧ 0) ∧ (w2 = x ∧ w ≧ 0) ⇒ v = w)
    一意性の証明
  codomain ∀x∈(R | x≧0).((y2 = x ∧ y ≧ 0) ⇒ y≧0)
    余域条件の証明
end

一般的な関数定義の形は次のようになります。

function f := λx∈(X | A).εy∈(Y | B).P
justification
  existence ∀x∈(X | A).∃y∈Y.P
    存在の証明
  uniqueness ∀x∈(X | A).∀v, w∈Y.(P[y := v]∧P[y := w] ⇒ v = w)
    一意性の証明
  codomain ∀x∈(X | A).(P ⇒ B)
    余域条件の証明
end

余域条件を存在命題のなかに組み入れてしまってもかまいません(そのほうがスッキリします)。

function f := λx∈(X | A).εy∈(Y | B).P
justification
  existence ∀x∈(X | A).∃y∈(Y | B).P
    存在の証明
  uniqueness ∀x∈(X | A).∀v, w∈Y.(P[y := v]∧P[y := w] ⇒ v = w)
    一意性の証明
end

ここで、∃y∈(Y | B).P は ∃y∈Y.(B ∧ P) の略記です。


このような形で関数定義を書いてみるメリットは、関数が関数として成立するにはどんな条件が必要かがハッキリすることです。それらの条件をキチンと保証しない限りは、関数を定義したとは言えないのです。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20180531

2018-05-25 (金)

その時の事実だけが問題なのではない: 日大アメフト部問題

| 17:09 | その時の事実だけが問題なのではない: 日大アメフト部問題を含むブックマーク

このブログで、世間で話題のニュースに反応することは、ほとんどありません。稀に反応するときって、もうお決まりで、僕がどういう偏向を持っているか明らかですね -- 根性論、精神論がホントに嫌いなんです。

次の2つの過去記事から、他の“アンチ根性論”記事へのリンクがあります。

今回の日大アメフト部問題も、あまりの嫌悪感から(比喩じゃなくて)気分が悪くなってます。

宮川選手と内田前監督/井上コーチの言い分が違うことから、「どっちが嘘ついてる?」「事実を明らかにしろ」という疑問・指摘もありますが、それはさして重要じゃないと思います。

「相手チームのクォーターバックを潰せ」発言に対して、井上コーチは「『潰せ』程度はよく使う言葉だし、気合を入れるつもりだった」と述べていますが、僕はこれはホントかも知れないと思っています。もっと正確に言うと、「ホントだと仮定して議論してもよい」と思っています。

監督・コーチには、「相手チームの選手を負傷させる」意図なんて全くなかった、と仮定しましょう。しかし、選手は「負傷させろ」という指示と受け取り、自分が不本意でもそれに従わなくてはならない、と思い込んでしまったわけです。

誤解した選手が悪い? -- バカなっ! 内田前監督/井上コーチの発言に嘘はなかったとしても、前監督/コーチが悪い、非常に悪い。宮川選手が「潰せ」を「負傷させる」と誤解したのなら、その誤解を引き起こす環境があったわけです。「待てよっ、俺、勘違いしてたわ」と思い直せず、実行してしまったのも、そう行動せざるを得ない環境があったからです。

環境とは、恐怖支配体制とか暴力を肯定する雰囲気とかです。個別の発言や行動を環境から切り離して「指示した/指示してない」を判断するのは(無意味ではないにしろ)重要じゃないでしょう。犯罪的行動を引き起こすような環境を作った点において、前監督/コーチその他関係者には既に責任があります。

「恐怖支配・暴力肯定的な環境があった」と今は断定できませんが、もしあったのなら、宮川選手個人の問題ではなくて、その環境下に置かれた全ての選手の問題です。また、環境は、監督・コーチをすげ替えても残ってしまう可能性があります。根性主義や暴力を支持する人間は一定数いて、有効なメソッド/成功体験として次世代に受け継がれるケースがあるからです。

事件を引き起こした背景・環境を調査して、恐怖と暴力の体質は根絶やしにして欲しいですね。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20180525

2018-05-23 (水)

とある心理学実験への参照

| 16:25 | とある心理学実験への参照を含むブックマーク

日本大学のアメリカンフットボール部の選手の記者会見を見ました。彼が全く悪くないと主張するつもりはないけど、「監督とコーチに言われた」らやるしかない、となるのは当然な気がする。

おそらく多くの人が指摘してんだろう、と思うけど、次の有名な心理学実験を参照する価値はあるでしょう。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20180523

2018-05-17 (木)

ド・ラーム・コホモロジーとホッジ分解のオモチャ (2/2)

| 12:57 | ド・ラーム・コホモロジーとホッジ分解のオモチャ (2/2)を含むブックマーク

ド・ラーム・コホモロジーとホッジ分解のオモチャ (1/2)」の続き・後編です。今回の第2節から第6節(全8節)で、オモチャ=有限離散モデルを作ります。この部分は、純粋に線形代数の話です。ここだけを取り出して(文脈を無視して)、線形代数の練習問題として読むこともできます。第7節で、前回の話との関係を述べます。「背景を知らずに代数的議論だけを追うのはイヤだ」という方は、第7節を先に読んでください。

内容:

  1. この記事の記述方法について
  2. 内積ベクトル空間と随伴線形写像
  3. 部分空間の直交性と直交補空間
  4. ホッジの分解定理(ラプラシアンなしバージョン)
  5. ラプラシアンとホッジ分解
  6. ド・ラーム・コホモロジー空間
  7. 多様体から線形代数へ
  8. おわりに

前回・前編の内容

  1. 予備知識は線形代数だけ
  2. 背景のオハナシ(超・急ぎ足)
  3. 複体
  4. 複体上のパスとチェーン
  5. 実数係数チェーン空間
  6. 境界作用素 1
  7. 境界作用素 2
  8. 組み合わせ複体と代数的複体
  9. 代数的複体もっと
  10. ラプラシアンとラプラス方程式

この記事の記述方法について

この節には、僕からの注意とお願いが含まれます。

記事内で述べられている命題のあいだの関係をハッキリさせるために、命題にラベルを付けることにします。例えば:

  • [記述サンプル] (a + b) + c = a + (b + c) ---(足し算の結合法則)

この例では、「足し算の結合法則」というラベルが導入されています。ラベル付けされた命題を参照するときは、「$(ラベル)」と書くことにします。

  • [記述サンプル] $(足し算の結合法則)によりウンヌンカンヌン

参照からもとの命題にハイパーリンクを張ったりすると便利でしょうが、そこまではやってません。文字列検索で、もとの命題は探せるでしょう。

命題をラベルにより参照したとき、その命題を繰り返し記述(引用)するときは、次に形にします。

  • [記述サンプル] $(足し算の結合法則: (a + b) + c = a + (b + c) )によりウンヌンカンヌン

一時的なラベルには番号(「---(1)」や「$(1)」)を使います。

記事本文内で言及してないが、予備知識だと想定されている命題への参照は、「$?(ラベル)」とします。

  • [記述サンプル] $?(ピタゴラスの定理)によりウンヌンカンヌン

この場合、「ピタゴラスの定理」というラベルが記事本文内にあるわけではありません。必要があれば、ラベルの文言をヒントに何かで調べてください。

こういうルールで書き進めてみると、問題が発生しました。命題のラベルにそれらしい語句を割り当てようとすると、本文内で説明してない言葉が入り込んでしまうのです。例えば、「ヌルベクトル」について一切説明してないにも関わらず、ラベルは「非自明ヌルベクトルの非存在」となったりします(実際、このラベルを使っています)。それで、ラベル内の文言を脚注で説明しだしたのですが、いちいちこれをやっていると、脚注が増えて大変。

ラベルを、通し番号やランダム文字列にすればこの問題は発生しませんが、それも味気ないし、ラベルを記憶できません。それでお願いです。ラベルの意味が分からなくても詮索しないでください。識別用の文字列に過ぎない、と割り切ってください。よろしくお願いします。

ラベルが付いている命題を、この記事内ですべて証明しているわけではありません。が、要点となる目ぼしい命題には証明を付けています。僕は、説明(地の文)に証明を埋め込むスタイルが好きなんですが、それが苦しいときは別枠で証明を書きます(けっこう別枠が多い)。

あ、それと; 僕の横着から、F;Gのような図式順記法と、G¥circFのような反図式順記法が混じっています。それを不快と感じたり困惑してしまう方は、「双対や随伴に強くなるためのトレーニング」を読んでトレーニングしてくださいな。

内積ベクトル空間と随伴線形写像

Vは実数係数ベクトル空間で、内積〈inner product〉が備わっているとします。u, v∈V に対して、uとvの内積を(u|v)と書きます。内積は双線形(uに関してもvに関しても線形)な実数値関数で、次を満たすものです。

  1. (u|v) = (v|u) ---(内積の対称性)
  2. (v|v) ≧ 0 ---(内積の正定値性)
  3. (v|v) = 0 ならば v = 0 ---(非自明ヌルベクトル*1の非存在)

次の事実は、定義からすぐに出ますが、重要です。

  • (任意の u∈V に対して (u|v) = 0) ⇔ v = 0 ---(内積の非退化性*2)

ここから先、ベクトル空間は有限次元のものだけ考えます。ベクトル空間Vが内積を持つとき、正規直交枠 {a1, ..., an} (ai∈V)が取れます。枠〈frame〉とは、基底の要素に番号(全順序)を付けたものです*3。{a1, ..., an} の双対枠を {f1, ..., fn} としましょう。双対枠は、Vの双対空間 V* = (V上の線形形式の空間) の枠となります。双対枠の要素fjは、次のように定義されます。

  • i = 1, ..., n に対して、fj(ai) := δji ---(双対枠の定義)

ここでδjiはクロネッカーのデルタで、

  • δji := (if i = j then 1 else 0)

aiをfiに対応させる写像を線形に拡張して Φ:V→V* が定義できます。このΦは、実は正規直交枠の取り方に寄りません。正規直交枠を使わずいきなりΦを定義するなら、

  • Φ(u)(v) := (u|v) ---(カリー化内積の定義*4)

あるいはラムダ記法を用いて、

  • Φ(u) := λv.(u|v)

と定義します。Vが有限次元でないと、このΦが全射であることは自明ではありません(リースの表現定理など)。今は有限次元での話なので、Φが(ベクトル空間の)同型写像なのは容易にわかります。

V, Wが2つの内積ベクトル空間〈inner product vector space〉(内積が備わったベクトル空間)だとして、F:V→W を線形写像だとします。Fの随伴線形写像〈adjoint linear map〉Fを次のように定義します。

  • F := Φ;F*-1 :W→V ---(随伴線形写像の定義)

ここで:

  • ';'は、“写像の結合”の図式順〈diagrammatic-order〉記号です。反図式順〈anti-diagrammatic-order〉記号'¥circ'を使うなら、F := Φ-1¥circF*¥circΦ 。
  • 図式順記法で左のΦはWに対する Φ = ΦW :W→W* で、右のΦ-1はVに対する Φ-1 = (ΦV)-1 :V*→V です。つまり正確に書けば、F := ΦW;F*;(ΦV)-1
  • F*はFの双対線形写像〈dual linear map〉で、(F*(g))(v) := g(F(v)) として定義されます。

Fは次の性質を持ちます。

  • 任意の v∈V, w∈W に対して、(F(v)|w) = (v|F(w)) ---(随伴線形写像の基本性質)

この性質を持つような(唯一の)線形写像としてFを特徴付けることもできます。記法の工夫(すぐ下の箇条書き)の例示も兼ねて、実際に計算しておきましょう。

  1. f∈V*, v∈V に対して、f(v)を<f|v>とも書く。
  2. F;G = G¥circF を単に FG と書いてよい。
  3. F(v) を単に Fv と書いてよい。
  4. 結合(写像の合成、記号は'¥circ', ';', 併置)よりも、単項演算子のスター(-)*、ダガー(-)のほうが優先される。
  5. V** = (V*)* をVと同一視して、Φ:V→V* の双対を Φ*:V→V* とみなす。この設定で、F** = (F*)* = F, Φ* = Φ, (Φ-1)* = Φ-1

ターゲット命題: (F(v)|w) = (v|F(w)) ---(随伴線形写像の基本性質)

内積(-|-)を、Φと<-|->で表すなら、
$(随伴線形写像の基本性質: (F(v)|w) = (v|F(w)) )は
  <ΦFv|w> = <Φv|Fw> ---(1)
と同値なので、$(1)を示せばよい。

$(1: <ΦFv|w> = <Φv|Fw> )を示す。

先に、(F)* を計算しておく。
    (F)*
// $(随伴線形写像の定義)により
  = (ΦV-1F*ΦW)*
// $?(双対を取るスター・オペレーターの性質)により
  = ΦW*F**V-1)*
// F** = F, Φ* = Φ, (Φ-1)* = Φ-1 を使って
  = ΦWV-1
よって、
  (F)* = ΦWV-1
簡略に書けば
  F* = ΦFΦ-1 ---(2)

次に、目的の等式$(1)を示す。
    <Φv|Fw>
// $?(双対線形写像の性質)から
  = <(F)*Φv|w>
// 先に計算した $(2: F* = ΦFΦ-1 )を使って
  = <(ΦFΦ-1)Φv|w>
// Φ-1Φ を消して
  = <ΦFv|w>
よって、
  <ΦFv|w> = <Φv|Fw>

$(1)が示せた。

正規直交枠を使って行列表示すると、F*もFも、Fを表す行列の転置行列で表示できます。このため、F*とFは混同/同一視されがちですが、ここでは区別してください。F*とFでは、写像としてのプロファイル(域と余域)が違います。

  • F*:W*→V*
  • F:W→V

線形写像にその随伴線形写像を対応させるダガー・オペレーター(-)は、次のような法則を満たします。

  1. (F) = F ---(ダガーの対合性)
  2. (F;G) = G;F または (G¥circF) = F¥circG ---(ダガーの反変性)
  3. (idV) = idV ---(恒等のダガー)
  4. (0V,W) = 0W,V (0V,Wは、V→W のゼロ写像) ---(ゼロ射のダガー)

部分空間の直交性と直交補空間

Vを有限次元内積ベクトル空間だとして、S, TなどはVの部分ベクトル空間〈部分空間〉だとします。次の定義の右辺が成立するとき、SとTは直交している〈orthogonal〉といい、S⊥T と書きます。

  • S⊥T :⇔ 任意の u∈S, v∈T に対して、(u|v) = 0 ---(空間の直交の定義)

部分空間Sに対して、Sの直交補空間〈orthogonal complement〉S は次のように定義します。

  • S := {v∈V | 任意の s∈S に対して、(s|v) = 0} ---(直交補空間の定義)

定義からすぐに次が言えます。

  1. SはVの部分空間である。 ---(直交補空間の部分空間性)
  2. S⊥S ---(部分空間と直交補空間は直交)
  3. S⊥T ⇒ S∩T = {0} ---(直交する空間の共通部分)
  4. S⊥T ⇔ S⊆T ⇔ T⊆S ---(直交の言い換え)

Vの部分空間S, Tに対して、S∧TとS∨Tを次のように定義します。

  • S∧T := S∩T (集合の共通部分) ---(ミート空間の定義)
  • S∨T := {v∈V | s∈S と t∈T により、v = s + t と書ける} ---(ジョイン空間の定義)

S∧TとS∨Tの定義に内積は関係ありませんが、内積があると、次の法則が言えます。

  • (S∨T) = S∧T ---(直交補空間 ド・モルガンの法則 1)
  • (S∧T) = S∨T ---(直交補空間 ド・モルガンの法則 2)

これは、論理におけるド・モルガンの法則と同じ形です。“ド・モルガンの法則”の1番目の半分 (S∨T) ⊆ S∧T だけ示すと:

ターゲット命題: (S∨T) ⊆ S∧T

  v∈(S∨T) と仮定する。
$(ジョイン空間の定義)と$(直交補空間の定義)から
  任意の s∈S, t∈T に対して、(v|s + t) = 0
$?(内積の双線形性)から
  任意の s∈S, t∈T に対して、(v|s) + (v|t) = 0 ---(1)
t = 0 でも$(1)は成立するから
  任意の s∈S に対して、(v|s) = 0 ---(2)
s = 0 でも$(1)は成立するから
  任意の t∈T に対して、(v|t) = 0 ---(3)
$(2)を言い換えると
  v∈S ---(4)
$(3)を言い換えると
  v∈T ---(5)
$(4), $(5)から
  v∈(S∧T)
以上より
  v∈(S∨T) ⇒ v∈(S∧T)
vは任意だったから
  ∀v.(v∈(S∨T) ⇒ v∈(S∧T))
つまり
  (S∨T) ⊆ S∧T

対偶の法則に相当する次も成立します。

  • S⊆T ⇔ T⊆S ---(直交補空間 対偶の法則)

内積ベクトル空間Vの部分空間の集まりSubspace(V)は、命題論理やベキ集合のブール代数と酷似した構造を持ちます。どこまで似ていて、どこが違うかを調べるのは面白い課題です。

S⊥T のとき、S∨T を S¥oplusT とも書きます。S¥oplusT を、SとTの直交直和〈orthogonal direct sum〉といいます。S¥oplusT と書いたときは、S⊥Tを前提にしているので、S∧T = O (Oはゼロ空間{0})です。直交直和の命題論理における類似物は、排他的命題の連言です。

通常の直和 S¥oplusT は外部直和であり、S¥oplusT ⊆ V とはいえません。それに対して直交直和 S¥oplusTはS∨Tのこと(ただし、S⊥T)なので S¥oplusT ⊆ V です。とはいえ、外部直和 S¥oplusT に、S⊥Tとなるような内積を入れることが出来て、そうやって作った内積ベクトル空間も S¥oplusT と書くので、S¥oplusT ⊆ V かどうかは定義によりけりですね。

論理の排中律 P∨¬P = True (PまたはPでない は いつだって真)に相当する法則は次のように書けます。

  • S¥oplusS = V ---(直交補空間 排中律)

直交直和記号¥oplusに、S⊥Sの意味を込めているわけですが、¥oplusを使わずに2つの命題に分けたほうが分かりやすいかも知れません。

  1. S∧S = O = {0} ---(部分空間と直交補空間の排他性)
  2. S∨S = V ---(直交補空間 排中律 ジョイン版)

直交補空間の排中律から、一意直交分解が可能となります。

  • 任意の v∈V は、s∈S と t∈S により、v = s + t と一意的に分解できる。 ---(直交分解の原理)

ホッジの分解定理(ラプラシアンなしバージョン)

U, V, Wが有限次元の内積ベクトル空間だとして、F:U→V, G:V→W を線形写像とします。FとGは次の条件を満たすとします。

  • F;G = 0 :U→W ---(複体条件)

等式右辺の0はゼロ写像のことです。F;G = 0 と Im(F) ⊆ Ker(G) は同じことです。

F, Gと共にF, Gも考えます。これからの登場人物である空間・写像は次のようです(3つの空間と4つの写像)。

F;G = 0 を満たす (U, V, W, F, F, G, G) は、共変/反変を一緒にした代数的複体(前回の第2節第9節を参照)の一部を切り取ったものです。なので、このような構造をミニ複体〈mini-complex〉と呼ぶことにします*5。ここから先、特別に断らなければ、このミニ複体 (U, V, W, F, F, G, G) に関する命題を扱います。

[追記]前回・今回で話題にしている「オモチャ」とは何なのか? と聞かれれば、それはズバリ、ミニ複体です。ミニ複体は、有限次元内積空間の圏のなかで定義できる比較的簡単な構造です。ミニ複体に対して、ド・ラーム・コホモロジー(単一のベクトル空間)とラプラシアンが定義できます。そしてホッジ分解が成立します。背景はともかくとして、ミニ複体の議論には有限次元線形代数の概念しか使わないので、いじりやすいという意味で「オモチャ」と呼んでいいと思います。[/追記]

まず、次の補題を確認します。これは、F;G = 0 を使ってないので、随伴線形写像に関する一般的な事実です。

  • Im(G) = Ker(G) ---(Im-Ker随伴性 1)
  • Im(F) = Ker(F) ---(Im-Ker随伴性 2)

この2つは実質的に同じ命題なので、1番目だけ示します。

ターゲット命題: Im(G) = Ker(G) ---(Im-Ker随伴性 1)

Im(G) ⊆ Ker(G) と
Ker(G) ⊆ Im(G) を示せばよい。

Im(G) ⊆ Ker(G) を示す。

  v∈Im(G) と仮定する。
$?(Imの定義)より
  適当な w∈W を使って v = G(w)と書ける。

  u∈Ker(G)と仮定する。
u と v = G(w) の内積を計算する。
     (u|v)
  =  (u|G(w))
// $(随伴線形写像の基本性質)から
  = (G(u)|w)
// 仮定 u∈Ker(G) より G(u) = 0 だから
  = (0|w)
// $?(内積の双線形性)より
  = 0
よって、
  (u|v) = 0
u∈Ker(G)と v∈Im(G) は任意だったから
  ∀u∈Ker(G), v∈Im(G).(u|v) = 0
つまり、
  Im(G)⊥Ker(G)
$(直交の言い換え)から
  Im(G) ⊆ Ker(G)
が示せた。

Ker(G) ⊆ Im(G) を示す。

$(直交補空間 対偶の法則)から、Im(G) ⊆ Ker(G) を示せばよい。

Im(G) ⊆ Ker(G) を示す。

  u∈Im(G) と仮定する。
  v∈Im(G) と仮定する。
$?(Imの定義)より
  適当な w∈W を使って v = G(w)と書ける。
u と v = G(w) の内積は0だから
  (u|G(w)) = 0
$(随伴線形写像の基本性質)から
  (Gu|w) = 0
vは任意だったからwも任意となり、$(内積の非退化性)により
  Gu = 0
つまり
  u∈Ker(G)
以上により
  u∈Im(G) ⇒ u∈Ker(G)
uは任意だったから
  ∀u.(u∈Im(G) ⇒ u∈Ker(G))
つまり
  Im(G) ⊆ Ker(G)
が示せた。

Fの像Im(F)とGの像Im(G)は、いずれもVの部分空間です。この2つの部分空間は直交します。

  • Im(F) ⊥ Im(G) --(コバンダリと随伴コバンダリの直交性)

ターゲット命題: Im(F) ⊥ Im(G)

  v∈Im(F), v'∈Im(G) と仮定する。
$?(Imの定義)より
  適当な u∈U を使って v = F(u)と書ける。
  適当な w∈W を使って v' = G(w)と書ける。
v = F(u) と v' = G(w) の内積を計算する。
    (v|v')
  = (F(u)|G(w))
// $(随伴線形写像の基本性質)から
  = (G(F(u))|w)
// $(複体条件)から G(F(u)) = 0 だから
  = (0|w)
// $?(内積の双線形性)から
  = 0
よって
  (v|v') = 0
v, v'は任意だったから
  ∀v∈Im(F), v'∈Im(G).(v|v') = 0
$(空間の直交の定義)より
  Im(F) ⊥ Im(G) 。

さて、いよいよ今回のハイライト、ホッジの分解定理〈the Hodge decomposition theorem〉です。定理の主張は、ミニ複体において「Vに直交直和分解が作れるよ」と言っているだけですが、その意味は前回第7節を参照してください。

  • X = Ker(F)∧Ker(G) とすると、V = Im(F)¥oplusIm(G)¥oplusX ---(ホッジ分解)

ターゲット命題: V = Im(F)¥oplusIm(G)¥oplusX 

(Im(F)∨Im(G))を計算する。
    (Im(F)∨Im(G))
// $(直交補空間 ド・モルガンの法則 1)により
  = Im(F)∧Im(G)
// $(Im-Ker随伴性 2: Im(F) = Ker(F) )と$(Im-Ker随伴性 1: Im(G) = Ker(G) )により
  = Ker(F)∧Ker(G)
よって、
(Im(F)∨Im(G)) = Ker(F)∧Ker(G) ---(1)

$(直交補空間 排中律)から
  V = (Im(F)∨Im(G))¥oplus(Im(F)∨Im(G))
$(1)から
  V = (Im(F)∨Im(G))¥oplus(Ker(F)∧Ker(G))
X = Ker(F)∧Ker(G) としていたので
  V = (Im(F)∨Im(G))¥oplusX
$(コバンダリと随伴コバンダリの直交性)から Im(F)∨Im(G) = Im(F)¥oplusIm(G) なので
  V = (Im(F)¥oplusIm(G))¥oplusX

ラプラシアンとホッジ分解

前節と同じ状況設定 -- つまり、ミニ複体 (U, V, W, F, F, G, G) があるとして、線形写像 L:V→V を次のように定義します。

  • L := G;G + F;F = G¥circG + F¥circF = GG + FF ---(ラプラシアンの定義)

この線形写像Lは、(ミニ複体の)ラプラシアン〈Laplacian〉と呼びます。この言葉の由来は前回第7節で触れています。

ラプラシアンLに対して次が成立します。

  • Ker(L) = Ker(F)∧Ker(G) ---(調和コチェーンの特徴付け)

これからこの命題$(調和コチェーンの特徴付け)を示します。まずは補題からです。

  • Ker(G;G) = Ker(G) ---(随伴ラウンドトリップの核 1)
  • Ker(F;F) = Ker(F) ---(随伴ラウンドトリップの核 2)

この2つは実質的に同じ命題なので、1番目だけ示します。

ターゲット命題: Ker(G;G) = Ker(G) ---(随伴ラウンドトリップの核 1) 

Ker(G;G) ⊆ Ker(G) と
Ker(G) ⊆ Ker(G;G) を示せばよい。

Ker(G;G) ⊆ Ker(G) を示す。

  v∈Ker(G;G) と仮定する。
つまり
  (G;G)v = (G¥circG)v = G(G(v)) = 0
v∈V と G(G(v)) との内積を取ると
  (v|G(G(v))) = (v|0) = 0
$(随伴線形写像の基本性質)より (v|G(G(v))) = (G(v)|G(v)) だから
  (G(v)|G(v)) =  0
$(非自明ヌルベクトルの非存在)より
  G(v) = 0
つまり
  v∈Ker(G)
以上より
  v∈Ker(G;G) ⇒ v∈Ker(G)
vは任意だったから
  ∀v.(v∈Ker(G;G) ⇒ v∈Ker(G))
つまり
  Ker(G;G) ⊆ Ker(G)
が示せた。

Ker(G) ⊆ Ker(G;G) を示す。

  v∈Ker(G) と仮定する。
(G;G)v を計算する。
    (G;G)v
  = (G¥circG)v
  = G(G(v))
// 仮定より G(v) = 0 なので
  = G(0)
  = 0
よって
  (G;G)v = 0
つまり
  v∈Ker(G;G)
以上より、
  v∈Ker(G) ⇒ v∈Ker(G;G)
vは任意だったから
  ∀v.(v∈Ker(G) ⇒ v∈Ker(G;G))
つまり、
  Ker(G) ⊆ Ker(G;G)
が示せた。

さて、$(調和コチェーンの特徴付け: Ker(L) = Ker(F)∧Ker(G) )を示しましょう。$(複体条件: F;G = 0 (G¥circF = 0))があるので、Ker(F)∧Ker(G) ⊆ Ker(L) は簡単です。逆向きの包含 Ker(L) ⊆ Ker(F)∧Ker(G) だけを示します。

ターゲット命題: Ker(L) ⊆ Ker(F)∧Ker(G) 

Ker(L) ⊆ Ker(G) と
Ker(L) ⊆ Ker(F) を示せばよい。

Ker(L) ⊆ Ker(G) を示す。

  v∈Ker(L) と仮定する。
つまり
  Lv = 0
$(ラプラシアンの定義)より
  Lv = (GG + FF)v = 0
つまり
  GGv + FFv = 0 ---(1)

$(1)の両辺にGを作用させると
  GGGv + GFFv = 0
$(複体条件)より GF = 0 なので、
  GGGv = 0
つまり
  GG(v)∈Ker(G) ---(2)

一方で、
  GG(v)∈Im(G)
$(Im-Ker随伴性 1)より Im(G) = Ker(G) なので、
  GG(v)∈Ker(G) ---(3)
$(2), $(3)より
  GG(v)∈(Ker(G)∧Ker(G)) ---(4)
$(直交補空間は直交), $(直交する空間の共通部分) より
  Ker(G)∧Ker(G) = {0} ---(5)
$(4), $(5)より
  GG(v) = 0
つまり
  v∈Ker(GG)
$(随伴ラウンドトリップの核)より Ker(GG) = Ker(G) なので、
  v∈Ker(G)
以上より
  v∈Ker(L) ⇒ v∈Ker(G)
vは任意だったから
  ∀v.(v∈Ker(L) ⇒ v∈Ker(G))
つまり
  Ker(L) ⊆ Ker(G)
が示せた。

Ker(L) ⊆ Ker(F) を示す。

$(1)の両辺にFを作用させると
  FGG(v) + FFF(v) = 0 ---(6)
$(複体条件)より GF = 0 なので、
  FG = (GF) = 0 = 0 ---(7)
$(6), $(7)より
  FFF(v) = 0
つまり
  FF(v) ∈Ker(F)
$(Im-ker随伴性 2)より Im(F) = Ker(F) なので、
  FF(v)∈Im(F) ---(8)

一方で、
  FF(v)∈Im(F) ---(9)
$(8), $(9)より
  FF(v)∈Im(F)∧Im(F)
$(直交補空間は直交), $(直交する空間の共通部分) より
  FF(v) = 0
つまり
  v∈Ker(FF)
$(随伴ラウンドトリップの核 2)より
  v∈Ker(F)
以上より
  v∈Ker(L) ⇒ v∈Ker(F)
vは任意だったから
  ∀v.(v∈Ker(L) ⇒ v∈Ker(F))
つまり
  Ker(L) ⊆ Ker(F)
が示せた。

前節の$(ホッジ分解)により、V = Im(F)¥oplusIm(G)¥oplusX と直交直和分解できるわけですが、Xは Ker(F)∧Ker(G) でした。この節の$(調和コチェーンの特徴付け)によれば、Ker(L) = Ker(F)∧Ker(G) なので、ホッジ分解を次の形に書き直すことができます。

  • V = Im(F)¥oplusIm(G)¥oplusKer(L) ---(ホッジ分解 ラプラシアン版)

ラプラシアンの核空間Ker(L)とは、調和形式/調和コチェーンの空間です(前回第7節を参照)。

ド・ラーム・コホモロジー空間

引き続き、ミニ複体 (U, V, W, F, F, G, G) がある状況で話をします。

$(複体条件: F;G = 0 )から Im(F) ⊆ Ker(G) が言えるので、商ベクトル空間 Ker(G)/Im(F) を作ることができます。この商ベクトル空間 Ker(G)/Im(F) を、ミニ複体のド・ラーム・コホモロジー空間〈de Rham cohomology space〉と呼びます。この言葉の由来も前回第7節で触れています。

ド・ラーム・コホモロジー空間 Ker(G)/Im(F) は、ミニ複体から抽象的に定義されるベクトル空間で、Vの部分空間ではありません。しかし、Vの部分空間とみなすことができます。なぜなら、次の同型があるからです。

  • Ker(G)/Im(F) ¥stackrel{¥sim}{=} Ker(L) ---(ド・ラーム・コホモロジーの調和コチェーン表現 1)

ここで、Lは前節の$(ラプラシアンの定義)で定義したラプラシアンです。また前節で、$(調和コチェーンの特徴付け: Ker(L) = Ker(F)∧Ker(G) )を示しているので、次の形でも同じです。

  • Ker(G)/Im(F) ¥stackrel{¥sim}{=} Ker(F)∧Ker(G) ---(ド・ラーム・コホモロジーの調和コチェーン表現 2)

この$(ド・ラーム・コホモロジーの調和コチェーン表現 2)をこれから示すことにします。

まず、内積空間の一般論を少しします。S, Tは内積空間Vの部分空間で、S ⊆ T ⊆ V だとします。Sは、V内でのSの直交補空間です。それに対して、(S in T) は、TのなかでのSの直交補空間を表すとします。典型例を図示すれば次のようになります。

この状況で次が成立します。

  • (S in T) = S∧T ---(相対直交補空間と直交補空間のミート)

これは、u∈(S in T) と u∈S∧T を論理的に書いてみると、どちらも次のようになることから分かります。

  • (任意の s∈S に対して (s|u) = 0) かつ u∈T

次に、やはり S ⊆ T ⊆ V の状況で商空間と直交補空間の関係を考えます。次が成立します。

  • T/S ¥stackrel{¥sim}{=} S∧T ---(商空間と直交補空間)

ターゲット命題: T/S ¥stackrel{¥sim}{=} S∧T  ---(商空間と直交補空間)

線形代数の一般論から、$?(商空間T/Sは、TにおけるSの補空間と同型)。
これより
  T/S ¥stackrel{¥sim}{=} (S in T)
$(相対直交補空間と直交補空間のミート)より
  (S in T) = S∧T
したがって
  T/S ¥stackrel{¥sim}{=} S∧T

$(商空間と直交補空間)を、Im(F) ⊆ Ker(G) ⊆V に対して適用します。すると次が言えます。

  • Ker(G)/Im(F) ¥stackrel{¥sim}{=} Im(F)∧Ker(G)

$(Im-Ker随伴性 1)から、Im(F) = Ker(F) なので、

  • Ker(G)/Im(F) ¥stackrel{¥sim}{=} Ker(F)∧Ker(G)

これは、$(ド・ラーム・コホモロジーの調和コチェーン表現 2)そのものです。

以上より、Ker(G)/Im(F) ¥stackrel{¥sim}{=} Ker(F)∧Ker(G) が得られました。左辺はド・ラーム・コホモロジー空間、右辺はラプラシアンの核空間だったので、ミニ複体において:

  • ド・ラーム・コホモロジー空間 ¥stackrel{¥sim}{=} ラプラシアンの核空間

多様体から線形代数へ

前回の記事と今回の記事の大きな流れとしては、「多様体 → 有限離散近似 → 有限次元線形代数」という翻訳をしています。したがって、有限次元線形代数の範囲内だけで証明された定理に、その起源として、多様体上の幾何・解析的な事実が対応しています。

「多様体 → 有限離散近似」という翻訳は、次のような対応をもとにしています。

多様体 有限離散近似
多様体 M 幾何複体 K
特異チェーンの空間 Ck(M) 組み合わせチェーンの空間 Ck(K)
微分形式の空間 Ωk(M) 組み合わせコチェーンの空間 Ωk(K)
境界作用素 ∂k:Ck(M)→Ck-1(M) 境界作用素 Bk:Ck(K)→Ck-1(K)
外微分作用素 dkk(M)→Ωk+1(M) 余境界作用素 Dkk(K)→Ωk+1(K)
ベルトラミ作用素 δkk(M)→Ωk-1(M) ベルトラミ作用素 Akk(K)→Ωk-1(K)
ラプラシアン Δkk(M)→Ωk(M) ラプラシアン Lkk(K)→Ωk(K)
調和形式の空間 Θk(M) = Ker(Δk) 調和コチェーンの空間 Θk(K) = Ker(Lk)

幾つかの注意事項を述べます。

「多様体Mを、幾何複体Kで有限離散近似する」ことから話が出発しているわけですが、どんな多様体が有限離散近似可能なのか? そもそも、それは近似になっているのか? といった問題はほとんど議論してません。これは難しい問題です。が、個別事例においては「頑張って近似しよう」という態度でもいいのかな、と思います。

Ck(-)とΩk(-)は互いに双対空間となっています。この双対性は、ペアリング〈pairing | evaluation map | 評価射〉 <-|->:Ck(-)×Ωk(-)→R により与えるのがスッキリすると思います。多様体の場合は、微分形式の特異コチェーンに沿った積分がペアリングであり、有限離散近似では、チェーン空間×コチェーン空間上の非退化双線形形式がペアリングになります。

多様体のド・ラーム・コホモロジーは、外微分作用素さえ作れば定義できます。しかし、ホッジ分解の定式化には、Ωk(M)の内積が必要です。内積の構成はけっこう大変です。リーマン計量、外積代数、ホッジ・スター演算子、体積形式による積分などの道具が必要になります。それに対して有限離散近似では、いきなり「Ωk(K)に内積があるとしましょう」でした(苦笑)。個別事例においては、“自然な内積”が見つかりそうだからです。ただ、“正しく近似する”立場からは、有限離散近似でも系統的に内積を構成する手順が必要でしょう。

ベルトラミ作用素〈Beltrami operator〉とは、外微分作用素/余境界作用素の随伴線形写像のことです*6。余微分作用素〈codifferential operator〉と呼ばれることが多いのですが、用語法が混乱する(後述)ので、「ベルトラミ作用素」と呼ぶことにします*7。ベルトラミ作用素は、Ωk(-)→Ωk-1(-) と次数を下げるので、(δk, Akのように)添字は下にしたほうが良かったかも知れませんが、添字ルールはほころびを避けられないので気にしないことにしましょう。

多様体のΩk(M)の要素をk次微分形式/k-形式と呼ぶのですが、外微分作用素/ベルトラミ作用素との関連で、以下のような分類がされています。

呼び名 英語 意味
k次閉形式 closed form of deg. k Ker(dk)の要素
k次完全形式 exact form of deg. k Im(dk-1)の要素
k次余閉形式 coclosed form of deg. k Ker(δk)の要素
k次余完全形式 coexact form of deg. k Im(δk-1)の要素

ウーム、覚えられない。双対を意味する「コ」と「随伴」を形容詞に使ったほうが幾分か系統的でマシだと思います。

伝統的呼び名 マシな呼び名 意味
k次形式 k-コチェーン Ωk(M)の要素
k次閉形式 k-コサイクル Ker(dk)の要素
k次完全形式 k-コバンダリ Im(dk-1)の要素
k次余閉形式 k-随伴コサイクル Ker(δk)の要素
k次余完全形式 k-随伴コバンダリ Im(δk-1)の要素

さて、多様体からその有限離散近似に移った後で、特定のkに注目して、3つの空間 Ωk-1(K), Ωk(K), Ωk+1(K) とそのあいだの余境界作用素/ベルトラミ作用素 Dk-1, Dk, Ak+1, Ak を抜き出します。

そして、次のような名前の付け替えをします。

有限離散近似 有限次元線形代数
Ωk-1(K) U
Ωk(K) V
Ωk+1(K) W
Dk-1k-1(K)→Ωk(K) F:U→V
Akk(K)→Ωk-1(K) F:V→U
Dkk(K)→Ωk+1(K)G:V→W
Ak+1k+1(K)→Ωk(K) G:W→V

この表の右の欄 U, V, W, F, F, G, G によりミニ複体を構成しました。ミニ複体に対する有限次元線形代数の議論(いわばミニ・ホモロジー代数)を展開したのが、今回の第2節から第6節です。

ミニ複体のラプラシアンの定義 L := GG + FF :V→V は、適当なkにおいて、Lk := Ak+1Dk + Dk-1Ak となり、これは多様体上の Δk := δk+1dk + dk-1δk に対応します。そして、k次の離散ラプラシアンLkの核空間Ker(Lk)は、k次の調和形式の空間 Θk(M) = {α∈Ωk | Δk(α) = 0} に対応します。

有限次元線形代数の言葉で語られたホッジの分解定理を、多様体上に戻して解釈すれば:

  • k次微分形式の空間は、“コバンダリの空間”と“随伴コバンダリの空間”と“調和形式の空間”に直交直和分解される。

同様に、ド・ラーム・コホモロジーに関する定理は:

  • 微分形式のド・ラーム複体から構成されたド・ラーム・コホモロジーのk次の空間は、k次調和形式の空間と同型である。

もちろん、多様体上での理論は、有限次元線形代数で済むオモチャとは随分と違います。微積分の知識(ストークスの定理やポアンカレの補題)や、ド・ラーム・コホモロジー以外のホモロジー論(特異ホモロジーとチェック・コホモロジー)も必要になります。しかしそれでも、代数的な大枠は、オモチャと共通する部分があります。

おわりに

前回の記事と今回の記事でやってみたことは、なめらかな関数のグラフを折れ線で近似して、いくつかの数値データを取り出して、それを加減乗除だけの算数で計算したようなものです。算数の計算だけを見れば、それほど難しいことはなく、むしろ味気ないかも知れません。しかし、そのような算数計算も、もとの関数のグラフにおいて解釈すればなにがしかの意味はあるのです。

この2回の記事は、目で見えて手で触れるオモチャの提供が目的なので、端折った雑な議論が多かったです。連続的な対象物・現象の有限離散近似を真面目に考えるのは、もはやオモチャや遊びの域を越えて、シリアスなチャレンジとなります。体力・気力に満ちたアナタにお任せします。

*1:一般化された内積では、v ≠ 0 で (v|v)= 0 であるベクトルの存在を認めていて、それを(非自明な)ヌルベクトルと呼びます。

*2:すぐ後で定義されるカリー化内積Φの核がゼロ空間であることを意味します。これにより、カリー化内積Φは単射です。「(v|v) = 0 ならば v = 0」のことを非退化性と呼ぶことも多いです。

*3:Vの枠を、数ベクトル空間RnからVへの線形同型写像 a:Rn→V だと定義すると何かと都合がいいです。正規直交枠は、Rnの標準内積を保存する内積同型写像として定義できます。

*4:Vの内積は V×V→R という関数なので、カリー化すると V→Lin(V, R) となります。ここで、Lin(V, R)はVからRへの線形写像の空間。Lin(V, R) = V* なので、内積のカリー化は V→V* という線形写像です。

*5:共変/反変を一緒にまとめた代数的複体を双複体〈bicomplex〉とでも呼んで、ミニ双複体とか言うのが正確でしょう。しかし、「複体」という言葉は反変/共変の方向を気にしないで曖昧に使ったりするので、片方向か双方向かが曖昧でも責められはしないでしょう。

*6:有限離散版のベルトラミ作用素がAkとなっているのに大した理由はありません: Bだと境界作用素とかぶるので、余境界作用素DのAdjointだからAとしただけ。

*7:余微分作用素をベルトラミ作用素と呼んでいる前例は記憶にあるのですが、今、見つからない。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20180517