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

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

2018-06-22 (金)

超曖昧語「母集団」「標本」にケリをつける

| 10:15 | 超曖昧語「母集団」「標本」にケリをつけるを含むブックマーク

曖昧・多義的に使われている専門用語は全然珍しくありません。確率・統計の分野でも、たくさんの曖昧語・多義語が登場します。そのなかでも、特に曖昧性がひどく、意味不明の四天王だと僕が思っている言葉は、

  • 確率変数
  • 分布
  • 母集団
  • 標本

です。どれも手強くて、「四天王の中でも最弱」とか「最強」とかの順位付けは難しいです。

*1

「確率変数」については何度も話題にしています。2つだけ過去記事を選ぶなら:

「分布」に関しては:

今回この記事では、残る2つの超曖昧語「母集団」「標本」について、出来る限りの解明を試みます。中心的話題は、「標本」に対するまったくかけ離れた2つの定義を結びつけることです。2つの定義を結びつけるために、「独立ベキ測度の前送り定理」を紹介します。

内容:

  1. 諸悪の根源: 構造と台集合の混同
  2. 「母集団」の背後にある構造
  3. 母集団に関する記法と概念
  4. 母集団からの標本
  5. 抽出法とコレクションデータ型
  6. 抽出される確率と抽出の確率空間
  7. 標本サイズごとに分けて考える
  8. 確率空間の独立積/独立ベキ
  9. IID列と独立ベキ測度の前送り定理
  10. おわりに

諸悪の根源: 構造と台集合の混同

曖昧語・多義語が生まれてしまう原因は色々あるでしょうが、広く浸透している悪習が原因となっていることがあります。そんな悪習のひとつに:

  • 構造と、その構造を載せている台集合を区別しない、意図的に混同する

という習慣があります。悪習なので弊害があります。しかし、広く浸透しているので、今さらどうにもならないものです。

例えば、すべての自然数からなる集合は N = {0, 1, 2, ...} と書かれます。Nは単なる集合です。N上に大小順序を考えれば、(N, ≦) は順序集合(順序構造を持った集合)となります。N上に足し算を考えれば、(N, +, 0) は可換モノイドになります。掛け算を考えても、(N, ×, 1) は可換モノイドです。足し算と掛け算の両方とも考えれば、(N, +, 0, ×, 1) は可換半環〈commutative semiring〉だし、それに順序もあわせると、(N, +, 0, ×, 1, ≦) は順序半環〈ordered semiring〉です*2

Nとだけ書いたときは、本来なら単なる集合のはずです。ところが、文脈により、順序集合としてのN、可換モノイドとしてのN、可換半環としてのN、順序半環としてのNなどの多様な意味で(つまり、曖昧・多義的に)Nが使われます。

曖昧性が多少は解消するように、あるいは、意図的に曖昧に書いていることを表明するために、次のような記法が使われます。

  • N = (N, ≦)
  • N = (N, +, 0)
  • N = (N, ×, 1)
  • N = (N, +, 0, ×, 1)
  • N = (N, +, 0, ×, 1, ≦)

ある特定の文脈で、けっこう複雑な構造を想定していても、台集合(集合だけでは何の構造もない)により、構造を代表させることがあるのです。そんなとき、文字通りに集合だと受け取ってはダメです。空気を読んで、集合上の構造を想定するのです。

このテの悪習に文句を言ってもはじまりません。やめさせることは絶対に不可能ですから。悪習が蔓延〈はびこ〉っている事実を認識して注意するだけです。

「母集団」の背後にある構造

「母集団」という言葉は、前節で述べた悪習にひどく蝕〈むしば〉まれた言葉です。表立っては集合として定義されますが、背後には複雑な構造があります。

例えば、日本人の成人男性全員からなる集合をAとしましょう。集合Aを母集団と呼ぶのは普通のことです。しかし、集合Aだけがあってもなんも面白くありません。A上で定義された関数が考察の対象になります。例えば、身長を考えましょう。身長は f:A→R という関数として定式化されます。とりあえず、集合Aと関数 f:A→R を組み合わせた構造 (A, f) が想定できました。

