不動点コンビネータ

不動点コンビネータとは、与えられた関数の不動点を求める高階関数である。不動点演算子、パラドキシカル結合子などとも呼ばれる。ここで関数//f//の不動点とは、//f// = //x//を満たすような//x//のことをいう。

すなわち高階関数// が不動点コンビネータであるとは、

任意の関数//f// に対し、//p// = //とすると, //f// = //p// が成立する事を指す。

不動点コンビネータの定義は、任意の関数//f// に対し、

が成立する事であるとも言い換えられる。

第一級関数をサポートしているプログラミング言語では、不動点コンビネータを用いて識別子に束縛されない関数の再帰を定義することができる。そういったテクニックは、しばしば無名再帰と呼ばれる。

不動点コンビネータは高階関数であるため、その歴史はラムダ計算の発達と深く関係している。型無しラムダ計算においては、ハスケル・カリーのY = λf·) )という不動点コンビネータがよく知られている。型無しラムダ計算には無数の不動点コンビネータが存在するが、一方で単純型付きラムダ計算などのより限定的な計算モデルでは、不動点コンビネータは必ずしも存在するとは限らない。

1. 不動点コンビネータによる再帰の実現
--------------------

不動点コンビネータにより、第一級関数をサポートしているプログラミング言語において、明示的に再帰を書かずに再帰を実現する為に用いる事ができる。なお、一般にそういった言語では普通に再帰が使えるので、プログラミングにおいてはパズル的なテクニック以上の意味は無い。一方、循環なく関数の意味を定義する、ということは、計算理論の上では重要である。

まず、再帰関数の性質を簡単に振り返り、記号をいくつか定義する。関数//a// が再帰的に定義されているとき、//a//の定義式は何らかの高階関数//U// を用いて、

...と書ける。たとえば//a// がxの階乗を計算する関数である場合、//U//として

を取る事ができる。上述のように定義された//U// がを満たすのは明らかであろう。

//U// を用いて高階関数を

...と定義する。

//V// の定義より、はそれ自身関数であり、任意の//x// に対し、

...が成り立つ。ここでは関数に//x// を入力したときの値。

さて、// を不動点コンビネータとするとき、不動点コンビネータの定義より特に、は//V// の定義域の元である事が分かる。//V// の定義域は関数の集合だったので、これはすなわちはそれ自身関数である事を意味する。 この関数が式で定義された再帰関数//a// と一致する事を示す事ができる。

よって以下のようにすれば不動点コンビネータ// で再帰関数//a// を実現できる事になる：

//U// のプログラムを書く。
//V// を式のように定義し、とする。

1.1. の証明
--------

最後にが式で定義された再帰関数//a// と一致する事を示す。 不動点コンビネータの定義より、は

...を満たす。

前述したようにはそれ自身関数なので、値//x//に対しを考える事ができる。は以下を満たす：

すなわち

。 ...とを見比べると、はで//a//を に置き換えたものに等しい事が分かる。 は//a// の定義式であったので、これはすなわち が//a// の定義式を満たす事を意味する。 よって

。が成立する事が分かった。

2. 不動点コンビネータの例
--------------

型無しラムダ計算や組合せ論理などの特定の数学的な計算形式化においては、すべての式は高階関数とみなすことができる。これらの形式化では、不動点コンビネータが存在することはすなわち、すべての関数が少なくとも1つの不動点を持つことを意味する。さらに、関数は複数の異なる不動点を持つことができる。

単純型付きラムダ計算などの他のいくつかの体系では、十分に型付けされた不動点コンビネータを書くことはできない。それらの体系で再帰をサポートするには、明示的に言語体系に組み込む必要がある。それでも再帰データ型によって拡張された単純型付きラムダ計算などでは不動点演算子を書くことができるが、ある種の「実用的な」不動点演算子は制限される。多相ラムダ計算では多相不動点コンビネータは型∀a.→aを持つ。

2.1. Yコンビネータ
------------

型無しラムダ計算においてよく知られた不動点コンビネータはYコンビネータと呼ばれる。これはハスケル・カリーによって発見されたもので、次のように定義される。

Y = ) ))実際に関数//g//を適用することによって、この関数が不動点コンビネータとして動作するのが分かる。

これをそのままラムダ計算で使うと、評価戦略が値渡しだった場合には  が ) と展開された後も、引数の値を先に求めようとして )) →...→ )...) のように無限に展開され続けて止まらなくなってしまうので、次節で示すZコンビネータのように修正する。評価戦略が名前渡しの場合はこのまま使える。

このカリーによるコンビネータのみをYコンビネータとすることもあるが、実装などでは不動点コンビネータを指す名前として他の形であってもYという名前を使っていることもある。

SKIコンビネータ計算では次のようになる。

Y = S )  K) ))

2.2. Zコンビネータ
------------

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

Z = λf. ) )Python での実装。その他のプログラミング言語での実装は無名再帰を参照。 Z = lambda f: ))))

利用方法Z)<WtXmlEndTag />

2.3. チューリング不動点コンビネータ
--------------------

もう一つの一般的な不動点コンビネータは、チューリング不動点コンビネータである。

