-
Notifications
You must be signed in to change notification settings - Fork 9
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Applicability of Rules Depend on their Order in the Rule File #64
Comments
I think the problem is in the filtering of the restricted chase, which does not seem to work correctly with multihead rules that share an existential variable. For now, you can work around it by using the "--rewriteMultihead true" option for vlog. |
I have "fixed" this issue by always rewriting existential multi-head rules. |
Hi. If by "always rewriting existential multi-head rules" you mean always executing this function, then please be aware that it might affect termination of some existential rule programs when executing the restricted chase |
Hi Larry, can you elaborate on that? Because yes, that is what I mean.
For instance, the rule
e(N1,N), e(N,N2) :- rule1(X,N1), derived1(X,N2)
would be rewritten to:
…__Generated_Head_0(N1, N2, N) :- rule1(X,N1), derived(X, N2)
e(N1, N) :- __Generated_Head_0(N1, N2, N)
e(N, N2) :- __Generated_Head_0(N1, N2, N)
Do you mean that such a transformation is not correct?
On 22 Nov 2022, at 16:03, Larry González ***@***.***> wrote:
Hi. If by "always rewriting existential multi-head rules" you mean always executing this function, then please be aware that it might affect termination of some existential rule programs when executing the restricted chase
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you modified the open/close state.
|
The transformation is correct, but it affects termination of the restricted chase Let P be a existential rule program, and P' its transformation with single-headed rules. As an example let's consider the program
The restricted chase sequence would be then
which terminates.
And its restricted chase sequence would be something like:
which is non-terminating. Essentially the problem is that the freshly introduced Datalog rules propagate every null because they are not restricted in anyway (because they are Datalog). This has been mentioned by Krötzsch here and by Carral et al. here (Theorem 28). I am sure there are other references but I don't have them at the top of my head PD. @irina-dragoste provided the example, :) |
Basically, rules with multiple head atoms that would be satisfied in the restricted chase are no longer satisfied, as the fresh predicate in the rewriting is not produced elsewhere. Here is another example ruleset with a more complex multi-head that loses termination if re-writen.
|
Would also adding a Datalog rule
fresh(x,y) :- R(x,y) A(y)
resolve this?
… On 22 Nov 2022, at 17:44, Larry González ***@***.***> wrote:
The transformation is correct, but it affects termination of the restricted chase
Let P be a existential rule program, and P' its transformation with single-headed rules.
There are some cases in which P terminates for all strategies, but P' does not.
As an example let's consider the program
A(c) .
R(y,x) :- R(x,y) .
R(x,y),A(y) :- A(x) .
The restricted chase sequence would be then
A(c)
A(c) R(c,n1)
A(n1)
A(c) R(c,n1)
A(n1) R(n1,c)
which terminates.
On the other hand, the transformed existential rule program would be like:
A(c) .
R(y,x) :- R(x,y) .
fresh(x,y) :- A(x) .
R(x,y) :- fresh(x,y) .
A(y) :- fresh(x,y) .
And its restricted chase sequence would be something like:
A(c)
A(c) fresh(c,n1)
A(c) fresh(c,n1) R(c,n1)
A(c) fresh(c,n1) R(c,n1)
R(n1,c)
A(c) fresh(c,n1) R(c,n1)
A(n1) R(n1,c)
...
which is non-terminating.
Essentially the problem is that the freshly introduced Datalog rules propagate every null because they are not restricted in anyway (because they are Datalog). This has been mentioned by Markus here and by David et al. here. I am sure there are other references by I don't have them at the top of my head
PD. @irina-dragoste provided the example, :)
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you modified the open/close state.
|
I don't think so (maybe I interpreted your suggestion wrongly) The problem is that Let's consider the program
here But this is considering only this particular example. It would still remain to discuss how this (new) transformation would be in the general case |
Ok, apparently I don’t understand how the restricted chase works in the multi-headed case.
How is it that fresh(x,y) :- A(x) is not blockable but R(x,y),A(y) :- A(x) is?
… On 23 Nov 2022, at 12:45, Larry González ***@***.***> wrote:
I don't think so (maybe I interpreted your suggestion wrongly)
The problem is that rule2 -in the following code chunk- is not blockable
Let's consider the program
rule0: A(c) .
rule1: R(y,x) :- R(x,y) .
rule2: fresh(x,y) :- A(x) .
rule3: R(x,y) :- fresh(x,y) .
rule4: A(y) :- fresh(x,y) .
rule5: fresh(x,y) :- R(x,y), A(y) .
here rule5 has a trigger only after fireing rule3 and rule4, which necessarily creates a new atom to fire rule2, repeting the cicle. Furthermore, the trigger for rule5 is not active
But this is considering only this particular example. It would still remain to discuss how this (new) transformation would be in the general case
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you modified the open/close state.
|
This is actually not true. Rule2 can be applied only after all Datalog rules (including rule5) have been saturated, creating |
Yes, here Carral et al. here propose the 2-way atomic decomposition (Definition 32) that preserves Datalog-first restricted chase termination (Theorem 37). It would be ideal to solve the multi-head bug without this workaround or rewriting rules. But if this is too difficult or time consuming to solve, I guess the 2-way atomic decomposition is the best solution |
Thanks for pointing this out. I did not considered Datalog-first restricted chase, which VLog implements
Yes. It would |
Thank you for the clarification! It seems I’m re-inventing the wheel... I would like to solve the multi-head bug without the workaround, but at the moment don’t know how to do that. So, for now, I’ll implement the "2-way atomic decomposition”.
… On 23 Nov 2022, at 16:00, Irina Dragoste ***@***.***> wrote:
Would also adding a Datalog rule fresh(x,y) :- R(x,y) A(y) resolve this?
Yes, here Carral et al. here propose the 2-way atomic decomposition (Definition 32) that preserves Datalog-first restricted chase termination (Theorem 37).
So this 2-way atomic decomposition solution to the multi-head bug would preserve termination, but potentially slow down reasoning, as it introduces new rules.
It would be ideal to solve the multi-head bug without this workaround or rewriting rules. But if this is too difficult or time consuming to solve, I guess the 2-way atomic decomposition is the best solution
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you modified the open/close state.
|
FYI, with the above commits, reasoning is now correct. |
I have the instance
t.csv
:and the rules in file
rules
:The three-rule blocks (starting with rule1-4) create some facts (derived1 and derived2) and create a graph structure (predicate e). Running vlog in version 6f9d199 shows wrong behavior on the very last. Although vlog recognizes a match for the body of the rule, it does not derive any new tuples. To show this behavior, we have included the following auxiliary rules:
While vlog has a match for
body
and materializes it, it does not derive any tuples inhead
. The expected behavior can be observed when moving the last rule in filerules
to an earlier position in the file, e.g.,rules2
:With the first rule file, there are 14 derivations and with the second one, there are 17. The auxiliary rules indicate the second one to be actually sound and complete. Unfortunately, I was not able to reduce the example any further. If one of the three-rule blocks unrelated to this last rule is missing, the error is not observable.
I used the following call string:
vlog mat --storemat_path . --storemat_format csv --decompressmat 1 --rules [RULEFILENAME]
, where[RULEFILENAME]
ranges over byrules
andrules2
. I've been usingedb.conf
:as configuration file.
The text was updated successfully, but these errors were encountered: