日々の流転

λ. 祖母の百ヶ日なので、家族でお墓参り。

λ. war driving

どうせなので、霊園の行き返りに Netstumbler を立ち上げていたら、 約40箇所ほどヒット。chikoさんが京都に行ったときの話から、もう少しヒットするのではないかと思ってたけど、まぁこんなもんか。傾向としては、市街地よりも住宅地の方が多かったのが少し意外だった。WEPを使っていたのは18%ほどで、SSIDにはYBBUserとかデフォルトのをそのまま使ってそうなのが多かった。

λ. 昼食

濱町で「漁師のフライ定食」。濱町の割りばしの袋に書いてある箸置の折り方は、覚えたいと思うのだけど、いつもいつのまにか忘れてしまっている。

λ. war driving その2

今度はchikaとケシと藤沢方面へ。

λ. ワイヤレスネットワークの脆弱性の実証とWEPを使う上での対策

直江さんの卒論を読み返してみたり。

λ. バイオハザード

バイオハザードのDVDをケシゴムに借りた。ミラ・ジョヴォヴィッチはいいなぁ。

λ. John Major's equality

最近のAgdaにはagda-show-contextというコマンド(キーバインディングは「C-c |」)が実装されていて、これを使うと現在のコンテキストから見えるシンボルの一覧が表示できる。で、何も読み込んでいない状態で、これを実行してみたところ、幾つかの基礎的なデータ型やモナドと一緒に以下のようなシンボルが表示されているのを見つけた。

JMeq :: (A::Set) -> (x1::A) -> (B::Set) -> (x2::B) -> Set
same :: (A::Set) |-> (x1::A) |-> JMeq A x1 A x1

どうやらJMeqの唯一のデータ構築子(あるいは導入規則)がsameのようだが……これは何じゃ!?　JMeqで検索してみると、Coq-Clubメーリングリストの[Coq-Club] Playing with equalityというスレッドが見つかった。

なるほど。予め型が等しいと分かっていない二つの値を等号で結ぶための型で、(inductive familyとしての)通常の除去規則とは異なった除去規則を持っている。そして、通常の等号の型IdにUIPを追加したものと等しいと。この辺りから想像がつくが、内包的な型理論の内部では定義出来ない。そこで、CoqのCoq.Logic.JMeqではAxiomを使って定義している。agdaでもpostulateを使って同様に定義する方法もあったと思うが、agdaは組み込みの型としてJMeqのパターンマッチを特別扱いしているようだ。JMeq A a A aのような型の値には通常はcaseが使えないようチェックされているが、JMeqの場合には引っかからずにcaseが使えるできる。

それから、John Major's equality という名前が最初に使われたのは C. Mc Bride 氏の PhD thesis の Dependently Typed Functional Programs and their proofらしい。そのページのp.119に由来が書いてあった。John Major ってどっかで聞いたことのある名前だと思ったら……

It is now time to reveal the definition of ≃, the ‘John Major’ equality relation.² John Major's ‘classless society’ widened people's aspirations to equality, but also the gap between rich and poor. After all, aspiring to be equal to others than oneself is the politics of envy. In much the same way, ≃ equations between members of any type, but they cannot be treated as equals (ie substituted) unless they are of the same type. Just as before, each thing is only equal to itself.

---

² John Major was the last ever leader of the Conservative Party to be Prime Minister (1990-1997) of the United Kingdam, in case he slipped your mind.

classless society ってメージャー首相の言っていたいわゆる「階級なき社会」ってやつですね。それから、Epilogue に書いてあった「telescopic」という言葉についても p.120 に書いてあった。

λ. 今日から早昼勤

休み明けは憂鬱。「今週」4日間は早昼勤(8:00〜18:30)なので夜勤よりは楽そうだけど、プールに行けそうな時間はない。

勤務中に頭痛くなってきた。これは風邪かもわからんね。 パブロン飲んで寝る。

λ. 大掃除

ふと思い立って、部屋とPCの中身の大掃除。 色々大量に捨てる。10年前のフロッピーとかCD-Rとか。

懐かしいKondaraの箱なんかも出てきた。