可逆編程語言相關(guān)理論及實(shí)踐研究

摘要：從編程語言的角度研究了可逆計(jì)算。首先，給出可逆編程語言流程圖的3種基本結(jié)構(gòu)，從而構(gòu)建一個(gè)可逆編程語言的可視模型；其次，證明可逆語言的可逆圖靈機(jī)完備性，進(jìn)而論證其與傳統(tǒng)編程語言在計(jì)算能力上的一致性；最后，介紹了可逆編程語言Janus并進(jìn)行了編程實(shí)踐。

關(guān)鍵詞關(guān)鍵詞：可逆計(jì)算；可逆編程語言；流程圖；圖靈機(jī)；圖靈完備

DOIDOI：10.11907/rjdk.1431017

中圖分類號(hào)：TP314

文獻(xiàn)標(biāo)識(shí)碼：A文章編號(hào)文章

編號(hào)：16727800（2015）002006204

基金項(xiàng)目基金項(xiàng)目：南通理工學(xué)院校級(jí)科研項(xiàng)目（2014002）

作者簡(jiǎn)介作者簡(jiǎn)介：衛(wèi)麗華（1984-），女，江蘇南通人，碩士，南通理工學(xué)院軟件工程系講師，研究方向?yàn)榭赡嬗?jì)算。

0引言

可逆計(jì)算作為一個(gè)新興學(xué)科，對(duì)未來計(jì)算機(jī)的持續(xù)發(fā)展起著決定性的作用。自20世紀(jì)60年代以來，計(jì)算機(jī)硬件一直遵循著Moore定律＼[1＼]高速發(fā)展，但這種發(fā)展趨勢(shì)預(yù)計(jì)會(huì)在2020年左右終結(jié)＼[2＼]，主要原因如下：?jiǎn)挝幻娣e器件數(shù)量的增加，會(huì)導(dǎo)致產(chǎn)生的熱量超出芯片能承受的極限。R·landauer最早考慮了能耗導(dǎo)致計(jì)算機(jī)芯片發(fā)熱的問題＼[3＼]，他指出能耗來源于計(jì)算過程中的不可逆操作，因此采用可逆計(jì)算可以大大降低計(jì)算機(jī)的能耗?？赡嬗?jì)算主要關(guān)注兩個(gè)方面：物理可逆和邏輯可逆，R.Landauer在文獻(xiàn)＼[3＼]中證明，如果一個(gè)計(jì)算過程物理可逆，那么該過程須同時(shí)邏輯可逆。一個(gè)計(jì)算過程如果不僅能從輸入狀態(tài)得到輸出狀態(tài)（正向），并且能從輸出狀態(tài)唯一確定輸入狀態(tài)（反向），那么該計(jì)算過程便是邏輯可逆的。

當(dāng)今流行的計(jì)算機(jī)（RAM機(jī)或圖靈機(jī)）都是邏輯不可逆的，因?yàn)樗鼈冊(cè)谟?jì)算過程中會(huì)銷毀或丟失信息，從而不能回推前狀態(tài)。Landauer認(rèn)為通過保存運(yùn)算過程中的歷史信息，可以將不可逆性通過逆向跟蹤程序流程圖得到。本文根據(jù)傳統(tǒng)程序流程圖的3種基本結(jié)構(gòu)，將一個(gè)不可逆運(yùn)算轉(zhuǎn)變成可逆運(yùn)算，引入額外信息通過反向運(yùn)算清除＼[4＼]。理論上講，只要存儲(chǔ)空間足夠，任何不可逆計(jì)算都可以轉(zhuǎn)換成可逆計(jì)算。目前已經(jīng)出現(xiàn)了一些可逆計(jì)算模型，比如可逆圖靈機(jī)＼[4＼]和可逆細(xì)胞自動(dòng)機(jī)＼[5＼]，但針對(duì)較高邏輯層級(jí)的軟件（即編程語言）進(jìn)行的研究還比較欠缺。

