函数式编程中的 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 的形式化定义，可以写出两条规约公式：

$\frac{t \rarr t'}{\text{fix } t \rarr \text{fix } t'}$

$\frac{}{\text{fix } (\lambda f.t)\rarr [f:=\text{fix } (\lambda f.t)]\,t}$

那么，我们试着依照这个规则来计算 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 的一个不动点。

也就是说，对于某些点 $x_0$，令 $x_n = f(x_{n-1})$。当 $n\rarr +\infty$ 时，$x_n = f(x_n)$

而对于 fact，先令 ft = \f n -> if n == 0 then 1 else n * f (n - 1)。

如果我们令 x0 = id：

ft id 可以正确计算所有 $n \leq 0$

ft $ ft id 可以正确计算所有 $n \leq 1$

ft $ ft $ ft id 可以正确计算所有 $n \leq 2$

…

最终，我们有 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 试试

$\begin{aligned} Y\, g &= (\lambda f . (\lambda x . f (x x)) (\lambda x . f(x x))) g \\ &= (\lambda x . g (x x)) (\lambda x . g (x x)) \\ &= g\, ((\lambda x . g (x x)) (\lambda x . g(x x))) \\ &= g\, (Y\, g) \end{aligned}$

这样就得到了与前面 fix 相同的表达式。y-comb 也就实现无中生有递归啦！