Haskell/Fix 和递归
fix 函数乍看上去非常难以理解. 但是, 它有着一个有用的理论用途: 使用它来定义递归函数, 并引入有类型 lambda 演算.
引入 fix
[编辑]首先我们来看一看 fix 的实现:
fix :: (a -> a) -> a fix f = let x = f x in x
我们很难一眼看出这个函数想实现什么. fix f 似乎会产生一串无穷的 f 调用: f (f (f (... )))? 这时就要用到我们的老朋友, 懒惰计算了. 一般来说, 这串无穷的 f 调用当且仅当 f 是懒惰时才会收敛到某个值. 让我们看一些例子:
例子: fix 的例子
Prelude> :m Control.Monad.Fix Prelude Control.Monad.Fix> fix (2+) *** Exception: stack overflow -- 栈溢出 Prelude Control.Monad.Fix> fix (const "hello") "hello" Prelude Control.Monad.Fix> fix (1:) [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,...
我们首先从 Control.Monad.Fix 模块中导入 fix (Data.Function 模块中也有相同的定义). 然后我们来看看这些例子. 因为 fix 的内容是如此简洁, 我们可以试着展开它:
fix (2+) = 2 + (fix (2+)) = 2 + (2 + fix (2+)) = 2 + (2 + (2 + fix (2+))) = 2 + (2 + (2 + (2 + fix (2+)))) = ...
显然, 这个表达式永远不会收敛至任何值. 我们来试着展开下一个例子:
fix (const "hello") = const "hello" (fix (const "hello")) = "hello"
现在情况有些不同了: 我们发现, 在展开一层 fix 调用后, 因为 const 总是忽略它的第二个参数, 计算就此结束; 换句话说, 表达式收敛了. 最后一个例子又有些不同, 但我们的方法还是差不多的:
fix (1:) = 1 : fix (1:) = 1 : (1 : fix (1:)) = 1 : (1 : (1 : fix (1:)))
虽然这看起来并不会收敛至某个值, 但是我们注意到, 当我们在 GHCi 中输入 fix (1:) 时, GHCi 所做的仅仅是试图将 show 应用到这个表达式上. 因此我们或许可以看看 show (fix (1:)) 是如何被求值的 (简洁起见, 我们假定 show 并不会在列表里的元素间插入逗号).
show (fix (1:)) = "[" ++ map show (fix (1:)) ++ "]" = "[" ++ map show (1 : fix (1:)) ++ "]" = "[" ++ "1" ++ map show (fix (1:)) ++ "]" = "[" ++ "1" ++ "1" ++ map show (fix (1:)) ++ "]"
因此, 即使对表达式 map show (fix (1:)) 的计算永远不会终止, 我们仍然能够得到一个结果: GHCi 仍然能够打印出字符串的开头, "[" ++ "1" ++ "1", 并且当 map show (fix (1:)) 产生字符串的剩余部分时将它们打印出来. 这里懒惰计算开始起作用了: 打印函数不需要得到整个输入后才能够开始工作.
最后, 这是一个计算一个数平方根逼近的算法,
fix (\next guess tol val -> if abs(guess^2-val) < tol then guess else
next ((guess + val / guess) / 2.0) tol val) 2.0 0.0001 25.0
= let f next guess tol val = if abs(guess^2-val) < tol then guess else
next ((guess + val / guess) / 2.0) tol val
in fix f 2.0 0.0001 25.0
= let f ... = ...
in f (fix f) 2.0 0.0001 25.0 -- next = fix f = f (fix f) = f next ...
= 5.000000000016778
| 练习 |
|---|
|
如果以下表达式收敛的话, 它们会收敛成什么?
|
fix 和不动点
[编辑]一个函数 f 的不动点 是一个值 a 使得 f a == a. 比如说, 0 是函数 (* 3) 的不动点, 因为 0 * 3 == 0. 这也是 fix 的名字 ("固定") 的由来: 它将找到一个函数的最小不动点. (稍后我们将解释"最小"的含义.) 我们可以注意到, 对于以上两个收敛的例子, 我们可以看到:
const "hello" "hello" -> "hello" (1:) [1,1,..] -> [1,1,...]
而没有一个数 x 能够使 2+x == x 成立, 因此 fix (2+) 不收敛.
| 练习 |
|---|
对于前一个练习模块中的所有形如 fix f 的表达式, 如果你认为其收敛的话, 验证 fix f 确实会得出一个不动点. |
事实上, 从 fix 的定义中我们就能看出, 显然当它收敛时我们就找到了一个不动点. 我们只需将 fix 的定义反过来:
f (fix f) = fix f
这恰恰就是不动点的定义! 因此 fix 应该总是找到一个不动点. 但有时 fix 似乎并不能找到一个不动点 (换句话说, 不能收敛). 然而我们能够使用指称语义修复这一个漏洞. 所有的 Haskell 类型事实上都有着一个对应的此类型的值, 称为 bottom, 写做 ⊥. [1] 举个例子, 类型为 Int 的值实际上不仅仅有 1, 2, 3, 还有 ⊥. 发散的计算我们用 ⊥ 来表示, 举个例子, fix (2+) = ⊥.
特殊值 undefined 也同样用 ⊥ 来表示. 现在我们能够明白 fix 是如何找到 (2+) 函数的不动点的了:
例子: (2+) 的不动点
Prelude> (2+) undefined *** Exception: Prelude.undefined
也就是说, 将 undefined (⊥) 传递给 (2+) 后我们仍将得回 undefined. 因此 ⊥确实是 (2+) 的一个不动点!
在 (2+) 一例中, 这就是唯一的不动点了. 然而, 存在一些函数 f, 其存在一个或多个不动点, 但是 fix f 依旧发散: fix (*3) 是发散的, 但我们能够注意到 0 时此函数的一个不动点. 这时就需要我们之前提到的"最小"定义了. Haskell 中的类型都形成一个偏序集, 被称为定义性 (definedness). 对于任何类型, ⊥ 都有着最小的定义性 (因此叫做 "bottom", 译作"底部"). 对于 Int 之类的初级类型, 这个偏序集中只存在 ⊥ ≤ 1, ⊥ ≤ 2 以及之类的关系. 对于任何非 bottom 的 Int 值 m, n, 我们不定义它们之间存在关系. 对于其他的简单类型, 譬如 Bool 和 (), 我们作同样的规定. 对于"多层次"的类型, 比如 Maybe 和列表, 情况稍稍复杂一些, 可以参见指称语义.
那么, 由于 ⊥ 是任何类型的最小定义性的值, 而 fix 依据定义将返回最小定义性的不动点, 若 f ⊥ = ⊥, 则我们有 fix f = ⊥ (反之亦然). 如果你读了上面引用的指称语义的文章 (当然不读也并无大碍), 你会发现这是严格函数的定义.[2]: fix f 离散当且仅当 f 是严格的.
递归
[编辑]如果你已经见过一些 fix 的例子, 有可能它们涉及了 fix 和递归. 这里我们来看一个经典的例子:
例子: 使用 fix 来表示递归
Prelude> let fact n = if n == 0 then 1 else n * fact (n-1) in fact 5 120 Prelude> fix (\rec n -> if n == 0 then 1 else n * rec (n-1)) 5 120
这里我们使用了 fix 来"表示"阶乘函数: 我们可以注意到 (如果我们将 fix 看做"语言的一部分") 我们的第二个阶乘定义并没有使用递归. 在一门例如有类型 lambda 演算(因为无法命名, 所以不能递归)这样没有递归的语言中, 我们可以使用 fix 来表示递归函数:
例子: More fix examples
Prelude> fix (\rec f l -> if null l then [] else f (head l) : rec f (tail l)) (+1) [1..3] [2,3,4] Prelude> map (fix (\rec n -> if n == 1 || n == 2 then 1 else rec (n-1) + rec (n-2))) [1..10] [1,1,2,3,5,8,13,21,34,55]
它是如何工作的? 我们先从指称语义的角度分析一下 fact 函数. 简洁起见, 我们定义:
fact' rec n = if n == 0 then 1 else n * rec (n-1)
这和上面的例子里的实际上是同一个函数, 只是我们为匿名 lambda 函数命名了; 因此我们现在可以写成 fix fact' 5 了. fix 会找到 fact' 函数的一个不动点, 换句话说, 一个使得 f == fact' f 的函数 f. 我们将这个式子展开:
f = fact' f = \n -> if n == 0 then 1 else n * f (n-1)
我们所做的仅仅是将在 fact' 的定义中将 rec 替换成 f. 但现在这个定义已经被变换成阶乘函数的递归形式了! fix 将 fact' 作为第一个参数传递给它自己以用一个高阶函数构造出一个递归的函数.
我们也可以从实际运行状况的角度考虑. 我们把 fix fact' 的定义展开:
fix fact'
= fact' (fix fact')
= (\rec n -> if n == 0 then 1 else n * rec (n-1)) (fix fact')
= \n -> if n == 0 then 1 else n * fix fact' (n-1)
= \n -> if n == 0 then 1 else n * fact' (fix fact') (n-1)
= \n -> if n == 0 then 1
else n * (\rec n' -> if n' == 0 then 1 else n' * rec (n'-1)) (fix fact') (n-1)
= \n -> if n == 0 then 1
else n * (if n-1 == 0 then 1 else (n-1) * fix fact' (n-2))
= \n -> if n == 0 then 1
else n * (if n-1 == 0 then 1
else (n-1) * (if n-2 == 0 then 1
else (n-2) * fix fact' (n-3)))
= ...
我们可以注意到, fix 使得我们可以不停地"展开" fact': 每次我们进入 else 分支时, 我们都籍由 fix fact' = fact' (fix fact') 构造出一次对 fact'的调用, 由此进入了递归链中的下一层. 直到最终我们进入 then 分支, 达到递归链的底部.
| 练习 |
|---|
|
本节我们将拓展之前提到的一点: 用 fix 在有类型 lambda 演算中如何使用 fix 表示递归函数. 我们假定你已经碰到过有类型 lambda 演算了. 回忆一下, 在有类型 lambda 演算中, 我们不能使用 let 或顶层绑定. 每一个程序都是简单的 lambda 抽象, 应用和字面常量. 假设我们想写一个 fact 函数; 假定我们有表示自然数的 Nat 类型, 这个函数大致会是这样:
λn:Nat. if iszero n then 1 else n * <???> (n-1)
问题是, 在 <???> 处我们应该填入什么呢? 我们不能对函数命名, 因此我们不能递归调用自己. 唯一一种将表达式绑定至一个名字的方法是使用一个抽象, 我们试一试:
(λf:Nat→Nat. λn:Nat. if iszero n then 1 else n * f (n-1)) (λm:Nat. if iszero m then 1 else m * <???> (m-1))
展开:
λn:Nat. if iszero n then 1
else n * (if iszero n-1 then 1 else (n-1) * <???> (n-2))
我们仍然有一个讨厌的 <???>. 我们可以试着加入更多层:
(λf:Nat→Nat. λn:Nat. if iszero n then 1 else n * f (n-1)
((λg:Nat→Nat. λm:Nat. if iszero n' then 1 else n' * g (m-1))
(λp:Nat. if iszero p then 1 else p * <???> (p-1))))
->
λn:Nat. if iszero n then 1
else n * (if iszero n-1 then 1
else (n-1) * (if iszero n-2 then 1 else (n-2) * <???> (n-3)))
很明显, 不管我们命名多少次都无法消除 <???>. 除非我们使用 fix —— 它使得我们能够无需命名进入下一层递归:
fix (λf:Nat→Nat. λn:Nat. if iszero n then 1 else n * f (n-1))
这是有类型 lambda 演算中使用 fix 实现的一个完美的阶乘函数.
在有类型 lambda 演算之外, fix 还有一个有趣的特性: 如果我们把它引入一门语言中, 那么任何类型都是居留(至少有一个该类型的值)得了, 因为对于任意类型 T, 都能构造出以下类型为 T 的表达式:
fix (λx:T. x)
这个表达式, 用 Haskell 的话来说, 其实是 fix id, 指称语义中写作 ⊥. 因此我们发现, 只要我们将 fix 引入有类型 lambda 演算中, 并不是所有项都能规约成一个值了.
作为数据类型的 Fix
[编辑]我们能够在 Haskell 中定义一个 fix 数据类型.
有三种方式来定义这个类型.
newtype Fix f = Fix (f (Fix f))
或者使用 RankNTypes 扩展
newtype Mu f=Mu (forall a.(f a->a)->a) data Nu f=forall a.Nu a (a->f a)
Mu 和 Nu 能够帮助我们推广 folds, unfolds 和 refolds.
fold :: (f a -> a) -> Mu f -> a fold g (Mu f) = f g unfold :: (a -> f a) -> a -> Nu f unfold f x = Nu x f refold :: (a -> f a) -> (g a-> a) -> Mu f -> Nu g refold f g = unfold g . fold f
Mu 和 Nu 是受限的 Fix. Mu 可用来构造归纳有限值 (inductive noninfinite data), Nu 可用来构造反归纳无限值 (coinductive infinite data). 例如:
newpoint Stream a = Stream (Nu ((,) a)) -- forsome b. (b, b -> (a, b)) newpoint Void a = Void (Mu ((,) a)) -- forall b. ((a, b) -> b) -> b
和不动点函数不同, 不动点数据类型并不会得出 ⊥. 在下例中 Bot 是良定义的. 它和单位类型 () 同构.
newtype Id a = Id a newtype Bot = Bot (Fix Id) -- 相等性 newtype Bot = Bot Bot -- 只有一个合法的值. Bot $ Bot $ Bot $ Bot ..,
Fix 数据类型并不能实现所有形式的递归. 例如这个不规则的数据类型.
data Node a = Two a a | Three a a a data FingerTree a = U a | Up (FingerTree (Node a))
用 Fix 将它构造出来并不容易.
| Fix 和递归 |
| 习题解答 |
| 理论提升 |
|
指称语义
>> Equational reasoning
>> Program derivation
>> Category theory
>> The Curry-Howard isomorphism
>> |
| Haskell |
|
Haskell基础
>> 初级Haskell
>> Haskell进阶
>> Monads
|
注
[编辑]- ↑ 关于这一点, 可以参见类型居留问题和在Haskell里，每个类型都可以构造出来一个此类型的表达式吗？中更详细的解释
- ↑ 遗憾的是中文维基百科词条中并没有提到这个定义.