Constructive Second-Order Proofs in Logical Databases

1. Introduction

A logical databa·e is a finite structure U, defined by successive expansions of a database DB with new inductively defined relations, functions and functionals. In this paper, we concentrate on expansions obtained with inductive relational queries only, but the notion of constructible second-order proofs can be generalized to logical databases built with functions and functional&.

With a boolean inductive query Q on a class K of finite structures U we associate a uniform proof i.e. a function which to each structure U of a class K defines a proof of Q or ~Q in U (depending if the interpretation of Q. in U, IQ]u, is true or false) . Uniform proofs are constructible objects in the following sense: let Q be an inductive query on the class K , and let K 1 ={U 1 = (U,IQ]U : U E K} . Then to an i11ductive query Q 1 on the class K 1 there corresponds a uniform proof, built from the uniform proof of Q on K .

Inductive queries exactly capture the notion of polynomial time computability (as a function of the size of the data) 19], and these uniform proofs hence capture the notion of effectiveness (computability in polynomial time) . These proofs use computations on sets and the finiteness of the structures in a fundamental way . They are second-order proofs, but only capture the construr.tible put of second order logic on finite structures. We show the non-monotonicity of the corresponding calculus, and indicate that some of its intensional properties are also

constructive.

ln the second section, we review the definition of an inductive query, and the differences between logic programming and inductive definability. We give some examples and then describe compilation techniques. In the third section we introduce the notion of a uniform proof, and in the fourth section we study properties of uniform proofs, namely non-monotonicity and intensionality.

2. Inductive definability.

2.1 Notations: We assume that data is given as sets of tuples defining relational sets !l,1' .. ,gk. !l:;(a 1 , .. ,ai) iff <al' ... ,ai > is a tuple of arity j in the set !l:i' where a1' .. . ,ai E D, for a finite set D. A databa1e is a relational structure DB= <D, !!:l'···!l:k> and a databa·e uhema is the class K of all finite relational structures DB of similar signature. A logical databau (or knowledge-ba1e) is a logical e~pansion of a database, i.e. a structure U =<D, !l,l' .. ,.!!,k, R1' .. ,RP f1' .. . ,fm, 0,1> , where Rl' ... ,R 1 are relations on D, f1' ... ,fm are functions on D, and 0 and 1 'are two distinguished elements of D; in the complexity arguments, n=IDI; a knowledge uhtma is a class K of all finite structures U of similar signature. For a knowledge-base U, !l, 1 , ... ,!l,k are ba1e relation·, whereas !l,l' .. ,~, Rl' .. ,R 1 are ezplicit relation·. For a class K, let L 1 (K) be classical first-order language with equality, and L 2 (K) be the second-order language. Let S 1 , .. . ,Sm be new relational symbols in

the language L 2 (K) .

