離散的に時間をとらえる場合のメタファ

　最近、また夢をよく見るようになった。夢を見る＝眠りが浅いという意味である。過去に夢を見るとだいたいあり得ないぐらいの悪夢であった。しかし、最近の夢はやたら示唆的だ。起きている時よりはるかに頭を使わないと出てこないような発想や検討をしている過程をすべて夢で見ている。これは、前回の発作以降、起きている時に不調であまり物事を考えることができなくなっていることへの脳の一種の反抗なのか。
　今日の夢は、俺は大学生だという設定。新しい教授が来て、彼が俺のそれまでの研究（現実の会社での研究がそれにあたっている）を徹底的に批判され、それに対して反証するというようなものだった。その教授はやたら痛いところを論理的に突いてくる。これはきつい。ただ、それに対して俺もいろいろ考えて反論する。それがまた論理的で気持ちがいい。なんかものすごくエキサイティングな夢だった。これなら夢のほうがよっぽど成果を出しそうだ。
　その中で、過去のWebサービスの自動的な合成をSituation Calculusという手法を用いて導出するという研究に対して教授にダメ出しされた。そして、なぜかその秘書に、時間は離散的にとらえられるものでないのに、なぜ離散的にとらえる手法が有効なのかわかんない、普通に微分方程式を使えばよいのではと言われて、その正当性を秘書の人にもわかるように説明するべきメタファを求められていた。そして、俺は、離散的に時間をとらえるというのは決して時間を羊羹のようにとらえて、それを区切るということではない（微分方程式は時間をこのようにとらえて、羊羹の長さが限りなく微小になったら？という発想で定式化している）、時間をperiodicalに時刻で切り出し、その切り出した時刻の状態を述語論理でモデル化し、時刻的に近接であるモデル間の関係を時刻に対して全称的に表現する、それがSituation Calculusである。そしてやり方でモデル化できるもののみがSituation Calculusの対象になる。で、このようなモデル化はメタファとして「だるまさんが転んだ」を考えてほしい。鬼が木のほうを向いている時にもみんな動いている。けど、鬼が振り向いた時だけが現実であり時間が固定された状態として扱うというモデルなんだ。と。そんなことを夢で自分は、教授と秘書に言っていた。なかなかいいことを言っている、夢の俺。実際、その夢の振り返りで、「だるまさんが転んだ」モデルで時間をとらえるというメタファで、ようやく過去に勉強したSituation Calculusを本当に理解した気がする。いまさらだが。