身長関数 f:A→R に誤差は考えないことにします。Aの各要素(日本人成人男性の個体)aに対して f(a) が実数として正確に定まると想定します。このfは確率変数です。変数ではないし、ランダム性(偶然による不定性/予測不可能性)はコレッポッチもありませんが、それでも確率変数です*3

単なる関数(正確には可測関数)を確率変数と呼ぶのはいいのですが(いや、良くないけど認めましょう)、「確率変数」という言葉を使うときのココロとして「関数の域〈domain〉には確率測度が載っている」という想定があります。つまり、集合A上に確率測度が必要です。

確率測度は測度に条件が付いたものです。測度概念(測度空間)を構成する材料は次のものです。

  1. 台集合
  2. σ代数〈σ集合代数 | 完全加法族〉
  3. 測度(測度関数)

台集合はA(日本人成人男性)と決まっているので、A上のσ代数と測度を定義しましょう。

  • σ代数は、Aのベキ集合 Pow(A) に通常の集合演算を考えたもの。これをΣ(総和記号じゃないよ!)と書く。
  • 測度(測度関数) ν:Σ→R を、S∈Σ に対して ν(S) = (Sの基数〈個数〉) とする。

Aは有限集合なので S⊆A も有限集合で、ν(S)は集合Sの個数(人数)を勘定した値です。

(A, Σ, ν) は測度空間になりますが、確率空間(確率測度を持った測度空間)にはなっていません。ν(A) = 1 ではないからです。そこで、新しい測度μを次のように定義します。

  • μ(S) := ν(S)/ν(A)

μは、正規化された基数測度です。(A, Σ, μ) は確率空間になります。確率空間 (A, Σ, μ) にも「偶然による不定性/予測不可能性」といった意味合いは(今のところ)見い出せません*4

以上に述べたように、母集団Aと言った場合、集合Aだけを意味しているのではなくて、構造 (A, Σ, μ, f) を想定しています。これを、広く浸透している悪習に従って書けば:

  • A = (A, Σ, μ, f)

イコールの左側のAは構造としての母集団、右側のAは台集合としての母集団です。

母集団に関する記法と概念

前節で述べたように、母集団の構造は (A, Σ, μ, f) のように書くことにします。

  • Aは母集団の台集合(狭義の母集団)
  • Σは母集団のσ代数
  • μは母集団の確率測度
  • fは母集団の変量〈variate〉

と呼ぶことにします。複数の母集団を考える場合は次のように書きます。

  • A = (A, ΣA, μA, fA)
  • B = (B, ΣB, μB, fB)

もし、構造と台集合をちゃんと区別したいなら、台集合をΩAのように書くことにします。また、変量fAの余域〈codomain〉はXAと書きましょう。この記法だと:

  • A = (ΩA, ΣA, μA, fAA→XA)

A, ΣA) は可測空間、(ΩA, ΣA, μA) は確率空間の構造であり、fAA→XA は確率変数(可測関数)です。ここから先では、fA と XA の下付きAは省略して、f, X と書きます(さすがにウザいからね)*5

ときに多変量〈multivariate〉の母集団を考えることがあります。例えば、身長 f:A→R と共に体重 g:A→R も考えるとかです。一般に、f1:A→X1, f2:A→X2, ..., fk:A→Xk がk個の変量のとき、

  • f(a) := (f1(a), f2(a), ..., fk(a))

と定義した

  • f:A→X1×X2×...×Xk

を考えれば、X1×X2×...×Xk に値をとるひとつの変量fがあるとみなすことが出来ます。よって、とりたてて多変量を扱うことはしません*6

僕の他の記事でも述べているように、「確率分布」は「確率測度」と同義語です。ときに、確率密度関数を確率分布とも呼びますが、確率密度関数から確率測度が決まるので、確率分布=確率測度 で大丈夫でしょう。

さて、母集団 A = (A, ΣA, μA, f:A→X) の分布と言った場合、もともとある確率測度μの意味ではなくて、μをfでX側に前送り〈push-forward〉した確率測度を意味することが多いようです。前送り測度(像測度ともいう) f*(μ) は次のように定義されます。

  • U∈ΣX に対して、(f*(μ))(U) := μ(f*(U)) ここで f*(U) := {a∈A | f(a)∈U}