各種流行的程序設(shè)計(jì)語言，如C++、Java等均是完備的圖靈機(jī)＼[67＼]，即可將其視為一個(gè)特殊的圖靈機(jī)。鑒于一般圖靈機(jī)的不可逆性，這些編程語言也是不可逆的。另外，對(duì)傳統(tǒng)編程語言進(jìn)行改造，使得改進(jìn)后的結(jié)構(gòu)既可以正向執(zhí)行又可以反向跟蹤，從而構(gòu)建可逆編程的可視模型。本文對(duì)可逆編程語言Janus＼[8＼]作了介紹，并給出了示例代碼。

1可逆編程流程

目前流行的傳統(tǒng)程序語言均是不可逆的，即不能確保從輸出狀態(tài)獲得輸入狀態(tài)，這從程序流程圖上就可以看出（見圖1），在流程圖中的有些分支匯聚點(diǎn)是沒有判定條件的，這就導(dǎo)致了反向執(zhí)行流程時(shí)，不知道該跟蹤哪個(gè)分支。此外，不強(qiáng)制要求每個(gè)單步操作（對(duì)應(yīng)流程圖中的處理框）可逆也是導(dǎo)致傳統(tǒng)程序語言不可逆的原因之一。傳統(tǒng)語言的基本結(jié)構(gòu)（順序結(jié)構(gòu)、選擇結(jié)構(gòu)和循環(huán)結(jié)構(gòu)）都存在上述問題，通過對(duì)傳統(tǒng)程序流程圖進(jìn)行擴(kuò)展可以解決上述不可逆問題。

擴(kuò)展的可逆程序流程圖＼[9＼]包含以下3個(gè)基本元素（見圖2）：?jiǎn)尾讲僮?、判定、斷言。其中“單步操作”必須是一個(gè)可逆操作，即可以由輸出唯一確定輸入，如x=y，由于x值被y所覆蓋無法再恢復(fù)，所以是不可逆的，可以用x=x x or y這樣的可逆形式取代前者；“判定”根據(jù)內(nèi)部條件的取值（真或假）執(zhí)行不同分支；“斷言”則根據(jù)內(nèi)部條件的不同取值接受不同分支，如取真時(shí)，接受分支t，取假，接受分支f?！芭卸ā焙汀皵嘌浴倍及粋€(gè)內(nèi)部判斷條件，但是前者是流程圖中的發(fā)散點(diǎn)，而后者是匯聚點(diǎn)，兩者在程序正向執(zhí)行和逆向跟蹤時(shí)進(jìn)行相互轉(zhuǎn)換。此3個(gè)基本元素可以構(gòu)成可逆程序流程圖的3種基本控制結(jié)構(gòu)。

1.1可逆順序結(jié)構(gòu)

在傳統(tǒng)順序結(jié)構(gòu)的基礎(chǔ)上，保證每個(gè)單步操作的局部可逆性就得到可逆的順序結(jié)構(gòu)（見圖3）。局部可逆性解釋如下：將單步操作a看作一個(gè)狀態(tài)變換函數(shù)，當(dāng)且僅當(dāng)存在和上下文無關(guān)（即和在流程圖中的所處位置無關(guān)）的反函數(shù)a-1時(shí)，稱a為局部可逆的。關(guān)于局部可逆在文獻(xiàn)＼[11＼]中有詳細(xì)介紹。

圖3可逆順序結(jié)構(gòu)

1.2可逆選擇結(jié)構(gòu)

傳統(tǒng)的ifthenelse選擇結(jié)構(gòu)包括兩部分：一個(gè)判定條件，兩個(gè)分支?？赡孢x擇結(jié)構(gòu)在此基礎(chǔ)上在分支匯聚點(diǎn)加上斷言c2，結(jié)構(gòu)見圖4。反向執(zhí)行時(shí)，判定c1變成斷言c1，斷言c2變成判定c2。

圖4可逆選擇結(jié)構(gòu)

1.3可逆循環(huán)結(jié)構(gòu)

傳統(tǒng)循環(huán)結(jié)構(gòu)包含兩個(gè)部分：循環(huán)判定條件、循環(huán)體?？赡嫜h(huán)結(jié)構(gòu)如圖5所示，包含3個(gè)部分：斷言c1、兩個(gè)操作序列A和B、循環(huán)判定條件c2，當(dāng)A為空時(shí)對(duì)應(yīng)while循環(huán)，當(dāng)B為空時(shí)，對(duì)應(yīng)dowhile循環(huán)。

