無限リストと不動点

Jun Inoue @jun0inoue

@ksknac @nobsun でも(:)をあくまでHaskellの(:)と解釈すると、ones=⊥はones=1:onesの解釈になりません。なぜならその二つからは1:⊥=⊥が導け、(:)が遅延構築子ではない事が示せるからです。ones=⊥は正格な構築子の場合の解になりますが、

Κeіsuke Νakanο @ksknac

@jun0inoue @nobsun おっしゃることはわかります． Haskellの(:)の意味は確かにそうなのですが，(Haskellの入門書ということなので) Haskellを知らない人に(:)の非正格性を説明せずに「onesは最小不動点だ」と主張するのは無理がありませんか？

Jun Inoue @jun0inoue

@ksknac @nobsun 正格な(:)と非正格な(:)は別の関数ですから「Haskellでones=1:onesの解は?」という問に対する答えとして⊥は不適切です。あくまで(:)をHaskellのそれと解釈する限りでは自明な無限リストが最小解です。

Nobuo Yamashita @nobsun

なんで最小ではないのかが判らなかったんですが，⊥＝1:⊥ という解釈だとそういことになるんですね．理解しました． twitter.com/jun0inoue/stat…

Jun Inoue @jun0inoue

@ksknac @nobsun 元の本を読んでないので分かりませんが、そもそもHaskellすら知らない人に不動点の話をすること自体非生産的だと思います。しかし教育的効果の程はともかく、数学的には間違ってませんし、そういう意味でトンデモとかではないです。無闇に難解なだけ。

Nobuo Yamashita @nobsun

@ksknac @jun0inoue すみません．その点を予め説明してませんでした．データコンストラクタの非正格性も，無限リストを近似列の極限として考えられるという話もでてきたあとの主張です．

Jun Inoue @jun0inoue

@ksknac @nobsun ちょっとしつこくてすいませんけど、これはリストという「型」(を解釈する集合や対象)が最小不動点、ストリームという「型」が最大不動点という事であって、onesという「項(ないし値)」が最小かどうかとはまた違った話です。

Jun Inoue @jun0inoue

twitter.com/nobsun/status/… 入門…書……? ((((；ﾟДﾟ))))

Κeіsuke Νakanο @ksknac

@jun0inoue @nobsun すみません．文脈から誤解を招くかもしれませんが， 帰納的定義と余帰納的定義の話をしたかっただけでした．

Jun Inoue @jun0inoue

@ksknac @nobsun あ、これは失礼しました。

Nobuo Yamashita @nobsun

@jun0inoue @ksknac もったいを付けたみたいですみません． "Thinking Functionally with Haskell"というIFPHの全面改訂版での記述です．旧版のIFPHでも9章に無限リストを近似列の極限として考えるという話がでてきます:)

Jun Inoue @jun0inoue

@nobsun @ksknac あー Bird さんの鈍器か。道理で。

Masahiro Sakai @masahiro_sakai

@nobsun @ksknac @jun0inoue リストっぽい終余代数(バリエーションは幾つかありますが)で解釈するなら、終余代数の普遍性から ones = 1 : ones の解は一意なので、最小不動点かつ最大不動点です。