Aggregates: count and exists in rule bodies

Area: Rules, aggregates & recursion Teaches: the aggregate forms exists { B } and count { B } cmp N inside a derive body — a subquery whose cardinality (or mere non-emptiness) drives the head. Aggregation is part of the rule language, not a separate report step. Prerequisites: concepts and <: specialization, and derive rule bodies (see first-class relations). Run: ox build examples/aggregate_count_v0 && ox derive examples/aggregate_count_v0 <predicate>

A data language that cannot count inside a rule pushes every cardinality question out to application code. Argon admits an aggregate atom as a subquery in the body: exists { B } is true when B has any solution, and count { B } yields the number of solutions so a comparison atom can filter on it.

What to read in company.ar

The corpus is three people, one of them a manager:

pub fact Person(alice);
pub fact Person(bob);
pub fact Person(carol);
pub fact Manager(alice);

exists { B } is a bare Boolean — the head fires iff the body has at least one solution:

pub derive any_person()  :- exists { Person(p) };
pub derive any_manager() :- exists { Manager(p) };

count { B } cmp N compares the cardinality. The aggregate binds the count to a synthesized variable; the comparison atom is the filter:

pub derive at_least_three_persons() :- count { Person(p) } >= 3;
pub derive thin_management()        :- count { Manager(p) } < 2;
pub derive huge_company()           :- count { Person(p) } >= 100;

These heads are 0-ary: each is a propositional flag that either fires or does not.

Running it

ox derive <predicate> prints the derived tuples. A 0-ary head that fires returns exactly one tuple — the empty tuple (); one that does not fire returns none:

derive(any_person):              1 tuple(s)   ()   — three Persons exist
derive(any_manager):             1 tuple(s)   ()   — alice is a Manager
derive(at_least_three_persons):  1 tuple(s)   ()   — count{Person} = 3, so >= 3 holds
derive(thin_management):         1 tuple(s)   ()   — count{Manager} = 1, so < 2 holds
derive(huge_company):            0 tuple(s)        — count{Person} = 3, so >= 100 fails

The decisive contrast is at_least_three_persons vs huge_company: the same count { Person(p) } subquery (which evaluates to 3) yields opposite verdicts because the threshold differs. The count is computed inside the rule, not handed to the rule.

Honest caveats (what runs today)

• v0 admits count (and bare exists) with the comparison operators ==, !=, <, <=, >, >=. The comprehension form (sum(expr for x in S where φ)), aggregators beyond count / count_distinct, and nested aggregates are γ follow-ons of RFD 0011.
• A 0-ary head models a proposition: one tuple means true, zero tuples means false. The single tuple is the empty tuple ().
• This package builds and runs under ox; unlike its sibling aggregate_membership_join it is not yet pinned by a corpus test, so it documents the surface rather than a regression.

Source

The package’s real Argon source, transcluded from the files this corpus compiles — what you read here is exactly what CI builds.

root.ar

//! Aggregates v0.1 — `count { atoms }` / `exists { atoms }`
//! demo. Phase γ closes one of the last open substrate audit
//! walls (RFD 0011); this example exercises the end-to-end
//! pipeline: surface syntax → SUBQUERY_EXPR CST → AtomIR::
//! Aggregate → CompiledAtom::Aggregate → executor.
//!
//! v0.1 scope:
//!
//!   * `count { B }` — cardinality of solutions to B (binds
//!     to a result var when followed by a comparison).
//!   * `exists { B }` — bare-form Boolean (truthy iff B has
//!     any solution).
//!   * Comparison forms: `count { B } cmp N` for `==`, `!=`,
//!     `<`, `<=`, `>`, `>=`.
//!
//! Deferred (RFD 0011 / γ follow-ons):
//!
//!   * Comprehension form `sum(expr for x in S where φ)`.
//!   * Truth4 interval semantics under OWA.
//!   * Aggregators other than `count` / `count_distinct`.
//!   * Nested aggregates (OE1311).

mod company;

company.ar

//! `company` — a small employment ontology with aggregate
//! queries over the workforce.

pub type Person;
pub type Manager <: Person;

pub fact Person(alice);
pub fact Person(bob);
pub fact Person(carol);
pub fact Manager(alice);

// ANCHOR: aggregates
/// Truthy iff there is at least one Person in the catalog.
/// Uses bare-`exists` form; the result is a Boolean atom.
pub derive any_person() :- exists { Person(p) };

/// Truthy iff there are at least three Persons.
/// Comparison form: the aggregate binds the cardinality to a
/// synthesized variable; the paired comparison atom filters.
pub derive at_least_three_persons() :- count { Person(p) } >= 3;
// ANCHOR_END: aggregates
/// Truthy iff there is at least one Manager.
pub derive any_manager() :- exists { Manager(p) };

/// Truthy iff the workforce has fewer than two Managers.
pub derive thin_management() :- count { Manager(p) } < 2;

/// Negative case: 100+ persons; should NOT fire on this corpus.
pub derive huge_company() :- count { Person(p) } >= 100;