Θ = )) ))これはシンプルな値渡し形式も持つ。

Θv = )) ))

2.4. SとKによる最もシンプルな不動点コンビネータ
---------------------------

SKIコンビネータ計算のSとKによる最もシンプルな不動点コンビネータは、ジョン・トロンプによって発見された以下であり、

Y' = S S K ))) K)これは次のラムダ式と対応する。

Y' =  )

2.5. その他の不動点コンビネータ
------------------

型無しラムダ計算における不動点コンビネータは無数に存在するので、特に珍しいわけではない。2005年、メイヤー・ゴールドバーグ  は型無しラムダ計算の不動点コンビネータの集合が帰納的可算集合であることを示した。

次のようないくつかの不動点コンビネータは、主として遊びに使われる。

Yk = ここで

L = λabcdefghijklmnopqstuvwxyzr. )

2.6. 非標準不動点コンビネータ
-----------------

型無しラムダ計算には不動点演算子と同じベーム木を持つラムダ式がある。すなわちそれらはλx.x)と同じ無限の拡張を持つ。これは非標準不動点コンビネータと呼ばれる。定義より、あらゆる不動点コンビネータは非標準でもあるが、すべての非標準不動点コンビネータが不動点コンビネータであるわけではない。それらのいくつかは「標準」の定義を満たさないからである。これらの変わったコンビネータは特にstrictly non-standard fixed point combinatorsと呼ばれる。例として、B = λx.xxかつM = λxyz.xとしたときのコンビネータN = BMB)が挙げられる。非標準不動点コンビネータの集合は帰納的可算集合ではない。

3. 不動点コンビネータの実装
---------------

これまでの節で実装というよりは主に理論の観点から述べてきた、評価戦略が名前渡しの場合と値渡しの場合の違いは、実装においては、非正格なプログラミング言語と正格な言語の場合にほぼそのまま対応する。非正格な言語ないし処理系においては、ほぼ不動点コンビネータの意味そのままに循環的に実装できる。正格な場合は修正が必要であり、後述する。理論的には循環が無いことに意味があったが、実装においては循環的で普通は問題が無く、そのほうが効率的でもある。以下にHaskellによる不動点コンビネータの実装を示す。この不動点コンビネータはHaskellにおいては伝統的にfixと呼ばれる。fixは多相不動点コンビネータであることに注意せよ。なお、Haskellには型推論があるが、以下では曖昧さをなくすために型は明記する。定義の後に使用例が続く。

なお、型無しラムダ計算におけるカリーのYコンビネータは、そのまま実装しようとすると、Haskellの型チェッカによって拒否される。

fixの適用は遅延評価されるので無限ループにはならない。たとえばfix がとして展開されるとき、部分式fix fは評価されない。ところが、Haskellによるfixの定義を正格プログラミング言語に持ち込むと無限ループになる。なぜなら、fへ渡した引数は事前に展開され、無限の呼び出しの連続f  ... ))を生み出すからである。

MLのような正格言語においては、クロージャの使用を強制することによって無限再帰問題を回避することができる。fixの正格なバージョンは型∀a.∀b.→)→を持つべきである。要するに、これは関数を取って返す関数でのみ動く。例として、以下はfixの正格なバージョンのOCamlコード実装である。

let rec fix f x = f  x 

let factabs fact = function  0 -> 1 | x -> x * fact 

let _ =  5 <WtXmlEndTag />

以下は Python での実装。 def fix: return lambda x: f)

利用方法fix)<WtXmlEndTag />

Java 8 や C++11 では無名関数が使えるので上記と同じ方法で実装できる。それよりも前の時代の Java や C++ では少々複雑だった。

3.1. 再帰型による符号化の例
----------------

再帰データ型をサポートしているプログラミング言語では、型レベルで再帰を適切に計算することによってYコンビネータの型付けが可能になる。変数xを自己適用する必要性は同型の  を用いて定義される型  によって管理することができる。

例として、以下のHaskellコードは、型とともに同型写像のInとoutの2つの方向の名前を持つ。

そして次のように書くことができる。

OCamlによる等価なコードは以下。

type 'a recc = In of  let out  = x

let y f =  a)  a))<WtXmlEndTag />

3.2. グラフ簡約
----------

グラフ簡約による計算系では、不動点コンビネータへの適用は理論通り展開しても良いが、左の図のように循環のあるグラフに簡約するという一種の、のぞき穴的最適化が知られている。また、これはカリーのYコンビネータではないが便宜的にYという名前で呼ばれていることもある。

4. 関数の自己参照による無名再帰
-----------------

不動点コンビネータは識別子に束縛されていない関数が自分自身を呼び出す一般的な方法であるが、言語によっては特別な名前などで自分自身を呼び出すことができる。詳細は無名再帰を参照。

5. 関連項目
-------

不動点反復法
無名関数
固有関数

6. 脚注
-----

7. 参考文献
-------

Werner Kluge, //Abstract computing machines: a lambda calculus perspective//, Springer, 2005, ISBN 3540211462, pp. 73-77
Mayer Goldberg,  //[1]//, BRICS Report RS-05-1, University of Aarhus