このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

コンピュータ科学や組み合わせ論を“微分幾何”とみなす:CADGの夢

『シン・ゴジラ』僕のツボにはまったんですよね。コワ面白かった! 最近、もうひとつ「これは面白い!」と思っていることがあります。微分幾何の応用の話です。多くの人が「応用」という言葉から連想する内容とはちょっと違います。微分幾何を換骨奪胎して、その枠組を、微分とも幾何ともまったく無関係と思える分野にも適用するのです。

微分とも幾何ともまったく無関係と思える分野」には、コンピュータ科学や組み合わせ論が含まれます。これには驚きました。好奇心を刺激されて、しばらく猿になって調べまくってました。

調べても理解できないことがたくさんあるので、断片的で中途半端な知識を推測(妄想?)でつなぎ合わせるという手法(いつものやり口)で語ってみます。圏と多様体の定義くらいは仮定しますが、それ以外の知識は要求しないオハナシ調です。

内容:

リソース計算が微分計算だってぇぇ?!

ラムダ計算をご存知でしょうか? ラムダ計算はコンピュータ科学において重要な位置を占めます。関数型プログラミング言語は、すべからくラムダ計算の影響を受けています。関数型とは言いがたいプログラミング言語(例えばJavaC++)でさえ、最近はラムダ式(ラムダ計算の表現法)をサポートしています。

1993年、ボードル(Gérard Boudol)は、多重度付きラムダ計算という“ラムダ計算の変種(バリアント)”を提案しました。

多重度付きラムダ計算は後〈のち〉にリソース・ラムダ計算(resource lambda-calculus)、あるいは単にリソース計算(resource calculus)と呼ばれるようになります。リソースとは、現実世界の物品のように、使いたいなら生産する必要があり、消費すればなくなり、破棄にもコストがかかるモノです。ボードルのリソース・ラムダ計算は、“リソースを引数に受け取る関数”の計算体系です。

21世紀に入ってすぐに、また別種のラムダ計算が登場します。エラア/レギエ(Thomas Ehrhard, Laurent Regnier)による微分ラムダ計算(differential lambda-calculus)です。

スコット(Dana Scott)などの手法により、計算可能関数はある位相空間上の連続関数とみなせます。この連続関数を多項式関数(のようなもの)で近似できないか? というのが動機だったようです。計算可能関数=連続関数=微分可能関数というフィクショナルな仮定のもとで、テイラー展開により多項式近似ができます -- そこで、ラムダ計算に微分概念を導入しよう、と。たぶんそんな感じ。

リソース・ラムダ計算にも微分ラムダ計算にも、ジラール(Jean-Yves Girard)の線形論理の影がちらついているので、両者の類似性に気付いていた人はいたでしょう。が、リソース・ラムダ計算と微分ラムダ計算の関係に決着が付くのはさらに10年ほど(ボードルからは20年ほど)たってからです。

マンゾネット(Giulio Manzonetto)は、リソース・ラムダ計算と微分ラムダ計算のあいだの構文的変換を構成すると共に、両者に共通なモデルを与えます。モデルとは、ラムダ計算の形式的・記号的な式や手順に対する実体的な意味のことです。

つまり、リソース・ラムダ計算と微分ラムダ計算は、構文は違えども、その意味するところは同じだったのです。

微分の計算が出来る圏

リソース・ラムダ計算と微分ラムダ計算が共通に「意味するところ」とは何なのでしょう? マンゾネットが使ったモデル(「意味するところ」)は、ブルート/コケット/シーリー(Richard Blute, Robin Cockett, Robert Seely)が定義していたデカルト微分(Cartesian differential categories)です。

デカルト微分圏は、デカルト圏(直積がある圏と思えばいいです)であり、射に対する微分が行える圏です。圏Cの射 f:A→B に対して、その微分 D[f] が圏C内の射として確定します。f |→ D[f] という対応が組み込まれている圏がデカルト微分圏です。

D[-] は微分作用素(differential operator)ですが、ここではラムダ計算の習慣に従い微分コンビネータ(differential combinator)と呼びましょう。この微分コンビネータは、微分計算に必要な道具と法則を抽象化したもので、チェーンルール(合成関数の微分公式)や偏微分と全微分との関係などが微分コンビネータの公理になっています。高校から大学教養で習う程度の微分計算は、微分コンビネータとその性質を使ってだいたいは出来ます。

