Tweet on Univalent Theory

寄り道の寄り道をしていたら目に入った、Baezの最新のblog。”From Set Theory to Type Theory”  とても面白い。彼の講義録、blog、10年分ぐらい読まずにたまっているのだけれど、いつか全部読んでみたい。

 2013年1月13日
Baezのpostは、univalent type theoryの重要性をわかりやすく解説したもの。しかも前半部分は、ETCS(Elementary Theory of the Category of Sets) = LawvereのTopos理論の面白い解説になっている。

 2013年2月11日
一日、Univalent Theoryの論文とビデオをZapping。久しぶりに萌える。Topos, LQG以来かな。数学の基礎の話だが、そのうち、確実にCSに落ちてくるだろう。

 2013年2月11日
Univalent Foundations of Mathematics で、Univalent Theoryの大ボスのVoevodskyが面白いエピソードを紹介している。

 2013年2月11日
彼は、集合論に代わる数学を基礎づける演繹システムを探して、"homotopy λ- calculus"という難しい理論をひねり出すのだが、ある時それが自分の大学のCSの学部学生が普通に習っているコンピュータ上の「証明支援」システムと同じものであることに気付く。2009年のこと。

 2013年2月11日
Voevodskyの論文の一部は、Coqという「証明支援」言語のライブラリーとして提供されている。Githubにある。 Coqについては、

 2013年2月24日
LaTexで原稿をGitHubに集めて、日々、更新される本。数時間前にも、原稿が更新されているのが分かる。プログラム以外のGitHubの使い方として、面白い。HoTT bookは、Hot bookだ。

2013年2月24日
重要なことは、HoTTは、抽象的なCategory Theoryの顔も持つが、論理学やコンピュータでの自動証明の理論と密接に結びついているということ。The Bookの2nd Versionは、自分の理論を自分に適用しようという、意欲的な試みだと思う。

 2013年2月24日
プリンストンは、今、Univalentで、祭り状態になっている。ビデオで公開されている講義集を見れば、その勢いが分かる。 ここで展開されている、訳の分からない議論が、未来のIT技術を左右するだろうと、僕は思っている。

 2013年2月24日
今年は、Turing生誕100周年だが、Univalentの議論が、一般のプログラマや、更には、コンシューマの利用技術に落ちてくるのは、もっと速いスピードで進むだろう。それ以前に、プログラムの検証、テストの世界は、もっと早く影響を受けるだろう。

 2013年2月25日
IASのビデオ、MACでは、なぜかトリックプレーが効かない。しょうがないので、Voevodskyの講義のビデオを、沢山ダウンロードする。Univalent Foundation of Mathematicsの連続講義、8月まで続くらしい。それじゃ、ディスク足りないな。

 2013年2月26日
論理的・数学的なものの本性の洞察は、univalent theoryで大きく進むだろう。それは、物理学にも大きな影響を与えることになるだろう。望むらくは、我々の言語についての理解が、一層、深まることである。それは、情報の世界でも、本質的に重要な課題である。若い人、頑張らないと。

 2013年3月1日
Martin-L ̈ofの型の理論、ちゃんと勉強したことが無かったので、"Programming in Martin-L ̈of’s Type Theory" を読む。今日は、5章まで読んだ。

2013年3月11日
"Voevodsky’s Univalence Axiom in homotopy type theory" Univalent Theoryの分かりやすい概説。

 2013年3月11日
でも、Univalence Axiomを「等価公理」としてしまうと、そうすると、Equivalent もUnivalent も「等価」になってしまう。物理の「等価原理」とまぎらわしいのは構わないのだが。やっぱり、「一価公理」かな。

2013年3月11日
このあたりは、"HOMOTOPY TYPE THEORY AND VOEVODSKY'S UNIVALENT FOUNDATIONS"の、第三章 Basic Coq constructionsに少し詳しい説明がある。

 2013年3月11日
Univalence をなんと訳せばいいのだろう?化学の世界では、結合価の「一価」と訳すのが一般的なようだ。そうすると、Univalence Axiomは、「一価公理」ということになる。 Identityは「同一性」equivalenceは「等価性」としてみると次のようになる。

2013年3月11日
「Univalent Theoryの中心は、次のようなUnivalence Axiomである」を翻訳してみよう。 
「単価理論の中心は、次のような単価性公理である:同一性は、等価性と等価である」
2013年3月11日
一価公理:「同一性は、等価性と等価である。」 Univalence Axiom (A = B) ≃ (A ≃ B). Identity is equivalent to equivalence. どうも「一価」がピンと来ない。「等価公理」と言った方がいいようにも思うのだが。

 2013年3月11日
でも、Univalent Theoryを「一価理論」にするの、なんかいやだな。辞書を見ると、「単価 」とか「単葉」というのもある。これも、いまいち。Univalent = Uni + (equi)valentとして、「単一等価性」というのはどうだろ? 名前が長い。「唯等価性」?

 2013年3月11日
