日々の流転

λ. ひぐらしのなく頃に

2004年の夏コミで買ったのを今頃になってプレイ中。まだ鬼隠し編と綿流し編をプレイしただけだけど、えぐえぐなストーリーがとてもとても(・∀・)イイね。

今のところネタばれが怖くてネット上の情報は全然見ていないのだけど、複数のシナリオの関係ってどうなっているんだろう。パラレルワールド?　基本的な設定は同じと思ってよいのだろうか?　もしそうなのだとしたら、あるシナリオで疑問だった点が別のシナリオで解けたりして、なかなか面白い構成になっていると思う。

謎については、超常現象を否定するならば、ほとんどの解は論理的帰結であるか、あるいはそもそもゲーム中の情報からは推理困難なものであるかのように思った*1。ただ、やっぱりどうしても説明がつかない点もあって気になるところ。しかし、ほとんどの謎は論理的に説明できるけど、ほんの少しだけ説明が付かないところが残るという匙加減がうまい*2。他のシナリオが気になるなぁ。

ついでに、ひぐらし人狼も少しプレイしてみたくなった。

疑問点や気になる点 (ネタバレ注意?)

• 富竹と鬼隠し編の圭一の怪死の原因は何か?
• 鬼隠し編の最後に圭一がオヤシロ様の存在を突然信じたのは何故?
• 自分の死を偽装したであろう鷹野(と呼ばれる人物)はその後何をしていたのか?
• 詩音と鷹野の間には何らかの協力関係があったか?
• 綿流し編の祭具殿で、富竹と詩音にだけ聴こえた「子供が跳ねるような音」というのは何か?
• 綿流し編、詩音が自らの計画に圭一を巻き込むことに必然性はあったのか?
• 綿流し編、梨花の持っていた注射器は何か?
• 綿流し編の最後のシーン、ベットに下に居たのは誰?　圭一の夢ないしは妄想?

λ. 自宅に無線LANを導入

この季節、コタツに入ってテレビを見ながらネットが出来ないのは悲しい。ということで、自宅に無線LANを導入してみる。

アクセスポイントは適当に安そうな WHR-G54S/P を買ってみた。802.11gのカードが一枚ついて¥8,355だった。 このカードは無線LAN内蔵していない親父のノートパソコン用。 僕の Let's note CF-T1PWAXS に内臓のは11bだけで11gに対応してないのが残念だけど、速度が不満になるのは時々だし、とりあえず気にしない*1。

それから、弟の thinkpad は IBM Access Connections でネットワーク周りを管理しているせいか、「ネットワーク接続」の「ワイヤレスネットワーク接続」のプロパティに「ワイヤレスネットワーク」のタブがなくて、設定に少し困ってしまった。

