FO[Agg]¶
Goal
The goal of FO[Agg] is to allow expressing knowledge about the size (aka cardinality) of a set,
as well as aggregates (sum
, min
, and max
).
This extension extends FO[Int] and/or FO[Real].
Lexicon
Token 
Pattern 
Example 

CARD 


MIN 


SUM 

Syntax
FO[Agg] adds these production rules:
Base ← CARD '{' Quantee {',' Quantee} [ ':' Expression ] '}';
Base ← MIN '{' Expression '' Quantee {',' Quantee} [ ':' Expression ] '}';
Base ← SUM '{{' Expression '' Quantee {',' Quantee} [ ':' Expression ] '}}';
Wellformedness
in
CARD{ x∈T : φ }
,φ
must be a boolean expression.in
MIN{ t  x∈T: φ }
,t
must be a numeric term, andφ
a boolean expression.in
SUM{{ t  x∈T: φ }}
,t
must be a numeric term, andφ
a boolean expression.the variables in
t
andφ
must bex
or declared in a outer quantification or aggregation.
Semantics
#{ x∈T: φ }
is the cardinality of the set of elementsx
inT
that makeφ
true.min{ t  x∈T: φ }
is the minimum oft
for eachx
inT
such thatφ
is true.sum{{ t  x∈T: φ }}
is the sum oft
for eachx
inT
such thatφ
is true.
Example
c() = #{x∈T: p(x)}.
[The perimeter is the sum of the lengths of the sides]
perimeter() = sum{{ length(n)  n ∈ Side_Nr }}.
FO(Agg) abstract language
The formal semantics of FO(Agg) is described in [DPB01].