変量が値をとる空間Xにもσ代数ΣXはあるとしています。多くの場合、X = R か X = Rk なので、X上には標準的なΣXがあります。

母集団からの標本

A = (A, ΣA, μA, f:A→X) を母集団とします。日本人成人男性の例は離れて、以下、一般論であることに注意してください。

母集団Aからの「標本」という言葉があります。この「標本」の意味が僕はサッパリ分かりませんでした。いくつかの定義(らしきもの)があるのですが、それらの定義(らしきもの)の相互関係が理解できないのです。そもそもが無関係の同音異義語って可能性もありますしね。

まず、確率空間の文脈で「標本空間」という言葉があります。これはまー、割とどうでもいいので、すぐ下の補足コラムにします。本文では、確率空間の標本空間じゃなくて、調査目的で抽出される標本を問題にします。

[補足]

A, ΣA, μA) が確率空間のとき、台集合ΩAを標本空間〈sample space〉と呼びます。ΩAの要素を標本点または単に標本とも呼びます。これは、「そう呼ぶよ」って約束なので、「はい、そうですか」ってだけの話です。

f:ΩA→X が確率変数(単なる可測関数)のとき、集合X上に前送り測度 f*(μ) を載せると、(X, ΣX, f*(μ)) は確率空間になり、できた確率空間の標本空間はXです。この状況で:

  1. ΩAを標本空間と呼び、Xは標本空間とは呼ばない。
  2. Xを標本空間と呼び、ΩAは標本空間とは呼ばない。
  3. ΩAもXも標本空間と呼ぶ。

という用法があります。もともとが確率空間の台集合を標本空間と呼ぶなら、「こっちを標本空間とは呼ばない」という判断は根拠がありません。一方で、確率空間の台集合をすべからく標本空間と呼ぶなら、確率・統計の文脈で出てくる集合は、たいてい標本空間となるわけで、あえて標本空間と呼ぶ意義があるか疑問です。

そして、今問題にしている「調査目的で抽出された標本」との混同・混乱も生じるので、確率空間の台集合を標本空間と呼ぶのはやめたほうがいいだろうと思います。

[/補足]

「標本」に対するよくある説明を見てみましょう。「基本統計量の算出」というWebページによれば、

  • 母集団: 分析が対象とするすべてのデータ.例えば,早稲田大学の学生全員.
  • 標本: 母集団からの一部のデータ.例えば,今日,教室にいる早大生諸君.

と説明されています。

ここでの「母集団」は、母集団構造の台集合のことでしょうから、集合としてのAです。「一部のデータ」の意味は、事例「今日,教室にいる早大生諸君」を考慮すると、Aの部分集合のことのようです。つまり、次のように定義してよさそうです。

  • 母集団 A = (A, ΣA, μA, f:A→X) からの標本とは、集合としてのAの有限部分集合のことである。

Sが標本だとは、「S⊆A かつ Sは有限集合」という意味です。有限集合Sの基数(個数)を標本サイズ〈sample size〉と呼びます。

大数の法則や中心極限定理でも“標本”を扱います。ここで登場する標本は母集団台集合の有限部分集合でしょうか? 中心極限定理の定式化などを見るに、まったく違ったものを標本と呼んでいるようです。

集合Aから集合Xへの確率変数(単なる可測関数)の列 g1, g2, ..., gn独立同分布だとは、次のことです。

  • g1, g2, ..., gn は独立な確率変数である。
  • giによる前送り測度 (gi)*(μ) は、すべて等しい。つまり (g1)*(μ) = (g2)*(μ) = ... = (gn)*(μ)

独立同分布をIID〈independent and identically distributed〉と略称するので、独立同分布な確率変数の列をIID列と呼ぶことにします。中心極限定理などの文脈における標本とはIID列のことです。

  • 母集団 A = (A, ΣA, μA, f:A→X) からの標本とは、IID列 g1, g2, ..., gn : A→X であって、(gi)*(μ) = f*(μ) を満たすものである。

nを標本サイズと呼ぶのは同じです。

