对church-rosser定理的再探讨

邱易

（华中科技大学计算机科学与技术学院，武汉　430074）

对church-rosser定理的再探讨

邱易

（华中科技大学计算机科学与技术学院，武汉430074）

在lambda演算中，找到永不终止却有意义的lambda项，并讨论它的意义：任何可计算的函数都可能在它的求值过程中出现，且出现顺序受到求值顺序控制。

无限；停机；lambda演算

0　引言

长久以来，业界一直认为，有意义的计算必须是在有限步之内终止的，对“有限”这一概念的执着发展到极致，就催生出了像coq这样不管怎样都一定会停机的语言，好像现在不能在有限步之内停止的计算已经排除在计算之外了，有人竟然产生了“操作系统这种永不停机的程序已经超出丘奇图灵论题的描述能力”这种怪论，然而，永不停止的过程同样是计算，例如这个tag machine［1］，符号有两个，a，b，每次擦除符号串尾的元素，如果它是a，就在符号串头写下a，如果是b，就可以在符号串头写下b或aba，这个规则显然是永不停止的，我们来看一下这个规则的演化过程［1］：

可以看出左边和右边的a个数加起来等于中间的a个数，因此这个规则描述了加法这一计算。

而本文要讨论的church-rosser定理，与这种言必有限的思潮有着莫大的关系。该定理是这样的，lambda演算中，任何一个lambda项，不管通过何种顺序计算，最后不终止则已，要终止，就一定终止在同一个lambda项上。而问题是大家好像默认为，一个计算，不管通过何种顺序计算，结果一定相同，而所有停不下来的情况，都不叫计算，惟“死循环”三个字而已，而接下来将要看到，无限之中，还有非常丰富的计算过程。

1　church-rosser定理及其例外

1.1lambda演算与church rosser定理

lambda演算研究的对象称为lambda项，lambda项构成如下：

所有字母是lambda项；如果a是字母，M N是lambda项，则λa.M和M N都是lambda项。这些计算有三条规则

α变换对于λa.m，把所有a换成其他字母，意义不变；

β规约（λa.M）N规约结果为把M里所有出现a的地方换成N；

ζ等价可以理解为λx.F x等价于F。

Church-rosser定理正是关于beta规约的定理，举例说明：

1.2一个特殊的lambda项及其展开过程

现在给出一个lambda项，为了方便，用=表示左边的符号代表右边的lambda项，变量均用一个字母表示，λxy代表λx.λy：

以上这些，car，cdr，cons定义了链表，通过X的复合可以构造出所有的可计算函数，这里不再证明，leftfold函数是把（a b c）形式的链表转化成（（a b）c）形式的链表，righ-fold是把（（a b）c）转化成（a（b c））形式的链表，而对一个完全由atom构成的链表L，L eval相当于对把atom换成X得到的表达式进行求值。而我们关注main的展开，可以发现，采用不同的求值顺序，任何函数都可以被计算，而通过控制求值顺序，可以完全控制这些函数计算的次序。

例如我想第一个计算函数（X（X X）（X X）），可以这样：

Step1：展开main，这个f的参数为atom；

Step2：展开这一层的（f f（left-cons x）），这里f的参数为（atom atom）

Step3：展开这一层的（f f（left-cons x），这里f的参数为（atom atom atom）

Step4：展开这一层的（f f（left-fold x），这里f的参数为（（atom atom）atom）

Step5：展开这一层的（f f（right-fold x）），这里f的参数为（atom（atom atom））

Step6：展开这一层的（f f（left-cons x），这里f的参数为（atom atom（atom atom））

Step7：展开这一层的（f f（left-fold x），这里f的参数为（（atom atom）（atom atom））

Step8：展开这一层的（f f（left-cons x），这里f的参数为（atom（atom atom）（atom atom））

Step9：展开这一层的（x eval），愉快地计算（X（X X）（X X））

1.3该lambda项的意义

所有计算都可能在这个过程里出现，因此，整个过程的返回值没有什么意义，而这些计算出现的顺序就至关重要，想象你是在学园都市里面一个没权没钱的研究人员，要申请使用学园都市算力最高的计算机——树形图设计者，但是刚申请下来，排队等着前面人用完的时候，你跟管这个计算机的人起了冲突，他叫嚣要给你点颜色看看，你想，无所谓，church—rosser定理不是这等宵小之辈可以撼动得了的，结果那边他每通过一个使用树形图设计者的申请，就把它排在你前面，这下子除非学园都市再没人搞研究，你都别想用了。

这个方式可以看做一个最简单的操作系统，试想，在现实的电脑上运行一个死循环程序，电脑并不会就此瘫痪，过一会儿，操作系统就会提示你”程序无响应要关掉它吗？”，这就是说，CPU并没有直接计算那个死循环程序，而是在计算操作系统和死循环组成的大程序，而操作系统随时可以将它停止，而在这里，你在计算的是那个lambda项，你想要停止当前的程序prog，可以让下一步求值不再计算prog，而是把上一层（λabcdeg.a）的参数全部以传名的方式传入（λabcdeg.a），这样那个程序在下一步的求值中就不存在了。

2　结语

在大家的心里，有限的过程丰富多彩，再往上都是死循环，死循环的步数都是潜无穷，都一个样，再往上就是现世的机械触及不到之处。而在本文中可以看到，同样是无限步的过程，可以是开头那个单一的加法，也可以是这个涵盖所有函数的操作系统，这时候才知道无限之上，犹有境界。

［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-），男，山东济南人，在读本科

2016-07-19

2016-09-10