Information Technology Reference
In-Depth Information
2 MFOTL with Aggregation Operators
2.1 Preliminaries
We use standard notation for sets and set operations. We also use set notation
with sequences. For instance, for a set
A
and a sequence
s
=(
s
1
,...,s
n
), we
write
A
∪
s
for the union
A
∪{
s
i
|
1
≤
i
≤
n
}
and we denote the length of
s
by
|
s
|
.Let
I
be the set of nonempty intervals over
N
. We often write an interval
as [
b,b
):=
a<b
}
,
b
∈
N
∪{∞}
,and
b<b
.
in
I
{
a
∈
N
|
b
≤
,where
b
∈
N
.Thisdefi-
nition extends the standard one to multi-sets where elements can have an infi-
nite multiplicity. A multi-set is
finite
if
M
(
a
)
A
multi-set
M
with domain
D
is a function
M
:
D
→
N
∪{∞}
∈
N
for any
a
∈
D
and the set
{
a
∈
D
|
M
(
a
)
>
0
}
{|
|}
is finite. We use the brackets
and
to specify multi-sets.
{|
·
n/
2
|
n
∈
N
|}
denotes the multi-set
M
:
N
→
N
∪{∞}
For instance,
2
with
M
(
n
)=2if
n
is even and
M
(
n
)=0otherwise.
An
aggregation operator
is a function from multi-sets to
Q
∪{⊥}
such
that finite multi-sets are mapped to elements of
Q
and infinite multi-
sets are mapped to
⊥
. Common examples are
CNT
(
M
):=
a∈D
M
(
a
),
SUM
(
M
):=
a∈D
M
(
a
)
·
a
,
MIN
(
M
):=min
{
a
∈
D
|
M
(
a
)
>
0
}
,
MAX
(
M
):=max
{
a
∈
D
|
M
(
a
)
>
0
}
,and
AVG
(
M
):=
SUM
(
M
)
/
CNT
(
M
)
if
CNT
(
M
)
is a finite
multi-set. We assume that the given aggregation operators are only applied over
the multisets with the domain
=0and
AVG
(
M
) := 0 otherwise, where
M
:
D
→
N
∪{∞}
Q
.
2.2 Syntax
A
signature
is a tuple (
F
,
R
,ι
), where
F
is a finite set of function symbols,
R
is
a finite set of predicate symbols disjoint from
F
, and the function
ι
:
F
S
∪
R
→
N
assigns to each symbol
s
∈
F
∪
R
an arity
ι
(
s
). In the following, let
S
=(
F
,
R
,ι
)
be a signature and
V
a countably infinite set of variables, where
V
∩
(
F
∪
R
)=
∅
.
Function symbols of arity 0 are called
constants
.Let
C
⊆
F
be the set of
S
S
constants of
are defined inductively: Constants and variables
are terms, and
f
(
t
1
,...,t
n
)isatermif
t
1
,...,t
n
are terms and
f
is a function
symbol of arity
n>
0. We denote by
fv
(
t
) the set of the variables that occur in
the term
t
.Wedenoteby
T
the set of all terms over
S
,andby
T
∅
the set of
ground terms. A
substitution
θ
is a function from variables to terms. We use the
same symbol
θ
to denote its homomorphic extension to terms.
Given a finite set
Ω
of aggregation operators, the MFOTL
Ω
formulas
over
the signature
.
Terms
over
S
are given by the grammar
ϕ
::=
r
(
t
1
,...,t
ι
(
r
)
)
|
(
¬
ϕ
)
|
(
ϕ
∨
ϕ
)
|
(
∃
x.ϕ
)
|
(
I
ϕ
)
|
(
ϕ
S
I
ψ
)
|
[
ω
t
z.ϕ
](
y
;
g
)
,
where
r
,
t
and the
t
i
s,
I
,and
ω
range over the elements in
R
,
T
,
,and
Ω
,
respectively,
x
and
y
range over elements in
V
,and
z
and
g
range over sequences
of elements in
V
. Note that we overload notation:
ω
denotes both an aggregation
operator and its corresponding symbol. This grammar extends MFOTL's [20] in
two ways. First, it introduces aggregation operators. Second, terms may also be
I
