可逆编程语言相关理论及实践研究

摘要：从编程语言的角度研究了可逆计算。首先，给出可逆编程语言流程图的3种基本结构，从而构建一个可逆编程语言的可视模型；其次，证明可逆语言的可逆图灵机完备性，进而论证其与传统编程语言在计算能力上的一致性；最后，介绍了可逆编程语言Janus并进行了编程实践。

关键词关键词：可逆计算；可逆编程语言；流程图；图灵机；图灵完备

DOIDOI：10.11907/rjdk.1431017

中图分类号：TP314

文献标识码：A文章编号文章

编号：16727800（2015）002006204

基金项目基金项目：南通理工学院校级科研项目（2014002）

作者简介作者简介：卫丽华（1984-），女，江苏南通人，硕士，南通理工学院软件工程系讲师，研究方向为可逆计算。

0引言

可逆计算作为一个新兴学科，对未来计算机的持续发展起着决定性的作用。自20世纪60年代以来，计算机硬件一直遵循着Moore定律＼[1＼]高速发展，但这种发展趋势预计会在2020年左右终结＼[2＼]，主要原因如下：单位面积器件数量的增加，会导致产生的热量超出芯片能承受的极限。R·landauer最早考虑了能耗导致计算机芯片发热的问题＼[3＼]，他指出能耗来源于计算过程中的不可逆操作，因此采用可逆计算可以大大降低计算机的能耗。可逆计算主要关注两个方面：物理可逆和逻辑可逆，R.Landauer在文献＼[3＼]中证明，如果一个计算过程物理可逆，那么该过程须同时逻辑可逆。一个计算过程如果不仅能从输入状态得到输出状态（正向），并且能从输出状态唯一确定输入状态（反向），那么该计算过程便是逻辑可逆的。

当今流行的计算机（RAM机或图灵机）都是逻辑不可逆的，因为它们在计算过程中会销毁或丢失信息，从而不能回推前状态。Landauer认为通过保存运算过程中的历史信息，可以将不可逆性通过逆向跟踪程序流程图得到。本文根据传统程序流程图的3种基本结构，将一个不可逆运算转变成可逆运算，引入额外信息通过反向运算清除＼[4＼]。理论上讲，只要存储空间足够，任何不可逆计算都可以转换成可逆计算。目前已经出现了一些可逆计算模型，比如可逆图灵机＼[4＼]和可逆细胞自动机＼[5＼]，但针对较高逻辑层级的软件（即编程语言）进行的研究还比较欠缺。

各种流行的程序设计语言，如C++、Java等均是完备的图灵机＼[67＼]，即可将其视为一个特殊的图灵机。鉴于一般图灵机的不可逆性，这些编程语言也是不可逆的。另外，对传统编程语言进行改造，使得改进后的结构既可以正向执行又可以反向跟踪，从而构建可逆编程的可视模型。本文对可逆编程语言Janus＼[8＼]作了介绍，并给出了示例代码。

1可逆编程流程

目前流行的传统程序语言均是不可逆的，即不能确保从输出状态获得输入状态，这从程序流程图上就可以看出（见图1），在流程图中的有些分支汇聚点是没有判定条件的，这就导致了反向执行流程时，不知道该跟踪哪个分支。此外，不强制要求每个单步操作（对应流程图中的处理框）可逆也是导致传统程序语言不可逆的原因之一。传统语言的基本结构（顺序结构、选择结构和循环结构）都存在上述问题，通过对传统程序流程图进行扩展可以解决上述不可逆问题。

扩展的可逆程序流程图＼[9＼]包含以下3个基本元素（见图2）：单步操作、判定、断言。其中“单步操作”必须是一个可逆操作，即可以由输出唯一确定输入，如x=y，由于x值被y所覆盖无法再恢复，所以是不可逆的，可以用x=x x or y这样的可逆形式取代前者；“判定”根据内部条件的取值（真或假）执行不同分支；“断言”则根据内部条件的不同取值接受不同分支，如取真时，接受分支t，取假，接受分支f。“判定”和“断言”都包含一个内部判断条件，但是前者是流程图中的发散点，而后者是汇聚点，两者在程序正向执行和逆向跟踪时进行相互转换。此3个基本元素可以构成可逆程序流程图的3种基本控制结构。

1.1可逆顺序结构