Definition:ISJ an 'inductive ·lllltm S with parameter~ is a sequence of first-order formulas IF l' ... ,F k] in the language L 1 (K) u {S1' ... Sm}, where each Si occurs positively and where the arity of Si is equal to the number of free variables in Fr

We write a system as:

The parameter variables are kept constant in a system. H for i= 1, .. . m d; ~ d, we say the system is of dimen1ion d. H each F; is in disjunctive normal form, i.e. F;<=>Fn V ·.· Fiq' each Fii is the j-th component of Fi" The fixed-point semantic associate for each structure U, the simultaneous fixed-point IS 1 Ju, ... ,1Sm]u, and we define the notion of an inductive query .

Definition: /I, 2] A query Q(xl".xq) is inductive on a clau K if there exists a system with parameters such that for all U: /Q(xl ... xq)Ju <=> /SI(xl" .. xd ;xd +l''''' x )Ju. I I q

!1.!1. Inductive definability and logic programming.

In classical logic programming data and logical definitions are treated as first-order axioms and a query is solved by attempting to find some first-order proof of Q in the theory defined by the axioms. If the data changes, the theory changes and so will the proof of Q.

In the inductive definability framework, we set a fundamentally different formalism as we distinguish between data and logical definitions. The data determines the finite relational structure U of a class K. and the logical definitions are taken u inductive definitions relaiive to K. To a class K we associate a c/au of tile or,, namely the set of true fll'lt-order formulas of U (Th(U) ), for each U. If the data changes, the structure changes within the same class K, but the the class of theory does not change.

We only · solve inductive queries on the class K. Given an inductive query Q and a structure U, we solve the query Q and produce a proof of Q or ~Q in U . To the query Q corresponds a uniform proof, i.e. a function which for each structure U associates a proof of Q or ~Q in U. Although we will obtain different proofs for each structure U (database state), they will all correspond to the same uniform proof.

Let us illustrate this fundamental difference with a simple classical example. A more detailed analysis is made in /7] . We adopt the Prolog notations: in the inductive framework, · ·" replaces the symbol " :-" .

Example:Consider two classes of acyclic directed graphs:

The class of graphs G 1 ( n),

Each finite graph is defined as a structure G 1 (n)=<{0,1, ... ,2n}, ~>, i=l or i=2, where ~(a,b) <=> there is an edge from a to b. The transitive closure of a graph is a binary relation tc, such that tc(a,b)<=> there is path from a to b. This new relation tc can be defined u a logic program and as an inductive definition:

o Inductive definition:

The inductive definition defines te(X,Y) on the class of finite graphs (in particular on the classes G 1 (n} and G 2 (n}} , where Y is a parameter. In the logic program, tc is defined by 2 rules, and the inductive definition of te has t component·. Let us analyse the query tc(0,1} in both formalisms .

The inductive definition of tc will be compiled into code independent of the data (C-code, then machine code} , using call-by-value for the parameter variables, 'and a call-by-sets for the recursion variables (see next section). In the case of tc(O,l}, the computation leads to computing {a// tc 1 (a; 1}/u, ... ,{a//te 1 (a;l}]u}, ... , i.e. unary sets until the closure ordinal A (less then 2n) is reached. Then we check if 0 E { a//tcA(a;l )Ju.

The query tc(0,1) evaluates to false on G 1 (n) and to true on G 2 (n) . Let us compare the proofs generated by these two approaches.

Logic programa: On G 1 (n) , tc(O,l} evaluates to no, using negation by failure /3], in time 0(2"), as all the paths from 0 are considered. On G 2 (n), tc(O,l) evaluates to ""'· but the complexity analysis depends on the position of the new atomic clause "~(0, 1) . " . If this new clause is inserted before the clause "~(0,2).", the complexity is constant (one step). If it is inserted after the clause "!(0,2} .", the complexity will be 0(2"} . The worst-case analysis is therefore 0(2"). If we add data (for example "!!(0,1)"), the theory changes, and the proofs change. Each proof of tc(0,1) is specific to a given finite graph .

Inductive defina bllity: For all constants o and /3, the uniform proof of tc(o,/3), is a construc.tible second-order proof that paraphrases the compilation of the inductive definition. It could be represented as: Tile inductive 10t A={a : fte(a,/3)/U} lla1 been computed. If- o EA then ""'' otherwi1e no. We obtain the same uniform proof independently of the graphs. As we compute a unary set, the relativized complexity is O(n) . It can be pre-computed at compile-time, and is the basis of the intensional analysis.

On the graphs G 1 (n), te(O,l) evaluates to no, using the implicit negation b11 inductive clo1ure 2 . We use the symbol o to represent this negation . On the graphs G 2 (n} , te(0,1} evaluates to II"'· The following labeled trees represent these proofs: In C 1 : .· c,

We ohow that the constructive calrulus associated with the inductive definability framework is non-monotonic . The notion of stratification /10] in logic programming is a step towards inductive definability, and towards a distinction between the structure (the data) and the logical definitions.

2 Tht ltl A={a : jtc(a,I)IGI(n)) baa bttn computed. Of!A lhtrtfor· no.

2.3. The rompllatlon of inductive queries.

Let K be & dus of logic&( d&t&bues. Euh explicit rel&tion R i· compiled into two C-functions. For simplicity, let us suppose R bin&ry, &nd usume th&t & type-definition set hu been defined th&t includes the d&t&-structures for bue rel&tions (GRIDS) .

The C-function Rb usumes th&t x and y &re known strings a and b representing elements of the dom&in, &nd returns 1 if JR(a,b)JU &nd 0 if J~R(a,b) Ju, whereu the function Rr usumes th&t &t leut one of the v&ri&bles is unknown or free (v&lue nil), &nd returns & pointer to & set .

2.3.1. Compilation rule: [6]

Let JS 1 , ... ,SkJ be a system defining R.

• For dimension 0 inductions, gener&te S 1 b &nd Sir for i= 1, ... ,k, following the cues: Selection, Projection, Join, Intersection, Union, Exp&nsion.
• For inductions of positive dimension d, compile Sir &nd Sir &S before. Pus the p&r&meter by v&lue, &nd compute the inductive sets {&/ jS 1 1 (&;b)Ju}, ... ,{&/jSk 1 (a;b)JU} until the closure ordin&l is re&ched. Project on the recursive v&ri&bles if known.

This comput&tion rule defines Rb &nd Rr, &nd works for existenti&l induction (Horn-Cl&uses), &nd Univernl inductions. In this lut cue, we compute & set &nd check th&t its cudin&lity is equ&l to the cudin&lity of the finite dom&in. We &lao compile ~R by gener&ting -,Rb(x) and set ·~Rr(x) (using the complement oper&tor on the finite dom&in q. 3

2.3.2. Witnesses.

Suppose. R is defined on & dus of structures where S &nd T &re explicit by the component: "R(x,y) . : S(x,z) , T(z,y) ." The vui&ble z is qu&ntified existenti&lly. In order to prove JR(&,b)JU we h&ve to exhibit &n element c in D such th&t JS(&,c)JU &nd JT(c,b) Ju . The comput&tion of Rb will c&ll for & selection &nd then a JOm-oper&tion. We will compute JS(&,z)ju, &nd check for e&ch element d of th&t set if JT(d,b)Ju. The first d th&t we find with this property is the witneu of JR(&,b)Ju.

In an induction of positive dimension, & new element in the inductive set S &t stage i, uses a witness &t st&ge i-1. These witnesses c&n be stored together with the inductive sets, &t no extr& cost .

3 Tbis construction is inefficient as soon as the arity of R is 2, but the intensional analysis will aUowa us to know in advance that it ia inefficient. .

3. Uniform proofs

Let Q be &n inductive query of &rity j on & clus K where &II strings &re const&nt symbols. We usoci&te to the boole&n query Q(& 1 , ... ,&l) on U & l&beled proof-tree, with Q(& 1 , ... ,&l) u !&bel of the root if JQ(& 1 , ... ,&l) JU &nd with ~Q(a 1 , ... ,&j) as l&bel of the root if J~Q(& 1 , ... ,al) Ju . The uniform proof or conltructible 1econd-order proof is the function th&t usoci&tes a l&beled proof­ tree with e&ch structure U .

Definition: A labeled tree in U is & finite tree where leaves &re l&beled with !!:(b 1 , .. . ,b 1 ), 'v'xT(x,b 1 , ... ,b 1 ) or o &nd where nodes &re l&beled with <R(b 1 , .. . ,b 1 ), i>, where R(b 1 , ... ,b 1 ) is in L 1 (U) &nd i is &n integer, such th&t:

• E&ch le&f is labeled with R(e 1 , ... ,ej) for an explicit R, with 'v'xT(x,b 1 , ... ,b 1 ) for &n explicit set-relation T or with o.
• If & node is l&beled <R(b 1 , b 2 ), i>, &nd its children &re l&beled <R 1 (b 1 ,c)), i 1 >, <R 2 (c,b 2 ), i 2 >, then the i-th component of the inductive definition of R is of the form "R(x,y) : R 1 (x,z) ,R 2 (z,y)" . 4
• If a node is l&beled with <R(b 1 , .. . ,b 1 ), i> &nd its child with 'v'xT(x,b 1 , ... ,b 1 ) , then the i-th component of the inductive definition of R is " R(y) : 'v'x T(x,y)" .

Definition: An effective proof of Q(o 1 , .. . ,o;J in U is & l&beled tree in U whose root is l&beled with Q(a 1 , .. . ,aj) and &n effective proof of ~Q(a 1 , .. . ,o;J in U is & l&beled tree in U whose root is l&beled with ~Q(& 1 , ... ,&l) .

We write UJ-.Q &nd U J-.~Q to denote effective proofs of Q &nd ~Q in U .

Definition: A uniform proof of & query Q on a clus K is & function, comput&ble in polynomi&l time, th&t usoci&tes &n effective proof of Q or ~Q in U, with e&ch structure U of K,

Theorem 1: If Q is &n inductive query on & class K, then for all U in K, U I= Q iff Ul-. Q, &nd U I= ~Q iff Ul-. ~Q.

Theorem 2: A query Q is comput&ble in polynomi&l time iff there is & uniform proof of Q.

~ Theorem 3: If & clus K 1 1s &n inductive expansion of & class K, &nd if there is & uniform proof of Q on K 1 , then there is & uniform proof of Q on K .

Theorem 1 is implicit with our definition of 1-·. Theorem 2 comes from the equiv&lence between inductiveness &nd being uniformly prov&ble. Theorem 3 is the recursion theorem rephrued in this context.

·similar cases handle the components with explicit negation, and allow nod eo lo be ma.rked negatively ( < ~R(b 1 ,b 2 ),i> ).

4. Properties of uniform proofs.

We show that the calculus associated with inductive definitions is non·monotonie: the addition of data or logical definitions changes the provability of a query .

.£.0.1. Change or data or transaction.

Consider the class of directed graphs augmented with tc , i.e. G=< D, ~. tc, 0> and the following inductive definition: "P <=> 'Vx(x=O v tc(x,O))."

To P corresponds a uniform proof of P. Let G 2 (n) be a graph , as in section 2. G 2 (n) I= P and therefore G 2 (n) I· .P. Suppose we add a new edge <2n+1, 2n+2> to the graph G 2 (n) (making a transaction on the data) , and define G 3 (n) as the new disconnected graph. G 3 (n) I= ~P and therefore G 3 (n) 1-. ~P.

.£.0.2. Change or a logical definition.

The non-monotonicity is simply based on the constructive negation, as the following example (adapted fom 14]) shows.

• Consider the relational schema Parent(NAME,NAME) and Origin(NAME, ADDRESS), i.e. <Joe, Adam> is a tuple of Parent. meaning that Adam is the parent of Joe, and <Joe, Antarctic> is a tuple of Origin meaning that Joe lives in the Antarctic. Let DB=<Bird, D 2 , Parent, Origin, C > be the finite structure with domain Bird and D 2 , base relations Parent and Origin given by the following tables, and an infinite set of constants C . (Bird is the set of individuals {Tweety, Bill, Joe, Adam} and D 2 is the set of individuals addresses {Marineland, Antarctic , Adelie} ).

Let K be the class of structures DB, and let us defme Anc on K (as tc in section 2) .

Anc(x,y) : Parent(x,y)

; Parent(x,z), Anc(z,y).

Let K 1 be the class of structures U 1 = <Bird, D 2 , Parent, Origin , Anc,C> , and let define Penguin on K 1 .

Penguin(x) : Anc(x,y), Origin(y," Antarctic") .

Let K 2 be the class of structures U 2 = <Bird, D 2 , Parent, Origin, Anc, Penguin, C> and let define fly:

If we find out that Penguins can also ongmate from Adelie, we modify the definition of Penguin(x) with:

Penguin(x) : Anc(x,y), Origin(y, "Antarctic")

; Anc(x,y), Origin(y, "Adelie")

In 181, we sbow~d bow to define constructively two intensional functions time.Q and space.Q, defining the worst-case time an.d space complexities of an inductive query Q, as a function of the size of the data. The average complexities can be approximated with similar methods, using statistical information associated with base relations . The uniform proofs that we introduced share these intensional properties, as an effective proof is built by solving the query. In practice given a query Q, one computes time.Q (negligeable complexity), anf if the result is greater than say 20 seconds, a process is forked, and a new query can be taken. Once the background process terminates, the constructive proof is passed to the parent process through a pipe.