純粋関数型言語で定義できない純粋な関数

並列論理和の続きで真のエキスパート氏から教えていただいた話（の劣化コピー）。並列論理和は、逐次言語では定義できないけど「計算可能」な（並列言語では定義でき、領域理論でも連続になる）関数でしたが、その親戚というか兄弟です。

MLで（実はHaskellでも良いのですが）、unit→unit型の純粋な（＝副作用のない）関数は、

  • let f1 () = ()
  • let rec f2 () = f2 ()

の2つがあります。ただし、たとえ内部の実装が異なっても、外部から観察できる振る舞いが同じ関数は同じとみなします。たとえば

  • let f1' () = try (raise E) with E -> ()

なるf1'はf1と同じ（かつ純粋）とみなします。

以下、「関数」としてデフォルトでは「振る舞いが純粋な関数」だけを考えることにします。すると、上と同様に、(unit→unit)→unit型の関数は

  • let g1 f = ()
  • let g2 f = f ()
  • let rec g3 f = g3 f

の3つがあります。言い換えると、

  • g1(f1) = g1(f2) = ()なるg1
  • g2(f1) = ()かつg2(f2) = \bot（無限ループ）なるg2
  • g3(f1) = g3(f2) = \botなるg3

の3つです。

では、((unit→unit)→unit)→unit型の関数はいくつあるでしょうか。

  • let h1 g = ()つまりh1(g1) = h1(g2) = h1(g3) = ()なるh1
  • let h2 g = g f1つまりh2(g1) = h2(g2) = (), h2(g3) = \botなるh2
  • let h3 g = g f2つまりh3(g1) = (), h3(g2) = h3(g3) = \botなるh3
  • let rec h4 g = h4 gつまりh4(g1) = h4(g2) = h4(g3) = \botなるh4

の4つはすぐにわかります。

ところが、その他に

  • h5(g1) = h5(g3) = \botかつh5(g2) = ()なるh5

があります（追記：誤植h4(g2)をh5(g2)に訂正）。領域理論を知っていると「そんなわけはない」と思うかもしれませんが、

  • let rec h5 g = (let r = ref false in g (fun () -> r := true); if !r then () else h5 g)

というh5です。もちろん、fun () -> r := trueは「純粋」じゃないなのですが、rがローカルなので、h5の振る舞いは純粋です。

ということで、h5は「振る舞いは純粋なのに、純粋関数型言語では定義できない関数」になります。

ちなみに、このようなh5は破壊的代入ではなくcall/ccでも定義できます（cf. call/ccが「副作用」である理由）。

ネタ元はhttp://citeseer.ist.psu.edu/longley99when.htmlです。もっといろいろと面白いことが書いてあるのですが、それはまたいずれ…

追記：げ、もろに被ってる…。気がつきませんでした。いや、本当に…