2006-09-12 [長年日記]
λ. PPL Summer School 2006
今日は PPL Summer School に行ってくる。 色々な人に会えるであろうから楽しみ。
行ってきた。昨日のSLACSはほとんど宇宙語の世界だったが、今日はこころある人間の言語のようで、気楽に聴いていられた。色々な人にお会いできたが、あまり話すことが出来ず残念だった。
以下色々書くが、これらは講演内容をまとめたわけではなく、私の単なるメモであり、偏っており間違いを含む可能性も高いのでご注意を。まあ、真に受ける人はいないと思うが。
λ. 圏論の諸相
- 講師
- 木下 佳樹 先生（産業技術総合研究所）
- 概要
-
圏論は、圏の構造についての理論ではあるが、その利用者にとっては、ものの見方を与え、いい定義を探すための道具であるという面がある。定理の証明よりいい定義を見つけるのが難しい、というのは、圏論や型理論に共通の特徴で、同じ数学でも整数論などとちがうところである。圏論特有の普遍性を用いた議論のすすめかたを紹介する。時間があれば、函数プログラマが興味を持たれると思われる単子(monad)と代数系の関係について説明して、単子の公理の種明かしの助けとしたいが、二時間ではあまり内容に深入りできそうにない。むしろ、圏論の学び方について、いくつか提案してみたい。
同型の記号「≅」を「∝」だか「∽」だかで代用していたが、同型の記号「≅」は Unicode には含まれる(U+2245)し、JIS X 0213 にも含まれる(1-2-77)。なので、UnicodeベースのPowerPointでは普通に使えますよ。そうコメントしようかと思ったが機会を逃してしまった。
「証明が自明だとして論文がrejectされる。証明が自明になるよう工夫して理論を構成しているのに、それをわかってくれない」という Michael Barr の嘆きの話が面白かった。Barrほどの人でもそんなことがあるのね。
最後の方で、ちょこっと Lawvere theory や Sketch の話をしていて、「equational horn clause は lawvere theory をはみだすが sketch では扱える」とか「formal theory を対象化しているので、theoryに対する操作を扱える」とか言っていたが、このあたりの話をもっと聞きたかったなぁ。
動かしてみたい人にはAgdaやCoq等の定理証明系がお勧めと言っていたが、個人的には結構微妙だと思う。これらの上で圏論を形式化しようとすると、等号の扱いとか圏論にとって非本質的な部分で落とし穴にはまりがちだと思うので(というか、私ははまった)。それから、個人的には、動く例が欲しいのであれば他にも CPL や Computational Category Theory も試すことも出来ると思う。CPLは、今回扱ったものの中では equalizer や coequalizer は扱えないが、inductive/coinductiveなデータ型は扱えるしね。
それから、時間がないため講演では触れていなかったが、配布資料のMonoid(単)の説明が間違ってる。正しい図は以下の通り。
![\xymatrix@+30pt{M\times (M\times M) \ar[d]_{\mbox{id}_M \times m} \ar[r]^\alpha & (M\times M)\times M \ar[r]^{m\times \mbox{id}_M} & M\times M \ar[d]^m \\M\times M \ar[rr]_m & & M}](tex/9ea952744d289edf740b88b6e86082a2.png "\xymatrix@+30pt{M\times (M\times M) \ar[d]_{\mbox{id}_M \times m} \ar[r]^\alpha & (M\times M)\times M \ar[r]^{m\times \mbox{id}_M} & M\times M \ar[d]^m \\M\times M \ar[rr]_m & & M}")
![\xymatrix@+20pt{\{*\}\times M \ar[r]^{e \times \mbox{id}_{M}} \ar[dr]_\lambda & M\times M \ar[d]^m & M\times\{*\} \ar[l]_{\mbox{id}_{M}\times e} \ar[dl]^\varrho \\& M & }](tex/1f1822281e8a5ee629e54d9af77c5f7a.png "\xymatrix@+20pt{\{*\}\times M \ar[r]^{e \times \mbox{id}_{M}} \ar[dr]_\lambda & M\times M \ar[d]^m & M\times\{*\} \ar[l]_{\mbox{id}_{M}\times e} \ar[dl]^\varrho \\& M & }")
対応する等式は以下のようになる。
- m∘(idM×m) = m∘(m×idM)∘α
- m∘(e×idM) = λ
- m∘(idM×e) = ϱ
λ. 2時間で真似(まね)ぶ関数型言語のコンパイラ
- 講師
- 住井 英二郎 先生 (東北大学)
- 概要
-
関数型言語MLの極めて小さなサブセットのコンパイラについて解説する。表面言語からアセンブリまで、すべてのパスを理解することにより、「関数型言語も命令型言語と同様に効率のよいコードへ（しかもより簡単に）コンパイルできる」ことを納得し、「関数型言語は難しい」「関数型言語は遅い」「関数型言語は命令型言語とまったく異なる」といった迷信を打破する。
<URL:http://d.hatena.ne.jp/sumii/20060912/1158058050>
色々なマニアックな話や裏話(?)が聴けて楽しかった。
僕はA正規形(A-Normal Form; The Essence of Compiling with Continuationsを参照)とK正規形(K-Normal Form)の違いがずっと気になっていたのだけど、その違いを教えてもらったのは収穫だった。A正規系ではletの右辺のletは許されず、また末尾以外のifも許されない。それに対してK正規形はそこまで厳しくはない。例えば、「... (if ...) ...」のような式は、CPSやA正規形だとまわりの部分を全部複製するか関数にするかする必要があり、これが嫌だったためMinCamlでK正規系を選んだとのこと。というか、このことは <URL:http://d.hatena.ne.jp/sumii/20051207/1133967246#c> に既に書いてあったのに見落としてた。
質疑で「Closure変換はラムダ・リフティング(lambda lifting)ではダメなのか?」という話がU野氏からあった。部分適用が存在するならば、ラムダリフティングで super combinator に変換し、部分適用すればローカルな関数が得られる。ただ、MinCamlには部分適用がないからクロージャ変換をラムダリフティングに置き換えることは出来ない。結局、「部分適用」か「クロージャ変換」のいずれかを実装すれば他方も実現できるということだと思う。なお、部分適用の実装については Making a fast curry: push/enter vs. eval/apply for higher-order languages を参照せよ。
以下雑多なメモ。
- Schemeはset!でいきなり変数に代入できるので、コンパイラが面倒くさい。
- 【2007-01-17 追記】 黎明日記(電撃戦) (2007-01-02)で「自分の記憶が正しければ Common Lisp や Emacs Lisp の setf/setq なら可能だけど Scheme の set! は無理だったと思う」ツッコミが。もう記憶が怪しいのだけど、「いきなり」というのは「MLでは参照型の値を使うのに対して、Schemeでは一般の変数に対していきなり代入することが出来てしまう」ということについての話だったと思う。
- アセンブリ生成が長いのは、書かなくてはならない文字列が長いからであって、中身が長いわけではない
- コンパイラ作っていて一番難しかったのはif文。
- K正規系への変換では
- Sparcでは定数(特に大きな定数)は則値で使えないので、定数も一時変数におく。
- 変数を一時変数におかないのは、デバッグのときに見やすいように。
- インライン展開のヒューリステッィクは「シンタックスツリーのノードの数」と「千回やって止まらなかったら止める」程度の簡単なものでも十分。
- Lispのダイナミックバインディングは最初はバグだったらしい。
- フロー解析のかわりに、関数の定義があったらスコープの中だけで「自由変数がない」ことを認識。
- OCamlで末尾呼び出しを判定するには、生成されたバイトコードをみるのが、事実上一番手軽。
- ocamloptは多相性をサポートするため浮動小数点数をボックス化してアロケートするから、一部のベンチマークで遅くなる。
- raytraceでmincamlがgccと比べて遅いのは、浮動小数点演算のスケジューリングの最適化が大きい。
- ocamloptは let rec と書かれているだけでインライン展開を諦めるので注意。
- コンパイル時間。レジスタ割り当ての先読みに O(n2) とかあるはずだけど、gccもO(n2)くらいのアルゴリズムは結構使っていたりする。レジスタ割り当てでバックトラックしないようにしたのでそんなに問題にはならないのでは。
λ. 述語抽象化によるアルゴリズムの検証 〜 シェープ解析を例として
- 講師
- 田辺 良則 先生 (産業技術総合研究所)
- 概要
-
設計したアルゴリズムが正しいことを検証したいとき，それを表現したソースコードまたは擬似コードの検証に帰着できれば嬉しい．「検証」への様々なアプローチのなかに，モデル検査と呼ばれる「力ずくで全部の可能性を数え上げてチェックしてしまおう」という手法があるが，対象がソースコードの場合，素朴に扱うと可能な組合せが多すぎて，この手法は破綻してしまう．しかし，抽象化という，本質的でない違いを無視することで組合せを減らす方法の進歩により，ソースコードの検証も可能になってきている．このチュートリアルでは，抽象化，特に，このような検証の枠組みとしてよく用いられる述語抽象化を紹介する．基本となる考え方から始めて，いくつかのトピックと，研究レベルの検証ツールについて述べ，応用として，シェープ解析と呼ばれる分野でのアルゴリズム検証例を示す．
「圏論の諸相」はほとんど既知の内容だったし、「2時間で真似(まね)ぶ関数型言語のコンパイラ」もある程度前提知識を持っている話だったのに対して、この話は色々と新鮮だった。
述語抽象化の話が面白い。私は、具体状態の上に同値関係を定義して、抽象状態と遷移関係を定義するのだと思い込んでいたが、そうではないのだな。その代わり、述語抽象化によって抽象状態を定義し、最弱事前条件を使って遷移関係を定義する。その上で Existential Abstraction を示し、simulationの関係になっていることを確かめる。
「述語抽象化による安全性検証: 全体像」のスライドのループの終了が保障されているわけではないという話で、質問してループが終了しない例を教えてもらったのだけど、具体例を忘れてしまった。もし知っている人がいたら、教えていただけるとありがたいです。
情報の不等号、この不等号の向きは逆にして1/2を⊥とした半順序集合と考えた方がよいのではないかと思った。けど、開集合のようなものと考えれば、1/2がこの不等号で最大なのも納得できるか。
それはそうと、例の『四日で学ぶモデル検査』(読書記録) の続編が読みたくなった。
λ. 今日のSLACS
今日は、学術的興味よりも楽しさを優先して、SLACSではなく、PPL Summer School に来てしまったわけだけど、今日のSLACSがどんな感じだったのか気になる。昨日は様相論理関係が多かったが、今日はもう少し自分の興味に近い話が多かったしね。それから、それらの中で「Prologによるmakeの実装 〜Mipl〜」という題目だけが浮いていたのでﾜｸﾜｸﾃｶﾃｶしてたのに……*1
発表資料とかって公開されないのかなぁ……
【追記】 「PrologによるMakeの実装」のプロシンでの発表についての言及をメモ。
その昔、木下さんは、「Computational Category Theory」を評して、こんなんで圏論をわかったと思ってはいかんと言っていたので考えが変わっていなければ紹介されないかな。
鴨先生たちの Prolog で Make の話は 10/12 - 10/13 の奈良女子大での ALGI 17 でも発表があるらしい
鴨さん！なつかしいなあ。ぼくに最初にPrologというものを教えてくれたのが鴨さんでした。もう20年以上も昔の話
＞rpfさん<br>多分考えは変わっていないんじゃないかと。今回も「Computational Category Theory」等には触れていませんでしたし、「Mac Laneを読むのが結局近道」と言っていましたし。<br>個人的には、最終的には Mac Lane を避けて通ることは出来ないにしても、入り口はもっと簡単な本で構わないと思うんですけどね。<br><br>＞とおりすがりさん<br>情報ありがとうございます。<br>そういえばプロシンでも発表していたみたいですね。<br><br>＞おおもりさん<br>おお、そんな繋がりが。<br>私はその頃のことはあまり知らないのですが、当時はきっとPrologは大きな注目を集めていたのでしょうね。