Information Technology Reference
In-Depth Information
3. Function symbols and rigid predicate symbols have rigid interpretations, that
is,
f
D
i
=
f
D
i
+1
and
p
D
i
=
p
D
i
+1
, for all
f
∈
F
,
p
∈
R
r
,and
i
≥
0. We also
write
f
D
and
p
D
for
f
D
i
and
p
D
i
, respectively.
We call the elements in the sequence
τ
timestamps
and the indices of the elements
in the sequences
¯
and
τ
time points
.
A
valuation
is a mapping
v
:
V
D
→
D
. For a valuation
v
, the variable sequence
x
=(
x
1
,...,x
n
), and
d
=(
d
1
,...,d
n
)
d
] for the valuation
n
,wewrite
v
[
x
∈
D
→
n
, and the other variables' valuation is unaltered.
We abuse notation by also applying a valuation
v
to terms. That is, given a
structure
that maps
x
i
to
d
i
,for1
≤
i
≤
,weextend
v
homomorphically to terms.
For the remainder of the paper, we fix a countable domain
D
D
with
Q
∪{⊥}⊆
D
.
We only consider a single-sorted logic. One could alternatively have sorts for the
different types of elements like data elements and the aggregations. Furthermore,
note that function symbols are always interpreted by total functions. Partial func-
tions like division over scalar domains can be extended to total functions, e.g.,
by mapping elements outside the function's domain to
⊥
.Sincethetreatment
of partial functions is not essential to our work, we treat
⊥
as any other element
D
of
. Alternative treatments are, e.g., based on multi-valued logics [21].
Definition 1.
Let
(
¯
D
, τ
)
be a temporal structure over the signature
S
,with
¯
D
=(
D
0
,
D
1
,...
)
and
τ
=(
τ
0
,τ
1
,...
)
,
ϕ
a formula over
S
,
v
a valuation,
.Wedefinetherelation
(
¯
and
i
∈
N
D
, τ,v,i
)
|
=
ϕ
inductively as follows:
=
p
(
t
1
,...,t
ι
(
r
)
)
iff
v
(
t
1
)
,...,v
(
t
ι
(
r
)
)
∈
(
¯
p
D
i
D
, τ,v,i
)
|
(
¯
iff
(
¯
D
, τ,v,i
)
|
=
¬
ψ
D
, τ,v,i
)
|
=
ψ
(
¯
iff
(
¯
=
ψ
or
(
¯
ψ
=
ψ
D
, τ,v,i
)
|
=
ψ
∨
D
, τ,v,i
)
|
D
, τ,v,i
)
|
(
¯
iff
(
¯
D
, τ,v,i
)
|
=
∃
x.ψ
D
, τ,v
[
x
→
d
]
,i
)
|
=
ψ
,forsome
d
∈
D
(
¯
I,
and
(
¯
D
, τ,v,i
)
|
=
I
ψ
iff
i>
0
,τ
i
−
τ
i−
1
∈
D
, τ,v,i
−
1)
|
=
ψ
(
¯
I,
(
¯
=
ψ
S
I
ψ
=
ψ
,
D
, τ,v,i
)
|
iff for some
j
≤
i, τ
i
−
τ
j
∈
D
, τ,v,j
)
|
and
(
¯
D
, τ,v,k
)
|
=
ψ,
for all
k
with
j<k
≤
i
(
¯
D
, τ,v,i
)
|
=[
ω
t
z.ψ
](
y
;
g
)
iff
v
(
y
)=
ω
(
M
)
,
where
M
:
D
→
N
∪{∞}
is the multi-set
v
[
z
d
](
t
)
(
¯
∈
D
|z|
.
d
]
,i
)
=
ψ,
for some
d
→
D
, τ,v
[
z
→
|
Note that the semantics for the aggregation formula is independent of the order
of the variables in the sequence
z
.
For a temporal structure (
¯
D
, τ
), a time point
i
∈
N
,aformula
ϕ
, a valuation
v
,
and a sequence
z
of variables with
z
⊆
fv
(
ϕ
), we define the set
(
¯
D
,τ,i
)
z,v
d
(
¯
d
]
,i
)
∈
D
|z|
|
ϕ
{
D
, τ,v
[
z
→
|
=
ϕ
}
.
:=
We drop the superscript when it is clear from the context. We drop the subscript
when
z
=
fv
(
ϕ
). Note that in this case the valuation
v
is irrelevant and
(
¯
D
,τ,i
)
ϕ
denotes the set of satisfying elements of
ϕ
at time point
i
in (
¯
, τ
).
With this notation, we illustrate the semantics for aggregation formulas in
the case where we aggregate over a variable. We use the same notation as in
D
