https://twitter.com/kinaba のログ (twilog の方が便利です。)
| http://d.hatena.ne.jp/monjudoh/20110720/1311165336 そうそう。なるほど。自分の感覚をよく代弁してくれている気がする。知らなくて何も問題ないつもりで放たれてるネタなのにわざわざ知ってて当然という強要として捉えてしまうのはよくない | |
| @finalfusion まあかなり真剣に買おうと思っています。今のvaioちゃんがなんだか物理的に崩壊してきたので…。しかし本当に、バッテリ10時間持たないノートPCは屑鉄と見なす主義をとっているとなかなか選択肢が増えない… | |
| #PPDP11 今日は http://www-ps.informatik.uni-kiel.de/ppdp11/ のはじまりだったのだけど会場のネットが繋がらなくて実況できてないので多分明日起きたらまとめる | |
| #PPDP11 とりあえず10年前の最影響論文賞が Danvy&Nielsen "Defunctionalization at Work"。受賞スピーチでDanvyが突然「PPDPにはテーマソングが足りない」と言い出し音楽スタート＆指揮を始めるので皆で唱和するカオス空間だったww | |
| @bonotake 「もーど」に聞こえました。 | |
| @bonotake ちなみに僕は脳内で発音したことしか無くてしかも「まうーで」でしたが、冷静に考えたらその発音はないですな… | |
| #PPDP11 "Dynamic Symbolic Computation for Domain-Specific Language Implementation" 招待講演。演算をその場でやるんじゃなくて、記号的に演算式を覚えておいて、あとで必要になったときにやるテクニック(続 | |
| #PPDP11 続)をプッシュするお話。C++erはExpression Templateを思い浮かべていただければと。"遅延評価"ではない。演算子の満たす代数法則を使ってあとで動的に最適化、とかできる余地は非常に大きい。面白かったのは、データを作る演算だけでなくて、(続 | |
| #PPDP11 続)データを消費する演算もできるだけ記号的にに書かせてさらなる代数的最適化の機会を得るのだーのだーという辺り。例えば行列演算だったら四則演算を記号化しておくだけじゃなくて、行列に対する色んなアクセス操作を書けるDSLと呼べるレベルのものを記号化して用意して色々。 | |
| #PPDP11 "The Challenges of Constraint-Based Test Generation" 招待講演２。Cadence http://www.cadence.com のアーキテクトによる、ハードウェア検証のためのランダムテストデータ生成の話。(続 | |
| #PPDP11 続) Specman/e言語 http://bit.ly/wq8SA のお話ですね。技術的には、制約を満たす解を一様にランダムに、しかも再現可能なように取るための色々な手法の比較的な話が面白かった。外部のヒューリスティックスソルバを呼ぶとその辺難しいとか。(続 | |
| #PPDP11 Formal Verification対Test on Simulatorの文脈で "(形式手法は)verification environment cannot be resued for post-silicone testing"ってのが、そうだよなーと思た | |
| #PPDP11 "Incremental Checking of Well-Founded Recursive Specifications Modulo Axioms" 項書き換え系の停止性を"インクリメンタルに"、つまり停止性がわかってる系に新しくいくつかルールを加えたら(続 | |
| #PPDP11 続)加えた分に関するだけの検証で全体の停止性がわかるようなそういう系の定義の枠組みはどんなのか、といったお話。諸事情()によりちゃんと聴けてないんだけど、しかし条件がパッと見、適切な順序関係があって綺麗に分かれてるルールなら綺麗に分けて検証できる、以上に見えぬぬ。 | |
| #PPDP11 "Graph-Transformation Verification using Monadic Second-Order Logic"関数を再帰なし(なくても色々書ける強力な論理の)論理型言語に変換＆返値型にインライン展開しまくると引数型推論できてやっほー的遊び | |
| ところで5時間後に "Nitpicking C++ Concurrency" という、C++0xの最新ドラフトのメモリモデル検証をAlloyをバックエンドに使ってIsabelle/HOLと組み合わせて検証する話の発表があるっぽいんですが誰かそれまでに論文読んで僕に解説を！＞諸方面 | |
| #PPDP11 "Bellman's GAP - A Declarative Language for Dynamic Programming" 動的計画法を書くことに特化した専用言語。http://gapc.eu/ これ。基本的に漸化式を素直に書いたらコード生成します、(続 | |
| #PPDP11 続)というものなんだけど、DPの探索空間をそのDPのAlgebraという形で明示して、その代数に載る計算をいろいろ足せるようにして例えばスコア計算だとかパス情報を残すだとかそういうのが色々足せる感じ（たぶん）。DPで難しいのってそこかなあ、という疑問があるなあ(続 | |
| #PPDP11 続)Bellmanの最適性原理を満たす部分問題の発見がとにかく大変なので、それができてしまえば、あとは、いや確かに表埋め式DPで複雑の書くのしんどいのはわかるけど、メモ化再帰で書いてしまえばそこまで苦労なくないですか的な | |
| #PPDP11 あー、でも、例 http://gapc.eu/app/matrix （見方: sigが探索空間の定義で他がその上で計算したいコスト関数）を見ると、典型的なコスト集積が deriving auto できるのは結構楽しい気もする | |
| @ksknac @haruo_hosoya @50storms @ksuenaga バレた！（当たり前です | |
| #PPDP11 "A Modular Semantics for Higher-Order Declarative Programming with Constraints" TOY http://toy.sf.net のような高階パターンマッチ、制約解消、FLP、モジュール(続 | |
| #PPDP11 続)の入った言語のcompositionalでfull abstractionのあるsemanticsがなかったので作った、というお話、らしい。前日の遅延実況しながら聴いてたせいなんだけど、難しくて詳細のポイントは全然わからんかったorz | |
| #PPDP11 "Minimally Strict Polymorphic Functions" とても面白かった。http://bit.ly/oPaW7F Sloth の話。Haskellの関数を受け取り「無駄にstrictになってないか（可能な限界までlazyか）」判定。(続 | |
| #PPDP11 続) たとえば http://bit.ly/q3fJ1E Data.List.intersperse の実装が"無駄にstrict"なことが発見できて、実際それで無駄にメモリ消費が増えちゃうケースの改善に使えるとか。既存手法の問題は"無駄にstrict"基準が(続 | |
| #PPDP11 続)厳しすぎることで、魔術unsafePerformIOを使ってヘビーな実装しないと改善できないケースを指摘されても…みたいなことが起こり得てしまっていた。実装はパラメトリシティで話を有限ドメインに落として、CPO上の単調関数の性質を使って最適とのズレを探す。 | |
| @john_229 にちようび | |
| #PPDP11 "Protocol Analysis in Maude-NPA Using Unification Modulo Homomorphic Encryption" 暗号プロトコルの色んな性質（情報漏らさないとか）の解析する Maude-NPA フレームワーク(続 | |
| #PPDP11 続) で Homomorphic Encryption http://bit.ly/Snng5 であるということを考慮に入れた解析ができなかったのをできるようにしたというお話、らしい。全然よくわかってない。 | |
| #PPDP11 "Symbolic analysis of network security policies using rewrite systems" ルーティングの設定とかファイアウォールの設定とか全て項書き換え系として書くと嬉しいですぞ～！！！などと述べています。 | |
| #PPDP11 "Precision and Complexity of XQuery Type Inference" XQueryの部分式の型から全体の型を決める推論は、W3Cの規格だと効率重視で精度を犠牲にしているんだけど、逆に精度重視の重い解析も提案されてて、その辺 (続 | |
| #PPDP11 続) 具体的にどういう型どういうXQueryのコードで差が出てくるのか細かくボーダーラインを調べてみた、という話。ところで僕の論文を引用してくれてるのは嬉しいのですが、その論文にはinverse type inferenceの話なんて一行も書いてないぞ謎い… | |
| #PPDP11 "A Contextual Semantics for Concurrent Haskell with Futures" Concurrent Haskell に Implicit Future 入れようという話。実装はまあどうにでもなるので、論文の内容は、(続 | |
| #PPDP11 続) 意味論とプログラム等価性を定義して、future を入れてもモナド則を保たれていることの証明に割かれている。 | |
| "Devils are in the details, and the details are in the paper." | |
| #PPDP11 "Nitpicking C++ Concurrency" http://bit.ly/n3sOLM http://bit.ly/qKwWJp http://bit.ly/rsUGdH http://bit.ly/pdNBM3 。 | |
| 発表を聴く数時間前に適切な人に論文を(ノ ・O・)ノ投げて感想を集積するというのが新時代の実況です | |
| #PPDP11 一応マジメに書くと、Isabelle/HOLで形式化したC++0xのメモリモデルは既存研究(POPL11)としてあって、その検証（いろいろな例の挙動が、確かに仕様から導出できる）もされていて、今回のはそれをNitpickというライブラリ経由でKodkodという(続 | |
| #PPDP11 続)ライブラリ経由でSATソルバを使った例・反例作成によって追試した、というお話。よりスケーラビリティがあってでかい例でも調べられる。Nitpick(HOL→FO)でもSATソルバでもなくKodkod(FO→SAT)がボトルネックで、実行時間の95%とのこと。 | |
| #PPDP11 あと、最終的に0xのドラフトにバグはありませんでしたがHOLでのformalizationの方に(typo程度の)バグがががが、というのが面白かったりした。発表うまくて面白かったです。 |