Inigo Incer and Leonardo Mangeruca and Tiziano Villa and Alberto L. Sangiovanni-Vincentelli

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2020-179

September 1, 2020

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2020/EECS-2020-179.pdf

Seeking the largest solution to an expression of the form A x ≤ B is a common task in several domains of engineering and computer science. This largest solution is commonly called quotient. Across domains, the meanings of the binary operation and the preorder are quite different, yet the syntax for computing the largest solution is remarkably similar. This paper is about finding a common framework to reason about quotients. We only assume we operate on a preorder endowed with an abstract monotonic multiplication and an involution. We provide a condition, called admissibility, which guarantees the existence of the quotient, and which yields its closed form. We call preordered heaps those structures satisfying the admissibility condition. We show that many existing theories in computer science are preordered heaps, and we are thus able to derive a quotient for them, subsuming existing solutions when available in the literature. We introduce the concept of sieved heaps to deal with structures which are given over multiple domains of definition. We show that sieved heaps also have well-defined quotients.

---

BibTeX citation:

@techreport{Incer:EECS-2020-179,
    Author= {Incer, Inigo and Mangeruca, Leonardo and Villa, Tiziano and Sangiovanni-Vincentelli, Alberto L.},
    Title= {The Quotient in Preorder Theories},
    Year= {2020},
    Month= {Sep},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2020/EECS-2020-179.html},
    Number= {UCB/EECS-2020-179},
    Abstract= {Seeking the largest solution to an expression of the form A x ≤ B is a common task in several domains of engineering and computer science. This largest solution is commonly called quotient. Across domains, the meanings of the binary operation and the preorder are quite different, yet the syntax for computing the largest solution is remarkably similar. This paper is about finding a common framework to reason about quotients. We only assume we operate on a preorder endowed with an abstract monotonic multiplication and an involution. We provide a condition, called admissibility, which guarantees the existence of the quotient, and which yields its closed form. We call preordered heaps those structures satisfying the admissibility condition. We show that many existing theories in computer science are preordered heaps, and we are thus able to derive a quotient for them, subsuming existing solutions when available in the literature. We introduce the concept of sieved heaps to deal with structures which are given over multiple domains of definition. We show that sieved heaps also have well-defined quotients.},
}

EndNote citation:

%0 Report
%A Incer, Inigo 
%A Mangeruca, Leonardo 
%A Villa, Tiziano 
%A Sangiovanni-Vincentelli, Alberto L. 
%T The Quotient in Preorder Theories
%I EECS Department, University of California, Berkeley
%D 2020
%8 September 1
%@ UCB/EECS-2020-179
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2020/EECS-2020-179.html
%F Incer:EECS-2020-179