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.
Cite this item
Raya, R., & Kuncak, V. (2024). Succinct ordering and aggregation constraints in algebraic array theories. Journal of Logical and Algebraic Methods in Programming, 140, Article 100978. https://doi.org/10.1016/j.jlamp.2024.100978
Click Copy to copy the citation, or select the text manually.
1-s2.0-S2352220824000324-main.pdf
Publisher
Published version
openaccess
CC BY
942.77 KB
Adobe PDF
3a6316219bbf682b0d6ebd5dc7d46587