意味的には、Univalent「等価同一」がいいのだが。「単価」は直訳。Univalent Theory「単価理論」「等価同一理論」Univalence Axiom「単価性公理」「等価同一性公理」どっちがいい?

 2013年3月11日
「等価同一理論の中心は、次のような等価同一性公理である:同一性は、等価性と等価である。」 この文章だけなら、「等価同一」圧勝の予感。

 2013年3月12日
訳語は片付けたとして、面倒なのは人名。ペール・マーティン-レフはいいとして(もっとも、僕は、「パー」だと思っていたのだが)、厄介なのは、Voevodskyだ。「ヴョヴドゥスキー」に聞こえるが、これでいいのかしら?舌かみそうだし、なじみにくい。

 2013年3月18日
集合論についてのエポック・メーキングな仕事は、この60年代のコーヘンの仕事と、70年代のローヴェールの仕事があげられる。あとは、何と言っても、21世紀に入ってからの最近のVoevodskyのUnivalent Theoryだろう。

 2013年3月18日
Lawvereの時には、まだ、Category Theoryは、Universal Non-Senseだという雰囲気が残っていた。今度のUnivalentで、ようやく、「集合論はスジが悪い」とは言われなくなると思う。

 2013年3月20日
ヴェイユ予想を解いたのは、グロタンディックではなく、彼の弟子のドリーニュだった。UnivalentVoevodskyも、時代は離れているが、グロタンディックの弟子のようなもの。

 2013年4月7日
Univalent TheoryVoevodskyは、証明に100年かかったポアンカレ予想を、コンピュータで自動証明させることを一つの課題として提起している。おそらく、「10年以内に」それは可能になるのではと、僕は考えている。

2013年4月27日
数学的には、古典的な集合論から、Topos理論への移行は、永遠不変な集合概念から、「変異する集合」概念への移行であった。現在進行中のUnivalent理論は、同一性概念を、いわば、"Path Dependency"で再定義しようという試みである。そう考えると、いろいろ面白い。

2013年6月1日
どんな成果が得られたか、先日レポートがあった。Homotopy Theory in Type Theory: Progress Report  中味はよく分からんのだが、いろんなことが「証明」されている。解説を読むと楽しい。

 2013年6月1日
この間のプリンストンでの「まつり」の御大Voevodskyのまとめの報告みたいなもの。Univalent Foundations and Set Theory 新しい概念が導入されている。黒板でのビデオではみたのだが。 

 2013年6月1日
Univalent FoundationsのGITサイト。Coqでの証明がのっている(らしい。まだ動かしていない。) 数学の証明も、こうしたものになっていくんだろうな。「ポアンカレ予想」のコンピュータによる証明も、時間の問題かも。

 2013年6月7日
Univalent Theoryの紹介をしようと思っています。うまく行くのかしら? 先生のマルレクのお知らせが来たんだけど、今後の講演予定に型理論と証明支援って書いてある…。

 2013年9月10日
11月に予定している「新しい型の理論」の話は、それより敷居が高い。「最先端の研究」として、Univalent Theoryの話をする意味があるのか疑問もある。マーティン・レフ、COQあたりが、ちょうどいいところかも。まあ、9月のマルレクの反応を見て考えようと思う。

 2013年9月29日
知能研究、もう少し制限的に、機械による推論能力の獲得については、COQやAGDAといったシステムに関心を持っている。その数学的な基礎付けは、近年のUnivalence Theoryの登場で劇的に変わろうとしている。この分野では、学習理論より数学的な枠組みが重要だと思っている。

 2013年9月30日
ただ、11月のマルレク、「型の理論」をテーマにすると予告したのだけれど、少し悩んでいる。Homotpy Type Theory , Princetonからいい本がでたのだけど、やはり少し難しい。

 2013年9月30日
先に紹介した本は実に良く出来ていて、Homotopy Type Theory といいながら、Homotopyの説明は直観的なもので、基本群やホモロジーの話がでてくる訳でもない。Type Theoryといいながらマーティン・レフやゲンツェン流の証明図式は、Appendixにあるだけ

 2013年9月30日
女子高校生(執筆当時)が書いた、COQのチュートリアル見つける。 とても良く出来ている。多分、特別な子だとは思うが、IT技術者、COQだけなら難しいと言ってられないということ。HoTTの扱いが問題なのかな。HoTTから攻めるのやめるか。

 2013年10月5日
HoTT (Homotopy Type Theory)については、最後に少しだけ触れることは出来ると思います。orz .... そのかわり、こうしたアプローチの、テストや誤りのないプログラム開発への応用といった、話題が盛り込めればいいと思っています。

 2013年10月31日
