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

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

2018-08-21 (火)

『圏論による量子計算と論理』はエキサイティングだ (1/2)

| 13:03 | 『圏論による量子計算と論理』はエキサイティングだ (1/2)を含むブックマーク

共立出版の大谷さんに書籍『圏論による量子計算と論理』を送っていただきました。ありがとうございます。ざっと“眺めた”(一部分は“読んだ”)ので、感想だのナニヤラを記します。2回に分けた前編(1/2)です。今回は本の内容について、次回は内容以外について述べます。

内容:

  1. 読むけど読まない人
  2. どんな本なの
  3. 第2章と第3章:圏論的線形代数と埋め込みの諸相
  4. 僕たちの2008-2009年
  5. 第4章:量子ハイパードクトリン
  6. 第5章:トポスの中と外
  7. 具象への回帰

この記事の節タイトルは、『圏論による量子計算と論理』の章タイトルではありません。

読むけど読まない人

『圏論による量子計算と論理』がどんな本かすぐ知りたい人次節に飛べ → ; この節は私的雑談。

僕は、割と本を読むほうかと思うのですが、本に関するブログ記事はほとんど書きません。いま、「本を読む」と言いましたが、実際はチャンと読むことなんてなくて、「本の一部を適宜利用する」だけです。なので、本についてナニゴトかを書くのはおこがましい、著者・関係者に失礼かな、と感じるのです。このブログ始めて14年目になりますが、書評(つうか読書感想文)記事は5回しか書いてません。

  1. 書評:理工系のための トポロジー・圏論・微分幾何 2007年
  2. 清水明著『量子論の基礎』はいい本だ 2008年
  3. 山本陽平さんの『Webを支える技術』はWeb技術者に必携だな 2010年
  4. 『抽象によるソフトウェア設計』とAlloy、第一印象報告 2011年
  5. 渡辺竜・著『レスポンシブWebデザイン』はとても良い本だ 2013年

理工系のための トポロジー・圏論・微分幾何』は第5章以外は斜め読みです。それでも随分と読んだほうで、ジョニー(id:hiroki_f)に推奨されて買った本『量子論の基礎』については、

まだ読んでないけど、これはいい本です。
[...sinip...]
A5判(20.8x14.8x1.8cm)288(内容264)ページは非常に扱いやすいサイズです。もちろん、ハードカバーなんてバカなことはなくて、ソフトカバーです。ソフトカバーのなかでもほんとにソフトな作りで取り回しが楽。いいですねぇ。カバーに光沢加工がしてあって撥水性があるので、今日みたいな雨の日に少し濡らしたくらいでは大丈夫。コーヒーをこぼしたりしても少量なら問題ないでしょう。

本の形状・形態しか書いてません(なんせ読んでないから)。僕にとって形状・形態は大きな評価ポイントなんです。デジタルデータに比べて紙の書籍の際立った特徴は「物体である」ことです。物体としての機能性は気になるところです。

Webを支える技術』に関しても、

『Webを支える技術』は版型もコンパクトだし、取り扱いがとても楽です。付録・索引も充実しているので、ハンドブック的に、いつでも手元に置きたい本です。

付録・索引の充実 -- これはホントに重要。紙の本の困るところは、ハイパーリンクや文字列検索が使えないことです。それを補う機能としての索引は必須! 索引がない(あるいは、ないに等しいほど貧弱な)専門書は買うに値しないと思っています。

抽象によるソフトウェア設計』に関する記事を書いたとき、本は「序章4ページ + 付録2.5ページ」しかマトモに読んでなくて、ソフトウェアの使用記が大部分でした。ここでも僕の評価ポイントを繰り返しています。

  • 紙の本は、モノとしての形態がすごく気になるのですが、その点では使い勝手がいいです。
  • 付録が便利でとても助かります(つーか、主に付録を読んでるんですが)。
  • 訳語一覧があるのも好感が持てます。欲をいえば、もう少し語数が多いと良かったかな。例えば、「基本型」は訳語一覧には載ってません; 「基本」と訳す言葉に base, basic, primitive, atomic, ground, fundamental とかありますからね、モトを知りたい。

レスポンシブWebデザイン』は、全320ページ中176ページ、つまり半分以上読んだので得意になって記事を書きました。門外漢で飽きっぽい僕でも半分までは読める本て素晴らしいな、ってことですね。

毎度こんな感じなんですが、今回の『圏論による量子計算と論理』も、第4章から読み始めて、必要に応じて前の章を参照し、第5章で「はぁー、むずかしいな、これ」とかひとりごつってるのが現時点の状況(イマココ)です。

どんな本なの

タイトル「圏論による量子計算と論理」が、本書の内容を端的に表していると思います。

コンピュータは電子機器なので、根源的な自然法則としての量子物理に強く依存した製造物です。しかし、プログラミングのレベルで量子物理を意識することはなかったですよね; 今までは。今後、量子物理特有な現象をプログラミングのレベルで利用するとなると、「プログラマにとっての量子物理 = 量子計算論」が必要になります。計算がどのように為されるかを云々するとき、当然に論理を使います。今までは、計算の論理*1は古典論理(または直観主義論理)で十分でしたが、量子現象/量子計算に関わる論理は古典論理とはどうも異なるようです。量子を扱うための非古典論理が必要なんでしょう。

クリス・ヒューネン〈Chris Heunen〉のこの本は、量子計算論とそれに関わる論理を基礎的〈foundational〉な立場から解説しています。具体的な量子アルゴリズムや応用事例は少数しか載ってません。紙幅のほとんどを基礎に費やしているからです。基礎的であることは易しいことを意味しません。実際、この本はだいぶ難しい本だと思います。だけど、(適宜他の文献なども参照しながら)読み進めるなら、とてもシッカリとした認識と見識を得られます。

