[Core] ACTION-703: More sophisticated notions of safety

was: ACTION-703: Investigate implementations that will reject infinite 
rulesets


Part 1:
- I contacted implementers of Answer set programming engines. Although 
only the dlv [1] implementers got back to me, and I only tried out some
unrestricted example with smodels/lparse [2], I summarize that this 
confirmed so far my impression that the general notion of safety we have 
at the moment which allows infinite ground programs would NOT be 
accepted by ASP engines without further restrictions.
  These systems need normally a stornger definition of safety, i.e. that 
each variable in the rule head is bound in a non-external body atom (not 
talking about discjunctions in bodies here).

Part 2:
There exist more sophisticated notions of safety such as e.g.
strong saftey [3] which I will shortly sketch in the following.
Other works which introduce classes of programs with
infinite domains that can be dealt with in  Answer set programming 
include [4,5]

Now for strong safety, citing p.95 of [3]:

"Informally, a rule is strongly safe, if its external atoms receive 
their input from a lower stratum of the program. This way, even if they 
occur in a cycle, their output cannot grow infinitely, since the size of 
their input is fixed "before entering" the cycle."

External predicates are here somewhat like our built-in predicates, 
where each external predicate has input and output parameters, which we 
can model by binding patterns. That is, each external predicate has, 
without loss of generality the form f(Y, X), such that Y, X are vectors 
of parameters where Y are the inputs and X are the outputs of the 
predicate, i.e. there exists a binding pattern which guarantees that f 
has a finite extension if the values of Y are bound to fixed values.

To ease the pain for you on going through the formal definitions in [3], 
I'll try to paraphrase it for our needs.

I only consider rules without disjunction in the rule body here and do 
not consider external functions but only predicates, i.e. a rule set is 
a set of rules

  h(...) :- b1(...), ..., bk(...), f1(Y1, X1 ), ... fn(Yn, Xn ).

where h(...) is the head, b1(...),...., bk(...) are ordinary predicates 
and f1(Y1, X1 ), ... fn(Yn, Xn ) are external predicates.

========================================================================
We first build a dependency relation R between all head and body atoms 
(ordinay or external) occurring in a ruleset P as follows:

* if h occurs in head of a rule r and b in the body of r then add (h,b).
* if b occurs in the body of a rule r and h in the head of r' such that
b and h unify, then add (b,h)
* if b is either an external predicate with x in its output variables X 
or an ordinary predicate with variable x, and b' is an external 
predicate with x in its input variables such that b,b' appear in the 
same rule body, then add (b',b).

We say a depends on b if (a,b) is in R.
We say a transitively depends on b, if (a,b) is in the transitive 
closure R* of R.
We say a strictly depends on b if (a,b) in R* but not vice versa.


We are now ready to define strong safety:

Let r be a rule in P with external predicates
     f1(Y1, X1 ), ... fn(Yn, Xn ) in Body(r)

Let further E be the set of all variables in the union of all variables 
in Yi, i.e. the union of all "input variables".

Moreover, let S be the set of atoms b in Body(r), i.e. body atoms, such 
that Head(r) depends strictly on b.

  Let V be the set of all variables that occur in the ordinary atoms in 
S plus all variables in the output list of the external atoms in S . 
Then, r is strongly safe, iff r is safe in the traditional sense, i.e. 
all head variables appear in the body and additionally E is a subset of V.
========================================================================

Thas is just a simplified transcript of the definition in [3] which 
leaves out that rules there can also be negated with default negation, 
there could be more than one head predicate, and that actually 
predicates are allowed as "inputs" in the language used there.


As you can verify:

  a(1)
  a(x) :- a(y), x = y +1.

is not strongly safe following this definition, whereas.

  b(1).
  a(x) :- b(y), x = y +1.

is.

1. http://www.dlvsystem.com

2. http://www.tcs.hut.fi/Software/smodels/

3. Roman Schindlauer. Answer-Set Programming for the Semantic Web. PhD 
thesis, Vienna University of Technology, Austria, December 2006.
http://www.kr.tuwien.ac.at/staff/former_staff/roman/papers/thesis.pdf

4. Mantas Šimkus and Thomas Eiter. FDNC: Decidable Non-monotonic 
Disjunctive Logic Programs with Function Symbols. LPAR 2007.
http://www.springerlink.com/content/y75377w6mp3p1595/

5. F. Calimeri, S. Cozza, G. Ianni, N. Leone.
"Computable Functions in ASP: Theory and Implementation".
Proceedings of the 24th International Conference on Logic Programming -- 
ICLP'08, LNCS Vol. 5366, December 9--13, 2008, Udine, Italy. pp. 407--424.

-- 
Dr. Axel Polleres
Digital Enterprise Research Institute, National University of Ireland, 
Galway
email: axel.polleres@deri.org  url: http://www.polleres.net/

Received on Wednesday, 11 February 2009 00:48:58 UTC