利用者:Foxtrot/翻訳/Haskell/不動点と再帰
The fix function is a particularly weird-looking function when you first see it. However, it is useful for one main theoretical reason: introducing it into the (typed) lambda calculus as a primitive allows you to define recursive functions.
初めて fix 関数を目にしたときは、これはとても奇妙な関数に思えることだろう。しかしながら、再帰的な関数を定義可能にする組み込み要素として(型付き)ラムダ計算へとして導入するとき、主要な理論的根拠のひとつとして有用なものとなるのである。
Introducing fix fix の導入
[編集]Let's have the definition of fix before we go any further:
議論に入る前に、fix の定義をしておこう。
fix :: (a -> a) -> a fix f = f (fix f)
This immediately seems quite magical. Surely fix f will yield an infinite application stream of fs: f (f (f (... )))? The resolution to this is our good friend, lazy evaluation. Essentially, this sequence of applications of f will converge to a value if (and only if) f is a lazy function. Let's see some examples:
これは一見していかにも摩訶不思議に思える。どうみてもfix f は f (f (f (... ))) のような fの限りない適用のくり返しを生じるだろう。我らが盟友、遅延評価がこの問題の解決策になる。基本的には、この f の適用の連鎖は、もしfが遅延関数であれば(その時に限り)ある値へと収束する。いくつか例をみていこう。
Example: fix examples
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,...
We first import the Control.Monad.Fix module to bring fix into scope (this is also available in the Data.Function). Then we try some examples. Since the definition of fix is so simple, let's expand our examples to explain what happens:
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+) = ...
It's clear that this will never converge to any value. Let's expand the next example:
これはどんな値にも決して収束しないのは明らかだ。それでは次の例を展開しよう。
fix (const "hello") = const "hello" (fix (const "hello")) = "hello"
This is quite different: we can see after one expansion of the definition of fix that because const ignores its second argument, the evaluation concludes. The evaluation for the last example is a little different, but we can proceed similarly:
これはまったく異なる結果になる。const はその第二引数を無視するので、 fix の定義を一度展開すれば評価は完了することがわかる。最後の例の評価は少し異なるが、同様に進めていくことができる。
fix (1:) = 1 : fix (1:) = 1 : (1 : fix (1:)) = 1 : (1 : (1 : fix (1:)))
Although this similarly looks like it'll never converge to a value, keep in mind that when you type fix (1:) into GHCi, what it's really doing is applying show to that. So we should look at how show (fix (1:)) evaluates (for simplicity, we'll pretend show on lists doesn't put commas between items):
これは決してなんらかの値に収束しないように見えるが、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:)) ++ "]"
So although the map show (fix (1:)) will never terminate, it does produce output: GHCi can print the beginning of the string, "[" ++ "1" ++ "1", and continue to print more as map show (fix (1:)) produces more. This is lazy evaluation at work: the printing function doesn't need to consume its entire input string before beginning to print, it does so as soon as it can start.
map show (fix (1:))は決して終了しないだろうが、出力は行われる。GHCi は "[" ++ "1" ++ "1" という出力文字列の最初のほうを出力することができ、さらにどんどん map show (fix (1:)) がさらに文字列を生むたびに出力をし続ける。これは遅延評価が働いているのだ。この関数は出力を開始する前にその入力文字列全体を消費する必要がなく、一部でも出力可能になったらすぐさま出力を開始することができるのだ。
| 演習 |
|---|
|
What, if anything, will the following expressions converge to? もし収束値が存在するとしたら、次の式は何の値に収束するだろうか？
|
fix and fixed points fix と不動点
[編集]A fixed point of a function f is a value a such that f a == a. For example, 0 is a fixed point of the function (* 3) since 0 * 3 == 0. This is where the name of fix comes from: it finds the least-defined fixed point of a function. (We'll come to what "least defined" means in a minute.) Notice that for both of our examples above that converge, this is readily seen:
関数 f の不動点 とは、f a == aを満たすような値 a のことである。例えば、0 * 3 == 0なので0 は関数(* 3)の不動点である。fixという名前は、それが関数の最小で定義された固定された点を導くことからきている("最小で定義された"(least-defined)が意味するところは、すぐにわかるようになるだろう)。先ほどの収束するのふたつの例について考えると、これはすぐにわかる。
const "hello" "hello" -> "hello" (1:) [1,1,..] -> [1,1,...]
And since there's no number x such that 2+x == x, it also makes sense that fix (2+) diverges.
そして、2+x == xを満たすような数xは存在しないので、fix (2+)が発散するのもつじつまがあっている。
| 演習 |
|---|
|
For each of the functions
|
In fact, it's obvious from the definition of fix that it finds a fixed point. All we need to do is write the equation for fix the other way around:
実際には、それが不動点を求めることができるのはfixの定義より明らかである。やらなければならないのは、fixの等式をそれとは別の方法で書き表すことである。
f (fix f) = fix f
Which is precisely the definition of a fixed point! So it seems that fix should always find a fixed point. But sometimes fix seems to fail at this, as sometimes it diverges. We can repair this property, however, if we bring in some denotational semantics. Every Haskell type actually include a special value called bottom, written ⊥. So the values with type, for example, Int include, in fact, ⊥ as well as 1, 2, 3 etc.. Divergent computations are denoted by a value of ⊥, i.e., we have that fix (2+) = ⊥.
これは不動点の定義そのものだ！よって、これは fix は常に不動点を導くはずであるのがわかる。しかし fixはそれが発散することもあるので、しばしば失敗する。しかしながら、いくつかの表示的意味論を導入すれば、この特性を修正することはできる。すべての Haskell 型は実際には ⊥ と表記されボトム(Bottom)と呼ばれる特別な値を含んでいる。例えば、Int は実際には 1, 2, 3 ...を含むのと同様に ⊥ も含んでいる。発散する計算結果は⊥の値で示され、すなわち fix (2+) = ⊥ である。
The special value undefined is also denoted by this ⊥. Now we can understand how fix finds fixed points of functions like (2+):
特別な値 undefined もまた、この⊥で表される。これで、いよいよ fixがどうやって(2+)のような関数の不動点を求めているかが理解できる。
Example: Fixed points of (2+) (2+)の不動点
Prelude> (2+) undefined *** Exception: Prelude.undefined
So feeding undefined (i.e., ⊥) to (2+) gives us undefined back. So ⊥ is a fixed point of (2+)!
よって、(⊥のような)undefinedを(2+)へ与えると、undefinedが返ってくる。したがって⊥は (2+)の不動点である！
In the case of (2+), it is the only fixed point. However, there are other functions f with several fixed points for which fix f still diverges: fix (*3) diverges, but we remarked above that 0 is a fixed point of that function. This is where the "least-defined" clause comes in. Types in Haskell have a partial order on them called definedness. In any type, ⊥ is the least-defined value (hence the name "bottom"). For simple types like Int, the only pairs in the partial order are ⊥ ≤ 1, ⊥ ≤ 2 and so on. We do not have m ≤ n for any non-bottom Ints m, n. Similar comments apply to other simple types like Bool and (). For "layered" values such as lists or Maybe, the picture is more complicated, and we refer to the chapter on denotational semantics.
(2+)の場合、これが唯一の不動点である。しかしながら、fix f が発散するにもかかわらず複数の不動点を持つ他の関数 fも存在する。fix (*3)は発散するが、上記で発見したように0はこの関数の不動点である。これは"最小の定義"という節が現れるところである。Haskell の型は definedness と呼ばれている半順序を持つ。いずれの型も⊥は最小定義の値である(それゆえボトムという名前である)。Intのような単純な型については、半順序における比較可能な対は⊥ ≤ 1と⊥ ≤ 2 などしかない。どんなボトムでないIntのm、nについても、m ≤ nはない。Bool や ()のような他の単純な型も同様である。リストやMaybeのような多相的な型については、状況はより複雑であり、表示的意味論の章で扱っている。
So since ⊥ is the least-defined value for all types and fix finds the least-defined fixed point, if f ⊥ = ⊥, we will have fix f = ⊥ (and the converse is also true). If you've read the denotational semantics article, you will recognise this as the criterion for a strict function: fix f diverges if and only if f is strict.
そして、⊥はすべての型で最小定義された値で、fixは最小定義された不動点を求めるので、もしf ⊥ = ⊥なら、fix f = ⊥となる(逆もまた真である)。もし表示的意味論の項をすでに読んでいるなら、これを正格関数であるかどうかの基準として認識することができるだろう。fix fはfが正格であるとき、そのときに限り発散する。
Recursion 再帰
[編集]If you've come across examples of fix on the internet, or on the #haskell IRC channel, the chances are that you've seen examples involving fix and recursion. Here's a classic example:
もしインターネット上や#haskell IRC channelで fixの例に出くわしたことがあれば、fixと再帰を取り入れている例を見るチャンスである。古典的な例として、
Example: Encoding recursion with fix 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
Here we have used fix to "encode" the factorial function: note that (if we regard fix as a language primitive) our second definition of fact doesn't involve recursion at all. In a language like the typed lambda calculus that doesn't feature recursion, we can introduce fix in to write recursive functions in this way. Here are some more examples:
ここで階乗関数を"書き換え"るために fixを使っている。(もし fixを言語に組み込みのものとみなすなら)factの二番目の定義は再帰をまったく含んでいない。型付きラムダ計算のような再帰の機能のない言語では、このように再帰的関数を書くためにfixを導入することができる。他の例としては、
Example: More fix examples さらなる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]
So how does this work? Let's first approach it from a denotational point of view with our fact function. For brevity let's define:
では、これはどのように働くのであろうか？このfact (階乗)関数によって表示的な視点からの最初の一歩を踏み出そう。簡潔さのために次のように定義する。
fact' rec n = if n == 0 then 1 else n * rec (n-1)
So that we're computing fix fact' 5. fix will find a fixed point of fact', i.e. the function f such that f == fact' f. But let's expand what this means:
これによってfix fact' 5というように計算できるようになる。fixはfact'の不動点、すなわちf == fact' fを満たす関数 fを求めるだろう。でも、これが何を意味するのか展開してみよう。
f = fact' f = \n -> if n == 0 then 1 else n * f (n-1)
All we did was substitute rec for f in the definition of fact'. But this looks exactly like a recursive definition of a factorial function! fix feeds fact' itself as its first parameter in order to create a recursive function out of a higher-order function.
ここで行ったのは、recをfact'の定義におけるfで置き換えただけであるが、これは階乗関数の再帰的定義にそっくりである！高階関数から抜けだして、再帰的な関数を作るためにfixはfact'自身をその最初の引数として与えている。
We can also consider things from a more operational point of view. Let's actually expand the definition of 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)))
= ...
Notice that the use of fix allows us to keep "unravelling" the definition of fact': every time we hit the else clause, we product another copy of fact' via the evaluation rule fix fact' = fact' (fix fact'), which functions as the next call in the recursion chain. Eventually we hit the then clause and bottom out of this chain.
fixの使用によって fact'の定義を"分解"し続けることができていることに注意されたい。else節を入力するときはいつも、評価の規則fix fact' = fact' (fix fact')を通じて、再帰の連鎖において次の呼び出しとして機能する fact'の新たな複製を乗算しているのである。結果的にこの連鎖の外でthen節やボトムに達するのだ。
| 演習 |
|---|
|
The typed lambda calculus 型付きラムダ計算
[編集]In this section we'll expand upon a point mentioned a few times in the previous section: how fix allows us to encode recursion in the typed lambda calculus. It presumes you've already met the typed lambda calculus. Recall that in the lambda calculus, there is no let clause or top-level bindings. Every program is a simple tree of lambda abstractions, applications and literals. Let's say we want to write a fact function. Assuming we have a type called Nat for the natural numbers, we'd start out something like the following:
この節ではこれまでの節で何度か言及してきた点について展開していく。型付きラムダ計算においては、fixはどうやって再帰の書き換えを可能にしているのだろうか。あなたがすでに型付きラムダ計算を知っていると仮定する。ラムダ計算にはlet節やトップレベルの束縛は存在しないことを思い出そう。どんなプログラムもラムダ抽象、適用、リテラルのいずれかからなる単なる木である。fact関数を書きたいとしよう。自然数としてNatと呼ばれる型があるものとして、次のようにとりかかった。
λn:Nat. if iszero n then 1 else n * <blank> (n-1)
The problem is, how do we fill in the <blank>? We don't have a name for our function, so we can't call it recursively. The only way to bind names to terms is to use a lambda abstraction, so let's give that a go:
問題は、<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))
This expands to:
これはつぎのように展開される。
λn:Nat. if iszero n then 1
else n * (if iszero n-1 then 1 else (n-1) * <blank> (n-2))
We still have a <blank>. We could try to add one more layer in:
まだ <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)))
It's pretty clear we're never going to be able to get rid of this <blank>, no matter how many levels of naming we add in. Never, that is, unless we use fix, which, in essence, provides an object from which we can always unravel one more layer of recursion and still have what we started off:
何段階名前付けを加えようとも、この<blank>を取り除くことができそうもないのはどうみても明らかだ。fixを使わない限り、本質的に決して取り除くことはできず、つねに再帰のもう一段階を解くことができ、出発した時のままなのである。
fix (λf:Nat→Nat. λn:Nat. if iszero n then 1 else n * f (n-1))
This is a perfect factorial function in the typed lambda calculus plus fix.
これはfixを加えた型付きラムダ計算における完全な再帰関数だ。
fix is actually slightly more interesting than that in the context of the typed lambda calculus: if we introduce it into the language, then every type becomes inhabited, because given some concrete type T, the following expression has type T:
型付きラムダ計算の文脈においては、fixは実際にはこれよりもうすこし興味深いものである。もしこれをこの言語に導入すると、なんらかの具体的な型Tがあれば次の式は型Tを持つので、どんな型も空でない集合となる。
fix (λx:T. x)
This, in Haskell-speak, is fix id, which is denotationally ⊥. So we see that as soon as we introduce fix to the typed lambda calculus, the property that every well-typed term reduces to a value is lost.
これはHaskellでいうところのfix idであり、表示的な ⊥である。ゆえに、型付きラムダ計算にfixを導入するやいなや、あらゆる well-typed な項が値へと還元されるという性質は失われることがわかる。
Fix as a data type データ型としての Fix
[編集]It is also possible to make a fix data type in Haskell.There are three ways of defining it.
Haskell では、fix データ型を作ることも可能である。定義する方法は３つある。
newtype Fix f=Fix (f (Fix f))
or using the RankNTypes extension
もしくは、RankNTypes 拡張を利用する。
newtype Mu f=Mu (forall a.(f a->a)->a) data Nu f=forall a.Nu a (a->f a)
Mu and Nu help generalize folds, unfolds and refolds.
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 f -> Nu g refold f g=unfold g . fold f
Mu and Nu are restricted versions of Fix.
Mu と Nu は Fix の特殊化されたバージョンである。
Mu is used for making inductive noninfinite data and Nu is used for making coinductive infinite data. Eg)
Mu は帰納的な無限でないデータを作るのに使われ、Nu は余帰納的(coinductive)で無限のデータを作るのに使われる。例えば、
newpoint Stream a=Stream (Nu ((,) a)) -- forsome b. (b,b->(a,b)) newpoint Void a=Void (Mu ((,) a)) -- forall b.((a,b)->b)->b
Unlike the fix point function the fix point types do not lead to bottom. In the following code Bot is perfectly defined. It is equivalent to the unit type ().
不動点関数とは異なり、不動点型はボトムにならない。次のコードにおける Bot は完全に定義されている。これはユニット型 () と等価である。
newtype Id a=Id a newtype Bot=Bot (Fix Id) -- equals newtype Bot=Bot Bot newtype Bot=Bot Bot に等しい -- There is only one allowable term. Bot $ Bot $ Bot $ Bot .., 可能な項は一つだけ存在する。Bot $ Bot $ Bot $ Bot…
The Fix data type cannot model all forms of recursion. Take for instance this nonregular data type. Fix データ型はすべての再帰構造を作ることができない。例えば次の非正則なデータ型、
data Node a=Two a a|Three a a a data FingerTree a=U a|Up (FingerTree (Node a))
It is not easy to implement this using Fix.
これを Fix を用いて実装するのは容易ではない。