しかし、それにしても、この2つの定義、あまりにも違いすぎませんか。こんだけ違うと同じ名前で呼ぶわけにもいかないので、先の定義による標本を標本部分集合〈sample subset〉と呼び、今の定義による標本を標本IID列〈sample IID sequence〉と呼ぶことにします。標本部分集合のサイズは基数(個数)のこと、標本IID列のサイズは列の長さのことです。

抽出法とコレクションデータ型

実際の調査作業として“標本”を選び出すとき、いくつかのやり方があるようです。それを(標本の)抽出法と呼びます。例えば、アンケート調査とかを思い描いてください。

  • 非復元抽出 : 一度選んだ個体(例えば人)は、もう選ばないようにする選び方
  • 復元抽出 : 一度選んだ個体でも、また選んでもよい選び方
  • 非順序抽出 : 選んだ順序は無視する(記録しない)選び方
  • 順序抽出 : 選んだ順序も記録する選び方

この分類は2×2のマトリックスとして理解したほうがいいでしょう。

復元 非復元
順序 順序復元抽出法 順序非復元抽出法
非順序非順序復元抽出法 非順序非復元抽出法

これらの抽出法は、プログラミングにおける複合データ型構成と密接に関係します*7。いま、Zを何でもいいから集合(プログラミング的にはデータ型)としましょう。Zの要素を組み合わせて新しいデータ型を作ることができます。次のようなデータ型があります。

  1. Subset(Z) : Zの有限部分集合をデータ(インスタンス)とするデータ型
  2. List(Z) : Zの要素を並べたリストをデータとするデータ型
  3. UniqList(Z) : Zの要素のリストだが、同じ要素の重複出現を許さないリストをデータとするデータ型(Uniqは一意性を意味するuniqueから)
  4. Bag(Z) : Zの要素を集めたバッグをデータとするデータ型

バッグ〈bag〉とは、要素の並び順は考慮しないが、要素の重複出現回数は意味を持つデータです。これらのデータ型は、要素の集まり〈collection〉のデータ型なので、コレクションデータ型〈collection data type〉と呼びます*8

この節冒頭で説明した抽出法により選んだ結果のデータは、コレクションデータ型のデータ(インスタンス)になります。A = ΩA を母集団台集合として:

  1. 非順序非復元抽出法による抽出結果 → Subset(A)型のデータ
  2. 順序復元抽出法による抽出結果 → List(A)型のデータ
  3. 順序非復元抽出法による抽出結果 → UniqList(A)型のデータ
  4. 非順序復元抽出法による抽出結果 → Bag(A)型のデータ

前節で述べた標本部分集合は、抽出法として非順序非復元抽出法を採用した場合の抽出結果ですね。他の抽出法を排除する理由はないので、「標本」の意味を次のように変更したほうがいいでしょう。

  • 母集団 A = (A, ΣA, μA, f:A→X) からの標本とは、何らかの抽出法による抽出結果であるコレクションデータ型のデータである。

こうすると、標本は、抽出法(あるいはコレクションデータ型)に依存するので、次のように呼び分けるべきです。

  1. 標本部分集合
  2. 標本リスト、または標本タプル*9
  3. 標本一意リスト(重複を許さないリスト)
  4. 標本バッグ

これらを総称するときは、標本コレクション〈sample collection〉ということにします。標本コレクションの一般論もできます。しかし、採用する抽出法(コレクションデータ型)により、その後の議論が大きく変わるところもあります。なので、抽出法(コレクションデータ型)を明示しない曖昧な議論は好ましくありません。

理論的に扱いやすい抽出法(コレクションデータ型)は順序復元抽出法(リスト型)です。IID列としての定義に直接結びつくのは、“標本リスト=リスト型の標本データ”に限られます。なので、当初は「標本=標本部分集合」と定義されたにしても、どこかで「標本=標本リスト」に変更する必要があります。このような区別や切り替えを曖昧なままにすることがあるとすれば、それも悪習です。

抽出される確率と抽出の確率空間

確率というと、コイントス、サイコロふり、宝くじなどの博打のイメージがあるでしょう。しかし、日本人成人男性の身長のような例では、博打的要素はないように思えます。実は、博打的要素が入ってくるのは、標本抽出の時点なのです。