チャンと理解するには物理の知識が必要なんでしょうが、僕みたいに物理に無知な人でもなんとか読み進められます。著者はセフルコンティンド〈自己充足的〉になるように努力してますが、後ろのほう(第5章)は、関数解析やC*〈C-star algebra〉の知識が若干要るので、この本だけではキビシイかも。僕は、『作用素環入門 I』(asin:4007305943*2を引っ張り出してきました。

本書『圏論による量子計算と論理』の構成は次のようです。

  • 第1章 はじめに (10p)
  • 第2章 テンソル積と双積 (44p)
  • 第3章 ダガー圏 (64p)
  • 第4章 ダガー核論理 (52p)
  • 第5章 ボーア化 (52p)

「はじめに」は導入と概要紹介です。2,3章が線形代数、4,5章が論理の話ですね。第2章は内積を考えない線形代数、第3章は内積付きの線形代数です。第4章は、ベクトル空間の部分空間束を論理的対象と考えての述語論理、第5章は状態空間と観測量を扱う論理です。こう書くと、オーソドックスなコースのように思えるかも知れませんが、いやいやっ、並の教科書とは違いまっせ、徹底的に圏論的〈カテゴリカル〉で公理的です。圏論的線形代数と圏論的論理のテキストなのです。次節以降でもう少し詳しく内容を紹介しますけどね。

時間がない人は、最後の節に飛べ →

以下この記事では、『圏論による量子計算と論理』を「ヒューネン本」とも呼びます。翻訳日本語本であることを強調したいときは「ヒューネン/川辺本」とします。僕が通常使っている用語とヒューネン/川辺本の用語が違うときは、「檜山の用語《ヒューネン/川辺本の用語》」という書き方で表すことにします。

第2章と第3章:圏論的線形代数と埋め込みの諸相

圏論的線形代数も圏論的論理も、僕自身が割と長い期間興味を持ち続けてきたトピックなので、ヒューネン本の直接的内容だけではなくて、周辺事項(「余計な事」とも言う)も色々書きます。本書に刺激されて、10年ほど前の記憶や興味が呼び覚まされました。それらをもう一度掘り起こそうという意図もあります。なので、檜山の記憶と連想の話がだいぶ入ります、あしからず。

本書の第2章「テンソル積と双積」と第3章「ダガー圏」は圏論的線形代数の解説です。圏論的線形代数というと、アーベル圏を思い浮かべる人が多いでしょう。アーベル圏は、圏論的・公理的に定義される圏(の種別)ですが、とある環(非可換かも知れない)の上の加群の圏だと思っていいものです。なぜ「思っていい」のでしょうか? 「抽象的なアーベル圏を、具体的な加群の圏に埋め込めるよ」と主張するフレイド/ミッチェルの埋め込み定理〈Freyd-Mitchell embedding theorem〉があります。この埋め込み定理が「思っていい」根拠であり、アーベル圏の理論の中核的な結果です。

ヒューネン本はアーベル圏を扱っているわけではありません。ヒューネンは、扱っている圏にカチッとした名前を与えてないのですが*3、「有限双積をもつ圏」*4と「有限双積をもつモノイダル圏*5」が(内積がない)線形代数で扱う圏です。このブログ内ではそれぞれ、半加法圏テンソル半加法圏と呼んでいた圏です。第3章では、ダガー圏とその変種が登場します。

アーベル圏が最初から足し算・引き算を仮定しているのに対して、有限双積をもつ圏は足し算だけを仮定します。また、アーベル圏はホモロジー代数を意識していて、完全列がやたらに出てくるのですが、ヒューネン本では完全列/完全性に注目してません。今言った「引き算」と「完全列」は、僕がアーベル圏を敬遠する理由でした。計算科学への応用上は邪魔になる前提「引き算」「完全列」を外している点で、ヒューネンが扱っている圏論的線形代数は、より広範で実務的なものだと感じます。

とまー、アーベル圏とはだいぶ違った様相の“線形代数の圏”をヒューネンは扱っているのですが、大枠において、あるいは精神においてはフレイド/ミッチェル・スタイルを踏襲しています。つまり、抽象的に与えられた圏を具体的な圏に埋め込むことにより、抽象的な定義の妥当性と、いざとなったら集合・写像として扱える安心感を担保しています。

埋め込みに使うテクニックをザッと見ておきましょう。

CのホムセットをC(X, Y)と書きます。A∈|C| を固定して、C(A, -)を考えると、CSet という共変関手ができます。このC(A, -)を、Aによる共変主表現〈covariant principal representation〉*6または共変ホム関手〈covariant hom-functor〉と呼びます。C(-, A)ならば、共変が反変に変わります。(共変または反変)主表現と自然同型な(共変または反変)関手は表現可能関手〈representable functor〉で、Aがその表現対象〈representing object〉です。

対象Aによる共変主表現をA、反変主表現をAと僕は書きます。下付き・上付きの米〈コメ〉は米田の星です(「困った時の米田頼み、ご利益ツールズ // ラムダ記法と米田の星」参照)。固定していたAを動かした X|→X米田埋め込み〈Yoneda embedding〉

  • (-):C→[Cop, Set] ([-, -] は関手圏)

を与えます。そして、X|→X余米田埋め込み〈coYoneda embedding〉

  • (-):Cop→[C, Set] ([-, -] は関手圏)

を与えます。なので、固定したAに対する A, A は、(余)米田埋め込みの一点(特定対象)での値となります。

フレイド/ミッチェル・スタイルの埋め込みは、余米田埋め込み (-):Cop→[C, Set] の一点Pでの値Pですが、Pをうまく選んで P∈Obj([C, Set]) が埋め込み(充満忠実関手) P:CSet になるようにします。このとき、圏Cが備えている圏論的構造を利用して、Cの各ホムセットに集合論的構造を載せ*7、Pの値の圏を単なるSetではない圏、例えば左R-加群の圏RModに仕立てて、P:CRMod とするのです。

フレイド/ミッチェル・スタイルの埋め込みを構成する要点をまとめるなら:

  • Cの各ホムセットに構造を載せる、つまり豊饒化《豊穣化》して、主表現関手〈ホム関手〉が値をとる圏をSetからSet上の具象圏〈concrete category〉へと持ち上げる。線形代数の場合は、Set上の具象圏として、環R上の左加群の圏RModをとる(左右はどうでもいいけど)。
  • Cの対象Pをうまく選んで、Pによる主表現関手〈ホム関手〉 P:CRMod が充満忠実関手になるようにする。充満忠実じゃなくても役に立つこともある。線形代数の場合は、Pとして射影分離子《射影的生成元》をとる。

米田埋め込みの場合は、全ての主表現〈ホム関手〉を総動員して、全体として“関手圏(前層の圏)への埋め込み”を構成します。個々の対象(いわば個人)の資質・能力に頼らず社会全体として埋め込みというミッションを遂行するのです。一方のフレイド/ミッチェル・スタイル埋め込みでは、極めて有能な代表者(対象)を一人(ひとつ)だけ選出し、その特定対象の資質・能力に依拠して“構造を持つ集合の圏への埋め込み”を構成します。当然に、有能な代表者の存在がキモになります。

「米田埋め込み vs. フレイド/ミッチェル・スタイル埋め込み」における「凡庸な民衆の総体 vs. 有能な一個人」の対比は、なんか面白なと思います(そこに余計な意味を見い出そうとしてはいけない!が)。有能な一個人(特別な対象)の存在を保証しているのは、圏全体が持つ圏論的構造です。その圏論的構造とは、双積や(双積とは別な)テンソル積、ダガー構造などです。

さて、ヒューネン本の第2章「テンソル積と双積」、第3章「ダガー圏」の読み方ですが; 章内で導入した様々な圏(有限双積をもつ圏/有限双積をもつ(対称)モノイダル圏/有限双積をもつ正則圏/コンパクト閉圏/前ヒルベルト圏/ヒルベルト圏)に対してフレイド/ミッチェル・スタイルの埋め込みを構成するストーリーだと思うと流れを見失わずに楽しく読めると思います。

抽象的圏の埋め込み先である具象圏は、加群*8の圏ですが、加群にはスカラー系(スカラーモノイド/スカラー半環/スカラー環/スカラー体)が付随します。最初にスカラー系を決めないと加群を作れないので、圏全体からスカラー系を絞り出す操作がまず必要です。圏のマクロ構造から(圏に比べると)ミクロなスカラー系が析出される様はなかなかに興味深く、ダガー構造に種々の条件を付けると、スカラー系が複素数体の部分体にまで特殊化されたりします。初見では茫漠とした圏から、カッキリしたお馴染みの構造が現出するのは驚きです。そう(so)、エキサイティング。

僕たちの2008-2009年

ヒューネン本では、圏論的線形代数だけでなく圏論的論理も解説されています。その部分(後半)を紹介する前に、時間を遡った話をします。回り道をしたくない人次節に飛べ → ; この節は私的雑談。

ヒューネン本は、もともとはヒューネンの学位論文で、2009年に出版されています。その1年前、僕たち(檜山、たけをさん(id:bonotake)、酒井さん(id:msakai)、ジョニー(id:hiroki_f)、nucさん(id:nuc))は、「圏論と量子」の話題でちょいと盛り上がっていました。

ちょうど10年前のことです。手分けして論文を読んだり、ブログエントリーを上げたりしています。

この頃読もうとしていた著者は、アブラムスキー〈Samson Abramsky〉、クック〈Bob Coecke〉、バヴロヴィック(Dusko Pavlovic)、アルテンキルヒ〈Thorsten Altenkirch〉、セリンガー〈Peter Selinger〉あたりかな。当時(今でもだけど)、圏論と量子に関して包括的イメージを持つことは出来ず、摘み食いして面白がっていただけでした。量子テレポーテーションを中心とするアワブームは、お盆前後の3週間ほどで沈静化しました(「飽きた」とも言う)。

でも、一年後の8月にも、関連記事は書いてますよ。うっすらと興味は続いていたのです。

2008年以前も(以後も)、ボブ・クックのお絵描き量子論はちょくちょく紹介してます。

ヒューネン本の主題のひとつであるダガー・コンパクト閉圏について言えば、当初アブラムスキー/クックは強コンパクト閉圏〈strongly compact closed category〉と呼んでいて、2005年にセリンガーがダガー・コンパクト閉圏へと改名したものです*9。古ーい短い記事「Dagger compact closed category」でそのことに言及しています。

話は変わって2009年春に、ジョニーが『層・圏・トポス』の勉強会を始めました。老婆心から書いた記事が、

竹内さんはゲーデルも一目置いたほどの世界的な論理学者(ロジシャン)ですが、その書きっぷりは粗っぽくてエエカゲンなところがあります(そこがまた素敵だったりするのですが)。

竹内本をテキストに使うことに僕は賛同しない*10のですが、ヒューネン本、特に第5章に対する副読本として『層・圏・トポス』はいいかも知れない、と思ったりします(が、上記記事の注意事項を読んでね)。あるいは逆に、事例が少ない竹内本を、ヒューネン本第5章のクリプキ・トポスを想定しながら読むのも面白いかも(特におすすめはしませんが)。

第4章:量子ハイパードクトリン

ヒューネン本の第2章と第3章は線形代数としてひと続きのものです。第4章「ダガー核論理」は線形代数を使った論理なので、第2章・第3章と関連しています。伝統的な量子論理*11は、ヒルベルト空間の閉部分空間の束、あるいは射影作用素の束を調べるものですが、第4章「ダガー核論理」は、同じ趣旨で“論理”を展開していると言っていいでしょう。

集合圏におけるXのベキ集合Pow(X)に相当するものとして、ダガー核圏における核部分対象〈kernel subobject〉の集合KSub(X)というものを採用します。KSub(X)に論理演算を入れて、論理代数と捉えれば、(第4節のタイトルである)X上のダガー核論理ができあがります。ここまでだと命題論理の話であって、述語論理の限量子《量化子》が出てきません。

限量子の導入方法としては、ベースの圏のなかで射 f:X→Y を考えて、fによる論理代数の引き戻し f*:KSub(Y)→KSub(X) を考える方法があります。f*は議論域〈domains of discourse〉を取り替える操作、あるいは論理式への代入操作をシミュレートしています。そして限量子は、f*の随伴として導入します。限量子を導入するこの手法については次の記事で説明しています。

上記記事では名前を出さなかったのですが、インデックス付き圏《添字付き圏》と随伴を使うフレームワークハイパードクトリン〈hyperdoctrine〉と呼びます。ハイパードクトリンはローヴェア〈William Lawvere〉が発案・命名したようですが、政治か宗教のようなネーミングで、どうも使うのが憚られます。

ともかくも、ダガー核論理に対してハイパードクトリンの手法を組み合わせて、ヒューネンは量子論理の限量子を構成しています。ただし、存在限量子だけで全称限量子は存在しないようです。ヒューネンが記述している量子述語論理が、伝統的な量子論理からどれほど進化しているのか? 僕にはハカリかねるのですが、ハイパードクトリン・ベースの定式化により、古典論理などの他の論理との連絡が良くなっていると思います。

第5章:トポスの中と外

ヒューネン本のなかでもっとも面白そう、だけどもっとも難しそうなのが第5章「ボーア化」です。物理的な課題に対して、トポスと作用素環を組み合わせてアプローチしているようです。第5章「ボーア化」の前半はトポスのミニコースで、ここはなんとか読めるのですが、後半、本書の最後の32ページが僕には難物。物理的な背景や動機をなーんも理解してませんからね。

ふと思い起こすのは、本書でも名前が出ているクリス・イシャム〈Chris J. Isham〉が、量子物理にトポスを使っているという噂を聞いたことです。それに対して「スジ悪で脈がない」という意見もどこかで目にした記憶があります。トポスに対応する論理は直観主義論理です。直観主義論理と量子論理は大きく異なるので、トポスと量子がフィットするわけがない、という指摘です。しかし、イシャムのような思慮深い数理物理学者が、そこまで軽率な発想をするとも思えないので、「なにかあるんだろうなぁ(よく知らんけど)」と思ってました。

ヒューネン本第5章がイシャム達の試みと同じかどうか知りませんが、非可換な作用素環の可換な影絵をトポスのなかに映し出すような話らしい(あくまで「らしい」)です。ボーア化という名前は、ボーアの「古典的概念の教義」から来ているそうです。トポスの外部にある非古典(≒非可換)なモノが、ボーア化を通してトポス内では古典的(≒可換)に見えるのでしょう(たぶん)。

可換の場合、ノルム環(可換C*環)とゲルファント・スペクトル、ブール束とストーン・スペクトル(ストーン空間)のように、代数(環や束)と空間(スペクトル)がうまいこと対応してきれいな双対性が成立しています。非可換だと、代数-空間・対応がそれほどうまくはいかないのでしょう。ボーア化は、トポスに投影された可換な影により、トポス内でゲルファント双対/ストーン双対を構成する試みみたいです。このテの双対性の簡単な例は次の記事で紹介しています。

前の節で名前を出した竹内外史さんが、適当なトポス内(集合論を構成できる環境内)で実数論や複素数論を展開すると、それが(外から見れば)作用素環の議論になっている、といったことをやっていたような気がします*12。ボーア化と関係するのかも知れませんね。

具象への回帰

前の節で触れたように、僕はボブ・クック教授のファンなんですが、彼はヒルベルト空間と線形写像を嫌い、それらをお絵描きで置き換えました。絵は、抽象的構造の直截的表現として使われています。

ヒューネンの定式化も、有限双積をもつ圏やダガー圏から出発しているので同じラインに沿っていると言えます(絵は使わないけど)。しかし、具象へと回帰する意識が強いな、と感じます。要所要所に、埋め込み定理、表現定理が配置されています。埋め込み定理/表現定理は、公理的に規定された構造物が、実は手で触れる具体物と同型だったと主張する定理です。

抽象と具象を行き来するプロセスがいきいきと描かれていることにより、ヒューネン本はエキサイティングなものとなっています。新興分野である圏論的物理/圏論的情報学の魅力を十分に伝えていると思います。こういった本を日本語で読めるというのは、僕には感慨深いですね。


後編(2/2)は何なんだ? ってことですが、冒頭に書いた、紙の情報伝達媒体としての評価です。これを気にするのは僕の偏向した基準なので、切り離したほうがいいと思ったんです。

*1:「計算の論理」という言葉は曖昧で、計算のなかで使われる(例えばif文の条件記述)論理なのか、計算現象に関する法則を記述するメタ論理なのかハッキリしません。この曖昧さをハッキリさせることも「計算の論理」の一部なのでしょう。

*2:現在は岩波オンデマンドブックス https://www.amazon.co.jp/dp/4007305943 として販売されているようです。僕がたまたま持っていたのは、2007年のハードカバー本 https://www.amazon.co.jp/dp/4000054082 です。

*3:ベクトル空間や加群の圏の抽象化にはたくさんの変種があり、確立されたネーミングはありません。

*4:ヒューネンの定義では、双積と有限双積には微妙な違いがあります。

*5:僕は通常、「モノイド圏」と呼びますが、ヒューネン/川辺本では形容詞「モノイダル」が使われています。

*6:主表現という呼び名は今では古いらしく、(単項の)ホム関手と呼ぶのが普通のようです。

*7:とても簡単な例: 圏にゼロ対象《ヌル対象》があると、ホムセットを付点集合〈pointed set〉にできます。

*8:スカラー系が半環のときは半加群というべきかも知れません。が、単に「加群」で済ませます。

*9:セリンガーからの引用: Dagger compact closed categories were recently introduced by Abramsky and Coecke, under the name "strongly compact closed categories", as an axiomatic framework for quantum mechanics.

*10:竹内さんは、それほどチャンとした本を書く人じゃない、ということは知っておいたほうがいいです。でも、内容のエエカゲンさを補って余りある示唆・洞察・見識が含まれます。そこが魅力。

*11:昔からある量子論理のつもりで「古典的量子論理」と最初書いてしまったのだけど、それだと意味不明になってしまうよね。

*12:おそらく G. Takeuti, "Two applications of logic to mathematics" Princeton University Press, 1978

2018-08-13 (月)

ポンプの補題とその使い方: 回文の例

| 15:57 | ポンプの補題とその使い方: 回文の例を含むブックマーク

ポンプの補題の証明は比較的簡単ですが、言っていることの解釈や使い方は難しいです。

内容:

  1. なんかオカシイ
  2. ポンプの補題
  3. 正規言語
  4. ポンプの補題 再度
  5. 「ポンプする」とは
  6. 「ポンプしない」とは
  7. 回文の全体は正規言語ではない
  8. おわりに

なんかオカシイ

インターネット上で、ポンプの補題と回文について説明しているスライドに出会いました*1。回文とは、「シンブンシ」とか「タケヤブヤケタ」のように、逆向きに読んでも同じになる文字列のことです。件のスライドは「文字列が回文か否かを、正規表現を使って判断できない」ことを示していて、結論自体は正しいのですが、途中の議論がだいぶアヤシイ(つうか間違ってます)。

でも、「しょうがないかな」という気もします。回文の全体が正規言語にならないことを示すにはポンプの補題〈pumping lemma〉を使います。このポンプの補題は、その表現が複雑で、取り扱いが難しいのです。

ポンプの補題

ポンプの補題を日本語で書いてみます。

  • Lが無限正規言語であれば、次の性質を満たす整数 p ≧ 1 が存在する。
    • 長さがp以上の任意のLの語wは、次の性質を満たす分解 w = xyz を持つ。
      1. xyの長さはp以下
      2. yの長さは1以上
      3. 任意の非負整数(0も入れる)iに対して、xyiz はLの語である。ここで、yiは語yをi回繰り返したもの。

一読して何を言ってるのかを理解するのは難しいですよね。でも、証明は意外に簡単で、鳩の巣原理〈pigeonhole principle〉を使います。

ポンプの補題の記述を日本語で正確に扱うのは困難そうなので、後で論理式に直します。ここでは、ポンプの補題の(おそらく)語源だと思われる事実を指摘します。諸々の条件のもとで、語wを w = xyz とうまいこと分解すると、xz, xyz, xyyz, xyyyz, xyyyyz, ... がすべてLの語になります。

*2

この様子が、xとzのあいだに井戸があり、ポンプのひと押しごとにyを汲み出しては貯めていくように見えるからポンプの補題なのでしょう、たぶん(よく知らんけど)。

正規言語

記号を並べたものを〈word〉と呼びます。語を構成している個々の記号〈symbol〉は、集合Σの要素だとします。ギリシャ大文字シグマを使うのは形式言語理論の習慣です(おそらく、symbolのSから)。集合Σをアルファベット〈alphabet〉と呼び、ここでは有限だと仮定します。Σの要素を文字〈character〉とか〈letter〉と呼ぶこともあり、そのときは語を文字列〈string〉とも呼びます。ときに、Σの要素を語と呼び、語を〈sentence〉と呼ぶこともあります。

Σの記号から構成される語の全体をΣ*と表します。Σ*の部分集合を言語〈language〉と呼びます。形式言語理論の文脈での「言語」は今定義したものであり、通常の意味の「言語」とは違います。言語学的/哲学的に考えないでください*3。Lが(アルファベットΣ上の)言語だとは、LがΣ*のベキ集合Pow(Σ*)の要素であること L∈Pow(Σ*) 、それだけのこと、それ以上でも以下でもありません。

さて、Σ上の言語Lが正規言語〈regular language〉であることには、同値ないくつかの定義があります。

一番馴染みやすいのは、「正規表現で定義できる言語が正規言語である」でしょう。他に、クリーネ代数を使った定義、論理系を使った定義、半環上の行列代数を使った定義、トレース付きモノイド圏を使った定義などもあります。正規表現(とオートマトン)の基本的なことは次の記事にあります。

ポンプの補題 再度

ポンプの補題〈pumping lemma〉は、正規言語の性質を述べているものです。ただし、有限な正規言語(有限言語はすべて正規言語)では成立しませんたいして意味を持ちません。正規言語Lが集合として無限集合のときだけポンプの補題が成立しますを考えることにします[追記]「… では成立しません。」という言い方は不適切でした。この記事のコメント欄と記事最後の追記を参照。[/追記]ポンプの補題は次のように書けます。

  • Regular(L) ∧ Infinite(L) ⇒ Pump(L)

Pump(L)は、Lがポンプの補題の性質を満たすことです。Pump(L)を日本語で「Lはポンプする」と言うことにします。上記命題を日本語で言えば:

  • Lが正規言語で かつ Lが無限集合 ならば Lはポンプする

ポンプの補題は、与えられた言語Lが正規言語でないことを証明する際に使われます。このとき、「背理法を用いて、Lを正規言語だと仮定して矛盾を導く」とかよく言いますが、そう考える必要はありません。与えられた言語Lが、単に「ポンプしない」ことを示せばいいだけです。

先のポンプの補題の対偶をとってみます。'¬'は否定(not)を表す論理記号です。

  • ¬Pump(L) ⇒ ¬(Regular(L) ∧ Infinite(L))

'⇒'の右側にド・モルガンの法則を適用すれば、

  • ¬Pump(L) ⇒ ¬Regular(L) ∨ ¬Infinite(L)

通常、与えられる言語は無限言語だと分かっていますから、Infinite(L)は仮定されています。Infinite(L) と ¬Regular(L) ∨ ¬Infinite(L) からは ¬Regular(L) が出ます。

がんばって証明
     :
     :
--------------
   ¬Pump(L)   [ポンプの補題] ¬Pump(L) ⇒ ¬Regular(L) ∨ ¬Infinite(L)
------------------------------------------------------------------------[1]
[最初からの仮定] Infinite(L)   ¬Regular(L) ∨ ¬Infinite(L)
-------------------------------------------------------------[2]
              ¬Regular(L)

推論[1]は、「A, A⇒B よって B」というモーダスポネンンスです。推論[2]もモーダスポネンスです。¬A∨¬B ≡ ¬B∨¬A ≡ B⇒¬A なので、「B, B⇒¬A よって ¬A」という形です。

あるいは、論理式に関して、'⇒'越しに式を移動する“移項の原理”*4を使って、

  • ¬Pump(L) ⇒ ¬Regular(L) ∨ ¬Infinite(L)

から

  • ¬Pump(L) ∧ Infinite(L) ⇒ ¬Regular(L)

も言える、と思ってもいいです。

結局、無限言語Lに関して、Lがポンプしないことを示せば、Lは正規言語でないことになります。あえて背理法とか言うこともないでしょう。

「ポンプする」とは

与えられた言語Lがポンプしないことを示せば、Lが正規言語でないと言えます。ポンプしない、すなわち ¬Pump(L) を正確に書いてみましょう。そのためには、まずは Pump(L) を正確に書いて、それを否定します。

Pump(L)は次の形をしています。

  • Pump(L) ≡ ∃p≧1.Pump(L, p)

ここで、'≡'は論理式として同値な(同じとみなしてよい)ことです。'≡'の右側にも'Pump'が出てきますが、これは'≡'の左側の'Pump'とは別物です。引数の数〈number of arguments〉が違うんで区別できるだろうと、サボって同じ記号を流用(オーバーロード)してます。∃p≧1.Pump(L, p) で存在が保証される整数pを、Lのポンプ長〈pumping length〉といいます。Pump(L, p)を、「Lは(ポンプ長)pでポンプする」と言えば、

  • Lがポンプする とは Lがpでポンプするようなポンプ長pが存在する

ですね。さらに「Lはpでポンプする」を分解していきます。|w|は語wの長さです。

  • Pump(L, p) ≡ ∀w∈L.(|w|≧p ⇒ pump(L, w, p))

これは、Lの語wが長さp以上なら、「(語として)ポンプする」ことです。小文字の'pump'は、「Lの語wは、(ポンプ長)pでポンプする」と読むことにして、これは語wにフォーカスした言明になっています。その pump(L, w, p) は、

  • pump(L, w, p) ≡ ∃x, y, z.(w = xyz ∧ |xy|≦p ∧ |y|≧1 ∧ ∀i≧0.(xyiz∈L))

x, y, z はΣ*の要素ですが、x, y, z∈Σ* の'∈Σ*'は省略しています。どんな x, y, z が存在するのかというと:

  1. x, y, z をこの順で連接〈concatenate〉するとwになる。
  2. xyの長さはp以下。
  3. yの長さは1以上。
  4. 任意の非負整数iに対して、xyiz がLの語になる。

はい、これで(ポンプの補題の意味での)「ポンプする」の記述はオシマイです。全部展開して書くと:

  • ∃p≧1.(∀w∈L.(|w|≧p ⇒ (∃x, y, z.(w = xyz ∧ |xy|≦p ∧ |y|≧1 ∧ ∀i≧0.(xyiz∈L)))

「ポンプしない」とは

「Lがポンプしない」は、¬Pump(L) を求めればいいので、前節の分解した定義に従って順に否定していきましょう。

  • ¬Pump(L) ≡ ¬∃p≧1.Pump(L, p)

存在記号に関するド・モルガンの法則により、

  • ¬Pump(L) ≡ ∀p≧1.¬Pump(L, p)

¬Pump(L, p) は、

  • ¬Pump(L, p) ≡ ¬∀w∈L.(|w|≧p ⇒ pump(L, w, p))

全称記号に関するド・モルガンの法則により、

  • ¬Pump(L, p) ≡ ∃w∈L.(|w|≧p∧¬pump(L, w, p))

ここで、含意 A⇒B の否定が A∧¬B であることを使っています。さらに、¬pump(L, w, p) は、

  • ¬pump(L, w, p) ≡ ¬∃x, y, z.(w = xyz ∧ |xy|≦p ∧ |y|≧1 ∧ ∀i≧0.(xyiz∈L))

また存在記号に関するド・モルガンの法則により、

  • ¬pump(L, w, p) ≡ ∀x, y, z.(w = xyz ∧ |xy|≦p ∧ |y|≧1 ⇒ ¬∀i≧0.(xyiz∈L))

ここでは、A∧B∧C∧D の否定が A∧B∧C ⇒ ¬D となっています。これは次のような変形の結果です。

    ¬(A∧B∧C∧D)
 ≡ ¬((A∧B∧C)∧D)
 ≡ ¬(A∧B∧C)∨¬D
 ≡ (A∧B∧C) ⇒ ¬D

¬∀i≧0.(xyiz∈L) に、また全称記号に関するド・モルガンの法則を適用して、

  • ¬∀i≧0.(xyiz∈L) ≡ ∃i≧0.(xyiz !∈ L)

'!∈'は「所属しない」の意味です。今までの変形をまとめると:

  • ∀p≧1.(∃w∈L.(|w|≧p ∧ ∀x, y, z.(w = xyz ∧ |xy|≦p ∧ |y|≧1 ⇒ ∃i≧0.(xyiz !∈ L))))

日本語にしてみると:

  • 1以上の任意の整数pに対して、次の性質を満たすLの語wが存在する。
    • wは長さp以上。
    • Lの任意の語x, y, zに対して、次が成立する。
      • w = xyz であり かつ xyの長さがp以下 かつ yの長さが1以上 ならば 次の性質を持つ。
        • ある非負整数iが存在して、xyizはLの語ではない。

「存在する/存在して」が入っているので、「ポンプしない」ことを示すには、条件を満たす語wと非負整数iを具体的に見つける必要があります。

回文の全体は正規言語ではない

では、表記の命題をポンプの補題を使って証明しましょう。まずは注意事項: アルファベットΣが単一の記号、例えばaしか含まないとき、Σ = {a} 上の語はすべて回文になります。(Σ上の回文の全体) = Σ* = (正規表現 a* で定義される言語) なので、回文の全体は正規言語です。これは例外です。

Σは2個以上の要素を持つとします。要素は何でもいいので、Σ = {0, 1} とします(3個以上の要素があっても話は同じ)。Σ上の回文〈palindrome〉の全体をP(大文字だよ)とします。Pがポンプしないことを示します。

p(小文字だよ)を1以上の任意の整数とします。このpに対して、回文(Pの語)を次のように定義します。

  • w = 0p10p

ここで、0pは0をp個並べたものです。例えば(あくまで例えば) p = 3 ならば、w = 0001000 です。wは明らかに回文です。

wを w = xyz かつ |xy|≦p かつ |y|≧1 であるように分解します。|xy| ≦ p であることから、xyは0の並びになります。yは1個以上の0の並びです。xの長さをn、yの長さをmとしましょう。すると、

  • xy = 0n+m (0 ≦ n ≦ p - 1, 1 ≦ m ≦ p, 1 ≦ n + m ≦ p)
  • x = 0n
  • y = 0m

と書けます。ここで、xy0 = x とすると、長さは n となり、(p - 1)個以下の0の並びです。したがって xy0z は、「(p - 1)個以下の0の並び 1 p個の0の並び」となり回文ではありません。(iを十分大きくしても回文でなくなります。)

以上で、w = 0p10p という回文(Pの語)と、i = 0 という非負整数が見つかって、「w = xyz かつ |xy|≦p かつ |y|≧1 であるような分解」をどう取ろうが、xy0zはPの語ではないように出来ることが分かりました。つまり、回文の全体Pはポンプしません

ポンプの補題が「ポンプしない無限言語は正規言語ではない」と主張しているので、回文の全体Pは正規言語ではありません。もちろん、Pを正規表現で定義できるはずはありません。

おわりに

命題が複雑になると、その否定や対偶を作るのはけっこう大変になります。しかし、否定や対偶は頻繁に使う論理的操作なので、正確に変形できないと困ることがあります。入れ子になった存在記号や全称記号はド・モルガン法則で否定しましょう。そもそも、入れ子になった存在記号や全称記号の解釈が難しいので、正確を期すには自然言語だけでなく論理式で書いたほうがいいと思います。


[追記]コメント欄で、はいさんからご指摘があったように、Regular(L) ∧ Infinite(L) ⇒ Pump(L) ではなくて、Regular(L) ⇒ Pump(L) でも命題は成立するので、Infinite(L) を明示的に付ける必要はありません。Lが有限言語の場合、pをどの語の長さよりも大きく取ると、|w|≧p ⇒ pump(L, w, p) の |w|≧p が常に偽になり、pump(L, w, p) の真偽に関わらずこの含意命題が成立し、有限言語でも適当な整数pにおいてポンプの補題の性質を満たすことになります。

というわけで、Infinite(L)は不要です。でも、事実上無限言語でしかポンプの補題を使わないので、一種の適用条件としてInfinite(L)を置いといても害はないと思います。本文内の記述はそのままです。[/追記]

*1:間違いを具体的に指摘するのが目的ではないので、URL参照はしません。

*2:画像: https://ja.wikipedia.org/wiki/手押しポンプ#/media/File:WellPump.JPG 神戸市市東灘区石屋川の公園にある井戸ポンプ

*3:形式言語理論/数理言語学言語学の一部門と考えるなら、今は数理的なアプローチしか考えない、ということ。

*4:厳密には、論理式を古典論理のシーケントの形に書いたときに、移項の原理が機能します。

はいはい 2018/08/13 16:51 > ただし、有限な正規言語(有限言語はすべて正規言語)では成立しません。正規言語Lが集合として無限集合のときだけポンプの補題が成立します。

に関して, 有限正規言語に対してはポンプ長を長くとることでポンプの補題が自明に成立するようにするのが標準的なのではないか, と指摘しようとしたのですが, 考えてみると, ポンプの補題をこう拡張しても実際に補題を使う場面ではメリットが少ないですね.

ポンプの補題を使ってある言語Lが正規言語でないことをいうためには, Lに含まれるポンプできない文字列の長さが有界でないことを示さなければいけませんが, これが示せたときLが有限言語でないことは明らかです. ですので, 最初からポンプの補題の適用対象を無限言語に制限していても全く問題ないと思います.

m-hiyamam-hiyama 2018/08/13 17:02 はいさん、
記事内の「… では成立しません。」という言い方は不適切かも知れませんね。
> 最初からポンプの補題の適用対象を無限言語に制限していても全く問題ないと思います.
僕の気持ちは、有限言語に対して「ポンプの補題」とか言ってもしょうがないので、無限言語という条件を付けてから命題を記述しよう、ということです。
記述の一様性のために有限の場合も含めてもいいし、最初から無限言語の文脈で語るでもかまいません。

はいはい 2018/08/13 17:15 > 有限言語に対して「ポンプの補題」とか言ってもしょうがない

そうですね. 言語がはじめから有限と分かっているときにポンプの補題を持ち出してきても全然嬉しくない, というのは全くその通りだと思います.

m-hiyamam-hiyama 2018/08/13 19:54 はいさん、
「成立しません」は訂正しました。ご指摘、ありがとうございます。

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

2018-08-06 (月)

「ホッジ・ランク」は追記予定

| 10:34 | 「ホッジ・ランク」は追記予定を含むブックマーク

ホッジ分解を利用して求めた順位、すなわちホッジ・ランクについては、追記予定です。追記したらtwitterで通知がいくようにします。ホッジ・ランクの絵も描いてあるしね。

ロマ数ナイト #12 サポート記事: ホッジ・ランク

| 18:41 | ロマ数ナイト #12 サポート記事: ホッジ・ランクを含むブックマーク

この記事は、「ロマンティック数学ナイト@渋谷 #12」の事後サポート用の記事です。今週中に何度か更新(編集・追加)すると思います。

[追記 date="木曜・朝"]大きな編集・追加はまだしてません。ミスの修正、表現の変更はしました[/追記][追記 date="木曜・夜"]「中間のまとめと展望」以降を追加しました。でも、資料作製は未着手。[/追記][追記 date="金曜・夕刻"]資料を提出。「ホッジ分解」の節を追加。あと、「ホッジ分解のランキング問題への応用」が残ってますが、これは明日口頭で話せるかも。[/追記]

内容:

  1. この記事の目的
  2. 比較可能性グラフ
  3. 離散ド・ラーム理論のセットアップ
  4. ド・ラーム複体とド・ラーム・コホモロジー
  5. ド・ラーム複体の解釈
  6. 中間のまとめと展望
  7. 双対空間、チェーンと離散積分
  8. 内積と随伴線形写像
  9. 離散外解析/離散ベクトル解析
  10. 離散解析の4つの作用素
  11. ホッジ分解
  12. ホッジ分解のランキング問題への応用 見出しだけ

この記事の目的

2018年8月11日開催の「ロマンティック数学ナイト@渋谷 #12」でショートプレゼンします。時間は数分なので、尻切れトンボになるのは目に見えています。なので、僕のプレゼンをお聞きいただいた後の確認や補足のために、この記事を準備しておきます。

現時点では、当日資料(スライド)を作ってないので、資料の作製に伴いこの記事にも手を加えるでしょう。フィックスするのは金曜日かな。(資料はその前に提出したいけど、締切に間に合うかな、どうかな? -- とか言い訳っぽく言っておく。)

この記事だけ読んでもあんまり分かんないかも知れません。でも、この記事とは別に、ホッジ・ランクの入門記事を書く可能性はあります。そうなれば、この記事は、入門記事に対する続き(第二章)という位置付けになります。

話のネタ元は次の論文です。

  • Title: Statistical ranking and combinatorial Hodge theory (2009 v2)
  • Authors: Xipaoye Jiang, Lek-Heng Lim, Yuan Yao, Yinyu Ye
  • Pages: 42p.
  • URL: https://arxiv.org/abs/0811.1067

この論文を忠実に紹介するわけではありません。使う用語、記号・記法も変えているところがあります。

事後サポートであることの意味は、既に話題と問題意識は理解されている前提で書く、ということです。ショートプレゼンで問題意識は説明できても、おそらく、方法と背景を述べる余裕はないでしょう。

本文内で、《…》 と書かれた用語は、この記事内で説明してないけど既知と仮定する言葉です。僕のショートプレゼン内で説明されているでしょう(そう期待します)。

比較可能性グラフ

G = (V, E) を有限無向単純グラフとします。その意味は:

  1. Vは、有限集合です。Vの要素を頂点〈vertex〉と呼びます。
  2. Eは、Vの2元部分集合の集合Pow2(V)の部分集合です。Eの要素を無向辺〈undirected edge〉、または単に〈edge〉と呼びます。(この記事内では、単に「辺」と言ったら無向辺です。)

Pow(X)はXのベキ集合(部分集合の集合)で、Pown(X)は基数(要素の個数)がnである部分集合の集合です。Gはグラフですが、辺に向きはなく、多重辺も自己ループ辺も認めません。

G = (V, E) を《ランキング問題》のモデルと考えるときは:

  1. 頂点は選択肢〈alternative〉と考えます。僕は評価対象と呼んでいます。
  2. 頂点Aと頂点Bが辺で結ばれている({A, B}∈E である)ときは、AとBは比較可能〈comparable〉だと言います。AとBが比較可能でない〈比較不能〉とは、種類が違うので比較がナンセンスだとか、比較する手段や比較用のデータがないとかです。

Gは幾何的形状を持つので、連結成分とか幾何的サイクル(1次元の有向な輪)とかを定義できます。

ときに、Gの頂点の集合Vに全順序〈total order〉を入れます。この全順序はまったく便宜的なものです。頂点に通し番号を付けて、その番号で順序付けしてもいいし、頂点の個数が少ないなら英字一文字で頂点にラベルして、アルファベット順で順序付けしてもいいです。なんでもいいです、便宜的なので。

A, B, C∈V、{A, B, C}∈Pow3(V) として、三元集合{A, B, C}が三角形〈triangle〉だとは、次を満たすことです。

  • {A, B}∈E かつ {B, C}∈E かつ {A, C}∈E

三辺形と言ってもいいですね。三角形と三辺形は同義語として使います。辺に向きがないので、三角形も向き〈orientation〉を持たないことに注意してください。

Gのすべての三角形からなる集合をT(T⊆Pow3(V))とします。GからTは一意に決まります。三角形の集合をよく使うので、最初からグラフの構成素に入れて G = (V, E, T) としておきます。(Tを落としても、V, Eから再構成できますが、入れておけば便利。)

三角形の集合を添えた有限無向単純グラフ G = (V, E, T) を、《ランキング問題》の観点からは比較可能性グラフ〈comparability graph〉と呼びます。

離散ド・ラーム理論のセットアップ

比較可能性グラフは、《離散ド・ラーム理論》を載せるための台空間〈underlying space〉と言えます。比較可能性グラフ G = (V, E, T) 上にド・ラーム複体を構成しましょう。なお、ド・ラーム複体やホッジ分解に関しては次の記事で説明しています。

上記記事で、離散的(組み合わせ的)なケースを紹介しているのですが、「離散」の意義が違います。上記記事では、

  • 連続な状況に対する近似としての離散

を想定しています。今回は、

  • 最初から離散な状況

です。

さて、まず G = (V, E, T) に対する組み合わせ複体(単体複体)K(G)を定義しましょう。以下、K = K(G) と略記します。一般的に「単体複体とは何であるか」は気にしなくていいです。比較可能性グラフGから作ったKを単体複体〈simplicial complex〉と呼ぶ、ということだけ知ってれば今は十分です*1。単体複体Kは、K0, K1, K2 という3つの有限集合から構成されます。

  • K0 := V
  • K1 := {(A, B)∈V×V | {A, B}∈E}
  • K2 := {(A, B, C)∈V×V×V | {A, B, C}∈T}

集合Kkの要素をk-セル〈k-cell〉と呼びます*2。k-セル(k = 0, 1, 2)と、頂点/辺(無向辺)/三角形を同じ意味で使うときが多いのですが、ここでは同じ意味とは限りません

  • 頂点Aと、0-セルAは同じ意味。
  • 無向辺{A, B}に対して、2つの1-セル (A, B), (B, A) が対応する。
  • 三角形{A, B, C}に対して、6つの2-セル (A, B, C), (A, C, B), (B, A, C), (B, C, A), (C, A, B), (C, B, A) が対応する。

0-セルは頂点そのもの、1-セルと2-セルは辺・三角形の頂点に順番を付けたものです。頂点の順番付け〈oerdering〉が違えば、台図形〈underlying shape〉が同じでも違うセルです。

Kk(k = 0, 1, 2)上のR値関数で、交代的〈反対称〉なものを考えます。交代的とは次のことです。

  • f:K0R が交代的 :⇔ なんでもいい(特に条件なし)
  • ω:K1R が交代的 :⇔ (A, B)∈K1 に対して、ω(A, B) = -ω(B, A) が成立する。
  • σ:K2R が交代的 :⇔ (A, B, C)∈K2 に対して、以下の等式が成立する。
    1. σ(A, B, C) = σ(A, B, C) (自明)
    2. σ(A, C, B) = -σ(A, B, C)
    3. σ(B, A, C) = -σ(A, B, C)
    4. σ(B, C, A) = σ(A, B, C)
    5. σ(C, A, B) = σ(A, B, C)
    6. σ(C, B, A) = -σ(A, B, C)

置換の符号という概念を使えば一般的な定義ができますが、k = 0, 1, 2 だけなので一般論は不要です。

Ω0(K), Ω1(K), Ω2(K) を次のように定義します。

  • Ω0(K) := {f:K0R | fは交代的(特に条件なし)}
  • Ω1(K) := {ω:K1R | ωは交代的}
  • Ω2(K) := {σ:K2R | σは交代的}

Ωk(K) (k = 0, 1, 2)は自然にR上のベクトル空間の構造を持つので、以下、ベクトル空間として扱います。ベクトル空間Ωk(K)の要素をk-コチェーン〈k-cochain〉またはk-形式〈k-form〉と呼びます。この呼び方の背景を知りたい方は:

具体的な計算をするために、ベクトル空間の基底を固定します。そのために、比較可能性グラフGの頂点集合Vに全順序を入れます。この全順序は、計算の都合のために便宜的・人為的に入れるもので、構造的・内在的な意味は何もないことに注意してください。

V = (V, ≦) を便宜的・人為的に定めた全順序構造とします。この全順序構造のもとで:

  • 任意の0-セルAを、強単調0-セルと呼ぶ
  • A < B である1-セル(A, B)を、強単調1-セルと呼ぶ
  • A < B < C である2-セル(A, B, C)を、強単調2-セルと呼ぶ

強単調k-セル〈strongly monotonic k-cell〉(k = 0, 1, 2)は、セルを {0, ..., k}→V という全順序集合のあいだの写像と考えたときに強単調(i < j ならば f(i) < f(j))なことです。強単調なk-セルに限定すると:

  • 比較可能性グラフGの頂点と、単体複体Kの強単調0-セルは、1:1対応する。
  • 比較可能性グラフGの辺と、単体複体Kの強単調1-セルは、1:1対応する。
  • 比較可能性グラフGの三角形と、単体複体Kの強単調2-セルは、1:1対応する。

強単調k-セル全体の集合をK<kとします。今言ったことから、V ¥stackrel{¥sim}{=} K<0, E ¥stackrel{¥sim}{=} K<1, T ¥stackrel{¥sim}{=} K<2

ベクトル空間Ωk(K) (k = 0, 1, 2)の基底を、強単調k-セルでインデックスして定義しましょう。定義には型付きラムダ記法(ココを参照)を使います。

A∈K<0 に対して、
  δA :=
      λX∈K0.(if (X = A) then 1 else 0)

(A, B)∈K<1 に対して、
  δA,B :=
      λ(X, Y)∈K1.(
          if ((X, Y) = (A, B)) then 1
          elseif ((X, Y) = (B, A)) then -1
          else 0
      )

(A, B, C)∈K<2 に対して、
  δA,B,C :=
      λ(X, Y, Z)∈K2.(
          if (
              (X, Y, Z) = (A, B, C) or
              (X, Y, Z) = (B, C, A) or
              (X, Y, Z) = (C, A, B)
             ) then 1
          elseif (
              (X, Y, Z) = (A, C, B) or
              (X, Y, Z) = (B, A, C) or
              (X, Y, Z) = (C, B, A)
             ) then -1
          else 0
      )

今定義したδ達は、クロネッカーのデルタとエディントンのイプシロンを混ぜてカリー化した*3ようなものですが、記号はデルタを使いました。強単調k-セルでインデックスされたδ達は、ベクトル空間Ωk(K) (k = 0, 1, 2)の基底となるので、次のような表示が可能です。

 f ¥,=¥, ¥sum_{A¥in K^{<}_0} f(A)¥delta_{A}

 ¥omega ¥,=¥, ¥sum_{(A, B)¥in K^{<}_1} ¥omega(A, B)¥delta_{A,B}

 {¥bf ¥sigma} ¥,=¥, ¥sum_{(A, B, C)¥in K^{<}_2} {¥bf ¥sigma}(A, B, C)¥delta_{A,B,C}

あるいは、A, B, C∈V であるのは了解されているとして:

 f ¥,=¥, ¥sum_{A} f(A)¥delta_{A}

 ¥omega ¥,=¥, ¥sum_{A < B} ¥omega(A, B)¥delta_{A,B}

 {¥bf ¥sigma} ¥,=¥, ¥sum_{A < B < C} {¥bf ¥sigma}(A, B, C)¥delta_{A,B,C}

行きがかり上、今定義したΩk(K)の基底をデルタ基底〈delta basis〉と呼びましょう。Ωk(K)のデルタ基底は、強単調k-セルの集合K<kでインデックスされます。デルタ基底の概念は、最初に人為的に決めた全順序 (V, ≦) に依存しますが、頂点集合Vの全順序を固定した上で、標準的〈canonical〉な基底と言えます。

今後、ベクトル空間Ωk(K) (k = 0, 1, 2)に関する具体的計算は、すべてデルタ基底を用いて行います。記号δが、クロネッカーのデルタとは少し違うことには注意してください。

ド・ラーム複体とド・ラーム・コホモロジー

離散の場合の用語法をどうするか悩むのですが、「ド・ラーム・コホモロジーとホッジ分解のオモチャ (2/2) // 多様体から線形代数へ」で決めた用語を使うことにします。以下に用語対応表を再掲します。(今、用語の意味が分からなくてもかまいません。)

連続(多様体)の場合 離散(比較可能性グラフ)の場合
多様体 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)

ただし、《ランキング問題》に固有な言葉も同義語として併用します。

では、余境界作用素(外微分作用素に相当)を定義しましょう。D00(K)→Ω1(K) と D11(K)→Ω2(K) を次のように定義します。

  • f∈Ω0(K) に対して、
    (D0(f))(A, B) = f(B) - f(A)
    D0(f)∈Ω1(K)
  • ω∈Ω1(K) に対して、
    (D1(ω))(A, B, C) = ω(B, C) - ω(A, C) + ω(A, B)
    D1(ω)∈Ω2(K)

D0(f), D1(ω) が交代的〈反対称〉であることを確認する必要があります(やってください)。そして、次の事実が極めて重要です。'¥circ'は作用素の結合〈合成〉、'0'はゼロ写像です。等式は簡単に確認できますね。

  • D1¥circD0 = 0 : Ω0(K)→Ω2(K)

上の等式から、Ker, Im を線形写像の核空間、像空間として、次が成立します。

  • Im(D0) ⊆ Ker(D1)

D0とD1にゼロ写像を付け加えた線形写像の列

  • O -(ゼロ写像)→ Ω0(K) -(D0)→ Ω1(K) -(D1)→ Ω2(K) -(ゼロ写像)→O

を、単体複体Kの(あるいは比較可能性グラフGの)ド・ラーム複体〈de Rham complex〉と呼びます*4。そして、ド・ラーム複体の Ker/Im をとった以下のベクトル空間の列を、単体複体Kの(あるいは比較可能性グラフGの)ド・ラーム・コホモロジー〈de Rham cohomology〉と呼びます。

  • H0(K) := Ker(D0)/O ¥stackrel{¥sim}{=} Ker(D0)
  • H1(K) := Ker(D1)/Im(D0)
  • H2(K) := Ω2(K)/Im(D1)

それぞれのベクトル空間Hk(K)をk次のド・ラーム・コホモロジー空間〈de Rham cohomology space of degree k〉といい、コホモロジー空間の要素をコホモロジー・クラス〈cohomology〉と呼びます。もっとも、0次のコホモロジークラスは、もとの空間Ω0(K)の要素とみなせるので、クラス(同値類)っぽくないですが。

《ランキング問題》の文脈では、今まで出てきた集合・空間の要素を、次のように呼びます。

  • A∈K0 : 選択肢、評価対象
  • (A, B)∈K1比較可能ペア〈comparable pair | pair-wise comparison data〉(比較される二者)
  • (A, B, C)∈K2比較可能トリプル〈comparable triple | triple-wise comparison data〉(A, B, C 3つの評価対象と、(B, C), (A, C), (A, B) の3つの比較可能ペア)
  • f∈Ω0(K) : スコア関数〈score function〉
  • ω∈Ω0(K) : ペア選好形式〈pair-wise preference form〉(二者間で、どっちを選好〈prefer〉するかの値)
  • σ∈Ω0(K) : トリプル矛盾形式〈triple-wise inconsistency form〉(三者間の比較に矛盾があるかどうかを示す値)

「ペア」を「二者」または「二者間」、「トリプル」を「三者」または「三者間」ともいいます。例えば、二者間選好形式、三者間矛盾形式という言葉を使います。

ド・ラーム複体の解釈

比較可能性グラフGから作られた単体複体Kに対して、ド・ラーム複体 O→Ω0(K)→Ω1(K)→Ω2(K)→O が定義できました。このド・ラーム複体を、《ランキング問題》の観点から解釈してみます(諸々の呼び名だけは前節最後で紹介しました)。

比較可能性グラフGは、問題の定式化の幾何的下部構造〈underlying geometric space〉を与えます。Gのトポロジカルな性質は、単体複体Kに、さらにド・ラーム複体Ωk(K)にと反映されるので、Gのトポロジカルな性質が問題全体を支配することになります。

ド・ラーム複体の0-形式〈0-コチェーン〉は、頂点集合V上で定義された実数値関数で、これが選択肢〈評価対象〉を(相対比較ではなくて)大域的に絶対比較した結果であるスコア関数となります。スコア関数fがあれば、次のようにしてV上にプレ順序(順序の公理から反対称律を取り除いた関係)が入ります。

  • A  ¥preceq B :⇔ f(A) ≦ f(B)

左辺の'≦'は実数の大小順序です。こうして定義されるプレ順序' ¥preceq'は、便宜的・人為的に入れたV上の全順序'≦'とは別物で、何の関係もありません。fから決まるV上のプレ順序が、スコア関数による順位〈rank | ランク〉です。プレ順序なので、同順位(甲乙つけがたい)を認めます。

我々が特に注目するのはΩ1(K)の要素、1-形式です。比較可能なペア(順序対)(A, B)に対して1-形式は、「Aに対してBが、どのくらい好ましいか」を表す選好値〈preference value〉を割り当てます。「AとBを比べたとき、Bをどのくらい余計に推すか」でもあるので推し値と言ってもいいかも知れません。

選好値を{-1, 0, 1}に限ると、単純な二者比較(程度は考えない)になりますが、ここでは任意の実数値を許すので、選好(推し)の程度を定量的に表現できます。選好値を0に設定すれば「甲乙つけがたい」ですが、これは比較不能とは違います。比較不能はGのトポロジカルな性質で、選好値0はG上の1-形式の特性です。

今述べた事情により、1-形式を二者間選好形式〈pair-wise preference form〉、あるいは単に選好形式〈preference form〉と呼ぶわけです。

スコア関数fがあると、それに余境界作用素D0を作用させたD0(f)(しばしばDfと略記される)は二者間選好形式です。比較可能ペア(A, B)に対する選好値は f(B) - f(A) なので、スコアの差分です。Dfの形である選好形式から、スコア関数fを再現できます。そのためには、比較可能性グラフG上のパスに沿った“線積分”(離散的なもの、計算は総和)を求めればいいのです。

ベクトル解析との類似性から言うと、スコア関数はポテンシャルに相当します。ポテンシャルの勾配〈gradient〉として得られた場から、線積分により、定数の差を除けばポテンシャルを回復できます。積分定数の個数は、下部構造である多様体の連結成分の個数と同じでした。比較可能性グラフ上の離散線積分でも同様で、比較可能性グラフGの連結成分の個数だけ積分定数が出てきます。比較可能性からの同値関係でグループ分けした各ジャンル(同値類=連結成分)ごとに、積分定数=スコア関数の基準ゼロ値を任意に選べます*5

任意の微分形式/ベクトル場がポテンシャルの勾配として得られるとは限らないのと同様に、任意の選好形式がスコア関数の差分として得られるとは限りません。離散線積分から関数が得られるとは限らないのです。もっと精密な分析が必要です。そのために、分析の道具を準備しますが、先に進む前に中間まとめ(次節)。

中間のまとめと展望

今までのおさらい; 我々の出発点は、有限無向単純グラフ G = (V, E) でした。これに、三角形の集合Tを添えて、G = (V, E, T) として、2次元の幾何的対象と考えました。G(《ランキング問題》の観点からは比較可能性グラフ)は、2次元の多様体と類似性があると期待できます。

実際、2次元の(なめらかでコンパクトな)多様体と三角形を添えた有限無向単純グラフには強い類似性があります。《ランキング問題》、《ホッジ・ランク》の理解のために多様体についての知識は必須ではありませんが、既にご存知の方のために、多様体=連続の場合と離散の場合の対応関係を示します(下の表)。下の表内で、T(M) は多様体Mの接バンドル、V∧W はベクトル空間VとWの外積です。

離散の場合 連続の場合
有限無向単純グラフ+三角形 G 2次元コンパクト多様体 M
Gの頂点 A∈V (頂点=0-セル) Mの点 p∈M
Gの1-セル (A, B)∈V×V Mの接ベクトル(線素) Xp∈Tp(M)
Gの2-セル (A, B, C)∈V×V×V Mの面素(無限小) Sp∈Tp(M)∧Tp(M)
単体複体 K = K(G) -
0-形式の空間 Ω0(K) 0-微分形式の空間 Ω0(M)
1-形式の空間 Ω1(K) 1-微分形式の空間 Ω1(M)
2-形式の空間 Ω1(K) 2-微分形式の空間 Ω2(M)
余境界作用素 D00(K)→Ω1(K) 外微分作用素 d00(M)→Ω1(M)
余境界作用素 D11(K)→Ω2(K) 外微分作用素 d11(M)→Ω2(M)
ド・ラーム複体 Ωk(K)→Ωk+1(K) ド・ラーム複体 Ωk(M)→Ωk+1(M)
ド・ラーム・コホモロジー Hk(K) ド・ラーム・コホモロジー Hk(M)

2次元多様体Mを三角形分割すれば、Mから単体複体 K(M) を作れますが、グラフGが多様体の近似というわけではないので、K(G) ←→ K(M) のような対応は考えないことにします。つまり、K = K(G) に直接対応する連続バージョンはないとします。

G = (V, E, T) を2次元の幾何的対象とみなした図形(単体複体Kの幾何実現)はありますが、これが2次元多様体となるとは限りません。むしろ、たいていは多様体じゃないです。上に挙げた類似性は、k-形式(k-コチェーンとも呼ぶ)のベクトル空間Ωk(-)とそのあいだの作用素(線形写像)のレベルでより顕著です。つまり、抽象線形代数に持ち込んでしまえば、ほぼ同じ代数的構造を持ちます。

「G = (V, E, T) と2次元コンパクト多様体Mの類似性」は我々の指導原理(アイディアの源泉)ですが、M上にはリーマン計量が載り、外微分解析〈exterior differential calculus〉/ベクトル解析〈vector calculus 〉ができて、ホッジ理論〈Hodge theory〉が展開できます。これらの概念の離散バージョンを作ることが次の目標になります。

双対空間、チェーンと離散積分

比較可能性グラフ G = (V, E, T) において、Vは有限集合でした、E⊆Pow2(V) も有限で、T⊆Pow3(V) も有限、K1⊆V×V, K2⊆V×V×V も有限です。cardを集合の基数をとる関数だとして、

  • dim(Ω0(K)) = card(V)
  • dim(Ω1(K)) = card(K<1) = card(E)
  • dim(Ω2(K)) = card(K<2) = card(T)

なので、Kの(Gの)ド・ラーム複体に出現するベクトル空間はすべて有限次元です。したがって、有限次元実数係数の線形代数が適用できます。これから、双対空間〈双対ベクトル空間〉の議論が出てきますが、次の記事が多少は参考になるかも。

さて、まず、k-形式(k-コチェーンともいう)の空間Ωk(K)の双対空間をCk(K)と書き、Ck(K)の要素をk-チェーン〈k-chain〉と呼びます。kはチェーンの次元〈dimension〉または次数〈degree〉と呼びます。各次元のチェーンを次のように表すことにします。

  • 0-チェーン : P, Q, R (英字大文字)
  • 1-チェーン : a, b, c (英字小文字)
  • 2-チェーン : s, t, u (英字小文字太字)

もとの空間と双対空間のあいだの標準ペアリング〈canonical pairing〉(「双対ベクトル空間、これくらい知ってればイインジャナイ // 標準双対ベクトル空間」参照)は <-|->k(kは次数)と書きます。つまり:

  • <P|f>0 = P(f) (P∈C0(K), f∈Ω0(K))
  • <a|ω>1 = a(ω) (a∈C1(K), ω∈Ω1(K))
  • <s|σ>2 = s(σ)(s∈C2(K), σ∈Ω2(K))

たいてい、<-|->k:Ck(K)×ΩkR のkは省略します。

我々のストーリーでは、k-コチェーンの空間Ωk(K)を先に定義したので、k-チェーンの空間Ck(K)を双対空間として定義しました。しかし、Ck(K)を先に定義すれば、Ωk(K)がその双対空間になります。もとの有限次元ベクトル空間とその双対空間は対等なので、どっちが先でも大丈夫です。差別しないで、公平〈unbiased〉に扱いましょう

k-コチェーン〈k-形式〉の空間Ωk(K)には、標準的な基底であるデルタ基底がありました。デルタ基底の双対基底を便宜上ガンマ基底〈gamma basis〉と呼び、次のように表します。

  • γA : デルタ基底との関係 <γAX>0 = if (A = X) then 1 else 0
  • γA,B : デルタ基底との関係 <γA,BX,Y>1 = if (A = X かつ B = Y) then 1 else 0
  • γA,B,C : デルタ基底との関係 <γA,B,CX,Y,Z>2 = if (A = X かつ B = Y かつ C = Z) then 1 else 0

ガンマ基底も、K<0, K<1, K<2 でインデックスされた基底です。ガンマ基底によるk-チェーンの展開は次のようになります。

 P ¥,=¥, ¥sum_{A¥in K^{<}_0} P_A¥gamma_{A}

 a ¥,=¥, ¥sum_{(A, B)¥in K^{<}_1} a_{A, B}¥gamma_{A,B}

 {¥bf s} ¥,=¥, ¥sum_{(A, B, C)¥in K^{<}_2} {¥bf s}_{A, B, C}¥gamma_{A,B,C}

ガンマ基底の要素 γA, γA,B, γA,B,C を、強単調k-セル A, (A, B), (A, B, C) と同一視してしまい、次のようにも書きます。

 P ¥,=¥, ¥sum_{A¥in K^{<}_0} P_A A

 a ¥,=¥, ¥sum_{(A, B)¥in K^{<}_1} a_{A, B} (A, B)

 {¥bf s} ¥,=¥, ¥sum_{(A, B, C)¥in K^{<}_2} {¥bf s}_{A, B, C}  (A, B, C)

あるいは、A, B, C∈V であるのは了解されているとして:

 P ¥,=¥, ¥sum_{A} P_A A

 a ¥,=¥, ¥sum_{A < B} a_{A, B} (A, B)

 {¥bf s} ¥,=¥, ¥sum_{A < B < C} {¥bf s}_{A, B, C}  (A, B, C)

こう考えると、標準ペアリングは次のように展開できます。

 <P | f> ¥,=¥, <¥sum_{A} P_A A | f> ¥,=¥, ¥sum_{A} P_{A}f(A)

 <a | ¥omega> ¥,=¥, <¥sum_{A < B} a_{A,B} (A, B) | ¥omega> ¥,=¥, ¥sum_{A < B} a_{A,B}¥omega(A, B)

 <{¥bf s} | {¥bf ¥sigma} > ¥,=¥, <¥sum_{A < B < C} {¥bf s}_{A,B, C} (A, B, C) | {¥bf ¥sigma}> ¥,=¥, ¥sum_{A < B < C} {¥bf s}_{A,B,C}{¥bf ¥sigma}(A, B, C)

計算の途中で <A|f> = f(A) などとしています。これは頂点Aと頂点Aにおける求値作用〈evaluation〉を同一視しているわけで、A|→<A|-> はゲルファント変換です -- 詳しくは「双対ベクトル空間、これくらい知ってればイインジャナイ // 二重双対空間」を参照。

今述べた同一視のもとで、k-チェーンとは、k-セル(頂点、頂点の順序ペア、頂点の順序トリプル)の線形結合だと言えます。1次の標準ペアリング <a|ω>11-形式の離散線積分、2次の標準ペアリング <s|σ>22-形式の離散面積分を与えます。

離散線積分/面積分に関して、ストークスの定理とポアンカレの補題が成立します。境界作用素 Bk:Ck(K)→Ck-1(K) をガンマ基底を使って次のように定義します。

  • B2A,B,C) = γB,C - γA,C + γA,B
  • B1A,B) = γB - γA

定理の記述は次のようになります。

  • ストークスの定理 1-2次元: <B2s|ω> = <s|D1ω>
  • ストークスの定理 0-1次元: <B1a|f> = <a|D0f>
  • ポアンカレの補題: 単一の三角形 {A, B, C} に関して、この三角形だけから作った単体複体をLとすると、Lのド・ラーム・コホモロジーはすべての次数でゼロ空間になる。i.e. Hk(L) = O (k = 0, 1, 2)。

内積と随伴線形写像

今まで、k-形式〈k-コチェーン〉の空間Ωk(K)に内積はありませんでした。内積を入れましょう。Ωk(K)に内積を入れることは、連続(多様体)の場合にリーマン計量を与えることに相当します。

ここでは、もっとも簡単な形の内積を考えます。一番単純な内積を採用しても、実用的モデルとして十分使えます。

 (f|g)_0 ¥: :=¥, ¥sum_{A ¥in K^{<}_0} f(A)g(A)

 (¥omega|¥rho)_1 ¥: :=¥, ¥sum_{(A, B) ¥in K^{<}_1} ¥omega(A, B)¥rho(A, B)

 ({¥bf ¥sigma}|{¥bf ¥tau})_2 ¥: :=¥, ¥sum_{(A, B, C) ¥in K^{<}_2} {¥bf ¥sigma}(A, B, C){¥bf ¥tau}(A, B, C)

この内積により、デルタ基底は正規直交基底になります。逆の言い方をすれば、デルタ基底を正規直交基底にする内積を入れたのです。

有限次元ベクトル空間においては、内積を入れると、内積を入れた空間とその双対空間のあいだの線形同型が誘導されます。今の場合、次の同型が誘導されます。

  • Ω0(K) ¥stackrel{¥sim}{=} C0(K)
  • Ω1(K) ¥stackrel{¥sim}{=} C1(K)
  • Ω2(K) ¥stackrel{¥sim}{=} C2(K)

この同型も非常に単純で、デルタ基底とガンマ基底の1:1対応(下)を線形拡張したものです。

  • δA ←→ γA
  • δA,B ←→ γA,B
  • δA,B,C ←→ γA,B,C

この「デルタ←→ガンマ 対応」は、単純で自然なため、しばしばΩk(K)とCk(K)が区別できなくなります。これは良い点(話が単純になる)もあり、悪い点(違うものを混同する)もあります。区別はしながらも、ほとんど同じだと考えましょう。

一般に、内積空間のあいだの線形写像があると、逆向きの随伴線形写像を作ることができます。Ωk(K)達に内積が入れば、ド・ラーム複体の余境界作用素 Dkk(K)→Ωk+1(K) の随伴線形写像を定義できるので、それらを Akk→Ωk-1 とします。次のような感じになります。

詳しくは「ド・ラーム・コホモロジーとホッジ分解のオモチャ (2/2) // 内積ベクトル空間と随伴線形写像」を参照。

Akk(K)→Ωk-1(K) は、余境界作用素の随伴線形写像なので、そのまんま随伴余境界作用素〈adjoint coboundary operator〉、またはベルトラミ作用素〈Beltrami operator〉と呼びます。余境界作用素の系列と、随伴余境界作用素の系列の双方向系列を備えたΩk(K)達を、ここではド・ラーム/ホッジ複体〈de Rham-Hodge complex〉と呼びましょう。通常、これもド・ラーム複体と呼んでしまうのですが、随伴系列があるとホッジ理論(後述)が構成できます。

離散外解析/離散ベクトル解析

今までの話は、基本的には線形代数の議論です。味気ない・色気ないという印象はまぬがれないですね。ここから先では、K = K(G) のド・ラーム/ホッジ複体Ωk(K)に、離散物理的な意味付けを与えます。直感に訴えるカラフル・ヴィヴィッドな描像が得られます。

多様体M上の解析(微積分)を、外微分解析〈exterior differential calculus〉/ベクトル解析〈vector calculus〉と呼びます。外微分解析は微分形式(の場)の微積分、ベクトル解析はベクトル場の微積分です。離散の場合に「微分」を付けるのはさすがに抵抗があるので、「微分形式→形式」「外微分解析→外解析」とします。

まず、離散空間である G = (V, E, T) 上の“ベクトル場”を定義しましょう。Gは、有限無向単純グラフだったので、もともと向き〈direction, orientation〉はないことに注意してください。ベクトル場〈vector field〉は、Gに向きと大きさを与えます。

G上のベクトル場の定義を、インフォーマル・図形的に与えます。Gの無向辺 {A, B} ごとに、その向き〈direction〉を、次のいずれかひとつを実行して与えます。

  1. AからBに向けた矢印 A→B を描く。
  2. BからAに向けた矢印 B→A を描く。
  3. 矢印を描かない。

次に大きさ〈magnitude〉を割り当てます。

  1. A→B または B→A の矢印には、正の実数を大きさとして割り当てる。
  2. 矢印を描かなった辺には、大きさ0を割り当てる。

次の絵はGとG上のベクトル場の例です。

G上のベクトル場をフォーマルに定義すると、1-形式(1-コチェーンともいう)の定義と同じになってしまいます。ベクトル場とは、1-形式に対する別な見方です。ただし、心理的(メンタル)には別物と思っていたほうがいいかも知れません(連続の場合、ベクトル場は1-形式の双対なので)。

連続(多様体)の場合、ベクトル場は多様体上の流れ〈flow〉を誘導します(下の図)。なので、ベクトル場と流れを同義語のように扱う場合もあります。離散の場合も、ベクトル場と流れは、ほぼ同義語として扱います。

*6

離散空間=無向グラフ上の流れは、電気回路〈electric circuit〉や液体パイプ網〈liquid piping network/system〉のモデルと考えるといいでしょう。ベクトル場は、流れの速度や勢いを表します。

離散1-形式を流れと解釈した場合、Ωk(K)の要素は次のような物理的解釈を持ちます。

0-形式 ∈Ω0(K) ポテンシャル または 湧き出し量/吸い込み量
1-形式 ∈Ω1(K) 流れ
2-形式 ∈Ω2(K) 渦源〈うずげん | かげん〉

ポテンシャルは、電気回路なら電位です。液体パイプ網なら、頂点にタンクがあるとしてタンクの水量とか位置(高度)かな。湧き出し/吸い込みの量は、頂点が外部と入出力をしているとして、頂点から(電流や液体が)湧き出す/吸い込まれる量です。渦源〈vortex source〉は、三角形の内部にあって、渦を引き起こす源〈みなもと〉。渦源があると、三角形の周囲に循環流〈circulation flow〉が発生します。

離散解析の4つの作用素

2次元のド・ラーム/ホッジ複体では、4つの作用素(線形写像)が出てきます。

  1. D00(K)→Ω1(K) 0次余境界作用素
  2. D11(K)→Ω2(K) 1次余境界作用素
  3. A22(K)→Ω1(K) 2次随伴余境界作用素
  4. A11(K)→Ω0(K) 1次随伴余境界作用素

前節の物理的解釈を念頭に、これらの作用素に別名を与えます。

  1. grad = D00(K)→Ω1(K)
  2. curl = D11(K)→Ω2(K)
  3. circ = A22(K)→Ω1(K)
  4. div = A11(K)→Ω0(K)

gradを勾配〈gradient〉、curl回転curl | rotation〉、circを循環〈circulation〉、divを発散〈divergence〉と呼びます。これらの言葉は、3次元の(普通の)ベクトル解析でお馴染みでしょう。3次元ベクトル解析では、curlとcircの区別がないのですが、それは計算上の差がないからと、違う作用素を同一視しているせいです(よくない)。

gradとcurlの具体的な表示(定義)は既にありますが、circとdivも具体的に表示できます。そのために、無向グラフ上での隣接点〈adjacent point/vertex〉という概念を使います。

  • A∈V の隣接点とは、{A, B}∈E となる点B
  • {A, B}∈E の隣接点とは、{A, B, C}∈T となる点C

Aの隣接点の全体(からなる集合)をAdja(A)、{A, B}の隣接点の全体をAdja(A, B)と書くことにします*7。隣接点を使って、circ, div は次のように書けます。

 (circ ¥,{¥bf ¥sigma})(A, B) ¥: :=¥: ¥sum_{X¥in Adja(A, B)} {¥bf ¥sigma}(A, B, X)

 (div ¥,¥omega)(A) ¥: :=¥: ¥sum_{X¥in Adja(A)} ¥omega(A, X)

この具体的定義と、随伴線形写像としての定義が一致することは計算で確認できます。これらの定義の直感的意味は次のとおりです。

  • (circ σ)(A, B) : 辺{A, B}を含む三角形{A, B, X}(の渦源)による循環流の、A→B方向の流量(実数値)を、Xを動かして足し合わせた量。
  • (div Ω)(A) : 辺{A, X}の、A→X方向の流量(実数値)を、Xを動かして足し合わせた量。

以下では、1-形式、ベクトル場のことも“流れ”と表現するので気をつけてください。正確に言えば「1-形式/ベクトル場から誘導された流れ」です。

  1. 流れωが、ポテンシャルfにより ω = grad f = D0(f) と書けるとき、ωを勾配流〈gradient flow〉と呼びます。
  2. 流れωが、curl ω = D1(ω) = 0 のとき、無回転流〈irrotational flow | curl-free flow〉と呼びます。
  3. 流れωが、渦源σにより ω = circ σ = A2(σ) と書けるとき、ωを循環流〈circulation flow〉と呼びます。
  4. 流れωが、div ω = A1(ω) = 0 のとき、無発散流〈divergence-free flow〉と呼びます。

無回転流は、本田圭佑や乾貴士のシュート・テクニックみたいなので、渦無し流れという言葉も使います。無発散流は、外部との入出力(流入と流出)がないので、出入り無し流れとも言うことにします。また、div ω = 0 は物理の非圧縮性流体の連続の方程式(保存則)に類似なので、ωを保存流〈conservative flow〉とも呼びます。

ド・ラーム複体の性質として Dk+1¥circDk = 0 なので、次が成立します。

勾配流 grad f の回転がゼロになるので、ポテンシャルfによる勾配流は必ず渦無しです。

随伴線形写像に関して Ak-1¥circAk = 0 が成立するので、

  • div circ σ = 0

循環流 circ σ の発散がゼロになるので、渦源σによる循環流は必ず出入り無しの保存流です。

次に述べるホッジ分解は、勾配流、無回転流(渦無し流れ)、循環流、無発散流(出入り無し流れ)のあいだの、もっと精密な関係を与えます。

ホッジ分解

ド・ラーム/ホッジ複体のホッジ分解〈Hodge decompsition〉とは、各次元のコチェーン空間Ωk(K)に対して、直交直和分解を与えるものです。主たる興味は k = 1 のところ、Ω1(K) の分解です*8。ベクトル空間Ω1(K)は1-形式〈1-コチェーン〉の空間ですが、既に述べたように、G上のベクトル場の空間、あるいはG上の流れの空間ともみなせます。

ド・ラーム/ホッジ複体のなかで、Ω1(K)を余域〈終域〉とする作用素が2つ、Ω1(K)を域〈始域〉とする作用素が2つあります。

  1. grad = D0 : Ω1(K)が余域
  2. circ = A2 : Ω1(K)が余域
  3. curl = D1 : Ω1(K)が域
  4. div = A2 : Ω1(K)が域

Ω1(K)を余域とする作用素ではその像空間を、Ω1(K)を域とする作用素ではその核空間を考えると、Ω1(K)に4つの部分空間が定義できます。それぞれの部分空間の要素の呼び名を記します。(呼び名の整理については、「ド・ラーム・コホモロジーとホッジ分解のオモチャ (2/2) // 多様体から線形代数へ」参照。)

要素 一般的な呼び名 流れモデルの呼び名
Ωk(M)の要素 1-コチェーン 流れ
Im(grad)の要素 1-コバウンダリ 勾配流
Im(circ)の要素 1-随伴コバウンダリ 循環流
Ker(curl)の要素 1-コサイクル 無回転流(渦無し)
Ker(div)の要素 1-随伴コサイクル 無発散流(出入りなし)

ベクトル空間Ω1(K)の部分空間 Im(grad), Im(circ), Ker(curl), Ker(div) の関係は、次の図のようになります。

このような部分空間の相互関係を教えてくれるのが、ホッジの定理です。ド・ラーム/ホッジ複体の定義から、「勾配流の空間 ⊆ 無回転流の空間」と「循環流の空間 ⊆ 無発散流の空間」は言えました(前節)が、さらに:

  1. 勾配流の空間(Im(grad))と無発散流の空間(Ker(div))は直交し、それらの直和はΩ1(K)になる。
  2. 循環流の空間(Im(circ))と無回転流の空間(Ker(curl))は直交し、それらの直和はΩ1(K)になる。
  3. 無回転流の空間(Ker(curl))と無発散流の空間(Ker(div))の共通部分(Ker(culr)∩Ker(div))を調和流〈harmonic flow〉の空間と呼ぶ(これは定義)。
  4. 勾配流の空間(Im(grad))と循環流の空間(Im(circ))と調和流の空間(Ker(culr)∩Ker(div))は互いに直行し、それらの直和はΩ1(K)になる。

次の3つの直交直和分解がホッジ分解です。

  1. Ω1(K) = Im(grad) ¥oplus Ker(div)
  2. Ω1(K) = Im(circ) ¥oplus Ker(curl)
  3. Ω1(K) = Im(grad) ¥oplus Im(circ) ¥oplus (Ker(curl)∩Ker(div))

ド・ラーム/ホッジ複体の対するホッジ分解定理は、純粋に代数的に証明できます。次を参照してください。

調和流の空間は、Ker(curl)∩Ker(div) として定義しましたが、ラプラシアン(という作用素)の核空間としても定義できます。それについては:

ホッジ分解のランキング問題への応用

... TBD ...

*1:ここで登場する単体複体は、グラフの2-クリーク複体〈2-clique complex〉と呼ばれるものです。

*2:k-単体と呼んでもいいのですが、ここでの定義では、非退化な単体しか考えてないのでセルと呼ぶことにしました。

*3:「混ぜてカリー化」は、どう考えても料理の手法。

*4:Ω-1(K) := O = ゼロ空間、Ω3(K) := O、D-1-1(K)→Ω0(K)、D22(K)→Ω3(K) と定義すると、次数付けの辻褄は合います。D-1の(-1)は逆写像じゃなくて、単なる番号です。まー、次数付けの整合性は気にするほどのことではないでしょう。

*5:ポテンシャルは、スカラー体や1次元ベクトル空間に値をとるというより、1次元アフィン空間に値をとるので、原点の選び方は自由です。

*6:画像: https://en.wikipedia.org/wiki/Vector_field#/media/File:VectorField.svg より

*7:AdjでなくAdjaとしたのは、adjointやadjunctionと誤解されないようにです。

*8:k = 1 のホッジ分解をヘルムホルツ分解〈Helmholtz decomposition〉とも呼びます。

2018-08-03 (金)

TypeScriptで(無理して)論理式: 言霊排除

| 13:55 | TypeScriptで(無理して)論理式: 言霊排除を含むブックマーク

論理的議論は、日常生活の情念や雑念を取り払った、シンプルでドライなスタイルで遂行します。例えば、日常会話においては、「Aである」と「Aでなくはない」の意味は違います(違いをうまく説明できないけど)。論理(古典論理*1)では、「Aである」と「Aでなくはない」は完全に同じです。日常言語の微妙さ・煩雑さを切り捨て、理想化・単純化することにより、強靭な推論能力が手に入るのです。

日常言語を使っているかぎり、日常の論理、あるいは日常の非論理が混ざり込むことは避けられません。論理的推論のための人工言語を使うのが望ましいでしょう。そこで、プログラミング言語TypeScriptを(かなり無理クリに)使って、論理的命題の記述を試みてみます。

本文中の例題を実行してみたい方は、最後の節を先に見てください。

内容:

  1. 命題と真偽判定とは何であるか
  2. TypeScriptを使う
  3. 言霊の影響からの脱却
  4. なぜTypeScriptなのか
  5. 論理結合子
  6. 含意命題
  7. 全称命題
  8. 全称命題の実行の仕掛け(インチキ)
  9. 含意と全称について考える
  10. まだ先があるけれど
  11. HTML/JavaScript/TypeScriptコード

命題と真偽判定とは何であるか

次の文を考えてみましょう。

  • xは大きい数である。

この文は、普通は「命題ではない」と言われます。なぜかというと、大きい数かどうかの真偽判定の基準がないからです。であるなら、真偽判定の基準を作ればいいだけです。そのとき、日本語で基準を書かないでプログラミング言語で書くことにします。

JavaScriptで書いてみます。

function isLarge(x) {
    return (x > 100);
}

ブラウザのコンソールで実験してみれば:

>> isLarge(3)
   false
>> isLarge(100)
   false
>> isLarge(100.01)
   true
>> isLarge(200)
   true

上から順に:

  1. 「3 は大きい数である。」は偽
  2. 「100 は大きい数である。」は偽
  3. 「100.01 は大きい数である。」は真
  4. 「200 は大きい数である。」は真

と真偽判定できています。通常の表現では、「は真」は省略して、「は偽」を「ではない」と言うので:

  1. 「3 は大きい数である。」ではない
  2. 「100 は大きい数である。」ではない
  3. 「100.01 は大きい数である。」
  4. 「200 は大きい数である。」

日本語の言い回しと、鍵括弧・句読点を調整して:

  1. 3 は大きい数ではない。
  2. 100 は大きい数ではない。
  3. 100.01 は大きい数である。
  4. 200 は大きい数である。

真偽判定とはこういうものです。「大きい数である」の基準を定義すれば、それだけで真偽判定が可能となります。このとき:

  • 「大きい数である」とは何か? を国民投票で決める必要はありません。
  • 知人を集めて会議を開く必要もありません。
  • 哲学的議論も不要です。(むしろ、不毛です。)
  • 国語辞書を引く必要もありません。
  • 社会通念に合致しているかを検討する必要もありません。

単に、真偽値(trueまたはfalse)を返す関数を定義するだけです。

関数名isLargeは英語の句"is large"からとっているので、意味が推測できますが、次の関数を代わりに使ってもかまいません。関数名の選択も全く自由です*2

// 一文字の名前
function L(x) {
    return (x > 100);
}

あるいは、

// 意味不明な名前
function taboncha_hoy(x) {
    return (x > 100);
}

またあるいは、

// 意味はわかるが、
// ふさわしいとは思えない名前
function BeerIsGood(x) {
    return (x > 100);
}

真偽値を返す関数を定義すれば、それだけで真偽判定ができる -- この極めてシンプルでドライな事実が、なかなかに理解してもらえないようです。

TypeScriptを使う

TypeScriptは、JavaScriptに対して上位互換なプログラミング言語で、洗練された機能と構文を持ちます。JavaScriptにコンパイル(トランスパイル)されて実行されるので、ブラウザ(のコンソール)で確認できます。素晴らしい!

TypeScript自体の説明はここではしません。Web上にたくさんの資料があります。僕自身もTypeScriptの記事をいくつか書いていますが、ひとつだけ(最初に書いた)記事を挙げると:

TypeScriptでは、次の形で無名関数*3を書けます。

  • (引数の宣言) : 戻り値の型 => 関数の本体

記号'=>'は、論理記号の'⇒'(意味は「ならば」)と似てますが関係ありません。関数のヘッド(見出し部)とボディ(本体部)を区切る記号です。

例えば、先のisLarge関数は、TypeScriptでは次のように書けます。

(x:number) :boolean =>(x > 100)

簡潔に書けるだけでなく、JavaScriptには無かった型宣言ができます。この関数はnumber型を引数にして、boolean型(真偽値型)の戻り値をとることを、明確に記述できます。素晴らしい!

(x:number) :boolean =>(x > 100) は無名関数ですが、そのまま引数を渡すことができます。((x:number) :boolean =>(x > 100))(3) とか ((x:number) :boolean =>(x > 100))(200) とかです。しかし、同じ関数を何度も使うときは名前がないと不便です。無名関数に名前を付けるには、次の形式を使うことにします。

let isLarge = (x:number) :boolean =>(x > 100)

1行のコードですが、解説しましょう。「let 名前 = 式」は、「名前を、式とする」とか「名前とは、式のことである」と読めばいいでしょう。この例では:

  • isLarge を、 (x:number) :boolean =>(x > 100) とする。
  • isLarge とは、 (x:number) :boolean =>(x > 100) のことである。

式の部分は既に紹介した無名関数です。この無名関数は、次のように読めます。

  • ヘッド部 (x:number) :boolean --- 型がnumberである引数xに対して、型がbooleanである戻り値を返す。
  • ボディ部 (x > 100) --- 引数xが100より大きいかどうかを判定する。

TypeScriptには型があるので、関数isLargeの引数に文字列や配列が入ることはありません。コンパイラがチェックしてくれます。しかし、数値型がnumber型しかないので、整数と実数(コンピュータでは浮動小数点数)の区別もできません。そこで、TypeScriptにはない数値型を新しく導入します。natural, integer, rational, real の4つの型です。

型の名前 対応する集合 意味
natural N 自然数の型
integer Z 整数の型
rational Q 有理数の型
real R 実数の型

これらの新しい型をほんとに導入することは、TypeScripでは(ほとんどのプログラミング言語で)出来ません。組み込み型としてサポートすべき型です。なので、実際には型の名前だけ使えて、実質はnumberです。型の名前を使えるようにする仕掛けは後の節で明かします。

数値データやオブジェクトが、natural, integer, rational, real の4つの型に所属するかどうかを判定するには、次の関数が使えます。

  1. isNatural(x:any) :boolean
  2. isInteger(x:any) :boolean
  3. isRational(x:any) :boolean
  4. isReal(x:any) :boolean

型がナンチャッテ型なので、型への所属判定もナンチャッテですが、isNaturalとisIntegerはまーまー信頼できます。

さて、数の種類を自然数に特定した次の命題を考えます。

  • 自然数xは大きい数である。

この命題に対応する真偽判定関数は次のように書けます。

let isLargeNatural = (x:natural) :boolean =>(x > 100)

引数の型がnumberからnaturalに変わっただけです。

言霊の影響からの脱却

TypeScriptで色々な命題を書いていきたいわけですが、その前に、僕がこんなことをしようとした動機を説明します。

数学的・論理的な命題を自然言語(我々にとっては日本語)で書くのは、なにかと問題があると思います。まず、自然言語は曖昧だから、正確な記述が難しいという問題が思い浮かぶでしょう。ですが、それより深刻な問題は、自然言語が強烈なイメージ喚起力を持っていることです。個々の言葉が、それぞれの人ごとに、経験や環境や状態に依存した強い連想を引き起こすこと -- これが大きな問題です。

例えば、先に扱った例である「大きい数」を「定義する」場合、「大きい数」「定義する」という日本語が、心のなかに様々な思いを湧き上がらせ、葛藤を引き起こします。

  1. 世間の人々は、どのくらいの数を「大きな数」と呼ぶんだろう?
  2. アンケート調査したほうがいいのかな?
  3. Wikipediaに「大きな数」ってないのか、調べてみよう。
  4. 「100を超えたら大きな数」って決めたら、誰かが「俺は300以上だと思う」とか言い出さないか?
  5. そもそも、ボクに「大きな数」を定義する資格なんてあるのだろうか? そんな大それた事はボクには出来ない。

我々は、社会のなかで日常生活を営んでいます。その日常において使う言語が自然言語であるため、自然言語の言葉は社会や個人と深く結びつき、言葉を使うと同時に、現実世界や感情の世界に巻き込まれます。自然言語(日本語)には言霊〈ことだま〉が宿るとかいいますが、強烈なイメージ喚起力は言霊のパワーなのかも知れません。

数学的・論理的な命題の記述と解釈においては、言霊の影響 -- 現実世界や感情の世界への連想・参照 -- をできるだけ排除したい。命題を記述・解釈するとき、今日の天気も気分も株価も、消費税率も世界情勢も関係ないのです。ひたすらドライに真偽判定だけに注目します。

定義(それと公理)は、真偽判定をする際のベースを与えるものです。誰がどんな定義をしようが全く自由です。何の資格も要らないし(定義士2級試験とかない!)、明確であれば(真偽判定が実際にできれば)内容的制限もありません。矛盾したらマズイのですが、あえて「俺は矛盾した体系が作りたい」のであれば、それさえも自由です。

数学的・論理的な定義をするとき、あるいは公理を提示するとき、あなたの家族や友人や会社に許可を取る必要はないし、社会通念や多数派の意見を考慮する必要はないし、国語辞書やWikipediaを引用する必要もありません。それらを無視しろ、ということではなく、単に関係ないのです。ひたすら関係ないのです。

なんか誤解されそうな言い方をしてますが、一旦誤解されてその誤解を解くほうが楽なんで、今言ったことに注釈や補足を付けることはしません*4。ともかく、命題を扱う際は真偽判定に集中してください。言霊の影響を断ち切ってください。

なぜTypeScriptなのか

言霊の影響を断ち切るには、自然言語を使うのをやめて人工言語を使えばいいのです。標準的な(ポピュラーな)人工言語は、古典述語論理とラムダ計算でしょう。しかし、これらの言語にどうも馴染めない、という人もいるし、ソフトウェアで構文をチェックしたり実行したりするすることが(お手軽には)できません。

CoqIsabelleMizarなんてプログラミング言語もありますが、これらも敷居が高いので、普通のプログラミング言語(汎用プログラミング言語)を使うことにします。そう、TypeScriptです。TypeScriptがサンプル記述に向いていることは次の記事で書いています(興味があれば見てください)。

TypeScriptは、命題や証明の記述を目的にしてないので、うまくいかない事も多々あるんですが、そこは姑息な小手先の対処で乗り切りましょう。小手先の対処なので、実用性はありません。しかしそれでも、古典述語論理・ラムダ計算入門の素材、言霊の呪縛から逃れる手段としては使えると思います。

論理結合子

2つの命題を結びつけたり、命題の意味を変える演算子を論理結合子〈logical connective〉といいます。次の対応表を見るのが早いでしょう。

名称 意味 論理記号 TypeScript
連言 かつ &&
選言 または ||
否定 ではない ¬ !, not
含意 ならば ⇒, ⊃ ? : true

論理記号は比較的よく使われているものを選びました。他の論理記号については次の記事を見てください(興味があれば)。

TypeScriptの(というかJavaScriptの)演算子 &&, ||, ! は、論理の「かつ〈and〉」「または〈or〉」「ではない〈not〉」と同じか? と聞かれると、「いや、違う」と答えざるを得ないのですが、我々の目的内では論理的な演算子と解釈しても大丈夫です。否定の ! は、not関数の形も許します。「ならば〈implies〉」として使う ? : true は、三項演算子の最後の項(引数)にtrueを入れたものです。

isLarge(x:number) :boolean が既に定義されているとして、論理結合子〈論理演算子〉を使った例を見てみましょう。

let bothAreLarge = (x:number, y:number) :boolean =>(isLarge(x) && isLarge(y))

let atLeastOneIsLarge = (x:number, y:number) :boolean =>(isLarge(x) || isLarge(y))

let isNotLarge = (x:number) :boolean =>(not(isLarge(x)))

let bothAreNotLarge = (x:number, y:number) :boolean =>(isNotLarge(x) && isNotLarge(y))

ブラウザで試してみます。

>> bothAreLarge(30, 200)
   false
>> bothAreLarge(300, 200)
   true
>> atLeastOneIsLarge(0, 100.01)
   true
>> atLeastOneIsLarge(200, 100.01)
   true
>> bothAreNotLarge(0, 100.01)
   false
>> bothAreNotLarge(0, 100)
   true

人工言語であるTypeScriptの実行結果を、自然言語である日本語に翻訳すれば次のようになります。

  1. 「30 と 200 の両方とも大きな数である。」は偽
  2. 「300 と 200 の両方とも大きな数である。」は真
  3. 「0 と 100.01 の少なくともひとつは大きな数である。」は真
  4. 「200 と 100.01 の少なくともひとつは大きな数である。」は真
  5. 「0 と 100.01 の両方とも大きな数ではない。」は偽
  6. 「0 と 100 の両方とも大きな数ではない。」は真

日本語の言い回しと、鍵括弧・句読点の調整は皆さんにお任せします。

含意(「ならば」)の使用例は次節にします。

含意命題

そろそろ「大きな数」の例も飽きてきたので、別な例題にします。自然数(非負の整数)だけを考えることにして、次の命題を例にします。

  • x は y の倍数である。

TypeScriptで定義します。

let isMultipleOf = (x:natural, y:natural)/*{y !== 0}*/ :boolean =>(x % y === 0)

解説します。

  • 命題の真偽判定をする関数の名前は isMultipleOf です。
  • 引数は2つで、型はどちらも natural(自然数)です。
  • /*{y !== 0}*/ は、第二引数 y に0は入れないでね、という制約です。コメントなので実効性はありませんが、守ってくれると信じましょう。
  • 関数の戻り値は boolean(真偽値)です。
  • 関数の本体は、引数 x を引数 y で割り算した余りを求めて0と比較するだけです。'%'は割り算の余りを求める演算子、'==='は等号です*5

ちょっとだけ試してみます。

>> isMultipleOf(4, 2)
   true
>> isMultipleOf(2, 4)
   false
>> isMultipleOf(12, 4)
   true
>> isMultipleOf(5, 4)
   false
>> isMultipleOf(5, 5)
   true

説明はいらないでしょう。

さて、次の2つの命題を考えます。

  1. 4の倍数は2の倍数である。
  2. 4の倍数は3の倍数である。

もっとハッキリと言えば:

  1. x が 4 の倍数であるなら、x は 2 の倍数でもある。
  2. x が 4 の倍数であるなら、x は 3 の倍数でもある。

日本語としてのテニヲハとか句読点とかはどうでもいいので、

  1. x は 4 の倍数である ならば x は 2 の倍数である。
  2. x は 4 の倍数である ならば x は 3 の倍数である。

これらの命題は、TypeScriptで次のように書きます。

let multipleOf4IsMultipleOf2 = (x:natural) :boolean =>(
    isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true )

let multipleOf4IsMultipleOf3 = (x:natural) :boolean =>(
    isMultipleOf(x, 4) ? isMultipleOf(x, 3) : true )

「A ならば B」(記号的には「A ⇒ B」)という命題は、TypeScriptでは

  • A ? B : true

という形で書きます。'?'と':'の組み合わせに慣れてない方は、次のif文と同じと思ってください。

if (A) {
    return B;
} else {
    return true;
}

一番目の命題を、JavaScript構文とif文で書けば:

function multipleOf4IsMultipleOf2(x) {
    if (isMultipleOf(x, 4)) {
        return isMultipleOf(x, 2);
    } else{
        return true;
    }
}

「A ならば B」の形の命題を含意命題〈conditional proposition | 条件命題〉と呼びます。Aを含意命題の前件〈antecedent〉と呼び、Bは後件〈succedent〉と呼びます。前件が偽のときは、含意命題全体は真になります。これも、哲学的・言語学的思弁にふけらないで、含意〈implication〉とはそういうものだ、と割り切ってください*6。「ならば」という日本語や、日本語を使う個人・社会を分析するのではなく、上に示したようなプログラムの挙動が分析の対象です。

では、実行して試してみます。

>> multipleOf4IsMultipleOf2(1)
   true
>> multipleOf4IsMultipleOf2(2)
   true
>> multipleOf4IsMultipleOf2(4)
   true
>> multipleOf4IsMultipleOf3(12)
   true
>> multipleOf4IsMultipleOf3(24)
   true

日本語に翻訳すれば:

  1. 「1 は 4 の倍数である ならば 1 は 2 の倍数である。」は真
  2. 「2 は 4 の倍数である ならば 2 は 2 の倍数である。」は真
  3. 「4 は 4 の倍数である ならば 4 は 2 の倍数である。」は真
  4. 「12 は 4 の倍数である ならば 12 は 3 の倍数である。」は真
  5. 「24 は 4 の倍数である ならば 24 は 3 の倍数である。」は真

1番目、2番目の命題で、「1 は 4 の倍数である」「2 は 4 の倍数である」は偽なので、全体は真です。こう真偽判定しないとダメな理由は次節以降で明らかになります。

全称命題

もう一度、前節で扱った2つの命題を挙げます。

  1. x が 4 の倍数であるなら、x は 2 の倍数でもある。
  2. x が 4 の倍数であるなら、x は 3 の倍数でもある。

1番目は真だが、2番目は偽のように思えます。しかし、2番目の命題が真になることもあるのは実験で確認済みです。これも再掲しましょう。

>> multipleOf4IsMultipleOf3(12)
   true
>> multipleOf4IsMultipleOf3(24)
   true

xの値を12や24にしたときは、「x が 4 の倍数であるなら、x は 3 の倍数でもある。」は真になります。それなのに、2番目の命題は偽だと判断する根拠は何でしょう? これは、ヨーク考えてみるべきことです。

我々が、変数を含む命題を解釈するとき、「どんな場合でも」「いつでも」「常に」といった言葉を先頭に付けているのです(無意識かも知れませんが)。「どんな場合でも」を先頭に付けると:

  1. どんな場合でも、x が 4 の倍数であるなら、x は 2 の倍数でもある。
  2. どんな場合でも、x が 4 の倍数であるなら、x は 3 の倍数でもある。

そうなると、たまたまxの特定の値で命題が成立しても、「どんな場合でも」とは言えません。実際、x = 4 で実験すると:

>> multipleOf4IsMultipleOf3(4)
   false

これが、2番目が偽である理由です。

「どんな場合でも」をもっと正確に言うと「x がどんな数であっても」です。数の種類(型)は自然数(natural型)だとしていたので、「x がどんな自然数であっても」です。論理記号では「∀x∈N」と書きます。記号'∀'は、"Any", "All"の"A"をひっくり返したものです。"for all x in natural"のように読みます。論理記号'∀'で始まる命題を全称命題〈universal proposition〉と呼びます。

全称命題を日本語で言うときは、「どんな自然数xでも」「すべての自然数xは」「任意の自然数xにおいて」「勝手に取った自然数xに対して」など様々な言葉使いをします。日本語表現の微妙な差異を分析するとかやりだすと*7、ラチがあかない、どうにもならないのでやめましょうね。くどく言いますが、我々は日本語を調査・分析したいのではありません! むしろ日本語を使いたくないのです。

さて、∀x∈N.( … ) をTypeScriptでどう書けばいいでしょう。

  • forAll(x:natural)( isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true )

のように書けたら非常によいのですが、これは無理です。

  • forAll( (x:natural)=>( isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true) )

これでもいいですね。forAllの内部は無名関数です。forAllを、何もしないダミー関数として定義すれば、この書き方が出来ますが、実行は無意味になってしまいます。

多少は意味がある実行をするために、次の書き方とします。naturalを二度書く必要がありますが、我慢してください*8

  • natural.forAll( (x:natural)=>( isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true) )

ところで、forAllのなかに入っている関数は既に名前が付いてました。以下に再掲。

let multipleOf4IsMultipleOf2 = (x:natural) :boolean =>(
    isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true )

この名前 multipleOf4IsMultipleOf2 を無名関数の代わりに使っても同じです。

  • natural.forAll(multipleOf4IsMultipleOf2)

実験してみます。

>> natural.forAll(multipleOf4IsMultipleOf2)
   true
>> natural.forAll(multipleOf4IsMultipleOf3)
   false

期待通りの結果になりました。種明かしは次節でします。

なお、注意事項ですが、TypeScriptソースコード上では natural.forAll( (x:natural)=>( isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true) ) のように書けますが、ブラウザのコンソールでTypeScriptは使えないので、JavaScriptの書き方をしなくてはなりません(泣)。natural.forAll( function(x){return isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true} ) ですね。僕は、コンソールにTypeScript式を入れて、構文エラーでしばらく困惑してました、ダハハハ。

全称命題の実行の仕掛け(インチキ)

例題である全称命題を再度確認しましょう。

  • 日本語: どんな場合でも、x が 4 の倍数であるなら、x は 2 の倍数でもある。
  • より正確な日本語: 任意の自然数 x に対して、x が 4 の倍数である ならば x は 2 の倍数である。
  • 論理式: ∀x∈N.( isMultipleOf(x, 4) ⇒ isMultipleOf(x, 2) )
  • TypeScript: natural.forAll( (x:natural)=>(isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true) )

この命題の真偽判定をするには、変数xにすべての自然数を代入して確認する必要があります。自然数は無限個あるので、そんなことがコンピュータに出来るはずもなく、実行はハナからインチキだと分かります。

インチキの手口を紹介しましょう。まず、配列変数naturalが次のように定義されています。

var natural = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9];

配列のメソッドforAllが事前に定義されていて、natural.forAll(fn) と呼び出すと、次のコードと同じ働きをします。

    var len = natural.length;
    var result = true;
    var i;
    for (i = 0; i < len; i++) {
        result = result && fn(natural[i]);
    }
    return result;

要するに、0から9の10個の自然数に対してだけ関数値(boolean型の値になる)をチェックして、全部trueならtrueを、そうでないならfalseを返すのです。natural.forAll(fn) の値は、次の長い式の値と同じです。

fn(0) && fn(1) && fn(2) && fn(3) && fn(4) &&
fn(5) && fn(6) && fn(7) && fn(8) && fn(9)

含意と全称について考える

「ならば」(論理記号では'⇒')と「任意の」(論理記号では'∀')を含むような命題は非常にしばしば登場します。「4の倍数は2の倍数である。」は次のように書けたのでした。

  • より正確な日本語: 任意の自然数 x において、x は 4 の倍数である ならば x は 2 の倍数である。
  • 論理式: ∀x∈N.( isMultipleOf(x, 4) ⇒ isMultipleOf(x, 2) )
  • TypeScript: natural.forAll( (x:natural)=>( isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true ) )

全称命題は、「どんな場合でも成立する」と主張するので、この場合「x = 0 でも、x = 1 でも、x = 2 でも、x = 3 でも、x = 4 でも、x = 5 でも、その他 x がどんな自然数でも」ということです。

  • x = 0 のとき: 0 は 4 の倍数である ならば 0 は 2 の倍数である。
  • x = 1 のとき: 1 は 4 の倍数である ならば 1 は 2 の倍数である。
  • x = 2 のとき: 2 は 4 の倍数である ならば 2 は 2 の倍数である。
  • x = 3 のとき: 3 は 4 の倍数である ならば 3 は 2 の倍数である。
  • x = 4 のとき: 4 は 4 の倍数である ならば 4 は 2 の倍数である。
  • x = 5 のとき: 5 は 4 の倍数である ならば 5 は 2 の倍数である。
  • … …

ここでもし、「0 は 4 の倍数である ならば 0 は 2 の倍数である。」を偽と判定すると、x = 0 の時点で命題は成立せず、「どんな場合でも成立する」と主張できるはずありません。含意命題の前件「0 は 4 の倍数である」が偽のときは、これはヨシ(つまり真)として、さっさと先に進むのです。

もう一方の命題「4の倍数は3の倍数である。」も考えてみましょう。

  • より正確な日本語: 任意の自然数 x において、x は 4 の倍数である ならば x は 3 の倍数である。
  • 論理式: ∀x∈N.( isMultipleOf(x, 4) ⇒ isMultipleOf(x, 3) )
  • TypeScript: natural.forAll( (x:natural)=>( isMultipleOf(x, 4) ? isMultipleOf(x, 3) : true ) )

「どんな場合でも成立する」と主張しているので、

  • x = 0 のとき: 0 は 4 の倍数である ならば 0 は 3 の倍数である。
  • x = 1 のとき: 1 は 4 の倍数である ならば 1 は 3 の倍数である。
  • x = 2 のとき: 2 は 4 の倍数である ならば 2 は 3 の倍数である。
  • x = 3 のとき: 3 は 4 の倍数である ならば 3 は 3 の倍数である。
  • x = 4 のとき: 4 は 4 の倍数である ならば 4 は 3 の倍数である。
  • x = 5 のとき: 5 は 4 の倍数である ならば 5 は 3 の倍数である。
  • … …

このなかで注目すべきは、「4 は 4 の倍数である ならば 4 は 3 の倍数である。」です。含意命題の前件「4 は 4 の倍数である」は真ですが、後件「4 は 3 の倍数である」が偽です。これは、もとの主張に対する反例です。反例が見つかったので全称命題は偽です。しかし、最初の「0 は 4 の倍数である ならば 0 は 3 の倍数である」は反例ではありません。なぜなら、この命題は真だからです。

今の例では、xが0から9の範囲で反例が見つかって偽と判定できましたが、コンピュータでの実行では、調べた範囲に反例が見つからないでtrueを返すこともあります。無限に調べられないので、コンピュータからの報告は当てになりません!

  • 有限個の自然数を調べて全て真でも、自然数全体で真とは保証できない。

0から9の範囲を広げて、0から百兆にしたところで事情は変わりません。だから、実験ではなくて証明が必要になるのです。

まだ先があるけれど

全称命題は紹介しましたが、全称とペアになる存在命題があります。また、「ただひとつだけ存在する」を意味する存在命題(一意存在命題)も重要です。一意存在命題に基づいて関数を定義することが非常にしばしばあります。例えば:

  • 日本語: 実数 a に対して、a が非負なら、x2 = a かつ x ≧ 0 である実数xがただひとつだけ存在する。
  • 論理式: ∀a∈R.( a ≧ 0 ⇒ ∃!x∈R.( x2 = a ∧ x ≧ 0 ) )
  • TypeScript:すぐ下(↓)
real.forAll( (a:real)=>(
        a >= 0 ?
        real.uniquelyExists( (x:real)=>(
                x*x === a &&
                x >= 0 )
        ) : true )
)

'∃!'と'uniquelyExists'は、一意存在の論理記号です。この一意存在命題に基づいて非負平方根関数が定義されます。そのとき、「… であるところの x」という意味の論理記号が使われます。

このへんの話はちょっと難しいのでまたの機会にします。今日のところは、日本語表現にまとわりつく余計な情感や怨念(?)、邪魔になる意味的夾雑物を取り除くためにプログラミング言語表現が使えることが分かれば十分です。

HTML/JavaScript/TypeScriptコード

ブラウザで実験したいときは、次のようなHTMLファイルを作ります。

<!DOCTYPE html>
<html>
  <head>
    <meta charset="utf-8">
    <title>logical</title>
    <script src="./logical-support.js"></script>
    <script src="./logical.js"></script>
    <script src="./my-sample.js"></script>
  </head>
  <body>
    <h1>logical</h1>
  </body>
</html>

読み込んでいるJavaScriptファイルのなかで、logical-support.jsは直接JavaScriptで手書きしたファイルです。「今どき、prototype使いやがって」と怒られそうですが、これしか手段が思いつかなくて …

/* logical-support.js */

Array.prototype.forAll = function(condFn) {
    var arr = this;
    var len = arr.length;
    var result = true;
    var i;
    for (i = 0; i < len; i++) {
        result = result && condFn(arr[i]);
    }
    return result;
}

Array.prototype.exists = function(condFn) {
    var arr = this;
    var len = arr.length;
    var result = false;
    var i;
    for (i = 0; i < len; i++) {
        result = result || condFn(arr[i]);
    }
    return result;
}

Array.prototype.uniquelyExists = function(condFn) {
    var arr = this;
    var len = arr.length;
    var count = 0;
    var i;
    for (i = 0; i < len; i++) {
        if (condFn(arr[i])) {
            count++;
        }
    }
    return (count === 1);
}

Array.prototype.the = function(condFn) {
    var arr = this;
    var len = arr.length;
    var count = 0;
    var item;
    var i;
    for (i = 0; i < len; i++) {
        if (condFn(arr[i])) {
            count++;
            item = arr[i];
        }
    }
    if (count !== 1) throw "Not exist or Not unique";
    return item;
}

logical.jsとmy-sample.jsは、対応するTypeScriptファイルをコンパイルしたものです。先にコンパイル済みのJavaScriptコード、その後にTypeScriptソースコードを示します。

// logical.ts
var natural = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9];
var integer = [-5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5];
var rational = [-2, -1.5, -1, -0.5, 0, 0.5, 1, 1.5, 2];
var real = [-2, -1.5, -1, -0.5, 0, 0.5, 1, 1.5, 2];
var isNatural = function (x) { return ((typeof x) === 'number' &&
    Math.ceil(x) === x &&
    x >= 0); };
var isInteger = function (x) { return ((typeof x) === 'number' &&
    Math.ceil(x) === x); };
var isRational = function (x) { return ((typeof x) === 'number'); };
var isReal = function (x) { return ((typeof x) === 'number'); };
var not = function (x) { return (!x); };
// my-sample.ts
/// <reference path="./logical.ts" />
var isLarge = function (x) { return (x > 100); };
var bothAreLarge = function (x, y) { return (isLarge(x) && isLarge(y)); };
var atLeastOneIsLarge = function (x, y) { return (isLarge(x) || isLarge(y)); };
var isNotLarge = function (x) { return (not(isLarge(x))); };
var bothAreNotLarge = function (x, y) { return (isNotLarge(x) && isNotLarge(y)); };
var isMultipleOf = function (x, y) { return (x % y === 0); };
var multipleOf4IsMultipleOf2 = function (x) { return (isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true); };
var multipleOf4IsMultipleOf3 = function (x) { return (isMultipleOf(x, 4) ? isMultipleOf(x, 3) : true); };
var nonNegativeSquareRootUniquelyExists = real.forAll(function (a) { return (a >= 0 ?
    real.uniquelyExists(function (x) { return (x * x === a &&
        x >= 0); }) : true); });
// logical.ts

type natural = number;
type integer = number;
type rational = number;
type real = number

var natural = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9];
var integer = [-5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5];
var rational = [-2, -1.5, -1, -0.5, 0, 0.5, 1, 1.5, 2];
var real = [-2, -1.5, -1, -0.5, 0, 0.5, 1, 1.5, 2];