これであと必要なのはDSとマリオカート(違

λ. USBから電源供給可能なスイッチングハブ

メモ。

• IO-DATA ETX-SH5Sシリーズ
• ELECOM LD-CSW05Nシリーズ
• Planex FX-08Mini

λ. Packrat Parsing: Simple, Powerful, Lazy, Linear Time. Bryan Ford

ナイーブなパーサコンビネータライブラリーでパーサを書くと、入力文字列に対して最悪指数オーダだが、メモ化(memoization)*1によってリニアなオーダになる。非正格関数型言語の性質を利用してそのメモ化を行うのがPackratパーサ。

ちょっと面白いと思ったのは、一般的なアルゴリズムでパーサを書く場合にレキサとパーサを分ける理由。一般的なアルゴリズムでは、トークン単位でしか先読みできず、より大きな単位での先読みが出来ないために、先読みで必要なだけの情報をレキサがトークンにまとめておかなくてはならないから、というもの。ちなみに、Packratパーサは入力文字列のSuffixに対するパース結果を自由に先読み出来るので、レキサをパーサから分離する必要はない。

λ. Proof Methods for Corecursive Programs. Jeremy Gibbons, Graham Huttton.

recursiveなプログラムは定義域がinductiveなデータ型であるようなプログラム、corecursiveなプログラムは値域がcoinductiveなデータ型であるようなプログラム。そして、corecursiveなプログラムについての証明の基本は、二つのプログラムが等しいことの証明。この論文では The map-iterate property (map f . iterate f = iterate f . f) の証明を例として、以下の4つの方法を説明し比較している。

• fixpoint induction
• the approximation (or take) lemma
• coinduction
• fusion

ほとんど知ってることしか書いてなかったので、個人的にはあまり面白くなかった。 guarded coinduction (と guarded corecursion) について知りたかったんだけどなぁ。

λ. 今日の夢

既に地球が存在せず、火星も人類には適さない環境になりつつある、そんな未来の夢を見た。人類は木星の衛星エウロパの海底都市に細々と生き残っていたのだけど、もはや人類にかつてのような力はなく、既に存在しない地球に対して望郷の念を抱きながら、ゆっくりと文明は衰退していく。宇宙開発が無限の夢をもって語られた時代は過ぎ去り、限界ばかりが意識される。哀愁。

λ. Guarded Induction on Final Coalgebras. Duško Pavlović

guarded (co)induction に対して圏論的なモデルを構成しているのだが……結構複雑だな。もっとシンプルなものを期待していたので驚いた。これはこれで興味深いけど、とりあえず深入りしないことにしよう。

それと、興味深く思ったのは、以下のような視点というか考え方。

In fact, the most interesting conceptual distinctions often begin to surface only when the symmetry starts breaking down. Going back to monads and comonads, recall, e.g., how the free algebras for a monad form an algebra classifier (the clone), whereas the cofree coalgebras for a comonad do not seem to either classify or “coclassify” anything meaningful. And indeed, the former turns out to be the foundation of a rich mathematical theory, capturing algebraic varieties by functorial semantics, whereas the latter remains a symptom of the fundamental fact that this theory does not have a dual: coalgebras for comonads on toposes tend to form toposes again, rather than “covarieties”.

私も含めて圏論ユーザは双対性を圏論を強力な武器と認識していて、双対性が利いてくるような状況には興味を示すけど、双対性が役に立たないような状況には比較的興味を示さないことが多いです。でも、そういう状況でこそ見えてくる興味深い点というのもあるんだなぁ。反省、反省。

• <URL:http://www.kestrel.edu/home/people/pavlovic/coalgebra.html>
• <URL:http://dx.doi.org/10.1016/S1571-0661(04)00056-8>
• citeseer:pavlovic98guarded.html

分からなかった点など

• p.3 で　tree induction, stream induction, labelled tree induction と呼んでいるのは何を指している?　inductionという言葉をどういう意味で使っているのか正確な定義が知りたい。
• p.7 の F=P_Σ のときの、prefixing operations が変な気がする。Σの部分集合の個数だけあるのでは?
• p.6 の 「But !: γ is surely an epi, because it is split by fix (be it unique or not). So ∂ induces a unique prefix η1, and η1 induces a unix fixpoint fix.」という部分が良く分からない。epiだと何故uniqueに?

λ. 正方形と正三角形のクイズ

先日に続いて、質問に即答できず悔しい思いをした問題がまたあったので、ここに書いてみる。

問題

正方形と正三角形を貼り合わせた以下のような図形の角xを求めよ。

参考

• 正方形と正三角形のクイズの図を描く (sumimさん)

λ. 全国一斉！日本語テスト

soutaroさんのmixi日記(2005-01-15) より。

私は72点でした。 間違えたのは1,5,7,12,23,24,25,27の8問で、手紙の問題が難しかったです。 「時には手紙を書いてみよう」という寸評をもらってしまいました。

周りの人の結果

• chiko
• suzuvaki
• takot
• 小熊さん

λ. 情報教育論

KJ法

λ. 怡口蓮(Choclairs)

中国のお土産にもらった。

λ. 複雑系とゲーム理論

NHKの「世紀の頭脳対決 - チェス対決徹底分析」のビデオを見た。

λ. ゴールを明確に

ゴールを明確に
でないとサーベイが出来ない
by chiko

λ. ライブドアショック

たまたまキャッシュポジションを増やしていたのでラッキーだった。 下落で損もしたけど、以前から購入したかった銘柄が比較的手頃な価格で買えたし、今のところトータルではそう悪くない感じ。 明日以降どうなるか知らないけどさ……

ネタ色々

• 堀江の拳
• <URL:http://slashdot.jp/~astro/journal/339329>
• <URL:http://www.shota.tv/EVA3.swf>

マネックス証券批判について (2005-01-20 追記)

いきなり掛目をゼロにしたのは性急過ぎたというのはあるとは思いますが、掛目を引き下げたこと自体は当然だと思うし、ちょっと批判されすぎという気がします。

ヤバイことになった企業の株なり何なりの担保としての評価を下げ、契約に基づいて担保の追加なりを求めるのは当然であり、普通の金融機関ではどこでもやっていることです。お金を貸す以上そういったことは当然でしょう。 ましてや、代用有価証券は「代用」というくらいで、所詮は委託保証金の代用に過ぎないんですよね？　マネックス証券の言い分の「特定の株式の担保評価が困難になった場合、担保価値を下げることは経営の選択肢の1つ」というのは全くもってその通りだと思う。

今回の掛目の引き下げで追証に追われマネックス証券を批判している人は、自分が借金をして株を買っているということにあまりに無自覚だったのではないでしょうか。レバレッジのかかったハイリスクな取引を行い、これまで利益を追求してきながら、いざ失敗したら他者に責任を転嫁しようとする。自業自得でしょう。

λ. 『59番目のプロポーズ』, 長原 万里子

なんか知らないけど研究室においてあったので読んでみた。

λ. インターネット構成法 最終試験

予想していたより難しかった。問題は以下の通り。

問題1

MACアドレスの特徴とその役割を100字以内で説明しなさい。

問題2

Spannning Tree Protocol (STP) を100字以内で説明しなさい。

問題3

Port VLAN を100字以内で説明しなさい。

問題4

Autonomous System (AS) を100字以内で説明しなさい。

問題5

Interior Gateway Protocol (IGP) と Exterior Gateway Protocol (EGP) に おける経路制御プロトコルを1つづつ挙げなさい。

問題6

マルチキャストの経路制御プロトコルを1つ挙げなさい。

問題7

IPアドレスのマスクについて、経路制御の観点から100字以内で説明しなさい。

問題8

経路表の構成要素を2つ挙げなさい。

問題9

デフォルトルートを100字以内で説明しなさい。

問題10

光ファイバを用いたネットワークにおける帯域を示す単位として、OC(Optical Carrier level)が用いられる。OC12は622Mbpsを示し、OC48は2.5Gbpsを示す。このとき、OC768が示す帯域を答えなさい。

問題11

建物内の同一フロアなど、限られた空間に複数の無線LAN基地局を設置する場合、どのような点に注意すべきかを説明しなさい。(字数制限なし)

問題12

静的経路制御と動的経路制御の違いを、それぞれの特徴を具体的に説明しながら説明しなさい。(字数制限なし)

問題13

二つの隣接するサブネットA(192.168.1.0/24)とサブネットB(192.168.2.0/24)の2本の回線によって接続性を冗長化し、現用系の接続性が失われた際に予備系に切り替わるよう工夫したい。このとき、二つのサブネットを接続する機器(ルータやスイッチ)や回線をどのように接続するか図示しなさい。また、そのネットワーク構成をとるのに必要な通信技術またはプロトコルが図中のどの機器で動作すべきか、必要であればその設定を含めて説明しなさい。(字数制限なし)

λ. 『マッチ箱の脳(AI)―使える人工知能のお話』, 森川 幸人

結構面白かった。 これは学部一年の時に読んでいたかったな。

λ. 第十三回圏論勉強会

今日は圏論勉強会。今回は田町の男女共同参画センターという場所だった。

写真

昼飯

昼飯の時に駅の反対側に行って何か見たことのある風景だなと思ったら、慶應の三田キャンパスがあるのが田町だった。気づかなかった……

Session 24 の Exercise 3 (p.268)

力学系(dynamic system) X^↻α と Y^↻β の表現(presentation)から力学系 X^↻α×Y^↻β の表現を求める方法を考える問題で苦戦してしまった。X^↻α の表現における生成元の集合をG_X、関係(等式の集合)をR_Xとすると、以下のようにすれば一応表現は得られると思うが、これだと生成元の定義が嫌な感じ。

生成元の集合

{ (x,y) | x∈X, y∈Y, x∈G_X∨y∈G_Y }

等式の集合

{ γ^min(m,i)(α^m-min(m,i)a,β^i-min(m,i)c) = γ^min(n,j)(α^n-min(n,j)b,β^n-min(n,j)d) | (α^ma = αⁿb)∈R_X, (a,b∈G_X), (βⁱc = β^jd)∈(R_Y∪R_Y^-1), (c,d∈G_Y)}
(ただしR_Y^-1はR_Yの等式の両辺を入れ替えたもの。)

図 (2006-02-01 追記)

X^↻α

Y^↻β

X^↻α×Y^↻β

λ. 初雪 (2)

一夜明けてこんな感じ。

λ. 初雪 (3)

まだ学校には雪が結構残っていた。

λ. 複雑性とゲーム理論　期末試験

ボロボロだった。単位がくるといいなぁ……

複雑性とゲーム理論　期末試験問題

問1

テニスのレシーバーのレシーブ成功確率が、下表のように与えられているものとする。このとき、サーバーとレシーバーの最善の混合戦略を計算せよ。

+--------------------------------------+--------------+--------------+
| レシーバー側の動き＼サービス側の狙い | フォアハンド | バックハンド |
+--------------------------------------+--------------+--------------+
| フォアハンド                         |     90%      |     10%      |
+--------------------------------------+--------------+--------------+
| バックハンド                         |     30%      |     50%      |
+--------------------------------------+--------------+--------------+

問2

ある財に対する市場需要曲線が p = -d + 100 で与えられているとする。また、複占企業A社、B社の限界費用は共に10で一定であるとする。この時、製品差別化が存在しない状況の下で、クールノー(Cournot)解を求めよ。

問3

以下の2つのタカ・ハトゲームにおける進化的安定戦略(ESS)を求めよ。

（1）

+--+----+----+
|  |  H |  D |
+--+----+----+
|  |   3|   0|
|H |3   |10  |
+--+----+----+
|  |  10|   5|
|D |0   |5   |
+--+----+----+

（2）

+--+----+----+
|  |  H |  D |
+--+----+----+
|  |  -3|   0|
|H |-3  |10  |
+--+----+----+
|  |  10|   5|
|D |0   |5   |
+--+----+----+

問4

ある企業には4人の株主A,B,C,Dがいて、持ち株数の比率を反映して議決権が 4 : 3 : 3 : 1 の割合で各人に割り当てられているものとする。この時、株主総会において各種の議決が単純多数決で行われる場合、各人のシャプレイ・シュビック(Shapley-Shubik)指数を計算せよ。

λ. Infinite Objects in Type Theory. Thierry Coquand.

を読んだ。 guarded induction についての多分最初の論文。

どうでも良いけど、表記が少し珍しい気がする。 普通「f : (N -> P) -> P」と書くところを「f : ((N)P)P」と書き、「λx.u」と書くところを「[x]u」と書いている。

【2007-09-11追記】 「[x]u」は「自由変数としてxを含む項u」という意味だろうし、「((N)P)P」についても同様だろう。 なので、上記部分は私の勘違いだろうと思う。

Quotation

In order to establish that a proposition φ follows from other propositions φ₁,...,φ_q, it is enough to build a proof term e for it, using not only natural deduction, case analysis, and already proven lemmas, but also using the proposition we want to prove recursively, provided such a recursive call is guarded by introduction rules. We call this proof principle the “guarded induction principle”.

sec. 2.8 より。 Guarded Induction on Final Coalgebras で引用されていたのと同じところを引用するのは、ちょっと癪だけど。

分からなかった点など

impredicative proof of Tarski's fixed point theorem.

Tarskiの不動点定理について良く知らないことに気づいた。どの辺りがimpredicativeなんだろう... <URL:http://www.hss.caltech.edu/~fede/wp/pf-tarski4.pdf> とかは関係ある?

strong positivity

P.Dybjer. Inductive Families. を参照。

λ. 『国家の罠―外務省のラスプーチンと呼ばれて』, 佐藤優

読了。これはすごい本である。 感想は後でちゃんと書きたい。

λ. RDスタイルでプラグイン引数がエスケープされる問題へのパッチ

• rd_style_unescape.rb.patch

プラグイン呼び出しの引数がエスケープされてプラグインに渡されてしまうのを避けるためのパッチ。 [tDiary-devel] RDスタイルでプラグインの引数がエスケープされてしまう で報告、2006-09-13に取り込まれた。

λ. Haskell is not not ML. Ben Rudiak-Gould, Alan Mycroft, and Simon Peyton Jones.

<URL:http://lambda-the-ultimate.org/node/1248> より。

継続が否定の計算的解釈というのはもちろん知ってはいたけど、二重否定がliftingに対応するということには気づいてなかったし、call-by-name CPS translation と call-by-value CPS translation についても知らなかった。知らないことばかりで勉強になった。それにしても、こういう理論的な話と実装寄りの低レベルな話とがうまく結びついているのは好きだな。

IL は paraconsitent だという話があったが、paraconsistent logic というものがあるようだ。

• <URL:http://plato.stanford.edu/entries/logic-paraconsistent/>
• <URL:http://en.wikipedia.org/wiki/Paraconsistent_logic>

λ. RDスタイルへのパッチ

rd_style_textblock.rb.patch

メソッドリストを使ってブロック要素を書く際に、中身が一段落しかない場合でもp要素にする。

後でtDiary-develに送る。

λ. デジカメ用液晶保護フィルム & 携帯ストラップ

湘南台のデンソーダイソーでデジタルカメラ用液晶保護フィルムの1.5インチのやつと、あと携帯のストラップを買ってきた。液晶保護フィルムは ipod nano の液晶に貼ろうと思って買ったのだけど、ピッタリだった。 nano専用の保護フィルム(e.g. SANWA SUPPLY 液晶保護フィルム(iPod nano専用) PDA-FIPK7)だと数百円くらいすると思うのでお薦め。

λ. CiteULike: A free online service to organise your academic papers

学術論文に特化したソーシャルブックマークサービスか。 ちょっと面白そう。 とりあえずアカウント取ってみた。 <URL:http://jp.citeulike.org/user/msakai>

CiteULikeは、読んでいる学術論文の情報をシェア・保存・整理することのできる、研究者のための無料サービスです. おもしろそうな論文をウェブ上で見つけたら、ボタンをクリックするだけであなたの個人ライブラリに追加することができます. CiteULikeが自動的に書誌情報を取得しますから、一つ一つ入力する必要もありません. また、全部ウェブブラウザー上で済ませられます. 専用のソフトウェアをインストールする必要はありません.

あなたの個人ライブラリはすべてCiteULikeのサーバーに保存されますから、どこからでもアクセス可能です. また、ほかの人と自分のライブラリをシェアしたり、同じ論文を読んでいる人を探すこともできます. さらには、自分の研究分野の中でそれまで知らなかった文献に出会う可能性もあります.