Theseus : A High Level Language for Reversible Computing
Theseus : A High Level Language for Reversible Computing
复制标题
Theseus：可逆计算的高级语言
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Roshan P. James
中科院分区：
文献类型：
--
作者：
Roshan P. James
用可逆语言编程仍然与传统的不可逆语言编程“不同”，需要专门的抽象和独特的思维模式。我们提出了一个高级语言的可逆编程，称为忒修斯，自然与传统的编程语言抽象的网格。Theseus具有传统函数式语言的外观和感觉，同时与基于类型同构的低级语言家族保持密切的对应关系[9]。与图灵机的无点组合子不同，忒修斯有变量和绑定形式，代数数据类型，通过模式匹配定义函数，并且是图灵完备的。该语言是强类型的，所有类型良好的程序都是可逆的。我们解释的语义忒修斯通过收集逐步表达的例子，并概述其对应的。
Programming in a reversible language remains “different” than programming in conventional irreversible languages, requiring specialized abstractions and unique modes of thinking. We present a high level language for reversible programming, called Theseus, that meshes naturally with conventional programming language abstractions. Theseus has the look and feel of a conventional functional language while maintaining a close correspondence with the low-level family of languages Π based on type isomorphisms [9]. In contrast to the point-free combinators of Π , Theseus has variables and binding forms, algebraic data types, function definitions by pattern matching, and is Turing complete. The language is strongly typed and all well-typed programs are reversible. We explain the semantics of Theseus via a collection of progressively expressive examples and outline its correspondence to Π .