https://twitter.com/kinaba のログ (twilog の方が便利です。)
| @finalfusion いえすいえす。 | |
| #WMM Nominal Isabelleの招待講演：「α変換を上手く仮定して変数名は変にぶつからないとする」という規約はプログラミング言語に関する証明には無いと全てが異様に複雑化して死ねるのですが、機械化するとこの複雑化がもろに降りかかって全員死ぬ、というのがこの分野最大の問題 | |
| #WMM （…と先程@chunjp に説明したら"なんで？"と一蹴されたけどえーと、やればわかる！）のを何とかする試みの一つ。データ型宣言時に"名前だ"（束縛順/未使用変数が影響する/しない等のモード付）と指定すると、それ関係の帰納述語に対し自動で名前考慮済帰納法を示してくれる等 | |
| #WMM Olegさんらのマルチステージ+shift/resetの型システムの初の機械証明の話： twelfで。現在はscope侵犯が起きないように防衛的に暗黙にreset入れる場合限定(？)。"progress"の証明とevalの定義が一体化したような記述になってて面白かった | |
| #WMM Cheneyの「"既にある物を検証する"だけじゃなくて、定理証明系の存在を前提にして言語をデザインするとかそういう方向がそろそろあっていいんじゃないの？」という提案： 面白かった。W3C標準として定期的にDSLが作られているわけだけど、そこを乗っ取るのだ！(意訳)など等 | |
| #WMM Montagu&Remyの、最近のPOPLで提案されてた何か綺麗な存在型のシステムF^zipを定理証明系でやったよという話：Coq(+UPenn Lib.)+Ott+LNgenを使用、と。LNgen http://www.cis.upenn.edu/~baydemir/papers/lngen/ って知らなかった便利そう | |
| そして Nominal Isabelle の話を聴いたら午後のHOASとLocally namelessの招待講演も聴いて比較理解すべきだった気がしたけど、MSFP の方が面白そうだったのでフラフラと惹かれてそっちに来ている | |
| #MSFP 「○×ゲームとチコノフの定理と二重否定移動の共通点は何か？」：大変おもしろかった。後で長くまとめるかも。："Quantifier"は"Selection Function"で特徴づけられる。Drinker Paradox、最大値の定理、中間値の定理…は全て共通の構造 | |
| #MSFP これらselectionには「チコノフの定理=コンパクト空間の積空間はコンパクト」に依って積や無限積を定義することができて、複雑なquantifierが作れ、例えば∃∀∃∀...（やsup inf...）という積は二人ゲームの必勝戦略を表す、とHaskell実装でデモ | |
| #MSFP 浅田さん： Haskell等のArrowに関する圏論的な話。詳細は僕はまったく理解できてないけど要するに 「function：relation = functor：profunctor = Strong-Monad：Arrow」 だそうだ。 | |
| #MSFP Hindly-Milnerの型推論の綺麗な再定式化の話： これも楽しかった。あとで実装しよう。しかしどっかでこのやり方見た記憶があるんだけど気のせいかな…。要は、型コンテキストを、「set of 変数の型情報」でなく、「list of 変数の型 or 型変数導入」… | |
| #MSFP …と型変数の導入をexplicitにして、unificationが必要になると「変数のスコープがおかしくならない最初の位置に変数導入を動かす」とする。と、letの型推論が始まるときにマーカーを入れてマーカー超えなかった分を汎化、とlet多相がなる、などなど | |
| ところで今更ですけど何についてポストしているかというと http://www.icfpconference.org/icfp2010/ とその併設ワークショップです。僕が実況すると意味の分からない日本語が生成されるので、聴き終わった後に整理してまとめる方針で。 | |
| #MSFP "Epigram prime"：Epigram http://www.e-pig.org/ のデモ。拡張子がpigでEpigramマニュアルにはEmanuelとか名前がついておる…。デモ自体は初歩的すぎて結局最後までCoqやIsabelleとの差が一つも見えなかった… | |
| ニコ動の動画のロードに失敗した時に出てくる「※クッキーの制限をされている場合、nicovideo.jpを許可願います。」を見ると時々、ええい人のせいにするな、という気分になってイラッ☆としたりもする。 |