在传统顺序结构的基础上，保证每个单步操作的局部可逆性就得到可逆的顺序结构（见图3）。局部可逆性解释如下：将单步操作a看作一个状态变换函数，当且仅当存在和上下文无关（即和在流程图中的所处位置无关）的反函数a-1时，称a为局部可逆的。关于局部可逆在文献＼[11＼]中有详细介绍。

图3可逆顺序结构

1.2可逆选择结构

传统的ifthenelse选择结构包括两部分：一个判定条件，两个分支。可逆选择结构在此基础上在分支汇聚点加上断言c2，结构见图4。反向执行时，判定c1变成断言c1，断言c2变成判定c2。

图4可逆选择结构

1.3可逆循环结构

传统循环结构包含两个部分：循环判定条件、循环体。可逆循环结构如图5所示，包含3个部分：断言c1、两个操作序列A和B、循环判定条件c2，当A为空时对应while循环，当B为空时，对应dowhile循环。

图5可逆循环结构

从图3、图4及图5可知，由可逆程序流程图得到反向图是件很容易的事情，主要包含以下几个步骤：①改变流程线的箭头方向；②用a-1代替单步操作a；③判定和断言相互转换，即发散点处的判定转变成汇聚点处的断言，而汇聚点处的断言变成发散点处的判定。

2可逆程序语言计算能力验证

传统编程语言（如Java、C++等）的强大功能已经被实践所证明，它能胜任一切图灵机所能执行的计算任务，因此这些编程语言被称为图灵机完备（定义1）或图灵机等价。而可逆编程模型在传统语言模型的基础上施加了诸多限制和扩展，还能不能像传统语言一样强大确实值得怀疑。在文献＼[4＼]中，Bennett证明了一个基本结果：所有不可逆的通用图灵机，都可以找到一个对应的可逆图灵机，使得两者具有完全相同的计算能力。因此只要证明了可逆编程模型是可逆图灵机完备（定义2、定义3），即可表明可逆程序和传统程序一样有巨大的运算能力和实用价值。

定义1（图灵完备性）：图灵完备指在可计算性理论中，编程语言或任意其它的逻辑系统具有等同于通用图灵机的计算能力。换言之，此系统可与通用图灵机互相模拟。

定义2（可逆图灵机）：一个图灵机被称为是可逆的，当且仅当其既具有前向确定性又具有反向确定性。

区别于传统图灵机采用五元组表示规则，可逆图灵机形式化定义采用四元组表示规则＼[4＼]。可逆图灵机形式化定义主要包含以下元素：Q是有限的状态集合，S是有限的输入符号集合，R代表控制规则集合。其中规则集合R中又包含两类规则：符号规则﹤q1，s1，s2，q2﹥，表示如当前状态为q1，且读写头所指的字符是s1，则机器进入q2状态，且将读写头所指符改为s2；移动规则﹤q1，/，d，q2﹥，表示如果当前状态为q1，则根据d移动读写头，其中d∈{-1，0，+1}，分别表示左移一格、不移动和右移一格。一个图灵机被称为是可逆的，当且仅当其既具有前向确定性又具有反向确定性，即对任意两个不同规则﹤q1，s1，s2，q2﹥和﹤q1，s1，s2，q2﹥，如果q1=q1，则s1≠/，s1≠/，且s1≠s1。

定义3（可逆图灵完备）：可逆图灵完备是指编程语言能在不引入垃圾信息的基础上模拟可逆图灵机所执行的一切计算。

定理1（可逆编程语言的可逆图灵完备性）：可逆编程语言是可逆图灵机完备的。

证明＼[10＼]：可逆图灵机在某一时刻的格局（configuration）可以描述如下：q代表当前状态，s表示读写头处的符号，Left代表磁带在读写头左边的部分，Right代表磁带在读写头右边的部分，可将这两部分看成堆栈，栈顶在s处（见图6）。

图6可逆图灵机格局

