テキストか画像か、… えっ!?

コーヒーを飲んでいたり食事をしていても、そのテの会話は耳に入ってしまいます。“そのテ”とは、「日報の管理をデジタルデータに移行する」ための打ち合わせ的な会話です。

メール本文にテキストで書いてもらうか、画像を添付してもらうか、どっちにしようか? みたいな内容でした。まず、「メールなんかい?」と思いました。さらに、画像添付の画像とは手書きの用紙をスキャンするか写真に撮るらしいと知って、「えーっ、なにそれ?」 -- それならメール本文のほうがマシだろう、と。

ところが、画像添付方式に話が決定しそうな流れに。「そのほうが手間が少ないから」と。他人事ながら、「いや、手書きして画像にするほうが手間がかかるだろう」と言いたくなります。が、僕の誤解でした。

紙の日報を廃止できない前提なのです。どっちにしろ紙の日報を書くので、それをテキストデータに書き写すよりは、画像にするほうが手間が少ないだろう、ということです。確かに。

しかしそれにしても、メール添付で集まった画像データをいったいどうやって「管理」するのでしょうか? まー、他人事だけどさ。

苦難! それぞれの戦略と選択

たい焼き屋さんにはとって、夏場は苦難の季節ですね。

天然たいやき 鳴門鯛焼本舗

夏場のあいだは休業。

赤字で営業するよりは、いっそ休んでしまえ、と。これもひとつの判断でしょう。

一方、銀座たい焼き 櫻家

店舗をリニューアルしました。

とりあえず今年の夏はタピオカ押しで乗り切る戦略でしょうか。

掛け算の順序問題: 檜山の地雷を踏まないで

掛け算の順序問題: 左右の意味あいが違う事例はあるけど…」:

掛け算順序区別論に反論する気もないです。理由は、めんどくさいからです。鬱陶しいからです。

反論しない主たる理由が「めんどくさい/鬱陶しい」からなのはホントです。

で、「それはそうだけど」の事例を幾つか出します。「もう、それは分かっているからさー」と言いたいから確認するだけです。そこから先の本論はしないけどね。

「そこから先の本論」はしたくないのです(したくなかったのです)。

実は、したくない理由がもうひとつありまして; そこから先の本論に入ると、僕は感情的になり強い言葉を吐くであろうことが予測できるからです。

僕は、根性主義や体罰を極度に嫌っているのですよ。2006年3月以前の、「アンチ根性主義」に関連する記事は、次のリンク集からたどれます。

そこから2016年までの間の記事は、次の記事内にリンクがあります。

2018年記事でも過去記事群を参照してます。

根性主義/体罰と、掛け算の順序問題は何の関係もないだろうと思えるのですが、過敏(ゆえに不正確)な僕のセンサーは反応してしまうのです。

非常に抽象度の高いくくり方をすると、「正しい目的のためには、多少は乱暴な/望ましくない手段も許される」という考え方が、それはそれは物凄く、とてつもなく嫌いなんです。

「正しい目的」があるがために、賛同や共感を得やすく、実際に多くの人が「乱暴な/望ましくない手段」を許容してしまう事態が、ほんとにほんとに腹立たしくイラつくのです。どんなに正しい目的(例:スポーツで優勝する)であっても、当事者の心身を傷付けるような行為はダメです。

直前の2つの記事で僕が書いている事は、掛け算順序問題の背後にある「正しい目的」についてです。「もう、それは分かっているからさー」と言いたいから書いたのです。(だから、もう繰り返し言わないで。)

掛け算順序問題の「正しい目的」のために、ローカル・ルールを押し付けて守らせる(服従させる、とも言える)のは、やはり「乱暴な/望ましくない手段」なので、僕は許容できません。完全にエモーショナルな理由で、理論的根拠なんてありません。

掛け算の順序問題: 左右の意味あいが違う事例はあるけど…

「掛け算の順序(あるいは左右)を区別して、それを逆に(左右を交換して)書くことは過ちとすべき」という意見の持ち主を、ここでは“掛け算順序区別論者”と呼ぶことにします。

僕は、掛け算順序区別論者に与することはありません。とはいえ、

「5×4 と 4×5 を区別せよ」論者に対して、懇切な説明や説得を試みる気はありません。「5×4 と 4×5 を区別せよ」を本気で主張している人を説得できる可能性は低いでしょう。説得可能だとしても、とても労力がかかるでしょう。-- 不毛。

掛け算順序区別論に反論する気もないです。理由は、めんどくさいからです。鬱陶しいからです。

ひとつ前の記事のコメント欄で、差し障りがある事を言ってしまったんですが:

結局、このテの“掛け算順序区別論者”は、現象と法則の認識能力と、それを整理して位置付けるバランス感覚が欠如しているんだよね。だから説得できない。

バランス感覚が欠如している相手は説得できないから、説得はしないよ、は本音です。

“めんどくさい/鬱陶しい”ことになる事情のひとつは、掛け算順序区別論者が根拠とする個別事例(例えば、入れ子になったループの内側と外側を交換できないとか)は、それ自体は正しいので、「それはそうだけど」と言わざるを得ないことです。「それはそうだけど」の後が本論なのだけど、「それはそうだけど…」「でしょう、やっぱりそうでしょう。他にも…」みたいな展開になると、もうウンザリ、グンニャリ

で、「それはそうだけど」の事例を幾つか出します。「もう、それは分かっているからさー」と言いたいから確認するだけです。そこから先の本論はしないけどね。


掛け算の背後にある状況、算数の文章題が記述するような状況では、a×b のaとbが異なる意味あいを持つことは多いです。「速さ×時間」は典型的でしょう。

  • a km/時間 × b 時間

これを、速さを固定して時間を動かすと考えれば、距離 = f(時間) という「等速直線運動を記述する関数」になります。関数 f が、パラメータである速さ a km/時間 で決まる状況です。

関数適用 f(b) を、<f | b> の形に書いてみます。これも一種の掛け算と言えます*1が、<f | b> の左は関数で右はその引数です。線形代数の文脈では、左が双対ベクトル空間の要素(コベクトル)で、右が元のベクトル空間の要素(ベクトル)になります。関数と引数、あるいは双対空間と元の空間を混同するのはマズイので、左と右は区別すべきです。

