Embedding CHR in LMNtal

Presentation on theme: "Embedding CHR in LMNtal"— Presentation transcript:

1 Embedding CHR in LMNtal
上田研究室 M2 原　耕司 2005/06/07(Wed) 1 / 20

2 Motivation しかし CHR は強力な制約処理系で応用例も多い
Scheduling, Planning, Timetabling, Layout, Placement, Verification [Frü05] CHR は字面上は LMNtal で書ける しかし Propagation rule の実行で無限ループ 現状、実行はできていない。 CHR Interpreter on klic [加藤02] も未対応 2 / 20

3 Motivation (2) LMNtal にあって CHR にないもの 良い部分を組み合わせたい！ 膜（実行制御、計算の局所化）
分散・並列実行 良い部分を組み合わせたい！ 3 / 20

4 Our Goal LMNtal で CHR の Propagation rule を重複なく適用できるようにする。
CHR のアプリが LMNtal 処理系でも（高速に）動作し、 分散・並列実行ができる事を示す。 4 / 20

5 CHR Applications POPULAR [Mol94, FMB96, FrBr97] 時間割作成・教室割り当て [Abd00]
Siemens R&D などが開発 時間割作成・教室割り当て [Abd00] University of Minich で運用 1000 講義/週 5 / 20

6 What is CHR Operational Semantics and Confluence of Constraint Propagation Rules[Abd97] 実装に近い立場からの操作的意味論 上記論文に沿って説明します 6 / 20

7 Syntax Simplification rule Propagation rule Simpagation rule
H1, ..., Hi <=> G1, ..., Gj | B1, ..., Bk Propagation rule H1, ..., Hi ==> G1, ..., Gj | B1, ..., Bk Simpagation rule H1, ..., HL \ HL+1, ..., Hi <=> G1, ..., Gj | B1, ..., Bk 実はすべて Simplification rule に直せる 消す 残す 残す 消す 7 / 20

8 Declarative Semantics 宣言的意味
Theory and Practice of Constraint Handling Rules[Frü98]より 8 / 20

9 Operational Semantics 操作的意味
これらから成る States Computation steps ⊂ States × States Initial and final states State 9 / 20

10 States GS ：ゴールストア ユーザ定義制約と組み込み制約が入る CU ：ユーザ定義制約ストア CB ：組み込み制約ストア
Τ ：トークン（propagation rule 関連） 　Set of 反応できるユーザ定義制約 ν ：GS, CU, CB に出てくる変数 10 / 20

11 State : Computation steps State の正規化関数 11 / 20

12 T(C, CU) ( ) 直感的な説明： C∧CUの一部が propagation rule の左辺と unify するならその制約を返す
( ) 要らない？ 12 / 20

13 Example Computation 13 / 20

14 Initial and Final States
Initial state Final state これ以上遷移できなく、CB ∋ false →成功 →失敗 14 / 20

15 Example – Loop detect (edge は省略) ポイント： edgeデータは消費されない
edge(A,B), edge(B,C), edge(C,D), edge(D,E), edge(E,A) ==> loop([A,B,C,D,E]). edge(1,4), edge(1,9), edge(2,8), edge(3,10), edge(5,1), edge(5,8), edge(7,4), edge(7,5), edge(7,10), edge(8,3), edge(8,9), edge(9,3), edge(10,7). loop([3,10,7,5,8]), loop([8,3,10,7,5]), loop([5,8,3,10,7]), loop([7,5,8,3,10]), loop([10,7,5,8,3]). ポイント： edgeデータは消費されない (edge は省略) 15 / 20

16 現状の LMNtalで書いてみる (edge は省略)
edge(A0, B0), edge(B1, C0), edge(C1, D0), edge(D1, E0), edge(E1, A1) :- A0=A1, B0=B1, C0=C1, D0=D1, E0=E1 | edge(A0, B0), edge(B1, C0), edge(C1, D0), edge(D1, E0), edge(E1, A1), loop([A0, B0, C0, D0, E0]). edge(1,4), edge(1,9), edge(2,8), edge(3,10), edge(5,1), edge(5,8), edge(7,4), edge(7,5), edge(7,10), edge(8,3), edge(8,9), edge(9,3), edge(10,7). ==> loop([3,10,7,5,8]), loop([3,10,7,5,8]), loop([3,10,7,5,8]), ==> (edge は省略) 16 / 20

17 問題点 同じ変数（の組み合わせ）に対してpropagation rule が何回も適用される
CHR の各種処理系では各自の工夫で 回避している マッチした構造の履歴を記録 chr.hs in HaskellCHR [Gregory J. Duck 04] 処理系依存 CHR on LMNtal でも考えなければならない 17 / 20

18 CHR の処理系いろいろ ? CHR module on SWI-Prolog HaskellCHR, ToyCHR on Prolog
Tom Schrijvers HaskellCHR, ToyCHR on Prolog Gregory J. Duck CHR Interpreter on klic Norio Kato /home/n-kato/klic/chr/ on LMNtal Koji Hara ? 18 / 20

19 LMNtal の他の話題との関連 集合（not 多重集合）は必要？ 優先度との関連は？ π計算の ! との関連は？ 19 / 20

20 今後の研究 CHR の論文や処理系のソースを読む 履歴管理のアルゴリズムを検討 実装 CHR の例題を LMNtal 化する
ライブラリの整備が必要かも operator(100, xfx, ‘::’) など 実行速度、メモリ効率などを測定する 20 / 20