假设可逆图灵机的开始状态和终止状态分别是qb和qe，控制规则集合形如{R1，R2，R3，…，Rn}。首先，将任意规则Ri转换成等价的可逆编程流程图Ci，转换规则如图7所示。图中函数FQ（q1，q2）模拟从状态q1到状态q2的可逆变换，包含以下步骤：q=q xor q1，q=q xor q2。FS（s1，s2）是模拟将当前符号s1改为s2的可逆操作，包含以下步骤：s=s xor s1，s=s xor s2。Move（d）模拟读写磁头的移动，当d=1时右移，将当前符号s压进Left栈，同时将s退出Right栈，即push s Left，pop s Right；当d=-1左移，操作和右移相反，即push s Right， pop s Left；d=0是不移动，无需进行进出栈操作。图7（a）模拟字符规则﹤q1，s1，s2，q2﹥，含义为如当前状态为q1，且当前字符是s1，则进入t分支，执行FQ（q1，q2）和FS（s1，s2），否则转向f分支执行Ci+1，Ci+1是其它某个规则的等价转换图，最后两个分支汇聚在断言（q=q2 ∧s=s2）上，该断言可以确保反向执行时能回溯到正确的前状态。图7（b）模拟移动规则﹤q1，/，d，q2﹥，含义为如当前状态为q1，则进入t分支，执行FQ（q1，q2）和Move（d），否则进入f分支，最后两个分支汇聚在断言（q=q2）处，该断言也可确保反向执行时回溯到正确的前状态。由图7的两个规则转换图并结合递归思想可知，C1中包含C2，C2中包含C3，直到Cn，因此C1可代表可逆图灵机的所有控制规则。

图7可逆图灵机规则转换

图8主循环C0

3可逆编程语言Janus

Janus＼[8＼]是编程语言史上第一个可逆编程语言，由Lutz和Derby发明，该语言可作为开发其它可逆编程语言的参考模型，包含一个编译器和一个解释器，编译器由SLIMEULA编写，将代码编译成SLIMEULA类结构，该结构可以被解释器直接执行。Janus的编译器主要由词法分析器、递归下降解析器、解释器、运行时命令扫描器组成。Janus语法如下：

Janus程序由一个主函数和若干个自定义函数组成，且函数中的每一个元素都是可逆的。首先，每一个赋值操作（形如x⊕=e|x＼[e＼]⊕=e）均是可逆的，式中的左值x不能出现在右表达式e中，e可以是一个常量、变量、数组元素或表达式等，⊕是含3种可逆运算符（含加法、减法和异或运算符）的集合，通过如此限制保证其可逆性，如x：：=x+e的逆形式为x：：=x-e；其次，条件语句和循环均是可逆的，其结构流程图分别对应图4和图5，即在进入结构处有判定条件，在退出结构处有断言。另外，对内存的动态分配也是可逆的，其中进出栈操作显然互为逆操作，而局部变量块（local t x=e1 s delocal t x=e2）包含以下步骤：为类型为t的变量x分配内存并赋初值为e1；经过语句s后，其值变为e2；通过delocal语句回收满足x=e2的内存。执行该语句块后，内存没有发生任何变化，因此也是可逆的；最后，函数调用也是可逆的，其中call q（x，x，…，x）表示以正向的语义执行函数，而uncall q（x，x，…，x）表示以反向的语义执行函数。

在理想情况下（即内存空间无限且不考虑运行效率），所有使用传统程序编写的代码段都可以转换成相同功能的Janus程序段，举例如下：

Ex1. Fibonacci数列：

以下便是Janus版的Fibonacci数列代码段，其中正向调用call由n=4，计算出x1=5、x2=8；而反向调用由x1=5、x2=8，计算出n=4，由此可见计算过程是完全可逆的。

Ex2. 由年收入计算税金。规则如下：1 000元之内，按10%收取；1 000元到10 000元之间的部分，按30%收取；10 000元以上部分，按50%收取。

以下代码段，正向运行由年薪计算税金，反向运算由税金计算年薪。

Ex1代码：

procedure fib

if n=0 then x1 += 1

x2 += 1

else n -= 1

call fib

x1 += x2

x1 <=> x2

fi x1=x2

procedure main_fwd

n += 4

call fib

procedure main_bwd

x1 += 5

x2 += 8

Ex2代码：

Procedure tax

if x<1000 then x：=0.1*x

else if x<1000 then x：=0.3*x-200

else x：=0.5*x-2200

fi x<2800

fi x<100

procedure main_fwd

x += 900

call tax

procedure main_bwd

x += 90

uncall tax

4结语