しかし、<f | b> という書き方の約束は恣意的なものであり、<b | f> と書いても何の不都合も起きません。通常の関数適用 f(a) にしても、(a)f と書いても(ローカル・ルールとしては)別にかまいません。f(a) と書くのは、(広く合意はされているが)単なる偶発的習慣に過ぎません。線形代数における関数適用〈ペアリング〉については次の記事に書いてあります。

次に、足し算について考えてましょう。基数(モノの個数)の場合、a + b の左右の役割の区別は特になく、“合併としての足し算”の交換法則はほぼ明らかでしょう。強いて言えば、「最初にa個あったところに、後からb個付け足した」と「最初にb個あったところに、後からa個付け足した」のように、時間的な推移を入れると左右の区別があるかもしれません*2

序数(モノの順番)の場合、足し算の交換法則はそれほど明らかではありません。基数に比べて、より時間的・手順的な操作が伴うからです。「a番目まで勘定した後で、そこからさらにb番目まで勘定する」と「b番目まで勘定した後で、そこからさらにa番目まで勘定する」の違いです。関連することが次の記事に書いてあります。

足し算の左右の意味あい・役割が違う例に、アフィン空間の足し算 P + v があります。これは点とベクトル(移動)との足し算で、次の法則が成立します。

  • P + (v + w)= (P + v) + w
  • P + 0 = P
  • P, Q に対して、P + v = Q となるvがひとつだけ存在する

P + (v + w) と書いたとき、最初の足し算記号は「点に対して、ベクトルが移動として作用」することを表しており、二番目の足し算記号は「ベクトルの足し算」です。

足し算ではあっても、左と右の役割は違うので区別する必要があります。ただし、点を左に、ベクトル(移動)を右に書くのは恣意的な取り決めです。ベクトルの足し算が可換なので、左にベクトルを書いてもかまいません*3。アフィン空間については、次の記事に書いています。

*1:ペアリング <- | -> が双線形写像ですから。

*2:積分定数さんによるコメントのリンク先を参照

*3:非可換な群やモノイドが集合に作用しているときは、左作用と右作用は明確に区別します。

掛け算の順序問題: 「またプログラマーか!」と言われてる

KuwataさんのTwitter経由で知った https://twitter.com/genkuroki/status/1145698996033167360/ に貼ってあったスクリーンショット画像。

"AtheOS@技術者育成中(進行形)"さんが返信で言いたいことは、おそらく:

for (int j = 0; j < 5; j++) {
  for (int i = 0; i < 4; i++) {
    なにか;
  }
}
for (int j = 0; j < 4; j++) {
  for (int i = 0; i < 5; i++) {
    なにか;
  }
}

「上の2つのコードで表現される処理は違うよ」ってことでしょう。それ自体はまったく正しいことです。上記2つのコードの実行は、違った処理過程になりますし、処理結果も違うかも知れません(同じときもあります)。

しかし、それを根拠に「5×4 と 4×5 を区別するよう教育せよ」と主張しているところが、理解しがたい*1

ここで断っておきますが、「5×4 と 4×5 を区別せよ」論者に対して、懇切な説明や説得を試みる気はありません。「5×4 と 4×5 を区別せよ」を本気で主張している人を説得できる可能性は低いでしょう。説得可能だとしても、とても労力がかかるでしょう。-- 不毛。

感じたこと/思ったことをパラパラと書くだけです。

まず、“順序区別論者”に対して「交換法則があるでしょ」と言っても意味ないですね。「掛け算の順序を区別せよ」と言ってるだけで、交換法則を否定してるわけじゃないですから。

「5個/袋 × 4袋」と「4個/袋 × 5袋」は違うとか、「5km/時間 × 4時間」と「4km/時間 × 5時間」は違うとかが、背後にある状況が違うでしょ、ってことならその通りで異論はないです。むしろ、背後にある状況の違いはシッカリ認識すべきだと思います。

4回の繰り返し(内側ループ)を5回繰り返す(外側ループ)と、5回の繰り返し(内側ループ)を4回繰り返す(外側ループ)も、背後にある状況(繰り返し処理の構造と挙動)は違います -- 異論はないです

で、そのような背後にある状況の違いを、表記上も違う書き方をすると約束して守らせたいの? そこが分からん! …… (しばらく自分で考えてみた) 背後にある状況の違いを認識しているかどうかを確認するために、ローカル・ルールを設ける、って話かな? 必要なのかぁ、そんなこと。

それと、掛け算ばっかりやり玉に挙げるけど、足し算は放置でいいの? 指を折る“数え足し”を考えると、4 + 5 と 5 + 4 は違います。

  1. 最初に指を4本折る、次に指を5本折る。
  2. 最初に指を5本折る、次に指を4本折る。

この2つは、違った処理過程(手順の遂行過程)になります。足し算の順序も「徹底するようにして下さい」ってならないの?

*1:もっと正直に言うと; おまえ何考えてんだよ!? どうかしてんだろ。

データベース:: 論理の使い所は

2017年に「奥野幹也『理論から学ぶデータベース実践入門』はどこがダメなのか」という記事を書きました。そこで指摘した内容で、補足・敷衍したい事が幾つもありました(ピンク色になってます)。が、書き記す気力がなかなか湧かない。

ちゃんと書こうと思うと億劫になるので、ふと思い立ったときに、データベースと論理に関するラフなメモ書きを残すことにします。

内容:

データベースのどこに論理を使うか

奥野幹也『理論から学ぶデータベース実践入門』はどこがダメなのか // 消極的提案: 第2章を削除する」より:

僕が感じたこの本の問題点のひとつは「論理をほとんど使ってない」ことです。どうせ使わないのなら、第2章「述語論理とリレーショナルモデル」は不要です。奥野さんは、

  • 論理学に触れない正規化の解説は、でたらめだと言っても過言ではありません。

と思いっきり強調太字で書いてますが、過言です。実際に、第3章以降で、述語論理を実質的・本質的に使っている所はないです。

奥野本に限らず、「RDB集合論をベースにしている」「RDBは論理を使っている」と言うだけで、実際には集合論も論理もロクに使っていない説明をみうけます。

論理を使うのは、形式化のためです。何らかの形式体系〈formal system〉としての論理系〈logical system〉をセットアップして、その論理系の構文論と意味論により対象物や現象を記述・分析することになります。

