公式は覚えるものではなく, 必要に応じて導出するものだよ (?)
不動点オペレータ
不動点オペレータ (大抵 fix
という名前, コンビネータ計算の文脈では Y
とも) は Haskell では以下のように定義される関数である.
fix f = f (fix f)
つまり, fix f
は関数 f
の不動点となっている.
OCaml のような値呼びの言語では, 評価順序の影響で, 定義は以下のようになる.
let rec fix f = f (fun x -> fix f x)
fix
が何に使えるのかは直感的にはわかりにくいが, これは再帰関数を定義するときに便利である.
例えば let rec
は fix
を用いた式の糖衣構文と見ることもできる.
以下では型無しラムダ計算での不動点オペレータの導出?を行う. 型無しラムダ計算の説明は省く (面倒なので). あと文法は例によって謎の ML 風のアレ.
再帰関数の定義
型無しラムダ計算には組み込みの fix
のようなオペレータは存在しない.
それではどのように再帰関数を定義するのかというと,
例えば階乗を計算する関数は素朴には以下のように書ける.
let factorial f n = if n = 0 then 1 else n * f f (n - 1) let ans = factorial factorial 10
このままだと n
の階乗を計算するためには factorial factorial n
のように
factorial
にそれ自身を引数として明示的に与えてやる必要がある.
これは面倒なので, 次のように定義し直す.
let factorial = let m f = fun n -> if n = 0 then 1 else n * f f (n - 1) in m m let ans = factorial 10
一般に再帰関数は次のように書ける.
let recursive = let m f = C[f f] in m m
ここで C[f f]
となっているのは f f
を含む項という程度の意味で,
上の階乗の例では C[t] = fun n -> if n = 0 then 1 else n * t (n - 1)
だった.
この let m f = ... in m m
という部分はどのような再帰関数に対しても同じなので,
C
を外部から与えるようにしてしまえば, 再帰関数を定義するための関数が作れる.
let recursive g = let m f = g (f f) in m m
あるいは let
を使うのをやめると,
let recursive g = (fun f -> g (f f)) (fun f -> g (f f))
これは以下のように使用できる.
let factorial = recursive (fun f n -> if n = 0 then 1 else n * f (n - 1) )
また, recursive g
の呼び出しを適当に評価してやると,
recursive g ~> (fun f -> g (f f)) (fun f -> g (f f)) ~> g ((fun f -> g (f f)) (fun f -> g (f f))) == g (recursive g)
となっており, 実は最初に挙げた Haskell での fix
と同じ動きをするということが分かる.
というわけで, 以降 recursive
ではなく fix
と呼ぶことにする.
let fix g = (fun f -> g (f f)) (fun f -> g (f f))
関数の不動点という, いかにも数学的な概念そのもののような定義の fix
だが, そのまま便利な道具として使えるのは少し面白い.
値呼びでの注意点
ところでこの関数の呼び出しは値呼びだと問題があり, 評価を追ってみると,
fix g ~> (fun f -> g (f f)) (fun f -> g (f f)) ~> g ((fun f -> g (f f)) (fun f -> g (f f))) ~> g (g ((fun f -> g (f f)) (fun f -> g (f f)))) ~> ...
のように引数部分を延々と評価し続けてしまい, g
が呼び出されることはない.
一方で最初に定義した factorial
の動作に問題はなかった.
なぜこのようになってしまったかというと, C[f f]
を g (f f)
で置き換えたとき,
元の定義では f f
は直ちに評価されなかったのが,
置き換えた後では g
の呼び出し前に評価するようになってしまっているためである.
この f f
の評価されるタイミングを調整する (遅延させる) ため,
f f
の代わりに同じ動きをする関数 fun x -> f f x
(η-expansion とかいう名前がついている) を g
に与えるように変更する.
let fix' g = let m f = g (fun x -> f f x) in m m
あるいは let
を使わずに書けば,
let fix' g = (fun f -> g (fun x -> f f x)) (fun f -> g (fun x -> f f x))
このようにすることで, f f
が評価されるタイミングが元と同じになる.
実際, 呼び出しの評価がどのように行われるかを見てみると,
fix' g ~> (fun f -> g (fun x -> f f x)) (fun f -> g (fun x -> f f x)) ~> g (fun x -> (fun f -> g (fun y -> f f y)) (fun f -> g (fun y -> f f y)) x) == g (fun x -> fix' g x)
となり, 正しく g
が呼び出されるようになる.
また, この挙動は一番最初に挙げた OCaml での fix
と一致する.
このように変更しても使い方は変わらない.
let factorial = fix' (fun f n -> if n = 0 then 1 else n * f (n - 1) )