"A Gentle Introduction to Type Classes and Relations in Coq" 関数型での型クラス・Monadの意味を、Coqの側から説明したもの。

 2013年11月25日
この分野での特筆すべき動きは、Vladimir Voevodsky等による、新しい型の理論である、HoTT(Homotopy Type Theory)の発見です。

 2013年11月25日
プログラムと証明との同一性では、関数型言語の型に登場する矢印 -> が、論理式で、「A ならば B」を意味する “A -> B” の中に出てくる矢印 -> との間に、対応関係があるという発見が大きな役割を果たします。詳細は、講演で。

 2013年11月29日
「同一性」の問題も、PropのFormation Ruleも、数学的には、Univalent Theory で捉え直した方が見通しはいいのだけど、それはそれ。後知恵になる。だから「哲学」なのだけれど、記号論理の初歩を知っている人は、かえってとまどうかも。

 2013年12月9日
HoTT(Homotopy Type Theory)では、dependent typeをFibrationだという。とても腑に落ちる説明。我々の認識は確実に前進しているということだと思う。

 2013年12月12日
Cantor, Frege, Russel, Zermelo, Church, Turing, Gödel, Curry, Lawvere, Martin-Löf, Voevodsky。役者が多すぎる。困ったな。

 2013年12月12日
"PAT"の説明は、Simon Thompsonの “Type Theory & Functional Programming”  に依拠した。この本は、読みやすくていい本だと思う。

 2013年12月12日
もっとも「型の理論」は、Voevodsky の理論を中心に、現在、猛烈なスピードで進化をしている。量子論でも「双対性」の認識は、その歴史の初期においては重要な重要な役割を果たした。型の理論も、1999年のSimonの認識を超えて進もうとしているのだと思う。

 2014年3月8日
ただ、英語でコミュニケーションをとっているとしても、UnivalentVoevodskyにしろ、AmplituhedronのNima Arkani-Hamedにしろ、英米人とはかぎらない。国籍は分からないのだが。Satoshi Nakamotoだってそうだ。

2014年4月9日
Baezのビジョンは、数学的にはVoevodskyUnivalent Theoryにつながっている。もとは、グロタンディックの夢だ。Baezのビジョンは、物理学的には、NimaのAmplituhedronとも重なる。ファインマンのアプローチの発展として。

 2014年8月12日
Homotopy Type Theoryは、数学の方が元気なのだが、CSの方でもいろんな動きが出ているようだ。CMUのHarperらの仕事。"Homotopical Patch Theory"...

 2014年8月13日
CMUでは、2011年にカリキュラム改革が行われたので、5年目になる来年は、この転換の「総括」が行われるだろうと思う。注目したい。ただ、関数型言語への転換の「急先鋒」だった、R.Harperは、HoTTへまっしぐら。これ、大学でどう教えるんだろう?

 2014年11月15日
グロタンディークがなくなった。 Toposも、最近のHomotopy Type Theoryも、彼なしには生まれなかったと思う。ただ、それは彼の仕事が及ぼした影響の一部に過ぎない。彼のビジョンは、今もまだ、生きている。...

 2016年1月22日
数学にStack Theoryという分野がある。僕は中身を理解しているわけではないのだが、面白いのは、この分野、The Stack Projectというのがあって、200人以上の数学者が参加して、GitHubを使ってThe...

 2016年1月25日
先のポストで、Stack Theoryの数学者たちが、GitHubを使ってドキュメントを公開していることを紹介した。こうした動きの先駆けになったのは、"Homotopy Type Theory "...

 2014年2月28日
Baez: "Network Theory II: Stochastic Petri Nets, Chemical Reaction Networks and Feynman Diagrams" アメーバーのファインマン・ダイアグラム
2014年3月2日
Network Theoryの最後の講義のスライドがアップされていないので、以前の彼の論文を読みなおす。"A Prehistory of n-Categorical Physics" 難しいが、見事なオーバービュー。

2014年3月2日
Network Theoryの最後の講義のスライドがアップされていないので、以前の彼の論文を読みなおす。"A Prehistory of n-Categorical Physics" 難しいが、見事なオーバービュー。

 2014年3月2日
この本が書かれたのは、2009年。グロタンディックの問題に取り組んでいたVoevodskyが、Homotopy Typeのequivalenceについての新しい主張 Univalent Theoryを展開する少し前? 続編が読みたい。

 2014年3月2日
Baezの最近のNetwork Theoryは、とても豊かだが、それは彼の志向する本来の理論の「応用」なのだと思う。応用される事で理論は力を持つから。いや、「確率力学」をキチンと定式化することが物理の次のステップにつながると思っているのかもしれないが。多分、前者だと思う。



コメント

このブログの人気の投稿

マルレク・ネット「エントロピーと情報理論」公開しました。

初めにことばありき

人間は、善と悪との重ね合わせというモデルの失敗について