例えば、A = 日本人成人男性, f = 身長 の例で、何人かが標本として抽出されるとします。どんな人々が標本として抽出されるかには「偶然による不定性/予測不可能性」があります。いやむしろ、「偶然による不定性/予測不可能性」があるように選ぶべきなのです。

それぞれの標本部分集合や標本リストには、抽出される“可能性の度合い”が定まります。これは、抽出される確率の確率密度です。確率密度関数があるということは、確率空間の構造があるはずです。標本部分集合の場合、つまり、抽出法として非順序非復元抽出法を採用した場合なら次のようになります。

  • 台集合: Subset(ΩA) : もとの母集団の台集合ΩAの有限部分集合全体からなる集合
  • σ代数: Subset(ΩA) のベキ集合 Pow(Subset(ΩA)) の部分代数である“なんらかのσ代数”
  • 確率測度: すぐ上のσ代数上で定義された“なんらかの確率測度”。Subset(ΩA) 上に確率密度関数が定義できれば、それをもとに確率測度を構成できる。

抽出法として、順序復元抽出法を採用するならば、上記のSubsetをListに置き換えた定義になります。“なんらかのσ代数”と“なんらかの確率測度”は自動的に生じるものではなく、頑張って構成しなくてはなりません。

Subuset(ΩA), List(ΩA) のように、抽出法により変わる「すべての標本データからなる集合」を総称して(抽象化して)、Sample(ΩA) と書くことにします。また、“なんらかのσ代数”と“なんらかの確率測度”をちゃんと決めて作った確率空間を Sample(A) とします。つまり、

  • Sample(A) = (Sample(ΩA), ΣSample(A), μSample(A))
  • Sample(ΩA) は、集合ΩAから作った「すべての標本データからなる集合」
  • ΣSample(A) は、頑張って構成した“なんらかのσ代数”
  • μSample(A) は、頑張って構成した“なんらかの確率測度”

“標本”という概念がとても難しい理由は、母集団Aから作った確率空間 Sample(A) = (Sample(ΩA), ΣSample(A), μSample(A)) を把握・理解するのが難しいからです。把握・理解せずにごまかして進むのも難しいです。もとの母集団Aと採用した抽出法に基づいて、台集合/σ代数/確率測度を具体的に構成してみるのが結局は近道なのかと思います。

次節以降で、抽出法を順序復元抽出法に限定して、確率空間 List(A) を構成してみます。

標本サイズごとに分けて考える

母集団 A = (ΩA, ΣA, μA, f:ΩA→X) に対して、標本リストの集合 List(ΩA) を台集合とする確率空間 List(A) = (List(ΩA), ΣList(A), μList(A)) を構成しましょう。この際、母集団の変量 f:ΩA→X は関係しないので、与えられた確率空間 (ΩA, ΣA, μA) から、新しい確率空間 (List(ΩA), ΣList(A), μList(A)) を構成する問題になります。

確率空間 (List(ΩA), ΣList(A), μList(A)) があるとは、標本リストの集合 S⊆ List(ΩA) に対して、Sが抽出される確率 μList(A)(S) が決まることです。ΩAが有限集合のときは、標本リスト(のインスタンス) s∈List(ΩA) ごとに μList(A)({s}) が決まれば抽出確率測度 μList(A) も決まりますが、一般的には μList(A)({s}) が意味を持つとは限りません(一点の確率は全部0かも)。

とりあえず、すべての標本リストの集合 List(ΩA) の上に確率測度を載せるのは難しそうなので、標本サイズ(リストの長さ)nを固定して考えましょう。

  • ListnA) := {s∈List(ΩA) | size(s) = n}

とします。List(ΩA) を全体として考えるのではなくて、nごとに ListnA) を考えて、nごとの確率空間を構成します。

  • Listn(A) = (ListnA), ΣListn(A), μListn(A))

ここで重要な事実は、n = 1 のとき、

  • List1(A) ¥stackrel{¥sim}{=} A

