Struct Semilattice 

pub struct Semilattice {
    pub idempotent: bool,
    pub commutative: bool,
    pub associative: bool,
    pub monotone_join: bool,
    pub has_top: bool,
}

Lattice properties of an aggregate.

Used by the Locy fixpoint engine to verify monotonicity and prove termination. The flags are not independent: monotone_join typically implies commutative and associative.

Fields

idempotent: bool

f(x, x) == x. Idempotent aggregates can deduplicate inputs.

commutative: bool

f(x, y) == f(y, x). Commutative aggregates are order-independent.

associative: bool

f(f(x, y), z) == f(x, f(y, z)). Associative aggregates can be partial-aggregated.

monotone_join: bool

f preserves or raises the partial order. Monotone aggregates produce sound fixpoints; non-monotone ones cannot be used inside recursive Locy clauses.

has_top: bool

Bounded domain — is_at_top() may return true. Enables fixpoint shortcuts (no further ingest can change the state).

Implementations

impl Semilattice

pub const NON_MONOTONE: Self

Properties of a non-monotone aggregate (SUM, AVG).

Such aggregates may not appear inside recursive Locy clauses.

pub const BOUNDED_MIN_MAX: Self

Properties of MIN / MAX over a bounded domain — fully monotone.

pub const COUNT: Self

Properties of COUNT — monotone but unbounded.

Trait Implementations

impl Clone for Semilattice

fn clone(&self) -> Semilattice

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Copy for Semilattice

impl Debug for Semilattice

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for Semilattice

impl PartialEq for Semilattice

fn eq(&self, other: &Semilattice) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for Semilattice