https://twitter.com/kinaba のログ (twilog の方が便利です。)
| #etaps2014 FoSSaCS3件目:面白いので皆読もうと第二著者のK.I氏が言ってました。文脈自由文法を拡張し各規則がパラメタとして別の文法記号をとれるようにした高階文法、これがチョムスキー階層タイプ1、"文脈依存"と呼ばれる表現力に収まるか？という未解決問題を少し解いた | |
| #etaps2014 少しというのは3階文法までは確かに文脈依存。証明は、高階文法というのは要はλ計算なので型で殴る。「この関数、引数のお手玉してるだけで意味のある計算してなさそう」みたいな型を推論してそういう部分を削ると、線形空間で構文解析できる文法(=文脈依存)に必ず変形可能 | |
| 再掲： みんな読めと書いたけど論文へのリンクはできるだけ http://togetter.com/li/652635 で貼っています。著者版のPDFがみつかったらそこへ、みつからなかったらSpringerのページ（有料） | |
| #etaps2014 FoSSaCS4件目: ゲーム意味論という、プログラムとは実行環境とプログラムが勝負するゲームの戦略である、と解釈することでプログラムの意味づけを行う分野がありまして、この発表は例外のある言語のFullyAbstractなゲーム意味論ができたよーというお話。 | |
| #etaps2014 FoSSaCS5件目: 面白かった。nondeterministicな高階関数型言語の"到達可能性"解析、つまりある特定のコード位置が実行される可能性があるかの判定問題は、CallByNameだと関数の高階度合い(order)に応じて計算が複雑になると(続 | |
| #etaps2014 続) 知られていたけれど、CallByValueだと、さらに関数の引数の個数の多さまで複雑さの要因として加わることを究明。証明のために、引数の多い関数と非決定性のフル活用で行われる自然数のエンコードが変態的で楽しげだった。非決定性プログラミングやっぱり楽しい | |
| #etaps2014 カンファレンスディナー会場 https://twitter.com/kinaba/status/454010736017043456/photo/1 | |
| #etaps2014 そしてベストペーパー賞《Best Theory Paper at ETAPS》を頂きました https://twitter.com/kinaba/status/454015171187318784/photo/1 | |
| .@zakkas783 @5mingame2 @phoenixstarhiro どもどもー | |
| #etaps2014 ETAPS運営組織が幾つかあるのでそれぞれからでベストペーパー3つ出るらしいんですが、昨日のAPLのやつと、金曜日に発表予定の飛行機の話と、EATCSのが同点で2つで、2階木言語のやつと金曜日に発表予定のマルコフモデルの話、とのこと | |
| @Prof_hrk @chunjp @masashinakata @finalfusion ありがとうございます！Dの頃から自分がやっていた研究の方向に近いテーマなのですが、小林先生らしい型理論で戦うというアプローチに会って面白い問題がより面白くなりました。 | |
| #etaps2014 招待講演homomorphic encryptionのイントロ的な話。例えばRSA暗号化された値どうしは、復号化せずとも単純に掛け算すれば元の値の掛け算を暗号化した結果が得られる…というように、これを乗算に限らず暗号化されたまま全計算を行ってやろうという分野 | |
| #etaps2014 非準同型暗号の復号器を準同型暗号でラップして投げることでリモートで安全に暗号を取替え！という可換図式など面白かった。文字列を3マシンにランダムに分散(ただしxorしたら元文字列に戻る)して、実際の文字列を漏らさないようにでもその上で正規表現マッチする例も。 | |
| #etaps2014 ESOP1件目:高階モデル検査に帰着するスタイルでプログラムの停止性判定。「この引数で呼んだこの関数からはこの引数で再帰が起きる」的な関係の引数値を線形式でうまくランクして整礎順序にできれば停止証明成功。CEGAR:沈黙の反例ドリブン改良で巧い順序を自動探索 | |
| （そういえばおかしなことを書いてたらビシベシバシ突っ込んでください） | |
| #etaps2014 ESOP2件目:停止性の話２。プログラム状態に巧く自然数を振って狭義単調減少なら停止、というのは常套手段だがそれでは足りぬ事も多いのでω^ωまでの順序数を振ろう！という案に基づく判定器の提案。"具体的な値は定まってないがあと自然数回で止まる"状態にωを振る等 | |
| #etaps2014 ω^ωまでを考えると言わずに自然数の組やリストの辞書順と考えるのと同型では？という質問が出てて実際同型は同型だけど順序数の算数の形で抽象化した方が見通しがよくて綺麗云々。2次式を考えるよりωを係数に入れた1次式で近似とか確かに見通しよくなることはありそう | |
| #etaps2014 モデル検査でプログラムを検査したときに、エラーがみつかったら具体的にその秘孔を突くテストデータを同時に自動で作りたいという問題について。SATソルバー方面のCDCLというアルゴリズムの応用で頑張る。CEGARとどういう関係になるんだろ | |
| #etaps2014 http://www.kroening.com/papers/popl2013.pdf 曰くCEGARはdomainとtransformerを改良するけどACDCLはdomainを変えない、これが効率面でクリティカル、と書いてある。あとで読んでおこう | |
| RT @Cryolite: 「感動して涙なしには見れなかった」っていう感想をまったく脈絡のない対象に対して安易に用いて強制的にオチつけるの，飽きてきたのを通り越してくどい感じがかなり強くなってきたので，ことごとく親指を立てながら溶鉱炉に沈んでほしい． | |
| そういえば、読書メーターの感想のタグ記入欄を開くと、どんな本を読んだ直後であっても「例：[ほのぼの][どんでん返し][泣ける]」って説明文が目に入るので、今読んだ話がほのぼのでどんでん返しが泣けたオチだったとしたら…と想像して毎度笑ってしまうのだった | |
| https://t.co/QfE5CHqRHS 防人歌の基礎構造 [ほのぼの][どんでん返し][泣ける] 振り飛車4→3戦法 [ほのぼの][どんでん返し][泣ける] 数学ガールの秘密ノート [ほのぼの][どんでん返し][泣ける] | |
| #etaps2014 ESOP4件目:これは日常的に気になる問題なので興味深く聞いた。アプリが落ちた時にエラー報告を自動/手動でアップロードしてもらう機能、できるだけ実行トレース他の再現に使えるデータは含みたいが、一方でユーザのプライバシーに直接間接で関わる情報は含みたくない(続 | |
| #etaps2014 続)この論文は、同じクラッシュポイントを再現できる範囲で変数に入っている値を変える、特に特徴として、途中のコントロールフローもできるだけ変えるようにデータを弄りつつ再現例を作る、という研究。どこまで実用にできるのかわからないけど必要度すごい高いテーマだと思う | |
| #etaps2014 TACAS招待講演:"safety"という条件（="一度まずい状態に陥ったら二度と成り立たすことができない"）を満たす性質は検証がしやすいので愛されている。このsafetyの様々なバリエーションについて語る講演。色々あったけど面白かったのは (続 | |
| #etaps2014 続)普通のsafetyは一人で動くシステムの性質だけど、外から入力も入れられる（つまり外から「叩いて直せる」）版safetyとか。あとf(L)={w∈有限長|∀u∈無限.wu∈L}のBuchi→NFAの状態爆発が指数というの。例聞いてから納得まで8秒程かかる | |
| #etaps2014 ESOP5件目:論文斜め読んだ限り、Actorの粒度でなく、多数のアクターが通信するネットワークバス的単位で言語機能として意味論定めた方が良いのでは？という問題提起ぽいのだけど、発表はこのモデルではこれがちゃんとできますの羅列で言語機能である意義がわからず… | |
| グルノーブル、いつ空を見上げても複数の飛行機雲が見える https://twitter.com/kinaba/status/454268168802820096/photo/1 | |
| フランスをフラフラしている https://twitter.com/kinaba/status/454271956041621504/photo/1 |