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

sum|min|max

CARD

#|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

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

  2. in AGG(lambda x∈T: φ), φ must be a number expression.

Semantics

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

  2. sum(lambda x∈T: φ) is the sum of φ for each x in T.

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].