不動点コンビネータ
不動点コンビネータ(ふどうてんコンビネータ、英: fixed point combinator、不動点結合子、ふどうてんけつごうし)とは、与えられた関数の不動点(のひとつ)を求める高階関数である。不動点演算子(ふどうてんえんざんし、英: fixed-point operator)、パラドキシカル結合子(英: paradoxical combinator)などとも呼ばれる。ここで関数 の不動点とは、 を満たすような のことをいう。
すなわち高階関数 が不動点コンビネータであるとは、
- 任意の関数 に対し、 とすると, が成立する
事を指す。
あるいは全く同じことだが、不動点コンビネータの定義は、任意の関数 に対し、
が成立する事であるとも言い換えられる。
第一級関数をサポートしているプログラミング言語では、不動点コンビネータを用いて識別子に束縛されない関数の再帰を定義することができる。そういったテクニックは、しばしば無名再帰と呼ばれる。[1][2]
不動点コンビネータは高階関数であるため、その歴史はラムダ計算の発達と深く関係している。型無しラムダ計算(英: untyped lambda calculus)においては、ハスケル・カリーの Y = λf·(λx·f (x x)) (λx·f (x x))
という不動点コンビネータがよく知られている。型無しラムダ計算には無数の不動点コンビネータが存在するが、一方で単純型付きラムダ計算などのより限定的な計算モデルでは、不動点コンビネータは必ずしも存在するとは限らない。
不動点コンビネータによる再帰の実現
[編集]不動点コンビネータにより、第一級関数をサポートしているプログラミング言語において、明示的に再帰を書かずに再帰を実現する為に用いる事ができる。なお、一般にそういった言語では普通に再帰が使えるので、プログラミングにおいてはパズル的なテクニック以上の意味は無い。一方、循環なく関数の意味を定義する(できる)、ということは、計算理論の上では重要である。
まず、再帰関数の性質を簡単に振り返り、記号をいくつか定義する。関数 が再帰的に定義されているとき、 の定義式は何らかの高階関数 を用いて、
と書ける。たとえば が の階乗を計算する関数である場合、 として
を取る事ができる。上述のように定義された が(Eq. 1)を満たすのは明らかであろう。
を用いて高階関数 を
と定義する。 (すなわち は関数 を入力として受け取ると 関数「」を出力する高階関数である。 ラムダ計算の用語で言えば、 は のカリー化にあたる。) の定義より、はそれ自身関数であり、任意の に対し、
が成り立つ。ここで は関数に を入力したときの値。
さて、g を不動点コンビネータとするとき、不動点コンビネータの定義より特に、 は の定義域の元である事が分かる。 の定義域は関数の集合だったので、これはすなわち はそれ自身関数である事を意味する。 この関数 が式で定義された再帰関数 と一致する事を示す事ができる(後述)。
よって以下のようにすれば不動点コンビネータg で再帰関数 を実現できる事になる:
- U のプログラムを書く。
- V をEq. 2式のように定義し、とする。
の証明
[編集]最後にが Eq. 1 で定義された再帰関数 と一致する事を示す。 不動点コンビネータの定義より、は
を満たす。
前述したようにはそれ自身関数なので、値xに対しを考える事ができる。 は以下を満たす:
(Eq. 4より) | ||
、 | (Eq. 3より) |
すなわち
Eq. 1 と Eq. 5 を見比べると、Eq. 5 は Eq. 1 で を に置き換えたものに等しい事が分かる。 Eq. 1は の(再帰的な)定義式であったので、これはすなわち が の定義式を満たす事を意味する。 よって
- 。
が成立する事が分かった。
不動点コンビネータの例
[編集]型無しラムダ計算や組合せ論理などの特定の数学的な計算形式化においては、すべての式は高階関数とみなすことができる。これらの形式化では、不動点コンビネータが存在することはすなわち、すべての関数が少なくとも1つの不動点を持つことを意味する。さらに、関数は複数の異なる不動点を持つことができる。
単純型付きラムダ計算などの他のいくつかの体系では、十分に型付けされた不動点コンビネータを書くことはできない。それらの体系で再帰をサポートするには、明示的に言語体系に組み込む必要がある。それでも再帰データ型によって拡張された単純型付きラムダ計算などでは不動点演算子を書くことができるが、ある種の「実用的な」不動点演算子(常にいずれかの適用を返すもの)は制限される。多相ラムダ計算(英: polymorphic lambda calculus、システムF、英: System F)では多相不動点コンビネータは型 を持つ(ただし は型変数である)。
Yコンビネータ
[編集]型無しラムダ計算においてよく知られた(そしておそらく最もシンプルな)不動点コンビネータはYコンビネータと呼ばれる。これはハスケル・カリーによって発見されたもので、次のように定義される。
Y = (λf . (λx . f (x x)) (λx . f (x x)))
実際に関数gを適用することによって、この関数が不動点コンビネータとして動作するのが分かる。
Y g
|
= (λf . (λx . f (x x)) (λx . f (x x))) g
|
(Yの定義より) |
= (λ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)
|
(第2式より) |
これをそのままラムダ計算で使うと、評価戦略が値渡しだった場合には (Y g) が (g (Y g))
と展開された後も、引数の値を先に求めようとして (g (g (Y g))) →...→ (g ... (g (Y g))...)
のように無限に展開され続けて止まらなくなってしまうので、次節で示すZコンビネータのように修正する。評価戦略が名前渡しの場合はこのまま使える。
このカリーによるコンビネータのみをYコンビネータとすることもあるが、実装などでは不動点コンビネータを指す名前として他の形であってもYという名前を使っていることもある(#グラフ簡約の節の注を参照せよ)。
SKIコンビネータ計算では次のようになる。
Y = S (K (S I I)) (S (S (K S) K) (K (S I I)))
Zコンビネータ
[編集]値渡し評価(適用順序)でも使用可能なバージョンのYコンビネータは、通常のYコンビネータの一部をη変換することで与えられる。
Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))
Python での実装。その他のプログラミング言語での実装は無名再帰を参照。
Z = lambda f: (lambda x: f(lambda *y: x(x)(*y)))(lambda x: f(lambda *y: x(x)(*y)))
# 利用方法(5の階乗の計算)
Z(lambda f: lambda n: 1 if n == 0 else n * f(n - 1))(5)
チューリング不動点コンビネータ
[編集]もう一つの一般的な不動点コンビネータは、チューリング不動点コンビネータである(発見者であるアラン・チューリングの名にちなむ)。
Θ = (λ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)))
SとKによる最もシンプルな不動点コンビネータ
[編集]SKIコンビネータ計算のSとKによる最もシンプルな不動点コンビネータは、ジョン・トロンプによって発見された以下であり、
Y' = S S K (S (K (S S (S (S S K)))) K)
これは次のラムダ式と対応する。
Y' = (λx. λy. x y x) (λy. λx. y (x y x))
その他の不動点コンビネータ
[編集]型無しラムダ計算における不動点コンビネータは無数に存在するので、特に珍しいわけではない。2005年、メイヤー・ゴールドバーグ (Mayer Goldberg) は型無しラムダ計算の不動点コンビネータの集合が帰納的可算集合であることを示した。[3]
次のようないくつかの不動点コンビネータ(ジャン・ウィレム・クロップによって組み立てられた)は、主として遊びに使われる。
Yk = (L L L L L L L L L L L L L L L L L L L L L L L L L L)
ここで
L = λabcdefghijklmnopqstuvwxyzr. (r (t h i s i s a f i x e d p o i n t c o m b i n a t o r))
非標準不動点コンビネータ
[編集]型無しラムダ計算には不動点演算子と同じベーム木(英: Böhm tree)を持つラムダ式がある。すなわちそれらは λx.x(x(x ... ))
と同じ無限の拡張を持つ。これは非標準不動点コンビネータ(英: non-standard fixed point combinators)と呼ばれる。定義より、あらゆる不動点コンビネータは非標準でもあるが、すべての非標準不動点コンビネータが不動点コンビネータであるわけではない。それらのいくつかは「標準」の定義を満たさないからである。これらの変わったコンビネータは特に strictly non-standard fixed point combinators と呼ばれる。例として、B = λx.xx
かつ M = λxyz.x(yz)
としたときのコンビネータ N = BM(B(BM)B)
が挙げられる。非標準不動点コンビネータの集合は帰納的可算集合ではない。[3]
不動点コンビネータの実装
[編集]これまでの節で実装というよりは主に理論の観点から述べてきた、評価戦略が名前渡しの場合と値渡しの場合の違いは、実装においては、非正格(non-strict)なプログラミング言語(ないし処理系)と正格(strict)な言語の場合にほぼそのまま対応する。非正格な(遅延評価の、と言い換えてもだいたい同じ。具体的にはHaskellなどがそう)言語ないし処理系においては、ほぼ不動点コンビネータの意味そのままに循環的に実装できる。正格な場合は修正が必要であり、後述する。理論的には循環が無いことに意味があったが、実装においては循環的で普通は問題が無く、そのほうが効率的でもある。以下にHaskellによる不動点コンビネータの実装を示す。この不動点コンビネータはHaskellにおいては伝統的にfix
と呼ばれる。fix
は多相不動点コンビネータであることに注意せよ(前述のシステムFに関する議論も参照)。なお、Haskellには型推論があるが、以下では曖昧さをなくすために型は明記する(一般に、こういった特殊な型を使う場合は型を明記したほうが良いし、推論の実装の限界のために明記が必要なこともある)。定義の後に使用例が続く。
なお、型無しラムダ計算におけるカリーのYコンビネータは、そのまま実装しようとすると、Haskellの型チェッカによって拒否される。[4]
fix :: (a -> a) -> a fix f = f (fix f) fix (const 9) -- constは第1引数を返し、第2引数を捨てる関数。9と評価される factabs fact 0 = 1 -- factabsはラムダ計算の例のFから拝借 factabs fact x = x * fact (x-1) (fix factabs) 5 -- 120と評価される
fix
の適用は遅延評価されるので無限ループにはならない。たとえばfix (const 9)
が(const 9)(fix f)
として展開されるとき、部分式fix f
は評価されない。ところが、Haskellによるfixの定義を正格(strict)プログラミング言語に持ち込むと無限ループになる。なぜなら、fへ渡した引数は事前に展開され、無限の呼び出しの連続f (f ... (fix f) ... ))
を生み出すからである。
MLのような正格言語においては、クロージャの使用を強制することによって無限再帰問題を回避することができる。fix
の正格なバージョンは型 を持つべきである。要するに、これは関数を取って返す関数でのみ動く。例として、以下はfix
の正格なバージョンのOCamlコード実装である。
let rec fix f x = f (fix f) x (* 余分なxに注目 *)
let factabs fact = function (* factabsはエクストラレベルのラムダ抽象 *)
0 -> 1
| x -> x * fact (x-1)
let _ = (fix factabs) 5 (* "120" と評価される *)
以下は Python での実装。
def fix(f):
return lambda x: f(fix(f))(x)
# 利用方法(5の階乗の計算)
fix(lambda f: lambda n: 1 if n == 0 else n * f(n - 1))(5)
Java 8 や C++11 では無名関数(ラムダ式)が使えるので上記と同じ方法で実装できる。それよりも前の時代の Java や C++ では少々複雑だった[5][6]。
再帰型による符号化の例
[編集]再帰データ型(システムFωを参照)をサポートしているプログラミング言語では、型レベルで再帰を適切に計算することによってYコンビネータの型付けが可能になる。変数xを自己適用する必要性は同型の (Rec a -> a) を用いて定義される型 (Rec a) によって管理することができる。
例として、以下のHaskellコードは、型とともに同型写像のInとoutの2つの方向の名前を持つ。
In :: (Rec a -> a) -> Rec a out :: Rec a -> (Rec a -> a)
そして次のように書くことができる。
newtype Rec a = In { out :: Rec a -> a } y :: (a -> a) -> a y = \f -> (\x -> f (out x x)) (In (\x -> f (out x x)))
OCamlによる等価なコードは以下。
type 'a recc = In of ('a recc -> 'a)
let out (In x) = x
let y f = (fun x a -> f (out x x) a) (In (fun x a -> f (out x x) a))
グラフ簡約
[編集]グラフ簡約(en:Graph reductionを参照)による計算系では、不動点コンビネータへの適用(apply, application)は理論通り展開しても良いが、左の図のように循環のあるグラフに簡約するという一種の、のぞき穴的最適化が知られている。また、これはカリーのYコンビネータではないが(この図のように)便宜的にYという名前で呼ばれていることもある[7]。
関数の自己参照による無名再帰
[編集]不動点コンビネータは識別子に束縛されていない関数が自分自身を呼び出す一般的な方法であるが、言語によっては特別な名前などで自分自身を呼び出すことができる。詳細は無名再帰を参照。
関連項目
[編集]脚注
[編集]- ^ This terminology appear to be largely folklore, but it does appear in the following:
- Trey Nash, Accelerated C# 2008, Apress, 2007, ISBN 1590598733, p. 462--463. Derived substantially from Wes Dyer's blog (see next item).
- Wes Dyer Anonymous Recursion in C#, February 02, 2007, contains a substantially similar example found in the book above, but accompanied by more discussion.
- ^ The If Works Deriving the Y combinator, January 10th, 2008
- ^ a b Goldberg, 2005
- ^ Haskell mailing list thread on How to define Y combinator in Haskell, 15 Sep 2006
- ^ The Y Combinator in Arc and Java - Javaコード
- ^ bind - Fixed point combinators in C++ - Stack Overflow - C++コード
- ^ たとえば、Turnerの"A New Implementation Technique for Applicative Languages"(doi:10.1002/spe.4380090105)の Figure. 3 と、その直前の説明を見よ。
参考文献
[編集]- Werner Kluge, Abstract computing machines: a lambda calculus perspective, Springer, 2005, ISBN 3540211462, pp. 73-77
- Mayer Goldberg, (2005) On the Recursive Enumerability of Fixed-Point Combinators, BRICS Report RS-05-1, University of Aarhus