デカルト微分圏を解析学入門の教材に使うのは、準備に時間がかかり過ぎるので、教育的に良い選択とは言えないでしょう。しかし、デカルト微分圏の内実解析学入門として特に違和感がないものです(記法や理論構成には違和感があるでしょうが)。

不思議なのは、解析学入門的な構造を持つデカルト微分圏が、解析学とはまったく無関係なリソース・ラムダ計算のモデルにもなることです。これは、リソース・ラムダ計算に特有な稀な現象なのでしょうか?

組み合せ論とデータ構造の理論

1986年、圏論の専門家であるジョイアル(André Joyal)は、組み合わせ論(combinatorics)で扱う離散構造(ツリー、グラフなど)の圏論的な定式化として組み合わせスピシーズ(combinatorial species)を導入しました。

組み合わせ的構造の表現であるスピシーズには、足し算・掛け算などの演算が定義できますが、それだけでなく、スピシーズの微分(derivation)が出来ます。

ジョイアルの原典は古いフランス語論文なので、フィオレ(Marcelo Fiore)の論文を引用しておきましょう。一般化されたスピシーズと、微分を含む種々の計算が解説されています。

ジョイアルのアイディアはプログラミングにも応用できます。

プログラミングでは、アルゴリズムと共にデータ構造が重要です。リスト、二分木、多次元配列などは典型的なデータ構造です。これらのデータ構造(のインスタンス)は、なんらかの形状(shape)を持ち、その形状のなかの“場所”に基本データを割当てて構成されます。「形状 + 場所 + 基本データ」で構成されるデータ構造をコンテナ(container)と呼びます。

コンテナは、関手(container functor)として定式化することが出来て、それらの関手の微分(differentiation/derivation)を定義可能なのです。これは、ジョイアルによる解析関手の微分*1(derivatives of analytic functors)をコンピュータ科学の文脈で再現・発展させたものです。コンテナの微分を簡潔に解説したものとして、次の論説があります。

スピシーズやコンテナの事例は、離散的・組み合わせ的構造のなかにも微分概念が潜んでいることを示唆します。デカルト微分圏やその一般化には、種々の微分概念に対する統合フレームワークとしての役割が期待されています。

伝統的微分幾何

話はまだ続きます。解析学入門(初等的な微積分)の次は何を学ぶでしょうか。色々な方向性があるでしょうが、有力な候補として多様体微分幾何(differential geometry of manifolds)があります。

微分幾何を展開するなら、多様体はなめらか(smooth)である必要があるので、単に多様体と言ったら“なめらかな多様体”のことだとします。また、「なめらか」と「C(無限回微分可能)な」は形容詞としてまったく同義として使います。

題名に「微分幾何」と付いている教科書で扱う内容は、(なめらかな)多様体の理論だと言っていいでしょう。この分野を伝統的微分幾何*2(traditional differential geometry)と呼ぶことにします。形容詞「伝統的」を付けたのは、非伝統的な微分幾何も扱う予定だからです。

さて、前節で紹介したデカルト微分圏という概念装置は、伝統的微分幾何を包摂しうるでしょうか? この問を言い換えると、なめらかな多様体の圏をC-Manとするとき*3C-Manデカルト微分圏であるか? となります。

答はNoです。圏C-Manデカルト微分圏(の実例)ではありません。もし、圏論的定式化により伝統的微分幾何まで扱いたいなら、別な手法が必要なのです。

実は、随分と以前に、伝統的微分幾何圏論的定式化に手を付けた人がいます。

上記論文でロシツキー(Jiri Rosicky)が示した先駆的アイディアは、ほぼ30年間かえりみられなかったようです。2010年代に入って、コケット(Robin Cockett)とクラットウェル(Geoffrey Cruttwell)がロシツキーの手法を発展させます。その結果が公表されたのは、ロシツキー論文からちょうど30年後の2014年です。

  • Title: Differential structure, tangent structure, and SDG
  • Authors: Cockett, R. and Cruttwell, G.
  • Journal: Applied Categorical Structures, 22 (2), pg. 331–417, 2014.

