日々の流転

λ. 買った本

「BASTARD!! 黒い虹I」

萩原一至[原作&イラスト]　ベニー松山[文]

「六人の超音波科学者 - Six Supersonic Scientists」

森博嗣[著]

Software Design 10月号

-

サイゾー 10月号

-

λ. 昼

昼は例によって家族でスカイラーク・グリル。

λ. 学校

時間割を貰いたかったのと、生協で買いたい本があったのとで、なんとなく大学に行ったんだけど、事務も生協もメディアセンターもしまってて、無駄足。24時間キャンパスは365日キャンパスではないのね…

λ. しっかし、人がいないなぁ。少々まぶしい陽光、コンクリート打ちはなしの建物、手入れの行き届いた緑、お祭でもやっているのか遠くから規則的に聴こえてくる太鼓の音、施設設備のこれまた規則的な小さな機械音−おそらくはポンプだろうか。

秋晴れの空を流れるわずかな雲を見ていると、どこか違う世界に迷い込んでしまったのではないかと怖くなる。建物があり、技術があり、文明がある。それなのにそれを生み出したはずの人間の姿だけが欠けている世界。とても畏ろしい。

摂理への反逆、忌まわしい予定調和。そんな言葉が頭に浮かんでは、眩暈を感じる。既視感に酔ってる自分を自覚して、ますます虚しくなる。あー、くだらねー

λ. 某氏が「悪代官」というゲームにはまってる。つーか、悪代官が「赤い彗星!?」とかいってんじゃねーよ。(微笑)

λ. 「海外援助の理念と実際 ……についての、講義をさぼった人にも多少はわかるかもしれないアンチョコ資料」

を読んだ。

λ. 夕食

家族で焼き肉屋へ。

λ. 読書

『X』18

CLAMP

λ. データ型

についてヘロヘロと考える。coherent condition (+α)を満たすようなcoercingを用いてsubtypeを定義するならば、全てのsupertypeは当然「ただ一つの値からなる、何の操作も定義されていない型」のではないか? これは型を値の集合として考えたときの姿とあまりにも違いすぎる……

λ. Agdaプラグイン機構; 池上 大介

を読んだ。使う側のインターフェースはシンプルでいい感じ。external予約語で書かれた項は、型チェック時に外部ツールが呼ばれる以外はabstractが指定された項と同じ扱いなのかな。それと、FOLプラグインの使用例を見ると、外部ツールには型情報も渡しているのかな。

λ. let rec と循環的定義と有理数と

ふと、OCaml で let rec を使って定義される値というのは有理数に似てるなと思った。リスト型を例にとると、任意の無限リストではなく途中で循環が現れる無限リストだけが表現可能で、これは循環小数(=有理数)に似ている。それから、自然数がinductiveで実数がcoinductiveなので、その中間は有理数だろうという安直な思いつき。

といって、そのような不動点を特徴付ける原理が思い浮かぶわけでもないけど。

【2006-09-26追記】 そのものずばり rational type という概念があることを知った。 そういや、rational tree というのもあったなぁ。 これらが圏論の言葉で定義できるかが気になる。

【2006-09-29追記】 キャリアが有限集合であるF余代数とそれらの準同型からなる圏を CoAlg(F)_fin とする。忘却関手 U_F: CoAlg(F)_fin→Set の余極限を考えるのはどうか?　……いや、このアプローチはイマイチな気がする。むしろ Adámek らの方法の特別な場合と考えることが出来ないかどうかを考えたほうが良いか?

λ. 『アンチ・ハウス』 森博嗣, 阿竹克人

を読んだ。

λ. 進化するモバイルノートPC

東芝レビュー8月号 の特集「進化するモバイルノートPC」を見ていて、最近のノートPCは凄いんだなぁと思った。

λ. ルービックキューブ

ルービックキューブを解いていたら、以下の写真のようになってしまった。 中央のマスの向きが合わなくても、絵柄はそろうんだなぁ。

λ. How a CDCL SAT solver works

1年くらい前に、知人にSATソルバの動作を説明しようとして、ちょうど良い資料がなくて、紙で頑張って説明したのを、スライド化してみた。 単純な分割統治による探索とはちょっと違った動作になっているのが分かると思う。

資料 (PDF, Keynote)

参考図書