Document

Embedding CHR in LMNtal
上田研究室
M2 原耕司
2005/06/07(Wed)
1 / 20
Motivation

CHR は強力な制約処理系で応用例も多い




Scheduling, Planning, Timetabling, Layout,
Placement, Verification [Frü05]
CHR は字面上は LMNtal で書ける
Propagation rule の実行で無限ループ
現状、実行はできていない。

CHR Interpreter on klic [加藤02] も未対応
2 / 20
Motivation (2)

LMNtal にあって CHR にないもの



膜（実行制御、計算の局所化）
分散・並列実行
良い部分を組み合わせたい！
3 / 20
Our Goal



LMNtal で CHR の Propagation rule を
重複なく適用できるようにする。
CHR のアプリが LMNtal 処理系でも
（高速に）動作し、
分散・並列実行ができる事を示す。
4 / 20
CHR Applications

POPULAR [Mol94, FMB96, FrBr97]



社内コードレスホンシステムの
無線APをどこに設置する？問題
Siemens R&D などが開発
時間割作成・教室割り当て [Abd00]


University of Minich で運用
1000 講義/週
5 / 20
What is CHR

Operational Semantics and Confluence
of Constraint Propagation
Rules[Abd97]


実装に近い立場からの操作的意味論
上記論文に沿って説明します
6 / 20
Syntax

Simplification rule


Rulename @ H1, ..., Hi <=> G1, ..., Gj | B1, ..., Bk
消す
Propagation rule

Rulename @ H1, ..., Hi ==> G1, ..., Gj | B1, ..., Bk
残す

Simpagation rule

Rulename @ H1, ..., HL \ HL+1, ..., Hi <=> G1, ..., Gj | B1, ..., Bk
残す

消す
実はすべて Simplification rule に直せる
7 / 20
Declarative Semantics
宣言的意味

Theory and Practice of Constraint
Handling Rules[Frü98]より
8 / 20
Operational Semantics
操作的意味

これらから成る



States
Computation steps
Initial and final states
9 / 20
⊂ States × States
State
States

GS ：ゴールストア
ユーザ定義制約と組み込み制約が入る



CU ：ユーザ定義制約ストア
CB ：組み込み制約ストア
Τ ：トークン（propagation rule 関連）
Set of ルール名 @ 反応できるユーザ定義制約

ν
：GS, CU, CB に出てくる変数
10 / 20
State :
Computation steps
State の正規化関数
11 / 20
T(C, CU)
直感的な説明：
C∧CUの一部が propagation rule の左辺と
unify するならその制約を返す
(
)
要らない？
12 / 20
Example Computation
13 / 20
Initial and Final States
Initial state
Final state
これ以上遷移できなく、CB ∋ false
→成功
→失敗
14 / 20
Example – Loop detect
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).
ポイント：
edgeデータは消費されない
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 は省略)
15 / 20
現状の LMNtalで書いてみる
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]), @601
==>
loop([3,10,7,5,8]), loop([3,10,7,5,8]), @601
==>
loop([3,10,7,5,8]), loop([3,10,7,5,8]), loop([3,10,7,5,8]), @601
==> ......
16 / 20
(edge は省略)
問題点


同じ変数（の組み合わせ）に対して
propagation rule が何回も適用される
CHR の各種処理系では各自の工夫で
回避している


マッチした構造の履歴を記録
chr.hs in HaskellCHR [Gregory J. Duck 04]
処理系依存
CHR on LMNtal でも考えなければならない
17 / 20
CHR の処理系いろいろ

CHR module on SWI-Prolog


HaskellCHR, ToyCHR on Prolog




Gregory J. Duck
CHR Interpreter on klic

?
Tom Schrijvers
Norio Kato
/home/n-kato/klic/chr/
on LMNtal

Koji Hara
18 / 20
LMNtal の他の話題との関連



集合（not 多重集合）は必要？
優先度との関連は？
π計算の ! との関連は？
19 / 20
今後の研究




CHR の論文や処理系のソースを読む
履歴管理のアルゴリズムを検討
実装
CHR の例題を LMNtal 化する

ライブラリの整備が必要かも


operator(100, xfx, ‘::’) など
実行速度、メモリ効率などを測定する
20 / 20

Download Report