無限リストと不動点

Nobuo Yamashita @nobsun

「関数プログラミングにおいては，再帰定義は最小不動点として解釈する．」と書いてある入門書。

Nobuo Yamashita @nobsun

「定義ones=1:onesは、onesは関数(1:)の不動点であるといっている。Haskellはこれを最小不動点として解釈する。」とある。 twitter.com/nobsun/status/…

Κeіsuke Νakanο @ksknac

これはひどい． twitter.com/nobsun/status/…

Nobuo Yamashita @nobsun

@ksknac ひどいですか？

Κeіsuke Νakanο @ksknac

@nobsun 少なくとも大学では使えないですね．

Nobuo Yamashita @nobsun

@ksknac どのように直せばよいですか．

Κeіsuke Νakanο @ksknac

@nobsun onesは最小不動点ではないのでその文言は削るべきですが，入門書ならそもそも最大/最小に触れる必要はないと思います．

Nobuo Yamashita @nobsun

@ksknac 最小ではないのですか？

Κeіsuke Νakanο @ksknac

@nobsun (1:) には最小不動点はありません．

Nobuo Yamashita @nobsun

@ksknac それはどうやったら示せますか．どうも最小の意味が私には理解できていないかも．

Jun Inoue @jun0inoue

twitter.com/ksknac/status/… (´・ω・｀)? 普通に lazy list CPO における最小不動点だと思うんだけど……

Κeіsuke Νakanο @ksknac

@nobsun 帰納的定義と余帰納的定義の違いはわかりますか？

Κeіsuke Νakanο @ksknac

@jun0inoue それは普通ですか…

Nobuo Yamashita @nobsun

@ksknac すみません．そこからお願いします．

Jun Inoue @jun0inoue

@ksknac 普通です。遅延構造がない CPO とか全部フラットで面白くもなんともないので、最小不動点がどうとか言う時は何らかの遅延を考えるのは普通です。λ算法だとλに付随する遅延だけが必須ですが、元ネタはHaskellなので当然構築子も遅延で考えればいいと思います。

Jun Inoue @jun0inoue

@ksknac s/元ネタ/元ツイ/

Κeіsuke Νakanο @ksknac

@jun0inoue 「最小不動点がどうとか言う時は普通」だとすると，「普通に最小不動点」というのは違和感があります．

Nobuo Yamashita @nobsun

@ksknac TAPLの21章をまず読んでから出直します．

Jun Inoue @jun0inoue

@ksknac 何が引っかかってらっしゃるのかよく分かりませんが、「普通に」と言ったのは単に「onesを最小不動点として解釈するのは別段おかしい事ではないと思う」という意味です。件の文章に最小不動点というキーワードが出てきているので、CPOの文脈で理解すべきだと思いますし、

Κeіsuke Νakanο @ksknac

@nobsun ものすごく乱暴にいうと「Nil はリスト」「xsがリストなら a:xsもリスト」という (帰納的) 定義から構成的に作れるリストが最小不動点で， 「a:xsがストリームならxsもストリーム」のように (余帰納的) 定義のみから構成されるのが最大不動点です．

Jun Inoue @jun0inoue

@ksknac CPOを持ち出すなら (しかも言語が Haskell なので) 遅延リストのCPOは自然と視野に入りますから、数学的に間違ってるわけでも、無理筋の説明でもないよなーと思ったわけです。

Nobuo Yamashita @nobsun

@ksknac onesは最大でも最小でもないということになりますか？

Κeіsuke Νakanο @ksknac

@nobsun 私がよく見る「普通の」定義では最大ですが，twitter.com/jun0inoue/stat… のような定義で捉えるなら最小と主張できますね．

Jun Inoue @jun0inoue

@ksknac @nobsun うーん…。Nakanoさんの仰る「普通の定義」って多分、ones=⊥を解釈として認めるような定義ですよね? ちょっといい加減な言い方ですけど、集合論的に考えうる全てのones=1:onesという方程式の解を不動点として認める、みたいな。

Κeіsuke Νakanο @ksknac

@jun0inoue 無理筋の説明ではないというのは理解しました． 引っかかっていたのは「最小不動点がどうとか言う時は普通」という条件付きの普通なのにその意味で「普通に最小不動点」である，という結論ありきの論法に見えたところです．