Information Technology Reference
In-Depth Information
The state at time point
i
, that is, after the procedure
eval
(
ϕ,i,τ
i
,Γ
i
)has
been executed, consists of the list
L
ϕ
of tuples (
τ
j
,R
j
) ordered with
j
ascending,
where
j
is such that
j
≤
i
and
τ
i
−
τ
j
<b
and where
D
,τ,j
)
s,C
j<k≤i
ψ
D
,τ,k
)
,
(
¯
(
¯
R
j
:=
ψ
with
s
and
C
defined as in Section 3.3. We have
D
,τ,i
)
=
j≤i,τ
i
−τ
j
∈I
R
j
.
The computation of this union is performed in the last line of the
eval since
procedure. Note that, in general, not all the relations
R
j
in the list
L
ϕ
are
needed for the evaluation of
ϕ
at time point
i
. However, the relations
R
j
with
j
such that
τ
i
−
(
¯
ϕ
τ
j
∈
I
,thatis
τ
i
−
τ
j
<a
, are stored for the evaluation of
ϕ
at
future time points
i
>i
.
We now explain how the state is updated at time point
i
from the state at time
point
i
1. We first drop from the list
L
ϕ
the tuples that are not longer relevant.
More precisely, we drop the tuples that have as first component a timestamp
τ
j
for which the distance to the current timestamp
τ
i
is too large with respect to
the right margin of
I
. This is done by the procedure
drop old
. Next, the state is
updated according to the logical equivalence
α
S
β
−
β
.This
is done in two steps. First, we update each element of
L
ϕ
so that the tuples in the
stored relations also satisfy
ψ
at the current time point
i
. This step corresponds to
the conjunction in the above equivalence and it is performed by the
map
function.
The update is based on the equality
R
j
=
R
i−
j
s,C
≡
(
α
∧
(
α
S
β
))
∨
(
¯
D
,τ,i
)
. Note that the
join distributes over the intersection. The second step, which corresponds to
the disjunction in the above equivalence, consists of appending the tuple (
τ
i
,R
i
)
to
L
ϕ
.Notethat
R
i
=
ψ
(
¯
D
,τ,i
)
.
Finally, we note that the proof of Theorem 6 follows the above presentation
of the algorithm, and is done by induction using the lexicographic ordering on
tuples (
i,
ψ
denotes
ϕ
's size, defined as expected. Further-
more, the proof of Lemma 5 is straightforward. It follows by induction on the
formula structure and from the equalities given in Section 3.3, as each relational
algebra operator produces a finite relation when applied to finite relations.
|
ϕ
|
), where
i
∈
N
and
|
ϕ
|
