Hypothetical answers to continuous queries over data streams
Lu\'is Cruz-Filipe, Gra\c{c}a Gaspar, Isabel Nunes
TL;DR
This paper introduces a semantics and online algorithm for continuous data stream queries that provide hypothetical answers, enabling users to consider possible future states despite delays or blocking in data processing.
Contribution
It proposes a novel semantics for hypothetical answers in continuous queries and an online method to update consistent facts based on current information.
Findings
Provides a formal semantics for hypothetical answers
Develops an online algorithm for fact updating
Enables real-time consideration of possible future data states
Abstract
Continuous queries over data streams may suffer from blocking operations and/or unbound wait, which may delay answers until some relevant input arrives through the data stream. These delays may turn answers, when they arrive, obsolete to users who sometimes have to make decisions with no help whatsoever. Therefore, it can be useful to provide hypothetical answers - "given the current information, it is possible that X will become true at time t" - instead of no information at all. In this paper we present a semantics for queries and corresponding answers that covers such hypothetical answers, together with an online algorithm for updating the set of facts that are consistent with the currently available information.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Database Systems and Queries · Data Management and Algorithms · Semantic Web and Ontologies
Hypothetical answers to continuous queries over data streams
Luís Cruz-Filipe1
Graça Gaspar2
Isabel Nunes2
(1 Dept. Mathematics and Computer Science, University of Southern Denmark
2 LASIGE, Departmento de Informática, Faculdade de Ciências, Universidade de Lisboa)
Abstract
Answers to continuous queries over data streams are often delayed until some relevant input arrives through the data stream. These delays may turn answers, when they arrive, obsolete to users who sometimes have to make decisions with no help whatsoever. Therefore, it can be useful to provide hypothetical answers – “given the current information, it is possible that will become true at time ” – instead of no information at all.
In this paper we present a semantics for queries and corresponding answers that covers such hypothetical answers, together with an incremental online algorithm for updating the set of facts that are consistent with the currently available information. Our framework also works in a language supporting negation.
1 Introduction
Modern-day reasoning systems often have to react to real-time information about the real world provided by e.g. sensors. This information is typically conceptualized as a data stream, which is accessed by the reasoning system. The reasoning tasks associated to data streams – usually called continuous queries – are expected to run continuously and produce results through another data stream in an online fashion, as new elements arrive.
A data stream is a potentially unbounded sequence of data items generated by an active, uncontrolled data source. Elements arrive continuously at the system, potentially unordered, and at unpredictable rates. Thus, reasoning over data streams requires dealing with incomplete or missing data, potentially storing large amounts of data (in case it might be needed to answer future queries), and providing answers in timely fashion – among other problems, see e.g. [7, 21, 47].
The output stream is normally ordered by time, which implies that the system may have to delay appending some answer because of uncertainty in possible answers relating to earlier time points. The length of this delay may be unpredictable (unbound wait) or infinite, for example if the query uses operators that range over the whole input data stream (blocking operations). In these cases, answers that have been computed may never be output. An approach to avoid this problem is to restrict the language by forbidding blocking operations [44, 51]. Another approach uses the concept of reasoning window [11, 39], which bounds the size of the input that can be used for computing each output (either in time units or in number of events).
In our work, we do not impose such restrictions, and we show that we are able to provide useful information even in some instances of blocking queries.
In several applications, it is useful to know that some answers are likely to be produced in the future, since there is already some information that might lead to their generation. This is the case namely in prognosis systems (e.g., medical diagnosis, stock market prediction), where one can prepare for the possibility of something happening. To this goal, we propose hypothetical answers: answers that are supported by information provided by the input stream, but that still depend on other facts being true in the future. Knowledge about both the facts that support the answer and possible future facts that may make it true gives users the possibility to make timely, informed decisions in contexts where preemptive measures may have to be taken.
Moreover, by giving such hypothetical answers to the user we cope with unbound wait in a constructive way, since the system is no longer “mute” while waiting for an answer to become definitive.
Many existing approaches to reasoning with data streams adapt and extend models, languages and techniques used for querying databases and the semantic web [6, 8]. We develop our theory in line with the works of [11, 19, 39, 45, 51], where continuous queries are treated as rules of a logic program consisting of both rules and facts arriving through a data stream. Our techniques bear some similarites to previous work on abduction (see the discussion on related work in Section 7), but to the best of our knowledge this is the first time that hypothetical reasoning has been considered in the context of continuous query answering.
Contribution
We present a declarative semantics for queries in Temporal Datalog, where we define the notions of hypothetical and supported answers. We define an operational semantics based on SLD-resolution, where we compute answers with premises to queries. We then show that there is a natural connection between the answers computed by the operational semantics and the hypothetical and supported answers defined declaratively. By refining SLD-resolution, we obtain an incremental online algorithm for maintaining and updating the set of answers that are consistent with the currently available information. Finally, we define Temporal Datalog with negation and show that our results can be extended to this language.
Publication history
A preliminary version of this work, not including proofs, was published in conference proceedings [16]. The current article extends that work with proofs of all results and further examples. Section 6 (negation), which was only a sketch, was completely restructured, and now includes a precise definition of the declarative and operational semantics, as well as full proofs of all results, and several examples. Several results in this section were not stated previously, including soundness and completeness.
Structure
Section 2 revisits some fundamental background notions, namely the formalism from [46], which we extend in this paper. Section 3 introduces our declarative semantics for continuous queries, defining hypothetical and supported answers, and relates these concepts with the standard definitions of answers. Section 4 presents our operational semantics for continuous queries and relates it to the declarative semantics. Section 5 details our online algorithm to compute supported answers incrementally, as input facts arrive through the data stream, and proves it sound and complete. Section 6 extends our framework to negation by failure. Section 7 compares our proposal to similar ones in the literature, discussing its advantages.
2 Background
2.1 Continuous queries in Temporal Datalog
We use the framework from [46] to write continuous queries over datastreams, slightly adapting some definitions. We work in Temporal Datalog, the fragment of negation-free Datalog extended with the special temporal sort from [15], which is isomorphic to the set of natural numbers equipped with addition with arbitrary constants. In Section 6 we extend this language with negation.
Syntax of Temporal Datalog
A vocabulary consists of constants (numbers or identifiers in lowercase), variables (single uppercase letters) and predicate symbols (identifiers beginning with an uppercase letter). All these may be indexed if necessary; occurrences of predicates and variables are distinguished by context. In examples, we use words in sans serif for concrete constants and predicates.
Constants and variables have one of two sorts: object or temporal. An object term is either an object (constant) or an object variable. A time term is either a natural number (called a time point or temporal constant), a time variable, or an expression of the form where is a time variable and is an integer.
Predicates can take at most one temporal parameter, which we assume to be the last one (if present). A predicate with no temporal parameter is called rigid, otherwise it is called temporal. An atom is an expression where is a predicate and each is a term of the expected sort. Without loss of generality, we assume that all predicates are temporal. Rigid predicates can be made temporal by adding a dummy temporal parameter that does not affect their semantics. In other words, we replace every instance of by . Thus, holds iff holds – and the values of at time points other than [math] will have no impact on the semantics.
A rule has the form , where and each are temporal atoms. Atom is called the head of the rule, and the body. Rules are assumed to be safe: each variable in the head must occur in the body. A program is a set of rules.
If a predicate symbol occurs in an atom in the head of a rule with non-empty body, we call that predicate intensional, or an IDB predicate. A predicate that is defined only through rules with empty body is called extensional, or an EDB predicate. An atom is extensional/intensional (or EDB/IDB atom) according to whether its predicate symbol is extensional or intensional.
A term, atom, rule, or program is ground if it contains no variables. We write for the set of variables occurring in an atom, and extend this function homomorphically to rules and sets. A fact is a function-free ground atom.
Rules are instantiated by means of substitutions, which are functions mapping variables to terms of the expected sort. The support of a substitution is the set . We consider only substitutions with finite support, and write for the substitution mapping each variable to the term , and leaving all remaining variables unchanged. We call each expression a binding. A substitution is ground if every variable in its support is mapped to a constant. An instance of a rule is obtained by simultaneously replacing every variable in by and computing any additions of temporal constants.
A temporal query is a pair where is a program and is an IDB atom in the language underlying . We do not require to be ground, and typically the temporal parameter is uninstantiated.111The most common exception is if represents a property that does not depend on time, which normally would be written using a rigid predicate. In our framework, this would mean that ’s temporal parameter would be instantiated to [math].
A dataset is an indexed family of sets of EDB facts (input facts), each intuitively corresponding to the facts delivered by a data stream to a reasoning system at each time point.
Definition 1**.**
A dataset is a family , where is a set of EDB facts with timestamp .
We call the -slice of . For each , we also consider ’s -history .
From these definitions it follows that for every , and that contains only facts whose temporal argument is at most . By convention, .
Semantics
The semantics of Temporal Datalog is a variant of the standard semantics based on Herbrand models. A Herbrand interpretation for Temporal Datalog is a set of facts. If is an atom with no variables, then we define as the fact obtained from by evaluating its temporal term. We say that satisfies , , if . The extension of the notion of satisfaction to the whole language follows the standard construction, and the definition of entailment is the standard one.
An answer to a query over a dataset is a ground substitution whose domain is the set of variables in , satisfying . In the context of continuous query answering, we are interested in the case where is a -history of some data stream, which changes with time. We denote the set of all answers to over as .
We illustrate the extension we propose with a Temporal Datalog program, which is a small variant of Example 1 in [46]. We will return to this example throughout our presentation.
Example 1**.**
A set of wind turbines are scattered throughout the North Sea. Each turbine is equipped with a sensor that continuously sends temperature readings to a data centre. The data centre tracks activation of cooling measures in each turbine, recording malfunctions and shutdowns by means of the following program .
[TABLE]
Consider the query . If , then at time point [math] we can infer , but there is no output for . If arrives to at time point , then , and we can infer and , but there still is no answer to . Finally, the arrival of to at time point yields , allowing us to infer , , and . Then .
2.2 SLD-resolution
We now revisit some concepts from SLD-resolution, adapted from [12, 35].
A literal is an atom or its negation. Atoms are also called positive literals, and a negated atom is a negative literal. A definite clause is a disjunction of literals containing at most one positive literal. In the case where all literals are negative, the clause is a goal. We use the standard rule notation for writing definite clauses.
Definition 2**.**
Given two substitutions and , their composition is the substitution obtained from
[TABLE]
by (i) deleting any binding where and (ii) deleting any binding where .
Condition (i) removes redundant identity bindings. Condition (ii) ensures that, for every atom , .
Definition 3**.**
Two atomic formulas and are unifiable if there exists a substitution , also called a unifier, such that .
A unifier of and is called a most general unifier (mgu) if for each unifier of and there exists a substitution such that .
It is well known that there always exist several mgus of any two unifiable atoms, and that they are unique up to renaming of variables.
Recall that a goal is a clause of the form . If is a rule , is a goal with , and is an mgu of and , then the resolvent of and using is the goal .
If is a program and is a goal, an SLD-derivation of is a (finite or infinite) sequence of goals with , a sequence of -renamings222I.e. program clauses from whose variables have been renamed. of program clauses of and a sequence of substitutions such that is the resolvent of and using . A finite SLD-derivation of where the last goal is a contradiction () is called an SLD-refutation of of length , and the substitution obtained by restricting the composition of to the variables occurring in is called a computed answer of .
Proposition 1** (Soundness).**
Let be a program, be a goal, and suppose that there is an SLD-refutation of with computed answer . Then .
Proposition 2** (Completeness).**
Let be a program, be a goal, and suppose that . Then there is an SLD-refutation of with computed answer .
The notation stands for the formula , where . Since is of the form , this formula can be written equivalently as – i.e., in the previous two theorems states that entails any instance of any atom in .
There are two degrees of freedom when trying to build SLD-derivations: which literal to choose in the goal at any given point, and which clause to unify it with (in case there are several possibilities). The choice of the goal is dictated by a computation rule; for a given computation rule , the SLD-tree for and is the tree containing , and where each node contains one descendent for each possible resolvent of the literal chosen by in that node and the head of a rule in .
Proposition 3** (Independence of the computation rule).**
Let be a program and be a goal. Then every SLD-tree for and has the same (finite or infinite) number of branches ending with the empty clause.
This result states that the computation rule does not affect whether one can find an SLD-refutation for and .
3 Hypothetical answers
In our running example, being delivered at time instant [math] yields some evidence that may turn out to be true. Later, we may receive further evidence as in the example (the arrival of ), or we might find out that this fact will not be true (if does not arrive).
We propose a theory that also allows for such hypothetical answers to a continuous query: if some substitution can become an answer as long as some facts in the future are true, then we output this information. In this way we can lessen the negative effects of unbound wait. Hypothetical answers can also refer to future time points: in our example, would also be output at time point 0 as a substitution that may prove to be an actual answer to the query when further information arrives.
Our formalism uses ideas from multi-valued logic, where some substitutions correspond to answers (true), others are known not to be answers (false), and others are consistent with the available data, but can not yet be shown to be true or false. In our example, the fact is consistent with the data at time point [math], and thus “possible”; it is also consistent with the data at time point , and thus “more possible”; and it finally becomes (known to be) true at time point 2.
As already motivated, we want answers to give us not only the substitutions that make the query goal true, but also ones that make the query goal possible in the following sense: they depend both on facts that have been delivered by the data stream and on facts that still may be delivered by the data stream (i.e., those whose timestamp is greater than ).
Definition 4**.**
A ground atom is future-possible for if .
Definition 5**.**
A hypothetical answer to query over is a pair , where is a substitution and is a finite set of ground EDB atoms (the hypotheses) such that:
- •
;
- •
* only contains atoms future-possible for ;*
- •
;
- •
* is minimal with respect to set inclusion.*
* is the set of hypothetical answers to over .*
Intuitively, a hypothetical answer states that holds if all facts in are ever delivered by the data stream. Thus, is currently backed up by the information available. In particular, if then is an answer in the standard sense (it is a known fact).
Proposition 4**.**
Let be a query, be a data stream and be a time instant. If , then .
Proof.
If , then . When , this reduces to , which coincides with the definition of answer. ∎
We can generalize this proposition, formalizing the intuition we gave for the definition of hypothetical answer.
Proposition 5**.**
Let be a query, be a data stream and be a time instant. If , then there exist a time point and a data stream such that and .
Proof.
Let be the data stream such that:
- •
for ;
- •
contains the elements of with timestamp for .
Let be the highest timestamp in . It is straightforward to verify that satisfies the thesis. ∎
Example 2**.**
We illustrate these concepts in the context of Example 1.
Consider . Since , Then
[TABLE]
Since , we conclude that . Finally, , so . This answer has no hypotheses, and indeed .
Now consider for another constant . Then also includes e.g. . However, since does not contain , there is no element for .
Hypothetical answers where can be further split into two kinds: those that are supported by some fact(s) delivered by the datastream, and those for which there is no evidence whatsover – they only depend on facts whose truth value is unknown. For the former, : they rely on some fact from . This is the class of answers that interests us, as there is non-trivial information in saying that they may become true.
Definition 6**.**
Let be a query, be a data stream and be a time instant. A non-empty set of ground EDB atoms is evidence supporting if is a minimal set satisfying . A supported answer to over is a triple such that where is evidence supporting . We denote the set of supported answers to over by .
Since we are working with finite sets, if and , then there exists a set such that is a supported answer to over . However, in general, several such sets may exist. As a consequence, Propositions 4 and 5 generalize to supported answers in the obvious way. The condition ensures that the evidence must be used to infer the answer.
Example 3**.**
In Example 2, the hypothetical answer is supported by the evidence , while is supported by .
Since there is no evidence for , this answer is not supported.
This example illustrates that unsupported hypothetical answers are not very informative: it is the existence of supporting evidence that distinguishes interesting hypothetical answers from any arbitrary future fact.
However, it is useful to consider even unsupported hypothetical answers in order to develop incremental algorithms to compute supported answers: the sequence of sets \Theta^{E}_{\tau}=\{\theta\mid\langle{\theta,H,E}\rangle\in\mathcal{E}(Q,D,\tau)\mbox{ for some H,E}\} is not monotonic, as at every time point new unsupported hypothetical answers may get evidence and supported hypothetical answers may get rejected. The sequence \Theta^{H}_{\tau}=\{\theta\mid\langle{\theta,H}\rangle\in\mathcal{H}(Q,D,\tau)\mbox{ for some H}\}, on the other hand, is anti-monotonic, as the following results state.
Proposition 6**.**
Let be a query, be a data stream and be a time instant. If , then there exists such that and . Furthermore, if , then .
Proof.
Recall that by convention. If , then . Since is finite, there is a minimal subset of with the property that and . Clearly .
Assume that is also such that . Then ; but , so and therefore also . By definition of , this implies that , hence .
Finally, if is evidence supporting , then , hence , since . ∎
Proposition 7**.**
Let be a query, be a data stream and be a time instant. If and , then there exists such that .
Proof.
Just as the proof of the previous proposition, but dividing into and instead of into and . ∎
Examples 2 and 3 also illustrate this property, with hypotheses turning into evidence as time progresses. Since , Proposition 6 is a particular case of Proposition 7.
In the next sections we show how to compute hypothetical answers and the corresponding sets of evidence for a given continuous query.
4 Operational semantics via SLD-resolution
The definitions of hypothetical and supported answers are declarative. We now show how SLD-resolution can be adapted to algorithms that compute these answers. We use standard results about SLD-resolution, see for example [35].
We begin with a simple observation: since the only function symbol in our language is addition of temporal parameters (which is invertible), we can always choose mgus that do not replace variables in the goal with new ones.
Lemma 8**.**
Let be a goal and be a rule such that is unifiable with for some . Then there is an mgu of and such that all variables occurring in also occur in .
Proof.
Let be an mgu of and . For each , can either be a variable or a time expression . First, iteratively build a substitution as follows: for , if occurs in but does not and does not yet include a replacement for the variable in , extend with , if is , or , if is .
We now show that is an mgu of and with the desired property. If , then either (i) is and is for some or (ii) . In case (i), by construction of if occurs in but includes a variable not in , then replaces that variable with a term using only variables in . In case (ii), by construction does not occur in .
To show that is an mgu of and it suffices to observe that is invertible, with . ∎
Without loss of generality, we assume all mgus in SLD-derivations to have the property in Lemma 8.
Our intuition is as follows: classical SLD-resolution computes substitutions that make a conjunction of atoms a logical consequence of a program by constructing SLD-derivations that end in the empty clause. We relax this by allowing derivations to end with a goal if: this goal only refers to EDB predicates and all the temporal terms in it refer to future instants (possibly after further instantiation). This makes the notion of derivation also dependent on a time parameter.
Definition 7**.**
An atom is a potentially future atom wrt if it is future-possible for or either contains a temporal variable.
This concept generalizes the notion of future-possible atom for to possibly non-ground atoms. In particular, any atom whose time parameter contains a variable is a potentially future atom, since it may be instantiated to a time point in the future.
Definition 8**.**
An SLD-refutation with future premises of over is a finite SLD-derivation of whose last goal only contains potentially future EDB atoms wrt .
If is an SLD-refutation with future premises of over with last goal and is the substitution obtained by restricting the composition of the mgus in to , then is a computed answer with premises to over , denoted .
Example 4**.**
Consider query from Example 1 and . There is an SLD-derivation of ending with , which contains a single potentially future EDB atom with respect to . Thus, with .
As this example illustrates, computed answers with premises are the operational counterpart to hypothetical answers, with two caveats. First, a computed answer with premises need not be ground: there may be some universally quantified variables in the last goal. Second, may contain redundant conjuncts, in the sense that they might not be needed to establish the goal. We briefly illustrate these two features.
Example 5**.**
In our running example, there is also an SLD-derivation of ending with the goal , which only contains potentially future EDB atoms with respect to . Thus also .
Example 6**.**
Consider the following program :
[TABLE]
and the query .
Let . Then there is an SLD-derivation of that ends with the goal , which only contains potentially future EDB atoms wrt . Thus . However, atom is redundant, since suffices to make an answer to for any .
(Observe that also , but produced by a different SLD-derivation.)
We now look at the relationship between the operational definition of computed answer with premises and the notion of hypothetical answer. The examples above show that these notions do not precisely correspond. However, we can show that computed answers with premises approximate hypothetical answers and, conversely, every hypothetical answer is a grounded instance of a computed answer with premises.
Theorem 1** (Soundness).**
Let be a query, be a data stream and be a time instant. Assume that . Let be a ground substitution such that: (i) and (ii) if is , then . Then there is a set such that .
Proof.
Assume that there is some SLD-refutation with future premises of over . Then this is an SLD-derivation whose last goal only contains potentially future EDB atoms with respect to . Let be any substitution in the conditions of the hypothesis. Taking , we can extend this SLD-derivation to a (standard) SLD-refutation for , by resolving with each of the in turn. The computed answer is then the restriction of to . By soundness of SLD-resolution, . Since is finite, we can find a minimal set with the latter property. ∎
Theorem 2** (Completeness).**
Let be a query, be a data stream and be a time instant. If , then there exist substitutions and and a finite set of atoms such that , and .
Proof.
Suppose . Then . By completeness of SLD-resolution, there exist substitutions and and an SLD-derivation for with computed answer such that .
By minimality of , for each there must exist a step in this SLD-derivation where the current goal is resolved with . By independence of the computation rule, we can assume that these are the last steps in the derivation. Let be the derivation consisting only of these steps, and be the original derivation without . Let be the answer computed by and be its last goal, let be the answer computed by , and define . Then:
- •
Let ; then occurs in . If occurs in , then by construction . If is a ground term or does not occur in , then trivially since does not change . In either case, .
- •
: by construction of , , and since is ground for each , it is also equal to .
The derivation shows that . ∎
All notions introduced in this section depend on the time parameter , and in particular on the history dataset . In the next section, we explore the idea of “organizing” the SLD-derivation adequately to pre-process independently of , so that the computation of (hypothetical) answers can be split into an offline part and a less expensive online part.
5 Incremental computation of hypothetical answers
Proposition 7 states that the set of hypothetical answers evolves as time passes, with hypothetical answers either gaining evidence and becoming query answers or being put aside due to their dependence on facts that turn out not to be true.
In this section, we show how we can use this temporal evolution to compute supported answers incrementally.
We start by showing a simple result on SLD-derivations that allows us to reorganize the resolution steps based on the timestamp (§ 5.1). Using this result, we propose a two-stage process for computing and updating supported answers to continuous queries over data streams: a first (offline) stage pre-processes the program as much as possible (§ 5.2), and a second (online) stage updates a set of supported answers based on incoming information (§ 5.3). Correctness of the online stage, due to its complexity, is delegated to a separate section (§ 5.4).
5.1 A two-stage process
We start by revisiting SLD-derivations and showing how they can reflect the structure of the datastream.
Proposition 9**.**
Let be a query and be a data stream. For any time constant , if , then there exist an SLD-refutation with future premises of over computing and a sequence such that:
- •
goals are obtained by resolving with clauses from ;
- •
for , goals are obtained by resolving with clauses from .
Proof.
Immediate consequence of the independence of the computation rule. ∎
An SLD-refutation with future premises with the property guaranteed by Proposition 9 is called a stratified SLD-refutation with future premises. Since data stream only contains EDB atoms, it also follows that in a stratified SLD-refutation all goals after are always resolved with EDB atoms. Furthermore, each goal contains only potentially future EDB atoms with respect to . Let be the restriction of the composition of all substitutions in the SLD-derivation up to step to . Then represents all hypothetical answers to over of the form for some ground substitution (cf. Theorem 1).
This yields an online procedure to compute supported answers to continuous queries over data streams. In a pre-processing step, we calculate all computed answers with premises to over , and keep the ones with minimal set of formulas. (Note that Theorem 2 guarantees that all minimal sets are generated by this procedure, although some non-minimal sets may also appear as in Example 5.) The online part of the procedure then resolves each of these sets with the facts delivered by the data stream, adding the resulting resolvents to a set of schemata of supported answers (i.e. where variables may still occur). By Proposition 9, if there is at least one resolution step at this stage, then the hypothetical answers represented by these schemata all have evidence, so they are indeed supported.
5.2 Pre-processing step
We now look at the pre-processing step of our procedure in more detail.
In general, this step may not terminate, as the following example illustrates.
Example 7**.**
Consider the following program , where is an extensional predicate and is an intensional predicate.
[TABLE]
If is delivered by the datastream, then is true for every .
Thus, for all . The pre-processing step needs to output this infinite set, so it cannot terminate.
We establish termination of the pre-processing step for two different classes of queries. A query is connected if each rule in contains at most one temporal variable, which occurs in the head whenever it occurs in the body; and it is nonrecursive if the directed graph induced by its dependencies is acyclic, cf. [46].
Proposition 10**.**
Let be a nonrecursive and connected query. Then the set of all computed answers with premises to over can be computed in finite time.
Proof.
Let be the (only) temporal variable in . We first show that all SLD-derivations for have a maximum depth. First, associate to each predicate the maximum length of a path in the dependency graph for starting from . Next, associate to each goal the sorted sequence of these values for each of its atoms. Then each resolution step decreases the sequence assigned to the goal with respect to the lexicographic ordering.
Since this ordering is well-founded, the SLD-derivation must terminate.
Furthermore, since is finite, there is a finite number of possible descendants for each node. Therefore, the tree containing all possible SLD-derivations for is a finite branching tree with finite height, and by König’s Lemma it is finite.
Since each resolution step terminates (possibly with failure) in finite time, this tree can be built in finite time. ∎
The algorithm implicit in the proof of Proposition 10 can be improved by standard techniques (e.g. by keeping track of generated nodes to avoid duplicates). However, since it is a pre-processing step that is done offline and only once, we do not discuss such optimizations.
The authors of [46] also formally define query delay333These are not communication delays, but delays in producing answers to queries. and window size as follows, where is a query with temporal variable .
Definition 9**.**
A delay for is a natural number such that: for every substitution and every , iff .
If has a delay , then a natural number is a window size for if: for every substitution and all , iff .
To show termination of the pre-processing step assuming existence of a delay and window size, we apply a slightly modified version of SLD-resolution: we do not allow fresh non-temporal variables to be added. So if a rule includes new variables in its body, we generate a node for each of its possible instances. We start by proving an auxiliary lemma.
Lemma 11**.**
If has delay and window size , then there exist two natural numbers and such that: if an atom in a goal in an SLD-derivation for contains a temporal argument with or , then the subtree with that goal as root does not contain a leaf including an extensional atom with a temporal parameter dependent on .
Proof.
Assume that the thesis does not hold, i.e. for any and there exists an atom in an SLD-derivation for whose subtree contains a leaf including an extensional atom with temporal parameter dependent on . By the independence of the computation rule, this property must hold for any SLD-derivation for .
Then there is a predicate symbol that occurs infinitely many times in the tree for with distinct instantiations of the temporal argument. Since the number of distinct instantiations for the non-temporal arguments is finite (up to -equivalence), there must be at least one instantiation that occurs infinitely often. If applying SLD-resolution to it generates an extensional literal whose temporal argument depends on , then the tree would have infinitely many leaves containing distinct occurrences of its underlying predicate symbol.
For any , it is then straightforward to construct an instance of the data stream and a substitution such that and , so no number smaller than can be a delay for . Similarly, we can construct an instance of the data stream and a substitution such that is an answer to over but not over , so cannot be a window size for . ∎
Proposition 12**.**
If has a delay and a window , then the set of all computed answers with premises to over can be computed in finite time.
Proof.
Let and be the two natural numbers guaranteed to exist by the previous lemma. Then, if a goal contains a positive literal with temporal parameter with or , we know that the subtree generated from that literal cannot yield leaves with temporal parameter depending on . Hence, either this tree contains only failed branches, or it contains leaves that do not depend on , or it is infinite.
Although we do not know the value of and , we can still use this knowledge by performing the construction of the tree in a depth-first fashion. Furthermore, we choose a computation rule that delays atoms with temporal variable other than . For each node, before expanding it we first check whether the atom we are processing has already appeared before (modulo temporal variables), and if so we skip the construction of the corresponding subtree by directly inserting the corresponding leaves.
If an atom contains a temporal variable other than , all leaves in its subtree contain no extensional predicates with non-constant temporal argument (otherwise there would not be a delay for ). Therefore these sub-goals can also be treated uniformly.
Finally, suppose that a branch is infinite. Again using a finiteness argument, any of its branches must necessarily at some point include repeated literals. In this case we can immediately mark it as failed. ∎
In general, given a query , we can try to compute a finite set that represents as follows. As in the proof of the previous proposition, choose a computation rule that delays atoms with temporal variable other than . Build an SLD-tree with as initial goal, with the following two extra checks.
- •
Before expanding a node, check whether the atom being processed has already appeared before (modulo temporal variables), and if so immediately generate the corresponding leaves.
- •
If the chosen atom has already appeared in the derivation, immediately mark the branch as failed.
Building the SLD-tree amounts to the worst case of deciding entailment using SLD-resolution, which is NP-complete.
Definition 10**.**
* is the set of all entries such that the SLD-tree for contains a leaf with computed answer with premises to over such that is minimal in the whole tree.*
Each tuple represents the set of all hypothetical answers as in Theorem 1.
Remark.
The hypotheses in Propositions 10 and 12 are not necessary to guarantee termination of the algorithm presented for the pre-processing step. Indeed, consider the following example.
Example 8**.**
In the context of our running example, we say that a turbine has a manufacturing defect if it exhibits two specific failures during its lifetime: at some time it overheats, and at some (different) time it does not send a temperature reading.
Since this is a manufacturing defect, it holds at timepoint [math], regardless of when the failures actually occur.444This is actually an example of a rigid predicate, which we model as described. We can model this property by the rule
[TABLE]
Let be the program obtained from by adding this rule, and consider now the query . Performing SLD-resolution between and yields the new goal , which only contains potentially future atoms with respect to .
The program in this example includes a rule that uses two different time variables. As a consequence, the query is not connected, and it does not have a delay or window size (since no single predicate can use both and ). Still, the pre-processing step terminates.
We assume from this point onwards that the query is connected.
5.3 The online step
We now describe how to compute and update the set in a schematic way, i.e., using variables to represent families of similar hypotheses.
Definition 11**.**
A schematic supported answer for a query at time is a triple where is a substitution, is a set of ground EDB atoms and is a set of (not necessarily ground) EDB atoms such that for every ground substitution .
Definition 12**.**
A substitution is a minimal substitution with property if: for any substitution with property , there exists such that .
In particular, an mgu for a set is a minimal substitution unifying all formulas in the set.
Definition 13**.**
Let be a query. For each time point , we define the set as follows.
- •
**
- •
If and is a minimal substitution such that and only contains potentially future atoms wrt , then .
- •
If and is a minimal substitution such that only contains potentially future atoms wrt , then , where .
In § 5.4, we prove that is a set of schematic supported answers that captures the set precisely. Before that, we show that can be computed as follows.
Definition 14**.**
Let be a set of schematic supported answers for a query at time and be the result of pre-processing . The update of using , , is computed as follows.
- •
For each , let be the set of atoms with minimal timestamp. For each computed answer to and , add to .
- •
For each , let be the set of atoms with timestamp . For each computed answer to and , add to .
Lemma 13**.**
For all , .
Proof.
Both cases of the computation of are similar. We show the first one in detail. Assume that and is a minimal substitution such that and only contains potentially future atoms wrt . By definition of potentially future atom and the fact that all the elements of have the same timestamp (), the set contains the elements of with minimal timestamp. Therefore is a minimal substitution unifying all the elements of with elements of , and the thesis follows by soundness and completeness of SLD-resolution. Note that cannot be empty, since .
For the second case, we observe that all elements of have their timestamp instantiated (by connectedness, there can be at most one temporal variable, which is instantiated when new elements are added from ). The proof then proceeds as in the previous case. ∎
Example 9**.**
We illustrate this mechanism with our running example, where
[TABLE]
The atom with minimal timestamp in is . We start by setting .
Since , SLD-resolution between and yields . Therefore,
[TABLE]
Next, . As before, SLD-resolution between and yields . Furthermore, SLD-resolution between and yields .
Therefore,
[TABLE]
Next we have . Again, SLD-resolution between and yields the substitution , while SLD-resolution between (the atom with minimal timestamp in both and ) and yields . Thus
[TABLE]
The last element of has an empty set of hypotheses, so the answer is known at this point.
Suppose now that . Then SLD-resolution between and fails, so no new elements are added from to . Furthermore, (which appears in both and ) does not unify with , and we know that it cannot be delivered by the data stream. Therefore
[TABLE]
This example illustrates that, in particular, answers are always propagated from to . In an actual implementation of this algorithm, we would likely expect these answers to be output when generated, and discarded afterwards.
5.4 Correctness
We now show that the algorithm given in the previous section indeed maintains a set of schematic supported answers to that captures all supported answers at any given time point.
Theorem 3** (Soundness).**
If , , and instantiates all free variables in , then for some .
Proof.
First, we show by induction on that there is an SLD-derivation with future premises of and with computed answer with premises . For this is trivially the case.
Suppose now that and . By Lemma 13, can be computed by SLD-resolution from for either some or some . In both cases, we can compose this SLD-derivation with the one obtained either by the way is constructed or the one obtained by induction hypothesis to obtain an SLD-derivation with future premises of and – this simply requires adding the remaining elements of to all nodes in the derivation from Lemma 13.
By applying Theorem 1 to this SLD-derivation, we conclude that for some . By construction, is evidence for this answer. ∎
It may be the case that contains some elements that do not correspond to hypothetical answers because of the minimality requirement. Consider a simple case of a query where , and . Then , and the second element of this set has a non-minimal set of hypotheses. We chose not to include a test for set inclusion in the definition of , though, for efficiency reasons.
Theorem 4** (Completeness).**
If , then there exist a substitution and a triple such that , and .
Proof.
By Theorem 2, for some substitution and set of atoms with and for some . By Proposition 9, there is a stratified SLD-derivation computing this answer. The sets of atoms from unified in each stratum of this derivation define the set of elements from that need to be unified to construct the corresponding element of , and it is straightforward to check that they are defined as in Lemma 13. ∎
It also follows from our construction that: if is a query delay for , then the timestamp of each element of is at most . Likewise, if is a window size for , then all elements in must have timestamp at least .
The following example also shows how, by outputting hypothetical answers, we can answer queries earlier than in other formalisms.
Example 10**.**
Suppose that we extend the program in our running example with the following rule (as in Example 2 from [46]).
[TABLE]
If , then
[TABLE]
are both in . Thus, the answer is produced at timepoint , rather than being delayed until it is known whether is an answer.
Theorem 5** (Complexity).**
The set can be computed from and in time polynomial in the size of , and .
Proof.
If , then we can compute the set of elements of with minimal timestamp in linear time. To decide which substitutions make a subset of , we can perform classical SLD-resolution between and . For each such element of , the size of every SLD-derivation that needs to be constructed is bound by the number of atoms in the initial goal, since only contains facts. Furthermore, all unifiers can be constructed in time linear in the size of the formulas involved, since the only function symbol available is addition of temporal terms. Finally, the total number of SLD-derivations that needs to be considered is bound by the size of .
If and , then again we can compute in linear time the set of facts in that must unify with – these are the elements of whose timestamp is exactly . As above, the elements that must be added to can then be computed in polynomial time by SLD-resolution. ∎
It would be interesting to generalize our algorithm to non-connected queries, in order to deal with examples such as Example 8. There, if , it would be nice to obtain
[TABLE]
as this can be relevant information, even if we do not know when (or whether) it will lead to an answer to the original query. However, such a generalization requires substantial changes to our approach, and we leave it for future work.
6 Adding negation
We now show how we can extend our framework to include negation. We extend the syntax of our programs to allow negated atoms in the bodies of rules, but not in heads of rules or in queries. The semantics of negation is based on the closed world assumption.
Hypothetical answers need to deal with the fact that this semantics introduces non-monotonicity: if holds at a given point in time, may still become true later due to new incoming data. Therefore can only be taken as evidence for a hypothetical answer when the current -history allows us to prove that does not hold in the whole dataset. We deal with this issue by giving supported answers a semantics reminiscent of the Kripke semantics for intuitionistic logic.
6.1 Temporal Datalog with negation
To the best of our knowledge, the existing works on Temporal Datalog only consider the negation-free fragment of the language. We extend the syntax of Temporal Datalog in the standard way [2], by allowing bodies of rules to contain negated atoms. We further require any variables appearing in negated literals to occur elsewhere in a positive literal in the same rule (safe negation).
We illustrate this extended language with the example that we use throughout this section.
Example 11**.**
A hospital is conducting a study on early detection of critical patients. A patient that either shows bad results on their lab tests or does not have good vital signs (cardiac markers and blood oxygen levels) is placed under observation. A patient that is under observation and does not have good vital signs is moved to the ICU. This patient is considered a candidate for early risk detection two days before being moved to the ICU.
These rules are implemented in the following program , which uses EDB predicates (bad clinical analyses), (good cardiac markers) and (good blood oxygen levels), as well as IDB predicates (good vital signs), (patient status) and (patient at risk). All these predicates include the patient’s name as the first argument and the timestamp as the last; predicate also includes the patient status ( for “under surveillance” and for “intensive care”) as second argument. Since the laboratory is overworked, they only communicate bad results of analyses as a combined outcome (predicate ) after two days.
[TABLE]
Note that actually conveys information about the patient’s status at timestamp . (In particular, and are never produced by the datastream for any .)
If is a program and is a dataset, we write to denote that is entailed by and according to the cautious answer set semantics for logic programming [24]. As usual, a precise correspondence between this semantics and an operational semantics based on SLD-resolution only holds in the presence of a stratification of the predicate symbols in the program with respect to negative dependencies [35]. We now discuss what a notion of stratification should look like for programs in Temporal Datalog with negation.
Definition 15**.**
The temporal closure of a program in Temporal Datalog with negation is the program defined as follows. For each -ary predicate symbol with a temporal argument in the signature underlying , the signature for contains a family of -ary predicate symbols . For each rule in , contains all rules obtained by instantiating its temporal parameter in all possible ways and replacing by .
Observe that is an infinite program (in Datalog with negation) as long as has at least one predicate with a temporal argument.
Recall that, for infinite programs, a stratification of is an infinite sequence of disjoint programs such that and, for each predicate symbol , (i) the definition of is contained in one , (ii) if occurs in the body of a rule with head , then the definition of is contained in for some such that (if the occurrence is not negated) or (if the occurrence is negated) [30].
Definition 16**.**
A program is -stratified if is stratified.
This definition of stratification is reminiscent of the concepts of locally stratified [41, 42] and temporally stratified [52]. However, it differs from both. Local stratification has mostly been studied in the context of programs with a finite number of constants, which is not our case (there are infinitely many time points). On the other hand, temporal stratification as in [52] requires each stratum to contain exactly the predicates with the same time parameter (i.e., contains all rules whose head uses predicate symbols indexed by ). We make no such assumption in this work.
Example 12**.**
Program is -stratified with the following strata:
[TABLE]
Given an interpretation , satisfaction of rules and programs is defined as before. (Note that the restriction that negation be safe removes any potential ambiguity.) It is easy to check that is a model of iff it is a model of , and as a consequence -stratified programs have a unique answer set that coincides with their well-founded model.
For finite programs, stratification can be phrased (and decided) as a property of the graph of dependencies between the predicate symbols in the program. In our case, such a graph is infinite, and such a procedure may not terminate. However, the usual construction can be adapted to our framework in order to provide a decision procedure.
Definition 17**.**
Let be a program. The temporal dependency graph of , , is the smallest graph satisfying the following properties:
for each predicate symbol with a temporal argument, includes a node with label (where is a formal temporal variable); 2. 2.
for each predicate symbol without temporal arguments, includes a node with label ; 3. 3.
for each node with label with and each rule in the definition of , let be the substitution that makes the temporal variable in the head of equal to :
- (a)
for each positive literal in , includes an edge between and with label . 2. (b)
for each negative literal in , includes an edge between and with label .
The graph can be constructed by starting with the nodes described in the first two conditions, adding the edges (and new nodes) required by conditions 3(a) and 3(b), and iterating the process for any newly created nodes.
Example 13**.**
The temporal dependency graph for the program is depicted below.
[TABLE]
Proposition 14**.**
*There is an algorithm that decides whether a program is -stratified. *
Proof.
We first show that we can decide whether contains a path that passes infinitely many times through distinct edges labeled with . Indeed, we can build a finite subgraph of by not expanding any nodes labeled if already contains a path from to for some . Since only contains a finite number of rules with a finite number of literals in their bodies, this condition generates an upper bound on the timestamps of the nodes that appear in the graph; since the number of predicate symbols is finite, must also be finite. Furthermore, contains a path in the conditions described if either (i) also contains such a path (i.e. it contains a loop including an edge labeled with ) or (ii) contains a path from to with that includes an edge labeled with .
Now we show that, if does not contain a path that passes infinitely many times through edges labeled with , then is -stratified.
Let be the graph of dependencies for . For each predicate symbol in , the graph contains a subgraph isomorphic to a subgraph555It may be a proper subgraph in case is low enough that some temporal arguments would become negative. of the connected component of containing . In particular, contains infinitely many copies of .
Suppose that contains a path that passes infinitely many times through edges labeled with , and let be a node in it with minimum value of (if occurs multiple times in the path, choose any one of its occurrences). Consider the isomorphic copy of embedded in where is mapped to . The whole path starting from must be contained in this copy, since the timestamps of all corresponding nodes in are greater or equal to .
Using these two properties, we can construct a stratification of in the usual inductive way.
- •
- •
For each , contains all predicates labeling nodes in such that: all paths from contain only edges labeled with .
- •
For each , is obtained from by removing all nodes with labels in and all edges to those nodes.
The only non-trivial part of showing that is a stratification of is guaranteeing that every predicate symbol is contained in for some . This is established by induction: if any path from contains at most edges labeled with , then . We now show that, for any , there is such a bound on the number of edges labeled with .
First observe that, in , there is a bound on the number of edges labeled with in any path starting from : (i) if there is a path from to for some and containing an edge labeled with , then there would be a path with an infinite number of such edges, and (ii) since there is a finite number of predicate symbols in we cannot build paths with an arbitrarily long number of edges labeled with .
Now consider a path starting at . If this path has length greater than , then it cannot be contained completely in the subgraph of isomorphic to containing . Therefore, it must at some point reach a node with . Likewise, the path starting at corresponds to a path in a (different) subgraph of isomorphic to , and as such cannot contain more than edges labeled with . Since we can only decrease a finite number of times, the path cannot contain arbitrarily many edges labeled with . ∎
Note that this does not contradict the classical undecidability of deciding whether a program has local stratification [40], since our language does not have function symbols.
Example 14**.**
When the graph is finite, the proof of Proposition 14 can be used to construct any stratum in finite time by constructing only the necessary part of . In particular, applying it to shown earlier yields the stratification already presented in Example 12.
For illustrative purposes, we show a fragment of the graphs , and , marking in color the nodes that are removed (i.e., collected in ).
[TABLE]
[TABLE]
6.2 Hypothetical answers in the presence of negation
The inclusion of negation in the language poses a new problem with respect to defining the notion of evidence for a hypothetical answer: we need to be able to argue that some atom will never become true given the set of hypotheses. To formalize this notion,
it is not enough to consider the data stream extended by – we need to account also for additional information that may make more atoms provable.
Definition 18**.**
Let be a dataset, be a time point and and be finite sets of ground EDB atoms. A dataset is a possible evolution of compatible with at time if:
- •
* for all ;*
- •
;
- •
.
Intuitively, contains the facts that must be produced by the data stream, and the facts that cannot be produced by the data stream.
Hypothetical answers to a query over , where may contain negated atoms, need to consider all possible evolutions of the dataset consistent with the hypotheses.
Given a set of literals , we write for the set of positive literals in and for the set of atoms whose negation is in . In particular, we use this notation in the next two definitions.
Definition 19**.**
A hypothetical answer to query over is a pair , where is a substitution and is a finite set of ground EDB literals such that:
- •
;
- •
* and only contain atoms future-possible for ;*
- •
* for each possible evolution of compatible with at time ;*
- •
* is minimal with respect to set inclusion.*
Definition 20**.**
Let be a query, be a data stream and be a time instant. A set of ground EDB literals is evidence supporting if:
- •
* and ;*
- •
;
- •
* for each possible evolution of compatible with at time ;*
- •
* is minimal with respect to set inclusion.*
Note that the third condition effectively ignores , since it ignores its contents at all time points. This matches our intuition that the evidence is exactly the information from the data stream that is relevant to prove the query.
A supported answer to over is a triple such that and is evidence supporting .
Intuitively, is the set of facts produced by the data stream that are essential to the hypothetical answer, while is the set of facts whose absence is relevant for the hypothetical answer.
We illustrate these alternative notions in the context of our running example.
Example 15**.**
Consider the program from Example 11 and the query , and let .
- •
Suppose that then where is one (of several) hypothetical answers to over , with evidence .
Indeed , so it can never hold; therefore holds, and we can conclude . If is never produced by the data stream, then also holds, from which we can derive and as a consequence .
- •
*Assume now that . Now there is a hypothetical answer to over , where . Indeed, holds as long as is produced by the data stream; and if is not produced by the data stream, then as before holds, from which we can derive and . At this stage, there is no evidence for . *
6.3 Pre-processing
The notion of computed answer with premises in the presence of negation is generalized by allowing leaves of SLD-resolution to contain negated (EDB or IDB) atoms besides positive EDB atoms.
Our two-stage algorithm can now be adapted to the language with negation using this extended notion. Let be a query. In the pre-processing step, we compute the set using SLD-resolution as before. For each element and , if is , we generate a new query , obtained by replacing the time parameter in with a variable, and repeat the pre-processing step to compute . We iterate this construction until no fresh queries are generated.
Given that the number of constants is finite and the number of arguments in any predicate in is finite, the total number of queries that can be generated is also finite – albeit quite high, as in the worst case we can generate auxiliary queries, where is the number of predicate symbols in the language, is the number of constants, and is the highest arity of any predicate in . (The only possible source of unboundedness is the temporal parameter, which we keep uninstantiated.) Therefore, Propositions 10 and 12 still hold for this more expressive language, but there is an exponential increase in worst-case complexity of the pre-processing step.
Example 16**.**
We continue with our running example (Example 11). Applying SLD-resolution to until we reach a goal with only extensional or negated atoms results in two possible derivations:
[TABLE]
This yields the following set .
[TABLE]
Since and appear as negated hypotheses, we generate two auxiliary queries and . These queries are now pre-processed in turn.
[TABLE]
Since the newly generated negated goals yield queries that have already been considered, the pre-processing step is finished.
Constants in generated queries
The negated atoms in leaves may be partly instantiated. This creates a need to decide whether those instantiations should be maintained, or whether all terms should be replaced by variables in the new query. The precise choice depends on the concrete instance of the problem: replacing all terms by variables restricts the total number of queries being managed, since all negated instances involving the same predicate reduce to the same query. However, having instantiated terms may substantially reduce the number of branches in the SLD-tree constructed, and the number of potential answers that have to be tracked. In particular, if the instance originates from a term that is instantiated in the original query, it might be counter-productive to replace it by a variable.
Example 17**.**
Consider the program below and the query .
[TABLE]
In this case, replacing the constants , and with a variable in the generated queries results in the same query in all cases. Keeping the constants in the generated queries results in the need to process , and , which generates three isomorphic trees and nearly identical computed answers with premises.
Example 18**.**
Consider the following program
[TABLE]
and the query . This query generates as premise , which can never hold because of the second rule. However, if is abstracted to a variable, the generated query becomes , which yields two computed answer with premises and .
One possible approach would be to keep all instantiated non-temporal terms unchanged, but replace them by variables if a new query on the same predicate is generated. We defer the concrete choice of strategy to future work, as it is immaterial for this work. In particular, the previous comment on Propositions 10 and 12 applies in either case.
Theorem 6** (Soundness and completeness of pre-processing).**
Let be one of the queries obtained from the pre-processing of , be a set of literals with timestamp higher than such that only contains EDB atoms. Assume that is consistent, and let be a substitution that instantiates all variables in . Then iff there exist substitutions and and a set such that , and .
Proof.
From soundness and completeness of SLD-resolution, it immediately follows that iff for some and such that and for some substitution . (Note that the pre-processing step essentially treats negated literals as EDB atoms.) ∎
6.4 The iterative step
In the online step of the algorithm, we now need to compute schematic answers not only to the original query, but also to each query generated by the pre-processing step. In this section, we use to range over all these queries. This step is now significantly more complex than for the language without negation: besides updating the (positive) hypotheses in hypothetical answers with information from the data stream, we need to apply a fixpoint construction in order to update the negative hypotheses – these are updated using the computed schematic answers themselves, and each update can trigger new possible updates.
In order to simplify the presentation, we first formulate the iterative step working only with ground terms. After discussing its soundness and completeness, we show how it can be reformulated in terms of schematic hypothetical answers using variables, as in the previous case. Without loss of generality, we also assume that all constants are abstracted to variables in the queries generated by the pre-processing step, so that for each literal there exists at most one query on the predicate symbol in . (This assumption removes the need for some quantifications, but does not change anything in an essential manner.)
We work with generalized hypothetical answers, where hypotheses can be EDB literals or negated IDB atoms, and we recursively define sets of these entities. The definition uses an auxiliary family ; intuitively, is computed from by updating positive hypotheses according to the data stream (as in the case without negation), and is computed from by updating the negative hypotheses.
Definition 21**.**
The families of sets and are defined recursively as follows, where is one of the queries under consideration.
. 2. 2.
For each , let be the (possibly empty) set of elements of with timestamp . If , . 3. 3.
For each , let be the set of elements of with minimal timestamp. For each substitution such that is ground:
- (a)
If is non-empty and , then . 2. (b)
If has timestamp and all elements of are negative literals, then . 3. (c)
If has timestamp and every element of has timestamp strictly larger than , then . 4. 4.
* is obtained by applying the following operator to until a fixpoint is reached: given a family of generalized hypothetical answers, non-deterministically select a query over a literal .*
- (a)
If there is a tuple , then for all remove every from whenever . 2. (b)
For all substitutions such that the timestamp of is at most and there is no tuple , if contains an element such that , then remove from and add it to .
We assume that selects a query such that changes, if possible.
The operator randomly selects a query and updates the generalized hypothetical answers that use negative ground instances of literal by (i) discarding the ones whose hypotheses contradict generated answers to and (ii) moving hypotheses to evidence when they match no generalized hypothetical answer to . In order to guarantee that all these steps are finite, the second step in the computation of only looks at hypotheses whose timestamp is at most the current value of – steps 3(b) and 3(c) ensure that does not incorrectly remove some negative hypotheses.
Lemma 15**.**
Iterating always reaches a fixpoint in finite time.
Proof.
If is different from , then either the total number of elements in all the sets decreases or the total number of elements in all the sets in tuples in all decreases. But set is finite: every element of either comes from unification between and the current -history (and since both and -histories are finite, only a finite number of elements can be generated in this way), or from directly instantiating elements of with a timestamp at most (which can only be done in finitely many ways). Therefore this process must terminate. ∎
Lemma 16**.**
For each query , the set is uniquely defined.
Proof.
We start by showing that: if we mark the generalized hypothetical answers that can be removed from a set and the set of (negative) hypotheses that can be turned into evidence, then, after applying once, all actions that were not made can still be applied afterwards. Together with the fact that the actions enabled by new tuples that arrive are the same, this implies that all actions must have been performed when reaching a fixpoint.
Let and be families of generalized hypothetical answers to the queries such that can be obtained from by application of .
- •
If can be removed from by application of and there is a corresponding tuple in (either the same or obtained by moving something from to in the second case defining ), then can be removed from by application of .
Indeed, if , then this answer must still be in , since does not remove answers (with empty set of hypotheses). Furthermore, if then , since prevents from being removed from by application of .
- •
If can be transformed into by application of and there is a corresponding tuple in with , then can be changed to by application of .
Indeed, if the timestamp of is at most and there is no tuple , then this must still be the case in , since does not add new tuples to .
Now consider two sequences of applications of starting from and ending at a fixpoint. By inductively applying the previous argument, any tuples that can be removed or changed in must have been removed or changed in the same way when reaching the fixpoint. Furthermore, new tuples that can be removed or changed due to tuples that were removed or changed will be the same in both sequences of applications, since these tuples are directly determined by the action(s) performed. Therefore both sequences must end at the same fixpoint. ∎
We illustrate this construction by means of a small example, before moving to our richer running example.
Example 19**.**
Consider the query where is the following program.
[TABLE]
The pre-processing step for this query generates . Since occurs negated in the premise of the only answer in this set, we generate a new query , for which the pre-processing step yields .
Assume that . Since the only element of contains a negated atom in its premises, we are in case (3c) and . Furthermore, , since . Since there is no element in , we move to the set of evidence in the only element of ; this yields a fixpoint of , so and .
Now suppose that . Reasoning as before, we obtain . However, since , we also obtain . Now there is an answer in with substitution and non-empty set of premises, so we cannot conclude anything about yet, and thus is already a fixpoint of ; so .
If , then . As a consequence, does not hold, and is removed by .
On the other hand, if , it is the answer that does not propagate to , from which applying will allow us to conclude that is output as an answer to .
Soundness and completeness hold for -stratified programs. Proving soundness requires a partial form of completeness, which is why the next lemma is stated as an if-and-only-if.
Theorem 7** (Soundness).**
Let , where is -stratified, be one of the queries obtained from the pre-processing of , be a set of literals with timestamp higher than such that only contains EDB atoms. Assume that is consistent, and let be a substitution that instantiates all variables in .
Then:
- (i)
If for some and such that and , then . 2. (ii)
If the timestamp of is at most , then the converse implication also holds.
Proof.
The proof is by induction on the construction of , considering all queries simultaneously. For clarity, we prove (i) and (ii) separately arguing by induction on the timestamp, but their proofs use each other’s induction hypothesis. We point out that induction hypotheses are always applied to sets that have been constructed earlier, i.e. we first conclude (i) and (ii) for , then for , then for , then for , etc, until we reach .
We first prove property (i). For , this is trivial. Assume that the result holds for . We go through the steps of the construction of .
- (Step 2.)
Suppose that , that for the set of elements with timestamp of , and that and . By construction , and . If is consistent, then the induction hypothesis yields the thesis, since . 2. (Step 3.)
Suppose that , let be the set of elements in with minimal timestamp, and suppose that makes all elements of ground. The cases (b) and (c) follow immediately from Theorem 6.
For case (a), suppose that and that . In particular, all elements of have timestamp . Then , so by Theorem 6, . The thesis follows by observing that . 3. (Step 4.)
The proof follows by induction on the number of times that is applied. Again, step (a) is trivial, since it generates no new generalized hypothetical answers.
For step (b), we need to look at the generalized hypothetical answers that are changed by . Assume that is such that for some and with the timestamp of at most , and that there is no tuple . Suppose that and . Then and .
But is consistent iff , which by induction hypothesis (on ) is the case since there are no tuples . Therefore the induction hypothesis (on ) allows us to conclude that . But the induction hypothesis (on ) also yields that : since is stratified, if this were not the case then , whence there would be some tuple .
We now move to property (ii). From Theorem 6, there exists such that for some substitution and . We prove that (ii) holds whenever the minimal timestamp of is at most , which implies the thesis. For this vacuously holds, since timestamps must be positive.
Assume that . If the minimal timestamp of is strictly smaller than , then by induction hypothesis applied to , there exists such that and . Step (2) of the algorithm then adds to , where , and by construction and . If the minimal timestamp of is exactly , then a tuple satisfying the thesis is added to in step (3).
We now show that the fixpoint construction in step (4) does not break this property.
- •
Suppose step 4(a) applies to a set . If there is a tuple , then by induction hypothesis for any set in the conditions of the theorem, and therefore is inconsistent whenever . As such, any tuple whose set contains can be removed from .
- •
Suppose step 4(b) applies to a set . Since this step adds elements to and removes elements from , the thesis holds even if this step is applied to this tuple.∎
This result guarantees that any answer to query will eventually be represented by an element of , but it does not ensure that that element necessarily becomes an answer, since the set of premises may never become empty. The next result shows that this is indeed the case.
Proposition 17**.**
In the same conditions as the previous theorem, if , then there exists such that either (a) or (b) does not contain any element of the form such that .
Proof.
By induction on the stratification of , i.e., on the stratum of , where is the (instantiated) temporal argument in .
If is in the lowest stratum, then it does not depend on any negated predicates. The thesis then follows by observing that the algorithm behaves for this predicate as in the case of the fragment without negation, and invoking Theorems 3 and 4.
Otherwise, by induction hypothesis, for every negative literal in there is a timestamp where the corresponding query is decided (any schematic answer for the relevant predicate has no premises). Take to be the highest of those timestamps. In step (4) of the algorithm, in any generalized hypothetical answers where instantiates the timestamp of to , all negated literals in the set of premises must either lead to the answer being discarded 4(a), or be moved to the set of evidence 4(b). Therefore, at the end of this iteration, for any generalized hypothetical answer the set only has positive literals. If is always empty, the thesis holds. Otherwise, let be the highest timestamp in all such sets ; the construction in step (3) guarantees that in all in answers that have not been discarded must be empty. ∎
Corollary 18** (Completeness).**
If is an answer to , then there exists such that contains a tuple where for some substitution .
Remark.
The correspondence with the declarative notion of (supported) hypothetical answer is less direct, since generalized hypothetical answers are allowed to have negated literals. Variants of Theorem 7 and Lemma 17 relating directly to hypothetical answers can be obtained by recursively processing negative hypotheses and evidence:
- •
if appears in a set of evidence, replace it with the evidence for that was used to place it there in step 4(b);
- •
if appears in a set of hypotheses, then replace the generalized hypothetical answer with all possible generalized hypothetical answers where is replaced by with and .
The last step generates a combinatorial explosion of the number of hypothetical answers. We also believe that generalized hypothetical answers are more readable in practice, as they encapsulate the strata of the program (and the information about negative hypotheses/evidence can be inspected separately). For these reasons, we do not pursue this correspondence further.
We now present an alternative to Definition 21 avoiding grounding and discuss its complexity.
Definition 22**.**
The sets and , where is one of the queries under consideration, are recursively defined as follows.
. 2. 2.
For each , let be the (possibly empty) set of elements of with timestamp . For all substitutions such that , . 3. 3.
For each , let be the set of elements of with minimal timestamp.
- (a)
If is non-empty, then for every substitution such that , then . 2. (b)
Let with the temporal variable in . If all elements of are negative literals, then . 3. (c)
Let with the temporal variable in . If every element of has timestamp strictly larger than the timestamp of , then . 4. 4.
* is obtained from as follows. Fix a topological ordering of the stratification of . There is only a finite number of such that has at least one schematic answer with (where is the temporal parameter in ). For each of these in order, set and let be the set of schematic answers to such that .*
- (a)
if contains a tuple , then: in each , replace every such that is unifiable with an element with all possible such that is a minimal substitution with the property that is not unifiable with ; 2. (b)
in each , for each such that contains an element with predicate symbol and timestamp and there is no tuple such that and are unifiable, then remove from and add it to .
Lemma 19**.**
The elements of are exactly the ground instances of the elements of .
Proof (Sketch.).
Straightforward by induction on the construction of the sets and , observing that the steps in Definitions 21 and 22 always yield sets in the relation stated in the lemma.
For step 4, since the order of iterations of to compute from is immaterial (Lemma 16), we can assume without loss of generality that always chooses a literal in the lowest possible stratum. Thus one application of (Definition 21) corresponds to performing step 4 in Definition 22 for one literal . Finally, using a topological ordering guarantees that a fixpoint is reached, since processing one of the cannot change elements of for each previously processed. ∎
Theorem 8** (Complexity).**
Let be the highest arity of any predicate that occurs negated in . If is -stratified, then can be computed in time exponential in and polynomial on the size of , , and the total number of queries.
Proof.
Steps (1), (2) and (3a) are as in Theorem 5, but they are now iterating over all sets of queries. Therefore the previous time bounds apply, multiplied by the total number of queries. Steps (3b) and (3c) can be done in time linear on the size of .
Each iteration of step (4) requires computing the set of negative literals in a schematic answer (which can be done in time linear on the size of the answer) and checking whether a corresponding tuple exists in the current . This can be done in time linear in the size of , which is polynomial in the size of (since it was computed from by a polynomial algorithm). The number of substitutions that need to be considered is bound by the number of constants to the power , which is constant; thus any remaining answers can be added in worst-case polynomial time. Finally, the total number of iterations of step (4) is at most the total number of queries multiplied by . ∎
The only parameter on which there is an exponential dependency in this complexity bound is . In practice, this value is small, since predicates in real-life programs typically do not involve more than a few variables. This minimizes the impact of this exponential complexity.
We can also improve on the average-time complexity by delaying the instantiation in step 4 through a number of other techniques. One possibility is delaying the application of step 4 until there are no positive atoms in , so that all negative literals are as instantiated as possible. In particular, if all negations in are safe, the only potential uninstantiated variables are those in the original query . Another possibility is storing abstractly, e.g. as a set of constraints on the substitution (such as ). In the worst case, though, any of these approaches still has the same complexity as the simpler version presented earlier – since we can always find an example where the number of answers to the original query is exponential on .
We now illustrate this algorithm with our running example, where all cases are covered.
Example 20**.**
Assume that there are two patients being monitored, and . Recall that pre-processing yielded the sets
[TABLE]
where the literals with minimal timestamp in each set of premises are underlined, and that, by definition, .
We start at time point , and assume that . Since for all queries , step 2 is trivial.
The table below shows the schematic hypothetical answers added in each substep of step 3. Substeps 3(b) and 3(c) uses in all queries.
[TABLE]
We obtain:
[TABLE]
We move on to step 4. In the stratification (up to timestamp [math]), and at the lowest stratum, and depends on both of them; we include only the relevant information on each – the substitution and whether the set of hypotheses is empty. Since is at the highest stratum, no schematic hypothetical answers can depend on it, and we do not include it in the table.
[TABLE]
We finally obtain:
[TABLE]
We move on to , and assume that . We summarize the application of step 2 in the next table.
[TABLE]
Furthermore, in step 3 we obtain the following additional schematic hypothetical answers, where substeps 3(b) and 3(c) use in all queries.
[TABLE]
Combining all these results, we obtain:
[TABLE]
and we observe that is an answer to . In order to perform step 4, we note that the relevant strata are: , and at the lowest level; at the next level; and finally and in the two highest levels, which we omit since no other queries depend on them. We again summarize application of step 4 in a table.
[TABLE]
At the end of this step, we have:
[TABLE]
We now consider , with . In step 2, the two answers from with as hypothesis are ignored (since does not unify with any element of ) and the remaining ones are copied to . After this step, we have therefore that
[TABLE]
In step 3a we obtain the answer in , while steps 3b and 3c are similar to the previous timestamps. After step 3, we have therefore
[TABLE]
The relevant strata for step 4 are now , and at the lowest level, followed by at the next level. As before we can omit from the discussion, since no other queries depend on that predicate. This step is summarized in the table below.
[TABLE]
At the end of this step, we have:
[TABLE]
Forgetting
The previous example shows that the online algorithm needs to keep track of a potentially large number of schematic supported answers while running. Furthermore, even answers without premises need to be kept due to the first check in step 3. This may raise concerns about this algorithm having potentially unbounded memory requirements.
For stratified programs, this is not the case, since all schematic answers eventually become answers (with no premises) or are discarded (this follows by combining Proposition 17 with Lemma 19). Furthermore, answers can also be forgotten eventually: static analysis on the sets can be used to determine how long an answer can influence the results of the algorithm (essentially, this is a refinement of the notion of the delay of the query), so that all answers can be discarded after enough time has passed. Hypothetical answers can also be discarded when there is an answer with the same substitution (this is the case for the query and at the end of the last example).
Explicit instantiation
Step 4 requires instantiating answers with all constants that do not satisfy a particular condition, which can immensely increase the number of schematic answers that have to be considered. In a practical implementation, as mentioned earlier, we expect that this can be addressed by adding constraints to the substitutions in these answers instead of explicitly instantiating them; in our example, in the different applications of step 4(a), we would typically add constraints or instead of explicitly instantiating . In this manner, we expect that we can partially avoid the exponential blowup that this step of the algorithm might cause.
7 Related work and discussion
Our work contributes to the field of stream reasoning, the task of conjunctively reasoning over streaming data and background knowledge [48, 49].
Research advances on Complex Event Processors and Data Stream Management Systems [18], together with Knowledge Representation and the Semantic Web, all contributed to the several stream reasoning languages, systems and mechanisms proposed during the last decade [21].
Hypothetical query answering over streams can be broadly related to works that study abduction in logic programming [29, 22], namely those that view negation in logic programs as hypotheses and relate it to contradiction avoidance [3, 23]. Furthermore, our framework can be characterized as applying an incremental form of data-driven abductive inference. Such forms of abduction have been used in other works [37], but with a rather different approach and in the plan interpretation context. To our knowledge, hypothetical or abductive reasoning has not been previously used in the context of stream reasoning, to answer continuous queries, although it has been applied to annotation of stream data [4].
Below we focus on four dimensions of stream reasoning — incremental evaluation, unbound wait and blocking queries, incomplete information, and negation —, which, in our opinion, due to the characteristics of our work, provide the most interesting and meaningful comparison with existing works in the field.
Incremental evaluation
Computing answers to a query over a data source that is continuously producing information, be it at slow or very fast rates, asks for techniques that allow for some kind of incremental evaluation, in order to avoid reevaluating the query from scratch each time a new tuple of information arrives. Several efforts have been made in that direction, capitalising on incremental algorithms based on seminaive evaluation [2, 9, 27, 28, 38], on truth maintenance systems [10], window oriented [25] among others. Our algorithm fits naturally in the first class, as it is an incremental variant of SLD-resolution.
Unbound wait and blocking queries
The problems of unbound wait and blocking queries have deserved much attention in the area of query answering over data streams. There have been efforts to identify the problematic issues [34] and varied proposals to cope with their negative effects, as in [11, 39, 44, 51] among others. Our framework deals with unbound wait by outputting at each time point all supported answers (including some that later may prove to be false), as illustrated e.g. in Example 10. Furthermore, if we receive a supported answer whose time parameters are all instantiated, then we immediately have a bound on how long we have to wait until the answer is definite (or rejected).
Blocking queries may still be a problem in our framework, though: as seen in Example 7, blocking operations (in the form of infinitely recursive predicates) may lead to infinite SLD-derivations, which cause the pre-processing step of our algorithm to diverge. We showed that syntactic restrictions of the kind already considered by [46] are guaranteed to avoid blocking queries; Example 8 illustrates that, as in the cited work, these conditions are however not necessary: pre-processing may terminate even though they do not hold.
Our algorithm also implicitly embodies a forgetting algorithm, as the only elements of kept in the sets are those that are still relevant to compute future answers to .
The approaches from [44, 50, 51], which are also specifically Datalog-based, make some restrictions to the form of rules in order to avoid blocking behaviours.
In [51], working in a variant of Datalog called Streamlog, the author characterises sequential rules and programs with the purpose of avoiding blocking behaviour. In particular, the rule from Example 1 is disallowed in this framework, since the timestamp in the head of a rule may never be smaller than the timestamps of the atoms in the body.
The authors of [44] propose the language of forward-propagating queries, yet another variant of Temporal Datalog that allows queries to be answered in polynomial time in the size of the input data. This is again achieved at the cost of disallowing propagation of derived facts towards past time points – once more precluding rule in Example 1. The authors present a generic algorithm to compute answers to a query, given a window size, and investigate methods for calculating a minimal window size.
Memory consumption is a concern in [50], where a sound and complete stream reasoning algorithm is presented for a fragment of datalogMTL – forward-propagating datalogMTL – that also disallows propagation of derived information towards the past. DatalogMTL is a Datalog extension of the Horn fragment of MTL [32, 5], which was proposed in [14] for ontology-based access to temporal log data. DatalogMTL rules allow propagation of derived information to both past and future time points. Concerned with the possibly huge or unbounded set of input facts that have to be kept in memory, the authors of [50] restrict the set of operators of datalogMTL to one that generates only so-called forward-propagating rules. They present a sound and complete algorithm for stream reasoning with forward-propagating datalogMTL that limits memory usage through the use of a sliding window.
More recently, [45] removes these syntactic restrictions on the forms of rules (keeping only the light requirement of temporal guardedness, which is similar to connectedness) and studies fragments of the language for which the existence of a query delay is decidable.
Incomplete information
When reasoning over sources with incomplete information, the concepts of certain and possible answers, and granularities thereof, inevitably arise [20, 26, 33, 43] as a way to assign confidence levels to the information output to the user. These approaches, like ours, also compute answers with incomplete information.
However, our proposal is substantially different from those works, since they focus on answers over past incomplete information. First, as mentioned in Section 2, we assume that our time stream is complete, in the sense that whenever it produces a fact about a time instant , all EDB facts about time instants are already there (in line with the progressive closed world assumption of [51]). Secondly, our hypothetical and supported answers are built over present facts and future, still unknown, hypotheses, and eventually either become effective answers or are discarded; in the scenario of past incomplete information, the confidence level of answers may never change.
Negation
Other authors have considered languages using negation. Our definition of stratification is similar to the concept of temporal stratification from [52]. However, temporal stratification requires the strata to be also ordered according to time (i.e., if the definition of is in and the definition of is in , then ). We make no such assumption in this work.
Beck et al. [10] also consider a notion of temporal stratification for stream reasoning. However, their framework also includes explicit temporal operators, making the whole formalization more complex.
Insofar as we are aware, this is also the first framework for continuous query answering that does not require negation to be safe.
8 Conclusions and future work
We introduced a formalism for dealing with answers to continuous queries that are consistent with the information that is available, but may still need further confirmation from future data. We defined the notions of hypothetical and supported answers declaratively, and showed how they can be computed by means of a variant of SLD-resolution. By refining this idea, we designed a two-phase algorithm whose online component maintains and updates the set of supported answers. Our framework also allows for negation, whose declarative semantics is in line with the progressive closed world assumption.
Our methodology avoids some of the typical problems with delay in continuous query answering. In particular, hypothetical answers allow us to detect that we are not in a situation of unbound wait: if we receive a supported answer whose time parameters are all instantiated, then we immediately have a bound on how long we have to wait until the answer is definite (or rejected). The usefulness of this information is of course application specific. In the situation of Example 9, we could for example take extra preventive measures to ensure that does not become true.
The offline step of our two-phase algorithm may diverge due to issues related to blocking queries. We showed that adequate syntactic restrictions prevent this situation from arising, but that they are not necessary.
For nonrecursive and connected queries without negation, the online step of our algorithm runs in polynomial time. However, it may still be computationally heavy if the sets of hypothetical answers that it needs to compute are large. In particular, pre-processing may produce output that is exponential in the size of the original program. We minimize the impact of this by representing hypothetical answers schematically (since we keep variables uninstantiated), thus limiting the space and time requirements for this algorithm. By adding instantiation constraints to this representation we can also reduce the impact of the exponential blowup introduced by negation. These are informal observations though, which we plan to measure more precisely in a future practical evaluation.
The sets of evidence for hypothetical answers can be used to define a partial order of relative “confidence” of each hypothetical answer. It would be interesting to explore the connection between such notions of confidence and other frameworks of reasoning with multiple truth values.
We also plan to implement our algorithm and evaluate its performance in practice – a first step in this direction, only for the positive fragment of the language, is described in [17]. It would also be interesting to explore approximation techniques for online algorithms in order to allow for unsafe forgetting, with bounds on how many wrong answers may be produced, and to extend our formalism to allow for communication delays, which are present in many interesting practical scenarios.
Acknowledgements
This work was partially supported by the Independent Research Fund Denmark, grant DFF-7014-00041, and by FCT through the LASIGE Research Unit, ref. UIDB/00408/2020 and ref. UIDP/00408/2020.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] 33rd AAAI Conference on Artificial Intelligence, AAAI 2019, Honolulu, Hawaii, USA . AAAI Press, 2019.
- 2[2] Serge Abiteboul, Richard Hull, and Victor Vianu. Foundations of Databases . Addison-Wesley, 1995.
- 3[3] José Júlio Alferes and Luís Moniz Pereira. Reasoning with Logic Programming , volume 1111 of Lecture Notes in Computer Science . Springer, 1996.
- 4[4] Marjan Alirezaie and Amy Loutfi. Automated reasoning using abduction for interpretation of medical signals. J. Biomed. Semant. , 5:35, 2014.
- 5[5] Rajeev Alur and Thomas A. Henzinger. Real-time logics: Complexity and expressiveness. Inf. Comput. , 104(1):35–77, 1993.
- 6[6] Arvind Arasu, Shivnath Babu, and Jennifer Widom. The CQL continuous query language: semantic foundations and query execution. VLDB J. , 15(2):121–142, 2006.
- 7[7] Brian Babcock, Shivnath Babu, Mayur Datar, Rajeev Motwani, and Jennifer Widom. Models and issues in data stream systems. In Lucian Popa, Serge Abiteboul, and Phokion G. Kolaitis, editors, 21st ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, PODS 2002, Madison, Wisconsin, USA , pages 1–16. ACM, 2002.
- 8[8] Davide Francesco Barbieri, Daniele Braga, Stefano Ceri, Emanuele Della Valle, and Michael Grossniklaus. C-SPARQL: SPARQL for continuous querying. In Juan Quemada, Gonzalo León, Yoëlle S. Maarek, and Wolfgang Nejdl, editors, 18th International Conference on World Wide Web, WWW 2009, Madrid, Spain , pages 1061–1062. ACM, 2009.