邱易

（華中科技大學(xué)計算機(jī)科學(xué)與技術(shù)學(xué)院，武漢　430074）

對church-rosser定理的再探討

邱易

（華中科技大學(xué)計算機(jī)科學(xué)與技術(shù)學(xué)院，武漢430074）

在lambda演算中，找到永不終止卻有意義的lambda項(xiàng)，并討論它的意義：任何可計算的函數(shù)都可能在它的求值過程中出現(xiàn)，且出現(xiàn)順序受到求值順序控制。

無限；停機(jī)；lambda演算

0　引言

長久以來，業(yè)界一直認(rèn)為，有意義的計算必須是在有限步之內(nèi)終止的，對“有限”這一概念的執(zhí)著發(fā)展到極致，就催生出了像coq這樣不管怎樣都一定會停機(jī)的語言，好像現(xiàn)在不能在有限步之內(nèi)停止的計算已經(jīng)排除在計算之外了，有人竟然產(chǎn)生了“操作系統(tǒng)這種永不停機(jī)的程序已經(jīng)超出丘奇圖靈論題的描述能力”這種怪論，然而，永不停止的過程同樣是計算，例如這個tag machine［1］，符號有兩個，a，b，每次擦除符號串尾的元素，如果它是a，就在符號串頭寫下a，如果是b，就可以在符號串頭寫下b或aba，這個規(guī)則顯然是永不停止的，我們來看一下這個規(guī)則的演化過程［1］：

可以看出左邊和右邊的a個數(shù)加起來等于中間的a個數(shù)，因此這個規(guī)則描述了加法這一計算。

而本文要討論的church-rosser定理，與這種言必有限的思潮有著莫大的關(guān)系。該定理是這樣的，lambda演算中，任何一個lambda項(xiàng)，不管通過何種順序計算，最后不終止則已，要終止，就一定終止在同一個lambda項(xiàng)上。而問題是大家好像默認(rèn)為，一個計算，不管通過何種順序計算，結(jié)果一定相同，而所有停不下來的情況，都不叫計算，惟“死循環(huán)”三個字而已，而接下來將要看到，無限之中，還有非常豐富的計算過程。

1　church-rosser定理及其例外

1.1lambda演算與church rosser定理

lambda演算研究的對象稱為lambda項(xiàng)，lambda項(xiàng)構(gòu)成如下：

所有字母是lambda項(xiàng)；如果a是字母，M N是lambda項(xiàng)，則λa.M和M N都是lambda項(xiàng)。這些計算有三條規(guī)則

α變換對于λa.m，把所有a換成其他字母，意義不變；

β規(guī)約（λa.M）N規(guī)約結(jié)果為把M里所有出現(xiàn)a的地方換成N；

ζ等價可以理解為λx.F x等價于F。

Church-rosser定理正是關(guān)于beta規(guī)約的定理，舉例說明：

1.2一個特殊的lambda項(xiàng)及其展開過程

現(xiàn)在給出一個lambda項(xiàng)，為了方便，用=表示左邊的符號代表右邊的lambda項(xiàng)，變量均用一個字母表示，λxy代表λx.λy：

以上這些，car，cdr，cons定義了鏈表，通過X的復(fù)合可以構(gòu)造出所有的可計算函數(shù)，這里不再證明，leftfold函數(shù)是把（a b c）形式的鏈表轉(zhuǎn)化成（（a b）c）形式的鏈表，righ-fold是把（（a b）c）轉(zhuǎn)化成（a（b c））形式的鏈表，而對一個完全由atom構(gòu)成的鏈表L，L eval相當(dāng)于對把a(bǔ)tom換成X得到的表達(dá)式進(jìn)行求值。而我們關(guān)注main的展開，可以發(fā)現(xiàn)，采用不同的求值順序，任何函數(shù)都可以被計算，而通過控制求值順序，可以完全控制這些函數(shù)計算的次序。

例如我想第一個計算函數(shù)（X（X X）（X X）），可以這樣：

Step1：展開main，這個f的參數(shù)為atom；

Step2：展開這一層的（f f（left-cons x）），這里f的參數(shù)為（atom atom）

Step3：展開這一層的（f f（left-cons x），這里f的參數(shù)為（atom atom atom）

Step4：展開這一層的（f f（left-fold x），這里f的參數(shù)為（（atom atom）atom）

Step5：展開這一層的（f f（right-fold x）），這里f的參數(shù)為（atom（atom atom））

Step6：展開這一層的（f f（left-cons x），這里f的參數(shù)為（atom atom（atom atom））

Step7：展開這一層的（f f（left-fold x），這里f的參數(shù)為（（atom atom）（atom atom））

Step8：展開這一層的（f f（left-cons x），這里f的參數(shù)為（atom（atom atom）（atom atom））

Step9：展開這一層的（x eval），愉快地計算（X（X X）（X X））

1.3該lambda項(xiàng)的意義

所有計算都可能在這個過程里出現(xiàn)，因此，整個過程的返回值沒有什么意義，而這些計算出現(xiàn)的順序就至關(guān)重要，想象你是在學(xué)園都市里面一個沒權(quán)沒錢的研究人員，要申請使用學(xué)園都市算力最高的計算機(jī)——樹形圖設(shè)計者，但是剛申請下來，排隊等著前面人用完的時候，你跟管這個計算機(jī)的人起了沖突，他叫囂要給你點(diǎn)顏色看看，你想，無所謂，church—rosser定理不是這等宵小之輩可以撼動得了的，結(jié)果那邊他每通過一個使用樹形圖設(shè)計者的申請，就把它排在你前面，這下子除非學(xué)園都市再沒人搞研究，你都別想用了。

這個方式可以看做一個最簡單的操作系統(tǒng)，試想，在現(xiàn)實(shí)的電腦上運(yùn)行一個死循環(huán)程序，電腦并不會就此癱瘓，過一會兒，操作系統(tǒng)就會提示你”程序無響應(yīng)要關(guān)掉它嗎？”，這就是說，CPU并沒有直接計算那個死循環(huán)程序，而是在計算操作系統(tǒng)和死循環(huán)組成的大程序，而操作系統(tǒng)隨時可以將它停止，而在這里，你在計算的是那個lambda項(xiàng)，你想要停止當(dāng)前的程序prog，可以讓下一步求值不再計算prog，而是把上一層（λabcdeg.a）的參數(shù)全部以傳名的方式傳入（λabcdeg.a），這樣那個程序在下一步的求值中就不存在了。

2　結(jié)語

在大家的心里，有限的過程豐富多彩，再往上都是死循環(huán)，死循環(huán)的步數(shù)都是潛無窮，都一個樣，再往上就是現(xiàn)世的機(jī)械觸及不到之處。而在本文中可以看到，同樣是無限步的過程，可以是開頭那個單一的加法，也可以是這個涵蓋所有函數(shù)的操作系統(tǒng)，這時候才知道無限之上，猶有境界。

［1］http：//songshuhui.net/archives/93188

A Re-Discussion about Church-Rosser Principle

QIU Yi
（College of Computer Science and Technology，Huazhong University of Science and Technology，Wuhan 430074）

Finds a term in lambda calculus that makes sense but will never halt，and then discusses its meaning，which is that all of the computable function can appear during the evaluation of it，and that the order of their appearance depends on the evaluation order of that term.

Unlimited；Halt；Lambda Calculus

1007-1423（2016）26-0029-03DOI：10.3969/j.issn.1007-1423.2016.26.007

邱易（1995-），男，山東濟(jì)南人，在讀本科

2016-07-19

2016-09-10