であることです。この同型関係の意味は、まずは集合として List1A) ¥stackrel{¥sim}{=} ΩA であり、この集合の同型に基づいて、σ代数の同型(可測空間としての同型)、確率測度の同型(確率空間としての同型)が言えるということです。

母集団の上に最初に与えられた確率空間構造は、サイズ1の標本(ひとつの個体)を抽出する際の抽出確率だったのです。ΩAが有限集合のとき、正規化された基数測度を母集団上の確率としたのは、「どの個体も公平に抽出される」ことの表現です。ΩAが有限でない場合でも、ΩA上に“なんらかの意味での一様確率測度”*10があれば、それが抽出の公平性の表現となるでしょう。与えられた確率測度μAが公平ではない、あるいは公平性の概念がないなら、それはそれで別にかまいません。μAが分かっている、あるいは想定できることが大事なのです。

List1(A) が何であるか分かったので、次に List2(A) を考えてみます。抽出法は順序抽出なので、1個目の標本データと2個目の標本データの区別があります。2個抽出に関して、次のことは仮定していいでしょう。

  1. 1個目の抽出結果が、2個目の抽出に影響を与えることはない。
  2. 1個目を抽出する際の抽出確率測度と、2個目を抽出する際の抽出確率測度は同じ。

このような仮定のもとで、確率空間 List2(A) (Listn(A) でも同様)を構成するには、独立積/独立ベキが使えます(次節)。

確率空間の独立積/独立ベキ

この節では、A, B などは(変量を持つ母集団ではなくて)単なる確率空間とします。アルファベットは有限個しかないので、使い回すしかないのですよ、かんべんしてね。

A = (ΩA, ΣA, μA) と B = (ΩB, ΣB, μB) に対して、AとBの独立積確率空間 A¥otimesB を定義できます。独立積〈independent product〉に関しては、次の記事で説明しています*11

AとBの独立積 A¥otimesB の構成要素は:

  • ΩA⊗B = ΩA×ΩB : 集合の直積
  • ΣA⊗B = ΣA¥otimesΣB : σ代数の独立積(テンソル積)
  • μA⊗B = μA¥otimesμB : 確率測度の独立積(テンソル積)

A = B の場合、A¥otimesA = A⊗2 と書いて、独立積の意味での二乗と考えます。より一般には:

  • A⊗n := A¥otimes... ¥otimesA (n個のAの独立積)

独立積の意味でのn乗を独立ベキ〈independent power | independent exponential〉と呼びます。

与えられた確率空間Aからの、サイズnの標本リスト抽出に関する確率空間 Listn(A) = (ListnA), ΣListn(A), μListn(A)) は、Aのn乗の独立ベキ A⊗n で与えられます。

  • ListnA) ¥stackrel{¥sim}{=}A)n (集合の直積の意味でのn乗)
  • ΣListn(A) ¥stackrel{¥sim}{=} ΣA⊗n = ΣA¥otimes ... ¥otimesΣA = (ΣA)⊗n
  • μListn(A) ¥stackrel{¥sim}{=} μA⊗n = μA¥otimes ... ¥otimesμA = (μA)⊗n

このようにして与えられた、台集合 ListnA) ¥stackrel{¥sim}{=}A)n 上の確率測度 μListn(A) ¥stackrel{¥sim}{=} μA⊗n = (μA)⊗n が、順序復元抽出法(リストデータ型)に伴うサイズnの抽出確率測度〈sampling probability measure〉です。確率測度と確率分布(略して単に分布)は同義語なので、抽出分布〈sampling distribution〉と言っても同義だし、"sampling"を「標本」と訳せば、標本分布でも同じことです。ただし、「分布」というときのココロ=言葉のニュアンスから、変量の値の空間Xを登場させる必要があるかも知れません(すぐ後に記述)。

さて、確率測度が載ってない単なる可測空間 X = (ΩX, ΣX) と Y = (ΩY, ΣY) に対しても、確率空間の独立積と同じように、X¥otimesY = (ΩX×ΩY, ΣX¥otimesΣY) を定義できます。行きがかり上、これも可測空間の独立積と呼んでしまいましょう。独立ベキ X⊗n = X¥otimes ... ¥otimesX も同様に定義します。

