In previous works a coordination-free strategy to compute Datalog with negation queries over databases distributed over many computational nodes has been studied, providing a syntactic characterization and proving the undecidability of the problem of deciding whether a query distributes. In view of a recast for FO queries, we report about a work in progress, namely the study of FO queries strongly distributing over components. We prove that the decision problem of establishing whether a FO query strongly distributes over components is undecidable and highlight how some syntactic bonds typical of Datalog with negation, namely safeness, play a crucial role in specifying strongly distributive FO queries.
In [
The aforementioned problem arises in the context of looking for a parallelized
coordination-free query computation strategy over databases distributed across
many computational nodes [
By Datalog: we refer to a variant of standard Datalog: [
H
B ?
B In both program and goal, neither constants nor equality are allowed. We say that a speci cation (P; g) is connected if, for each body B in (P; g), the graph (V; E) is connected, where V is the set of variables occurring in B and fx; yg 2 E i x and y occurs in the same asserted literal. For example the rule: is not connected, but the following one is it:
E0(x; w)
E(x; y) ^ E(z; w) E0(x; w)
E(x; y) ^ E(y; w)
Two results have been established, namely that: 1. A Datalog: query distributes over components i it is speci able by a connected speci cation; 2. The problem of deciding whether, given a Datalog: query q, q distributes over components is undecidable.
These results are proved exploiting recursive speci cations. With a view to recasting these results in absence of recursion, in this paper we report on a work in progress, namely the study of rst order (FO) queries distributing over components.1 Moreover, in this preliminary discussion, we abstract databases with purely relational structures of arbitrary cardinality and consider a stronger version of distribution over components, named strong distribution over components, i.e. those queries such that, for any structure S: q(S) = [ q(S0) =
S0 S
[
C2cc(S)
q(C)
The questions we want to answer are:
1 We consider FO queries because, except for some details, they have the same
expressive power as Datalog: without recursion (see Codd's theorems [
Let L be a relational vocabulary, i.e. a nite non empty set of relation symbols R=n, with positive arity n > 0, and constant symbols c.2 A structure S over L is a not empty set Dom(S), called the domain of S, enriched by interpretations RS Dom(S)n, for each relation symbol R=n 2 L, and cS 2 Dom(S), for each constant symbol c 2 L.
We say that a structure S0 is a substructure of S (S is a superstructure of S0), S0 S, i : 1. Dom(S0)
Dom(S);
, RS0 = RS \ Dom(S0)n; 32.. ffoorr eeaacchh rceolnasttioanntssyymmbboollRc=2n L2, LcS0 = cS.3 Given a subset A Dom(S) such that, for each constant symbol c 2 L, cS 2 A , A generates a substructure A of S, the only one such that Dom(A) = A .
The underlying graph of a structure S over L is the graph (V; E), where V = Dom(S) and fa; bg 2 E i there is a relation symbol R=n 2 L and a n-tuple such that a; b 2 2 RS. A connected component of S is a substructure generated by a connected component of its underlying graph. The set of connected components of S is denoted cc (S). If S admits only one connected component, then we say that S is connected.
Directed graphs are simple examples of relational structures. For instance the graph with vertex set V = fv1; v2; v3g and edge set E = f(v1; v2); (v3; v3)g can be considered as a structure S over the purely relational language L = fF=2g, where Dom(S) = V and F S = E. A substructure of S could be S0 with Dom(S0) = fv1; v3g and F S0 = f(v3; v3)g, while the connected components of S are the structures (fv1; v2g; f(v1; v2)g) and (fv3; v3g; f(v3; v3)g). 2.2
A FO formula ' (x1; : : : ; xn) over a vocabulary L is preserved under superstructures i , for any two structures S0 S over L:
8a1; : : : ; an 2 Dom(S0) S0 j= ' (a1; : : : ; an) ) S j= ' (a1; : : : ; an) 2 Note that no function symbols are allowed. 3 Therefore, cS 2 Dom(S0) holds. whereas, ' is preserved under substructures i the vice versa is valid, i.e.: 8a1; : : : ; an 2 Dom(S0)
S j= ' (a1; : : : ; an) ) S0 j= ' (a1; : : : ; an)
The following theorems [
1. A formula ' is preserved under superstructures i it is equivalent to a formula in 1, the set of prenex existential formulas. 2. A formula ' is preserved under substructures i it is equivalent to a formula in 1, the set of prenex universal formulas.
For example, 9x x = x is a valid 1 sentence.4 Since it is valid, it is preserved under substructures and, by preservation theorem, it must be equivalent to a (valid) 1 sentence, like 8x x = x. Finally, note that a quanti er-free formula is both 1 and 1. 2.3
Let L be a purely relational vocabulary, i.e. a relational vocabulary also without constant symbols. A FO speci cation over L is a couple ('; ), where ' is a FO formula over L and is a sequence of all elements in Var('),5 the set of free variables in '. A FO speci cation (' (x1; : : : ; xn) ; ) over L specify the FO query q('; ) such that, for any structure S over L:
q(S) = f(h(x))x2 jS j= ' (h(x1); : : : ; h(xn))g
S: 2. q is local i , for any structure S and a 2 q(S): q(S0)
q(S) 9C 2 cc (S) a 2 q(C) It is straightforward to prove that a FO query strongly distributes (as de ned in sec. 1) i it is both monotonic and local. Hence, we will split the study of strongly distributive queries in the study of monotonicity and locality. Lastly, it will be useful the notion of closure by constants: De nition 1. Given a FO formula ' (x1; : : : ; xn) over a vocabulary L, let L0 be the extension of L with n new constant symbols c1; : : : ; cn. The closure by constants 'c of ' is the sentence over L0 obtained replacing in ' each free variables xi with the constant ci, for any i 2 f1; : : : ; ng. 4 It is valid because the domain of a structure cannot be empty. 5 Eventually with repetitions.
We now characterize monotonic FO queries as those queries speci able by a formula. 1 Proposition 1. Let ' (x1; : : : ; xn) be a FO formula over a purely relational vocabulary L. A FO query q('; ) is monotonic i ' is preserved under superstructures.
Proof. ): Let S0 S and a1; : : : ; an 2 Dom(S0) such that S0 j= ' (a1; : : : ; an). Hence, there is at least a valuation h such that h(xi) = ai for any i 2 f1; : : : ; ng, (h(x))x2 2 q(S0) and, by hypothesis, (h(x))x2 2 q(S). So S j= ' (a1; : : : ; an). (: Similar to previous.
Applying the preservation theorem 1, we obtain the following theorem. Theorem 2. A FO query q('; ) is monotonic i formula (sentence). ' ('c) is equivalent to a 1 Therefore, to check whether a FO formula q('; ) is monotonic amounts to check if the closure by constants 'c is equivalent to a 1 sentence. We now prove that this last check is not algorithmically possible.
De nition 2. Let F1; F2 be two fragments of FO sentences over a vocabulary L. With Eq(F1; F2) we denote the decision problem of establishing whether, given a sentence '1 2 F1, 9'2 2 F2 '1 $ '2 Lemma 1. Let F1; F2 be two fragments of FO over a vocabulary L such that: 1. SAT (F1), the decision problem of satis ability of a sentence in F1, is undecidable; 2. SAT (F2) is decidable; 3. F1 contains all contradictory sentences.
Then, Eq(F1; F2) is undecidable.
Proof. If Eq(F1; F2) were decidable through an algorithm A, then, given a sentence ' 2 F1 as input to A, { If the output is negative, then ' is not contradictory, namely satis able; { If the output is positive, then there is at least one '0 2 F2 such that ' $ '0 is valid and, by completeness of FO, also derivable. Since the set of derivable sentences is recursively enumerable, it is possible to algorithmically build up at least one such '0. Recalling that SAT (F2) is decidable, it is possible to decide if '0, so ', is satis able.
In both cases it would be possible to decide whether ' is satis able and SAT (F1) would be decidable, which contradicts the hypothesis 1.
Theorem 3. Let L be a relational vocabulary su ciently expressive, i.e. with at least one relational symbol R=n with n 2. Let also 1 and 1 be, respectively, the set of existential sentences and universal sentences over L. Denoting with F O the set of all FO sentences over L, Eq(F O; 1) and Eq(F O; 1) are both undecidable.
Proof. It is well-known that the Bernays-Schon nkel-Ramsey fragment (BSR),
i.e. the set of FO prenex sentences (without function symbols)6 and with a pre x
like 9 8 , is such that SAT (BSR) is decidable [
We can summarize previous results in the following corollary: Corollary 1. The decision problem of establishing whether, given a FO query q('; ) over a su ciently expressive vocabulary, q('; ) is monotonic is undecidable.
Since any contradictory formula speci es a local FO query,8 the same argument used in lemma 1 can be reused for the decision problem of establishing whether a FO formula ' speci es a strongly distributive query, i.e. if ' is such that:
2. 'c is equivalent to a 1 sentence.
Corollary 2. The decision problem of establishing wheter, given a FO query q('; ) over a su ciently expressive vocabulary, q('; ) strongly distributes is undecidable. 4
Due to the previous section, we focus only on 1 formulas. Moreover, here we
consider only quanti er-free disjunctive normal form (DNF) formulas without
=.9 However, we report only about two syntactic bonds over conjunctions and
6 Recall that L is a purely relational vocabulary, hence function simbols would not
occour anyway.
7 All contradictions are equivalent and 9x x 6= x and 8x x 6= x are two of them,
the rst in 1 and the second in 1.
8 Because, for any structures S, q(S) = ; holds.
9 Anyway, we are con dent that adding equality would not change the core ideas
of what follows, but would only require some more technicality, like an equality
propagation procedure as the union- nd algorithm in [
We say that a formula ' (x1; : : : ; xn) is local i it speci es only local queries, i.e. i , for any structure S and any a1; : : : ; an 2 Dom(S):11
S j= ' (a1; : : : ; an) ) 9C 2 cc (S)
C j= ' (a1; : : : ; an) 4.1
Since a contradictory conjunction of literals is local, we will consider only satis able formulas. First, we focus on negative conjunctions, i.e. where all literals are negated, then, we take into account the remaining.
Theorem 4. Let L be a purely relational vocabulary and ' (x1; : : : ; xn) be a satis able negative conjunction of literals over L. Then ' is local i n = 1. Proof. Since ' is satis able, it is not possible that in ' occur both an asserted literal and its negation. ): Let S be a structure such that:
Dom(S) = fa1; : : : ; ang, where ai 6= aj if i 6= j; for any relation symbol R=m 2 L, SR = ;.12 Therefore, each a 2 Dom(S) forms a connected component and, since ' is negative:
S j= '(a1; : : : ; an) Since ' is local, (a1; : : : ; an) must lay on a single connected component. This is possible only if n = 1. (: By hypothesis, ' is of the form '(x). Then, let S be a structure and a 2 Dom(S) such that: Clearly, 9C 2 cc (S) such that a 2 Dom(C) and, by preservation theorem 2, also:13
S j= '(a)
C j= '(a)
Theorem 5. Let L be a purely relational vocabulary and ' (x1; : : : ; xn) a not negative satis able conjunction of literals over L. If ' is local, then ' is safe, i.e. any variable occurring in a negated literal ocours also in an asserted literal. 10 Recti cation and unfolding are those processes that allow to translate Datalog: without recursion in FO. 11 Clearly, it follows also that a1; : : : ; an 2 C. 12 I.e. S can be considered a plain set. 13 Each quanti er-free formula is also a 1 formula.
Proof. Let ' (x1; : : : ; xn) be a not negative satis able conjunction of literals Vi2I Li, where x 2 Var(') occurs only in negated literals. Say that x is x1. Since ' is not contradictory, then there is a structure S and a1; : : : ; an 2 Dom(S) such that: S j= ' (a1; : : : ; an). Now consider the structure S0, obtained from S adding a new element a to Dom(S). Therefore, a does not take part in the interpretative part of S0 and, clearly:
S0 j= ' (a; a2; : : : ; an) Since fag is the domain of a connected component of S0, the sequence (a; a2; : : : ; an) does not lay on a single connected component and so ' is not local. 4.2
Theorem 6. Let L be a purely relational vocabulary and ' (x1; : : : ; xn) a disjunction Wi2I 'i, where 'i is a satis able 1 formula over L for each i 2 I. If ' is local, then ' is regular, i.e. all disjuncts share the same set of free variables. Proof. Let ' (x1; : : : ; xn) be a satis able disjunction Wi2I 'i, where 'i 2 1 for each i 2 I. Suppose there are indices i; j 2 I such that Var('i) 6= Var('j ), say x 2 Var('i) n Var('j ) and suppose that x is x1. Since 'j (y1; : : : ; ym) is satis able, there is a structure S and a1; : : : ; am 2 Dom(S) such that:
S j= 'j (a1; : : : ; am) Let h be a valuation such that h(yi) = ai for each i 2 f1; : : : ; mg. Now, as in the previous proof, consider a structure S0, obtained from S adding an element a to Dom(S). Then, the valuation k, obtained from h putting k(x) = a, still satis es 'j in S0 (because x 62 Var('j )). So, by semantic of disjunction:
S0 j= ' (k(x1); : : : ; k(xn)) Since fk(x1)g = fag is the domain of a connected component of S0, (k(x1); : : : ; k(xn)) does not lay on a single connected component and so ' is not local. 5
We have proved that, for su ciently expressive vocabularies, the decision problem of establishing if a FO query strongly distributes over components is undecidable. This has been possible through a contrast with the Entscheidungsproblem of satis ability of F O formulas. However, we remark that we considered FO in its full expressive power, ignoring those syntactical bonds stemming from recti cation and unfolding, i.e. re ecting Datalog: safeness. Would something change if those bonds were considered? In fact, tackling the problem of locality, we showed that those bonds, in the form of safe conjunctions and regular disjunctions, are necessary conditions to allow locality of DNF quanti er-free formulas. This preliminary result should be extended to a full classi cation of FO formulas specifying local FO queries.