Haskell/不動点と再帰
初めて fix 関数を目にしたときは、これはとても奇妙な関数に思えることだろう。しかしながら、再帰的な関数を定義可能にする組み込み要素として(型付き)ラムダ計算へとして導入するとき、主要な理論的根拠のひとつとして有用なものとなるのである。
fix の導入
[編集]議論に入る前に、fix の定義をしておこう。
fix :: (a -> a) -> a fix f = f (fix f)
これは一見していかにも摩訶不思議に思える。どうみてもfix f は f (f (f (... ))) のような fの限りない適用のくり返しを生じるだろう。我らが盟友、遅延評価がこの問題の解決策になる。基本的には、この f の適用の連鎖は、もしfが遅延関数であれば(その時に限り)ある値へと収束する。いくつか例をみていこう。
Example: fix の例
Prelude> :m Control.Monad.Fix Prelude Control.Monad.Fix> fix (2+) *** Exception: stack overflow Prelude Control.Monad.Fix> fix (const "hello") "hello" Prelude Control.Monad.Fix> fix (1:) [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,...
fix をスコープに持ってくるため、最初に Control.Monad.Fix モジュールをインポートする(Data.Functionでも利用可能である)。それから例を試していく。fix の定義はとても単純なので、何が起きているか説明するためにこの例を展開していこう。
fix (2+) = 2 + (fix (2+)) = 2 + (2 + fix (2+)) = 4 + (fix (2+)) = 4 + (2 + fix (2+)) = 6 + fix (2+) = ...
これはどんな値にも決して収束しないのは明らかだ。それでは次の例を展開しよう。
fix (const "hello") = const "hello" (fix (const "hello")) = "hello"
これはまったく異なる結果になる。const はその第二引数を無視するので、 fix の定義を一度展開すれば評価は完了することがわかる。最後の例の評価は少し異なるが、同様に進めていくことができる。
fix (1:) = 1 : fix (1:) = 1 : (1 : fix (1:)) = 1 : (1 : (1 : fix (1:)))
これは決してなんらかの値に収束しないように見えるが、GHCi にfix (1:)と入力した時、実際に行われているのは show をこれに適用していることだというのを思い出そう。それでは、show (fix (1:)) がどのように評価されるのかを見ていこうと思う(単純にするため、 showはリストの要素をカンマで区切る記法を使わないことにしよう)。
show (fix (1:)) = "[" ++ map show (fix (1:)) ++ "]" = "[" ++ map show (1 : fix (1:)) ++ "]" = "[" ++ "1" ++ map show (fix (1:)) ++ "]" = "[" ++ "1" ++ "1" ++ map show (fix (1:)) ++ "]"
map show (fix (1:))は決して終了しないだろうが、出力は行われる。GHCi は "[" ++ "1" ++ "1" という出力文字列の最初のほうを出力することができ、さらにどんどん map show (fix (1:)) がさらに文字列を生むたびに出力をし続ける。これは遅延評価が働いているのだ。この関数は出力を開始する前にその入力文字列全体を消費する必要がなく、一部でも出力可能になったらすぐさま出力を開始することができるのだ。
| 演習 |
|---|
もし収束値が存在するとしたら、次の式は何の値に収束するだろうか？
|
fix と不動点
[編集]関数 f の不動点 とは、f a == aを満たすような値 a のことである。例えば、0 * 3 == 0なので0 は関数(* 3)の不動点である。fixという名前は、それが関数の最も定義されていない不動点を導くことからきている("最も定義されていない"(least-defined)が意味するところは、すぐにわかるようになるだろう)。先ほどの収束するのふたつの例について考えると、これはすぐにわかる。
const "hello" "hello" -> "hello" (1:) [1,1,..] -> [1,1,...]
そして、2+x == xを満たすような数xは存在しないので、fix (2+)が発散するのもつじつまがあっている。
| 演習 |
|---|
|
|
実際には、それが不動点を求めることができるのはfixの定義より明らかである。やらなければならないのは、fixの等式をそれとは別の方法で書き表すことである。
f (fix f) = fix f
これは不動点の定義そのものだ！よって、これは fix は常に不動点を導くはずであるのがわかる。しかし fixはそれが発散することもあるので、しばしば失敗する。しかしながら、いくつかの表示的意味論を導入すれば、この特性を修正することはできる。すべての Haskell 型は実際には ⊥ と表記されボトム(Bottom)と呼ばれる特別な値を含んでいる。例えば、Int は実際には 1, 2, 3 ...を含むのと同様に ⊥ も含んでいる。発散する計算結果は⊥の値で示され、すなわち fix (2+) = ⊥ である。
特別な値 undefined もまた、この⊥で表される。これで、いよいよ fixがどうやって(2+)のような関数の不動点を求めているかが理解できる。
Example: (2+)の不動点
Prelude> (2+) undefined *** Exception: Prelude.undefined
よって、(⊥のような)undefinedを(2+)へ与えると、undefinedが返ってくる。したがって⊥は (2+)の不動点である！
(2+)の場合、これが唯一の不動点である。しかしながら、fix f が発散するにもかかわらず複数の不動点を持つ他の関数 fも存在する。fix (*3)は発散するが、上記で発見したように0はこの関数の不動点である。ここで"最も定義されていない"の意味を考えてみよう。Haskell の型は definedness と呼ばれている半順序を持つ。いずれの型においても⊥は最も定義されていない値である(それゆえボトムという名前である)。Intのような単純な型については、この半順序における順序関係は⊥ ≤ 1や⊥ ≤ 2 などしかない。ボトム以外のどんなInt型のm、nについても、m ≤ nは成り立たない。Bool や ()のような他の単純な型も同様である。リストやMaybeのような多相的な型については、状況はより複雑であり、表示的意味論の章で扱っている。
そして、⊥はすべての型で最も定義されていない値で、fixは最も定義されていない不動点を求めるので、もしf ⊥ = ⊥なら、fix f = ⊥となる(逆もまた真である)。もし表示的意味論の項をすでに読んでいるなら、これを正格関数であるかどうかの基準として認識することができるだろう。fix fはfが正格であるとき、そのときに限り発散する。
再帰
[編集]もしインターネット上や#haskell IRC channelで fixの例に出くわしたことがあれば、fixと再帰を取り入れている例を見るチャンスである。古典的な例として、
Example: fixによる再帰の書き換え
Prelude> let fact n = if n == 0 then 1 else n * fact (n-1) in fact 5 120 Prelude> fix (\rec n -> if n == 0 then 1 else n * rec (n-1)) 5 120
ここで階乗関数を"書き換え"るために fixを使っている。(もし fixを言語に組み込みのものとみなすなら)factの二番目の定義は再帰をまったく含んでいない。型付きラムダ計算のような再帰の機能のない言語では、このように再帰的関数を書くためにfixを導入することができる。他の例としては、
Example: さらなるfixの例
Prelude> fix (\rec f l -> if null l then [] else f (head l) : rec f (tail l)) (+1) [1..3] [2,3,4] Prelude> map (fix (\rec n -> if n == 1 || n == 2 then 1 else rec (n-1) + rec (n-2))) [1..10] [1,1,2,3,5,8,13,21,34,55]
では、これはどのように働くのであろうか？このfact (階乗)関数によって表示的な視点からの最初の一歩を踏み出そう。簡潔さのために次のように定義する。
fact' rec n = if n == 0 then 1 else n * rec (n-1)
これによってfix fact' 5というように計算できるようになる。fixはfact'の不動点、すなわちf == fact' fを満たす関数 fを求めるだろう。でも、これが何を意味するのか展開してみよう。
f = fact' f = \n -> if n == 0 then 1 else n * f (n-1)
ここで行ったのは、recをfact'の定義におけるfで置き換えただけであるが、これは階乗関数の再帰的定義にそっくりである！高階関数から抜けだして、再帰的な関数を作るためにfixはfact'自身をその最初の引数として与えている。
もっと演算的な観点から考えることもできる。実際にfix fact'の定義を展開してみよう。
fix fact'
= fact' (fix fact')
= (\rec n -> if n == 0 then 1 else n * rec (n-1)) (fix fact')
= \n -> if n == 0 then 1 else n * fix fact' (n-1)
= \n -> if n == 0 then 1 else n * fact' (fix fact') (n-1)
= \n -> if n == 0 then 1
else n * (\rec n' -> if n' == 0 then 1 else n' * rec (n'-1)) (fix fact') (n-1)
= \n -> if n == 0 then 1
else n * (if n-1 == 0 then 1 else (n-1) * fix fact' (n-2))
= \n -> if n == 0 then 1
else n * (if n-1 == 0 then 1
else (n-1) * (if n-2 == 0 then 1
else (n-2) * fix fact' (n-3)))
= ...
fixの使用によって fact'の定義を"分解"し続けることができていることに注意されたい。else節を入力するときはいつも、評価の規則fix fact' = fact' (fix fact')を通じて、再帰の連鎖において次の呼び出しとして機能する fact'の新たな複製を乗算しているのである。結果的にこの連鎖の外でthen節やボトムに達するのだ。
| 演習 |
|---|
|
型付きラムダ計算
[編集]この節ではこれまでの節で何度か言及してきた点について展開していく。型付きラムダ計算においては、fixはどうやって再帰の書き換えを可能にしているのだろうか。あなたがすでに型付きラムダ計算を知っていると仮定する。ラムダ計算にはlet節やトップレベルの束縛は存在しないことを思い出そう。どんなプログラムもラムダ抽象、適用、リテラルのいずれかからなる単なる木である。fact関数を書きたいとしよう。自然数としてNatと呼ばれる型があるものとして、次のようにとりかかった。
λn:Nat. if iszero n then 1 else n * <blank> (n-1)
問題は、<blank>の部分をどのように埋めるかだ。この関数には名前を与えていないので、これを再帰的に呼びだすことはできない。項に名前を束縛する唯一の手段は、ラムダ抽象を使うことだ。それではこれをやってみよう。
(λf:Nat→Nat. λn:Nat. if iszero n then 1 else n * f (n-1)) (λm:Nat. if iszero m then 1 else m * <blank> (m-1))
これはつぎのように展開される。
λn:Nat. if iszero n then 1
else n * (if iszero n-1 then 1 else (n-1) * <blank> (n-2))
まだ <blank>がある。もう一段階やってみよう。
(λf:Nat→Nat. λn:Nat. if iszero n then 1 else n * f (n-1)
((λg:Nat→Nat. λm:Nat. if iszero n' then 1 else n' * g (m-1))
(λp:Nat. if iszero p then 1 else p * <blank> (p-1))))
->
λn:Nat. if iszero n then 1
else n * (if iszero n-1 then 1
else (n-1) * (if iszero n-2 then 1 else (n-2) * <blank> (n-3)))
何段階名前付けを加えようとも、この<blank>を取り除くことができそうもないのはどうみても明らかだ。fixを使わない限り、本質的に決して取り除くことはできず、つねに再帰のもう一段階を解くことができ、出発した時のままなのである。
fix (λf:Nat→Nat. λn:Nat. if iszero n then 1 else n * f (n-1))
これはfixを加えた型付きラムダ計算における完全な再帰関数だ。
型付きラムダ計算の文脈においては、fixは実際にはこれよりもうすこし興味深いものである。もしこれをこの言語に導入すると、なんらかの具体的な型Tがあれば次の式は型Tを持つので、どんな型も空でない集合となる。
fix (λx:T. x)
これはHaskellでいうところのfix idであり、表示的な ⊥である。ゆえに、型付きラムダ計算にfixを導入するやいなや、あらゆる well-typed な項が値へと還元されるという性質は失われることがわかる。
データ型としての Fix
[編集]Haskell では、fix データ型を作ることも可能である。定義する方法は３つある。
newtype Fix f=Fix (f (Fix f))
もしくは、RankNTypes 拡張を利用する。
newtype Mu f=Mu (forall a.(f a->a)->a) data Nu f=forall a.Nu a (a->f a)
Mu と Nu は fold、unfold、refold を一般化するのを補助している。
fold :: (f a -> a) -> Mu f -> a fold g (Mu f)=f g unfold :: (a -> f a) -> a -> Nu f unfold f x=Nu x f refold :: (a -> f a) -> (g a-> a) -> Mu g -> Nu f refold f g = unfold f . fold g
Mu と Nu は Fix の特殊化されたバージョンである。
Mu は帰納的な無限でないデータを作るのに使われ、Nu は余帰納的(coinductive)で無限のデータを作るのに使われる。例えば、
newtype Stream a=Stream (Nu ((,) a)) -- forsome b. (b,b->(a,b)) newtype Void a=Void (Mu ((,) a)) -- forall b.((a,b)->b)->b
不動点関数とは異なり、不動点型はボトムにならない。次のコードにおける Bot は完全に定義されている。これはユニット型 () と等価である。
newtype Id a=Id a newtype Bot=Bot (Fix Id) -- newtype Bot=Bot Bot に等しい -- 可能な項は一つだけ存在する。Bot $ Bot $ Bot $ Bot…
Fix データ型はすべての再帰構造を作ることができない。例えば次の非正則なデータ型、
data Node a=Two a a|Three a a a data FingerTree a=U a|Up (FingerTree (Node a))
これを Fix を用いて実装するのは容易ではない。