ここで、話を母集団 A = (ΩA, ΣA, μA, f:ΩX→X) に戻します。あっ、同じ文字'A'を使っていても、今度のAは母集団ね。母集団が単なる確率空間と違うのは、変量 f:ΩA→X を持つところです。確率空間や可測空間に独立ベキを定義できることは分かりました。変量fにも独立ベキを定義できるでしょうか? できます! 独立ベキとは言っても、単なる写像としての直積ベキですけどね。

f:ΩA→X に対して、

  • (f× ... ×f)(a1, ..., an) := (f(a1), ..., f(an))

として f× ... ×f:ΩA× ... ×ΩA→X× ... ×X を定義します。f× ... ×f をf×nと略記して:

  • f×n:(ΩA)n→Xn

今定義した f×n を確率空間の独立ベキに添えてあげると、母集団の独立ベキを定義できます。

  • A⊗n := ((ΩA)n, (ΣA)⊗n, (μA)⊗n, f×n:(ΩA)n→Xn)

これはまた、母集団Aに対する Listn(A) だと言ってもいいでしょう。

  • ListnA) ¥stackrel{¥sim}{=}A)n
  • ListnA) ¥stackrel{¥sim}{=}A)⊗n
  • ListnA) ¥stackrel{¥sim}{=}A)⊗n
  • (Listn(f):ListnA)→Listn(X)) ¥stackrel{¥sim}{=} (f×n:(ΩA)n→Xn)

こうして構成された母集団Aのn-独立ベキ A⊗n は、f×n:(ΩA)n→Xn を変量として持ちます。母集団台集合上に載る確率測度を、変量で前送りした確率測度を「分布」と呼びたがる傾向(言葉のニュアンス)があるので:

  • (f×n)*((μA)⊗n)

これが、皆さんお望みの標本確率分布〈抽出確率分布〉です。

母集団 A = (ΩA, ΣA, μA, f:ΩA→X) を調べる際にもっとも欲しいのは標本確率分布、つまりXn上の確率測度です。標本リストの空間 ListnA) ¥stackrel{¥sim}{=}A)n は、標本確率分布構成の素材に過ぎないと言えます。Xn上の標本確率分布ができあがると、ΩAや (ΩA)n忘れ去られてしまうこともあります。さらに、(ΩA)n とXn同一視してしまうこともあります。これも悪習ですが、しょうがない。

IID列と独立ベキ測度の前送り定理

標本IID列がまだ出てきてませんね。標本IID列は、前節最後に登場した標本確率分布を構成する道具です。母集団の独立ベキを構成した上で、独立ベキ上の前送り測度として標本測度を構成する方法(前節)が、僕は自然だと思いますが、「独立ベキを採用したくない」という方針もあるでしょう。そんなときに使われる手法がIID列です。

[追記] f×nで前送りするのはいいけど、f<n> = <f, ..., f> による前送りはダメですね。像測度が対角集合に集中してしまって、独立積による測度と一致しません。<f, ..., f> という記号表現のf達が、「同じ名前でも互いに独立ならば」という変な前提で計算してしまったのですが、そんなワケない! 錯覚でした。

後日訂正をしますが、もとの文(間違い)も消し線付きで残しておきます。[/追記]

まず、母集団の変量 f:ΩA→X に対して、関数fのn-タプルの意味でのベキを構成します。

  • <f, ..., f>(a) := (f(a), ..., f(a)) (すべての成分がf(a))

<f, ..., f>をf<n>と略記することにして、

  • f<n>A→Xn

集合の直積ベキXn上の可測空間構造は既に述べました。X⊗n = (Xn, (ΣX)⊗n) ですね。すると、f<n>によって、母集団台集合ΩAに載った確率測度μAを前送りできます。

  • (f<n>)*A)

この (f<n>)*A) はもちろん、集合Xn上の確率測度です。この確率測度を作る際に、<f, ..., f> じゃなくても、IID列 g1, ..., gn から作った <g1, ..., gn> を使っても同じ確率測度ができ上がります。これが標本IID列の使い方です。僕には、なんか技巧的な方便な感じがします。

[追記]ここから先はあってます。消し線のところを無視してもらえれば訂正になっているけど、たぶん間違った理由を説明します、後日。[/追記]

