Sparcl: a language for partially-invertible computation
Sparcl: a language for partially-invertible computation
复制标题
Spacl：一种用于部分可逆计算的语言
DOI：
10.1145/3409000
复制
发表时间：
2020
影响因子：
--
通讯作者：
Matsuda K
中科院分区：
文献类型：
--
作者：
Matsuda K
可逆性是计算机科学中的一个基本概念，在软件开发中具有多种表现形式（串行器/解串器、解析器/打印机、重做/撤消、压缩器/解压缩器等）。完全可逆性必然需要双射性，但是组合双射函数来开发可逆程序的直接方法限制太大，无法使用。在本文中，我们采用不同的方法，重点关注部分可逆函数——如果某些参数固定，则函数变得可逆。最简单的例子是加法，当固定操作数之一时，加法变得可逆。更涉及的例子包括基于熵的压缩方法（例如霍夫曼编码），它携带输入符号的出现频率（以某些格式，例如霍夫曼树），固定此频率信息使压缩方法可逆。我们开发了一种语言Sparcl，用于以自然方式编程此类函数，其中部分可逆性是常态，双射性是特殊情况，因此在不影响正确性的情况下获得了显着的表达能力。设计这种语言的挑战是允许普通编程（“部分”部分）与可逆部分自由交互，同时通过构造保证可逆性。 Sparcl 语言是线性类型的，并且具有类型构造函数来区分进行可逆计算的数据和不进行可逆计算的数据。我们展示了该语言的语法、类型系统和语义，并证明 Sparcl 正确保证了其程序的可逆性。我们通过示例展示了 Sparcl 的表达能力，包括从前序和中序遍历重建树以及霍夫曼编码。
Invertibility is a fundamental concept in computer science, with various manifestations in software development (serializer/deserializer, parser/printer, redo/undo, compressor/decompressor, and so on). Full invertibility necessarily requires bijectivity, but the direct approach of composing bijective functions to develop invertible programs is too restrictive to be useful. In this paper, we take a different approach by focusing onpartially-invertiblefunctions—functions that become invertible if some of their arguments are fixed. The simplest example of such is addition, which becomes invertible when fixing one of the operands. More involved examples include entropy-based compression methods (e.g., Huffman coding), which carry the occurrence frequency of input symbols (in certain formats such as Huffman tree), and fixing this frequency information makes the compression methods invertible.We develop a language Sparcl for programming such functions in a natural way, where partial-invertibility is the norm and bijectivity is a special case, hence gaining significant expressiveness without compromising correctness. The challenge in designing such a language is to allow ordinary programming (the “partially” part) to interact with the invertible part freely, and yet guarantee invertibility by construction. The language Sparcl is linear-typed, and has a type constructor to distinguish data that are subject to invertible computation and those that are not. We present the syntax, type system, and semantics of the language, and prove that Sparcl correctly guarantees invertibility for its programs. We demonstrate the expressiveness of Sparcl with examples including tree rebuilding from preorder and inorder traversals and Huffman coding.
登录
查看更多内容
线性时间可逆自解释器
DOI：
--
发表时间：
2015
期刊：
影响因子：
--
作者：
横山哲郎;ロバートグリュック
通讯作者：
ロバートグリュック
命运的逆转 - 垃圾收集的热力学
DOI：
10.1007/bfb0017210
发表时间：
1992
期刊：
J. Multiple Valued Log. Soft Comput.
影响因子：
--
作者：
H. Baker
通讯作者：
H. Baker
Sparcl 的原型实现和证明脚本：部分可逆计算语言
影响因子：
--
作者：
Kazutaka Matsuda;Meng Wang
通讯作者：
Meng Wang
DOI：
--
发表时间：
2005
期刊：
IEICE Trans. on Information and Systems(in Japanese) Vol.J88-D-I, No.8
影响因子：
--
作者：
Naoki Nishida;Masahiko Sakai;Toshiki Sakabe
通讯作者：
Toshiki Sakabe
影响因子：
0.6
作者：
Capretta, Venanzio
通讯作者：
Capretta, Venanzio