2010年07月02日のツイート

@kururu_goedel: @minami106 ポスドクやっていたところの(当時の)学科長は、オフィスに「Yes! We are clopen」と書いてある冗談の看板を貼ってました。

2010-07-02 14:57:01 via Seesmic to @minami106

@kururu_goedel: はてダのtwitter報告は扱いが難しいなぁ。ひとつ前のtweetは自分のブログ更新ね。

2010-07-02 14:08:57 via Seesmic

@kururu_goedel: Coqでの(普通の)たらい回し関数の停止性証明。多分かなり変。 URL

2010-07-02 14:06:05 via Hatena

@kururu_goedel: さてと、それでは査読やるか。この論文はこれで四本目の査読報告でもう一年以上の付き合いか。結果自体はニッチっぽいけれども、価値のある論文だと思うので、きちんと間違いや不明な点を叩き出してから送り出してやらねば。

2010-07-02 13:32:42 via Seesmic

@kururu_goedel: 査読中は、頭の中で自動修正しそうになるタイポとか論理の飛躍とかにも気をつけて読みながら、引用されている定理がちゃんと参照されている論文にあるか確認したり、証明が間違っているときには修正の方針考えたりして。ほとんど自分の論文と同じくらいに真面目に向きあってやるわけで。

2010-07-02 13:27:30 via Seesmic

@kururu_goedel: @mskota 分野の違いはあるのだろうと思いますが、一生懸命査読しているのを「当然の義務を果たしているだけ」と言われたらショックだなぁと思いますし、無償で面倒な作業をした上で匿名でいることになる査読者の人たちには本当に感謝しています。

2010-07-02 13:22:14 via Seesmic to @mskota

@kururu_goedel: @mskota 査読者には(謝辞に入れなくても)感謝してあげてくださいよ……。

2010-07-02 13:06:05 via web to @mskota

@kururu_goedel: ここ数日間、いやもっと長いか、やっていた普通のたらい回し関数の停止性のCoqによる証明がようやくできた。とてつもなくawkwardな感じだけれども、できたにはできた。

2010-07-02 12:43:54 via Seesmic

@kururu_goedel: ようやく違い。

2010-07-02 12:43:46 via Seesmic

@kururu_goedel: ここ数日間、いやもっと長いか、やっていた普通のたらい回し関数の停止性のCoqによる証明が要約できた。とてつもなくawkwardな感じだけれども、できたにはできた。

2010-07-02 12:40:21 via Seesmic

やったー、Coqでのたらい回し関数の停止性証明できたよー

Call-by-name版なので簡単ですけど。ものすごく下手なソースだと思いますが、一応晒しておきます。