https://twitter.com/kinaba のログ (twilog の方が便利です。)
| #etaps2014 ESOP6件目:Choreography(直訳すると踊りの"振り付け"?)という言葉でシステム全体のプロトコルのやりとり記述のようなものを指すらしい。コレオグラフィ記述をやってよいことの制約と見なす流儀と全て満たさなければならない義務と見なす流儀の (続 | |
| #etaps2014 続)でもないセマンティクスが必要で、そういうののフォーマライズしたという感じだと思う。個々の参加者が満たすべき制約がsession typeとして現れるみたいな雰囲気で。（あんまりちゃんと理解できなかった。） | |
| #etaps2014 TACAS3件目: 知識論理+時相論理の組み合わせみたいな記述で検証をする話。状態を表す変数に加えてそれがobservable、的な変数を導入して巧く繋いで、変数が増えるのはBDDさんがなんとかしてくる！と頑張る方向の実装 | |
| #etaps2014 TACAS4件目:「部品として人間が混ざってるシステム」の形式手法。すごい面白かった。基本は自動制御だけど、稀にやむを得ず人間に制御を渡す事がある系（具体的には自動運転カーを想定）の形式的仕様記述から、実行時の人間へ制御委譲の必要性/その際のシーケンスを導出 | |
| #etaps2014 状態図と仕様から「自動制御仕様が満たせない状態」を検出すると、そこに至るシナリオ…に至った時には人間が反応できる時間的余裕の分前の遷移を切って「人間に聞く」に変える。不快な渡し方回避を考えると最小カットetc。突飛なわけではないけど人間が形式化される感楽しい | |
| #etaps2014 TACAS5件目: 文字列の例から正規言語(オートマトン)を学習するアルゴリズム、古典的な方法は1文字1文字この文字が来たらどうですかと訊いてくるので文字種が多いと大変なのをどうにかする。文字の区間集合を辺にもつオートマトンを学習する、ということみたい | |
| 今日のセッションは以上です。ねむい | |
| 今日の洞窟です https://twitter.com/kinaba/status/454395886526033920/photo/1 | |
| 思ったよりかなり本格的に洞窟だった https://twitter.com/kinaba/status/454396541823119360/photo/1 | |
| @zakkas783 サイヤ人の乗り物みたいなのに乗っていくとたどり着けるダンジョンです https://twitter.com/kinaba/status/454397181487624193/photo/1 | |
| @sinya8282 自分の感覚としては、文字列マッチングのための正規表現を記述する目的としてはMSOの手書き/読解はしんどいです。文字列indexに関する論理式として書くので、いちいち、ここの終わりをiとして、こっちをjとして…みたいな書き方をしないといけないので。 | |
| あっFoSSaCSの招待講演が始まってしまった。続きはCMのあとで | |
| @sinya8282 と思います。Kleene代数の演算(concat,star,…)は良い命令だと思うのでそれをベースに、あとは世界中の文献を集めて主語が"string"の動詞として現れる動詞をことごとくオートマトンの演算に変えていくとか | |
| @sinya8282 あと関係あるようなないようなで、https://t.co/AfzcXLMhtA この論文は面白かったです（正規表現の試験の採点を、MSOで書いた時の見た目の近さとかでスコアづけする） | |
| #etaps2014 FoSSaCS招待講演: 二つの決定性文脈自由文法（LR(k)で書ける範囲）が同じ言語を表してるか？の判定問題、計算可能であることは"証明が難解"という評判と共に知られてます。これの人類に理解できる証明＆必要計算量は高々タワー関数という上限を示したというお話 | |
| #etaps2014 確かに筋道は多少把握できた。「2つのDPDA状態が異なる言語を受理するなら高々タワー長さで反例がある」が示したく、状態ペア列を変形してスタック2つの成長率が同じになるよう調整(=pump的議論がペアに適用できる)⇒ループなしでpopまでに取れる入力長を抑える | |
| #etaps2014 あとカウンターマシンの到達可能性からの帰着で非決定性PDAの双模倣がackermann-hardの証明、デクリメントをbisimulationの特徴使ったトリックで巧くエンコードしててかっこよかった。proceedings(28p)に全証明書いてある | |
| @ranha 講演開始1秒目から証明を初めて終了1秒前まで淡々と証明して終る講演でした。Proceedings http://link.springer.com/chapter/10.1007%2F978-3-642-54830-7_1 に全部書いてあるので頑張ると読めそうしかしスライドは絵による直感の説明があってわかりやすくなってたので公開待った方がいい鴨 | |
| #etaps2014 FoSSaCS1件目:確率的並行プロセスのbisumulation同値性を、ガリガリと計算して求めるアルゴリズムでは無く、同値性を導出できる健全で完全な公理系を構成してそのステップバイステップの証明で表現できるようにする話。SOSから公理系を機械的に導出 | |
| #etaps2014 わざわざ公理系を使って求めるというのは正規表現の公理系の応用例 http://www.diku.dk/kmc/documents/henglein2011.pdf/ からすると証拠termが残せるのが嬉しかったけどそういう応用できるのかなどうなんだろ | |
| @ranha マンガの予定は謎ですね…。無理矢理高さ揃えることで2つのDPDAの問題を1つに違い状態に持ち込むというのはなるほどなあという感じでした（そもそも私オリジナルのL(A)=?L(B)の証明もよく知らんのではありますが）。今度会う機会があったら議論しませう | |
| #etaps2014 FoSSaCS2件目: （招待講演の論文読んでたらほとんど発表が終わっていた…。）並行プロセスの実行過程のモデル(?)としてsynchronized treeというのがあったんだけど離散時間しか扱えないので連続/hybrid時間も扱えるようにしたらしい | |
| #etaps2014 FoSSaCS3件目: "communication transaction"、つまり普通のトランザクションのように一個の計算主体の動きをアトミックに見せるのではなくて、複数プロセスの関わりをトランザクション化する計算モデル、の双模倣関係とかの形式化。 | |
| 完全に意識が飛び始めていてタイトルだけ見て感想文を書いてみたみたいな文章しか書けていない。午後に Generalized Eilenberg Theorem とかいう文字列が見えるのでそれまでに意識を取り戻さなくては… | |
| RT @jonigata: GLRデモ http://jonigata.github.io/caper/glr/glrdemo.html 左上の「next」を連打するとGLRパーサの動きを見ることができます（遅いのであまり早くクリックしない方が良いです） | |
| #etaps2014 FoSSaCS4件目:確率+非決定性状態遷移系の仕様記述について、Lukasiewicz様相論理というのがいいよとプッシュするお話。論理式の解釈は0～1の実数値、◇様相は非決定的に得られる確率分布の先での期待値のsup。分布の凸合成で閉じてる系の双模倣と合う | |
| #etaps2014 FoSSaCS4件目: 圏 | |
| #etaps2014 FoSSaCS5件目: 正規言語とそれを受理する代数構造の間にある種の双対関係が成り立つというEilenbergの定理、を、特定の代数構造について示すんじゃなくて一般化して代数なんでも（なんでもじゃないけど）来いという形にしたものを証明したとのこと | |
| #etaps2014 FoSSaCS7件目(ずれてた): Structural Operational Semanticsからモデルを構成する一般的なな方法、既存のやり方は意味論が綺麗に帰納的なのを前提としてたけど項の置換規則みたいなのも入れられるように(!x := x|!x等) | |
| #etaps2014 結合的ではない(関数)合成（call-by-value と call-by-name が混ざっている状態等々）の圏論的なモデル。strictとlazyな型を言語で陽に区別する的なことを言っていたけど発表は完全に圏論の言葉で行われており僕は脱落しました… | |
| うっ明日の電王戦の解説面白そうなのに時差＆移動が | |
| #etaps2014 TACASの検証系ツールを実際に使ってみたセッション1件目。Matita http://matita.cs.unibo.it/ という対話証明系でジャンプ命令を縮める(short/long/相対/絶対を巧く選んで短くする;NP困難)の最適化の正当性証明書いてみた |