2011-01-07
A modular formalisation of finite group theory http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.122.5995 という論文を眺めたりした。CoqとCoqのライブラリであるSSReflectを使って、Feit-Thompsonの定理の証明を形式化しようという話らしい。試みとしては面白いけど、研究としてはどうなんだろうっていう。まあ、頑張ればきっと書けるのは書けるんだろうし(とてもしんどいとは思うけど)。 こういうのは、Wikipediaみたいに、ヒマ人がちょこちょこCoqのコードを投げていくと、そのうち証明が完成するというスタイルがいいんじゃないかとか思ったりもした。Wikipediaスタイルで、有志で完全にformalな数学辞典を作るとかは結構面白い気がする。名前は、Bourba
僕でもわかる継続と部分継続 - まめめも
callcc と shift/reset についてわかるとこだけ書いてみます。 継続 callcc という操作は、現在から実行終了まで、継続をまるごと取り出します。例題。 p [1] + callcc {|k| [2] + k.call([3]) } #=> [1, 3] callcc では callcc がリターンしてから実行終了するまでの継続 k が取り出せます。k.call([3]) で継続が呼ばれると、いきなり「callcc が [3] を返した瞬間」に実行が飛びます。つまりこんな感じ。 p [1] + [3] あとは自明ですね。"[2] +" のあたりは無視されます。 部分継続 shift という操作は、現在から reset まで、継続の一部だけを取り出します。この継続の一部を部分継続といいます。例題。 p [1] + reset { [2] + shift {|k| [3] +
Haskellと確率と限定継続 - Life Goes On
会社の勉強会で、Haskell による確率プログラミングについて話しました。 元ネタは Oleg さんの論文（Probabilistic Programming）です。OCaml で書かれていたプログラムを Haskell に翻訳しながら解説しました。 もともとの論文の主張は、木探索として定義したモデルを継続渡し方式（Continuation-Passing Style / CPS）にすることで効率化できる、さらに限定継続を利用することで、継続を意識せず直接方式（Direct Style）で書けるようになるというものでした。 木探索から CPS にすることで効率化という流れは Haskell でも同じなのですが、限定継続を利用しても直接方式では書けないため、あまり嬉しくありません。でも Haskell には do 記法があるので、モナドとして定義すれば擬似的に直接方式で書けてハッピーという
2010-06-27
第三回ProofCafeが開催されました。CPDTの Inductive Types の前半を読みました。 個人的には injective タクティックを使ったことがなかったので次から積極的に使おうと思いました。 この記事の続きはこちら 三次会では Olegさんによる限定継続モナド を触っていた。 これまで皆が使っているのを指をくわえて見ていたけど、自分でもやっと使いこなせるようになってきた気がする。うれしくなったのでこの記事を書く。 説明では疑似Haskellっぽい構文を使う。実際にOlegの限定継続モナドを使う場合はそれっぽく型を合わせる必要がある。 私の限定継続の理解 私の shift と reset はこういう理解： reset e 内側(引き数)にshiftが無ければ、中身(e)をそのまま返す shiftがあれば、shiftによる大域脱出の効果をそこまでに限定する (つまりこの時
限定継続モナドと再帰 - keigoiの日記
この記事の続きはこちら 三次会では Olegさんによる限定継続モナド を触っていた。 これまで皆が使っているのを指をくわえて見ていたけど、自分でもやっと使いこなせるようになってきた気がする。うれしくなったのでこの記事を書く。 説明では疑似Haskellっぽい構文を使う。実際にOlegの限定継続モナドを使う場合はそれっぽく型を合わせる必要がある。 私の限定継続の理解 私の shift と reset はこういう理解： reset e 内側(引き数)にshiftが無ければ、中身(e)をそのまま返す shiftがあれば、shiftによる大域脱出の効果をそこまでに限定する (つまりこの時点での継続を「捕まえておく」) shift f 限定継続kを取り出して、f k を計算し、その値で reset まで大域脱出する (つまりresetで捕まえていた継続を呼ぶ) このkは、引き数を渡すと shift
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
