Succinct ordering and aggregation constraints in algebraic array theories
We discuss two extensions to a recently introduced theory of arrays, which are based on considerations coming from the model theory of power structures. First, we discuss how the ordering relation on the index set can be expressed succinctly by referring to arbitrary Venn regions. Second, we show how to add general aggregators to the calculus. The result is a logic that subsumes four previous fragments discussed in the literature and is distinct from array fold logic, in that it can express summations, while its satisfiability problem remains in non -deterministic polynomial time.
1-s2.0-S2352220824000324-main.pdf
publisher
openaccess
CC BY
942.77 KB
Adobe PDF
3a6316219bbf682b0d6ebd5dc7d46587