日々の流転

λ. あー。プロジェクト総合講座のレポートが1/4あたりから進まない。…とか書いてみる。一応総合政策系のクラスターを志しているので、そっちのネタをある程度前面に出したいんだけど…どうもうまい具合に絡み合わない。

ところで、PowerPointのファイルになってる講義資料が多くて、かなりムカつく。何とかならんのかね〜

λ. 「Ruby-Fuを書こう」

という簡単なドキュメントを書いた。これで、RubyやRuby-Fuに入門できるとはとても思えないけど、何かのきっかけになれば良いなぁ。画像がScript-Fuのやつそのままでアレですが。

λ. 海外のメーリングリストに流れる日本語spam

海外のメーリングリストで日本語のspamを初めて見た。何か恥ずかしい。

λ. Ruby ショートサーキット論理評価

あぁ、こういう例を出せば良かったのか。なるほど。なるほど。

λ. それにしても、andやorをlisp同様に制御構造として使えるのはありがたいなりね。

λ. レポート

結局書けなかった。やっぱ、文章を書くのは苦手だわ。自分の要領の悪さが本当に嫌になる。

λ. Rubyの拡張ライブラリ

VALUEと整数を間違って相互に代入してしまうバグが多すぎ。変数への代入とかだと気が付きやすいけど、関数の引数とかだとなかなか気が付かない事がある。拡張ライブラリの作成で経験したバグの半分以上がこれだ。VALUEを構造体にしてしまえばコンパイラがチェックできるのに…

λ. プログラミング言語論レポート

提出。言語は結局Haskellを選んだ。

λ. 『土地改革の基本戦略—所有優先から利用優先へ』 岩田規久男

を借りた。岩田規久男はリフレ派の闘将というイメージが強いけど、元々はこういったのが専門。

λ. 参院選

投票してきた。私は自分の一票が「清き一票」だなんて全然思わないのだけど、組織票が大きな影響力を持っているのは嫌なので、そういう連中への嫌がらせと思って、一応欠かさず投票することにしてる。投票するからには適当に投票するのもアレなので、各党/各候補者の主張はチェックするのだけど、当然のことながら全ての論点において自分と同じ意見の政党/候補者なんて普通はいないわけで、結構悩んでしまうのだった。まぁ、結論としては自民党に投票したわけだが。

λ. HTTP 404 唯一ネ申検出

.

λ. 非外延的集合論

<URL:http://d.hatena.ne.jp/ytb/20060702/p1>

ビックリさせてしまって済みません。非外延的集合論は存在自体は知っていましたが、こんなところに役に立つのか、というのが新鮮でした。

λ. キミならどう書く 2.0 - ROUND 2 -

与えられた範囲の中でCollatz予想の収束までのステップ数が最大となる値を求める問題。とりあえず、Haskellで超素朴なコードで試してみたら「h 1000000」に40秒くらいかかった。

import List

g 1 = 1
g n = 1 + g (if even n then n `div` 2 else 3*n + 1)

h n = fst $ maximumBy c [(k, g k) | k <- [1..n]]
    where c (_,x) (_,y) = x `compare` y 

実行結果。

Main> h 100
97
Main> h 1000000
837799

以下のようにして100000までの値をテーブル化すると7秒まで縮んだ。 更に効率化するにはどうすれば良いだろう?

import List
import Array

