http://gengwg.blogspot.com/不动点组合子（英语：Fixed-point combinator，或不动点算子）是计算其他函数的一个不动点的高阶函数。
函数f的不动点是一个值x使得f(x) = x。例如，0和1是函数f(x) = x2的不动点，因为02 = 0而12 = 1。鉴于一阶函数（在简单值比如整数上的函数）的不动点是个一阶值，高阶函数f的不动点是另一个函数g使得f(g) = g。那么，不动点算子是任何函数fix使得对于任何函数f都有
f(fix(f)) = fix(f).
不动点组合子允许定义匿名的递归函数。它们可以用非递归的lambda抽象来定义。
目录 [隐藏]
1 Y组合子
2 不动点组合子的存在性
3 例子
4 其他不动点组合子
5 参见
6 外部链接
Y组合子[编辑]
在无类型lambda演算中众所周知的（可能是最简单的）不动点组合子叫做Y组合子。它是Haskell B. Curry发现的，定义为
Y := λf.(λx.(f (x x)) λx.(f (x x))) 用一个例子函数g来展开它，我们可以看到上面这个函数是怎么成为一个不动点组合子的：
(Y g)
= (λf.(λx.(f (x x)) λx.(f (x x))) g)
= (λx.(g (x x)) λx.(g (x x)))（λf的β-歸約 - 應用主函數於g）
= (λy.(g (y y)) λx.(g (x x)))（α-轉換 - 重命名約束變量）
= (g (λx.(g (x x)) λx.(g (x x))))（λy的β-歸約 - 應用左側函數於右側函數）
= (g (Y g))（Y的定義）
注意Y組合子意圖用于傳名求值策略，因為 (Y g)在傳值設置下會發散（對于任何g）。
不动点组合子的存在性[编辑]
在数学的特定形式化中，比如无类型lambda演算和组合演算中，所有表达式都被当作高阶函数。在这些形式化中，不动点组合子的存在性意味着“所有函数都至少有一个不动点”，函数可以有多于一个不同的不动点。
在其他系统中，比如简单类型lambda演算，不能写出有良好类型（well-typed）的不动点组合子。在这些系统中对递归的任何支持都必须明确的增加到语言中。带有扩展的递归类型的简单类型lambda演算，可以写出不动点算子，“有用的”不动点算子（它的应用总是会返回）的类型将是有限制的。
例如，在Standard ML中Y组合子的传值调用变体有类型∀a.∀b.((a→b)→(a→b))→(a→b)，而传名调用变体有类型∀a.(a→a)→a。传名调用（正规）变体在应用于传值调用的语言的时候将永远循环下去 -- 所有应用Y(f)展开为f(Y(f))。按传值调用语言的要求，到f的参数将接着展开，生成f(f(Y(f)))。这个过程永远重复下去（直到系统耗尽内存），而不会实际上求值f的主体。
例子[编辑]
考虑阶乘函数（使用邱奇数）。平常的递归数学等式
fact(n) = if n=0 then 1 else n * fact(n-1)
可以用lambda演算把这个递归的一个“单一步骤”表达为
F = λf. λx. (ISZERO x) 1 (MULT x (f (PRED x))),
这里的"f"是给阶乘函数的占位参数，用于传递给自身。 函数F进行求值递归公式中的一个单一步骤。 应用fix算子得到
fix(F)(n) = F(fix(F))(n)
fix(F)(n) = λx. (ISZERO x) 1 (MULT x (fix(F) (PRED x)))(n)
fix(F)(n) = (ISZERO n) 1 (MULT n (fix(F) (PRED n)))我们可以简写fix(F)为fact，得到
fact(n) = (ISZERO n) 1 (MULT n (fact(PRED n)))所以我们见到了不动点算子确实把我们的非递归的“阶乘步骤”函数转换成满足预期等式的递归函数。
其他不动点组合子[编辑]
Y组合子的可以在传值调用的应用序求值中使用的变体，由普通Y组合子的部分的η-展开给出：
Z = λf.(λx. f (λy. x x y)) (λx. f (λy. x x y))
Y组合子用SKI-演算表达为
Y = S (K (S I I)) (S (S (K S) K) (K (S I I)))在SK-演算中最简单的组合子由John Tromp发现，它是
Y' = S S K (S (K (S S (S (S S K)))) K)它对应于lambda表达式
Y' = (λx.λy. x y x) (λy.λx. y (x y x))
另一个常见不动点组合子是图灵不动点组合子（阿兰·图灵发现的）:
Θ = (λx.λy.(y (x x y))) (λx.λy.(y (x x y)))它也有一个简单的传值调用形式：
Θv = (λx.λy.(y (λz. x x y z))) (λx.λy.(y (λz. x x y z)))
函数f的不动点是一个值x使得f(x) = x。例如，0和1是函数f(x) = x2的不动点，因为02 = 0而12 = 1。鉴于一阶函数（在简单值比如整数上的函数）的不动点是个一阶值，高阶函数f的不动点是另一个函数g使得f(g) = g。那么，不动点算子是任何函数fix使得对于任何函数f都有
f(fix(f)) = fix(f).
不动点组合子允许定义匿名的递归函数。它们可以用非递归的lambda抽象来定义。
目录 [隐藏]
1 Y组合子
2 不动点组合子的存在性
3 例子
4 其他不动点组合子
5 参见
6 外部链接
Y组合子[编辑]
在无类型lambda演算中众所周知的（可能是最简单的）不动点组合子叫做Y组合子。它是Haskell B. Curry发现的，定义为
Y := λf.(λx.(f (x x)) λx.(f (x x))) 用一个例子函数g来展开它，我们可以看到上面这个函数是怎么成为一个不动点组合子的：
(Y g)
= (λf.(λx.(f (x x)) λx.(f (x x))) g)
= (λx.(g (x x)) λx.(g (x x)))（λf的β-歸約 - 應用主函數於g）
= (λy.(g (y y)) λx.(g (x x)))（α-轉換 - 重命名約束變量）
= (g (λx.(g (x x)) λx.(g (x x))))（λy的β-歸約 - 應用左側函數於右側函數）
= (g (Y g))（Y的定義）
注意Y組合子意圖用于傳名求值策略，因為 (Y g)在傳值設置下會發散（對于任何g）。
不动点组合子的存在性[编辑]
在数学的特定形式化中，比如无类型lambda演算和组合演算中，所有表达式都被当作高阶函数。在这些形式化中，不动点组合子的存在性意味着“所有函数都至少有一个不动点”，函数可以有多于一个不同的不动点。
在其他系统中，比如简单类型lambda演算，不能写出有良好类型（well-typed）的不动点组合子。在这些系统中对递归的任何支持都必须明确的增加到语言中。带有扩展的递归类型的简单类型lambda演算，可以写出不动点算子，“有用的”不动点算子（它的应用总是会返回）的类型将是有限制的。
例如，在Standard ML中Y组合子的传值调用变体有类型∀a.∀b.((a→b)→(a→b))→(a→b)，而传名调用变体有类型∀a.(a→a)→a。传名调用（正规）变体在应用于传值调用的语言的时候将永远循环下去 -- 所有应用Y(f)展开为f(Y(f))。按传值调用语言的要求，到f的参数将接着展开，生成f(f(Y(f)))。这个过程永远重复下去（直到系统耗尽内存），而不会实际上求值f的主体。
例子[编辑]
考虑阶乘函数（使用邱奇数）。平常的递归数学等式
fact(n) = if n=0 then 1 else n * fact(n-1)
可以用lambda演算把这个递归的一个“单一步骤”表达为
F = λf. λx. (ISZERO x) 1 (MULT x (f (PRED x))),
这里的"f"是给阶乘函数的占位参数，用于传递给自身。 函数F进行求值递归公式中的一个单一步骤。 应用fix算子得到
fix(F)(n) = F(fix(F))(n)
fix(F)(n) = λx. (ISZERO x) 1 (MULT x (fix(F) (PRED x)))(n)
fix(F)(n) = (ISZERO n) 1 (MULT n (fix(F) (PRED n)))我们可以简写fix(F)为fact，得到
fact(n) = (ISZERO n) 1 (MULT n (fact(PRED n)))所以我们见到了不动点算子确实把我们的非递归的“阶乘步骤”函数转换成满足预期等式的递归函数。
其他不动点组合子[编辑]
Y组合子的可以在传值调用的应用序求值中使用的变体，由普通Y组合子的部分的η-展开给出：
Z = λf.(λx. f (λy. x x y)) (λx. f (λy. x x y))
Y组合子用SKI-演算表达为
Y = S (K (S I I)) (S (S (K S) K) (K (S I I)))在SK-演算中最简单的组合子由John Tromp发现，它是
Y' = S S K (S (K (S S (S (S S K)))) K)它对应于lambda表达式
Y' = (λx.λy. x y x) (λy.λx. y (x y x))
另一个常见不动点组合子是图灵不动点组合子（阿兰·图灵发现的）:
Θ = (λx.λy.(y (x x y))) (λx.λy.(y (x x y)))它也有一个简单的传值调用形式：
Θv = (λx.λy.(y (λz. x x y z))) (λx.λy.(y (λz. x x y z)))
Comments
Post a Comment
https://gengwg.blogspot.com/