データベースとその周辺の事物を記述・分析する場合に、どこにどのような論理を使うべきなのでしょうか? 話が発散しないように、

  • 何を論理式で記述すべきなのか?

という問題設定で考えましょう。

データベース関連で論理式〈formula〉で書きたいもの・ことは、大別すれば次のニ種類でしょう。

  1. 個体に対する条件を論理式で書きたい。
  2. 関係に対する制約を論理式で書きたい。

ここでは、二種類の使用場面を区別するために、

  1. 条件記述〈condition description/definition〉の論理式
  2. 制約記述〈constraint description/definition〉の論理式

と呼び分けることにします。

条件記述の論理式の復習

条件記述の論理式はお馴染みのものです。SQL SELECT文のWHERE句のなかに書くような論理式ですね。

これについては特段に述べることもないですが、念のためにザッと復習して、それと共に用語・記法の確認をしておきます。

集合Aに対して、Formula(A) は、Aの要素に関して記述する論理式〈formula〉の集合とします。論理式は、なんらかの言語Lで書かれるので、L-Formula(A) のように書いたほうが正確ですが、論理言語Lは前もって決っているとします。また、Aの要素を表す変数名を固定するなら、Formula(x:A) のように変数名(ここでは'x')も入れますが、変数名は何でもいいので、変数名を特定せずに、その場その場で適当な変数を使います。

例えば、Personが“世界中のあらゆる時点における人”の集合だとして、年齢20歳以上の女性を選び出すには、次のような論理式を書くことになります。

  • age(x) ≧ 20 ∧ gender(x) = FEMALE

この論理式には色々な記号が登場しました。

  • 集合Person上を走る変数記号 'x'
  • 整数値の定数記号 '20' と、性別値の定数記号 'FEMALE'
  • 関数記号 'age', 'gender'
  • 関係記号 '≧' と '='
  • 論理記号 '∧' 意味は「かつ」

これらの記号達は、事前に論理系の構文論の一部として定義され、記号が指す対象〈デノテーション〉も意味論で決めておきます。

構文論と意味論がハッキリしているのなら、{x∈Person | age(x) ≧ 20 ∧ gender(x) = FEMALE} のような集合が、集合Personの部分集合として(原理的に)確定します。もちろん、「Personとは何か?」「genderという関数はどういうアルゴリズムで与えられるか?」とかは、現実には完全決着が付かないのですが、理想化した状況で考えます。

条件記述の論理式は、古典一階述語論理をそのまま使えばいいでしょう。古典一階述語論理は、極めて安定した基盤です。素直に古典一階述語論理を使えば問題はありません。ただし、古典一階述語論理は計算の効率は芳しくないので、その点の考慮や工夫は別途必要です。

関係とは

データベースにおいて主題的に考えるべき論理式は、“関係の性質”や“関係のあいだの関係”を記述する制約記述の論理式です。制約記述の論理式に関しては色々と問題がありますが、最大の問題は、制約記述の論理式に意識が向けられてないことでしょう。ちゃんと考えないとダメだよ。

制約記述の論理式を考える上で困ったことがあります。制約記述の論理式における定数記号や変数記号は“関係”を表すのですが、「関係」という言葉の意味がクリアではないのです。

数学における(標準的な)関係概念はきわめてクリアです。が、RDBの世界の「関係〈リレーション〉」はそれとは別の意味で使われています。ここでは、「関係」は数学の標準的な意味で使い、RDBジャーゴンRDBコミュニティ特有の隠語)としての「関係」は「テーブル」と呼びます。「RDBにおける『関係』は、数学の『関係』と同じだ」といった主張は信じないほうがいいです*1

以上の方針で述べるとして; A, B を集合として、AからBへの関係〈relation from A to B〉とは、直積集合 A×B の部分集合のことです。

  • rがAからBへの関係 :⇔ r⊆A×B

AからBへの関係の全体を Rel(A, B) と書くことにします。

  • r∈Rel(A, B) :⇔ rがAからBへの関係 ⇔ r⊆A×B

集合Xのベキ集合(部分集合全体からなる集合)を Pow(X) と書くことにすると:

  • Rel(A, B) = Pow(A×B)

次の点に注意してください。

  1. A, B に何の制限もない。任意の集合でよい。
  2. r⊆A×B にも何の制限もない。任意の部分集合でよい。
  3. 関係には向きがある。AからBへの関係とBからAへの関係は違う。
  4. ここでいう関係は、二項関係であり、単項関係や三項関係は含まれない。

二項関係しか考えないことが気になる人がいるかも知れませんが、二項関係があれば、任意のn項関係や高階関係(関係のあいだの関係)をシミュレートできるので心配ありません。常に二項関係で考えることが重要です。

rがAからBへの関係(r⊆A×B)のとき、Aをrの〈domain〉、Bをrの余域〈codomain〉と呼びます。また、rがAからBへの関係であることを r:A→B rel と書くことにします。'rel'を付けているのは、関数と誤解されないようにです。

  • r:A→B rel :⇔ rがAからBへの関係 ⇔ r∈Rel(A, B) ⇔ r⊆A×B

次の書き方も使います。

  • dom(r) = A :⇔ rの域はA
  • cod(r) = B :⇔ rの余域はB

制約記述の論理式とは

AとBを集合として、AからBへの関係の全体は Rel(A, B) と書くのでした。Rel(A, B) も集合なので、Rel(A, B) に関する論理式の集合 Formula2(Rel(A, B)) を考えることができます。'Formula'2と'2'を付けたのは、先程の論理式の集合とは別な言語を使うことになるからです。

Formula2の論理式、つまり制約記述の論理式は、二階の論理式と呼ばれたりもしますが、一階、二階と分類するより、互いに関連するが使用目的が違う二つの論理言語/論理式がある状況を理解することが重要です。

例として、A = B = Person = (人の集合) として、r:Person→Person rel を「結婚している」という関係だとします。

  • (x, y)∈r :⇔ x と y は結婚している

rに含まれるペア (x, y) を「夫婦」と呼び、一番目の要素xの役割名を「夫」、二番目の要素yの役割名を「妻」とすると、

  • (x, y)∈r :⇔ (x, y) は夫婦であり、x は夫、y は妻である