本研究首先给出了可逆编程的3种基本结构，这3种结构均是结构化编码的基本组成元素，它们都保持了单入口单出口的特点，由此组成的可逆算法在可读性和可维护性方面均高于非结构化的编码模型，另外，在功能上可逆结构化模型和可逆非结构化模型也是等价的，这个结论通过借鉴传统结构化编程的相似证明＼[9＼]，已由Yokoyama在文献＼[10＼]中给出证明，因此和传统算法设计一样，在进行可逆算法设计时也应该采用结构化编码方式。

其次，通过证明由3种可逆基本结构组成的可逆模型具备可逆图灵完备性，得出可逆编程语言和传统编程语言在功能上等价的结论。但是，实际上并不是每个问题都可以直接使用可逆编程模型解决，很多时候需要引入额外内存空间（保存运算过程的历史信息），使针对该问题解决方案的描述变得可逆，然后才能运用可逆编程模型去解决＼[1416＼]。这就意味着可逆编程语言在时空效率上较传统语言还有较大差距，有待进一步研究去缩减这个差距。

最后，本文简单介绍了第一个可逆语言Janus，并给出了两个示例。但到目前为止，Janus并不是唯一的可逆语言，还有其它一些可逆编程语言，如Gries＼[11＼]、Inv＼[12＼]、（E）SRL＼[13＼]、RJava＼[17＼]。

参考文献参考文献：

＼[1＼]VIDEO TRANSCRIPT. Excerpts from a conversation with gordon moore：moorels law ＼[Z＼].Intel Corporation， 2005.

＼[2＼]KANELLOS， MICHAEL. New life for moore's law＼[EB/OL＼].http：//news.cnet.com/NewlifeforMooresLaw/20091006_35672485.html.

＼[3＼]R LANDAUER. Irreversibility and heat generation in the computing process＼[J＼]. IBM Journal of Research and Development， 1961（5）： 183191.

＼[4＼]C H BENNETT. Logical reversibility of computation＼[J＼]. IBM Journal of Research and Development， 1973，17（6）： 525532.

＼[5＼]TOMMASO TOFFOLI. Computation and construction universality of reversible cellular automata＼[M＼]. Journal of computer and system sciences ， 1977（15）： 213231.

＼[6＼]GANDY R. Church's thesis and principles for mechanisms＼[J＼].In Barwise J ， Keisler H J ， Kunen K （eds） 1980. The Kleene Symposium. Amsterdam： NorthHolland.

＼[7＼]TODD L. Veldhuizen. C++ templates are turing complete＼[EB/OL＼].www.osl.iu.edu/～tveldhui/papers/www.osl.iu.edu/～tveldhui/papers/2003/turing.pdf， 2003.

＼[8＼]LUTZ C. Janus： a timereversible language＼[EB/OL＼].http：//www.cise.ufl.edu/？mpf/rc/janus.html.

＼[9＼]T YOKOYAMA， HB AXELSEN， R GLUCK. Reversible flowchart languages and the structured reversible program theorem＼[C＼].Automata， Languages and Programming （Proc.）， LNCS 5126， 2008：258270.

＼[10＼]DAVID C，COOPER. B¨ohm and Jacopinis reduction of flow charts＼[J＼]. Communications of the ACM， 1967，10（8）：463473.

＼[11＼]ROBERT GLUCK，MASAHIKO KAWABE. Derivation of deterministic inverse programs based on LR parsing＼[M＼]. In FLOPS， 2004： 291306.

＼[12＼]MU S C，Z HU，M TAKEICHI. An injective language for reversible computation＼[M＼].in： D. KOZEN.Mathematics of program construction.proceedings，LNCS 3125，2004： 289313.

＼[13＼]MATOS A B.Linear programs in a simple reversible language＼[M＼].Theor Comput Sci，2003（290）：20632074.

＼[14＼]KLUGE W E.A reversible SE（M）CD machine＼[M＼].Proceedings，Selected Papers，LNCS 1868，2000：95113.

＼[15＼]STODDART B，R LYNAS，F ZEYDA. A reversible virtual machine＼[M＼].in：I.ULIDOWSKI，editor，Reversible Computation，Preliminary Proceedings，2009：1832.

＼[16＼]GRIES D.The science of programming＼[M＼].Springer，Heidelberg，1981：265274.

＼[17＼]朱鹏程，管致锦，卫丽华.可逆变成语言RJAVA及其语言处理系统的设计＼[J＼]. 计算机工程与设计，2013，34（10）：35023510.

责任编辑（责任编辑：杜能钢）