let isNatural = (x:any) =>(
    (typeof x) === 'number' &&
        Math.ceil(x) === x &&
        x >= 0 )

let isInteger = (x:any) =>(
    (typeof x) === 'number' &&
        Math.ceil(x) === x )

let isRational = (x:any) =>(
    (typeof x) === 'number' )

let isReal = (x:any) =>(
    (typeof x) === 'number' )

interface Array<T> {
    forAll( condFn: (item:T)=>boolean ) : boolean;
    exist( condFn: (item:T)=>boolean ) : boolean;
    uniquelyExists( condFn: (item:T)=>boolean ) : boolean;
    the( condFn: (item:T)=>boolean ) : T;
}

let not = (x:boolean)=>(!x)
// my-sample.ts
/// <reference path="./logical.ts" />

let isLarge = (x:number)=>(x > 100)


let bothAreLarge = (x:number, y:number) :boolean =>(isLarge(x) && isLarge(y))

let atLeastOneIsLarge = (x:number, y:number) :boolean =>(isLarge(x) || isLarge(y))

let isNotLarge = (x:number) :boolean =>(not(isLarge(x)))

let bothAreNotLarge = (x:number, y:number) :boolean =>(isNotLarge(x) && isNotLarge(y))


let isMultipleOf = (x:natural, y:natural)/*{y !== 0}*/ :boolean =>(x % y === 0)