前節で「標本確率分布」と呼んだ確率測度を作る際に、f×n = f× ... ×f じゃなくても、IID列 g1, ..., gn から作った g1× ... ×gn を使っても同じ確率測度ができ上がります。これが標本IID列の使い方です。僕には、なんか技巧的な方便な感じがします。

さて、前節で作ったXn上の確率測度 (f×n)*((μA)⊗n) と、g1× ... ×gn により作ったXn上の確率測度 (g1× ... ×gn)*((μA)⊗n) が同じでないと困ります。同一性を保証する定理を「独立ベキ測度の前送り定理」と呼んでおきましょう。その主張は次の等式になります。

  • (f×n)*((μA)⊗n) = (g1× ... ×gn)*((μA)⊗n) = (f*A))⊗n

2つの確率測度の定義を追いかけて、σ代数の生成系の上で測度が等しい値を取ることを確認すれば示せます。

おわりに

以上述べたようなストーリーをたどることにより、調査実務としての標本概念からIID列までをつなぐことができます。確率変数のIID列という道具は確かに便利なんですが、唐突な感じは否めません。IID列は、“確率空間/母集団”の“独立積/独立ベキ”という概念を省いてショートカットする道具という位置付けではないでしょうか。

抽出法としては順序復元抽出法(標本データがリスト型データ)だけを述べましたが、別な抽出法ならば、変量の値の空間は、Xn = Listn(X) ではなくなるし、標本確率分布(変量の値側の確率測度)の構成も変わります。難しくなります。

今日はもう述べませんが、標本の抽出法がコレクションデータ型と対応するという事実はなかなか面白くて、標本の抽出法も(コレクションデータ型がそうであるように)関手やモナドとしての記述を持ちます。

さて、この長い記事で、超曖昧語「母集団」「標本」を解明することが出来たでしょうか。出来ていたらいいけど。

*1:画像: https://www.ttrinity.jp/product/3196459 より

*2:もちろん、それぞれの構造が満たすべき法則(公理)も一緒に考えています。

*3:身長の測定に誤差が生じてしまう事態を考えることも当然にあります。そのときは、fは誤差の影響を受けるという意味で「確率的」と言えるでしょう。今回の話は、誤差なしの設定だ、ということです。

*4:後で、正規化された基数測度を、選ばれるチャンスが公平であることだと再解釈します。

*5:しかしそれでも、混乱の心配があれば fA, XA のように書くべきです。「めんどくさいから省略」を積み重ねると意味不明になるので。

*6:変量のあいだの関係を問題にする場合など、多変量を多変量のまま扱う必要性もあります。

*7:この関係に気付くと、標本抽出が、モナド的な構造を持つであろうことも予想できます。

*8:コンテナデータ型と呼ぶこともあります。

*9:コンピュータで扱うデータとしては、リストとタプルは区別されます。メモリーレイアウトや操作可能性が違うからです。しかし、要素を並べた列という意味でなら同義語とみなしていいでしょう。

*10:「一様」だと言えるには、平行移動のような異なった場所を重ねて比較するメカニズムが必要です。したがって、異なる場所を比較できない場合は、「一様」に意味を持たせることができません。[追記]別な「一様」の定義として、標準的な測度が事前にあって、その標準測度に関して確率密度関数が定数というのもありますね。でも、「標準測度は公平」の根拠は天下り。[/追記]

*11:「確率空間の凸結合と分割」で、続きがあるようなことを書いてますが、この記事は続きではありません。

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

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円以下のメニュー項目がなくても、[発券]ボタン(↓)を押さないと食券が出てきません。無事に食券が出てきても、明示的に[おつり]ボタン(↓)を押さないとお釣りが出てきません。

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

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

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

通りすがり通りすがり 2018/06/19 02:48 下のお釣り出口は、お札が出てくるのじゃないかな、と思いました。

m-hiyamam-hiyama 2018/06/19 10:13 通りすがりさん、
なるほど、そうですね。

トラックバック - 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が測度ゼロの集合になる、でもいいでしょうが、煩雑なので空集合にしておきます。

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