https://twitter.com/kinaba のログ (twilog の方が便利です。)
| #etaps2014 チュートリアルセッション: MS Researchの Infer .NET http://research.microsoft.com/en-us/um/cambridge/projects/infernet/ から始まり Tabular http://research.microsoft.com/apps/pubs/?id=204661 までの確率プログラミング言語の解説。(続 | |
| #etaps2014 続) Inferは公式ページ曰くグラフィカルモデルでベイズ推定するための言語/環境。言語オタク的にはこれは確率変数がfirst classな言語、という理解でいいのかな。分布と観測値から改訂された分布を作るとかそういう操作達。(続 | |
| #etaps2014 続)Tabularは、そういうことをやるにもっと適した言語の形を探った結果、RDBのスキーマに付加する形で分布や潜在変数を入れとく⇒実データをinsertしたらそこから分布やパラメタを裏で推定⇒実データがない所をqueryしたら推定された分布が答えられたり。 | |
| #etaps2014 Kaggleで人気の言語 http://www.kaggle.com/wiki/Software の図を引っ張ってきて、こういう系統の言語へのプログラミング言語研究からのアプローチは少なすぎるんでは？？？という話をしていたのなども印象に残った | |
| ２日目の分はここまで。今日はなんか急に四方八方からタスクが飛んできて大変なことになっていた。旅に出たい | |
| @masashinakata どもーありがとうございます。こういうの残しておくの、何より未来の自分が参照するときに一番役に立つ、つまり自分でやった要約なので自分が記憶を戻すブートストラップにとても適しているのでぼちぼち続けたい次第です | |
| 学会の実況ツイートしてて一番覚悟がいるのが「これ面白い」と書くときだったりする。怪しいまとめを書いちゃうのはまあ単に話聞いてない人だーという感じだけど、「面白い」はそう一時的な状態じゃない自分を晒すことになるし、論文の面白さはある程度までは好みの問題でない絶対的な線があると思うし | |
| とはいえ何が面白いと思ったか明示されている方が読む側としては絶対に面白いと思っているので、まあ腹をくくって地雷を踏みに行くしかない | |
| #etaps2014 3日目〜。(写真は昨日の適当なタイミングのもの。) https://twitter.com/kinaba/status/453786421766008832/photo/1 | |
| #etaps2014 会場。 https://twitter.com/kinaba/status/453788266576101376/photo/1 | |
| #etaps2014 招待講演、完全に https://t.co/qjHdIMstgr と内容が一緒で、大事なことなので二回言いましたみたいになってる。 | |
| #etaps2014 ESOP招待講演:既に幾つも発表もあったquantative information flow、プログラムの情報漏れ度の定量評価を確立したい分野の解説。今の先端は1日目にもあったgain関数を使う奴で、情報量的に同じでも攻撃シナリオによって被害が違う物を(続 | |
| #etaps2014 続)攻撃者のgainをパラメタライズすることで区別できる。例えば(x|7)と(x&7?1:x)がどっちがxを漏らしてるか、という例が出てた。これで「どんなgainに対してもより安全」のように量化することで比較評価ができる。この順序は数学的にも割と綺麗。 | |
| #etaps2014 (個人の感想) 気になるのは どれも Σ_{y∈観測される事象}p(y)・measureなのが気になる。低い確率で凄い漏れる、というのは確率低くてもやばいとしたいことが多い気がするし、gainで区別はできそうだけど、もっとgain以前に理論の前提とできないか | |
| #etaps2014 あとこれはfuture workで言ってたけど、gainというオラクルで評価するんじゃ無くて、攻撃側が人間もしくは機械によるアルゴリズムでアタックするわけなので、ここで実行不可能なgainを考慮にいれる必要はなくて、gain側に計算論的な評価入れたいとか | |
| #etaps2014 ESOP1件目: "e1(+)e2" (確率50%でe1かe2になる)という式入りλ計算での、二つのプログラムが等価か？という判定問題への挑戦。"どの文脈にそれらのプログラムを置いても結果が同じ"が判定したいが計算むずかしいので、別の扱いやすい等価性 (続 | |
| #etaps2014 続)つまり双模倣 (http://www.kmonos.net/wlog/133.html#_0000131217 )による判定を実用上は使う。普通のλでは文脈等価と双模倣は一致するというありがたい定理がある。 遅延評価の確率λ計算では異なる。正格評価の確率λ計算なら一致する(new!)てのがこの論文の成果 | |
| #etaps2014 λx.λy.(無限ループ (+) 何もしない) と λx.(λy.無限ループ (+) λy.何もしない) みたいなのが評価戦略等がかかわってくるきわどい例(?) | |
| #etaps2014 ESOP2件目: 結局ぜんぜん何がポイントなのかわからんかった…。並行プログラムのモデルの一つでグローバルクロックに従って同期してせーので計算が進んでいくようなもでるを緩めて扱いやすくしつつもいい感じのところはいい感じにした感じの話?（まったくわかってない | |
| エアリプ勝手にまとめる作業難易度が高い | |
| #etaps2014 ESOP3件目:CallByValueとNameの双対性。これら評価戦略の差は、言語において「値」とは、評価文脈というか「co-値」とは何かの定義の差に過ぎず、値とco値の定義をパラメタ化した計算体系で一般的に捉えられる…という観察を元に暴れてみたというお話 | |
| #etaps2014 ユーザー定義データ型を入れつつとco-データ型を入れたり、call-by-needの双対とか、もっと色々評価戦略まぜこぜにすると楽しいとかいうことをやっていた。 | |
| 紺屋の白袴、コンピュータサイエンス学会の繋がらない無線LAN | |
| #etaps2014 ESOP4件目:前提として、言語の操作的意味論の作り方にsmall stepという流儀とbig stepという流儀があって一長一短あるのですが、昨年"pretty big step"なる方法を考えた人がいて、これはつまりbig stepよりも可愛い。(続 | |
| #etaps2014 続) ので、この論文は、small step意味論を全自動でカワイイpretty big step意味論に書き換える手法を提案。意味論を保つことの健全性完全性をCoqで証明。これでsmall stepで一個意味論書けばbig stepで証明したい時も安心。 | |
| #etaps2014 やり方はDanvyの抽象機械自動導出するやつ風味。"pretty"の元論文まだ読んでないんですが、"項↓値"で定義する精神は保ちつつ、項の部分項を全部値にして組合せるスタイルではなく、部分項１つ値に置き換えた項をも一度↓で評価するスタイルって理解でいいのかな | |
| #etaps2014 ESOP招待講演2: とても隅々まで話し方が面白かった。中身はとても導入的で、transactional memory すごいよ＆ロックが何故ダメかという話。今後の研究課題。 | |
| #etaps2014 TACAS4件目: Timed Automaton（現在時刻の情報に基づいた分岐とそのクロックのリセットができるオートマトン）の積で複合的なシステムを記述するときに、同じ動きをしているクロック変数を統合して状態遷移系を簡略化する手法について。 | |
| #etaps2014 TACAS5件目: Timed automaton間の包含関係(決定不能問題)を判定するセミアルゴリズムの提案。時間発展の木にunfoldしてレベル毎にクロック変数分けてsimulationとanti-chainで枝刈って頑張るなど。よくある手法大投入感 |