この論文はWeb上で入手できないようです*4が、今年の6月末(June 28, 2016)にarXiv.orgに投稿された次の論文からだいたいの内容は想像できます*5。([追記]公開されました→ https://www.mta.ca/uploadedFiles/Community/Bios/Geoff_Cruttwell/sman3.pdf[/追記]

  • Title: Differential bundles and fibrations for tangent categories (2016)
  • Authors: J.R.B. Cockett, G.S.H. Cruttwell
  • Pages: 58p
  • URL: https://arxiv.org/abs/1606.08379

接構造(tangent structure)を持つ圏 -- 接圏(tangent category)が、伝統的微分幾何の再定式化を与え、同時に非伝統的微分幾何をも射程に収めるフレームワークです。

なめらかさ

デカルト微分圏と接圏、そしてそれらの変種や拡張が幾つか提案されています。しかし、定義や用語法はまだ未整理で、若干の混乱も見受けられます。提案されている複数の圏(むしろ、圏の種別=ドクトリン)を大分類するために、微分コンビネータ付き圏(category with differentical combinator)と接構造付き圏(category with tangent structure)という言葉を使うことにします。

微分コンビネータと接構造は、「なめらかさ」を定義する2つの方法です。それぞれ、「なめらかな関数は、なめらかな微分導関数)を持つ」「なめらかな曲線は、なめらかに変動する接線族を持つ」という常識的見解を圏論的に定式化したものです。

圏論的定式化においては、「なめらかな関数(写像)とは何か?」「なめらかな図形(多様体)とは何か?」という問に答えることを放棄している点に注意してください。関数や図形がなめらかさを担うのではなくて、なめらかさは圏に付与される構造・特性です。個々の構成員ではなくて、社会・組織全体により「なめらかさ」が具現されるわけです。

これは、現代の線形代数が「ベクトルとは何か?」という問に答えることを放棄しているのと同じ事情です。ベクトル空間の要素を便宜上「ベクトル」と呼ぶだけで、ベクトルの正体はどうでもよいのです。注目すべきはベクトル空間のほうです。

同様に、なめらかな圏の対象を「なめらかな多様体」、射を「なめらかな写像」と呼ぶだけで、その正体はどうでもよいのです。注目すべきはなめらかな圏です。そして、なめらかな圏の定義法として、微分コンビネータ付き圏と接構造付き圏があるわけです。

対象や射が具体的に何であるかを問題にしないことは、非伝統的微分幾何を展開するうえで本質的です。例えば、リソース・ラムダ計算のモデルとして使われたMRelと呼ばれる圏の対象は、位相も何も持たない単なる集合です。しかし圏MRelなめらかな構造を持つので、MRelの対象を「なめらかな多様体」と呼んで差し支えないのです(無理にそう呼ぶ必要はありませんが)。

圏論的抽象微分幾何=CADG

微分コンビネータ付き圏が接構造付き圏になることは分かっています。そして、接構造付き圏により伝統的微分幾何がかなりの程度再現(recover)できることも分かってきました。まだ輪郭はハッキリとしないものの、新しい分野が立ち上がりつつあると言えるでしょう。先走ってこの分野に名前を付けてしまいましょう。

圏論的(特にトポス論的)な微分幾何は既に存在します。SDG(synthetic differential geometry)やC-schemeはそのようなものです。しかしこれらは、伝統的微分幾何のニュースタイルという趣であり、ジャンル内にとどまっている点においては保守的です。

一方、CADGの特徴は、非伝統的な微分幾何を射程に入れていることです。例えば、コケット/クラットウェルは、非伝統的応用を考慮してベクトル空間の使用をやめて、可換モノイドにまで一般化しています。そのため、伝統的微分幾何の引き写しではうまくいかないことも多いのです。

従来の論法が使えない状況において、クラットウェルは微分形式の外微分計算をしています。

今年(2016年)になってクラットウェルは、ド・ラーム・コホモロジーまで定義しようとしています(2013年の微分形式とは違った方法を使っているようです)。

  • Title: A simplicial foundation for de Rham cohomology in tangent categories (29 Jun 2016)
  • Authors: G.S.H. Cruttwell, Rory B. B. Lucyshyn-Wright
  • Pages: 52p
  • URL: https://arxiv.org/abs/1606.09080

これらのことから、CADGは空疎な枠組ではなくて、幾何的内容(geometric content)を含んでいるように思えます。

カリー/ハワード/ランベック対応

