型無しラムダ計算での不動点オペレータの導出

公式は覚えるものではなく, 必要に応じて導出するものだよ (?)

不動点オペレータ

不動点オペレータ (大抵 fix という名前, コンビネータ計算の文脈では Y とも) は Haskell では以下のように定義される関数である.

fix f = f (fix f)

つまり, fix f は関数 f不動点となっている.

OCaml のような値呼びの言語では, 評価順序の影響で, 定義は以下のようになる.

let rec fix f = f (fun x -> fix f x)

fix が何に使えるのかは直感的にはわかりにくいが, これは再帰関数を定義するときに便利である. 例えば let recfix を用いた式の糖衣構文と見ることもできる.

以下では型無しラムダ計算での不動点オペレータの導出?を行う. 型無しラムダ計算の説明は省く (面倒なので). あと文法は例によって謎の 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)
  )