不動点コンビネータ

不動点コンビネータ - Wikipedia

不動点コンビネータ (fixed point combinator) は与えられた関数の不動点を求める高階関数

不動点

写像の不動点とは、その写像によって自分自身に写される点のこと。

$x$ が写像 $f$ の不動点であるとは、$f(x)=x$ が成り立つこと。

高階関数 $g$ が不動点コンビネータであるとは、任意の関数 $f$ に対し、$p=g(f)$ とすると $f(p)=p$ が成立する、つまり、

$$f(g(f))=g(f)$$

が成立することである。

無名再帰

無名再帰とは、名前に束縛されない無名関数において再帰を行うこと。 自分自身が名前を持たないため、工夫が必要になる。

ラムダ計算においては、引数には名前があることを利用して、不動点コンビネータを利用して再帰を行う。

不動点コンビネータによる無名再帰

再帰的な関数 $a$ があるとき、$a$ の定義式は高階関数 $U$ を用いて

$$a(x)=U(a,x)$$

と書ける。 $a$ の定義に $a$ 自身が登場するということである。

$U$ をカリー化して高階関数 $V$ を

$$V:f\mapsto U(f,\cdot )$$

のように定義する。

$g$ を不動点コンビネータとするとき、$V$ の不動点 $g(V)$ は関数であり、$g(V)$ は再帰関数 $a$ と一致する (証明は後述)。 このことを利用して無名再帰ができる。

$a$ と同じ働きをする無名関数を得たい。 まず $U$ を定義する。 次に $U$ をカリー化して $V$ を得る。 $g(V)$ は再帰が可能な無名関数であり、これは $a$ と同じである。

$g(V)=a$ の証明

不動点コンビネータの定義より

$$V(g(V))=g(V)$$

となる。 値 $x$ に対して

$$\begin{array}{rl}g(V)(x)& =V(g(V))(x)\\ & =U(g(V),x)\end{array}$$

つまり

$$g(V)(x)=U(g(V),x)$$

これは

$$a(x)=U(a,x)$$

の $a$ を $g(V)$ で置き換えたものである。 これは $a$ の再帰的な定義式だったので、$g(V)$ が $a$ の定義式を満たすことがわかる。 そのため

$$a=g(V)$$

が成立する。

不動点コンビネータの例

ここでの型無しラムダ計算の EBNF は以下の通り。 自明な場合でもカッコの省略はしない。 カッコはすべて関数適用であり、式自体をカッコで囲むことはしない。

expr = "(", expr, expr, ")"  ? 関数適用 ?
     | "λ", IDENTIFIER, ".", expr  ? ラムダ関数 ?
     | IDENTIFIER

Y コンビネータ

型無しラムダ計算における不動点コンビネータの 1 つ。 ハスケル・カリーによって発見された。

Y = λf.(λx.(f (x x)) λx.(f (x x)))

実際の適用過程

(Y e) = (λf. (λx.(f (x            x           )) λx.(f (x x))) e)  -- Y の定義より
      =      (λx.(e (x            x           )) λx.(e (x x)))     -- β 簡約
      =      (λy.(e (y            y           )) λx.(e (x x)))     -- α 変換
      =          (e (λx.(e (x x)) λx.(e (x x))))                   -- β 簡約
      =          (e (Y e))                                         -- 2 行目より

Z コンビネータ

値渡し評価でも使用可能なバージョンの Y コンビネータである。 Y コンビネータの一部を η 変換することで得られるらしい。

Z = λf.(λx.(f λy.((x x) y)) λx.(f λy.((x x) y)))

---

"上"のページ: 計算理論