2001-09-12
λ. 「エリーゼのためのに」がやっと通して弾けるようになった。まだまだだな。午後は学校に行って、ちゃたのWebページ作成を手伝って来た。タイ語版のバスタードを見せてもらったし、夕食もおごってもらっちゃいました。わーい。
λ. 米国同時多発テロ事件
日経平均がガクーンと下がって9600円くらいか。それと例によって金とか石油の先物が高謄してるらしい。…ってのはおいておいて、何かこういう事件が起こるたびに、自分達の価値観がいかに普遍的で無いかを思い知らされて切ない。それと、これを機に反イスラムの変な論調が出て来そうで怖い。
λ. gdbm
扱うデータが大きくなるとPStoreじゃ重そうなので、gdbm拡張ライブラリを試してみたが、明示的に読み込み専用としてオープンする事が出来ないっぽくて、とても気持ち悪い。gdbmは読み込み専用なら複数のプロセスから同時にオープンできたはずだから、これってgdbmの機能を無駄にしてるよなぁ〜
2002-09-12
λ. Module#const_missing メソッド
以前に欲しいと思ったことはあったのだけど、こんなに簡単に実現できるものだったとは。
λ. functorのvarianceの計算
いまだに、functorのvarianceがどうやって計算されるのか良く分かってなかったり。
2003-09-12
λ. AMG
AcronymFinderでAMGを検索すると、「Aa! Megami Sama! (anime)」がトップにくる。「Ah! My Goddess」ではなく「Aa! Megami Sama!」がdefinitionとして載っていることに少し驚く。
λ. SLACS 2003
今日も行ってきた。発表を聞いていたら、僕も研究しなくちゃなぁという気がしてきた。
λ. 外延的π計算
へぇ、λ計算をπ計算に埋め込めるのか。
λ. 等式の対応関係について, 西原 秀明 (産総研/CREST)
.
λ. 学校
帰りに学校によって、幾つか雑用を済ませてくる。久しぶりの学校は何やら工事か何かをしていた。あ、ITSSの謝金申請書を提出してくるの忘れた。
λ. Scott位相, Compactness
Scott位相の開集合の条件に「inaccessible by directed join 」があるって事は、例えば、半順序集合 (N∪{∞}, ≦) 上のScott位相を考えると、{∞}は含まれないって事かな。……なるほど、なるほど。
Compactnessまだ分からん。池上さんも「普通に勉強していても詰まるところ」と言っていたので、気長に行こっと……
2004-09-12
λ. 型を返す関数
「型を返す関数」ってのは言い換えれば「値をパラメータとする型」で、ご存じかも知れませんが、一般に依存型(dependent type)と呼ばれてます。Haskell98の型システムでは依存型を直接表現することは出来ませんが、拡張機能を使ってよいのなら HaWiki:SimulatingDependentTypes のような事は一応出来ます(2006-04-23追記: GADT(2004-11-03参照)を使うことも出来ます)。また、Haskellに本物の依存型を追加しようという試みもあることはあって、こっちはJohn Hughesのスライド"Dependent Types in Haskell"(PPT,PDF)を見ると、きっとイメージがわくと思います。
【2006-04-23追記】 依存型を直接サポートする他の関数型言語にはAgda(カテゴリ:agda参照)やEpigram(2004-09-27参照)があります。 また、依存型をサポートする型理論はカリーハワードの同型対応(Curry-Howard isomorphism, Curry-Howard correspondence)によって、ある種の述語論理に対応します。そのような型理論には例えばCC(Calsulus of Construction)やITTがあります。
λ. 萩野服部研合宿
今日明日と修善寺。
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がこの不等号で最大なのも納得できるか。
それはそうと、例の『四日で学ぶモデル検査』(読書記録) の続編が読みたくなった。
2007-09-12
2009-09-12
λ. Google Code Jam 2009: Round 1A
参加はしてないけど、また解いてみた。 Qualification Round は楽勝な感じだったけど、今回はさすがに難易度があがってるのね。 私には二時間半の時間内に全問解ける気がまるでしない……
A. Multi-base happiness
素朴に、各基底に対してその基底でハッピーな数の集合を昇順の無限リストとして定義しておいて、それらの共通部分の最初の要素として解を定義した。 Largeは数分かかってしまったけど、なんとか解けた。 基底に対するハッピーな数の集合だけじゃなくて、基底の集合に対する解の集合も再利用するようにすれば、テストケースを越えて計算を共有できて、Largeももっと速くなるかなぁ。
B. Crossing the Road
「Project Euler の Problem 15 をちょっと面倒にしたようなものか。これならDP一発で楽勝」と思って解いたら、サンプルは通るけど B-small-practice.in をパスしない。 数時間悩んで*1、ようやく南から北、西から東だけでなく、北から南、東から西へ移動することで時間が短縮できる場合(B-small-practice.in だと Case #5 と Case #6)があることに気づく(死亡確定)。 仕方がないので、後から逆向きも見て小さいほうを選ぶというのを収束するまで繰り返すようにした。ちょっとどうかと思ったが、一応Largeでも一瞬で解けたのでよしとする。
C. Collecting Cards
確率とか私には無理すぎる。 立てた式が間違っていて、何故答えが合わないのか数時間*2悩んでしまった(死亡確定)。 確率についてはもう少し慣れておくべきと思った。
ψ ケシ [「エリーゼのために」ですよ(＾＾；]