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 |
---|---|---|
AGG |
|
|
CARD |
|
Syntax
FO[Agg] adds these production rules:
Base ← CARD '{' Quantee {',' Quantee} ':' Expression '}';
Base ← AGG '(' 'lambda' Quantee {',' Quantee} ':' Expression ')';
flowchart LR
subgraph Base
direction LR
start{ } --> CARD;
CARD --> lp["'{'"];
lp --> Quantee([Quantee]);
Quantee --> commaQ["','"];
commaQ --> Quantee;
Quantee --> colon["':'"];
colon --> Expression([Expression]);
Expression --> rp["'}'"];
rp --> endB{ };
start{ } --> AGG;
AGG --> lp2["'('"];
lp2 --> lambda["'lambda'"];
lambda --> Quantee2([Quantee]);
Quantee2 --> comma2["','"];
comma2 --> Quantee2;
Quantee2 --> colon2["':'"];
colon2 --> Expression2([Expression]);
Expression2 --> rp2["'('"];
rp2 --> endB{ };
end;
Well-formedness
in
CARD{x∈T: φ)}
,φ
must be a boolean expression.in
AGG(lambda x∈T: φ)
,φ
must be a number expression.
Semantics
#{x∈T: φ}
is the cardinality of the set of elementsx
inT
that makeφ
true.sum(lambda x∈T: φ)
is the sum ofφ
for eachx
inT
.
Example
c() = #{x∈T: p(x)}.
[The perimeter is the sum of the lengths of the sides]
perimeter() = sum(lambda n ∈ Side_Nr : length(n)).
FO(Agg) abstract language
The formal semantics of FO(Agg) is described in [DPB01].