A computational interpretation of compact closed categories: reversible programming with negative and fractional types
A computational interpretation of compact closed categories: reversible programming with negative and fractional types
复制标题
紧凑闭类别的计算解释：负数和分数类型的可逆规划
DOI：
10.1145/3434290
复制
发表时间：
2021
影响因子：
--
通讯作者：
Sabry, Amr
中科院分区：
文献类型：
--
作者：
Chen, Chao-Hong;Sabry, Amr
紧凑的封闭类别包括表示高阶函数的对象，并且是公认的线性逻辑、并发和量子计算模型。我们证明，通过定义对偶和类型（负类型）和对偶乘积类型（分数类型），可以为传统的和和乘积类型构造这种紧凑的封闭类别。受分类语义的启发，我们为负数和分数类型定义了良好的操作语义，其中负数类型表示“反转执行流程”的计算效果，分数类型表示“垃圾收集”特定值或抛出异常的计算效果。具体来说，我们扩展了负数和分数类型的类型同构的一阶可逆语言，指定 每个扩展的操作语义，并证明每个扩展形成一个紧凑的封闭类别。我们还表明，可以使用回溯和异常的标准组合来合并两种操作语义，从而实现负数和分数类型的平滑互操作性。我们通过编写一个可逆 SAT 求解器来说明这种组合的表现力，该求解器使用沿着新分配和取消分配的位置进行回溯搜索。操作语义、大部分元理论属性以及所有示例都在补充的 Agda 包中形式化。
Compact closed categories include objects representing higher-order functions and are well-established as models of linear logic, concurrency, and quantum computing. We show that it is possible to construct such compact closed categories for conventional sum and product types by defining a dual to sum types, a negative type, and a dual to product types, a fractional type. Inspired by the categorical semantics, we define a sound operational semantics for negative and fractional types in which a negative type represents a computational effect that ``reverses execution flow'' and a fractional type represents a computational effect that ``garbage collects'' particular values or throws exceptions.Specifically, we extend a first-order reversible language of type isomorphisms with negative and fractional types, specify an operational semantics for each extension, and prove that each extension forms a compact closed category. We furthermore show that both operational semantics can be merged using the standard combination of backtracking and exceptions resulting in a smooth interoperability of negative and fractional types. We illustrate the expressiveness of this combination by writing a reversible SAT solver that uses backtracking search along freshly allocated and de-allocated locations. The operational semantics, most of its meta-theoretic properties, and all examples are formalized in a supplementary Agda package.
登录
查看更多内容
作为广义基数的欧拉测度
DOI：
--
发表时间：
2002
期刊：
影响因子：
--
作者：
J. Propp
通讯作者：
J. Propp
DOI：
10.1007/978-3-030-33636-3_13
发表时间：
2019
期刊：
Math. Struct. Comput. Sci.
影响因子：
--
作者：
R. Kaarsgaard;Niccolò Veltri
通讯作者：
Niccolò Veltri
对直觉逻辑的某种扩展的代数和克里普克式方法
DOI：
--
发表时间：
1980
期刊：
影响因子：
--
作者：
C. Rauszer
通讯作者：
C. Rauszer
减法逻辑的公式作为类型的解释
影响因子：
0.7
作者：
T. Crolard
通讯作者：
T. Crolard
Pebble 游戏和复杂性
DOI：
--
发表时间：
2013
期刊：
影响因子：
--
作者：
Elchanan Mossel;L. Trevisan;Siu Man Chan
通讯作者：
Siu Man Chan