コンピュータと論理の界隈では、カリー/ハワード対応という教義があります。教祖をもう一人増やして、カリー/ハワード/ランベック対応(Curry-Howard-Lambek correspondence)と呼ぶこともあります。この教義によれば、「ラムダ計算、論理、圏」の三者は聖なるトリニティ(三位一体)を形成することになります。

最も基本的なトリニティは、「単純型付きラムダ計算、連言・含意を持つ命題論理、デカルト閉圏」から成るものです。他にも、カリー/ハワード/ランベック対応には色々な拡張・変種があります。

今我々が気になることは、微分トリニティが存在するかどうかです。微分ラムダ計算とデカルト微分圏との対応は既に確立されていると言ってでしょう。では論理は? 微分論理? って、それ何だ?

微分論理」という言葉を使っている人がいないわけではありません。例えば、次のレアード(Jim Laird)のスライド。

なんかあまりピンと来ません。論理として、分かりやすく説得的な解釈があるといいんですけどね。僕は、カリー/ハワード/ランベックの信奉者なので、いずれはハッキリとした微分論理が登場すると期待してます。

CADGのこれから

「CADGとは何であるか/何であるべきか」をまとめておくと: 「なめらかさ」を圏上の接構造(tangent structur)として捉えることにより、微分幾何的手法を広い範囲に適用する試み、となるでしょう。

これからやるべきことは:

  1. CADGの基礎をかためる。
  2. 広く浅く、非伝統的な事例を探索する。
  3. 狭く深く、伝統的微分幾何を再構成する。

あたりでしょう。

歴史が浅い分野なので、まだトッ散らかっています。定義の方法、公理の選び方、理論の組み立て方などは荒削りなので、整理して体系化する必要があるでしょう。それが基礎がためです。

現在、ラムダ計算、データ構造/データ型、組み合わせ論、論理などへの応用(適用)はされつつありますが、もっと多くの適用例が見つかると楽しいですね。物理や工学への応用があると説得力が増すでしょう。個人的には、形式言語理論/オートマトンの理論に応用できたら嬉しい(見通しはないけど)。

この記事の前のほうで「デカルト微分圏を解析学入門の教材に使うのは、準備に時間がかかり過ぎるので、教育的に良い選択とは言えない」と書きましたが、時間をかけてもいいのなら、教育の方法としても意外にイケる気がします。形式的計算で言えることと、解析学固有の議論を要することが、ハッキリと切り分けられるメリットがあります。

CADGの適用分野には、当の伝統的微分幾何も含まれます。幾何学的公理を付け加えることにより、「どこまで伝統的微分幾何を再現できるか?」は興味深い課題です。ベクトル場、微分形式、接続(共変微分)あたりの再現です。CADGとは無関係に、プロパーな幾何学の文脈で“圏上の接構造”を使っている例もあります。「接関手の上のモナド」で紹介したジャビン(Benoît Jubin)の論文はその例です。こういう動きもCADGに取り込めるかも知れません。

CADGを使って幾何学として新しいことが出来る望みは薄いと思います。しかし、伝統的微分幾何はCADGの本家であり、本家の概念や手法を他分野に輸出することを可能とするのがCADGフレームワークです。であるなら、本家における有効性をある程度は検証しておく必要があります。

現時点では、CADGの意義や将来性は何とも言えません。フレームワークだけでは有り難みが薄いので、アプリケーションがどれだけ出るか、が鍵でしょう(ソフトウェアと同じだな)。まー、好奇心と興味の対象としては今でも十分に面白いですけどね。

*1:derivative of a functor を導関数に似せて「導関手」と呼びたいところですが、導来関手(derived functor)と紛らわしいのでやめておきます。

*2:古典微分幾何(classical differential geometry)という言葉もよく使われます。

*3:過去の記事「微分のチェーンルール」や「接関手の上のモナド」では単にManと書いた圏です。

*4:マウント・アリソン大学(http://www.mta.ca/)のクラットウェルのページが消失しているようです。

*5:[追記]スライドはありますね。http://www.mathstat.dal.ca/~selinger/fmcs2012/slides/FMCS2012-Cruttwell.pdf このスライドからも概要は分かるでしょう。[/追記]

*6:"abstract differential geometry"という言葉が使われた事例はありますが、広く認知された用語ではないようなので、ここで使いました。