rは、戸籍を管理するデータベースの一部であるテーブルとみなせます。rが持っている情報は、世界全体の情報のごく一部でもかまいません。例えば、特定の市町村の夫婦だけを記録しているとか。

制約記述とは、rのような関係が満たすべき条件を明確に書き下すことです。rとして、Person×Person の勝手な部分集合を取っていいわけではありません。

現時点(2019年6月)日本において、結婚が可能な年齢は男女で差があり(改正される予定だが)、同性婚は認められていません。

  1. 夫婦の夫は18歳以上の男性である必要がある。
  2. 夫婦の妻は16歳以上の女性である必要がある。

これは、「結婚している」あるいは「夫婦である」を表す関係 r に課せられる条件です。関係が満たすべき性質とも言えます。条件を課せられる対象が関係なので、制約という言い方で区別しのたのでした。

データベースにおいて、関係(テーブル)が「異常」だとか「矛盾している」とか言いますが、それは制約を満たしてないことです。基準となる制約を明確にしない限り、「異常」「矛盾している」は無意味です。

関係と部分集合

先に進む前に、関係についてもう少し補足しておきます。

Rel(A, B) = Pow(A×B) なので、関係は部分集合の特殊な形と言えます。しかし一方、部分集合を関係の特殊な形とみなすこともできます。この相互の言い換えはとても重要です。

1 = {0} を単元集合〈singleton set〉(要素をひとつだけ持つ集合)とします*2。集合Aのベキ集合 Pow(A) は、次のように書けます。

  • Pow(A) \stackrel{\sim}{=} Pow(1×A) = Rel(1, A)

Pow(A) と Rel(1, A) のあいだの同型(1:1の対応)は、S⊆X ←→ s⊆1×A で与えられますが、要素のレベルで書けば:

  • x∈S ⇔ (0, x)∈s

Pow(A) と Rel(1, A) は完全に同じわけではありませんが、標準的な同型があります。今後は、Pow(A) の代理に Rel(1, A) を使うことがあります。なんなら同一視する(Pow(A) = Rel(1, A) とみなす)こともあります。

さて、関係 r:A→B rel に対して、im(r), coim(r) という集合を定義します。

  • im(r) := {y∈B | (x, y)∈r となる x∈A が存在する}
  • coim(r) := {x∈X | (x, y)∈r となる y∈B が存在する}

im(r) を関係rの〈image〉、coim(r) を関係rの余像〈coimage〉と呼びます*3。定義から、im(r)⊆B, coim(r)⊆A 、つまり、im(r)∈Pow(B), coim(r)∈Pow(A) です。すぐ前に言った事情で、im(r)∈Rel(1, B), coim(r)∈Rel(1, A) ともみなします。

r:A→B rel に対して、その転置〈transpose〉rT:B→A rel を次のように定義します。

  • rT := {(y, x)∈B×A | (x, y)∈r}

転置 rT は、r の向きを逆にしたものです。像・余像は転置で入れ替わります。

  • im(rT) = coim(r)
  • coim(rT) = im(r)

coim(r)⊆dom(r), im(r)⊆cod(r) ですが、域・余域と像・余像は別物です -- 区別しましょう。

制約記述の論理式の実際

制約記述の論理式は、例えば、「結婚している」を表す関係 r:Person→Person rel が、現状の日本の法律と照らし合わせて妥当かどうかを判断する基準を与えます。この例では、法律が制約として記述されますが、学校のデータベースならば、学校の規則が制約として記述されるでしょう。例えば、「データベース基礎」を受講してない学生は「データベース実践演習」を履修登録できない、とかです。また、企業のデータベースならば、ビジネスルールが制約として記述されるでしょう。

個体(例えば人)に対する条件記述と、関係に対する制約記述を、単一の論理言語で済ませることもできるし、それが便利なこともあります。しかし、互いに関連するふたつの論理言語を準備したほうが使い勝手は良さそうです。

制約記述言語で使われる記号は次のようになります。

  • 関係の集合 Rle(A, B) 上を走る変数記号 例: 'r', 's'
  • 特定の関係を表す定数記号 例: 空な関係を表す ∅, 恒等関係を表す 'idA'
  • 関係を受け取り関係を返す演算記号/関数記号 例: '∪', '∩', 'im', 'coim', 'T'
  • 関係の性質や、関係のあいだの関係を表す記号 例: '=', '⊆'
  • 論理記号 これは条件記述言語と共通

定数記号として、条件記述の論理式を使って定義された部分集合が使えます。例えば、{x∈Person | age(x) ≧ 20 ∧ gender(x) = FEMALE} は、Rel(1, Person) に値を取る関係とみなします。前節で述べた「部分集合を関係とみなす」方法を使います。

im, coim も、関係から関係への一引数関数とみなします。集合(を表す記号)A, B に対して、

  • im:Rel(A, B)→Rel(1, B) func
  • coim:Rel(A, B)→Rel(1, A) func

というプロファイル(関数の域・余域指定)を持ちます。'func'は関数であることを明示する符丁(マーカー)です。

「結婚している」を表す関係が、法的に妥当であることを記述する制約論理式の話に戻りましょう。制約論理式を書く準備に、まずは関係定数を定義します。

  • maleOver18 := {x∈Person | age(x) ≧ 18 ∧ gender(x) = MALE}
  • femaleOver16 := {x∈Person | age(x) ≧ 16 ∧ gender(x) = FEMALE}

これは特定の集合を表しますが、Pow(Person) = Rel(1, Person) とみなせば、maleOver18, femaleOver16∈Rel(1, Person) なので、maleOver18, femaleOver16 は関係定数です。より正確に言えば、'maleOver18', 'femaleOver16' という記号が表す意味〈デノテーション〉が 1→Preson rel というプロファイルを持つ関係です。

関係定数記号 'maleOver18', 'femaleOver16'、関係を受け取り関係を返す関数記号 'im', 'coim'、関係のあいだの関係を表す記号 '⊆'、論理記号 '∧' を使って、関数変数 'r' に関する制約論理式を書けます。

  • coim(r)⊆maleOver18 ∧ im(r)⊆femaleOver16

この論理式は、「結婚している」を表す関係rに対する法的な制約を表します。

データベースのための論理系の枠組み

