simplificationの修正(1)

[yoshihiro503]

（１）現状のsimplificationの修正について

現状simplificationすると、ビューに関するΔ述語をheadとするルールが、他で使われていなくても残ってしまっています。ビューに関するΔ述語については通常の述語と同様に、他で使われていなかったら消して頂きたいです。

具体例（１）：

source ps('A':int, 'B':int).
view pv('A':int).
-ps(A, B) :- ps(A, B) , ps(A, GENV9) , A = 1 , A <> 4.
-pv(GENV1) :- ps(GENV1, GENV7) , GENV1 = 1 , GENV1 <> 4.
+ps(A, B) :- A = 4 , ps(GENV10, GENV11) , GENV10 = 1 , GENV10 <> 4 , not ps(A, GENV1) , ps(GENV2, B) , ps(GENV2, GENV12) , GENV2 = 1 , GENV2 <> 4.
+ps(A, B) :- A = 4 , ps(GENV13, GENV14) , GENV13 = 1 , GENV13 <> 4 , not ps(A, GENV3) , not -ps(GENV4, GENV5) , B = -100.
+pv(GENV1) :- GENV1 = 4 , ps(GENV1_2, GENV8) , GENV1_2 = 1 , GENV1_2 <> 4.
pv(A) :- ps(A, GENV6).

このルールをsimplificationすると、以下の出力を得る。

source ps('A':int, 'B':int).
view pv('A':int).
+ps(A, B) :- ps(GENV13, _) , not -ps(_, _) , not ps(A, _) , A = 4 , B = -100 , GENV13 = 1.
+ps(A, B) :- ps(GENV10, _) , ps(GENV2, B) , not ps(A, _) , A = 4 , GENV10 = 1 , GENV2 = 1.
+pv(GENV1) :- ps(GENV1_2, _) , GENV1 = 4 , GENV1_2 = 1.
-pv(GENV1) :- ps(GENV1, _) , GENV1 = 1.
-ps(A, B) :- ps(A, B) , A = 1.

ここには、ビューに関するΔ述語+pvと-pvheadとするルールが存在しており、かつ+pv -pvはともに他のルールで使われていません。
したがってこれらのルールを消して頂きたいです。理由は、ビューに対する更新をソースに書き換えるのが目的ですのでビューに対する更新が残らないようにして欲しいからです。但し、他で使われている場合は残して頂き、最終的にdl2uするときに対応するように修正をお願いします。このdl2uの修正はこのあとに説明します。
上記の
ルールのsimplificationについて、望ましい結果は以下の通りです。

source ps('A':int, 'B':int).
view pv('A':int).
+ps(A, B) :- ps(GENV13, _) , not -ps(_, _) , not ps(A, _) , A = 4 , B = -100 , GENV13 = 1.
+ps(A, B) :- ps(GENV10, _) , ps(GENV2, B) , not ps(A, _) , A = 4 , GENV10 = 1 , GENV2 = 1.
-ps(A, B) :- ps(A, B) , A = 1.

具体例(2): ビューに関する述語が残る例

これは現状のsimplificationで望ましい結果が得られていますが、具体例(1)の修正を行うときにこの結果が得られるように注意してください。

source b('B':int, 'C':int).
source a('A':int, 'B':int).
view v('A':int, 'B':int, 'C':int).
-a(A, B) :- a(A, B) , not __updated__v(A, B, GENV1).
-b(B, C) :- b(B, C) , a(GENV2, B) , b(B, GENV3) , not -v(GENV2, B, GENV3) , not __updated__v(GENV4, B, C).
-b(B, C) :- b(B, C) , +v(GENV2, B, GENV3) , not __updated__v(GENV4, B, C).
-v(GENV1, GENV2, GENV3) :- a(GENV1, GENV2) , b(GENV2, GENV3) , GENV2 = 30 , GENV2 <> 60.
+a(A, B) :- a(A, B) , b(B, GENV5) , not -v(A, B, GENV5) , not a(A, B).
+a(A, B) :- +v(A, B, GENV5) , not a(A, B).
+b(B, C) :- a(GENV6, B) , b(B, C) , not -v(GENV6, B, C) , not b(B, C).
+b(B, C) :- +v(GENV6, B, C) , not b(B, C).
__updated__v(A, B, C) :- a(A, B) , b(B, C) , not -v(A, B, C).
__updated__v(A, B, C) :- +v(A, B, C).
v(A, B, C) :- a(A, B) , b(B, C).

これを、simplificationすると、以下のように望ましい結果を得られています。

source a('A':int, 'B':int).
source b('B':int, 'C':int).
view v('A':int, 'B':int, 'C':int).
-a(A, B) :- a(A, B) , not __updated__v(A, B, _).
-b(B, C) :- a(GENV2, B) , b(B, C) , b(B, GENV3) , not -v(GENV2, B, GENV3) , not __updated__v(_, B, C).
__updated__v(A, B, C) :- a(A, B) , b(B, C) , not -v(A, B, C).
-v(GENV1, GENV2, GENV3) :- a(GENV1, GENV2) , b(GENV2, GENV3) , GENV2 = 30.