let multipleOf4IsMultipleOf2 = (x:natural) :boolean =>(
    isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true )

let multipleOf4IsMultipleOf3 = (x:natural) :boolean =>(
    isMultipleOf(x, 4) ? isMultipleOf(x, 3) : true )


let nonNegativeSquareRootUniquelyExists :boolean =
real.forAll( (a:real)=>(
        a >= 0 ?
        real.uniquelyExists( (x:real)=>(
                x*x === a &&
                x >= 0 )
        ) : true )
)

*1:我々が使う論理は古典論理だと思っていいです。たくさんの非古典論理がありますが、当面は非古典論理を考える必要はありません。

*2:良いプログラミングの習慣として、分かりやすい名前を付けることが推奨されます。しかし、「名前によって関数の挙動が変わったりしない」という事実がとても重要です。

*3:匿名関数、インライン関数ともいいます。また、クロージャとかラムダ式と呼ぶこともあります。このへんの言葉使いについては「クロージャとラムダ式は同義だ、と主張してみる」、クロージャとオブジェクトの関係は「クロージャなんて貧乏人のオブジェクトだろ」を参照。

*4:って言っておいて、ひとつだけ注釈: 図形に対して「幾何的直感を使うな」とか、「比喩的説明はけしからん」とかではないです。全然違います。日本語の語・句・文から呼び起こされる印象・感情を論理的判断の基準にはできない、という話です。

