不動点とfix演算子
ある関数に対する不動点 とは、 なる です。 例えば、べき乗を関数とみなすと、 となり、1と0はべき乗の不動点となります [1]。
プログラム言語の教科書では という演算子が登場します [2,3,4]。 この と先の不動点はどう関係があるのか、フィボナッチ数の例で考えてみます。
フィボナッチ数を求める関数は、再帰的に定義すると次のようになります。
これをλ式で書くと
となります。しかしは、λ抽象の本体にという自由変数が現れています。
自由変数が現れているので、OCamlで書くとエラーになります(ただし、型なしラムダ計算では許されます)。
# let fib = fun n -> if n==0 || n==1 then 1 else fib (n-1) + (n-2);; Error: Unbound value fib
不動点
このままでは型付きの言語で再帰が書けません!
考え方を変えてみましょう。
次のような高階関数を定義します。
ここで本体の式にあるは、λによって束縛された変数であることに注意してください。 このを先ほどのに適用してみます。
\begin{align} F_{fib}\,fib &= (\lambda f. \lambda n. \mathsf{if}\;n=0 \lor n=1\;\mathsf{then}\;1\;\mathsf{else}\; f (n-1) + f (n-2))\;fib \\ &= \lambda n. \mathsf{if}\;n=0 \lor n=1\;\mathsf{then}\;1\;\mathsf{else}\; \color{red}{fib} (n-1) + \color{red}{fib} (n-2) \\ &= fib \end{align}
なんと、 という等式を満たすではありませんか!すなわち、はの不動点ということです。
しかし、 は自由変数が含まれており、実際には定義するとエラーになりました。 ということは をに適用することだって、本当はできません。 でも、高階関数 は定義できました!
不動点コンビネータ
先のを定義せず、から不動点なるを求めるにはどうしたらいいんでしょうか?
不動点コンビネータは、任意の関数からその関数の不動点を対応させてくれます。 代表的な不動点コンビネータの1つにコンビネータ [1]があり、次のように定義されます。
Yコンビネータを使うと、
となり、 であることがわかります。
になるのはわかりましたが、これをどうやって計算したらいいんでしょうか? この計算には、
- (1) 型を考えない(型なしラムダ計算)
- (2) 名前呼び戦略で計算する
という2点を知っておく必要があります。
(1) 型なしラムダ計算
型なしラムダ計算においては、どんな2つのλ式 であっても、 を に適用できます[5]。*1
例として、先の の赤字部分は、を自分自身に適用しています。これって型を考えるとおかしいですよね。 まずの型は です (最初に定義したの型はでした)。 ということは、 のの型はでなければなりません。
では、関数適用の型付け規則をみてみます。
ここで、 の型は のはずなので、
となります。
という式は、型を要求されています。
これはでなければならないはずです。
では、のの型についてはどうでしょうか?
だとわかりづらいので、と表記します。
いま不明な型をと表します。関数適用の型付け規則からの型は次のようになります。
さて、との型は同じはずです。 の型はいまなので、 も であるべきです。
おっと、 がであることを要求されてしまった!
というように自身の型が再帰的に現れています。 これは再帰型と呼ばれるものだそうです。 ということは、再帰型を扱えれば型付けされたYコンビネータが扱えるということでしょうか。 試してみましょう。
$ ocaml OCaml version 4.01.0 # let y = fun f -> ((fun x -> f (x x)) (fun x -> f (x x)));; Error: This expression has type 'a -> 'b but an expression was expected of type 'a The type variable 'a occurs inside 'a -> 'b $ ocaml -rectypes OCaml version 4.01.0 # let y = fun f -> ((fun x -> f (x x)) (fun x -> f (x x)));; val y : ('a -> 'a) -> 'a = <fun>
OCamlの-rectypes
を使ってYコンビネータを定義できました。
しかし、OCamlは値呼び戦略の言語であるため、これを実行すると延々と再帰し続け(後述)、スタックオーバーフローになります。
なおこのオプションは、より多くの値を受け付けてしまい、読みづらい型を与えてしまう傾向があるようです [6]。
ここでは単純な型の世界で再帰関数を実現したいので、再帰型は考えないことにします。 ともかく、Yコンビネータは型なしの世界で有効なのです。
(2) 名前呼び戦略 Call by Name
型を考えないとしても、 すなわち、をどのように計算すればいいでしょうか?
値呼び戦略 (Call by Value, CBV) だと延々と適用が繰り返されてしまいます。 CBVは関数適用の前に引数を先に計算して、その結果の値を関数に渡します。 試しに計算してみます。 の引数はですから、先にそれを計算します。
\begin{align} & F ( (\lambda x. F (x x) ) (\lambda x. F (x x) ) ) n \\ &= F ( (\lambda x. F (x x) ) (\lambda x. F (x x) ) ) n \\ &= F ( (\lambda x. F (x x) ) (\lambda x. F (x x) ) ) n \\ &= F (F ( (\lambda x. F (x x)) (\lambda x. F (x x) ) ) ) n \\ &= F (F (F ( (\lambda x. F (x x)) (\lambda x. F (x x) ) ) ) ) n \\ & \dots \end{align}
やはり延々と続いてしまいます。
では名前呼び戦略(Call by Name, CBN)はどうでしょうか? CBNでは、式の評価は名前を呼ばれるまで後回しにします。 ここで、読みやすさのためとします。 そして、は です。また、としておきます。
ではCBNで計算してみます。
\begin{align} & F (F' F') 5 \\ &= (\lambda n. \mathsf{if}\;n=0 \lor n=1\;\mathsf{then}\;1\;\mathsf{else}\;(\color{red}{F' F'}) (n-1) + (\color{red}{F' F'}) (n-2)) 5 \\ &= \mathsf{if}\;5=0 \lor 5=1\;\mathsf{then}\;1\;\mathsf{else}\;(\color{red}{F' F'}) (5-1) + (\color{red}{F' F'}) (5-2) \end{align}
おお!5への適用ができました! 引き続き、式の中を計算していきます。 の条件はになりますから、節を計算していきます。
\begin{align} &= (\color{red}{F' F'}) (5-1) + (\color{red}{F' F'}) (5-2) \\ &= F (F' F')(5-1) + (\color{red}{F' F'}) (5-2) \\ &= (\lambda n. \mathsf{if}\;n=0 \lor n=1\;\mathsf{then}\;1\;\mathsf{else}\; (\color{red}{F' F'}) (n-1) + (\color{red}{F' F'}) (n-2) ) (5-1) + (\color{red}{F' F'}) (5-2) \\ &= (\mathsf{if}\;(5-1)=0 \lor (5-1)=1 \\ &\phantom{=(}\;\mathsf{then}\;1 \\ &\phantom{=(}\; \mathsf{else}\;(\color{red}{F' F'}) ( (5-1)-1) + (\color{red}{F' F'}) ( (5-1)-2) ) (5-1) + (\color{red}{F' F'}) (5-2) \end{align}
あとは先ほどの繰り返しです。 以上のように、Yコンビネータで再帰処理が実現できました。
fix
Yコンビネータは型のない世界では有効ですが、型付きの世界では使えません。 そこで演算子です。 これはYと同じように不動点コンビネータとして作用します。
は教科書によっては と書いたり、と書いたりします。
先ほどのに対して、
前者:
後者:
と書きます。後者は中のをλで束縛するのではなく、で束縛します。のスコープは前者同様に、です。
ここでは後者の定義を用います。
各規則を以下に示します。
評価規則
は式中の変数を式に置き換える 代入 (substitution) と呼ばれる操作を行います。 これによってのときのように、再帰を実現しています。
型付け規則
型は関数型を含みます。
実際に式 を型付けしてみます。式 は型ですから、になります。
そしてlet recへ
は、との組み合わせで、以下のように定義できます [7]。
のほうが使いやすいですが、を使ったほうが計算の意味が見えてくると思います。
fixを実際に使ってみたい
を実際に使ってみたい方(あるいは自分で実装してみたい方)は、
https://github.com/succzero/fino
をどうぞ。(なお評価規則は、代入ではなく環境を使ったものになっています。)
cabal build
すれば使えるはずです。
OCamlではlet rec
を使ってしまえば、次のようにを定義できます。
# let rec fix f x = f (fix f) x;; val fix : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun> # let fibo = fun f -> fun n -> if n==0||n==1 then 1 else f (n-1) + f (n-2);; val fibo : (int -> int) -> int -> int = <fun> # fix fibo 10;; - : int = 89
Haskellの場合はfix
関数が用意されています。
Prelude> import Data.Function Prelude Data.Function> :i fix :: (a -> a) -> a -- Defined in ‘Data.Function’ Prelude Data.Function> let fact = fix (\f -> \n -> if n==0||n==1 then 1 else f (n-1) + f (n-2)) Prelude Data.Function> fact 10 89
まとめ
不動点コンビネータは、任意の関数から不動点を対応付けるものです。 型なしの世界で考えられた不動点コンビネータ(Yコンビネータ)は、単純な型付きの世界では型付けできないものでした。 型付きの不動点コンビネータとして作用するは、式あるいは型式中に再帰的に現れるに対して、代入操作を行うことで定義できました。 そして、再帰関数を束縛できるは、とによって定義付けでき、再帰関数の定義には不動点コンビネータが深く関わっていることをみてきました。
参考文献
[1] Fixed-point combinator - Wikipedia, the free encyclopedia. 2015年6月アクセス.
[2] Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press, Cambridge, MA, USA.
[3] Professor Robert Harper. 2012. Practical Foundations for Programming Languages. Cambridge University Press, New York, NY, USA.
[4] Gilles Dowek and Jean-Jacques Lvy. 2010. Introduction to the Theory of Programming Languages (1st ed.). Springer Publishing Company, Incorporated.
[5] 高橋正子 (1991). 計算論. 近代科学社.
[6] Jeremy Siek. Extensions the the Simply Typed Lambda Calculus. 2015年6月アクセス.
[7] Emmanuel Chailloux, Pascal Manoury, Bruno Pagano.
Developing Applications With Objective Caml, Appendix A Cyclic Types, Option -rectypes. 2015年6月アクセス.