tableMax = 100000  
table = array (1, tableMax) [(k, g' k) | k <- [1..tableMax]]

g n = if n <= tableMax then table ! n else g' n

g' 1 = 1
g' n = 1 + g (if even n then n `div` 2 else 3*n + 1)

h n = fst $ maximumBy c [(k, g k) | k <- [1..n]]
    where c (_,x) (_,y) = x `compare` y

λ. めがまり (4)

めがまりをクリアした。

ボスラッシュに苦戦するうちにボスの弱点がわかってきたので、ボスラッシュは弱点の技で適当に倒す。が、妖夢とレミリアが依然として苦手。生身のパチュリーはサウザンドナイブズで華麗にスルー。パチュリーマシンはフォースクライシスと紅色マジックでたこ殴り。クリアはできたけど、もうE缶残ってないよ。

もう余力が無かったので、最終ステージではあっさりゲームオーバーに。コンティニュー。小悪魔はパターンが簡単なので慣れれば楽勝。パチュリーカプセルはどの攻撃を撃ってくるのかが判別できずにダメージを受けてしまうのが嫌。パチュリーカプセルがかなり上の位置に現れた場合にはホーミングアミュレットで攻撃し、 自機のすぐ上に現れたときにはゴーストカッターでザクザク斬る。ラストのメカパチュリーは例によってフォースクライシスと紅色マジックで攻撃。攻撃はそれなりに激しいが、ある程度ダメージを与えたあとは、エネルギーを溜めての体当たり(?)が多くなり、これは魔法の箒を使えば比較的簡単にかわせるので結構楽。最終ステージはE缶まったく無しでクリア。

クリア後、攻略サイトを眺めていて、M缶やS缶の存在、それから四季映姫ステージのショートカットとかを知って、結構ショック。次の目標はノーコンティニュークリア?

λ. emacsagda-utf8

<URL:http://unit.aist.go.jp/cvs/Agda/>で配布されているWindowsパッケージ(Agda_1_0_2.exe)には emacsagda-utf8 というコマンドが付属しているのに気付いた。以下のような設定をすれば、ファイルをlatin-1ではなくutf-8で書けるようになる。

(setq agda-program "emacsagda-utf8")
(modify-coding-system-alist 'process "emacsagda-utf8" 'utf-8)

latin-1 なemacsagdaでは、latin-1の記号を使う都合上ファイルを latin-1 で保存せねばならず、そのためコメントにも日本語が使えず不便だった。しかし、これでこの問題も解決。 ただし、「"ほげほげ"」のようなリテラルは通るが、「"\12411\12370\12411\12370"」のような(Haskellの文法上正しい)リテラルはエラーになってしまうなぁ。

ところで、Agdaの公式サイトがいつのまにか産総研のところになっていて少し驚いたよ。

λ. デジカメ購入 (EX-V7BK)

カシオの EXILIM Hi-ZOOM (EX-V7BK) を勢いで買ってしまった。実のところそんなにデジカメを使うあてもないんだけどね……

λ. “100 years of Zermelo's axiom of choice: what was the problem with it?” by Per Martin-Löf

2004年にワークショップ「Types for Verification」で聴いたとき には断片的にしか理解できなかったので、ちゃんと読んでみた。

• 10.1093/comjnl/bxh162
• KTH/SU Mathematics Colloquium でのレクチャーノート版

選択公理は非構成的だと非難されることがあったが、Brouwer-Heyting-Kolmogorov解釈(BHK解釈)的な観点からは
(∀i : I)(∃x : S_i)A(i,x) → (∃f : Π_{i : I}S_i)(∀i : I)A(i,f(x))
という形の選択公理は完全に構成的*1(参考: Agda による選択公理の証明)。その一方で、(ある種の直観主義的集合論であるところの)トポスの理論では選択公理から排中律を導くことが出来る。その違いは何でどこに問題があるのか、という話。

ここではZermeloの選択公理の形式化のうち「集合Sの分割が与えられたときに、Sの部分集合S1で、分割の各部分A,B,C,…との共通部分が1要素になるようなものが存在する」を、集合を型理論での extentional set *2 とする解釈で解釈したものを考え、分析している。

前述の構成的な選択公理からZermeloの選択公理を証明することはできないが、これを拡張した外延的な選択公理
ExtAC = (∀i : I)(∃x : S_i)A(i,x) → (∃f : Π_{i : I}S_i)(Ext(f) ∧ (∀i : I)A(i,f(x)))
where Ext(f) = (∀i,j : I)(i =_I j → f(i) =_S f(j))
からは証明可能で、さらに同値になる。

ただし、当然ながらExtACのうちの選択関数fがExt(f)を満たすという部分は実際には導くことが出来ない部分なわけで、こうして構成的な世界で考えてみると、Zermeloの選択公理の構成的でない部分というのは、「選択関数の存在」ではなく「選択関数の外延性」だったということがわかる。

関連

• Sets in types, types in sets - ヒビルテ(2008-09-21)