對(duì)church-rosser定理的再探討

邱易

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

對(duì)church-rosser定理的再探討

邱易

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

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

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

0　引言

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

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

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

1　church-rosser定理及其例外

1.1lambda演算與church rosser定理

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

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

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

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

ζ等價(jià)可以理解為λx.F x等價(jià)于F。

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

1.2一個(gè)特殊的lambda項(xiàng)及其展開(kāi)過(guò)程

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

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

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

Step1：展開(kāi)main，這個(gè)f的參數(shù)為atom；

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

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

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

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

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

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

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

Step9：展開(kāi)這一層的（x eval），愉快地計(jì)算（X（X X）（X X））

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

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

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

2　結(jié)語(yǔ)

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

［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