Information Technology Reference
In-Depth Information
built from function symbols and not just from variables and constants. For ease
of exposition, we do not consider future-time temporal operators.
We call [
ω
t
z.ψ
](
y
;
g
)an
aggregation formula
. It is inspired by the homony-
mous relational algebra operator. Intuitively, by viewing variables as (relation)
attributes,
g
are the attributes on which grouping is performed,
t
is the term on
which the aggregation operator
ω
is applied, and
y
is the attribute that stores
the result. The variables in
z
are
ψ
's attributes that do not appear in the de-
scribed relation. We define the semantics in Section 2.3, where we also provide
examples.
The set of
free variables
of a formula
ϕ
, denoted
fv
(
ϕ
), is defined as expected
for the standard logic connectives. For an aggregation formula, it is defined
as
fv
[
ω
t
z.ϕ
](
y
;
g
)
:=
g
. A variable is
bound
if it is not free. We denote
by
fv
(
ϕ
) the sequence of free variables of a formula
ϕ
that is obtained by ordering
thefreevariablesof
ϕ
by their occurrence when reading the formula from left
to right. A formula is
well-formed
if for each of its subformulas [
ω
t
z.ψ
](
y
;
g
), it
holds that (a)
y
{
y
}∪
∈
g
,(b)
fv
(
t
)
⊆
fv
(
ψ
), (c) the elements of
z
and
g
are pairwise
distinct, and (d)
z
=
fv
(
ψ
)
g
. Note that, given condition (d), the use of one of
the sequences
z
and
g
is redundant. However, we use this syntax to make explicit
the free and bound variables in aggregation formulas. Throughout the paper, we
consider only well-formed formulas.
To omit parenthesis, we assume that Boolean connectives bind stronger than
temporal connectives, and unary connectives bind stronger than binary ones,
except for the quantifiers, which bind weaker than Boolean ones. As syntactic
sugar, we use standard Boolean connectives such as
ϕ
\
∧
ψ
:=
¬
(
¬
ϕ
∨¬
ψ
), the
universal quantifier
∀
x.ϕ
:=
¬∃
x.
¬
ϕ
, and the temporal operators
I
ϕ
:= (
p
∨
¬
and
p
is some predicate symbol of arity 0,
assuming without loss of generality that
R
contains such a symbol. Non-metric
variants of the temporal operators are easily defined, e.g.,
p
)
S
I
ϕ
,
I
ϕ
:=
¬
¬
ϕ
,where
I
∈
I
I
ϕ
:=
[0
,∞
)
ϕ
.
2.3 Semantics
We distinguish between predicate symbols whose corresponding relations are
rigid
over time and those that are
flexible
, i.e., their interpretations can change
over time. We denote by
R
r
and
R
f
the sets of rigid and flexible predicate
symbols, where
R
=
R
r
∪
R
f
with
R
r
∩
R
f
=
∅
. We assume
R
r
contains the
≈
≺
binary predicate symbols
and
, which have their expected interpretation,
namely, equality and ordering.
A
structure
D
over the signature
S
consists of a domain
D
=
∅
and interpre-
tations
f
D
∈
D
ι
(
r
)
,foreach
f ∈
F
and
r ∈
R
.A
temporal
structure
over the signature
S
is a pair (
¯
ι
(
f
)
→
D
and
r
D
⊆
D
¯
D
, τ
), where
D
=(
D
0
,
D
1
,...
)isa
sequence of structures over
and
τ
=(
τ
0
,τ
1
,...
) is a sequence of non-negative
integers, with the following properties.
S
1. The sequence
τ
is monotonically increasing, that is,
τ
i
≤
τ
i
+1
, for all
i
≥
0.
Moreover,
τ
makes progress, that is, for every
τ
∈
N
, there is some index
0 such that
τ
i
>τ
.
2. All structures
i
≥
D
i
, with
i
≥
0, have the same domain, denoted
D
.