一階述語論理+集合論とか高階述語論理とか、強力な論理言語/論理系がありますが、データベースの話をするには強力過ぎると思います。値や個体の集合を議論領域〈domain of discourse〉とする一階述語論理、関係の集合を議論領域とする一階述語論理の組み合わせで十分でしょう。前者が条件記述の論理、後者が制約記述の論理です。

条件記述の論理式 p∈Formula(A) は、{x∈A | p} という形で Rel(1, A) の定数(特定の関係)を定義できます。この定数は、制約記述の論理式内で使えます。この意味で、条件記述の論理と制約記述の論理は無関係ではありません。

もし、制約記述の論理式を高階述語論理で解釈したいなら、α∈Formula2(Rel(A, B)) に対応する、集合 A×B 上の2階述語論理式(または集合論の論理式)も構成できます。必要があるなら、強力な論理系に埋め込んで考えてもかまいません。

論理式に出てくる記号(名前)の型(プロファイル)と、定数記号か変数記号かの区別はとても大事です。集合を表す'Person'、関係(部分集合と同一視)を表す'maleOver18', 'femaleOver18' などは定数記号です。それに対して、「結婚している」を表す関係記号'r'(もっとそれらしく'married'とかにしてもよい)は変数記号です。なぜなら、時間の流れに沿って追加・削除されるからです。

変更される関係を指す記号〈名前〉が関係変数記号であり、プログラミングにおけるプログラム変数(破壊的代入を許す変数)に相当します。関係変数記号の値を勝手気ままに換えることが出来ないことを宣言するために、制約記述の論理式が使われるのです。

関係変数rと、rに関する制約論理式α、そして変更操作mがあるとき、次のことが要求されます。

  • 変更操作mの前に、rは制約αを満たしていたならば、変更操作mの後でも、rは制約αを満たしている。

例えば、「25歳の男性と30歳の男性の婚姻届を受理する」と、「coim(r)⊆maleOver18 ∧ im(r)⊆femaleOver16」という制約論理式を満たせなくなります。

制約論理式と変更操作について明確な定式化をしないままで、「異常だ」「矛盾だ」と言ってみても曖昧で雑なことしか言えません。現状のRDBシステム実装や、純粋主義リレーショナル理論は、制約論理式と変更操作について語る枠組みとして相応しくはありません。かといって、新しい枠組みを作る必要もありません(劣化した車輪の再発明をするだけ)。既存の枠組み(論理、集合、圏など)を、歪めたり矮小化しないで、普通に使えばいいのです。

普通に使う方法や例については、次に思い立ったときに。

*1:まったくの間違いではありませんが、断り書きを付けないと正確な主張にはなりません。

*2:単元集合の要素は何でもかまいません。

*3:像を余域、余像を域と呼ぶ人もいますが、そうすると、先に定義した域・余域と区別ができなくなります。それはとても困るので、像・余像を使います。

インスティチューションと忘却関手

昨日(2019-06-06(日曜))、インスティチューション理論についてほんの少しだけ説明しました(チアガールズの説明のほうが長かった気がする)。インスティチューションについては、「キマイラ飼育記」の初期の頃からチョコチョコ触れています。

インスティチューションに関する資料として、僕が最初に思い浮かべるのはゴグエン〈Joseph Goguen〉による次のページです。

Maintained by Joseph Goguen
Last modified: Fri Jan 6 07:46:59 PST 2006

ゴグエン先生は2006年7月3日に亡くなられているので、それ以降はメンテナンスされていません。このページに目ぼしい論文へのリンクがあります。外部サイト(arXivとか)へのリンクではなくて、ローカルリンクですね。PostScript形式が多いです。

インスティチューション理論では、指標の圏Signと、指標Σに対するモデルの圏 Model[Σ] は公理的に与えられるのですが、Sign, Model[Σ] を具体的に作りたいことが多いので、作り方(の一例)を述べます。

まず、指標Σはコンピュータッド(nLab項目 computad)だとします。(適当な条件を付けた)コンピュータッドとコンピュータッド準同型からなる圏が Sign = (指標の圏) ですね。コンピュータッドΣから生成されるn-圏をΣとしましょう。モデル(指標の意味となる実体)が棲むn-圏をCとして、Model[Σ] を次のように定義します。

  • Model[Σ] = C-Model[Σ] := [Σ, C]

, C] は関手圏です。n = 2 、つまりΣは2-コンピュータッドであり、CSetを自明に2-圏とみなしたもの*1であるケースが一番よく使われる設定です。

例えば、有向グラフ(ここでは単に「グラフ」と呼ぶ)の指標は次だとします。

signature Graph :=
begin
  sorts
    V /* 頂点集合 */
    E /* 辺集合 */
  operations
    src:E→V  /* 辺の始点 */
    trg:E→V  /* 辺の終点 */
  laws
    /* 特になし */
end

指標Graphから、ソートEとオペレーション src, trg を落としてしまえば、集合の指標になります。

signature Set :=
begin
  sorts
    V
  operations

  laws

end

Set⊆Graph という包含を表す指標射を j:Set→Graph in Sign として、Model[j]:Model[Graph]→Model[Set] in CAT が対応する忘却関手です。

*1:写像のあいだのイコール関係を2-射とします。

拡張された係数を持つ微分形式の空間の書き方

共変外微分の系列」で登場したド・ラーム複体や共変外微分の系列は、i = 0, 1, 2, ... で番号付けられた*1微分形式の空間と、隣り合う番号の微分形式の空間のあいだの外微分作用素からなる系列です。微分形式の空間を大文字オメガで表すのは、割と安定した習慣です。番号は上付き添字です。つまり、Ωi ですね。Ωi の後に括弧が付くことが多いです。

  • Ωi(ナニカ)

括弧内のナニカの種類により解釈が変わるので、ややこしい。

  1. Ωi(M) -- Mは多様体
  2. Ωi(U) -- Uは開集合
  3. Ωi(V) -- Vはベクトル空間
  4. Ωi(ξ) -- ξはベクトルバンドル
  5. Ωi(F) -- Fは加群

これらはどれも略記です。では、略記じゃなくてチャンと書いたらどうなるのでしょうか?

準備

次の記事に書いてあることを手短かにまとめます。

