From: Axel Polleres <axel.polleres@deri.org>

Date: Wed, 11 Feb 2009 06:12:29 +0000

Message-ID: <49926C4D.6050505@deri.org>

To: "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>

Date: Wed, 11 Feb 2009 06:12:29 +0000

Message-ID: <49926C4D.6050505@deri.org>

To: "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>

Axel Polleres wrote: > > 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 s/a set of rules/of the form/ > 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 06:13:16 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Tuesday, 2 June 2009 18:34:03 GMT
*