函数式编程中的 fix
先看看 fix 是什么
这是 fix
在 Haskell 中的定义:
fix :: (a -> a) -> a
fix f = let x = f x in x
哇!好怪,这个 x
是什么?我们好像只能知道它满足 x = f x
,但是这个值具体是怎么求的呢?
那我们还是先看看 fix
的应用吧
通常我们会这样定义阶乘。
fact :: Int -> Int
fact 0 = 1
fact n = n * fact (n - 1)
如果转换成 lambda 表达式呢?
fact :: Int -> Int
fact = \n -> if n == 0
then 1
else n * _ (n - 1)
这个 _
应该填什么?对照上文的代码,我们应该要填入一个 fact
。但是在这个 lambda 表达式中,fact
还没有被定义…
那我们可以试着多传一个参数进去。
fact :: (Int -> Int) -> Int -> Int
fact f = \n -> if n == 0
then 1
else n * f (n - 1)
也就是说,我们需要向 fact
提供一个真正的阶乘函数来得到一个阶乘函数。按照这样的想法,我们可以写出这样的代码:
realFact :: Int -> Int
realFact = fact realFact
咦 x = f x
,这不就是上面的 fix
吗?于是我们可以把 fact
定义成这样:
fact :: Int -> Int
fact = fix $ \f n ->
if n == 0
then 1
else n * f (n - 1)
唔 那再给出几个常见的递归函数的 fix
实现以供参考。
fib :: Int -> Int
fib = fix $ \f n ->
case n of
0 -> 1
1 -> 1
n' -> f (n' - 1) + f (n' - 2)
eq :: Int -> Int -> Bool
eq = fix $ \f n m ->
if n == 0
then m == 0
else f (n - 1) (m - 1)
那 fix
是怎么计算的呢
参考 SF-PLF-MoreStlc 一节中对 fix
的形式化定义,可以写出两条规约公式:
那么,我们试着依照这个规则来计算 fact 2
。
fact 2
=> fix (\f n -> if n == 0 then 1 else n * f (n - 1)) 2
=> (\n -> if n == 0 then 1 else n * fact (n - 1)) 2
=> if 2 == 0 then 1 else 2 * fact (2 - 1)
=> 2 * fact 1
=> 2 * (fix (\f n -> if n == 0 then 1 else n * f (n - 1))) 1
=> 2 * (\n -> if n == 0 then 1 else n * fact (n - 1)) 1
=> 2 * (if 1 == 0 then 1 else 1 * fact (1 - 1))
=> 2 * 1 * fact 0
=> 2 * 1 * (fix (\f n -> if n == 0 then 1 else n * f (n - 1))) 0
=> 2 * 1 * (\n -> if n == 0 then 1 else n * fact (n - 1)) 0
=> 2 * 1 * (if 0 == 0 then 1 else 1 * fact (0 - 1))
=> 2 * 1 * 1
=> 2
从不动点的角度理解 fix
回到 x = f x
,我们可以发现 x
就是 f
的一个不动点。
也就是说,对于某些点 ,令 。当 时,
而对于 fact
,先令 ft = \f n -> if n == 0 then 1 else n * f (n - 1)
。
如果我们令 x0 = id
:
ft id
可以正确计算所有
ft $ ft id
可以正确计算所有
ft $ ft $ ft id
可以正确计算所有
…
最终,我们有 fact = ft fact
,也就是说 fact
是 ft
的一个不动点。对 id
反复迭代 ft
就能逐渐逼近 fact
。(实际上 id
可以换成任意一个类型为 Int -> Int
的函数)
值得一提的是,coq 中定义递归函数的关键字就是
Fixpoint
fix
在 utlc 中的实现
不难发现,虽然我们通过 fix
实现了递归,但是在 stlc 中定义 fix
本身仍需要递归实现。
而在 utlc 里,我们可以通过 Y-Combinator
来实现 fix
。
#lang lazy
(define (y-comb f)
((λ (x) (f (x x)))
(λ (x) (f (x x)))))
(define fact
(y-comb
(λ (f)
(λ (x)
(if (= 0 x)
1
(* x (f (- x 1))))))))
这里使用
lazy
是因为Y-Combinator
并不支持 strict。如果在 strict 下想实现fix
可以参考Z-Combinator
呜呜 这个 y-comb
看起来比前面那个还奇怪。让我们来代入一个 g 试试
这样就得到了与前面 fix
相同的表达式。y-comb
也就实现无中生有递归啦!