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	#|CARD
MIN	min|max
SUM	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 ] '}}';

flowchart LR subgraph Base direction LR start{ } --> CARD; CARD --> lp["'{'"]; lp --> Quantee([Quantee]); commaQ --> Quantee; Quantee --> colon["':'"]; Quantee --> commaQ["','"]; Quantee --> rp; colon --> Expression([Expression]); Expression --> rp["'}'"]; rp --> endB{ }; start{ } --> MIN; MIN --> lp2["'{'"]; lp2 --> Expression3([Expression]); Expression3 --> mid["'|'"]; mid --> Quantee; start{ } --> SUM; SUM --> lp3["'{{'"]; lp3 --> Expression3; Expression --> rp2["'}}'"]; rp2 --> endB{ }; end;

Well-formedness

1. in CARD{ x∈T : φ }, φ must be a boolean expression.

2. in MIN{ t | x∈T: φ }, t must be a numeric term, and φ a boolean expression.

3. in SUM{{ t | x∈T: φ }}, t must be a numeric term, and φ a boolean expression.

4. the variables in t and φ must be x or declared in a outer quantification or aggregation.

Semantics

1. #{ x∈T: φ } is the cardinality of the set of elements x in T that make φ true.

2. min{ t | x∈T: φ } is the minimum of t for each x in T such that φ is true.

3. sum{{ t | x∈T: φ }} is the sum of t for each x in T 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].