Allowing Unsafe Rules in Datalog?

Certain rules are considered "unsafe" and disallowed in Datalog because they don't restrict all of their variables to a finite domain (and therefore may not have a finite number of solutions). For instance, in:

beef(X) :- lemur(X), not(alice(X, Y)), not(bahnanlagen(Y)).

Y is not restricted to a finite domain, so the rule is unsafe. Additionally, no use of the beef predicate can further restrict the domain of Y. However, a rule may be unsafe only because its distinguished variables are not restricted:

orange(X) :- zorro(Y), X < Y.

A predicate like orange/1 doesn't seem different from a negated relational predicate or an arithmetic predicate, since its otherwise unrestricted variables can be further restricted by the context in which it is used. For instance, a rule like:

fromage(X) :- elephant(X), orange(X).

...appears to be safe (where elephant/1 and zorro/1 are safe relational predicates). After all, the apparently equivalent:

fromage(X) :- elephant(X), zorro(Y), X < Y.

...is safe in that case. Provided their use is restricted in the same fashion as negated and arithmetic predicates, are there any problems with permitting this latter kind of unsafe rule that I'm just not seeing?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

safety and datalog

The standard Datalog simply does not admit built-in predicates. In an extended Datalog, all the vars should be range restricted as in your last query.

I did not think too hard about it, but unfolding a non-recursive query to its ground terms would allow to see if it is safe. I am pretty sure that query transformation to a potentially safe form is impossible with an arbitrary recursive query.

In any case, you can always use Prolog where unsafe clauses are OK :-)


Edited:
I meant of course "its edb predicates" rather than "its ground terms ".

I think in the recursive

I think in the recursive case an "unsafe" term has to be treated in the same way a negated relational term, though I'm not sure whether that extends to creating another level of stratification.