*5:僕は習慣的に3個のイコールを並べてしまうのですが、2個のイコールでもたいてい問題はありません。

*6:含意命題の真偽表〈真理値表〉をどう埋めるか? という問題です。この定義以外では具合が悪い理由がいくつもありますが、詳細は割愛します。

*7:日本語表現を分析するのは、言語学や文学の領域です。

*8:内側の (x:natural) の natural は省略しても動作に関係しません。短く書きたいときは省略してもいいです。

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

2018-08-02 (木)

ジイサンふたりの会話

| 10:15 | ジイサンふたりの会話を含むブックマーク

某氏「OS-9って、今でも生きてるんよ」
檜山「エエーッ」
某氏「組み込み用だけどね、… 」

檜山「XAtomってあったでしょ」
某氏「あったね、プロパティ名だっけ」
檜山「あれ、実体は整数で… 」

某氏「ITRONだとね、socket使えんのよ」
檜山「SVR4 TLI?」
某氏「そういうやつじゃなくて、…」

檜山「昔、registerって手で入れてたけどね」
某氏「あれ、無駄でしょ」
檜山「うん、無意味、今じゃいつレジスターに乗るかが …」

某氏「ATコマンド使って」
檜山「at、時間指定?」
某氏「いや、モデムの」
檜山「あーっ、ATDT番号とかの」

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

2018-07-31 (火)

空虚な束縛とEPペア

| 16:01 | 空虚な束縛とEPペアを含むブックマーク

昨日の記事「全称・存在限量子の色々をまとめた絵」に対するオマケのようなものです。が、昨日の記事とは独立に読めます。

空虚な束縛〈vacuous quantification〉の話をします。随伴関手対の観点からの説明です。

内容:

  1. 空虚な束縛とは
  2. 随伴ペアとEPペア
  3. 変数水増しと空虚な束縛
  4. 射影の逆像と像はEPペア

空虚な束縛とは

Pが、集合X×Y上の述語だとします。構文的には、Pは変数x, yを含む(可能性がある)とします。正確には、意味領域の述語(真偽値をとる関数) P:X×Y→{True, False} と、それを表現する構文領域の存在物である論理式は別物なんですが、ここではあまり区別しないで、同じ記号で表します。「命題」という言葉も、意味領域の述語だったり、構文領域の論理式だったり、文脈で指すものが変わります。

さて、全称命題 ∀x∈X.P(x, y) や存在命題 ∃x∈X.P(x, y) を作ると、変数xは束縛〈bind〉されるので、自由変数はyだけになり、集合Y上の述語となります。限量子(∀か∃)の束縛作用により、述語の領域〈domain of discourse〉が変わります -- 束縛作用とはそういうものです。

Pに変数xが出現してない場合はどうでしょうか。例えば、X = Y = R として、

  • P ≡ (y2 = 2)

ここで、'≡'は論理式(構文的表現)として同じことです。構文的な論理式を関数とみなすのに型付きラムダ記法を使うなら、

  • P = λ(x, y)∈R×R.(y2 = 2 : {True, False})

冒頭で「あまり区別しない」と言ったのは、論理式としての y2 = 2 と、関数としての λ(x, y)∈R×R.(y2 = 2 : {True, False}) をどちらも同じPで表すよ、という意思表示です。

論理式 P ≡ (y2 = 2) を限量子で束縛すると:

  • ∀x∈R.P ≡ ∀x∈R.(y2 = 2)
  • ∃x∈R.P ≡ ∃x∈R.(y2 = 2)

形の上では束縛してますが、束縛変数が出現しないので、束縛は無意味にみえます。このような束縛を空虚な束縛〈vacuous quantification〉と呼びます。「述語論理とインデックス付き圏と限量随伴性」では、若干意訳して「無意味限量」と言ってました。

これは名前通り、空虚で無意味に思えますが、実はなかなか面白いものです。空虚な束縛を分析するために、順序集合(むしろプレ順序集合)における随伴性を復習しましょう(次節)。

随伴ペアとEPペア

A = (A, ≦), B = (B, ≦) をプレ順序集合とします。プレ順序'≦'は次を満たします。

  • a ≦ a ---(反射律)
  • a ≦ b, b ≦ c ⇒ a ≦ c ---(推移律)

写像 f:A→B が単調〈monotone〉だとは、

  • a ≦ b ⇒ f(a) ≦ f(b)

であることです。

f:A→B, g:B→A が単調写像だとして、次の条件について考えます。

  1. ∀a∈A. a = g(f(a))
  2. ∀a∈A. a ≦ g(f(a))
  3. ∀b∈B. f(g(b)) = b
  4. ∀b∈B. f(g(b)) ≦ b

このなかから2つの条件を選んで組み合わせます。まず:

  • (∀a∈A. a = g(f(a))) ∧ (∀b∈B. f(g(b)) = b)

このとき、fとgは互いに逆です。fとgは逆ペアと呼んでいいでしょう。

次に:

  • (∀a∈A. a ≦ g(f(a))) ∧ (∀b∈B. f(g(b)) ≦ b)

このとき、fとgは随伴ペアです。詳しくは次の記事を参照してください。

逆ペアと随伴ペアの中間の存在として:

  • (∀a∈A. a = g(f(a))) ∧ (∀b∈B. f(g(b)) ≦ b)

