论文标题
预订理论中的商
The Quotient in Preorder Theories
论文作者
论文摘要
在工程和计算机科学的几个领域中，寻求最大的解决方案是x <= b的表达是一项常见的任务。这个最大的解决方案通常称为商。在整个领域，二进制操作和预订的含义完全不同，但是用于计算最大解决方案的语法非常相似。本文是关于找到一个通用框架来推理商的框架。我们仅假设我们在具有抽象单调乘法和不同步的预订上运行。我们提供了一种称为可接受性的条件，可以保证商的存在，并产生其封闭形式。我们称预订的那些结构满足可接纳性条件。我们表明，计算机科学中的许多现有理论都是预订的堆，因此我们能够为它们提供商品，并在文献中获得现有的解决方案。我们介绍了筛分堆的概念，以处理对定义多个领域的结构。我们表明，筛分堆也有明确的商。
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.
