日々の流転

λ. 猿の惑星

今日も眠れなかった、くそう。朝、親父と「猿の惑星」見て来た。エンターテイメント指向なのか何なのか知らんが、終始ご都合主義がかいま見えて、いまいち感情移入の出来ない映画だった。しかし、不条理で、しかも間の抜けたラストはなかなか良かった。そこだけは前作よりも個人的には好きだ。ところで、「トゥーム・レイダー」の予告をやってたんだけど、こっちは笑えた。「惑星直列が起こるとき、世界は終る」って、グラハム・ハンコックじゃないんだからさ(笑)

λ. 日記は現代の病

ちなみに元ネタは、自己の内面を日記につけ、そしてそれを公開さえすることを、ポール・ブルジェが「近代精神の病」と評した事だったりします。今年のセンター試験の国語で富永茂樹の「都市の憂鬱」が出たので知ってる人も多いかも。

λ. Gimp用のNamazuフィルタ

Gimp共同掲示板より。突っ込みもそちらへお願いします。

そういえば、namazu 2.0.6 がリリースされましたね。
ふと思い付いたんですが、
xcfファイル用のnamazuのフィルタを誰か作りませんか?
レイヤ名やコメントでxcfファイルを検索できたら面白そう。

Namazu文書フィルタの作成方法
http://namazu.org/~kenji/dekiru-namazu-filter.txt

λ. どうしても取れないバグがあって徹夜してしまったのだけど、実は一カ所INT2FIXを忘れていたのが原因だった。阿保らし。

λ. 「幻の大戦果 〜台湾沖航空戦の真相〜」というのをテレビでやっていたので見た。面白かった。

λ. 新宿鮫の続きを見た。

λ. 水泳

近所のプールで久しぶりに泳いできた。泳ぐのは多分1年ぶりくらいなので、とりあえず1キロほど。1時間くらいしかプールにはいなかったのだけど日焼けした。肩がヒリヒリする。

λ. iconv-io 0.0.5

速攻でakrさんにバグを指摘される。以前の実装のときに書いたコードをろくにテストもせずに入れていました。お恥ずかしい限りです。というわけで、0.0.5を出しました。

それと、たしかに UTF-16LE での each_line というのは現状では難しいですね。$/ = "\n\0" だけじゃだめですし……

λ. 第九回圏論勉強会

圏論勉強会。

λ. 第二十回圏論勉強会

世間はコミケだが、にも関わらず今日は圏論勉強会だった。写真。

λ. got Nintendo DS Lite

Two weeks ago I wrote that I had failed to buy Nintendo DS Lite. After that I enjoyed playing MAD PEOPLE instead and forgot about DS. But as my first game of MAD PEOPLE was over, I came to want DS again... Today, on my way home I stopped by the game shop "θ" and bought Nintendo DS Lite, Mario Kart DS and えいご漬け. As you know, Mario Kart is a famous racing game. And えいご漬け is a game for training English ability. As soon as I came home, I began to play them. They are exciting. Now I and my brother are obsessed with them.

λ. OSConでのSimon Peyton Jonesの講演

<URL:http://d.hatena.ne.jp/desumasu/20070811/1186838102> よりメモ。 長いので、ちょっとだけ見た。

• スライド
• OSCON 2007 - Simon Peyton-Jones - A Taste of Haskell Part I
• OSCON 2007 - Simon Peyton-Jones - A Taste of Haskell Part II

λ. 箱根 彫刻の森美術館

箱根 彫刻の森美術館 に行ってきた。奇怪なオブジェが沢山あって楽しい。昔、子供のころにも行ったことがあるはずなのだけど、それはあまり覚えてなくて、むしろ「これ美術の教科書でみたことあるな」という方が多かった。有名な作品は置いておくとして、個人的に少し印象に残ったのは、峯孝の1972のプリマヴェラ(Primavera)という作品。それから、足湯につかってきた。

λ. “The IDP framework for declarative problem solving” by Maarten Mariën, Johan Wittocx, and Marc Denecker

以前2009-03-04に数独を解いてみたIDP(Inductive Definition Programming)フレームワークの解説。背後にあるロジック、記述言語、動作例が中心で、ソルバーの仕組みにはあまり触れていない。

IDPの背後にあるロジックは、ソート付きの一階述語論理を帰納的定義で拡張したもので、問題は「指標Σ, セオリーT, 部分指標σ⊆Σ, 有限のσ構造A_Iの組〈Σ, T, σ, A_I〉が与えられたときに、A_Iの拡張で(A|_σ = A_I)、Tを満たす(A ⊨ T)ようなΣ構造Aを求める」というモデル拡張問題(model expansion problem)として形式化される。

また、問題の記述スタイルとしては、問題の一般的なルールをΣとTによって記述し、具体的な盤面など問題のインスタンスに固有の情報をA_Iで与えるというスタイルになっているのが面白い。

実装については以下のように書いてあった。

Its algorithms consist of an adaption of the DLL algorithm to rules, augmented with a variant of Smodels' AtMost. As such, the solver incorporates techniques from state of the art SAT and ASP solvers.

読んでると、解集合プログラミング(Answer Set Programming, ASP)との比較をかなりしている一方で、MaceやParadox等の一階述語論理のモデル発見器(model finder)については全く言及してなくて、ちょっと意外な感じがした。 ASPは最小エルブランモデルの一般化であるところの解集合を求めるので、ある意味全体が帰納的定義になっている一方で、一階述語論理のモデル発見器は帰納的定義が出来ないので、比較対象としてはASPの方が適当ということなのかな。 ただ、ASPが項をエルブラン宇宙で解釈するのに対して、IDPは一階述語論理のモデル発見器は任意の解釈をするので、実装的には一階述語論理のモデル発見器に近い部分もあると思うし、帰納的定義の追加による性能への影響とかも気になることは気になる。

それから、ちょっと気になったのは、以下の部分。

A historical AI argument (e.g. [15]) against FO as a computational logic is the semi-decidability of the deduction problem (and worse, undecidability in the case of FO(ID)).

一階述語論理FOがsemi-decidableなのはいいんだけど、一階述語論理に帰納的定義を加えたFO(ID)がundedidableというのはホント?　一階述語論理と同様に証明を枚挙して証明チェッカにかけるという方法は使えないのだろうか?

λ. お墓参りなど

家族でお墓参り。渋滞にはまってウンザリ。あと、やっぱり暑い。 お昼は、竹治(たけはる)というところで、まぐろ重なるものを食べた。

それから、プールでひと泳ぎし、夜は帰省した友人らと飲み会。 はじめて飲み会後にラーメン屋にいくなど。