Lossless compression implementations typically contain two programs, an encoder and a decoder, which are required to be inverse to one another. We observe that a significant class of compression methods, based on asymmetric numeral systems (ANS), have shared structure between the encoder and decoder -- the decoder program is the 'reverse' of the encoder program -- allowing both to be simultaneously specified by a single, reversible function. To exploit this, we have implemented a small reversible language, embedded in Agda, which we call 'Flipper' (available at https://github.com/j-towns/flipper). Agda supports formal verification of program properties, and the compiler for our reversible language (which is implemented as an Agda macro), produces not just an encoder/decoder pair of functions but also a proof that they are inverse to one another. Thus users of the language get formal verification 'for free'. We give a small example use-case of Flipper in this paper, and plan to publish a full compression implementation soon.
翻译：无损压缩执行通常包含两个程序, 一个编码器和一个解码器, 它们必须相互反向。 我们观察到, 大量基于非对称数字系统( ANS) 的压缩方法在编码器和解码器之间有共同的结构 -- 解码器程序是编码器程序的“ 反向 ”, 允许同时用一个可逆的单函数来指定两者。 要利用这个功能, 我们已采用了一个小的可逆语言, 嵌入了Agda, 我们称之为“ Flipper ” (可查阅 https://github.com/j-towns/flipper ) 。 Agda 支持对程序属性进行正式核查, 以及我们可变语言的编译器( 作为 Agda 宏执行), 不仅产生一个编码器/ decoder 函数的“ 反向”, 还能证明它们相互反向。 因此, 语言的用户可以免费获得正式的验证 。 我们举了一个小的例子, 。 我们用 Flipper 在本文中用一个小的例子, 并计划很快公布一个完整的压缩执行 。
相关内容
微信扫码咨询专知VIP会员