日々の流転

λ. はぁ。俺ってダメダメじゃん。まったく使えない奴だ。

λ. 認知科学

過去問が配られたのだけど、それに以下のような問題が載っていた。ましゅまろ部会ネタかと一瞬思ってしまった。

<問題12> マシュマロ・テストに関する適切な記述を次の中から選びなさい。

1. 甘さなどの味覚のテスト。
2. 柔らかさなどの触覚のテスト。
3. 大人にはあまり有効でない。
4. 知的な潜在能力を開花させる上で重要である。
5. 衝動を抑える能力を見る。
6. 情動を制御するテスト。

λ. Wiki

これまで放置していた自分のRWikiを最近少し使いだした。日記は流れていってしまうので、 流れていって欲しくないネタはこっちに書こっと。

λ. Ruby-CPL

Closed Functorial Expression のunificationを書いた。ちょっと手を抜いてるけど。

λ. category.rb導入

ふとこの日記にもcategory.rbを導入してみる。ちゃんとカテゴライズしてあれば便利そう。過去のエントリーも少しはカテゴライズしておこう。

λ. 『ネガティブハッピー・チェーンソーエッヂ』, 滝本 竜彦

を読んだ。読み終わってから気づいたのだけど『NHKにようこそ!』と作者同じなのか。

λ. フェイスオフ

たまたまテレビでやっていたので見た。最初は全然期待してなかったのだけど、面白かった。

λ. 何か変な夢見た

何か変な夢見た。 切羽詰ってくると変な夢みるよなぁ。

λ. ハマスとファタハ間の緊張高まる - パレスチナ自治区

とおやまさんのところから。 なんでハルヒなんだろう……

【追記】 翌日、S氏にファンタ with 涼宮ハルヒの憂鬱というのを紹介されて、「ファタハ with 涼宮ハルヒの憂鬱」と激しく空目した。

λ. SATCHMOで遊ぶ

先日の渕一博記念コロキウム『論理と推論技術：四半世紀の展開』での長谷川隆三氏の発表『モデル生成型定理証明系MGTPの要素技術』(スライド)で紹介されていたSATCHMOで少し遊んでみる。 これは節集合のモデルを作ることで、充足可能性を証明するのだとか。なので、当然、証明したい論理式の否定を与えてモデルが存在しないことを確認すれば、その論理式が恒真であることがわかるので、定理証明機として使うことが出来ると。

スライドで紹介されていたソースコードそのままだと SWI Prolog に怒られてしまったので、演算子の優先順位とあと動的に変化する述語をdynamicディレクティブで指示するようにしておく。

% satchmo.pl
:- op(1200, xfy, '--->').
:- dynamic false/0.

satisfiable :- is_violated(C), !, satisfy(C), satisfiable.
satisfiable.

is_violated(C) :- (A--->C), call(A), not(C).

satisfy(C) :- component(X,C), asserta(X),
              on_backtracking(retract(X)),
              not(false).

component(X,(Y;Z)) :- !, (X=Y; component(X,Z)).
component(X,X).

on_backtracking(_).
on_backtracking(X) :- call(X), !, fail.

しかし、トリッキーだなぁ。 Prologはこういうのが書けるのが楽しい。

問題S1

まずはスライドにあった問題S1。 Prologと同じで「,」がandで「;」がorを表している。

% s1.pl
:- dynamic p/1, q/1, r/1, s/1.

true ---> p(a); q(b).
q(X) ---> s(f(X)).
r(X) ---> s(X).
p(X) ---> q(X); r(X).
p(X), s(X) ---> false.
q(X), s(Y) ---> false.

で、satchmoを呼び出して充足可能性をチェック。

?- consult(satchmo).
Yes
?- consult(s1).
Yes
?- satisfiable.
No
?- 

うん、ちゃんと充足不可能なことを示してくれた。

モデルが存在する例

次はちゃんとモデルが存在する例を試してみる。

% hoge.pl
:- dynamic p/1, q/1.

true ---> p(x); q(x).
p(X) ---> false.
q(X) ---> q(X).

実行。

?- consult(satchmo).
Yes
?- consult(hoge).  
Yes
?- satisfiable.  
Yes

というわけで、充足可能なことが分かったので、今度はlistingを使ってPrologのデータベース中の述語を表示してモデルを調べてみる。

?- listing.
(略)
:- dynamic q/1.
q(x).
(略)

値域限定

色々と試していたら、satisfiableはNoになって欲しい節集合で、試したらYesになってしまったものがあって、どうしてなのか少し悩んでしまった。 原因は、SATCHMOの仮定している値域限定「節の結論部に現れる変数は仮定部にも現れなくてはならない」という制約に違反してしまっていたからだった。 なるほど、なるほど。

λ. iKnowの「旅に出よう！（出国＆街を歩く）」を完了

iKnowで2008-11-20に始めたコース「旅に出よう！（出国＆街を歩く）」が終わった。次は「旅を楽しもう！（レストラン＆ホテル）」をやる予定なので、「プロの英語（企業会計編）」はまだしばらくおあずけ。

ところで、私の知り合いで iKnow をやってる人がいましたら、よかったら一緒にやりませんか〜?
(⇒ 私のアカウント: <URL:http://www.iknow.co.jp/user/sakai>)

λ. お菓子補充

貯蔵していたお菓子が尽きたので補充。