feature image

2022年8月23日 | ブログ記事

ゆる不動点講座

こんにちは、22Bのzer0-starです。普段はインターネットの治安を守るために魔法少女として活躍しています。同志募集中です。よろしくお願いします。

この記事はtraP夏のブログリレー14日目の記事です。

ところでみなさん

不動点ってご存知ですか?

ある関数の不動点とは、となるようなのことです。すなわち、関数を適用しても変わらない(不動な)値のことです。例えば、の不動点はです。

また、関数に対しての不動点を与える(すなわちとなる)ようなを不動点コンビネータと呼んだりします。

この記事では、プログラミングにおける不動点について見ていきたいと思います。

実装

不動点コンビネータをプログラム上で実装するには、いくつか方法があります。

再帰的定義

という定義を素直に書き下せばいいです。

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

ただし、正格評価の言語(Haskell以外の大抵の言語)では、上の定義は無限に止まらない再帰を引き起こします。-変換したこちらの定義を使うと無限ループを回避できますが、関数 -> 関数の形の関数しか受け取ることができなくなります。(a() -> aに変換すれば実質同じになりますが)

PureScriptfix :: forall a b. ((a -> b) -> a -> b) -> a -> b
fix f = f (\x -> fix f x)

Yコンビネータ・Zコンビネータ

Yコンビネータというものがあります。これは、計算における不動点コンビネータのひとつです。

名前による再帰を行っていないところが注目ポイントですね。ちなみに、が実際に関数の不動点を与えることを確認するのはそう難しくないので、やってみてはいかがでしょうか。

計算で考えられたYコンビネータですが、プログラムで実装することもできます。ただし、再帰的な型が必要になるので、強い型システムが無い静的型付け言語では普通に実装できないかもしれません。

Haskellnewtype Inf a = Inf (Inf a -> a)

-- NOINLINEを付けないとインライン展開が無限に続き、コンパイルに失敗する
{-# NOINLINE runInf #-}
runInf :: Inf a -> Inf a -> a
runInf (Inf f) = f

y :: (a -> a) -> a
y f = (\x -> f (runInf x x)) (Inf \x -> f (runInf x x))

Inf aは、自分自身を適用できる関数を表す型です(Infという名前は私が適当につけました)。展開すると、という無限に再帰するヤバい関数になります。

例によって正格評価の言語だと無限ループになるので、-変換したバージョンのZコンビネータを使うと良いでしょう。

PureScriptnewtype Inf a = Inf (Inf a -> a)

runInf :: forall a. Inf a -> Inf a -> a
runInf (Inf f) = f

z :: forall a b. ((a -> b) -> (a -> b)) -> (a -> b)
z f = (\x -> f (\y -> runInf x x y)) (Inf \x -> f (\y -> runInf x x y))

コラム:

Yコンビネータに恒等関数idを適用すると、任意の型aを持つ値を取り出すことができます(当然、無限ループが生じるため実際にはになりますが)。それをプログラムとして書きなおすと、以下のようになります。

Haskellparadox :: a
paradox = (\x -> (runInf x x)) (Inf \x -> (runInf x x))

実は、このparadox(名前は適当につけました)は、カリーのパラドックスを表しています。

カリーのパラドックスとは、以下のようなパラドックスです。

「この文が真ならば、ラピュタは実在する」という文について考える。
この文が真であると仮定すると、「この文が真ならば、ラピュタは実在する」も「この文が真である」も真であるため、「ラピュタは実在する」が結論として得られる。
以上より、この文が真ならば、ラピュタは実在するということになる。これは、まさにこの文そのものであり、よってこの文は真であり、ラピュタは実在する。

より一般に、命題を、「ならば」と定義する。(すなわち、)このとき、任意の命題を証明することができる。

上で定義したInfが、まさに命題に対応しているというわけです。(newtypeのコンストラクタを剥がせば、Inf a = Inf a -> aとなっています)

また、仮定するとは引数にとることであり、モーダスポネンスとは関数適用であることを考えると、上記のラピュタのくだりは、paradoxの具体的な定義(あるいはInf aを用いてaを得るアルゴリズム)を与えているとも言えますね。

応用(再帰)

再帰とは、不動点です。

再帰関数を実装する一般的な方法は、関数に名前を付けて自分自身の定義で自分の名前を使うことです。

F#// ML系言語ではletではなくlet recを使う必要がある
let rec fib n = if n <= 1 then n else fib (n - 1) + fib (n - 2)

しかし、不動点を利用することで名前による再帰を用いずに再帰をすることができます。

今、不動点コンビネータfixが与えられていたとします。すると、例えば上の例は次のように書き換えられます。

F#// 名前による再帰をしていないので、recが必要ない!
let fib = fix (fun f n -> if n <= 1 then n else f (n - 1) + f (n - 2))

一般に、let recfixを用いてletに書き換えられます。

F#let rec hoge = ...
↓
let hoge = fix (fun hoge -> ...)

また、同じような流れ(ただし工夫は必要)で相互再帰も実現できるのですが、長くなってしまうので省きます。

というわけで

イカが

弟子

鷹!?

終わりです。楽しんでいただけましたか?

プログラミングにおける不動点という限定的なトピックなのに結構書けてびっくりしています。実は、もっと小ネタとかうんちくが出てくるんですが、小ネタすぎて記事の流れで出せないのでお蔵入りです。

割とがんばって書いたし満足しているんですが、不完全な記事が生成されることもあるので、間違いの指摘などは歓迎です。あと、わかりにくかったら言ってくださいね

以上、みんなのインターネット・魔法少女zer0-starでした。

明日の担当は@yashuさんです。楽し〜み

zer0-star icon
この記事を書いた人
zer0-star

インターネット以外全部したことあります

この記事をシェア

このエントリーをはてなブックマークに追加
共有

関連する記事

2021年8月12日
CPCTFを支えたWebshell
mazrean icon mazrean
2022年9月26日
競プロしかシラン人間が web アプリ QK Judge を作った話
tqk icon tqk
2022年9月16日
5日でゲームを作った #tararira
Komichi icon Komichi
2023年9月27日
夏のブログリレーは終わらない【駄文】
Komichi icon Komichi
2023年9月13日
ブログリレーを支えるリマインダー
H1rono_K icon H1rono_K
2023年8月21日
名取さなになりたくてOBSと連携する配信画面を作った
d_etteiu8383 icon d_etteiu8383
記事一覧 タグ一覧 Google アナリティクスについて