Mはなめらかな多様体として、CM(U, R) を、Mの開集合U上で定義された、なめらかな実数値関数の集合とします。マリオス〈Anastasios Mallios〉に従って、次の書き方も使います。

  • AM(U) := CM(U, R)

AM(U) はR-ベクトル空間であり、可換環でもあるとみなします。また、開集合Uを動かすことによりM上の層を定義できます。層は特別な前層ですが、前層 AM が値をとる圏は、CRngR = (R-ベクトル空間でもある可換環の圏) です。「R-ベクトル空間でもある可換環」は短くR-可換環と呼ぶことにします。M上のR-可換環層 AM 上の加群層の圏を AM-Mod-Sh[M] と書きます。

ξはM上のベクトルバンドルだとします。ξの大域セクションの全体を ΓM(ξ) と書き、局所セクションの空間は次のように定義します。

  • ΓM(U, ξ) := ΓU(ξ|U)

ΓM(U, ξ) はRベクトル空間として扱い、R-可換環 AM(U) 上の加群とみなします。Uを動かした ΓM(-, ξ) はM上の層となり、圏 AM-Mod-Sh[M] の対象になります。

M上のベクトルバンドルの圏を Vect-Bdl[X] とすると、ΓM は、ξ \mapsto ΓM(-, ξ) という対応になり、ベクトルバンドル射を加群層の射に対応付けるので、ΓM:Vect-Bdl[X]→AM-Mod-Sh[M] という関手になります。

記号'\otimesM'は、2つのベクトルバンドルの“M上のテンソル積”の意味で使います。'\otimesM'は、圏 Vect-Bdl[X] における演算です。一方、記号'\otimesAM'は、2つの加群層の“可換環層 AM に対するテンソル積”の意味で使います。'\otimesAM'は、圏 AM-Mod-Sh[M] における演算です。

略記の解釈

任意のベクトル空間Vに対して、Triv(M, V) は、M上のVをファイバーとする自明ベクトルバンドルのことだとします。

  • Triv(M, V) = (M×V, M, V, π1)

T*M は、Mの余接ベクトルバンドル、Λiξ は、ベクトルバンドルξを外積の意味でi乗したベクトルバンドルです。

さて、略記を解釈しましょう。

  1. Ωi(M) は、ΓM(M, ΛiT*M) の略記。
  2. Ωi(U) は、ΓM(U, ΛiT*M) の略記。
  3. Ωi(V) は、ΓM(M, Triv(M, V) \otimesM ΛiT*M) の略記。
  4. Ωi(ξ) は、ΓM(M, ξ \otimesM ΛiT*M) の略記。
  5. Ωi(F) は、ΓM(M, ΛiT*M) \otimesAM F の略記。

このなかで、1番と2番は通常の微分形式の空間ですが、3, 4, 5番はそれぞれ、ベクトル空間、ベクトルバンドル加群層へと係数域が拡張されています。拡張された係数を持つ微分形式は、接続〈共変微分〉の議論などで出てきます。

ΩiM(U) := ΓM(U, ΛiT*M) とするならば:

  1. Ωi(M) は、ΩiM(M) の略記。
  2. Ωi(U) は、ΩiM(U) の略記。
  3. Ωi(V) は、ΩiM(M) \otimesAM ΓM(M, Triv(M, V)) の略記。
  4. Ωi(ξ) は、ΩiM(M) \otimesAM ΓM(M, ξ) の略記。
  5. Ωi(F) は、 ΩiM(M) \otimesAM F の略記。

他にも、略記の仕方はいくらでもあるでしょうが、ΓM(開集合, ベクトルバンドル) と \otimesM, \otimesAN で書き下してみると、意味がハッキリするでしょう。

*1:ときに、負の番号も使うことがあります。

ゲージ変換の解釈

主バンドルの基本的なこと (1/2)」で述べたように、マーシュ〈Adam Marsh〉の論説・書籍を読み始めました。

障害というか、困難を感じる点は、物理と微分幾何の概念・用語の対応関係がよく分からないことです。物理的概念そのものは「どうせ分からんからいいや」とハナから諦めているのですが、物理起源の言葉がよく出現するので、それを微分幾何的に解釈する必要はあります。

この記事では、「ゲージ変換」という言葉の解釈を試みてみます。

内容:

バンドルの圏

主バンドルの基本的なこと (1/2) // 特定の空間上のファイバーバンドルの圏」、「主バンドルの基本的なこと (1/2) // 底空間を特定しないファイバーバンドルの圏」の復習をしましょう。Man = Man(∞) = (なめらかな多様体となめらかな写像の圏) をベースに考えます。ファイバーバンドルの全空間、底空間、典型ファイバーはすべてManの対象であり、射影はManの射です。ファイバーバンドルを単にバンドルともいいます。

ファイバーバンドルに、構造群〈structure group〉と呼ばれる群を一緒に考えることが多いのですが、ここでは構造群を考えません。ちなみに、構造群とゲージ群〈gauge group〉は完全に同義語なので、今言ったことを言い換えると「ゲージ群を考えません」なので、ゲージ群は一切出てきません

すべてのバンドルとバンドル射(ファイバーバンドルの準同型写像)の全体からなる圏をBundleとします。Bundleの対象は、ξ = (Eξ, Bξ, Fξ, πξ) のように書きます。ξからηへのBundleの射は、f:Eξ→Eη, φ:Bξ→Bη in Man のペア (f, φ) で、f;πη = πξ;φ を満たすものでした。これを、(f, φ):ξ→η in Bundle と書きます。

ξ, η∈|Bundle| に対して、ホムセット Bundle(ξ, η) は、バンドル射 (f, φ) からなりますが、底空間の写像φを特定の写像 ψ:Bξ→Bη に固定したバンドル射の全体を Bundle(ξ, η)[ψ] と書きます。

  • Bundle(ξ, η)[ψ] := {(f, φ)∈Bundle(ξ, η) | φ = ψ : Bξ→Bη in Man}

多様体X(Manの対象)をひとつ選んで、圏Bdl[X]を次のように定義します。

  • |Bdl[X]| := {ξ∈|Bundle| | Bξ = X}
  • Bdl[X](ξ, η) := Bundle(ξ, η)[idX]

多様体Xごとに圏Bdl[X]を作ることができます。各Bdl[X]はBundleの部分圏になります。

