Sparcl: A language for partially-invertible computation

Kazutaka Matsuda, Meng Wang

研究成果: Article査読

2 被引用数 (Scopus)


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 on partially-invertible functions - 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.

ジャーナルProceedings of the ACM on Programming Languages
出版ステータスPublished - 2020 8月 2

ASJC Scopus subject areas

  • ソフトウェア
  • 安全性、リスク、信頼性、品質管理


「Sparcl: A language for partially-invertible computation」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。