日々の流転

λ. レポート

体育のレポートをようやく提出。ギリギリまで粘った上に出来も悪い。何でこうレポートの度にエグい事になるんだろう。自分のレポート生産能力の低さが嫌になる。

λ. 思うに、レポートを書くってのは基本的にいらない部分をそぎ落す作業であって、そぎ落せるだけのモノを最初に持ってないと書くのは難しい。

関連する文献などをひたすら読んでくと、「この問題についてなら、何を訊かれても自分なりの答えを示せる」って感じるようになることがある。そこまで行けば、あとは簡単で、自分なりの切口で削っていって形にすれば良いんだけど、あれやこれやの理由で、そこまで問題を掘り下げていく事が出来るとは限らない。

λ. レポートが得意な人ってのはどうやってレポートを書いているんだろう。ちょっと気になる。

λ. 夢

今日の夢はなかなか楽しかった。あんな娘なら年下でも良いかも。(笑)

はじめまして、なるほど「エンティティー霊体」ですか。今度探してみるかもしれません。僕の知ってるのは違うタイトルだったような気がしますが、やっぱり色々あるんでしょうね。

λ. 昨日のGoogle

「Gimp 発音」で検索されてる。「ギンプ」って発音するのが普通だと思うなりよ。

λ. 借りた本

• 『「スポーツ医学」のすすめⅠ』　慶応大学スポーツ医学研究センター[著] 山崎元[監修]
• 『「スポーツ医学」のすすめⅡ』　慶応大学スポーツ医学研究センター[著] 山崎元[監修]

λ. ITスキル標準人材育成研修

マルチメディアデータベースとかメタデータの話。実習では、とりあえず画像のHSV(HLSの方が良かったかも?)の各成分について平均と分散を計算してみる。SとVは確かに画像の明るさや鮮やかさやコントラストを反映した結果が出てきたけど、Hは……って、考えてみたらHの平均や分散って何やねん! 単純に計算したら意味ないよねー。というわけで、Hは無視してSとVに関するデータを使って類似度を計量しようとするわけだけど、どうしたものかちょっと悩ましい。結局、考えるのが面倒くさくなってしまって、適当な係数で調整した後、ベクトルとして内積をとってみる。あー、なんて安直な。

終わってから気がついたのだが、最初にデータを平均や分散にしてしまったのがダメで、ヒストグラムをとって、ヒストグラムの差の積分(?)で距離を定義したりすると、もうちょっと良かったんじゃないかと。あー、でもヒストグラムが櫛になってる可能性を考えると、単純にこれではあまり嬉しくないかも。むー

λ. 『国民の天皇—戦後日本の民主主義と天皇制』

小熊さんの日記で紹介されていたので読んでみた。天皇制や昭和天皇に対して漠然と持っていたイメージとはまるで異なる実像で、目から鱗が落ちた。また、現在の天皇制等を巡る政治的状況についても、私はあまり意識することはなかったが、実は結構微妙なバランスの元にあったのだな。

λ. 様相論理のシーケント計算

First Steps in Modal Logic はずっとヒルベルト流の演繹体系で通してたので知らなかったが、論理と計算のしくみ(萩谷 昌己/西崎 真也) で様相論理にもシーケント計算での証明系があることを知る。やっぱりあるのね。これは通常の命題論理のシーケント計算に、以下の必然化の推論規則を追加したもの。

A1, …, An ├ B
─────────────── (必然化)
□A1, …, □An, Γ ├ Δ, □B

ちなみに、First Steps in Modal Logic でのヒルベルト流の必然化の推論規則は以下のようなものだったので、少し趣が異なっている*1。

φ
─── (Ni)
□φ

さらに、ワンのアルゴリズムを拡張した決定手続きも載っていた。いいね。

ただ、ここでは素の様相論理のシーケント計算だけしか載っていなくて、様々な公理を追加したときにどうするかというのが分からなかった。 T(φ) := □φ→φ の形の論理式を公理として追加した場合には簡単で、以下のような推論規則を追加すればよいのだと思う。

Γ, □φ, φ ├ Δ
──────────
Γ, □φ ├ Δ

しかし、4(φ) := □φ→□□φ のような形の論理式や、より一般的な (i,j,k,l)-confluence <i>[j]φ→[k]<l>φ の場合には、どのように追加すれば良いかは良くわからなかった。例えば、4に対応する推論規則として以下を追加すると、前述の決定手続きがうまく働かなくなりそう……*2

Γ ├ Δ, □□φ, □φ
────────────
Γ ├ Δ, □□φ

私はシーケント計算とか良く知らないのだけど、シーケント計算に詳しい人にはこういうのもすぐわかったりするのだろうか。あと、様相論理の証明系の話とかは頭腐の宮本賢治さんが詳しそうだなぁ……

8/7 追記

線形論理の ! がS4様相だという話を思い出した。 4に関しては ! の規則と同様に以下のような推論規則にすれば良いはず。

□Γ ├ φ
──────
□Γ ├ □φ

ただ、5(φ) := ◇φ → □◇φ に関してはこんな風にはいかなそう。 Deep Inference and the Calculus of Structures - Modal Logic にある“The Design of Modal Proof Theories: The Case of S5”を見ると、カット除去が成り立つような S5 の推論規則にはやはり deep inference が必要なようだ。

λ. Audible で Getting Things Done の原典を

20080623#p01 にダウンロードした God's Equation はとっくに聴き終わっていて、7月分のクレジットで何を買おうかしばらく悩んでいた。 で、今日Audibleのサイトを適当に眺めていたら、たまたまGetting Things Done: The Art of Stress-Free Productivity を見かけてたので、「そういえばこれまで原典は読んだことがなかったな」と思って購入してみた。まだ聴いてないけど、David Allen 本人が読んでるのね。