- From: Axel Polleres <axel.polleres@deri.org>
- Date: Wed, 11 Feb 2009 00:48:11 +0000
- To: "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>

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