kt3k 日記

スポンサーサイト

上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

MAKULA オープン

makula


フォトブログの MAKULA というサイトを作成しました。
若い写真家の人たちが、日常の中とか、作品制作の中で撮った写真を
気ままにアップロードするという趣旨のサイト。

注) IE6 非対応

スポンサーサイト

プロジェクトオイラー、久々に

euler_portrait

久々に Project Euler を2問ぐらい解いた。
ランキングが復活したり、スタティスティックスが復活したり、
サービスが向上(回復?)していた。
フォーラムを見ていたら、最近 anarchy golf - python でよく見かける hallvabo さんが
Norway norway_flag の人らしいということが分かった。

何回目かの考究

shoenfield_book

ゼミで Shoenfield, Mathematical logic の 115p - 119p
を発表。後半をあまり予習してなかったので、後半がだいぶグダグダ
な感じになって、聞いてる人に申し訳ない感じの発表になった。
でも、前半で、lemma の条件で β(a, i) <= a - 1 という条件不要じゃないか?
とか、page116, line16 l, j の条件は、1 <= j < l <= c じゃないかとか
おもしろい(と思える)突っ込みがあって、楽しかったので、トータルOK

LCM of 1 to n

anarchy golfLCM of 1 to n という問題が出てたので回答。(1ゲット)
出題1時間以上で、誰も解いてなかったので、もしかしたら、最後の方の
出力が計算が間に合わないのか?とか疑いながらコードを書いていたけど、
普通に、1 から n の lcm を地道に計算して解けた。書いてる途中で、
lcm(lcm(k, m), n) = lcm(k, m, n)
が成り立つんだったかどうだか、が不安になって、理由を考えながらコードを書いてたけど、
確かな証明が思い浮かぶ前にコードが書き終わってた。

Alnum challenge(?)

anarchy golf で、Alnum challenge という問題を出題。
説明文の、using as few symbols as possible の部分が「できるだけ、少ないシンボル数で」
というつもりで書いてたんだけど、「できるだけ小さなシンボルコードで」(つまり全く逆)
の意味にも取れることに気がついて、ちょっと悲しくなった・・・。
まあ、でも、そういうの関係なく解いてくれてる人もいるので、まあいいや・・・

追記(2008/11/03):
答えオープン。
一部の言語で、普段見掛けない感じのコードがいくつか上がってたので、良かったかな

立ち話

DJ、FLASHer、考究仲間の(qre)さんと2時間ぐらい立ち話した。

今日は考究が途中で中断して、みんなでゾロゾロ歩いて、
コレを聞きに行った。ACL2という証明器で、quicksort がソートできている
事を証明するデモなんかを眺めた。Ruben Gamboa さんという人が実装したという、
ACL2(r)というACL2の拡張で、解析学の定理を証明した話の紹介が興味深かった。

考究では、論理以外の公理を持たない理論の中で、existential な論理式が定理である
ためには、その論理式の matrix のインスタンス達を or でつないだもののうちで、
quasi-toutology になるものが存在することが必要十分であるということ(棒読み)を証明した。
(consistency theorem とか、prenex operation の基本的性質が証明済みなので、そこまで
難しくない。)

shoenfield


上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。