The expressive power of query languages based on logic programming
Mark L. Reynolds · Spiral (Imperial College London) · 1988
Datalog, or the Horn-Clause query language, is a successful form alisation o f the use o f pure logic programming to answer queries asked about finite relational structures.However, Datalog is not expressive enough fo r some practically useful problems as those logic programmers w ho feel the need to use the non-declarative feature negation as fa ilu re probably know .In this thesis we assess the increased expressive power got b y adding negation as fa ilu re to the pure logic programming query answering approach.To achieve our aim we first define a logical query language D E F w h ich is an extension of Datalog and has just as nice syntax and semantics as Datalog.W e show that D E F is equally as expressive as the most common fixed point query language w hich contains a lo t o f useful queries.We then show that D E F expresses exactly those queries w hich can be implemented using logic programming w ith negation as failure.I w ould lik e to express m y gratitude to m y supervisor, Professor D ov Gabbay, fo r his help and encouragement throughout m y PhD w ork.I w ould also lik e to thank D r Bob S u lliv a n and D r W ilfr id Hodges w ho gave me good advice w hen I was tryin g to decide on a satisfactory subject area in w h ich to do research.A l l the graduate students w ho contributed to making the office and department conducive to good research deserve praise.Pablo de la Quintana deserves special mention fo r his h e lp fu l comments on the thesis.C h i Cheong Tam and D avid F u lle r were very h e lp fu l w hen it came to the practicalities o f presenting the thesis in a readable form .I am v e ry grateful to the Association o f Commonwealth Universities fo r supporting m y research.M any thanks are due to the Dickens fa m ily fo r making m y life easy in a foreign country.O f course I w ould not have been able to start researching fo r a thesis i f it was not fo r the great help m y parents and fa m ily gave me in previous years.They also earn m y gratitude fo r the m oral support they gave me w h ile I have been studying.F in a lly , I w ould lik e to thank Sarah fo r giving me such reliable support and encouragement so that I was able to persevere through the researching and w ritin g up.restricted to Horn-clause theories we can neither completely describe the structure nor define (in the usual sense o f im p licit definition) the query.Thus, in practice, we get a lot o f "don't know " answers.A different method using much the same set up was pioneered in [ChH85].Instead of tryin g to define the query inside the theory, w e use the theory plus p ro v a b ility to specify a query.To define the conjunction o f R and S as above, we add the sentence Vr ( RCr) a S(r) -► fiGr) ) to a complete description o f the {R,S}-structure.The answer to the query is the relation o f tuples w h ich are provab ly in Q Le. those tuples w hich are in the interpretation o f Q in any expansion o f the queried structure to a model o f the sentence.T h is approach, w hen lim ited to relational Horn-Clause theories, is form alised in a language, sometimes called D A T A L O G , w hich contains queries such as transitive closure w h ich are not in FO.New Work O ur new w o rk starts w ith a definition of a pow erful generalisation o f D A T A L O G .P R O V contains a ll the queries w hich can be defined via p rovab ility from any relational theory.A P R O V query is an ordered pair, w ritten PROV(P;P), o f a finite theory P w ith relation symbols of tw o types -the old ones from the language of the queried structures plus some new different ones -and one o f the new symbols P. The answer to PROV(P;P), asked o f any finite structure of the old language, is the relation o f tuples w hich are in the interpretation of P in any expansion of the structure to a model of P .The expressive power o f P R O V is equivalent to that of the language USO of u n iversa lly quantified second order form ulae -a language containing queries w hich are almost certainly too hard to answer in a reasonable amount of time (see [Fag74D.P R O V is the query language of w hich a ll the other of our new languages are sub-languages.The least powerful sub-language of PROV which we consider is DATALOG itself.It -3) we could a llo w universal quantification to appear in the bodies o f clauses -producing non-existential theories.B y allow ing different combinations o f these features we get several query languages of differing expressive power and ease o f implementation.The strongest language, IMP, w h ich is based on sentences allow ing a ny o f the extensions, is shown to be as pow erful as P R O V itself.B y a result in [Fag74], it can thus express a ll the negations o f non-determ inistically polynom ial time computable queries.Polynom ial time computable queries are thus w e ll w ith in its power -fo r example , "is the size of the structure an odd number?" can be answered b y try in g to prove that Odd fo llo w s from a complete description o f the structure plus the fo llo w in g theory in w hich R, S and Odd are new symbols: { Vcy ( R(x,y) -> £(y,x) ) , V e ( R ixjc) -Odd ) , \Jxyz ( R(x,y) A Rixj) A y -* Odd, V cy R (x ,y) V Six,y\ Vc ( V/ Six,y) -» Odd ) }. -9 -DEF and FO+LFP O ur most im portant generalisation o f D A T A L O G is the query language D E F based on sentences w h ich can contain old negations, inequalities and universal quantifications as conjuncts in the body but one and o n ly one atomic form ula appears as the head and it is b u ilt from a new relation symbol.For example, i f your brother is liked by everyone then you are a correct answer to the D E F query PRO V(P;Q ) where P is as follow s; { \/x y z [ p a re n tC zjc ) A p a r e n t(z ,y ) A x ^y A m aleiy') A ( W U k e s(u ,y } ) -QCx)] }.In order to compare D E F w ith established query languages such as the least fixed point language FO + LFP defined in [G ur85l we note the least fixed point character of logic-programming type deductions.Basing our ideas on the use o f a fixed point operator in [Em K 7 6 l we invent a new least fixed point language L F P .It is characterised b y the use o f one m ultiple operator defined by several first-order formulae.W e show D E F = L F P , i.e. that D E F and L F P are equivalent in expressive power.B y showing that F O + L F P = £ F F , we can conclude that D E F = FO+LFP.To show the form er we use a result in [Imm82] im plyin g that the nesting o f fixed point operators and first-order constructions w ith in each other can actu ally be collapsed.We must also show that the m ultip le character of L F P can be mimicked by m ultiple uses o f sim ple LF P operators.Th is is not a triv ia l matter o f coding the tuples of relations involved in a L F P operation into one big relation.Nevertheless, we can conclude that D E F , FO+ LFP and L F P are a ll equally expressible.DEF and N A F The major results in this thesis are those demonstrating the close relationship between the class of queries implementable by logic programming w ith negation as failure CLPNAF) and the class o f queries expressible in D E F .B y a query implementable w ith -10-L P N A F , w e mean one that can be answered by extending the usual logic programming technique fo r answering D A T A L O G queries to the L P N A F technology -i.e.we have an L P N A F program PROG and a sym bol P such that finding out whether dr is a correct answer to a query or not can be accomplished b y asking " PGr)?" of the two-part program consisting o f a description o f D follow ed by PROG.The first problem is to get a workable definition o f N A F .On the basis o f comments in [She84l we reject a ny ideas that the closed w orld assumption or the C la rk completed database provide any account of a declarative meaning of an L P N A F program.Instead, we must base our w o rk on a definition of a query evaluation process fo r N A F .W e choose a s lig h tly more complete process (i.e. it gets more answers) than C la rk 's [Cla78] and so have to relate it back to d a r k 's.It w ould be easier i f we could use some sort o f declarative meaning o f N A F and, in fact, we do so.We show how to construct from each functionless L P N A F program, PROG, a first-order theory, SYNTH(PROG), such t h a t : 1) i f PGr) succeeds from PROG then PGr) is deducible from SYNTH(PROG); and 2) i f PGr) fin ite ly fa ils from PROG then PGr) is not deducible from SYNTH(PROG).Furthermore, we detail some conditions, and say that a program w hich satisfies them is covered.If PROG is covered then 3) i f PGr) is deducible from SYNTH(PROG) then PGr) succeeds from PROG.B y using the results 1 and 2, we get a correctness result -fo r each functionless and constantless L P N A F program, there is a D E F query such that the answers w hich are obtained using the program are correct answers to the D E F query.Thus, a ll queries implemented by L P N A F are in D E F. B y using result 3, we can get a completeness result -fo r any D E F query, there is an L P N A F program w hich can be used to answer the query.The program w ill get a ll the expressive as the first-order query language.However, there are languages much more pow erful than FO and fo r this reason, Codd's definition o f completeness is not to ta lly satisfactory.T w o related, ve ry pow erful languages are the universal and existential second-order languages, USO and ESO respectively.The w ff of U SO (L) are those of the form VS^CxO where S is a signature disjoint from L and a first-order form ula from L U S .The w ff V S $ G r), w ith x = tx lt . . .,x n\ represents the n-ary L-q u ery q, where, fo r a ll L-structures D , fo r a ll a € D n, a € q ( D ) Z)h V S # » V LU S-structures E such that E \L= D , _ET=<£(<r).ESO (L), on the other hand, has form ulas 3S#6r) such that D \= 3S$Gr) i f and o n ly i f there is an L U S -stru ctu re E such that E \L= D and i?l=<£(