递归函数(一):开篇
递归函数(二):编写递归函数的思路和技巧
递归函数(三):归纳原理
递归函数(四):全函数与计算的可终止性
递归函数(五):递归集与递归可枚举集
递归函数(六):最多有多少个程序
递归函数(七):不动点算子
递归函数(八):偏序结构
递归函数(九):最小不动点定理
- -
回顾
上文我们讨论了集合上的偏序结构,之所以谈论它们是因为,
完全偏序集上的连续函数具有最小不动点,这称之为最小不动点定理,
除了集合论的一些知识之外,我们还要讨论到底什么是连续函数,以及什么是完全偏序集。
有向子集与完全偏序
偏序集\((D,leqslant )\)的非空子集\(Ssubseteq D\)叫做有向子集(directed subset),
当且仅当,对于\(S\)中的任意元素\(a,bin S\),
存在\(S\)中的一个元素\(c\),有\(aleqslant c\)且\(bleqslant c\)。
如果一个偏序集\((D,leqslant )\)的每个有向子集\(Ssubseteq D\)都有上确界(记为\(bigvee S\))
就称它是一个有向完全偏序集,
此外,如果它还有最小元,就称它是一个完全偏序集。
注意,完全偏序集并不是每一个子集都有上确界,
而是它的每一个有向子集都有上确界。
连续函数
假设\((D,leqslant )\)与\((E,leqslant )\)是完全偏序集,
\(f:Drightarrow E\)是集合上定义的一个函数,
如果,\(Ssubseteq D\),则\(f(S)\)为\(E\)的子集,
其中\(f(S)=lbrace f(d)| din S rbrace\)。
对于任意的\(d,d'in D\),如果\(dleqslant d'\)就有\(f(d)leqslant f(d')\),
我们就说\(f\)是单调的。
可以看出,如果\(f\)是单调的,且\(S\)是\(D\)的有向子集,那么\(f(S)\)也是\(E\)的有向子集。
如果\(f\)是单调的,且对于任意有向子集\(Ssubseteq D\),
有\(f(bigvee S)=bigvee f(S)\),就称\(f\)是连续的。
连续函数集上的偏序结构
完全偏序集\((D,leqslant )\)和\((E,leqslant )\)上的连续也可以定义偏序结构,
我们称\(fleqslant g\),当且仅当对于每一个\(din D\),我们有\(f(d)leqslant g(d)\)。
这样我们就得到了一个元素为连续函数的偏序集,\((Drightarrow E,leqslant )\)。
可以证明,\((Drightarrow E,leqslant )\)也是一个完全偏序集。(证略
最小不动点定理
如果\((D,leqslant )\)是一个完全偏序集,且\(f:Drightarrow D\)是连续的,
则\(f\)有最小不动点,\(fix_D f=bigvee lbrace f^n(perp )| ngeqslant 0 rbrace \)。
因为\(perp \)是\(D\)中的最小元,且\(f(perp )in D\),所以,\(perp leqslant f(perp )\),
因为\(f\)是连续的,所以\(f\)也一定是单调的,所以,\(f(perp )leqslant f^2(perp )\),
继而,\(f^n(perp )leqslant f^{n+1}(perp )\),对于任意的\(ngeqslant 0\)都成立。
\(lbrace f^n(perp )| ngeqslant 0 rbrace\)构成了一个全序集,
所以,它是完全偏序集\((Drightarrow E,leqslant)\)的一个有向子集,必有上确界。
设\(a\)是上确界,\(a=bigvee lbrace f^n(perp )| ngeqslant 0 rbrace \),
首先\(a\)是\(f\)的不动点,因为,由\(f\)的连续性,
\(f(a)=f(bigvee lbrace f^n(perp )| ngeqslant 0 rbrace )\)
\(f(a)=bigvee lbrace f^{(n+1)}(perp )| ngeqslant 0 rbrace \),
但是由于\(lbrace f^n(perp ) rbrace\)与\(lbrace f^{(n+1)}(perp ) rbrace\),有同样的上确界,
所以,\(f(a)=a\)。
其次,\(a\)是\(f\)的最小不动点,
假设\(b=f(b)\)是\(f\)的任意不动点,因为\(perp leqslant b\),所以\(f(perp )leqslant f(b)\),
类似的,对于任意的\(ngeqslant 0\),\(f^n(perp )leqslant f^n(b)\)。
但是,由于\(b\)是\(f\)的不动点,所以\(f^n(b)=b\),
因此\(b\)是集合\(lbrace f^n(perp )| ngeqslant 0 rbrace\)的上界。
由于集合的最小上界是\(a\),所以有\(aleqslant b\)。
后继函数的不动点
succ :: Int -> Int
succ n = n+1
在第七篇中,我们说fix
可以得到任意函数的不动点,
那么这个succ
函数呢?它有没有不动点?fix succ
是什么?
现在我们有了最小不动点定理,
就得验证succ
所指称的数学函数,是不是一个完全偏序集上的连续函数,
如果是的话,它就有不动点。
在第四篇为了表示计算的不可终止性,我们对自然数集进行了扩充,\(Ncup lbrace perp rbrace\),
然后用这个集合作为程序中Int
类型的值的解释。
然而,\(Ncup lbrace perp rbrace\)不是一个完全偏序集,原因是它没有上界,
如果我们额外加入一个比其他的自然都大的元素\(+infty \),
则我们就得到了一个完全偏序集,\(Ncup lbrace perp rbracecup lbrace +infty rbrace\)。
然后,我们看succ
连续吗?
首先,它是单调的,如果我们再定义\(succ(+infty )=+infty \),
就有\(succ(bigvee N)=bigvee succ(N)\),
因此,succ
是一个连续函数。
根据最小不动点定理,succ
的最小不动点是,\(fix succ=bigvee lbrace succ^n(perp )| ngeqslant 0 rbrace \)。
由于\(succ(perp )=perp \),即对于非终止的输入succ
的计算也不会终止,
所以\(succ^n(perp )=perp \),
因此,\(fix succ=bigvee lbrace succ^n(perp )| ngeqslant 0 rbrace =perp \),
即,succ
的最小不动点是\(perp \),fix succ
的计算不会终止。
求解阶乘函数
上一篇中,我们证明了阶乘函数fact
是以下函数的不动点,fact = fix g
,
g :: (Int -> Int) -> Int -> Int
g f n = case n of1 -> 1_ -> n * f (n-1)
现在我们来看一下,如何运用最小不动点定理来得到这个答案。
为了避免篇幅过长,关于g
函数的连续性证明暂略,
我们直接使用公式,
\(fix g=bigvee lbrace g^n(perp )| ngeqslant 0 rbrace \),
即,g
函数的最小不动点,就是集合\(D=lbrace g^n(perp )| ngeqslant 0 rbrace\)的上确界。
我们先来看一下这个集合\(D\)中有哪些元素,
其中,\(g(perp )in D\),我们将\(perp \)传入\(g\)中,看看会得到什么,
f1 = \n -> case n of1 -> 1_ -> ...
这个函数能计算f1 1
,但是不能计算f1 2
,恰好是fact
函数有限展开的一阶项。
我们再来看\(g^2(perp )in D\),它等于\(g(f1)\),
f2 = \n -> case n of1 -> 1_ -> n * f1 (n-1)
这个函数能计算f2 1
以及f2 2
,但是不能计算f2 3
,恰好是fact
函数展开的二阶项。
由此,我们看出了规律,
\(g^n(perp )in D\)就是fact
函数有限展开的第\(n\)阶项。
上一篇中,我们已经证明了,当\(nrightarrow infty\)时,它就是fact
函数,
考虑到\(f1,f2,cdots\)这些函数的序关系,
因此,我们有\(fact=bigvee lbrace g^n(perp )| ngeqslant 0 rbrace \)。
即,fact
函数就是g
函数的最小不动点。
总结
到此为止,我想这个系列的文章已经讨论完了,
本系列文章一直围绕着递归函数和不动点进行分析,
在内容上可以分为两个部分,前半部分主要与可计算性理论有关,
后半部分与不动点定理有关,希望对大家有所帮助。
参考
有向集合
完全偏序
Kleene fixed-point theorem
Foundations for Programming Languages