“Separating Regular Languages with First-Order Logic”

Slides:



Advertisements
Similar presentations
第6章 ポインタ ポインタが分からずにC言語を投げ出す人が数多くいます。 その半面、使いこなせば強力な武器となります。 しっかりと学習していきましょう C 言語 最難関文法 C 言語 最難関文法 1 第 6 章 ポインタ.
Advertisements

プログラミング言語論 第3回 BNF 記法について(演習付き) 篠埜 功. 構文の記述 プログラミング言語の構文はどのように定式化できるか? 例1 : for ループの中に for ループが書ける。 for (i=0; i
プログラミング言語論 第10回(演習) 情報工学科 木村昌臣   篠埜 功.
正規表現からのDFA直接構成.
This slide was a material for the “Reading PLDI Papers (PLDIr)” study group written by Kazuhiro Inaba ( ), under my own understanding of.
コンパイラ 2011年10月17日
ISD実習E 2009年6月29日 LISPシステム入門 (第5回) 関数ポインタ eval システム関数.
プログラミング言語論 第6回 型 情報工学科 篠埜 功.
プログラミング言語論 第4回 式の構文、式の評価
全体ミーティング (6/13) 村田雅之.
Paper from PVLDB vol.7 (To appear in VLDB 2014)
2007/1/18 山下 諒蔵 佐藤 春旗 前田 俊行 大山 恵弘 佐藤 秀明 住井 英二郎
2006/10/19 山下 諒蔵 佐藤 春旗 前田 俊行 大山 恵弘 佐藤 秀明 住井英二郎
言語処理系(5) 金子敬一.
プログラミング論 II 電卓,逆ポーランド記法電卓
プログラミング演習Ⅰ 課題2 10進数と2進数 2回目.
コンパイラ 2012年10月15日
2007/1/11 山下 諒蔵 佐藤 春旗 前田 俊行 大山 恵弘 佐藤 秀明 住井 英二郎
コンパイラ 2012年10月22日
ML 演習 第 7 回 新井淳也、中村宇佑、前田俊行 2011/05/31.
コンパイラ 2011年10月24日
静的情報と動的情報を用いた プログラムスライス計算法
細かい粒度でコードの再利用を可能とするメソッド内メソッドのJava言語への導入
プログラミング2 関数
第9章 例外処理,パッケージ 9.1 例外処理 9.2 ガーベッジコレクション.
プログラミング言語論 第3回 BNF記法について(演習付き)
正則言語 2011/6/27.
東京工科大学 コンピュータサイエンス学部 亀田弘之
インラインスクリプトに対するデータフロー 解析を用いた XHTML 文書の構文検証
プログラミング 4 記憶の割り付け.
プログラミング言語入門.
コンパイラ 2012年11月15日
第7回 プログラミングⅡ 第7回
復習 前回の関数のまとめ(1) 関数はmain()関数または他の関数から呼び出されて実行される.
プログラミング言語論 第五回 理工学部 情報システム工学科 新田直也.
コンパイラ資料 実行時環境.
平成20年10月5日(月) 東京工科大学 コンピュータサイエンス学部 亀田弘之
計算の理論 II 前期の復習 -有限オートマトン-
バイトコードを単位とするJavaスライスシステムの試作
計算の理論 I ε-動作を含むNFA 月曜3校時 大月 美佳 平成15年6月2日 佐賀大学知能情報システム学科.
プログラムの基本構造と 構造化チャート(PAD)
東京工科大学 コンピュータサイエンス学部 亀田弘之
プログラミング言語論 第9回 情報工学科 木村昌臣 篠埜 功.
コンパイラ 2011年10月20日
オブジェクト指向言語論 第六回 知能情報学部 新田直也.
プログラミング言語論 第六回 理工学部 情報システム工学科 新田直也.
JavaScriptを含んだHTML文書に対する データフロー解析を用いた構文検証手法の提案
文法と言語 ー文脈自由文法とLR構文解析ー
vc-2. Visual Studio C++ のデバッガー (Visual Studio C++ の実用知識を学ぶシリーズ)
This slide was a material for the “Reading PLDI Papers (PLDIr)” study group written by Kazuhiro Inaba ( ), under my own understanding of.
計算の理論 I ー正則表現とFAの等価性ー 月曜3校時 大月 美佳.
情報工学概論 (アルゴリズムとデータ構造)
アルゴリズムとデータ構造1 2009年6月15日
述語論理式の構文と意味 一階述語論理式の構文 一階述語論理式の意味 述語,限量記号 自然言語文の述語論理式表現 解釈 妥当,充足不能
オブジェクト指向言語論 第五回 知能情報学部 新田直也.
4.プッシュダウンオートマトンと 文脈自由文法の等価性
情報処理Ⅱ 第7回 2004年11月16日(火).
発表者: 稲葉 一浩 複雑ネットワーク・地図グラフ セミナー 2017/1/19
コンパイラ 2012年10月11日
アルゴリズムとデータ構造 2010年6月17日
プログラミング入門2 第6回 関数 情報工学科 篠埜 功.
計算の理論 I ε-動作を含むNFAと等価なDFA
計算の理論 I ε-動作を含むNFA 火曜3校時 大月 美佳 平成16年5月25日 佐賀大学知能情報システム学科.
関数と再帰 教科書13章 電子1(木曜クラス) 2005/06/22(Thu.).
プログラミング演習I 2003年6月11日(第9回) 木村巌.
情報処理Ⅱ 2005年11月25日(金).
第10回 関数と再帰.
オブジェクト指向言語論 第三回 知能情報学部 新田直也.
情報処理Ⅱ 小テスト 2005年2月1日(火).
オブジェクト指向言語論 第六回 知能情報学部 新田直也.
Presentation transcript:

“Separating Regular Languages with First-Order Logic” Paper Reading Party 2014 Speaker: @kinaba 1: 読み終われなかった論文 Reading: “Separating Regular Languages with First-Order Logic”

論文概要 キーワード: “Separating Regular Languages with First-Order Logic” 正規言語 LICS (Logic in Computer Science) 2014 キーワード: Ehrenfeucht–Fraïssé ゲーム 正規言語 冪等元 正規 正規 一階述語論理

2: 読んで楽しんだ論文 Reading: “Zombie Swarms: An Investigation of the Behavior of Your Undead Relatives”

論文概要 “Zombie Swarms: An Investigation of the Behavior of Your Undead Relatives” FUN (Fun with Algorithms) 2014 キーワード: ゾンビ Picture by Assembléetest

“Liveness-Based Garbage Collection” 3: 読んだ紹介論文 Reading: “Liveness-Based Garbage Collection”

論文概要 キーワード: “Liveness-Based Garbage Collection” ガベージコレクション 文脈自由言語 逆元 CC (Compiler Construction) 2014 キーワード: ガベージコレクション 文脈自由言語 逆元 もっとゴミ 既存のゴミ

Garbage Collection プログラムの実行中に、「もう不必要になった」 メモリ領域を解放して再利用する機構 「もう不必要になった」とは? 既存手法: 今のスタック変数(など)からポインタをどれだけ辿ってもたどり着けない領域のこと 提案手法: プログラムを解析して、今後のプログラム実行で決して触らないと判断できる領域は到達可能でも容赦なく解放する

対象言語 e f e f (cons e f) (car e) (cdr e) if 文, 関数定義, 再帰 メモリの書き換え(破壊的代入)は無し e f (cons ) = 1 e f

例 .... (car (cons ☆ △)) ... ☆ △ このプログラムを実行中。☆を実行。△を実行。 そして cons を実行。 メモリ状態 = △ 部分は今後絶対触らない !!!捨てろ! .... (car (cons ☆ △)) ... 1 ☆ △

もう少しフォーマルに例 今注目している式 ....(car ☆).... の返値には、今後プログラムの実行中にポインタ   L ⊆ {0,1}* でしかアクセスしないことがわかっているとする  car の引数 ☆ の値には、ポインタ {0w | w∈L} でしかアクセスしない。 (ポインタ1側は捨てて良い)

式での「逆算」 (car ☆) に L でアクセス  ☆には {0w | w∈L} で。 (cdr ☆) に L でアクセス  ☆には {1w | w∈L} で。 (cons ☆ △) に L でアクセス  ☆ には {w | 0w ∈ L} でアクセス。 △ には {w | 1w ∈ L} でアクセス。 (if ☆ then △ else ◇) に L でアクセス  ☆ には {ε} でアクセス △ には L でアクセス ◇ には L でアクセス

関数定義 f(x) := ..... if ..x.. then ... x .... f(x) の返値に L でアクセス  引数xには、 ∪xの出現 “関数定義全体にLでアクセス”から逆算したxへのアクセス ※ 再帰関数がある場合この定義も再帰的になる

文脈自由文法 f(x) := car(cdr(x)) g(x) := f(f(x)) F ::= 10 G ::= FF どちらの処理も L を後ろにappendする形なので、 前に足すパス文字列だけ見る f と g の「逆算」関数は [f](L) = {10w | w∈L} [g](L) = [f]([f](L)) F ::= 10 G ::= FF

めんどくさいケース: cons 00 -> ε 11 -> ε (cons ☆ △) に L でアクセス  ☆ には {w | 0w ∈ L} でアクセス。 △ には {w | 1w ∈ L} でアクセス。 L の前に何かをprependという規則になっていない さっきのやり方で文法に変換するのが難しい (cons ☆ △) に L でアクセス  ☆ には {0w | w ∈ L} でアクセス。 △ には {1w | w ∈ L} でアクセス。 00 -> ε 11 -> ε パス文字列を”削る”操作を表す左逆元 0 1 を導入して無理矢理 文脈自由文法として扱えるようにする

めんどくさいケース: if (if ☆ then △ else ◇) に L でアクセス  ☆ には {ε} でアクセス △ には L でアクセス ◇ には L でアクセス L の前に何かをprependという規則になっていない 関数定義の逆算のところでそもそも分けて考えることにする (返値に漏れるアクセスとそうでないアクセスを分けて考える)

めんどくさいケース: if f(x) := ..... if ..x.. then ... x .... f(x) の返値に L でアクセス  引数xには、返値経由では、 ∪ifの外のxの出現 Lから逆算したxへのアクセス  引数xには、関数内では、 ∪ifの中のxの出現 Lから逆算したxへのアクセス

例 append(x,y) := [append_in_x] ::= ε [aapend_in_y] ::= ∅ if nil?(x) then y else cons(car(x), append(cdr(x),y)) [append_in_x] ::= ε [aapend_in_y] ::= ∅ [append_out_x] ::= 00 | 1 [append_out_x] 1 [append_out_y] ::= ε | [append_out_y] 1

GCの実行 プログラムの各時点で、今後アクセスする可能性のあるパス集合を求められるようにしておく その集合の範囲外のノードを判定して回収しまくる

プログラムの各時点で、今後アクセスする可能性のあるパス集合を求められるようにしておく 関数を呼び出すたびに、スタックに「今後のアクセス」を表す言語(を表した文法)を積む このスタックの concat と union で求まる gからreturnしたあとfにreturnするまでを表す言語 gの中でのアクセスを表す言語 関数 gを呼んだ 関数 f 実行中 スタック スタック

その集合の範囲外のノードを判定して回収しまくる さっきのスタックを使うと、各変数からの「今後使う可能性があるアクセスパス」がわかるので その範囲をマーキング x y z

注意事項: 00, 11 の扱い 作った文法は 0 や 1 という便宜上の記号が入っていて直接パスに対応しないので、 論文では、 CFG を正規言語で近似。 NFA にして、00 と 11 による遷移にε辺を張りまくる としてこれらを消す近似をしていました Appendの例 “A ::= 00 | 1 A 1” は “1*001*” になる

注意事項: traverseしまくり 普通のGCは「到達可能な範囲」をマークするので、 一度(他の変数経由などで)到達したブロックの先は全部到達可能なので、見る必要がない 提案手法のGCは、変数毎にアクセスパス集合が違うのでそれぞれから共有部分もたどらないといけない

議論しましょう CFG を正規言語で近似する必要は本当にあるのか? 複数回のtraverseが起きないように何かかっこいい実装できないか? (あるいは逆に、実際のメモリリークを考えると、もっとずっと弱い表現で近似してもよいという可能性はないか?) 複数回のtraverseが起きないように何かかっこいい実装できないか? その他、これを実用に耐えるものにしようと思ったらどうするといいか?