圖5可逆循環(huán)結(jié)構(gòu)

從圖3、圖4及圖5可知，由可逆程序流程圖得到反向圖是件很容易的事情，主要包含以下幾個(gè)步驟：①改變流程線的箭頭方向；②用a-1代替單步操作a；③判定和斷言相互轉(zhuǎn)換，即發(fā)散點(diǎn)處的判定轉(zhuǎn)變成匯聚點(diǎn)處的斷言，而匯聚點(diǎn)處的斷言變成發(fā)散點(diǎn)處的判定。

2可逆程序語言計(jì)算能力驗(yàn)證

傳統(tǒng)編程語言（如Java、C++等）的強(qiáng)大功能已經(jīng)被實(shí)踐所證明，它能勝任一切圖靈機(jī)所能執(zhí)行的計(jì)算任務(wù)，因此這些編程語言被稱為圖靈機(jī)完備（定義1）或圖靈機(jī)等價(jià)。而可逆編程模型在傳統(tǒng)語言模型的基礎(chǔ)上施加了諸多限制和擴(kuò)展，還能不能像傳統(tǒng)語言一樣強(qiáng)大確實(shí)值得懷疑。在文獻(xiàn)＼[4＼]中，Bennett證明了一個(gè)基本結(jié)果：所有不可逆的通用圖靈機(jī)，都可以找到一個(gè)對(duì)應(yīng)的可逆圖靈機(jī)，使得兩者具有完全相同的計(jì)算能力。因此只要證明了可逆編程模型是可逆圖靈機(jī)完備（定義2、定義3），即可表明可逆程序和傳統(tǒng)程序一樣有巨大的運(yùn)算能力和實(shí)用價(jià)值。

定義1（圖靈完備性）：圖靈完備指在可計(jì)算性理論中，編程語言或任意其它的邏輯系統(tǒng)具有等同于通用圖靈機(jī)的計(jì)算能力。換言之，此系統(tǒng)可與通用圖靈機(jī)互相模擬。

定義2（可逆圖靈機(jī)）：一個(gè)圖靈機(jī)被稱為是可逆的，當(dāng)且僅當(dāng)其既具有前向確定性又具有反向確定性。

區(qū)別于傳統(tǒng)圖靈機(jī)采用五元組表示規(guī)則，可逆圖靈機(jī)形式化定義采用四元組表示規(guī)則＼[4＼]?？赡鎴D靈機(jī)形式化定義主要包含以下元素：Q是有限的狀態(tài)集合，S是有限的輸入符號(hào)集合，R代表控制規(guī)則集合。其中規(guī)則集合R中又包含兩類規(guī)則：符號(hào)規(guī)則﹤q1，s1，s2，q2﹥，表示如當(dāng)前狀態(tài)為q1，且讀寫頭所指的字符是s1，則機(jī)器進(jìn)入q2狀態(tài)，且將讀寫頭所指符改為s2；移動(dòng)規(guī)則﹤q1，/，d，q2﹥，表示如果當(dāng)前狀態(tài)為q1，則根據(jù)d移動(dòng)讀寫頭，其中d∈{-1，0，+1}，分別表示左移一格、不移動(dòng)和右移一格。一個(gè)圖靈機(jī)被稱為是可逆的，當(dāng)且僅當(dāng)其既具有前向確定性又具有反向確定性，即對(duì)任意兩個(gè)不同規(guī)則﹤q1，s1，s2，q2﹥和﹤q1，s1，s2，q2﹥，如果q1=q1，則s1≠/，s1≠/，且s1≠s1。

定義3（可逆圖靈完備）：可逆圖靈完備是指編程語言能在不引入垃圾信息的基礎(chǔ)上模擬可逆圖靈機(jī)所執(zhí)行的一切計(jì)算。

定理1（可逆編程語言的可逆圖靈完備性）：可逆編程語言是可逆圖靈機(jī)完備的。

證明＼[10＼]：可逆圖靈機(jī)在某一時(shí)刻的格局（configuration）可以描述如下：q代表當(dāng)前狀態(tài)，s表示讀寫頭處的符號(hào)，Left代表磁帶在讀寫頭左邊的部分，Right代表磁帶在讀寫頭右邊的部分，可將這兩部分看成堆棧，棧頂在s處（見圖6）。

