日々の流転

λ. 英検準1級の2次試験を鵠沼女子で受けてきた。表現が言葉足らずではあったけど、去年落ちた時のように頭が真っ白になってしどろもどろになったりしなかったのでホッとしてる。僕は緊張にはすこぶる弱いのだけど、ちょうど僕の前だった女性と待ってる間に世間話出来て、それでリラックス出来たお陰のような気がする。ありがとー。で、お互い受かってるといいな〜

λ. 秋祭(あきまつり)

僕はこういう祭とかにはあんまし興味無いんで行かなかったんだけど、家族が行って、お土産にSFC-Noteというゲームを買って来た。G.A.Pというところが作ったらしい。弟が今遊んでる。

λ. gimp-1.3.0

./configureで「checking for Freetype 2.0 font support for Pango... configure: error: *** PangoFT2 0.21 or newer is required.」といわれて、freetype2-debelパッケージを入れずにpangoをビルドしていた事に気がついて、pangoをビルドし直す。時間が無いので、今日はここまで。

λ. 「酒井君は優しい人ですよ、少し横柄なだけで」と紹介されてしまう(笑)。もっと謙虚にならなくては……

λ. 東方紅魔郷ノーマルクリア(バッドエンド)

ノーマルをクリア。コンテニューしてしまったのでバッドエンドですが、今日はこれで満足。ところで、アイシクル・フォールよりもヘイルストームの方がずっと簡単だと思うのですが……

λ. 昼食

例によって学食なのだけど、アラビアータというスパゲティを初めて食べた。辛かった。

λ. Re: なんで、僕は本格ミステリが嫌いといっておきながら、森博嗣を読んでいるのだろう?

森博嗣は「本格」ではないと思うので、それは非常に正しいと思います。

λ. コンパイラ構成論

LR文法。

λ. 知的財産権論

著作権の許諾契約と委託管理等について。著作権関係の話は今日でおしまい。

λ. 企業会計論

企業会計原則とその改訂/廃止論。それから、商法、税法、証券取引法の関係とか。しかし、レジェンド問題とかジャパンプレミアム問題とかの話を聴いていると欝になるのう。

λ. 論文読み会 "PersonalRAID: Mobile Storage for Distributed and Disconnected Computers"

.

λ. 『親日派のための弁明』 金 完燮 (김 완섭) 著. 荒木 和博, 荒木 信子 [訳]

を借りた。

λ. 数学の基礎としての集合論 vs. 数学としての集合論

メモ。

λ. 各言語で作った簡易足し算器

あけてくれ日記(2003-11-18)より。ついでにHaskellでも書いてみる。

main :: IO ()
main =
    do s <- getContents
       putStrLn . show . sum . takeWhile (/= (0::Float)) . map read . lines $ s

λ. 『火車』, 宮部 みゆき

読了。

λ. 2日間みっちり！ Lispチュートリアル & Lispセミナー & Lisp事例紹介 (2)

今日は六本木ヒルズ49階。眺めがいいなぁ。

λ. Indexed types families in GHC

GHCの開発版には既に associated data type が実装されていたのね。 試してみよう。

λ. TPP2011のTPPmarkをZ3で解いてみた

昨日・今日で定理証明のイベント 7th TPP (2011) が開催されている。 私は残念ながら参加できないのだけど、お題(TPPmark)「Uniform Candy Distribution」 をSMTソルバZ3で解いてみた。

• 投稿版
• 最新版レポジトリ＠github

Z3等のSMTソルバは、通常の自動定理証明器や対話的定理証明と比べ、全称量化子や帰納法の取り扱いに制限があるため、その辺りでは苦労したものの、この程度の補助でこれだけ証明できるなら結構使えると感じた。

問題ページで、集まった解答が公開されているが、それを見ると私以外はIsabelle/HOLとCoq(+SSReflect)しか使ってなくて、他のツールの使い手は不甲斐ないなぁと思った。 ACL, PVS, Mizer あたりがいないのは参加者層が偏ってそうだ。 あと、汎用の定理証明ツールではないけど、MaudeやCafeOBJとかでどう扱われるのかとかも見てみたかったかも。