递归函数(七):不动点算子

回顾

以上几篇文章中,我们讨论了可计算性理论相关的一些内容,

可计算性与递归函数论存在着千丝万缕的联系,

不动点理论也是这样的,我们定义的递归函数一定存在吗?

在什么情况下它是存在的?


要回答以上这些问题,还要从方程,不动点,不动点算子说起。


约束方程



在中学时代,我们学过“方程”的概念,

方程可以简单表述为含有未知数的等式,例如,

未知数可以同时出现在等式的两边,例如,

通过合并同类项,我们可以求解


在大学时代,我们还学过线性方程组和微分方程,

例如,求解矩阵的特征值和特征向量,

二阶常微分方程(贝塞尔方程),


在计算机科学中,同样的未知“数”的思想,

还出现在了类型推导(例如:unification)与递归函数的定义中。


以上这些例子,方程是“约束”的一种表现形式。


我们回到最简单的阶乘函数fact的定义式,

1
2
3
fact :: Int -> Int
fact 1 = 1
fact n = n * fact (n-1)


去掉语法糖,稍微修改一下,

1
2
3
4
fact :: Int -> Int
fact n = case n of
1 -> 1
n -> n * fact (n-1)


我们发现,fact的定义和“方程”十分相似,fact同时出现在了等式的两边,

阶乘函数,就是这个“方程”的“解”。


函数的不动点



在中学数学中,我们已经学过不动点了,只是当时印象不是那么深刻,

函数的不动点,是指被这个函数映射到其自身的那些点。

例如:

是函数的一个不动点,


并不是每一个函数都有不动点,

例如,实数域上的函数,就没有不动点,对于任意实数,永远都不等于

(不动点是和定义域有关的,以后我们还会重新讨论的不动点。


一般的,函数的不动点,指的是这样的,使得


重新温习了不动点相关的知识之后,

我们就可以对上面的阶乘函数进行改造了,

我们要把阶乘函数看做另外一个函数的不动点。


定义函数

1
2
3
4
g :: (Int -> Int) -> Int -> Int
g f n = case n of
1 -> 1
n -> n * f (n-1)

我们可以得到,g fact = fact

因此,fact实际上就是函数g的不动点。


于是,在“方程”中求解fact的过程,

就转换成了求解函数g的不动点的过程了。


不动点算子



我们怎样求解函数g的不动点呢?

在Haskell中,可以很方便的定义一个高阶函数fix,它可以用来求解任意函数的不动点,

1
2
fix :: (a -> a) -> a
fix g = let x = g x in x


我们试验一下fix的强大威力,

1
2
3
4
5
fact 10
> 3628800

fix g 10
> 3628800


注意,fix g得到的是g的不动点,而不是fact的不动点,

(fix g) = g (fix g)


有了fix,我们就可以构造匿名递归函数了,

1
2
3
4
fact' :: Int -> Int
fact' = fix $ \fact -> \n -> case n of
1 -> 1
n -> n * fact (n-1)

fix后面跟的函数没有名字,它是匿名的,但是经过fix作用后,可以产生一个递归函数。

也就是说,为了实现递归,函数是可以没有名字的。


Y组合子



Y组合子,是Haskell B. Curry在研究演算时发现的,

它的表现形式如下,


演算中,(转换和规约

我们可以证明,对于任何函数g


因此,Y组合子是一个不动点算子,它可以得到任意函数的不动点。

其他的不动点算子还有图灵不动点组合子


讨论Y组合子在Haskell中的表示方式是有趣的,因为直接翻译过去会报类型错误,

1
2
3
4
5
6
7
8
y :: (a -> a) -> a
y = \f -> (\x -> f (x x)) (\x -> f (x x))

-- Occurs check: cannot construct the infinite type: r0 ~ r0 -> a
-- Expected type: r0 -> a
-- Actual type: (r0 -> a) -> a
-- In the first argument of ‘x’, namely ‘x’
-- In the first argument of ‘f’, namely ‘(x x)’

类型系统无法确定x的类型。


问题出在表达式x x上面,

假设x x的类型为a,则第一个x的类型就应该为? -> a

于是,第二个x的类型肯定也应该是? -> a。(因为都是x


又因为x x的类型为a

所以第一个x的类型? -> a中,?的类型就应该是? -> a

(因为((? -> a) -> a)作用到(? -> a)才能得到a


?的类型是? -> a,因此?应该是一个递归类型


下面我们来定义递归类型Mu,来帮助编译器进行恰当的类型推导,

1
2
3
4
newtype Mu a = Mu (Mu a -> a)

y :: (a -> a) -> a
y f = (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x)


最后,fact'就可以使用Y组合子来定义了。

1
2
3
4
fact' :: Int -> Int
fact' = y $ \fact -> \n -> case n of
1 -> 1
n -> n * fact (n-1)


总结

本文从简单的“方程”思想出发,引出了不动点的概念,

然后把递归函数看做了另外一个函数的不动点,

最后,我们讨论了Y组合子这样一个具体的不动点算子。


可是,这里隐藏着一个问题,我们看到fix是可以求解任意函数的不动点的,

而对于以下递归函数succ,即

1
2
succ :: Int -> Int
succ n = n+1

在实数域上是显然没有不动点的。


那么fix succ是什么呢?

这个问题,我们将在后文中继续讨论。


参考

方程

特征值和特征向量

微分方程

不动点

不动点组合子

Haskell/Fix and recursion

Y Combinator in Haskell