自明バンドルの圏

前節で、すべてのバンドルからなる圏Bundleと、X∈|Man|ごとの圏Bdl[X]を定義しました。バンドルのなかでも特に簡単なバンドルとして自明バンドルがあります。自明バンドルだけからなる圏を定義しましょう。

X, F∈|Man| に対して、バンドル (X×F, X, F, π1) を定義できます。ここで、π1は直積の第一射影です。この形のバンドルを、自明バンドル〈trivial {fiber}? bundle〉、直積バンドル〈{direct}? product {fiber}? bundle〉などと呼びます。

自明バンドルもバンドルなので、自明バンドルからの/自明バンドルへのバンドル射は普通に考えることができます。したがって、自明バンドルを対象とするBundleの充満部分圏TrivBundleを考えることができます。

同様に、Bdl[X]内の自明バンドルとバンドル射(底空間では恒等射)だけからなるBdl[X]の充満部分圏TrivBdl[X]も考えることができます。

これで、以下のような圏を定義できました。

  • Bundle
  • Xごとに Bdl[X]
  • TrivBundle
  • Xごとに TrivBdl[X]

同型射の圏と自己同型射の圏

この節は、圏の一般論です。Cを任意の圏とします。

Cの同型射〈可逆射 | isomorphism〉だけからなる部分圏を IsoC 、または Iso_C と書きます。念のため、Iso_C の対象類とホムセットを書くと:

  • |Iso_C| := |C|
  • Iso_C(A, B) := {f∈C(A, B) | fは同型射}

A, B が対象として同型でないときは、Iso_C(A, B) = 空集合 となることに注意してください。

Cの自己同型射〈automorphism〉だけからなる部分圏を AutC 、または Aut_C と書きます。念のため、Aut_C の対象類とホムセットを書くと:

  • |Aut_C| := |C|
  • Aut_C(A, B) := (A = B ならば {f∈C(A, A) | fは同型射}、そうでないなら空集合)

ホムセット Aut_C(A, B) は、A = B のときしか実質的な意味がないので、Aut_C(A) と書きます。

すべての射が可逆である圏を亜群〈groupoind〉と呼びます。Iso_C も Aut_C も亜群となります。対象Aに対して、Iso_C(A, A) 、 Aut_C(A, A) = Aut_C(A) は群になります。亜群 Aut_C は、対象ごとにひとつの群 Aut_C(A) があるだけなので、単に群の寄せ集めです。

ゲージ変換とゲージ変換群

「ゲージ変換」という言葉の語源やら物理的解釈やらは一切無視して、単に「どんな意味で使われているのか」だけに注目すると、

  • バンドルの圏の同型射または自己同型射をゲージ変換と呼ぶ

だと思われます。

「バンドルの圏」は何種類かあるので、表にまとめてみると:

バンドルの圏 同型射の圏 自己同型射の圏
Bundle Iso_Bundle Aut_Bundle
Bdl{X] Iso_Bdl[X] Aut_Bdl[X]
TrivBundle Iso_TrivBundle Aut_TrivBundle
TrivBdl{X] Iso_TrivBdl[X] Aut_TrivBdl[X]

この表で、同型射/自己同型射の圏が8種類出てきますが、これらの圏(亜群になっている)の射をゲージ変換〈gauge {transform | transformation}〉と呼んでいるようです。どの圏の射なのかは文脈によります。いずれの場合でも、ゲージ変換は可逆です。

ゲージ変換の集まりで群になっているものを、たぶんゲージ群と呼ぶのでしょうが、どうも次の2つのケースがありそうです。

1. ゲージ変換からなる亜群(群ではない)をゲージ変換群と呼ぶ。
2. ゲージ変換からなる群(ほんとに群)をゲージ変換群と呼ぶ。

同型射の圏 Iso_Bdl[X] をゲージ変換群と呼ぶことは、一番目の用法の例になります。ホムセットは Aut_TrivBdl[X](ξ) をゲージ変換群と呼ぶことは、ニ番目の用法の例になります。

混乱を避けるには、ゲージ変換からなる亜群はゲージ変換亜群〈gauge transformation groupoid〉と呼び、ほんとに群のときだけゲージ変換群〈gauge transformation group〉と呼ぶほうがいいでしょう。

最初に注意したように、今までの話でゲージ群=構造群は一切出てきてません。ということは、ゲージ群とゲージ変換群は別物だと分かります。ゲージ群を考えるならば、それはゲージ変換群と関係しますが、ゲージ群なしでもゲージ変換/ゲージ変換亜群/ゲージ変換群を定義できます。

共変外微分の系列

主バンドルの基本的なこと (1/2)」で、ファイバーバンドルとそのセクションの定義をしたので、それを使って共変外微分の系列を導入できますね。

  •  \nabla^i_U : \Omega^i_M(U, \xi) \rightarrow \Omega^{i+1}_M(U, \xi)

という記法の意味を説明します。

内容:

ファイバーバンドルのセクションの復習

この節は「主バンドルの基本的なこと (1/2)」の要約です。なめらかな多様体の圏 Man = Man(∞) で話をします。

ξ = (E, B, F, π) をファイバーバンドルとします。s:B→E という(なめらかな)写像で、s;π = idB を満たすものが、ξの大域セクション〈global section〉でした。ξの大域セクションの全体を Γ(ξ) と書きます。開集合 U⊆B の上で定義されたセクションは、ξをUに制限したファイバーバンドル ξ|U = (E|U, U, F, π|U) の大域セクションになります。

  • Γ(U, ξ) := Γ(ξ|U)

Γ(U, ξ) の要素は、ξの局所セクション〈local section〉と呼びます。

セクションの集合に、ファイバーバンドルの底空間を添えて、ΓB(ξ), ΓB(U, ξ) とも書きます。開集合Uを動かした対応 U  \mapsto ΓB(U, ξ) は、B上の層になります。

今回使うわけではありませんが; ファイバーバンドルξも動かすと、ξ  \mapsto ΓB(-, ξ) という対応は、“B上のファイバーバンドルの圏”から“B上の層の圏”への関手 Bdl[B]→Sh[B] になります(「層に関してちょっと」を参照)。

ド・ラーム複体

