Commutative Residual Algebra

motivation, decision, and applications


Commutative residual algebras (CRAs) are algebras having an axiomatised residuation operation. Key examples of CRAs are cut-off subtraction (monus) on the natural numbers, set and multiset difference, and cut-off division (dovision) on the positive natural numbers. Here we revisit CRAs, showing the usual construction of a commutative group (the integers) out of a monoid (the natural numbers) as pairs, can be extended and generalised, by constructing the latter from CRAs (the bits) as sequences (up to order), and yielding a commutative lattice-ordered group. This then affords a decision procedure for CRAs, by employing results known from the literature. We show CRAs arise from residual systems (going back to Stark and unpublished work of Plotkin) by imposing a commutativity condition, and we identify residuation as a Skolemised diamond property. Accordingly, we let it together with its associated rewrite technique of tiling take front and centre stage in our approach. We finally show that CRAs are at the natural level of abstraction to state and prove some examples from the literature, in particular the inclusion–exclusion principle, making the latter applicable to, among others, (measurable) multisets.