日々の流転

λ. 今日からゴールデンウィークか。何も予定考えてないよ。

λ. Efficient Object Sampling via Weak References

林さんの日記で知って、読んでみた。

λ. 借りた本

『最後の特派員』上巻

ダニエル・スティール(Danielle Steel)[著]

『ブギーポップ・カウントダウン - エンブリオ侵蝕』

上遠野 浩平[著]　緒方 剛志[イラスト]

λ. 円高

なんで円高に振れるのか不思議だったんだけど、横山さんの日記のNo.376を見て、なるほどと思った。

λ. エリザベス

を見た。硬派な映画だなぁ。ただ、少し物足りない感じがする。多少長くなっても構わないから、もっと詳細にエリザベスの生涯を描くべきだったと思う。

λ. "Language-Based Information-Flow Security", Andrei Sabelfeld and Andrew C. Myers

ふむ。

λ. 『政策分析入門』 E.ストーキー, R.ゼックハウザー

『政策分析入門』

E.ストーキー(Edith Stokey), R.ゼックハウザー(Richard Zeckhauser) [著], 佐藤 隆三, 加藤 寛 [監訳]

「公共選択論」の教科書。いい本らしかったので買ってみる。

λ. 昔から欺瞞に思ってた

「昔から欺瞞に思ってた」と「昔から疑問に思ってた」。それはだいぶ違う。

λ. 『不幸からの出発—アメリカの覇権の下で』, 熊沢 勉

を読んだ。理想論には興味はないが、911〜アフガン〜イラクという流れへの左派の視点が比較的分かりやすくまとまっているように思う。

λ. Agdaの紹介Flash

やねうらおさんのswf形式で動画キャプチャで紹介されていたCam Studioを使ってみたくなったので、Agdaでの簡単な証明風景をキャプチャしてみた。

ネタは、あろはさんが最近The Coq Proof Assistant A Tutorial (3) Minimal Logicで (A->B->C)->(A->B)->A->C の証明をやっていたので、それを使わせてもらった。ついでに、A->B->Aも証明*1。Setと書いた部分はPropと書いたほうが論理っぽいんだけど、AgdaではPropはSetの別名に過ぎないし、Propを定義してるライブラリを読み込みたくなかったので、Setで通した。

それから、分かり易いように各種のコマンドは固有のキーバインディングは使わず、メニューとM-xから実行してみた。まあ、細かいことはともかく、これを見るとCoqをコマンドラインから使う場合に比べ、ゴールの管理が非常に直観的なことがわかると思う。もちろん、CoqでもCoqIDEやProof Generalを使えば同じくらい直観的に使えるんだと思うけど、試したことないんでよく知らない。誰かそれらを使った証明風景をキャプチャして紹介してくれると嬉しい。

【2024-09-01】 Flashはサポートが終了しているので、YouTubeにもアップロードしてみた。

他の証明環境の紹介動画

• Twelfでの証明行為 (hyさん)
• Coq-IDEでの証明行為 (hyさん)
• Coqでニコニコ :-] (yoshihiroさん)
  • <URL:http://www.nicovideo.jp/watch/sm1276083>
  • <URL:http://jp.youtube.com/watch?v=f9XOdpmeJ0o>

λ. JSON in Haskell

激しく今更だが、ふとJSONのパーサをParsecを使って書いてみた。JSONはシンプルでいいね。コードは思ったよりも長くなってしまったので、添削きぼー。

• 最新版 JSON.hs
  • 文字をエスケープするか判断する関数を渡せるように変更
  • サロゲートペアをデコードするように変更
• 古いの
  • JSON-3.hs
  • JSON-2.hs
  • JSON-1.hs

λ. 有限モノイドへの準同型写像への逆像としての正規言語の定式化

有限モノイドへの準同型写像への逆像 : 村田　真のチャンネル -北国tvからメモ。

正規言語の定式化の一つとして、有限モノイドへの準同型 写像への逆像を用いるものがあります。(中略) 文字列の集合Lが正規であるのは、適当な有限モノイドM、 準同型f, Mの部分集合Nがあって、L = {u | f(u) はNに属する } が成立するときです。

檜山正幸のキマイラ飼育記 - 長文の反応に驚き！でも書かれてるけど、非常にスマートな定義だと思った。

λ. 5月は大分へ

5月は大分へ行くことに。

これじゃ、5月はRHG読書会も圏論勉強会もGaucheNightも参加できないか。 残念過ぎる。 が、折角なので九州方面での勉強会等に出たり、九州方面の人にお会いできたら良いなと思う。

それと、とりあえずネットワークがないと死ぬので AIR-EDGE か何かを用意せねば……*1

λ. 久しぶりのSFC

久しぶりにSFCへ。 萩野先生・服部先生・向井先生と会ってきた。

さらに、メディアセンターで図書利用券を作った。 で、早速借りたのが……『量子ファイナンス工学入門』(笑

λ. “Checking Race Freedom via Linear Programming” by Tachio Terauchi

We present a new static analysis for race freedom and race detection. The analysis checks race freedom by reducing the problem to (rational) linear programming. Unlike conventional static analyses for race freedom or race detection, our analysis avoids explicit computation of locksets and lock linearity/must-aliasness. Our analysis can handle a variety of synchronization idioms that more conventional approaches often have difficulties with, such as thread joining, semaphores, and signals. We achieve efficiency by utilizing modern linear programming solvers that can quickly solve large linear programming instances. This paper reports on the formal properties of the analysis and the experience with applying an implementation to real world C programs.

を読んだ。先日のPPL2008で発表されていたもの。そのときはちょっと良く分からなかったのだけど、改めて読んでみるとやっぱり面白いなぁ。線形計画法(linear programming)をこんなことに使えるなんて思いもよらなかった。

リファレンスにアクセスする権限をスレッド間で分け合ったり受け渡したりする。権限を少しでも持っていれば読み込みが出来て、権限を全部持っていると書き込みが出来る。それで、権限を非負の有理数で、制約を不等式で表現して、線形計画法のソルバを使って制約を充足するような割り当てが存在するかをチェックする。

C言語とpthreadで書かれたプログラムを検証するためのプロトタイプが実装済み。フロントエンドしてCILを使い、線形計画法のソルバにはGLPK (GNU Linear Programming Kit)を使っている。

ちょうど半年前くらいにGLPKとGLPKで楽しく最適化しよう！というページを知人に教えてもらったんだけど、それにしてもこんなことに使えるとは……

λ. パニックルーム

テレビでやっていたので見た。 こんな狭い舞台でどんな話が展開するのかと思ったが、結構面白かった。