圖6可逆圖靈機(jī)格局

假設(shè)可逆圖靈機(jī)的開始狀態(tài)和終止?fàn)顟B(tài)分別是qb和qe，控制規(guī)則集合形如{R1，R2，R3，…，Rn}。首先，將任意規(guī)則Ri轉(zhuǎn)換成等價(jià)的可逆編程流程圖Ci，轉(zhuǎn)換規(guī)則如圖7所示。圖中函數(shù)FQ（q1，q2）模擬從狀態(tài)q1到狀態(tài)q2的可逆變換，包含以下步驟：q=q xor q1，q=q xor q2。FS（s1，s2）是模擬將當(dāng)前符號(hào)s1改為s2的可逆操作，包含以下步驟：s=s xor s1，s=s xor s2。Move（d）模擬讀寫磁頭的移動(dòng)，當(dāng)d=1時(shí)右移，將當(dāng)前符號(hào)s壓進(jìn)Left棧，同時(shí)將s退出Right棧，即push s Left，pop s Right；當(dāng)d=-1左移，操作和右移相反，即push s Right， pop s Left；d=0是不移動(dòng)，無需進(jìn)行進(jìn)出棧操作。圖7（a）模擬字符規(guī)則﹤q1，s1，s2，q2﹥，含義為如當(dāng)前狀態(tài)為q1，且當(dāng)前字符是s1，則進(jìn)入t分支，執(zhí)行FQ（q1，q2）和FS（s1，s2），否則轉(zhuǎn)向f分支執(zhí)行Ci+1，Ci+1是其它某個(gè)規(guī)則的等價(jià)轉(zhuǎn)換圖，最后兩個(gè)分支匯聚在斷言（q=q2 ∧s=s2）上，該斷言可以確保反向執(zhí)行時(shí)能回溯到正確的前狀態(tài)。圖7（b）模擬移動(dòng)規(guī)則﹤q1，/，d，q2﹥，含義為如當(dāng)前狀態(tài)為q1，則進(jìn)入t分支，執(zhí)行FQ（q1，q2）和Move（d），否則進(jìn)入f分支，最后兩個(gè)分支匯聚在斷言（q=q2）處，該斷言也可確保反向執(zhí)行時(shí)回溯到正確的前狀態(tài)。由圖7的兩個(gè)規(guī)則轉(zhuǎn)換圖并結(jié)合遞歸思想可知，C1中包含C2，C2中包含C3，直到Cn，因此C1可代表可逆圖靈機(jī)的所有控制規(guī)則。

圖7可逆圖靈機(jī)規(guī)則轉(zhuǎn)換

圖8主循環(huán)C0

3可逆編程語言Janus

Janus＼[8＼]是編程語言史上第一個(gè)可逆編程語言，由Lutz和Derby發(fā)明，該語言可作為開發(fā)其它可逆編程語言的參考模型，包含一個(gè)編譯器和一個(gè)解釋器，編譯器由SLIMEULA編寫，將代碼編譯成SLIMEULA類結(jié)構(gòu)，該結(jié)構(gòu)可以被解釋器直接執(zhí)行。Janus的編譯器主要由詞法分析器、遞歸下降解析器、解釋器、運(yùn)行時(shí)命令掃描器組成。Janus語法如下：