このとき、fとgはEPペア〈EP pair〉と呼びます。EPは"embedding-projection"のことで、fが単射埋め込み、gがそれに対する全射射影と解釈できます。∀a∈A. a = g(f(a)) だけなら、gをレトラクション〈引き込み〉と呼ぶので、ER〈embedding-retraction〉ペアです。(もっとも、EPペアとERペアは明確に区別されないようです。)詳しくは次の記事を参照してください。

変数水増しと空虚な束縛

集合(議論の領域)Y上の述語全体の集合をPred[Y]と書きます。'Pred'と太字にしたほうが圏論と相性がいいですが、面倒なんで太字にしません。Pred[X×Y]も同じ解釈です。

π2:X×Y→Y は第二射影とします。この第二射影により、述語(真偽値をとる関数)の引き戻し π2*:Pred[Y]→Pred[X×Y] が誘導されます。

  • π2*(Q) := π2;Q = Q¥circπ2

すぐ上の定義は、意味的に考えたものですが、構文的にπ2*を考えると、変数yだけを含む(可能性がある)論理式Qを、ニ変数x, yの論理式だと“思い直す”ことです。“思い直す”だけなので、実際には何も起きず、分かりにくい操作です。

例えば、Q ≡ (y2 = 2) として、π2*(Q) は、見た目はQとまったく変わりません。見て区別できません。しかし、変数xとyを持つ論理式とみなした y2 = 2 なので、π2*(Q) = P なのです。ここで、Pは前節で定義した「たまたまxを含まない二変数論理式」です。

P, Qを意味的に考えて、真偽値をとる関数と解釈するなら:

  • Q = λy∈R.(y2 = 2)
  • P = λ(x, y)∈R.(y2 = 2)

実際には出現しない変数を足していくことを変数水増し〈variable thinning〉と呼びます。定数を関数とみなすのも変数水増しです。

  • C0 = 3 (ほんとの定数)
  • C1 = λx∈R.3 (一変数の定数関数)
  • C2 = λ(x, y)∈R×R.3 (ニ変数の定数関数)

空虚な束縛や変数水増しは、構文的な操作ですが、構文的に考えていると分かりにくく正体不明です。意味的に考えましょう。集合X上の命題Pは、P:X→{True, False} という真偽値関数とみなせば意味的解釈になりますが、さらに、外延的に考えて {x∈X | P(x)} のような集合を命題の意味としましょう。

すると、π2:X×Y→Y に伴って、逆像関数 π2*:Pow(Y)→Pow(X×Y) が定義できます。ここで、Pow(-) はベキ集合を表します。

  • π2*(B) := {(x, y)∈X×Y | π2(x, y)∈B} = {(x, y)∈X×Y | y∈B}

存在記号∃に対応する写像は π2*:Pow(X×Y)→Pow(Y) で、次のように定義される像関数 π2*:Pow(X×Y)→Pow(Y) です。

  • π2*(A) := {y∈Y | ∃x∈X.(π2(x, y) = y ∧ (x, y)∈A)} = {y∈Y | ∃x∈X.((x, y)∈A)}

この状況ならば、π2*, π2* の随伴性が見えやすくなります。次の図は「存在記号の除去規則について考える」で出したもので、設定が少し違います(第二射影じゃなくて第一射影)が、ヒントになるでしょう。

射影の逆像と像はEPペア

ここから先は、X×Y→Y という射影を単にπと書くことにします。毎回下付き'2'を書くのはめんどくさいし、第一射影でも第二射影でも話は変わらないので。

前節で述べた逆像写像は、π*:Pow(Y)→Pow(X×Y) です。逆像写像を引き戻し〈pullback〉とも呼びますが、πと逆方向に部分集合を移すからです。述語(真偽値関数)Pに対するπの前結合 P¥circπ も、部分集合Bの逆像 {(x, y)∈X×Y | π(x, y)∈B} も、どちらも引き戻しと呼び、π*(-) で表します。圏論のファイバー積も引き戻しなので、「引き戻し」は多義語です。

A∈Pow(X×Y) に対する像 π*(A) は、

  • π*(A) = {y∈Y | (x, y)∈A である x∈X が存在する}

像を対応させるπ*、その値 π*(A) を前送り〈pushuout | push-forward〉とも呼びます。

π*とπ*のあいだに次の関係があるのはすぐに分かるでしょう。

  • B∈Pow(Y) に対して、π**(B)) = B
  • A∈Pow(X×Y) に対して、A ⊆ π**(A))

これは、π*とπ*がEPペアになっていることです。π*がembeddingで、π*がprojectionです。

π*の論理的構文的解釈が存在限量子∃なので、π*と∃がEPペアと言っても同じです。さらに、π*の論理的構文的解釈が変数水増しオペレータなので、変数水増しオペレータと存在限量子がEPペアとも言えます。EPペアは、随伴ペアの特殊なものだったので、変数水増しオペレータと存在限量子は実際に随伴ペアです。

上記の事実を、論理的構文的にいえば:

  • ∃x∈X.Q(y) ⇔ Q(y)
  • P(x, y) ⇒ ∃x∈X.P(x, y)

変数水増しオペレータは表面に現れないので、[x, y]という形で無理に表現すれば:

  • (∃x∈X.[x, y]Q(y)) ⇔ Q(y)
  • P(x, y) ⇒ [x, y](∃x∈X.P(x, y))

全称限量子の場合は、少し複雑になりますが、同じスジミチをたどって、次が得られます。

  • P(x, y) ⇔ ([x, y]∀x∈X.P(x, y))
  • ([x, y]∀x∈X.P(x, y)) ⇒ P(x, y)

ここまで話した内容は、射影、像、逆像、補集合などの意味的(集合論的)な事実を、EPペアや随伴性を介して論理的構文的に再解釈してみたのです。論理では構文論(論理式と証明)のウェイトが高いですが、構文論だけではなかなか理解しにくいこともあるので、意味的解釈を併用しましょう -- というハナシでした。

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

2018-07-30 (月)

全称・存在限量子の色々をまとめた絵

| 15:11 | 全称・存在限量子の色々をまとめた絵を含むブックマーク

過去に、随伴関手対を使った全称限量子と存在限量子の解釈や、限量記号(∀と∃)の使い方などを述べたことがあります。これらのことを、短くまとめる必要があったので、まとめの絵を描きました。その絵をこの記事に載せます。

過去記事

全称限量子と存在限量子に関する過去記事を挙げておきます。本記事は短いまとめなので、より詳しいことを知りたくなったら過去記事を参照してください。

原理的な話は:

実際の証明で限量子をどのように扱うかのノウハウは:

全称限量子のまとめの絵

出現している記号の説明をします。

  • Pred[X] -- 集合X上の述語の集合。述語は、X→{True, False} という関数だと思っても、Xの部分集合だと思っても、どっちでもいいです。述語のあいだの順序関係をもとに、圏とみなします。
  • π2:X×Y→Y という第二射影
  • π2*:Pred[X]→Pred[X×Y] -- 第二射影π2から誘導される述語のあいだの写像。述語を関数だと思うなら、π2*(P) := P¥circπ2 。構文的には、変数水増し〈variable thinning〉オペレータです。
  • '-|' は随伴対を表す記号。

(関手の)随伴対については、次が詳しいです。

ただし、詳しすぎるかも。論理に出てくる随伴対は、プレ順序集合と単調写像における随伴対(ガロア接続)なので、次の記事のほうがお手軽です。

述語論理とプレ順序集合における随伴対(ガロア接続)の関係は、次の記事で主題的に扱っています。

絵の各部の説明
  • 1行目は、π2*:Pred[X]→Pred[X×Y] と ∀:Pred[X×Y]→Pred[X] が随伴対であることを主張しています。
  • その下は、ホムセット同型による随伴対の記述です。
  • その下は、関手の随伴対を図式で表現したものです。
  • 一番下の段は、証明における∀の使い方で、四角い箱は「論理の全称記号∀も存在記号∃もちゃんと使えるようになろう」で説明した∀導入ボックスです。π2*(Q) を Q' と略記しています。Q'(x, y) := Q(y) 。Q'にxは出現しません。

存在限量子のまとめの絵

記号は全称限量子のときと同じです。

絵の各部の説明
  • 1行目は、∃:Pred[X×Y]→Pred[X] と π2*:Pred[X]→Pred[X×Y] が随伴対であることを主張しています。
  • その下は、ホムセット同型による随伴対の記述です。
  • その下は、関手の随伴対を図式で表現したものです。
  • 一番下の段は、証明における∃の使い方で、四角い箱は「論理の存在記号∃をちゃんと使えるようになろう」で説明した∃除去ボックスです。π2*(R) を R' と略記しています。R'(x, y) := R(y) 。R'にxは出現しません。

∀導入と∃除去のボックスと固有変数条件

∀導入でも∃除去ボックスでも、ボックスの先頭で a∈X という変数宣言があります。選言された変数はボックス内でだけ使える変数です。このようなボックス・ローカルな変数を固有変数〈eigenvariable〉とかパラメータと呼ぶことがあります。

固有変数に関する条件〈eigenvariable condition〉をご存知の方、気になる方がいるかも知れません。ボックス -- つまり、変数のブロックスコープをちゃんと使うなら、固有変数条件を気にする必要はありません。

ブロックスコープにおいては、次のようなことは起きません。

  • ブロック外の変数が、ブロック内の同名変数を上書きしてしまう。
  • ブロック内の変数が、ブロック外でも使えてしまう。

ブロックスコープ構造を使ってない場合は、上記のような困った現象が起きるので、それを避けるために固有変数条件を付けています。

2018-07-26 (木)

訃報・又吉イエスさん

| 13:11 | 訃報・又吉イエスさんを含むブックマーク

一週間ほど前に、又吉イエスさんがお亡くなりになっていたんですね。

渋谷で街頭演説をする姿を何度か拝見したことがあります。甲高い声と独特なリズムのあの演説がもう聞けないのは残念です。ご冥福をお祈り申し上げます。

合掌

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

2018-07-25 (水)

カッコイイけど使える線形代数とは?

| 17:15 | カッコイイけど使える線形代数とは?を含むブックマーク

「カッコよさ」と「使えること」を両立させるにはどうしたらいいんでしょう?

内容:

  1. 古式テンソル計算のモダン化
  2. 圏論的線形代数
  3. 思い起こせば
  4. ニョロニョロ線形代数
  5. お絵描き線形代数
  6. 同一じゃなくて同型、これがイヤ!
  7. おわりに

古式テンソル計算のモダン化

ここ最近、「古典的微分幾何・ベクトル解析のモダン化」というシリーズ記事を書いています。この一環として、古式テンソル計算のモダン化をやりたいな、と思っています。

古式テンソル計算ってなに? -- 古いスタイルの(古典的、古式)微分幾何・ベクトル解析には、通常の(オーソドックスな)線形代数とはだいぶ違った線形計算体系が付属しています。これを、古式テンソル計算〈old-style tensor calculation〉と呼ぶことにします。上下の添字をあやつって計算する職人ワザです

「古典的微分幾何・ベクトル解析のモダン化」の方針を四字熟語で表現するなら「温故知新」です。古式テンソル計算のような古い方式を捨てる(全面廃棄処分にする)のではなく、良い部分は残してリフォーム/リノベーションしたいのです。このとき、モダンなデザインを注入してカッコよくしたい。そう思ってます。

で、モダンて何だろう? 時代的に新しいだけではダメな気がします。やっぱりカッコよさですね。カッコイイかどうかの判断は完全に個人の趣味嗜好の反映なので、僕が感じるカッコよさです。

古式テンソル計算のモダン化として、(おそらく)メジャーな方法はテンソル代数〈tensor algebra〉を使う方法でしょう。n次元多様体の(一点での)接ベクトル空間*1をXとして、Xからテンソル代数 TA(X) を作ります。TA(X) は、二重次数付き代数〈bi-graded algebra〉で、TAkj(X) は共変k階-反変j階のテンソル空間です。共変k階の交代〈反対称〉部分を取り出すと、k-形式の空間 Λk(X) となり、kを 0, 1, ..., n と動かした全体*2として外積代数〈exterior algebra〉*3 Λ(X) ができます。

今述べた定式化は十分にモダンだと思いますが、あまりカッコイイ気がしない。それに、多様体論に寄り過ぎていて、古式テンソル計算の技法を一般的な線形代数に適用したいときにどうしたらいいか分かりません。テンソル代数/外積代数のような、特定目的の代数系に注目するのではなくて、線形代数全体をモダン化するフレームワークのなかで古式テンソル計算をリノベーションしたいのです。

圏論的線形代数

僕は、「圏論バキバキに使ってるぜ」をカッコイイと感じるので、カッコよさの感覚が正常とは思えません。感覚に正常も異常もないとも言えますが、マジョリティでないのは確かでしょう。

とにかくマイナーでもなんでも、モダンな線形代数のフレームワークとして圏論的線形代数を使いたいのです。圏論的線形代数というと、アーベル圏論がまず候補にあがるでしょう。しかし、アーベル圏〈Abelian category〉は、環上の加群達を抽象化したもので、体上のベクトル空間を扱うにはオーバースペックです。僕、アーベル圏苦手だし*4

体K上の有限次元ベクトル空間達*5を、線形写像と共に圏にしたものは、FdVectKです。テンソル積がとても重要なので、テンソル積をモノイド積とするモノイド圏〈monoidal category〉 FdVectK = (FdVectK, ¥otimes, I) (←書き方は記号の乱用)を考えます。Iは特定された〈distinguished〉1次元空間(Kと同型)で、テンソル積の単位対象です*6

テンソル積を備えた FdVectK はモノイド圏なので、背景となる一般論はモノイド圏の理論となります。さらに、有限次元ベクトル空間Xにはその双対ベクトル空間X*が存在して、これまた重要です。モノイド圏に双対概念を取り込んだものとしてコンパクト閉圏〈compact closed category | compact category〉があります。双対まで含めると、コンパクト閉圏としてのベクトル空間の圏 FdVectK = (FdVectK, ¥otimes, I, (-)*, η, ε) を考えることになります。ここで、(-)*双対化子〈dualizer〉、ηは余評価射〈coevaluation | coevaluator〉、εは評価射〈evaluation | evaluator〉です。

内積を備えた有限次元ベクトル空間(有限次元ヒルベルト空間)の全体はFdHilbKという圏を作ります。Kは共役〈conjugate〉を備えた体とします。K = C なら共役は普通の複素共役です。K = R なら恒等写像idRを共役とします。FdHilbKは、コンパクト閉構造に加えて、内積から導かれるダガー構造を持ち、ダガーコンパクト閉圏〈dagger compact closed category〉になります(長たらしいので、最近はダガーコンパクト圏〈dagger compact category〉とも呼ぶようです)。

結局、内積を持たない線形代数ならコンパクト閉圏で定式化し、内積を持つ線形代数ならダガーコンパクト閉圏で定式化することになります。

参考(nLab項目):

思い起こせば

コンパクト閉圏/ダガーコンパクト閉圏をベースに初等的線形代数をやりたいという願望(?)はだいぶ昔からあって、ちょうど10年前の記事の「第三の流儀」は、圏論的線形代数を意図しています。

この頃(2008年夏)、テンパリー/リーブ圏がマイブームで、シブシブながら古式テンソル計算をしていました。次の記事に、内積空間において番号インデックス方式を用いた計算(への参照)があります。伝統的(古式)テンソル計算をダガーコンパクト閉圏で解釈する心づもりだったようです。

2016年になって、もう一度テンパリー/リーブ圏について書いてみた記事は:

2016年記事の冒頭に、2008年当時の記録への参照と、(2016年に)整理した定式化が書いてあります。2016年版の方法は、圏論的線形代数の良いヒントになりそうです。

コンパクト閉圏は、コンパクト論理のシーケント計算の解釈も与えるので、論理計算の観点から線形代数を考えた断片的メモも残っています。

入り口から一歩しか進めなかったですね(苦笑)。

コンパクト閉圏/ダガーコンパクト閉圏をベースにした線形代数は、アブラムスキー〈Samson Abramsky〉やボブ・クック〈Bob Coecke〉が十分に開拓していて、その紹介をしたことがあります。次の記事と、そこからのリンク先記事を見てください。

アブラムスキー/クックが率いるオックスフォード量子組(Oxford Quantum Group)は、古式テンソル計算を唾棄すべきものとみなしているようで、古式テンソル計算には(批判を除けば)言及していません。彼らには、コンパクト閉圏/ダガーコンパクト閉圏と古式テンソル計算をブリッジする気はなさそうです。

ニョロニョロ線形代数

コンパクト閉圏/ダガーコンパクト閉圏をベースにすると、双対性の概念はニョロニョロ〈snaky〉を使って定義します。ニョロニョロのことは次の記事で書いています。

ソフトウェアGlobularのなかで、ニョロニョロを定義したこともあります。

ニョロニョロとは、双対性/随伴性を定義するための基本関係式で snake {relation | equation | identity} と呼ばれるものです*7。蛇関係式よりはニョロニョロ関係式のほうが可愛い感じがするんで*8、そう呼んでいます。

*9

一番有名なニョロニョロは、随伴関手対の定義に登場するニョロニョロでしょう。次の記事に、随伴関手対とニョロニョロ関係式を詳しく述べています。

双対と随伴をキチンと区別することは出来ません。結局は、どっちも同じ定義になってしまうので、気分的・雰囲的に「双対」「随伴」と呼び分けているだけです。典型的な例として、関手の随伴対、双対ベクトル空間対、ガロア接続のあいだの対応表が「3Dでニョロニョロしたい」にあります。

大きな枠組みとしては、随伴関手対と双対ベクトル空間対〈双対ペア〉は同じ概念なんです。具体的なレベルでは、もちろん違いがあります。例えば、随伴関手対ではホムセット同型から随伴性を定義できますが、双対ベクトル空間対でホムセット同型は何の意味もありません(まったく使えない)。

大きな枠組みを意識したほうがいいな、と僕が思うのは、記法の統一などです。例えば、随伴関手対の F -| G にあわせて、双対ベクトル空間対(双対ペア)も X -| Y と書きたい、とか。もっとも、ペアのどっちを左(あるいは右)と呼ぶかで紛糾しそうですが … (左右問題はホントに頭が痛い。)

そして、ベクトル空間だけで見ていると見過ごしてしまうようなポイント(けっこう重要だったりする)も、大きな枠組み内で考えるとハッキリ見えたりします。

お絵描き線形代数

古式テンソル計算というと、数式の添字を記号操作するワザが思い浮かぶのですが、ペンローズ〈Roger Penrose〉は早くから絵を使ってテンソル計算をしていました。

ペンローズの俺流計算術だったペンローズ・ヒエログリフに、圏論的な定式化を与えた(そしてそれ以上のことも成した)歴史的な論文が次です。

この論文は長らく紙印刷物でしか読めなかったんですが、今はWeb上で見られます。続き(というか、ほぼ独立な)"II" (18ページ) もありますが、目ぼしいことは上記の"I"に書いてあります。

ニョロニョロ(ヘビ、蛇行)という言葉の語源も、当該の等式を絵に描いたときの形状からです。実際、ニョロニョロの計算には絵が極めて有効です*10。絵による計算を、そのまんま絵算〈{pictorial | graphical | diagrammatic} calculation〉と呼んでいます。絵算については次の記事あたりから読むといいでしょう。

絵算の系譜は次の記事に書いています。

上記のジョイアル/ストリート論文の手法を、(主に量子情報処理のために)さらに徹底してビジュアルにしたのが、既に触れたアブラムスキー/クック流線形代数です。ボブ・クックに言わせると、量子力学(のための線形代数)は、絵を使えば幼稚園児でも分かるそうです。

同一じゃなくて同型、これがイヤ!

ここまでで、幾つかの方針が決まってきました。

  1. ベクトル空間の圏を、コンパクト閉圏またはダガーコンパクト閉圏として捉える。
  2. ニョロニョロ関係式を基本に据える。
  3. 随伴・双対の一般論(ビッグ・ピクチャー)を意識する。
  4. 絵算を使う。

このような方針に沿った“モダンな線形代数”と、古式テンソル計算を結びつけたいのですが、ネックがあります。

モノイド圏のなかでは、ベクトル空間 X, Y, Z とテンソル積に関して、次のような等式は成立しません

  • (X¥otimesY)¥otimesZ = X¥otimes(Y¥otimesZ)
  • I¥otimesX = X
  • X¥otimesI = X

