日々の流転

λ. 『ガセネッタ＆(と)シモネッタ』 米原 万里

を読んだ。

λ. 正格な言語での不動点演算子

正格な言語、例えばOCamlでは、以下のようにして不動点演算子を定義することが出来る*1。これは常識ですね。

# let rec fix f x = f (fix f) x ;;
val fix : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
# let fib' f x = if x <= 1 then 1 else f (x - 1) + f (x - 2) ;;
val fib' : (int -> int) -> int -> int = <fun>
# let fib = fix fib' ;;
val fib : int -> int = <fun>
# fib 10 ;;
- : int = 89

で、ここでクイズなのだけど、f に対して fix f というのは一体何者でしょうか?　「そんなの f の最小不動点に決まってるじゃん」と思うかも知れないけど、ここでは正格な言語を考えているので「f ⊥ = ⊥」で、最小不動点は⊥なのでした。