Janus程序由一個(gè)主函數(shù)和若干個(gè)自定義函數(shù)組成，且函數(shù)中的每一個(gè)元素都是可逆的。首先，每一個(gè)賦值操作（形如x⊕=e|x＼[e＼]⊕=e）均是可逆的，式中的左值x不能出現(xiàn)在右表達(dá)式e中，e可以是一個(gè)常量、變量、數(shù)組元素或表達(dá)式等，⊕是含3種可逆運(yùn)算符（含加法、減法和異或運(yùn)算符）的集合，通過如此限制保證其可逆性，如x：：=x+e的逆形式為x：：=x-e；其次，條件語句和循環(huán)均是可逆的，其結(jié)構(gòu)流程圖分別對(duì)應(yīng)圖4和圖5，即在進(jìn)入結(jié)構(gòu)處有判定條件，在退出結(jié)構(gòu)處有斷言。另外，對(duì)內(nèi)存的動(dòng)態(tài)分配也是可逆的，其中進(jìn)出棧操作顯然互為逆操作，而局部變量塊（local t x=e1 s delocal t x=e2）包含以下步驟：為類型為t的變量x分配內(nèi)存并賦初值為e1；經(jīng)過語句s后，其值變?yōu)閑2；通過delocal語句回收滿足x=e2的內(nèi)存。執(zhí)行該語句塊后，內(nèi)存沒有發(fā)生任何變化，因此也是可逆的；最后，函數(shù)調(diào)用也是可逆的，其中call q（x，x，…，x）表示以正向的語義執(zhí)行函數(shù)，而uncall q（x，x，…，x）表示以反向的語義執(zhí)行函數(shù)。

在理想情況下（即內(nèi)存空間無限且不考慮運(yùn)行效率），所有使用傳統(tǒng)程序編寫的代碼段都可以轉(zhuǎn)換成相同功能的Janus程序段，舉例如下：

Ex1. Fibonacci數(shù)列：

以下便是Janus版的Fibonacci數(shù)列代碼段，其中正向調(diào)用call由n=4，計(jì)算出x1=5、x2=8；而反向調(diào)用由x1=5、x2=8，計(jì)算出n=4，由此可見計(jì)算過程是完全可逆的。

Ex2. 由年收入計(jì)算稅金。規(guī)則如下：1 000元之內(nèi)，按10%收取；1 000元到10 000元之間的部分，按30%收??；10 000元以上部分，按50%收取。

以下代碼段，正向運(yùn)行由年薪計(jì)算稅金，反向運(yùn)算由稅金計(jì)算年薪。

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結(jié)語

本研究首先給出了可逆編程的3種基本結(jié)構(gòu)，這3種結(jié)構(gòu)均是結(jié)構(gòu)化編碼的基本組成元素，它們都保持了單入口單出口的特點(diǎn)，由此組成的可逆算法在可讀性和可維護(hù)性方面均高于非結(jié)構(gòu)化的編碼模型，另外，在功能上可逆結(jié)構(gòu)化模型和可逆非結(jié)構(gòu)化模型也是等價(jià)的，這個(gè)結(jié)論通過借鑒傳統(tǒng)結(jié)構(gòu)化編程的相似證明＼[9＼]，已由Yokoyama在文獻(xiàn)＼[10＼]中給出證明，因此和傳統(tǒng)算法設(shè)計(jì)一樣，在進(jìn)行可逆算法設(shè)計(jì)時(shí)也應(yīng)該采用結(jié)構(gòu)化編碼方式。

其次，通過證明由3種可逆基本結(jié)構(gòu)組成的可逆模型具備可逆圖靈完備性，得出可逆編程語言和傳統(tǒng)編程語言在功能上等價(jià)的結(jié)論。但是，實(shí)際上并不是每個(gè)問題都可以直接使用可逆編程模型解決，很多時(shí)候需要引入額外內(nèi)存空間（保存運(yùn)算過程的歷史信息），使針對(duì)該問題解決方案的描述變得可逆，然后才能運(yùn)用可逆編程模型去解決＼[1416＼]。這就意味著可逆編程語言在時(shí)空效率上較傳統(tǒng)語言還有較大差距，有待進(jìn)一步研究去縮減這個(gè)差距。

最后，本文簡(jiǎn)單介紹了第一個(gè)可逆語言Janus，并給出了兩個(gè)示例。但到目前為止，Janus并不是唯一的可逆語言，還有其它一些可逆編程語言，如Gries＼[11＼]、Inv＼[12＼]、（E）SRL＼[13＼]、RJava＼[17＼]。

參考文獻(xiàn)參考文獻(xiàn)：

＼[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(xiàn) 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＼]朱鵬程，管致錦，衛(wèi)麗華.可逆變成語言RJAVA及其語言處理系統(tǒng)的設(shè)計(jì)＼[J＼]. 計(jì)算機(jī)工程與設(shè)計(jì)，2013，34（10）：35023510.

責(zé)任編輯（責(zé)任編輯：杜能鋼）