Tweet on Univalent Theory
寄り道の寄り道をしていたら目に入った、Baezの最新のblog。”From Set Theory to Type Theory” http://golem.ph.utexas.edu/category/2013/01/from_set_theory_to_type_theory.html#more …
とても面白い。彼の講義録、blog、10年分ぐらい読まずにたまっているのだけれど、いつか全部読んでみたい。
Baezのpostは、univalent type theoryの重要性をわかりやすく解説したもの。しかも前半部分は、ETCS(Elementary Theory of the Category of Sets) = LawvereのTopos理論の面白い解説になっている。
一日、Univalent Theoryの論文とビデオをZapping。久しぶりに萌える。Topos, LQG以来かな。数学の基礎の話だが、そのうち、確実にCSに落ちてくるだろう。
Univalent Foundations of Mathematics
http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2011_Goteborg.pdf …
で、Univalent Theoryの大ボスのVoevodskyが面白いエピソードを紹介している。
彼は、集合論に代わる数学を基礎づける演繹システムを探して、"homotopy λ-
calculus"という難しい理論をひねり出すのだが、ある時それが自分の大学のCSの学部学生が普通に習っているコンピュータ上の「証明支援」システムと同じものであることに気付く。2009年のこと。
Voevodskyの論文の一部は、Coqという「証明支援」言語のライブラリーとして提供されている。Githubにある。
https://github.com/vladimirias/Foundations/ …
Coqについては、http://coq.inria.fr/
LaTexで原稿をGitHubに集めて、日々、更新される本。数時間前にも、原稿が更新されているのが分かる。プログラム以外のGitHubの使い方として、面白い。HoTT bookは、Hot bookだ。
https://github.com/HoTT/book
重要なことは、HoTTは、抽象的なCategory Theoryの顔も持つが、論理学やコンピュータでの自動証明の理論と密接に結びついているということ。The Bookの2nd Versionは、自分の理論を自分に適用しようという、意欲的な試みだと思う。
プリンストンは、今、Univalentで、祭り状態になっている。ビデオで公開されている講義集を見れば、その勢いが分かる。
http://video.ias.edu/1213
ここで展開されている、訳の分からない議論が、未来のIT技術を左右するだろうと、僕は思っている。
今年は、Turing生誕100周年だが、Univalentの議論が、一般のプログラマや、更には、コンシューマの利用技術に落ちてくるのは、もっと速いスピードで進むだろう。それ以前に、プログラムの検証、テストの世界は、もっと早く影響を受けるだろう。
IASのビデオ、MACでは、なぜかトリックプレーが効かない。しょうがないので、Voevodskyの講義のビデオを、沢山ダウンロードする。Univalent Foundation of Mathematicsの連続講義、8月まで続くらしい。それじゃ、ディスク足りないな。
論理的・数学的なものの本性の洞察は、univalent theoryで大きく進むだろう。それは、物理学にも大きな影響を与えることになるだろう。望むらくは、我々の言語についての理解が、一層、深まることである。それは、情報の世界でも、本質的に重要な課題である。若い人、頑張らないと。
Martin-L ̈ofの型の理論、ちゃんと勉強したことが無かったので、"Programming in Martin-L ̈of’s Type Theory" http://www.cse.chalmers.se/research/group/logic/book/book.pdf …
を読む。今日は、5章まで読んだ。
"Voevodsky’s Univalence Axiom in homotopy type theory" http://arxiv.org/pdf/1302.4731v1.pdf …
Univalent Theoryの分かりやすい概説。
でも、Univalence Axiomを「等価公理」としてしまうと、そうすると、Equivalent もUnivalent も「等価」になってしまう。物理の「等価原理」とまぎらわしいのは構わないのだが。やっぱり、「一価公理」かな。
このあたりは、"HOMOTOPY TYPE THEORY AND VOEVODSKY'S UNIVALENT
FOUNDATIONS"の、第三章 Basic Coq constructionsに少し詳しい説明がある。
Univalence をなんと訳せばいいのだろう？化学の世界では、結合価の「一価」と訳すのが一般的なようだ。そうすると、Univalence Axiomは、「一価公理」ということになる。
Identityは「同一性」equivalenceは「等価性」としてみると次のようになる。
「Univalent Theoryの中心は、次のようなUnivalence Axiomである」を翻訳してみよう。
「単価理論の中心は、次のような単価性公理である：同一性は、等価性と等価である」
一価公理：「同一性は、等価性と等価である。」
Univalence Axiom (A = B) ≃ (A ≃ B).
Identity is equivalent to equivalence.
どうも「一価」がピンと来ない。「等価公理」と言った方がいいようにも思うのだが。
でも、Univalent Theoryを「一価理論」にするの、なんかいやだな。辞書を見ると、「単価 」とか「単葉」というのもある。これも、いまいち。Univalent = Uni + (equi)valentとして、「単一等価性」というのはどうだろ？ 名前が長い。「唯等価性」？
意味的には、Univalent「等価同一」がいいのだが。「単価」は直訳。Univalent Theory「単価理論」「等価同一理論」Univalence Axiom「単価性公理」「等価同一性公理」どっちがいい？
訳語は片付けたとして、面倒なのは人名。ペール・マーティン-レフはいいとして（もっとも、僕は、「パー」だと思っていたのだが）、厄介なのは、Voevodskyだ。「ヴョヴドゥスキー」に聞こえるが、これでいいのかしら？舌かみそうだし、なじみにくい。
集合論についてのエポック・メーキングな仕事は、この60年代のコーヘンの仕事と、70年代のローヴェールの仕事があげられる。あとは、何と言っても、21世紀に入ってからの最近のVoevodskyのUnivalent Theoryだろう。
Lawvereの時には、まだ、Category Theoryは、Universal Non-Senseだという雰囲気が残っていた。今度のUnivalentで、ようやく、「集合論はスジが悪い」とは言われなくなると思う。
ヴェイユ予想を解いたのは、グロタンディックではなく、彼の弟子のドリーニュだった。UnivalentのVoevodskyも、時代は離れているが、グロタンディックの弟子のようなもの。 http://fb.me/10WhDynnK
Univalent TheoryのVoevodskyは、証明に100年かかったポアンカレ予想を、コンピュータで自動証明させることを一つの課題として提起している。おそらく、「10年以内に」それは可能になるのではと、僕は考えている。
数学的には、古典的な集合論から、Topos理論への移行は、永遠不変な集合概念から、「変異する集合」概念への移行であった。現在進行中のUnivalent理論は、同一性概念を、いわば、"Path Dependency"で再定義しようという試みである。そう考えると、いろいろ面白い。
どんな成果が得られたか、先日レポートがあった。Homotopy Theory in Type Theory: Progress Report http://homotopytypetheory.org/2013/05/20/homotopy-theory-in-type-theory-progress-report/ …
中味はよく分からんのだが、いろんなことが「証明」されている。解説を読むと楽しい。
この間のプリンストンでの「まつり」の御大Voevodskyのまとめの報告みたいなもの。Univalent Foundations and Set Theory
http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2013_ASL.pdf …
新しい概念が導入されている。黒板でのビデオではみたのだが。
Univalent FoundationsのGITサイト。Coqでの証明がのっている（らしい。まだ動かしていない。）https://github.com/hott/hott
数学の証明も、こうしたものになっていくんだろうな。「ポアンカレ予想」のコンピュータによる証明も、時間の問題かも。
Univalent Theoryの紹介をしようと思っています。うまく行くのかしら？ @okapies @maruyama097 先生のマルレクのお知らせが来たんだけど、今後の講演予定に型理論と証明支援って書いてある…。
11月に予定している「新しい型の理論」の話は、それより敷居が高い。「最先端の研究」として、Univalent Theoryの話をする意味があるのか疑問もある。マーティン・レフ、COQあたりが、ちょうどいいところかも。まあ、9月のマルレクの反応を見て考えようと思う。
知能研究、もう少し制限的に、機械による推論能力の獲得については、COQやAGDAといったシステムに関心を持っている。その数学的な基礎付けは、近年のUnivalence Theoryの登場で劇的に変わろうとしている。この分野では、学習理論より数学的な枠組みが重要だと思っている。
ただ、11月のマルレク、「型の理論」をテーマにすると予告したのだけれど、少し悩んでいる。Homotpy Type Theory , Princetonからいい本がでたのだけど、やはり少し難しい。
http://hottheory.files.wordpress.com/2013/03/hott-ebook-323-g28e43741.pdf …
先に紹介した本は実に良く出来ていて、Homotopy Type Theory といいながら、Homotopyの説明は直観的なもので、基本群やホモロジーの話がでてくる訳でもない。Type Theoryといいながらマーティン・レフやゲンツェン流の証明図式は、Appendixにあるだけ
女子高校生（執筆当時）が書いた、COQのチュートリアル見つける。http://www.iij-ii.co.jp/lab/techdoc/coqt/ …
とても良く出来ている。多分、特別な子だとは思うが、IT技術者、COQだけなら難しいと言ってられないということ。HoTTの扱いが問題なのかな。HoTTから攻めるのやめるか。
HoTT (Homotopy Type Theory)については、最後に少しだけ触れることは出来ると思います。orz ....
そのかわり、こうしたアプローチの、テストや誤りのないプログラム開発への応用といった、話題が盛り込めればいいと思っています。
"A Gentle Introduction to Type Classes and Relations in Coq" http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf …
関数型での型クラス・Monadの意味を、Coqの側から説明したもの。
この分野での特筆すべき動きは、Vladimir Voevodsky等による、新しい型の理論である、HoTT(Homotopy Type Theory)の発見です。
プログラムと証明との同一性では、関数型言語の型に登場する矢印 -> が、論理式で、「A ならば B」を意味する “A -> B” の中に出てくる矢印 -> との間に、対応関係があるという発見が大きな役割を果たします。詳細は、講演で。
「同一性」の問題も、PropのFormation Ruleも、数学的には、Univalent Theory で捉え直した方が見通しはいいのだけど、それはそれ。後知恵になる。だから「哲学」なのだけれど、記号論理の初歩を知っている人は、かえってとまどうかも。
HoTT(Homotopy Type Theory)では、dependent typeをFibrationだという。とても腑に落ちる説明。我々の認識は確実に前進しているということだと思う。
Cantor, Frege, Russel, Zermelo, Church, Turing, Gödel, Curry, Lawvere, Martin-Löf, Voevodsky。役者が多すぎる。困ったな。
"PAT"の説明は、Simon Thompsonの “Type Theory & Functional Programming” http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf … に依拠した。この本は、読みやすくていい本だと思う。
もっとも「型の理論」は、Voevodsky の理論を中心に、現在、猛烈なスピードで進化をしている。量子論でも「双対性」の認識は、その歴史の初期においては重要な重要な役割を果たした。型の理論も、1999年のSimonの認識を超えて進もうとしているのだと思う。
ただ、英語でコミュニケーションをとっているとしても、UnivalentのVoevodskyにしろ、AmplituhedronのNima Arkani-Hamedにしろ、英米人とはかぎらない。国籍は分からないのだが。Satoshi Nakamotoだってそうだ。
Baezのビジョンは、数学的にはVoevodskyのUnivalent Theoryにつながっている。もとは、グロタンディックの夢だ。Baezのビジョンは、物理学的には、NimaのAmplituhedronとも重なる。ファインマンのアプローチの発展として。
Homotopy Type Theoryは、数学の方が元気なのだが、CSの方でもいろんな動きが出ているようだ。CMUのHarperらの仕事。"Homotopical Patch Theory"... http://fb.me/2Fqxqamh1
CMUでは、2011年にカリキュラム改革が行われたので、5年目になる来年は、この転換の「総括」が行われるだろうと思う。注目したい。ただ、関数型言語への転換の「急先鋒」だった、R.Harperは、HoTTへまっしぐら。これ、大学でどう教えるんだろう？
グロタンディークがなくなった。
Toposも、最近のHomotopy Type Theoryも、彼なしには生まれなかったと思う。ただ、それは彼の仕事が及ぼした影響の一部に過ぎない。彼のビジョンは、今もまだ、生きている。... http://fb.me/6YPkTIdWZ
数学にStack Theoryという分野がある。僕は中身を理解しているわけではないのだが、面白いのは、この分野、The Stack Projectというのがあって、200人以上の数学者が参加して、GitHubを使ってThe... http://fb.me/2hmvzNwZm
先のポストで、Stack Theoryの数学者たちが、GitHubを使ってドキュメントを公開していることを紹介した。こうした動きの先駆けになったのは、"Homotopy Type Theory "...
Baez: "Network Theory II: Stochastic Petri Nets, Chemical Reaction Networks and Feynman Diagrams" http://math.ucr.edu/home/baez/networks_oxford/networks_stochastic.pdf …
アメーバーのファインマン・ダイアグラム
Network Theoryの最後の講義のスライドがアップされていないので、以前の彼の論文を読みなおす。"A Prehistory of n-Categorical Physics" http://math.ucr.edu/home/baez/history.pdf …
難しいが、見事なオーバービュー。
Network Theoryの最後の講義のスライドがアップされていないので、以前の彼の論文を読みなおす。"A Prehistory of n-Categorical Physics" http://math.ucr.edu/home/baez/history.pdf …
難しいが、見事なオーバービュー。
コメント
コメントを投稿