分数类型：辅助钻头的表达和安全空间管理
Fractional Types: Expressive and Safe Space Management for Ancilla Bits
摘要：
在可逆计算中，空间的管理受到两大类约束。首先，与通用计算一样，每个分配都必须与匹配的解分配配对。其次，只有当空间的内容从分配时恢复到初始值时，空间才能安全地解除分配。一般来说，现有技术提供了有限的部分解决方案，其通过施加堆栈规程并通过将第二约束留给程序员的断言来解决第一约束。我们提出了一种新的方法，基于分数类型的想法。作为一个简单直观的示例，分配一个初始化为$\texttt{false}$的新布尔值也会创建一个值$1/{\texttt{false}}$，该值可被视为专门回收且仅回收包含值$\texttt{false}$的存储的垃圾回收（GC）进程。这个GC流程是一个一流的实体，可以被操作、分解成更小的流程并与其他GC流程组合。我们形式化这个想法的上下文中的可逆的语言建立在类型同构，证明其基本的正确性，并说明其表现力使用各种各样的例子。开发得到了完全正式的Agda实施的支持。
英文摘要：
In reversible computing, the management of space is subject to two broad classes of constraints. First, as with general-purpose computation, every allocation must be paired with a matching de-allocation. Second, space can only be safely de-allocated if its contents are restored to their initial value from allocation time. Generally speaking, the state of the art provides limited partial solutions that address the first constraint by imposing a stack discipline and by leaving the second constraint to programmers' assertions. We propose a novel approach based on the idea of fractional types. As a simple intuitive example, allocation of a new boolean value initialized to $\texttt{false}$ also creates a value $1/{\texttt{false}}$ that can be thought of as a garbage collection (GC) process specialized to reclaim, and only reclaim, storage containing the value $\texttt{false}$. This GC process is a first-class entity that can be manipulated, decomposed into smaller processes and combined with other GC processes. We formalize this idea in the context of a reversible language founded on type isomorphisms, prove its fundamental correctness properties, and illustrate its expressiveness using a wide variety of examples. The development is backed by a fully-formalized Agda implementation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
