計算科学やソフトウェア工学で次に流行るもの、それはホモトピーでしょう。
そのキザシがありましたよ、先日。id:ranhaさんと僕（檜山）が、同時刻に別な文脈で偶然にもホモトピーの話をしていた、と。ranhaさんにいたっては、なんだかワケワカンナイ挿絵いっぱいのホモトピー本まで持参するというありさま。それのどこがキザシなのか？ と。いや、まー、特に根拠はないです。言ってみただけ。
2年以上前ですが「ラムダ計算とスノーグローブ現象：oto-oto-otoさんの疑問に答える」において、ヴォエヴォドスキーのホモトピーラムダ計算に触れたことがあります。ジョン・バエズなども注目していたようですが、当時目にした（できた）資料は次だけ。
- Title: A very short note on homotopy lambda calculus (October 2, 2006)
- Author: Vladimir Voevodsky
- URL: http://www.math.ias.edu/~vladimir/Site3/home_files/2006_09_Hlambda.pdf （今は Not Found）
"A very short"と言ってるくらいですから、短くて何を言いたいかサッパリわからない。まー、長くても僕にはわからんでしょうが。
次はヴォエヴォドスキーの型理論。
- Title: Notes on type systems (working notes)
- Author: Vladimir Voevodsky
- URL: http://www.math.ias.edu/~vladimir/Site3/home_files/expressions_current.pdf （今は Not Found）
これもメモ書きでよくわからない。このノートだったか他だったか覚えてないのですが、ヴォエヴォドスキーは「ブロッホ・加藤（Bloch-Kato）予想も多少は解けたから、代数幾何はもういいや。次は計算機でもやるべー。型理論おもしろそうだしな」みたいな（あくまでも「みたいな」）ことを書いてました。
で、僕はホモトピーラムダ計算／ホモトピー型理論のことはしばらく忘れていたのですが、スティーブ・アウディの比較的読みやすい解説論文を見つけて「これは面白いかもな、これはスゴイことなのかもな」と思うようになりました。
- Title: CONSTRUCTIVE TYPE THEORY AND HOMOTOPY
- Author: Steve Awodey
- URL: http://logic.cmu.edu/seminar/notes/IAStalk.pdf
上記の論文は、The Univalent Foundationsプロジェクトの一環として書かれたモノのようです。
アウディは、他にもホモトピー型理論関係の論文をいくつか書いています（僕は読んでませんけど）。
- Title: Homotopy theoretic models of identity types
- Authors: Steve Awodey, Michael A. Warren
- URL: http://www.andrew.cmu.edu/user/awodey/preprints/homotopy.pdf
- Title: TYPE THEORY AND HOMOTOPY
- Author: Steve Awodey
- URL: http://www.mathematik.uni-muenchen.de/~cm2010/awodey.pdf
- Title: Martin-Lo:f complexes (2009)
- Authors: S. Awodey, P. Hofstra, M. Warren
- URL: http://www.andrew.cmu.edu/user/awodey/preprints/MLC.pdf
論理の関係ですが、アウディさんは日本語の論文もあります。
- Title: 位相と様相 : 1階様相論理への拡張
- Authors: アウディ, スティーブ ＆ 岸田, 功平
- URL: http://repository.kulib.kyoto-u.ac.jp/dspace/handle/2433/56973
そいえば、アブラムスキー一派のダンカンも計算とホモトピーを扱っていたような。確かに、シーケント計算はホモトピーっぽいですね。
ヴォエヴォドスキー本人がなにか書いてくれるといいんですが、いまのところ彼自身による解説はないようです。