なめらかな多様体Mに対して、そのド・ラーム複体は次の系列です。

  • Ω0M -(d0)→ Ω1M -(d1)→ Ω2M -(d2)→ ...

この系列が複体〈complex〉だとは、di;di+1 = di+1\circdi = 0 が成立することです。

各ΩiM は次のように定義されます。

  • Ω0M := C(M) = C(M, R) = (M上で定義されたなめらかな実数値関数の可換環)
  • Ω1M := ΓM(T*M) = (M上の1次微分形式のベクトル空間)
  • Ω2M := ΓM(T*M ∧M T*M) = (M上の2次微分形式のベクトル空間)
  • 以下同様

T*M はMの余接バンドルで、T*M ∧M T*M は、余接バンドルを(自分自身と)外積したベクトルバンドルです。'∧M'は、ファイバーごとに外積を作って、それらを寄せ集めることを意味します。

すべての ΩiMR上のベクトル空間ですが、Ω0M可換環で、ΩiM 達は可換環 Ω0M 上の加群と考えます。

開集合 U⊆M に対して、関数や微分形式をU上に制限して考えることにより、ΩiM(U) を定義できます。そして、U上に制限したド・ラーム複体も定義できます。

  • Ω0M(U) -(d0U)→ Ω1M(U) -(d1U)→ Ω2M(U) -(d2U)→ ...

Ω0M(-) はM上の可換環の層、ΩiM(-) はΩ0M(-)上の加群の層になります。ド・ラーム複体は、加群の層の圏のなかの複体とも、複体の圏に値をとる層(複体の層)ともみなせます。

ド・ラーム複体は、ド・ラーム・コホモロジーを定義する手段であるだけではなくて、それ自身で(コホモロジーを取らなくても)多様体Mに備わった計算システムと捉えることができます。ド・ラーム複体をベースに、より複雑な計算システムを構成することができます。後で述べる共変外微分系列がその例です。

共変微分の復習

共変微分については、次の記事で触れています。

が、ザッと復習しておきます。

ξを多様体M上のベクトルバンドルとします。セクションの空間 ΓM(ξ) はR-ベクトル空間であり、可換環 Ω0M 上の加群にもなっています。これらの構造を前提に、ξの共変微分と呼ばれる作用素を定義できます。

共変微分〈covariant derivative〉∇は、次の形の作用素です。

  • ∇ : ΓM(ξ) → ΓM(ξ)\otimesΩ1M

ここで、テンソル積の記号'\otimes'は、可換環Ω0M上の加群に対するテンソル積です。ベクトルバンドルのファイバーごとのテンソル積を'\otimesM'と書くなら、次の同型があります。

  • ΓM(ξ)\otimesΩ1M = ΓM(ξ)\otimesΓM(T*M) \stackrel{\sim}{=} ΓM\otimesM T*M)

これは、セクションをとる関手が、ベクトルバンドルテンソル積を加群テンソル積に写すことを意味しています。

共変微分∇が満たすべき法則は:

  1. ∇は、R-線形写像である。
  2. ∇は、ライプニッツの法則を満たす。
    ∇(sf) = (∇s)f + s\otimesdf

関数fは右から掛けていますが、ちゃんと統一性があれば、左右どっちでもいいです。

共変微分を備えたベクトルバンドルvector bundle with covariant derivative〉は、M上の微積分の舞台を提供します。さらに、局所的計算を可能とするために、層を導入しておきます。

開集合 U⊆M ごとに、次の共変微分を考えます。

  • U : ΓM(U, ξ) → ΓM(U, ξ)\otimesΩ1M(U)

Mのすべての開集合に渡ってこれらを総合すると、ベクトル空間かつ加群の層のあいだのライプニッツ射ができ上がります。これもまたξの共変微分と呼びます。

共変外微分とその系列

多様体M上のベクトルバンドルξの共変微分∇に基づいて、ド・ラーム複体と類似の系列を構成します。ただし、∇ベースの系列が複体になるとは限りません。むしろ、複体にならないことに意味があったりします。

最初から層の形で ΩiM(U, ξ) (i = 0, 1, 2, ...)を導入します。UはMの開集合です。

  • Ω0M(U, ξ) := ΓM(U, ξ)
  • Ω1M(U, ξ) := Ω0M(U, ξ)\otimesΩ1M(U)
  • Ω2M(U, ξ) := Ω0M(U, ξ)\otimesΩ2M(U)
  • 以下同様

'\otimes'は、可換環Ω0M(U)に関する加群テンソル積です。ベクトルバンドルテンソル積(と外積)を使うなら:

  • Ω0M(U, ξ) := ΓM(U, ξ)
  • Ω1M(U, ξ) := ΓM(U, ξ \otimesM T*M)
  • Ω2M(U, ξ) := ΓM(U, ξ \otimesM (T*M ∧M T*M))
  • 以下同様

ベクトルバンドルで見ると、余接バンドル T*M のk重の外積 ΛkMT*M に、ξをテンソル積したバンドルを作ることになります。セクションを取ると、微分形式の値を実数からξに拡張したものになります。

ΩiM(U, ξ) (i = 0, 1, 2, ...)のあいだを繋ぐ微分作用素共変外微分〈covariant exterior derivative〉 ∇iU です。まず、∇0U : Ω0M(U, ξ) → Ω1M(U, ξ) は、∇U そのものだとします。その他の ∇iU : ΩiM(U, ξ) → Ωi+1M(U, ξ) は、次の基本的な定義を拡張して計算できます。

  • iU(s\otimesω) = (∇Us)\otimesω + (-1)is\otimes(diUω)

ここで、diU は通常の外微分(ド・ラーム複体に現れる外微分)です。

以上で、ベクトルバンドルξと共変微分∇に伴う共変外微分〈外共変微分〉の系列が作れました。座標(チャート/アトラス)を使わないで定義したので、計算の労力はかかりませんでしたが、具体的な座標により表示するとなるとだいぶゴチャゴチャした感じになります。

バンドルの共変微分とバンドルの接続は、同じ概念の違った表現方法です。共変外微分の系列が複体にならない度合い、つまり ∇0;∇1 = ∇1\circ0 は、バンドルの曲率(物理ではフィールドストレングス)と呼ばれる重要な量になります。共変外微分系列を導入したので、曲率の議論をする準備は出来ました。