タグ

2014年8月14日のブックマーク (4件)

  • モナド教

    前提知識:モナド モナドを理解せずともモナド教を信ずることは出来ますが,理解していればより深く納得できるでしょう. 操作 :: 型 -> 型 は,"型"から"型"へ写す"操作"の存在を表します. モナドの文脈 m が必要とする2つの操作: return :: a -> m a で,値を保ちつつ文脈 m の中に入れ込むことが出来ます. (=<<) :: (a -> m b) -> (m a -> m b) で,「値を文脈に入った別の値へ写す操作」を「文脈に入った値を同じ文脈に入った別の値へ写す操作」に変換します. id :: a -> a は値をそのまま返す操作です. id を =<< で変換して得られる操作 join :: m (m a) -> m a で,二重に文脈に入った値を一重の文脈に入った値に戻すことが出来ます. 文脈の値から生の値を取り出す型 m a -> a を持つ操作は,一般

    kirakking
    kirakking 2014/08/14
    モナド教では"lift :: (Monad m, MonadTrans t) => m a -> t m a"は秘術あたりなのであろうか。
  • モナドトランスフォーマー・ステップ・バイ・ステップ(Monad Transformers Step By Step) - りんごがでている

    著者のMartin Grabmüller氏に許可をいただきましたので、 Haskellモナドトランスフォーマーのチュートリアルを翻訳したものを公開します。 タイポや誤訳、プログラムのミス等ありましたら、 Twitter宛@bicycle1885かコメント欄までご連絡頂けるとありがたいです。 元のテキストやプログラムは以下のリンクから得られます。 Monad Transformers Step by Step [2012/12/19] 誤りを多数訂正しました。id:qtamakiさん、ありがとうございます。 [2014/6/19] 誤りを2点訂正しました。id:daimatzさん、id:hitotakuchanさん、ありがとうございます。 Monad Transformers Step by Step Martin Grabmüller Oct 16 2006 概要(Abstract) この

    モナドトランスフォーマー・ステップ・バイ・ステップ(Monad Transformers Step By Step) - りんごがでている
  • Google Code Archive - Long-term storage for Google Code Project Hosting.

    Code Archive Skip to content Google About Google Privacy Terms

  • 400年の難問、「ケプラー予想の証明」やっと100%終わる

    400年の難問、「ケプラー予想の証明」やっと100%終わる2014.08.13 22:0019,492 satomi コペルニクスが提唱した地動説を、天体運行法則で不動のものにした偉人ヨハネス・ケプラー。 そのケプラーが1611年に提唱した「球は、八百屋に山盛りのオレンジみたいにピラミッド型に並べると一番沢山入る」という説が、400年の歳月を経て、100%正しかったことがコンピュータの力で証明されました。 この立体最密充填の解答は、誰でも直感的になんとなく正しいことがわかります。けれども証明するとなると超厄介で、世界歴代の天才がいくら頭脳を結集しても証明できなくて、ずっと「定理」ではなく「ケプラー予想」と呼ばれ続けてきた難題中の難題です(参考)。 証明したのは、米ピッツバーグ大学のトマス・ヘールズ教授です。もともと氏が1998年に発表し、「フェルマーの最終定理以来の難問が解けた!」と世界中

    kirakking
    kirakking 2014/08/14
    HOL/Isabelle で証明とは…。四色問題がコンピュータで解かれた有名な問題だが、次はこれか。調べよ。