日々の流転

λ. 原さんに敬意を表して「ヒビルテ」というタイトルにしてみる。

λ. ウルト・ヒケウ 萌え。とか書いてみるテスト。(2006-05-18追記: Googleイメージ検索でウルト ヒケウで検索しても一件も引っかからないのは非常にけしからんと思う。)

λ. ts日記の「コトの真相（私見）」が興味深い。

λ. 三田絵美子さんの日記の5/15に「数学と論理のSAもだいぶありえない。つかえない…。」と書かれていて、自分の事かと一瞬びびった。

λ. WindowsディベロッパのLinux感

COMは，なぜもっと簡単に使えるように提供されなかったのかを考えると残念でなりません(stdioに近いレベルの概念になっていればよかったのに)．

結構同感。仕方ないとも思うけど、もう少しなんとかならなかったかなぁとも思うんだよなぁ。 簡単さといっても、開発環境がテンプレートとかの機能を充実させて実現されるような「簡単さ」じゃなくて、それこそstdioを使うくらい気軽に使えるようになっていれば……

λ. x += y

C等の言語では「+」のような2項演算子について、「x = x + y」を「x += y」と略記出来る。どうせならば、演算子に限らず、YのX上の任意のアクション f: X×Y→X について「x f= y 」と書けるようにしたらどうだろうかと一瞬思った。

λ. 今日のインストール

ocaml-3.04

-

Coq-7.2

config/coq_config.mlに「\n」が入ってしまって構文エラーになってしまうので、そこだけファイルを編集してコンパイル。本当はconfigureを編集すべきなんだけど、ocamlわかんないんで。
それから、例のお馬鹿lnへの対処。

λ. Classification と Infomorphoism の圏

情報射の条件として「f↓(b) ⊨_A α iff b ⊨_B f↑(α)」というのはやはり扱いにくい。そこで、⊨_Xを tok(X)×typ(X) から Ω = {true, false} への写像 ψ_X と考えて、射の同一性で言い換えると「すべての <α,b>: X→typ(A)×tok(B) について、ψ_A <f↓b, α> = ψ_B <b, f↑α>」になる。あんま変わらないか……

情報射を構成する写像を、最初は「f_typ, f_tok」と書いて、次に「f^∧, f^∨」と書くのが正しいと知って、昨日は書き易そうだったから「f↑, f↓」と書いてみたりと、色々な書き方をしてしまったけど、どうせならtypとtokをそれぞれ集合の圏への covariant functor と contravariant functor と考えてしまって、「typ(f), tok(f)」と書くのが良さそうな気がしてきた。何でこう表記しないんだろう。

functorといえば、4.Type-Token Dualityのflipも contravariant functor で、しかも involution だよね。

λ. あと、とりあえずは ruby-parted かなあ。。。

おぉ。libparted-rubyを引き取ってくれると嬉しいなぁ。