Built-in Arithmetic in Knowledge Representation Languages
Contents
1. 1 is shown by giving a machine in NP that first guesses a stable model and then checks its stability in polytime The existence of such a guessing procedure is guaranteed by the A restrictedness property of the ASP program Corollary 1 ASP language of Lparse and Gringo captures small cost arithmetical NP problems Corollary 2 The IDP language captures the small cost arithmetical NP problems Proof By Theorem 1 GGF covers all small cost NP structures However we know that except for characteristic function x IDP supports all the rest of GGF So we only need to show that x can be written in terms of other arithmetical functions This is easy to show x 1 o 3 2 Non expressibility Results This part considers some natural arithmetical problems and shows that they cannot be encoded using only built in arithmetic of ASP languages or the input language of the IDP system Two such problems are considered the Integer Factorization problem and the Quadratic Residue Problem We first define them Integer Factorization is a natural arithmetical problem with wide applications in cryp tography You are given a number n and asked to either report it as a prime or find one of its nontrivial factors a positive factor except 1 and n itself As a side note although checking primality is in polytime it is not known if finding nontrivial factors of a com posite number can also be done in polytime Also there are several other versions2. 5 Examples of PBINT Axiomatizations In this section we give some examples of PBINT axiomatizations to demonstrate the naturality of them These examples include the two examples of integer factorization and quadratic residue so as to contrast against the results of Section 3 Example 2 Disjoint Scheduling Given a set of Tasks t1 tn and a set of con straints find a scheduling that satisfies all the constraints Each task t has an earliest starting time EST t a latest ending time LET t and a length L t There are also two predicates P t tj and D t tj which say respectively that task t should end before task t starts nd two tasks t and tj cannot overlap We are asked to find two functions sae i and end t satisfying te given conditions In PBINT we axiomatize this problem as follows Instance vocabulary consists of symbols EST LET L Task P and D Expansion vocabulary consists of two functions start and end The axiomatization below first gives the upper guards on these functions and then the axioms VtVs start t s gt Task t A s lt SIZE V s default no end t e gt Task t A lel lt SIZE V e default ti Task t gt start t gt EST t ti Task t gt end t lt LET ti ti Task t gt start t L t end t ve Vt Plt ti tj gt end t lt start t VEVE D ti j gt end t lt start t V end t lt start t SP ee In a
3. L Libkin Elements of Finite Model Theory 2004 L Libkin Embedded Finite Models and Constraint Databases pages 257 338 Springer 2007 D G Mitchell and E Ternovska A framework for representing and solving NP search problems In Proc AAAI 05 2005 D G Mitchell and E Ternovska Expressiveness and abstraction in ESSENCE Con straints 13 2 343 384 2008 A Skelley Theories and Proof Systems for PSPACE and the EXP Time Hierarchy PhD thesis University of Toronto 2005 D Suciu Domain independent queries on databases with external functions Theor Comput Sci 190 2 279 315 1998 T Syrj nen Lparse 1 0 User s Manual 2000 http www tcs hut fi Software smodels lparse ps gz E Ternovska and D G Mitchell Declarative programming of search problems with built in arithmetic In Proc of 21st International Joint Conference on Artificial Intel ligence IJCAI 09 pages 942 947 2009 R Topor Safe database queries with arithmetic relations In Proc 14th Australian Computer Science Conf pages 1 13 1991 S Tasharrofi and E Ternovska PBINT a logic for modelling search problems involv ing arithmetic In Proceedings of the 17th Conference on Logic for Programming Ar tificial Intelligence and Reasoning LPAR 17 Yogyakarta Indonesia October 2010 J Wittocx and M Marien The IDP System KUL August 2009 http www cs kuleuven be dtai krr software idpmanual pdf
4. Results Definition 4 An Arithmetical structure is a structure N containing at least N 0 1 Xs lt T 9 min MAT i IT with domain N the natural numbers and where min max X and IT are multi set operations and x T is the characteristic function Other functions predicates and multi set operations may be included provided every function and relation of N is polytime computable Definition 5 For an embedded arithmetical structure D define cost D the cost of D to be log 1 1 where is the largest number in adom 4 Definition 6 Small cost structures A class K of embedded arithmetical structures has small cost if there is some k N such that cost D lt adomp for every D K Next we are going to give a theorem that relates the expressibility power of ASP over arithmetical structures to the expressive power of GGF fragment of logic How ever ASP programs are traditionally defined over relational structures and thus we have to extend this notion to arbitrary structures In order to do this we define restricted ASP Programs Definition 7 A restricted ASP Programs Let B v r denote the set of predicate symbols that appear in the body of rule r with variable v as a term in it i e the term consists of only variable v Also let V r denote all the free variables in r and Rrr p 3 Multi sets are generalizations of sets that allow multiple occurrence of elements denote all rules in A
5. constant SIZE The constant SIZE is equal to adom 4 x S where adom 4 is the number of elements in the active domain and S is the size of binary encoding of the maximum element of the active domain In other words SIZE upper bounds the number of bits needed to encode in binary the input structure A embedded in V We also need a constant default denoting a particular default value needed in upper guards on functions Its meaning is specified by the user Logic PBINT We introduce a new logic PBINT standing for Polynomially Bounded Integers This logic is a variant of the double guarded logic except we use compact arithmetical structures and allow function symbols in both and or new kinds of guards with more freedom in existential and upper guards on the outputs of expansion functions The three forms of guards in PBINT are as follows 1 Instance Guards are instance relations including adom 4 interpreted by the in stance structure A Note that although not required to be so all specifications can be rewritten so as they only use adom 4 as an instance guard 2 Polynomial Range Guards are relations of the form poly SIZE lt x lt poly2 SIZE with poly and poly two polynomials 3 PBINT Guards are relations of form x lt poly SIZE where poly SIZE is a polynomial depending only on the constant SIZE Instance guards and polynomial range guards define ranges of size at most polyno mial in the binary encoding size of str
6. not 1 guarded The guards of GF are used to restrict the range of quantifiers They also use upper guard axioms which restrict the elements in expansion relations to those occurring in the interpretation of guard atoms To formalize this they introduce the following restriction of FO denoted GGF Definition 3 The double guarded fragment GGF of FO for a given vocabulary is the set of formulas of the form w with C vocablo AW where is a formula of G Fp and w is a conjunction of upper guard axioms one for each symbol of occurring in w of the form YT E Z D Gi 1 A A Gn Em where m lt k and the union of free variables in the G is precisely T Guards of GF that restrict quantifier ranges are lower guards and guards of Def 3 are upper guards In GGF all upper and lower guards are from the instance vocabulary o so ranges of quantifiers and expansion predicates are explicitly limited to adom 4 To finish definition of the logic they define well formed terms which depends on the vocabulary of the background structure The authors of TM09 use arithmetical structures same as GG98 They also introduce a fragment of arithmetical structures known as small cost arithmetical structures They prove that GGF captures NP for small cost arithmetical structures This paper continues on their path and proves that the property of capturing NP over small cost arithmetical structures can be e
7. Built in Arithmetic in Knowledge Representation Languages Shahab Tasharrofi and Eugenia Ternovska Simon Fraser University Canada sta44 ter cs sfu ca Abstract In previous papers results about capturing the complexity class NP as model expansion task for languages with built in arithmetic have been demon strated The purpose of this paper is to show implications of those results to the practice of KR and in particular to two system languages of ASP Gringo and Lparse and the IDP system In addition we describe a logic which we call PBINT and show that PBINT provides a good basis for an attractive modelling language We demonstrate that PBINT allows for compact and natural encodings 1 Introduction Currently several different specification modelling languages are being developed in different communities They have their associated solvers and are intended as universal languages for search problems in some complexity classes usually NP e g schedul ing planning etc Examples include Answer Set Programming languages Gringo Lparse modelling languages from the CP community such as ESSENCE FGJ 05 or the input language of the IDP system WM09 These languages do not closely cor respond to first order FO logic they often contain inductive definitions and built in arithmetic Designers usually focus on the convenience of the language and rarely pay attention to the expressiveness For each language several tasks can b
8. SP program IT with predicate symbol p in their head Also let M r denote all multi set terms t of r and Vm m denote all variables that are quantified by multiset operation m and Bm v m denote all predicate symbols that appear as a positive atom in multi set operation m and with variable v as one of their arguments We say that an ASP program IT is restricted if there is a function A from predicate symbols of II to natural numbers such that for all predicate symbols S in vocabulary of IT max min A T T B v r v V r r Ra S lt A S and max min A T T Bm v m v Vn m m E M r r Ra S lt A S Note that although the motivation for Definition 7 comes from Gringo it is in fact different from both A restrictedness in GST07 and level restrictedness in GKK 08 To see why Definition 7 is different from A restrictedness defined in GSTO7 look at the following example which is not accepted by Definition 7 but is A restricted due to GST07 q 0 p x q 0 x x Also to see why Definition 7 is different from level restrictedness defined in GKK 08 observe that assignment operator is not present in Definition 7 In fact Definition 7 ac cepts a subclass of ASP programs that are characterized by level restrictedness property which is in turn generalized to safety property in newer versions of Gringo software The reason we use this limited class of ASP programs and not the more inclusive ve
9. Syr00 There is also ex isting works such as GOS09 and BBG05 on how these systems deal with solving issues in presence of arithmetic constraints However we are not aware of any in depth study of the expressiveness of such languages in the presence of arithmetic constraints In many cases allowing arithmetic constraints without careful restrictions provides the language with very high expressiveness as is shown for ESSENCE MT08 7 Conclusion In modelling languages you are frequently faced with the problem of having a frame work to support both natural specifications of problems and reasoning about those problems In this paper we took our measure of naturality to be being able to use built in arithmetic and our measure of reasoning to be being in NP We showed some ex amples of problems of practical importance and proved that several existing modelling languages cannot express these problems naturally using their built in arithmetic and not by encoding numbers using abstract domain elements We also presented a solution to this problem and claimed without giving the proof that our fragment of logic can represent all arithmetical problems in NP naturally We supported our claim by giving natural axiomatizations for problems in NP that could not be naturally axiomatized in existing modelling languages This result guarantees universality of our logic for this complexity class and also settles our reasoning abilities by showing t
10. Ue such that A K iff there exists an expansion B of A with B 9 We do not give any proof for Theorem 3 in this paper The proof can be found in TT 10 The importance of this theorem is in its ability to capture all NP with arithmetic As shown previously most of previous frameworks for arithmetic in KR suffer from the fact that they can only axiomatize certain arithmetical problems in NP For example we showed that ASP and IDP cannot axiomatize integer factorization using their built in arithmetic On the other hand Theorem 3 shows that PBINT can axiomatize exactly those problems involving arithmetic which are in NP Moreover the background structure of PBINT is much simpler than many back ground structures in practical KR languages In particular there is no built in aggregate in compact arithmetical structures Together with Theorem 3 it shows that PBINT can define aggregates in terms of more primary operations those given in compact arith metical structures Therefore adding aggregates to your language would not increase the expressibility of your language Thus PBINT gives you a very concrete basis to build your language upon It tells you that if your language somehow supports all PBINT constructs you can 1 be sure that your language captures all of NP and 2 unless your other constructs are very powerful outside NP N co NP you can safely add them to your language without worrying about its complexity implications
11. cation The model expansion task remains the same expand a now embedded o structure to satisfy GGF Logical Fragment The authors of TM09 use a guarded logic in an embedded setting which allows them to quantify over elements of the background structure un like e g GG98 To do so they use an adaptation of the guarded fragment GF of FO GLSO1 In formulas of GF a conjunction of up to k atoms acts as a guard for each quantified variable Definition 2 The k guarded fragment GF of FO with respect to o is the smallest set of formulas that I contains all atomic formulas 2 is closed under Boolean operations 3 contains Jz Gi A GmA provided the G are atomic formulas of o m lt k ob GFy and each free variable of appears in some Gi 4 contains Vi Gi Gm D provided the G are atomic formulas ofo m lt k ob GFy and each free variable of appears in some Gi For a formula 4 AZ Gi A GmA conjunction Gy A Gm is called the existential guard of the tuple of quantifiers 3z universal guard is defined similarly Example 1 Let be E E2 The following formula is not guarded VaVy E1 y D Eo x y It is guarded when is replaced by P which is not in The following for mula is the standard encoding of the temporal formula Until P P2 Sve R v1 v2 A Po v2 A Vvs R v1 v3 A R v3 v2 D Pi v3 The formula is 2 guarded i e is in GF but it is
12. e studied satis fiability and model checking are among them Here since we are interested in search problems we focus on the task of model expansion MX the logical task of expanding a given structure with new relations The user axiomatizes their problem in some logic L a specification modelling language The task of model expansion for abbreviated L MX is Model Expansion for logic Given 1 An formula with vocabulary o U and 2 A structure A for o Find an expansion of A to o Ue that satisfies Thus we expand the structure A with relations and functions to interpret obtain ing a model 6 of The complexity of this task obviously lies in between that of model checking the entire structure is given and satisfiability no part of a structure is given In the combined setting an instance consists of a structure together with a formula We A language and system based on an extension of first order logic with inductive definitions under well founded semantics focus here on the data complexity where the formula is fixed and the input consists of an instance structure only We call the vocabulary of A the instance vocabulary and vocab o the expansion vocabulary Remark 1 Since FO MX can specify exactly the problems that SSO can one might ask why we don t stick with the standard notion of SSO model checking Primarily it is because we rarely use pure FO and because for each la
13. ence and genericity in such frameworks Another line of database motivated work over infinite background structures is em bedded model theory See Lib04 Lib07 Work in this area generally reduces ques tions on embedded finite models to questions on normal finite models An important result in this area is the natural domain active domain collapse for ISO for embedded finite models as well as other deep expressiveness results The work also describes a notion of safety through e g range restriction to achieve safety with many back ground structures and connections between safety and decidability The active domain quantifiers are similar to our proposal of lower guards however our goal was to reflect what is used in practical languages namely the so called domain predicates of Answer Set Programming and type information from other languages We have done it through the use of upper and lower guards In general research in database theory is mostly focused around computability and the expressive power of query languages while our interest following Gra07 is in capturing complexity classes but in connection with specification modelling languages We plan however to investigate the applicability of domain independence range restrictedness and other notions from embedded model theory to practical modelling languages Gradel and Gurevich GG98 studied logics over infinite background structures in a more general computer science context T
14. f Jadom However in the case of the two problems above factorization and quadratic residues we know that the number of elements in the input structure is always constant one el ement in factorization and 3 elements in quadratic residue Therefore f adom is always a constant depending on f but not A Thus the set 1 2 3 f Jadomy does not depend on structure A So program P takes the active domain of A and re turns a set S which upper bounds the active domain of all valid expansions of A The rest of the proof can be carried out in the same way as the previous case Corollary 3 Using only built in arithmetic of ASP language of Gringo and Lparse with or without 5 1 Unless P NP the quadratic residue problem cannot be axiomatized naturally and 2 Axiomatizing integer factorization naturally is possible only if it is polytime com putable So we proved that the two problems of factorization and quadratic residue cannot be axiomatized in either ASP or IDP system languages However we disregarded one of the features of both languages we analyzed the compact domain representation i e the use of two numbers n and nz to compactly represent all numbers in the range between n and n In fact the compact domain representation can be used to naturally axiomatize both problems above However there are two drawbacks associated with using compact domain representations 1 First the compact domain representatio
15. hat all PBINT ax iomatizations can be efficiently in polytime grounded to any state of the art solver of NP problems Our work is a significant step forward from the previous proposal since it overcomes a number of limitations The language we proposed is natural because it is essentially FO logic where guards can be made invisible through hiding them in a type system Solving can be achieved through grounding to SAT a work which is being performed in our group but falls outside of the topic of this paper and this conference In summary our work has pointed out some of the limitations of existing modelling languages and provided a solution to these limitations Future directions include a analysis of other existing languages in connection with the logical fragments defined here b design of logics with different useful background structures and analysis of existing modelling languages with respect to these background structures c continue with our implementation development Acknowledgement This work is generously funded by NSERC MITACS and D Wave We also express our gratitude towards the anonymous referees for their useful comments References BBG05 BC92 Bus85 CH80 CK01 Fag74 FGJ 05 GG98 GK99 S Baselice P A Bonatti and M Gelfond Towards an integration of answer set and constraint solving In M Gabbrielli and G Gupta editors Proceedings of the Twenty first Internat
16. hese categories It is proved that under complexity assumptions these categories cannot express some problems naturally Another motivation in this paper is to design a logic where you could use arithmetic naturally and where you can even have some form of quantification over the infinite domain of integers We want to impose as few limitations as possible but some are of course needed In particular we need to limit the range of the quantifiers We also need to limit the number of elements appearing in the solutions This is done by predicates which we call guards By itself this restriction is obvious and does not appear to be a contribution especially given that most practical languages do exactly that What is new here is that the exact choice of the arithmetic operations and the kind of guards allowed matter a lot A solution was given in TT10 There we introduce a new set of arithmetical oper ations and show that by supporting these operations you can capture exactly NP over arithmetical structures i e 1 nothing outside NP is expressible and 2 for every prob lem in NP involving arithmetic and numbers there is specification that works with numbers as numbers instead of encoding them using abstract domain elements This paper introduces this logical fragment in Section 4 but does not give proofs of capturing NP Later on in Section 5 we give some examples including those that could not be axiomatized in other language
17. hey characterized NP for arithmetical structures under some small weight property generalized to the small cost condition in TMO09 see TM09 for a more detailed discussion While this condition corre sponds to existing languages as shown in Section 3 1 our work here gives an uncon ditional result for capturing NP in the presence of arithmetical structures and thus is a step forward in the development of such languages Instead of controlling access to the background structure through the use of weight terms GG98 we rely on guarded fragments which is much closer to practical specification languages The work we mentioned so far is the closest to our proposal and was the most inspi rational The research on descriptive complexity in the embedded setting also includes the work of Gradel and Meer GM96 as well as Gradel and Kreutzer GK99 Another line Cook Kolokolova and others CK01 establishes connections between bounded arithmetic and finite model theory in particular by relying on Gradel s characterization of PTIME Another direction on capturing complexity classes is bounded arithmetic including Bus85 Ske05 BC92 However the characterization of complexity classes there is in terms of provability in systems with a limited collection of non logical symbols and is not applicable here Built in arithmetic is implemented in many modelling languages e g the IDP sys tem WM09 the Gringo system GKK 08 and LPARSE
18. ional Conference on Logic Programming ICLP 05 volume 3668 of Lecture Notes in Computer Science pages 52 66 Springer Verlag 2005 S Bellantoni and S Cook A new recursion theoretic characterization of the polytime functions extended abstract In STOC 92 Proceedings of the twenty fourth annual ACM symposium on Theory of computing pages 283 293 1992 S R Buss Bounded arithmetic PhD thesis Princeton University 1985 A Chandra and D Harel Computable queries for relational databases Journal of Computer and System Sciences 21 156 178 1980 S Cook and A Kolokolova A second order system for polytime reasoning based on gradel s theorem In Proceedings of Sixteenth Annual IEEE Symposium on Logic in Computer Science LICS 01 pages 177 186 2001 R Fagin Generalized first order spectra and polynomial time recognizable sets Complexity of computation SIAM AMC proceedings 7 43 73 1974 A M Frisch M Grum C Jefferson B M Hernandez and I Miguel The essence of essence A constraint language for specifying combinatorial problems In Proc of the Fourth International Workshop on Modelling and Reformulating Constraint Satisfaction Problems pages 73 88 2005 E Gradel and Y Gurevich Metafinite model theory Inf Comput 140 1 26 81 1998 E Gradel and S Kreutzer Descriptive complexity theory for constraint databases In Proceedings of the Annual Conference of the European Association for Computer Scie
19. n potentially ex ponentiate the size of the domain But by level restrictedness property summations separate levels Thus at most l different exponentiations can occur Now if we take f as follows it gives an upper bound on the number of elements at level l on F l times Then we use the same monotone polytime program P as in Proposition 2 with the difference that it takes two arguments and neglects the second one This program runs in polytime because the size of its input is so large that all of its computation time is bounded by a polynomial in that large number Please note that the function f given above is a very rough upper bound and we believe that upper bounds of form f n 224 work too although with a more detailed proof For Lparse again we only use the fact that all Lparse programs are also Gringo programs GKKT 08 Non expressibility for domain restricted logical fragments We now prove that in teger factorization and quadratic residue problem can not be naturally axiomatized in the logical fragments we defined For active domain restricted logical fragments this is obvious We need new numbers except those in the domain Below we prove the same property for the two other domain restricted fragments i e polytime and loosely domain restricted logical fragments Theorem 2 If is a polytime or loosely domain restricted logical fragment then 1 L cannot express integer factorization using built in arithme
20. nce Logic CSL 99 Madrid volume 1683 of LNCS pages 67 81 Springer 1999 GKK t08 M Gebser R Kaminski B Kaufmann M Ostrowski T Schaub and GLSO1 GM96 GOS09 Gr 07 GST07 S Thiele A User s Guide to gringo clasp clingo and iclingo November 2008 http potassco sourceforge net G Gottlob N Leone and F Scarcello Robbers marshals and guards game theoretic and logical characterizations of hypertree width In PODS 0 2001 E Gr del and K Meer Descriptive complexity theory over the real numbers Math ematics of Numerical Analysis Real Number Algorithms 32 381 403 1996 M Gebser M Ostrowski and T Schaub Constraint answer set solving In P Hill and D Warren editors Proceedings of the Twenty fifth International Conference on Logic Programming ICLP 09 volume 5649 of Lecture Notes in Computer Science pages 235 249 Springer Verlag 2009 E Gr del Finite Model Theory and Descriptive Complexity pages 125 230 Springer 2007 M Gebser T Schaub and S Thiele Gringo A new grounder for answer set pro gramming In C Baral G Brewka and J Schlipf editors Proceedings of the Ninth Lib04 Lib07 MT05 MT08 Ske05 Suc98 Syr00 TM09 Top91 TT10 WM09 International Conference on Logic Programming and Nonmonotonic Reasoning LP NMR 07 volume 4483 of Lecture Notes in Artificial Intelligence pages 266 271 Springer Verlag 2007
21. ng for practical spec ification languages Fagin s theorem allows one to represent all problems in NP how ever there is no direct way to deal with numbers and operations on them since in logic we have abstract domain elements encoding of numbers may be needed A usable logic for these problems would use standard arithmetic as in all realistic modelling languages One of the main contributions of this paper is to formally investigate the expressive power of arithmetic in some of the practical modelling languages such as the ASP language of Gringo and Lparse systems and the system language of IDP system For example as Section 3 shows if your system uses only ordinary arithmetical operations such as x and ordinary arithmetical aggregates such as X I min and maz then you will not be able to axiomatize some common computational problems such as integer factorization naturally i e you would need to use e g binary encodings of numbers In these cases you might need to use binary encodings as opposite to using built in arithmetic These limitations apply regardless of whether fixpoint constructions are present in the language or not For example both ASP language of Gringo and Lparse and the system language of IDP system support fixpoints while still unable of naturally ax iomatizing integer factorization Section 3 proves this by introducing several categories of logics and showing that all the system languages above fall into t
22. nguage MX is just one among several tasks of interest The authors of MT05 emphasized the importance of capturing NP and other com plexity classes for such languages The capturing property is of fundamental importance as it shows that for a given language a we can express all of NP which gives the user an assurance of universality of the language for the given complexity class b no more than NP can be expressed thus solving can be achieved by means of constructing a universal poly time reduction called grounding to an NP complete problem such as SAT or CSP The authors proposed to take the capturing property as a fundamental guarding prin ciple in the development and study of declarative programming for search problems in this complexity class and started careful development of foundations of modelling languages of search problems based on extensions and fragments of FO logic While the current focus is on the complexity class NP by no means do we suggest that the expressive power of the languages for search problems should be limited to NP Our goal is to design languages for non specialist users who may have no knowledge of complexity classes The users will be given a simple syntax within which they are safe and would be encouraged to express their problems in that syntax The classic Fagin s theorem Fag74 relating 4SO and NP states that when the formula is fixed FO MX captures NP However FO is too limiti
23. ns would take one well beyond NP and would enable one to describe for example the NEXP complete problem of tiling Therefore any hope for polynomial time grounding would be lost 2 Second the compact domain representation is not really an option for any reason able size instance For example in the case of factorization the numbers one need to factor in practice need more than 200 digits to represent So using compact do main representation yields a domain of size 102 which cannot be stored in any reasonable size memory in fact it is more than the number of atoms in the observ able universe 4 Logic PBINT In this section we describe a logic that can unconditionally characterize NP problems involving arithmetic The first step towards this goal is to use a different background structure Definition 11 A Compact Arithmetical structure is a structure N having at least N 0 1 x lt with domain N the natural numbers where 0 1 x and lt have their usual meaning and x returns the size of binary encoding of number zx i e a 1 loga x 1 Other functions predicates and multi set operations min max etc may be included provided every function and relation of N is polytime computable Requirements on o As before we consider embedded MX but the embedding is into the compact arithmetical structure We make some assumptions about the instance vocabulary It contains predicate adom 4 and a
24. ntroduced for each sub formula and Lloyd Topor trans formation is used to relate these sub formulas together in an appropriate way However the resulting ASP program is not still restricted In order to convert this ASP program into a restricted ASP program we have to incorporate information from lower and upper guards in the GGF specification Such guards define a permissible domain for each sub formula Therefore we introduce new domain predicates based on this information These predicates can be defined using a completely positive and non recursive ASP program So all rules generated above can be modified so as their variables are bounded by these new domain predicates Note that here we do not claim that a first order formula can be translated into a A restricted ASP program via Lloyd Topor transformation What we claim and what is needed here for the proof is that informally for a specification in GGF there is a A restricted ASP program P such that for all instance structures D there is a certificate for D in the GGF e sense iff there is a certificate for D in the ASP sense The key here is that the transformation does not have to preserve the entire models of the GGF formula What is needed to be presereved is the existence of an expansion and not the equivalence of the set of expansions for a given instance structure Also the expansion vocabulary of the ASP program does not have to be the same as 3
25. number of inputs Thus we can obtain a finite representation encoding of instance and expansion structures Having functions in the instance vocabulary imposes a small inconvenience with the definition of the active domain In a formalism based on classical logic all terms are total and therefore defined on all integers Thus if we add functions the notion of an active domain becomes meaningless On the other hand the user might quite reasonably assume that the inputs and the outputs of the instance functions are from a finite domain which makes these functions to be non total A safe solution would be to advise the user to use graphs of functions i e the corresponding predicates instead of instance functions It would solve the problem with the definition of an active domain but this solution seems too limiting for a nice logic Instead we choose to allow instance functions but to require all instance functions to have upper guards and the default value for inputs outside of the intended range just as we have for expansion functions Active domain now contains all elements of the universe contained in all instance relations together with all elements in the ranges of the instance functions Capturing NP with PBINT MX Theorem 3 Let K be an isomorphism closed class of compact arithmetical embedded structures over vocabulary o Then the following are equivalent I KENP 2 there is a PBINT sentence of a vocabulary T o Uv
26. of factorization problem which are all polynomially equivalent i e using an oracle for one version solution to other versions can be found in polytime Quadratic Residue Problem is an NP complete problem that involves only a few num bers You are given three numbers n a and c and you are asked if there is a number x such that x gt c and x a mod n Various domain restricted logical fragments Now we define several logical frag ments by restricting their MX tasks We also show that some practical KR system languages such as ASP and IDP fall into these fragments Then by showing some non expressibility results for these logical fragments we effectively prove that system languages of ASP and IDP cannot express integer factorization and quadratic residue problems naturally Definition 8 Active domain restricted logical fragment Let be a logical frag ment so that for all specifications in L and for all arithmetical structures A over a instance vocabulary and all expansions of A such as B satisfying o we have that adomp adoma We call this logical fragment an active domain restricted logical fragment Definition 9 Polytime domain restricted logical fragment Let be a logical frag ment so that for any specification in L there is a monotone polytime computable mapping P 2N 2N with the following property For all arithmetical structures A over o instance vocabulary and for all structures B expanding A and sa
27. omain of the instance structure Proposition 2 The language of ASP without X accepted by Gringo and Lparse is a polytime domain restricted logical fragment Proof For Gringo we know that a correctly constructed ASP program should be level restricted So we use induction on the levels of an ASP program and show that for each level l there is a monotone polytime program P 2N 2N that given the active domain of the previous level generates the active domain of the new level So as any fixed ASP specification has only constantly many different levels we can combine all P s to obtain a new monotone polytime program P that satisfies the polytime domain restrictedness condition For Lparse we just use the fact that all Lparse programs are also Gringo programs GKK 08 The condition on not including in Proposition 2 is essential because adding it will enable us to describe predicates consisting of exponentially many values The following ASP program shows one such scenario V 2 fori 0 1 2 n 1 A X amp not A X V X A X not A X V X E X X S Y A Y V Y This program has domain size n but predicate has domain 0 to 2 1 Proposition 3 ASP language of Gringo and Lparse is a loosely domain restricted log ical fragment Proof For Gringo again we use the level restrictedness property Assume that your specification has l levels As discussed above each summation ca
28. practical language upper and lower guards are defined by types and need not be given explicitly Here the predicate Task is a type and functions start and end are functions from type Task to integer type So predicate Task can disappear from the above sentences Example 3 Integer Factorization You are given a number n and asked to find some nontrivial factor of n Here o only has constant n and e only constant p which is upper guarded as follows p lt SIZE which abbreviates Vm c m gt m lt SIZE in case of zero ary constant expansion functions Now the axiomatization is p gt LlAp lt nA dq lq lt SIZE A px q n Example 4 Quadratic Residues You are given numbers r n and c and asked to find a number x such that z r mod n and x lt c Here instance vocabulary consists of constants n r and c and expansion vocabulary only has constant x upper guarded by sentence a lt SIZE The axiomatization consists of two sentences 0 lt x x lt chx lt nand dq q lt SIZE Axx x qxn r 6 Related Work Research in databases over infinite structures can be traced back to the seminal paper by Chandra and Harel CH80 There are several follow up papers with developments in several directions including Top91 Suc98 GG98 and more recent Gr 07 Topor Top91 studies the relative expressive power of several query languages in the presence of arithmetical operations He also investigates domain independ
29. r sions is to define a subclass of ASP programs that remains inside NP in the presence of arithmetic constructs This way practical ASP solvers can define a switch to either limit users to this syntax and give them a performance guarantee in return because of remaining in NP or to give them full access to the ASP language which can describe problems outside NP but without such performance guarantees Now we can use the notion of restricted ASP programs and define admissible ASP programs over arithmetical structures to be the set of A restricted ASP programs over such background structures Theorem 1 Let K be a class of small cost embedded arithmetical structures over vo cabulary o Ue Uv Then the following are equivalent 1 K NP 2 There is a first order formula of GGF such that D K if and only if there is an expansion D of D to so that D 3 There is a restricted ASP program P with instance vocabulary o such that D K iff there is an expansion D of D so that D is a stable model for P Proof 1 2 is shown in TM09 2 3 is shown by Lloyd Topor transformation We first push all negations inside and then introduce new relation symbols for negated expansion predicates For example for expansion predicate F Z new relation symbol E Z is introduced and two following sentences are added to the ASP program E amp not E Z E Z not E Also new relation symbols are i
30. s and show that the new logic can axiomatize them nat urally using its built in arithmetical operators The fragment can be viewed as an ide alized specification language and hopefully inspire the development of practical KR languages 2 Background MX with Arithmetic Throughout the paper we use Jg to denote 4a J n and Vz to denote Var V2n Embedded MX Embedded finite model theory see Lib04 Lib07 the study of finite structures with domain drawn from some infinite structure was introduced to study databases containing numbers and numerical constraints Rather than a database being a finite structure we take it to be a set of finite relations over an infinite domain Definition 1 A structure A is embedded in an infinite background or secondary structure M U M if it is a structure A U R with a finite set R of finite relations and functions where M A R 0 The set of elements of U that occur in some relation of A is the active domain of A denoted adom 4 In database research embedded structures are used with logics for expressing queries Here we use them similarly with logics for MX specifications Throughout we use the following conventions denotes the vocabulary of the embedded structure A U R which is the instance structure v denotes the vocabulary of an infinite back ground structure M U M is an expansion vocabulary A formula over cUvUe constitutes an MX specifi
31. tic unless factorization is in polytime 2 L cannot express quadratic residue problem using its built in arithmetic unless P NP Proof for polytime domain restricted logical fragments Let be a polytime domain restricted logical fragment and be a specification in such a fragment Then by defini tion there is a monotone polytime program P that gives an upper bound on the active domain of all valid expansions of a given instance structure Now if axiomatizes integer factorization with its built in arithmetic at least one factor of number n should appear in the output of P So checking all numbers that P outputs gives us one such factor Also as P is polytime the whole checking procedure would also be polytime and we would solve integer factorization in polytime Similarly if axiomatizes quadratic residue problem using its built in arithmetic then x appears in the output produced by P So checking all outputs of P gives us such x if it exists Again P being polytime implies that the whole procedure is also polytime and P NP because quadratic residue problem is NP complete Proof for loosely domain restricted logical fragments Let be a loosely domain restricted logical fragment and be a specification in such a fragment Then by def inition there is a function f and monotone polytime program P such that the ac tive domain of all valid expansions of an input structure A are upper bounded by P adom 1 2 3
32. tisfying Q we have adomg C P adom We call such logical fragments a polytime domain restricted logical fragment Definition 10 Loosely domain restricted logical fragment Let be a logical frag ment so that for any specification in L there is a function f N N and a monotone polytime mapping P 28 x 2N 2N such that For all arithmetical structures A over a instance vocabulary and for all structures B expanding A and satisfying we have adomg C P adoma 1 2 3 f adom We call such logical fragments a loosely domain restricted logical fragment Remark 2 Every polytime domain restricted logical fragment is also a loosely domain restricted logical fragment with f being a constant function and P being the same as before except it takes two argument and neglects the second one However there is an important difference between these two fragments Namely when specification is fixed for polytime domain restricted logical fragments polytime grounding in the size of instance structure is ensured while for loosely domain restricted logical fragments such grounding cannot be guaranteed Proposition 1 The language of the IDP system is a domain restricted logical frag ment Proof All predicates and functions in IDP system language should have proper type names Also all types are given as part of the input Thus the active domain of all structures satisfying an specification in IDP is exactly the active d
33. ucture However PBINT guards can define ranges with exponentially many different integers For example condition z lt SIZE is equivalent to x lt DITA E T exponential in the value of SIZE Also note that guards definable by stratifiable inductive definitions with 1 2 as the base cases can be added without changing our results Definition 12 logic PBINT We define our logic as follows Background Structure the compact arithmetical structure Terms are constructed as usual over v Uo U Formulas a Upper Guards i Expansion relations are upper guarded by instance or polynomial range guards ii An expansion function f has an upper guard of form ViVy f Z y gt G z y V y default where G z y is a conjunction of guards jointly guarding variables x and y so that z is upper guarded by instance or polyno mial range guards and y is upper guarded by any of the three types of guards b Lower Guards i Existential guards any of the three types of guards ii Universal guards instance or polynomial range guards The constant default can be interpreted by any number at the user s choice The part y de fault in a ii above is needed because all functions in FO logic are total thus defined on all natural numbers Without that part the upper guard axioms on expansion functions would always be false making all specifications with such functions useless Functions have meaningful non default outputs on a finite
34. xtended to several practical KR languages gt We use the definition of arithmetical structures and small cost arithmetical structures in this paper So for presentation reasons these definitions are moved from background section to where they are used in Section 3 1 3 Capturing and Non Expressibility Results for Practical KR Languages This section studies the expressiveness of built in arithmetic in existing KR languages But in order to formally investigate the expressibility of KR languages we first need to define what we mean by a specific language We have based our investigations on system manuals published for these languages And as these manuals often neglect the details we have had to do several experiments in order to understand if particular specifications are allowed or not In the end we believe that our results are true of the specific languages that we will talk about As is the case with all practical languages they evolve over time and their syntax changes from one version to another So what is not allowed in current version may be allowed in the next version or vice versa Therefore we specify the exact manual and version of these languages as below 1 IDP version 1 4 4 and the accompanying manual published in August 2009 WM09 2 Gringo version 2 0 5 and the accompanying manual published in November 2008 GKK 08 3 Lparse version 1 1 2 and the accompanying Lparse 1 0 user s manual Syr00 3 1 Capturing
Download Pdf Manuals
Related Search