次のような同型があるだけです。

  • (X¥otimesY)¥otimesZ ¥stackrel{¥sim}{=} X¥otimes(Y¥otimesZ)
  • I¥otimesX ¥stackrel{¥sim}{=} X
  • X¥otimesI ¥stackrel{¥sim}{=} X

また、双対に関して次の等式も期待できません。

  • (X*)* = X

これも同型があるだけです。

  • (X*)* ¥stackrel{¥sim}{=} X

このような同型を「めんどうだから等式にしてしまえ」とは、簡単には言えません。それどころか、「等式にできるのか?」はモノイド圏論の大きな問題意識です。高次圏になると、この問題はとてつもなく難しい問題です。

また、同型・同値ではなくて同一性を安易に使うことは、同値性の原理からは邪悪〈evil〉だと言われています。

いや、しかし、だけども、そうはいっても、同型を扱うのはホントにめんどくさいんですよ。やってられんのですよ。古式テンソル計算なんて、ぜーんぶ等号ですからね。同型なんて使ってませんから。

このギャップを解決するには、おそらく計算デバイスとしての圏(これが古式テンソル計算に対応)は、等号が成り立つように構成して、そこからVectKへの“計算の意味論”関手を作る、という方策かな、と。古式テンソル計算の圏 OTC = (OTC, ¥odot, I, (-), η, ε) では、次の等式が成立しているとします。

  1. (A¥odotB)¥odotC = A¥odot(B¥odotC)
  2. I¥odotA = A
  3. A¥odotI = A
  4. (A) = A

これらの等式が成立してないと、計算デバイスとしては(煩雑過ぎて)使えないですよ。

おわりに

ボブ・クック教授のように、「古式テンソル計算? ハッ、そんなのクソくらえだぜ!」と言ってしまえば、人生が楽になるのかも知れません。

*11

しかし、古式テンソル計算は根強く生き残っています。モダンな線形代数と古式テンソル計算の通路を作ること、相互翻訳のマニュアルを作ることは意味があるんじゃないかな、と思います。

*1:接ベクトルバンドルの典型ファイバーと言ってもいいです。

*2:多様体の次元n以上の階数を考えてもいいですが、全部ゼロ空間になります。

*3:交代テンソルの代数はグラスマン代数〈Grassmann algebra〉とも呼びます。

*4:そうはいっても、いずれアーベル圏を使わざるを得ないのですけどね。

*5:無限次元まで含めると、扱いが困難になるので有限次元に限定します。

*6:IはKと同型ですが、I = K とは限りません。I, K, End(I), II, I* などのあいだの関係は難しい問題です。

*7:ニョロニョロ等式をニョロニョロ同値に一般化したものは、snakeorator〈ニョロニョロ律子〉と呼ばれる2-射になります。例えば、"Surface proofs for linear logic" by Lawrence Dunn, Jamie Vicary に登場します。ニョロニョロ等式より難しくなります。

*8:それと、蛇の補題と紛らわしいので別な言葉を使っている、という理由もあります。

*9:画像: https://chicodeza.com/freeitems/hebi-illust.html より

*10:随伴/双対をニョロニョロで定義しても、絵を使わない人もいます。エミリー・リエル〈Emily Riehl〉女史などは、絵(ストリング図)を使わない人です。

*11:ボブ・クック教授はミュージシャンです

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

2018-07-23 (月)

上付き・下付き添字をマジに考えたら頭痛がした

| 14:29 | 上付き・下付き添字をマジに考えたら頭痛がしたを含むブックマーク

先日の記事「古典的微分幾何・ベクトル解析のモダン化: ダイレクトインデックス記法」で、上付き・下付き添字の説明をしたのですが、説明の対象である上付き・下付き添字以外に、上付き・下付き添字の記法を大量に使っている事実に気が付きました。随分とひどいオーバーロード〈多義的使用〉だわ。「過度のオーバーロードはやめよう」と主張している僕としては、ちょっと愕然としました。

僕自身が上付き・下付き添字をどんな目的で使っているかを解説することにより、反省の材料にしたいと思います。また、「古典的微分幾何・ベクトル解析のモダン化: ダイレクトインデックス記法」の分かりにくい記法への補足説明でもあります。

「古典的微分幾何・ベクトル解析のモダン化: ダイレクトインデックス記法」と強く関係している節(第5節です)を読み流してもらえれば、上付き・下付き添字記法がどのように使用されているかの調査報告(ただし、サンプル数は1)としても読めるでしょう。

内容:

  1. 上付き・下付き添字の使用状況
  2. マヤカシのRn
  3. 引数としての添字
  4. 作用素としての添字
  5. 問題の“あの添字記法”
  6. カリー化した関数を表す添字
  7. おわりに

上付き・下付き添字の使用状況

gがニ変数〈ニ引数〉の関数〈写像〉のとき、g(a, b)を短く書くために単なる併置〈juxtaposition〉を使います。

  • g(a, b) = ab

と書くわけです。掛け算が併置で書かれることはお馴染みですね。併置以外で短く書く記法というと、aとbの配置を斜め上下にすることにして:

  1. g(a, b) = ab
  2. g(a, b) = ab
  3. g(a, b) = ba
  4. g(a, b) = ba

となります。左上下はあまり使わないので*1、よく使うのは ab と ab です。これが上付き添字〈superscript | スーパースクリプト〉と下付き添字〈subscript | サブスクリプト〉です。添字をインデックス〈index〉ともいいます。

一変数関数fに対しても、f(a) を上付き・下付き添字で表すことがあります。

  1. f(a) = fa
  2. f(a) = fa
  3. f(a) = af
  4. f(a) = af

f(a) は、fのaによる評価〈evaluation〉または(同じことだが)aへのfの適用〈application〉なので、f(a) = eval(f, a) = app(a, f) とすれば:

  1. eval(f, a) = fa
  2. eval(f, a) = fa
  3. app(a, f) = af
  4. app(a, f) = af

と書けるので、ニ変数関数の添字記法だと解釈できます。

上付き添字の形で、たいていの人が思い出すのはニ変数の指数関数でしょう。

  • exp(a, b) = ab

この用法が多いので、上付き添字を見ると指数だと解釈してしまう人が多いみたいです。上付き添字と指数の結びつきは一旦チャラにして、「この上付き添字はどんな意味だろう?」と毎回考えるようにしてください。

マヤカシのRn

ここから先は、僕の記事「古典的微分幾何・ベクトル解析のモダン化: ダイレクトインデックス記法」に出現する上付き・下付き添字を、ほぼ出現順に解説していきます。

最初に出た添字表現は「Rn」です。ユークリッド空間と呼ばれる集合です。とりあえずこれは、数の指数と同じく“n個の累乗”という意味です。

  • Rn = R× ... ×R (n個)

こういう説明や定義をするたびに、僕は少し後ろめたくなります。これはマヤカシです。

2つの集合A, Bに対して、その指数〈ベキ〉を、

  • BA = (AからBへのすべての写像からなる集合) = Map(A, B)

とします。BA = Map(A, B) は標準的記法として認めましょう。この指数(上付き添字)記法が腑に落ちない方は次の記事をどうぞ。腑に落ちてる方は参照不要。

[0] = {}, [1] = [1], [2] = {1, 2}, ... などと定義します。一般的には、

  • [n] := {k∈N | 1 ≦ k ≦ n}

通常Rnと書かれているものは、R[n] = Map([n], R) = Map({1, ..., n}, R) と解釈したほうがいいです。何故かと言うと、もし、R3 := R×R×R としてしまうと、x∈R3 の下付き添字表示が x = (x1, x2, x3) とは書けずに、x = (x1, x2), x1 = ((x1)1, (x1)2) と書くハメになるからです。

'×'が二項直積の演算子記号として、R×R = R[2] は言えます*2が、R×R×R = (R×RR = R[3] は言えないのです。R[3]の要素 t = (a, b, c) (t(1) = a, t(2), t(3) = c)に対応する (R×RR の要素は、{1:{1:a, 2:b}, 2:c} とでも書くべきものです。 R×(R×R) の要素なら {1:a, 2:{1:b, 2:c}} です。もとの3-タプルは、(a, b, c) = {1:a, 2:b, 3:c} です。

{1:{1:a, 2:b}, 2:c}, {1:a, 2:{1:b, 2:c}}, {1:a, 2:b, 3:c} はイコールではなく、次の同型があるだけです。

  • (R×RR ¥stackrel{¥sim}{=} R×(R×R) ¥stackrel{¥sim}{=} R[3]

これは、つまらない話でも簡単な話でもなく、難しくて重用な話題です。直接の発展としては、モノイド圏に関するマックレーンの一貫性定理〈Mac Lane's coherence theorem for monoidal categories〉があります。

「二項直積演算が厳密には結合的ではない」という困難を避けるためには、R3 = (R×RR ではなくて、R3 = R[3] = Map({1, 2, 3}, R) と解釈したほうがいいでしょう。

引数としての添字

古典的微分幾何・ベクトル解析のモダン化: ダイレクトインデックス記法」で二番目に登場する添字記法は、「(ξi | i = 1, ..., n)」です。これは、ξ∈Rn を成分表示したものです。前節で述べたように、Rn = R[n] と考えると ξ∈Map([n], R) です。ξは関数ですから、型付きラムダ記法で書けば:

  • ξ = λi∈[n].ξ(i)

ξ(i) を ξi と書けば、λi∈[n].ξi 、これを (ξi | i∈[n]) のようにも書くのです。一般的に、関数 λi∈I.f(i) の別表記として (fi | i∈I) とか (fi)i∈I とか書かれます。これは単に関数〈写像〉の別表記に過ぎないのですが、こう書くとインデックス族〈indexed family〉と呼ばれたりします。「インデックス族」あるいは単に「族」は、「関数」と同義であり、使い分けは気分だけです*3

「(ξi | i = 1, ..., n)」における下付き添字の用法は、関数への引数渡し〈評価〉です。次のように書いてもまったく同じ意味です。違いは気分だけ

  1. ξ(i)
  2. ξi
  3. ξ[i]
  4. eval(ξ, i)
  5. app(i, ξ)

作用素としての添字

次に「f~」という上付き添字が登場します。この例では、上付きの'~'が作用素〈operator | オペレータ〉で、fがその引数〈オペランド | operand | 被作用項 | 被演算項〉です。「作用素」という言葉も、結局は関数・写像と同義語ですが、気分としては、“集合や関数を引数にとる関数”を作用素とか汎関数〈functional〉とか呼ぶ傾向があります。operatorの訳語が「作用素」または「演算子」なので、演算子でも作用素と同じニュアンスがあります。

上付き'~'が表す作用素をextとすれば、次の表現は同じ意味です。

  • f~
  • ext(f)
  • eval(ext, f)
  • app(f, ext)

extは、実はモナドのクライスリ拡張〈Kleisli extension〉オペレータです。モナドに関する解説は、興味があれば、次の記事からの参照をたどればいいと思います。

f~ において、f∈Map(A, X) だった(元の記事参照)ので、(-)~ = ext は次のようなオペレータ〈作用素 | 演算子〉です。

  • ext:Map(A, X)→Lin(RA, X)

ここで、Lin(-, -) は線形写像全体からなる集合を表します*4。extは、ベクトル空間Xとその基底Aに依存して決まるので、正確には extA,X のように書きます。あっ、またしても添字がぁー …

extA,X のように、集合や構造に依存して写像が決まることは多いのです*5。これも、(集合や写像)|→写像 という写像なので、ext(A, X) のように書いてもかまいません。しかし、ext(A, X) 自体がオペレータなので、f∈Map(A, X) を渡すと ext(A, X)(f) が出力されて、それがまた線形写像なので、ext(A, X)(f)(ξ)∈X となります。ここで最後の引数になっている ξ∈RA も写像(A→R)という状況です。引数渡しをすべて丸括弧で書くと区別が付きにくいので、添字にしたり角括弧〈ブラケット〉にしたりで、多少は見やすくするわけです。プログラミング言語だと、山形括弧もよく使います、ext<A, X> のように。

オペレータを表す添字や、集合や構造が引数になる場合の添字の例として、他に次があります(元の記事での出現順)。

  • inclA,X:A→X (A⊆X の包含写像)
  • A (上付き→は、基底からフレームを作るオペレータ)
  • (A)-1 (上付き-1は、逆写像を作るオペレータ)
  • A (上付き←は、基底から逆フレームを作るオペレータ)
  • idX (Xの恒等写像)

問題の“あの添字記法”

僕が「古典的微分幾何・ベクトル解析のモダン化: ダイレクトインデックス記法」で導入・解説したかった添字記法は、ベクトル空間Xとその基底Aに対して、gX,A:X×A→R という写像です。この写像の意味から、gではなくてdirectCoeffという長い名前を使いましょう。“ダイレクトな係数”〈direct coefficient〉の短縮です。

directCoeffは、ベクトル空間Xとその基底Aに依存して決まる写像です。directCoeff(X, A)でもいいですが、前節で述べた理由から、directCoeffX,Aとします。

directCoeffX,A:X×A→R なので、x∈X と a∈A を渡すと directCoeffX,A(x, a)∈R が定まります。この値を自然言語で説明すると*6

  • directCoeffX,A(x, a) := (Xのベクトルxを、基底Aで展開したときの、aに対する係数)

ベクトルxの展開(線形結合による表現)は次のようになります。

 x ¥,=¥, ¥sum_{a ¥in A} ¥mbox{directCoeff}_{X, A}(x, a)a

いかにも長ったらしいので、directCoeffX,A(x, a) を coeff(x, a) に省略・短縮すれば:

 x ¥,=¥, ¥sum_{a ¥in A} ¥mbox{coeff}(x, a)a

これでも頻繁に書くには辛いので、二変数関数への引数渡し coeff(x, a) を上付き添字記法にしようというわけです。

  • coeff(x, a) = xa

こうすると、固定したaに対して

  • λx∈X.coeff(x, a) = λx∈X.xa

λx∈X.xa のラムダ変数を無名化(ハイフン化)して λx∈X.xa = (-)a 、したがって、

  • (-)a = coeff(-, a)

いかなる(有限次元)ベクトル空間Xと基底Aに対しても同じ記法が使えます。標準双対ベクトル空間X*双対基底A#に対しても、次のことは言えます。

  • (-)w = directCoeffX*,A#(-, w)

しかし、w = (-)a のときに、

  • (-)a = directCoeffX*,A#(-, (-)a)

という下付き記法を導入します。X*上での下付き添字と上付き添字の関係は (-)a = (-)(-)a です。

今までの説明のなかに、X*とA#という上付き添字が出てますが、これは、集合や構造に作用するオペレータとしての添字です。上付き星印は、ベクトル空間の標準双対空間を作るオペレータ、上付きシャープ記号は、ベクトル空間の基底に対して双対基底(標準双対空間の基底)を作るオペレータです。

今になって思っていることは; (-)aという記法は分かりにくかったなー、です。基底Aと双対基底A#のあいだには、集合としての1:1対応(全単射)があるので、その全単射も上付きシャープ記号でオーバーロード(同じ名前で違うものを表す)して、(-)aの代わりに a# を使えば良かったかな、と。上付きシャープを、ゲルファント変換を表す上付きハット(サーカムフレックス記号)と一緒に使うと、展開公式が次の形になります。

 x ¥,=¥, ¥sum_{a ¥in A}<a^{¥sharp} | x>a

 v ¥,=¥, ¥sum_{a ¥in A}<a^{¥^} | v>a^{¥sharp}

<-|-> は標準ペアリング(<-|-> は評価 eval(-, -) と同じ)だとして、xa := <a#|x> , va := <a^|v> がダイレクトインデックス方式による上付き・下付き添字の定義になります。これって、スッキリしてんでしょ、まだ改善の余地があるかもしれないけど。構文・記法の設計は難しいけど楽しいなー。

カリー化した関数を表す添字

gは2変数関数 g:X×Y→Z だとします。gの第一引数をaに固定して Y→Z という関数だとみなしたものを ga と書きます。これも下付き添字ですな。

  • ga(y) = g(a, y)

無名ラムダ変数(ハイフン)を使って書けば、ga(-) = g(a, -) ですが、ちゃんとしたラムダ記法で書くと:

  • ga = ga(-) = λy∈Y.g(a, y)

aも動かしていいので、

  • g(-) = λa∈X.ga(-) = λa∈X.λy∈Y.g(a, y)

ラムダ変数は束縛変数なので、リネームしてもいいですから λa∈X.λy∈Y.g(a, y) = λx∈X.λy∈Y.g(a, y) 、こう書くと分かってくると思いますが、g(-) はgのカリー化だったのです。

もとの関数が λ(x, y)∈X×Y.g(x, y) という二変数だったのを、λx∈X.λy∈Y.g(a, y) という“一変数関数を値とする一変数関数”にしています。これがカリー化です。

  • gx(y) = (λx∈X.λy∈Y.g(a, y))(x)(y)

なので、下付き添字は、カリー化した後の変数〈引数〉として使われます。

g:X×Y→Z のカリー化を g:X→ZY と書きます。これまた上付き添字を使ってます。カリー化オペレータを表す上付き添字ですね。この書き方の由来(絵)は、「非対称閉圏のカリー化:記号法を工夫すれば、右と左の混乱も解消」を参照してください。

  • g(-) = g
  • gx = (g)(x)
  • gx(y) = (g)(x)(y)

g:X×Y→Z に対して、g:Y→ZX というカリー化もできます。ラムダ記法で書くなら:

  • g := λy∈Y.λx∈X.g(x, y)

g を添字で表現するときは、上付きにします。

  • g(-) = g
  • gy = (g)(y)
  • gy(x) = (g)(y)(x)

古典的微分幾何・ベクトル解析のモダン化: ダイレクトインデックス記法」のなかで、クロネッカーのデルタ δ:S×S→R に対して次の書き方を許しました。

  1. δ(s, t)
  2. δs(t)
  3. δt(s)
  4. δst

最初の3つは、δ, δ, δ に引数を順次(添字が先、丸括弧が後で)渡した形です。最後のは δst = δ(s, t) とみなしてかまいません。

カリー化が登場する別なケースを見てみましょう。evalS,T:TS×S→T, appS,T:S×TS→T で、evalとappは引数順序が逆転するだけとします。

  • eval(m, s) = app(s, m) = m(s)

evalA,R:RA×A→R を考えると、eval(ξ, a) = ξ(a) です。このevalを左側で(もとの第二引数が変数になる形で)カリー化すると:

  • (eval(a))(ξ) = evala(ξ) = ξ(a)

つまり、evalの左カリー化は射影に他なりません。

  • evala(ξ) = πa(ξ) = ξ(a)

evalaの上付きaは左カリー化に起因して、πaの上付きaは異なる射影を識別するラベルです。もとの定義も上付きの使用法も違いますが、evala = πa です。

ベクトル空間Xの標準双対ベクトル空間X*は、関数の空間なのでevalを考えことができます。evalX,R:X*×X→R で、

  • eval(v, x) = v(x) = <v|x>

このevalを左カリー化すると:

  • (eval(x))(v) = evalx(v) = v(x) = x^(x)

evalxはxのゲルファント変換x^です。eval自体は、eval = ЖX : X→X* を与えます。ЖXは「双対ベクトル空間、もう少し知っておいたほうがイイカモ // シャーとジェー」で定義しています。

おわりに

上付き・下付き添字は、併置の次に簡単で便利な記法です。長い関数名などを使わないで上付き・下付き添字で略記したい、とは誰もが思うでしょう。その結果、いろいろな関数が上付き・下付き添字記法で略記されることになります。出現した上付き・下付き添字が何を意味するかは、注意深く判断する必要があります。

使える文字・記号・記法はたいして多くないので、多義的使用/文脈依存は仕方ないのですが、そのなかでも上付き・下付き添字は大人気の記法ですから、超多義的使用/超文脈依存なのです。ちょっと頭痛がします。

*1:「カン拡張における上下左右: 入門の前に整理すべきこと」では、左上、左下、右上、右下に配置した添字をすべて使っています。互いに関連した4種類の二項操作を表現するためです。

*2R×Rの定義として、R[2]を採用してよい、ということです。

*3:インデックス族とかパラメータ族というと、値の領域が確定した集合ではないような印象はあります。集合とは限らない類〈class〉に値をとる場合が族の雰囲気。このテの話を、印象・雰囲気で議論してもラチがあかないので、やめときます。

*4:厳密には、Map(A, X)のXは、忘却関手をUとして U(X) です。集合圏とベクトル空間の圏のあいだの随伴関手対があるのです。

*5:自然変換や圏論的オペレータです。

*6:directCoeffの定義を形式言語でしようとすると、述語論理の論理式以外にヒルベルトのイプシロン記号が必要になります。

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