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

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 UTC