ナビゲーションに移動 検索に移動
 不動点と再帰 (Solutions) Wider Theory この章の目次を編集

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.

## Introducing `fix` fix の導入

Let's have the definition of `fix` before we go any further:

```fix :: (a -> a) -> a
fix f = f (fix f)
```

This immediately seems quite magical. Surely `fix f` will yield an infinite application stream of `f`s: `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
*** Exception: stack overflow
"hello"
[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 ("hello"++)`
• `fix (\x -> cycle (1:x))`
• `fix reverse`
• `fix id`
• `fix (\x -> take 2 \$ cycle (1:x))`

## `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:

```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 `f` in the above exercises for which you decided that `fix f` converges, verify that `fix f` finds a fixed point.

`fix f`が収束するかどうかを求めた前述の演習の関数 `f`それぞれについて、`fix f`が不動点を求めることを確かめよ。

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:

```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+)`:

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 `Int`s `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`節やボトムに達するのだ。

1. Expand the other two examples we gave above in this sense. You may need a lot of paper for the Fibonacci example!　この意味で前述した他のふたつの例を展開せよ。フィボナッチの例では大量の紙が必要になるかもしれない！
2. Write non-recursive versions of `filter` and `foldr`.　`filter``foldr`の非再帰的バージョンを書け。

## 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:

```(λ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:

```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 (λ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.

```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 ().

```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 を用いて実装するのは容易ではない。