不动点算子

**不動點組合子**（英語：Fixed-point combinator，或**不動點算子**）是計算其他函數的一個不動點的高階函數。

函數 **f** 的不動點是將函數應用在輸入值 x 時，會傳回與輸入值相同的值，使得 **f**(x) = x。例如，0 和 1 是函數 **f**(x) = x2 的不動點，因為 02 = 0 而 12 = 1。鑑於一階函數（在簡單值比如整數上的函數）的不動點是個一階值，高階函數 **f** 的不動點是另一個函數 **g** 使得 **f**(**g**) = **g**。那麼，不動點算子 **fix** 的定義是

　
: $x=f\ x$

使得對於任何函數 f

　
: ${\textsf {fix}}\ f=f\ ({\textsf {fix}}\ f)$

不動點組合子它們可以用非遞歸的 lambda 抽象來定義，在 lambda 演算中的函數都是匿名的。然而在命令式編程語言中的遞歸，或許限制只能以呼叫函數名稱作為參數來實作。在函數式編程語言中的不動點，以 lambda 抽象來定義的 **Y** 組合子為：

　
: ${\textsf {Y}}=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))$

則允許匿名函數足夠逹成遞歸的作用，即遞歸函數。應用於帶有一個變量的函數，**Y** 組合子通常不會終止。將 **Y** 組合子應用於二或更多個變量的函數，會獲得更有趣的結果。第二個變量可當作計數器或索引。由此產生的函數行為，表現出如命令式語言中一個 `while` 或 `for` 迴圈。

這個組合子也是 Curry 悖論的核心，演示了無型別的 lambda 演算是一個不穩固的推論系統，因由 **Y** 組合子允許一個匿名表達式來表示零或者甚至許多值，這在數理邏輯上是不一致的。

## 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**)))

## 參見

* 組合子邏輯
* lambda 演算
* 有類型 lambda 演算

## 外部連結

* http://okmij.org/ftp/Computation/fixed-point-combinators.html（頁面存檔備份，存於網際網路檔案館）
* http://www.cs.brown.edu/courses/cs173/2002/Lectures/2002-10-28-lc.pdf（頁面存檔備份，存於網際網路檔案館）
* http://www.mactech.com/articles/mactech/Vol.07/07.05/LambdaCalculus/（頁面存檔備份，存於網際網路檔案館）
* http://www.csse.monash.edu.au/~lloyd/tildeFP/Lambda/Examples/Y/（executable）
* https://web.archive.org/web/20060719181315/http://www.ececs.uc.edu/~franco/C511/html/Scheme/ycomb.html
* http://stackoverflow.com/questions/93526/what-is-a-y-combinator（頁面存檔備份，存於網際網路檔案館）