Route 477

■ [prog] Curry-Howard Isomorphism

「命題 ⇔ 型」 という一対一の対応関係、そして 「証明 ⇔ プログラム」という一対一の対応関係のことをいいます。命題や証明というのが論理学の概念ですね（"命題"というのはtrueかfalseなのかを議論できるような対象のことで…例えば "1" は命題じゃないですが "1+1=2" は命題、みたいな。 "証明"はみなさんご存じのいわゆる証明です）。型やプログラムというのがλ計算などなど、プログラミング言語の世界の用語です。この二つの一見あんまり関係なさそうな世界に見事な対応関係がある、というのがCurry-Howard 対応です。

面白かったっす。僕も論理学とλ計算は教わったけど*1 はこういう話は出てこなかったと思います。

■ [ruby][SDL] on Mac OS X

新入部員の一人が(KMCには珍しく)Mac使いで、Ruby/SDLのインストールに挑戦しているようです。 Ruby/SDLとMac OS Xというと

• http://www2s.biglobe.ne.jp/~nunokawa/wiki.cgi?page=Ruby%2FSDL+on+Mac+OS+X
• http://www.kumaryu.net/?%28Ruby%29+Ruby%2FSDL%CD%D1ruby

あたりが参考になります。

「最後の一行がうまく行かない」らしいので(make install)、手動でインストールしたらOKな気がするんだけど。

• sdl.rb, rubysdl_alias.rb を /usr/local/lib/ruby/site_ruby/1.8/ あたりに
• sdl.so を /usr/local/lib/ruby/site_ruby/1.8/i386-macosx(??) あたりに

コピーします(suが必要かも)。具体的なディレクトリ名は

ruby -e 'p $LOAD_PATH'

とかやると分かるはず。