日々の流転

λ. 文系・理系・体育会系の決定的な差

笑った。

λ. MaudeでCPL

CPLは、データ型定義から導出された書き換え規則を使って、項書き換えによって計算を行う。したがって、導出された書き換え規則をMaudeで定義してやれば、Maudeを使って計算が行えるはず。

というわけで、簡単な full evaluation の方でやってみる。 cpl.maude

厳密に再現するには、frozen属性を使って書き換えが起こる場所を限定してやる必要があり、そうすれば速度も上がるとは思うが、それはまだやっていない。

λ. 満員電車

夏休みが終わったからか知らないけど、電車が超混んでる。 疲れた。

λ. 『寄生獣 (1)』 by 岩明 均

を読んだ。

λ. 帰りの電車で寝過ごした

.

λ. True≠False の証明

ペアノの公理における 0≠s(x) のように、一般に異なるコンストラクタによって得られる値は異なるべきはず。 なので、最も単純な True≠False の場合について証明しようとしてみたのだが、簡単に証明できるかと思いきや large elimination が必要になってしまった。うーん……

data Taut = tt
data Absurd =

Not :: Set -> Set
Not X = X -> Absurd

idata Id (|X::Set) :: X -> X -> Set where
    refId (!x::X) :: Id x x

substId (X::Set) (!P::X->Set) (x,y::X) :: Id x y -> P x -> P y
substId id p = case id of (refId z)-> p

disjointness :: Not (Id True False)
disjointness id =
    let T :: Bool -> Set
        T b = case b of
                (False)-> Absurd
                (True )-> Taut
    in substId T id tt

λ. 「カッセ」

「カッセ」というのは何かと思っていたら、「かっ飛ばせ」の略だそうだ。 知らなかった。

λ. 『寄生獣 (2)』 by 岩明 均

を読んだ。

λ. 帰りの電車で今日も寝過ごした

.

λ. Constructing M-types from W-types

Containers: constructing strictly positive types の話。

先日、「W-typesによる帰納的データ型の表現」で書いたように、W-typesは整礎(wellfounded)な木のデータ型になっている。 そして、Wa:A. B(a) は関手 T(X) = Σa:A. B(a)→X の最小不動点になっている。 最小不動点があれば当然最大不動点も考えたくなるもので、それがM-types。 Ma:A. B(a) は T の最大不動点で、整礎とは限らない木のデータ型になっている。 ちなみに、名前はM-typesはW-typesの双対だから「W」を上下反転した「M」を使ったのだろうと思う*1。

で、M-typesはW-typesとは別に追加しなくてはいけないかと思ったら、実はMartin-Löf圏ではW-typesから構成することが出来るそうだ。 無限木を深さnで切ってそこをダミーの値に置き換えると有限の木になり、逆にnを大きくしていった時のそのような有限の木の極限が元の無限木と考えることが出来る。なので、元の無限木を直接扱う代わりに、そのような有限の木の族として扱う。有限の木はW-typesで表現出来るので、M-typesはW-typesで表現できると。

イデアル完備化との関係?

こういう話を聞いて連想するのは、Jiří Adámek の Final Coalgebras are Ideal Completions of Initial Algebras で……

後で書く。

Agdaによる実装

M-types.agda (作業中)

後で書く。

λ. 台風が来る

台風が来るそうなので早く帰る。

ところで、子供っぽいとは思うのだが、台風とか荒れ空とかは好き。吹き荒ぶ風雨は閉塞感を吹き飛ばしてくれそうで、そしてまだ見ぬ何かを運んできてくれそうで、ワクワクする。逆に雲一つ無い空というのは非常に気が滅入る。風よ吹け〜　雨よ降れ〜

λ. SLACS2007のプログラム

が出ていた。気になる発表が幾つかあるなぁ。 向井先生も例のPrologの話で発表するのね。

λ. 台風

通勤中、多摩川の増水のため戸塚で東海道線が止まってしまって困った。 適当に他の経路で通勤したが、電車も駅も無茶苦茶混んでいて、朝から疲れた。

何も考えずに会社に行ってしまったが、台風で某予定は無くなっていたので、午前半休を取ってしまっても良かったな。 あるいは、会社休んでIPA未踏ソフトウェア創造事業2006年度下期千葉PM採択プロジェクト最終成果報告会の方に行くという手もあったなぁ。 ちと勿体無いことをしたかも。

λ. 黒光りの嫌われ者：ゴキブリの秘密

• ニコニコ動画(RC)‐黒光りの嫌われ者：ゴキブリの秘密 1/2
• ニコニコ動画(RC)‐黒光りの嫌われ者：ゴキブリの秘密 2/2

K5の雑記帖 より。 興味深い。

λ. HDDの調子悪い

2年前(20050829#p03)に購入したハードディスクの調子が悪い。 チェックディスクに書けたら凄い時間がかかった(そのせいで圏論勉強会に出れなかった)。 バッドセクタはあったが、ファイルは壊れていないようなのがせめてもの救いか。 「まだ2年間しか使ってないのに」と思わないでもないが、まあ仕方が無い。 近いうちに新しいHDDを買わないとなぁ。はぁ…。

【2007-09-12追記】 今使っているのはSeagateのだったので、今度はHGSTのにしてみよう。 250GBでも使いきるには程遠かったので、現在主流(?)の500GBのではなく320GBのHDT725032VLAT80を注文してみた。送料込みで約8000円。 HDDは消耗品なので、当面困らない容量で安いものを買えば十分。

λ. 第三十三回圏論勉強会

今回は残念ながら出席できず。 でも写真はいつものようにミラー。

λ. Amazonポイント最大3%(3倍)還元キャンペーン

というのをAmazon.co.jpがやっているそうな。気になっている和書はこの機会に買ってしまおうかな。ちなみに、コミックは対象外と書いてあるけど、Horror & SF - coco's bloblog の漫画を書籍化した『今日の早川さん』は対象内だった(ので早速注文)。

しかし、Amazonカードのポイント2%と合わせても、たったの5%にしかならないんだよなぁ。学生時代は12.7%引きで買えた*1のに……学生時代が少し懐かしいよ。

λ. 『福翁自伝』 福沢諭吉 著　富田正文 校注

入学時に配布されていた『福翁自伝』を今頃になって読んだ。 在学中は自分の学校の歴史等についてあまり興味も無かったのだけど、卒業して何だか色々と知りたいと思うようになった。 何故かは良くわからないが、頭腐の宮本賢治さんの影響というのも少しあるのかと思う。 でも、何だか「海外に行って日本を知りたくなる」といったよくあるパターンのようでアレではあるが。

しかし、福沢諭吉はもっと真面目腐った人かと思っていたら、なかなか愉快な事をやってるじゃないか。 ここ数日は通勤中にずっと読みふけっていた。

• Digital Gallery of Rare Books & Spacial Collections ＜ 福澤著作コレクション 福翁自傳 ＞
• 福翁自伝 - Wikipedia

λ. 『ヘウレーカ』 by 岩明 均

を読んだ。 寄生獣の人の短編。

• ヘウレーカ - Wikipedia

λ. HDD移行

先日、HDDの調子悪いと書いたが、注文したHDDが届いたので早速移行作業開始。 例によって、RIP(Recovery is Possible) のCDで起動。 2004/01/22 三田(2) 「ディスクが BIOS から認識しなくても諦めるな！」を参考に、念のためhdparmでdmaを無効にして、それから「dd if=/dev/hdb of=/dev/hda ibs=512 obs=10MB count=488392065 conv=sync,noerror」等としてコピー。

I/Oエラーが起こったのは一部領域の100KB程度のみで割と問題なくコピーが終わった。16時間くらいかかって、終わったのは15日の昼過ぎだったが。その後、起動出来る事を確認し、チェックディスクをかける。幾つかエラーが発見されるがファイル自体には特に問題ないようだ。 よかったよかった。

しかし、こういう作業をするときは緊張するな。

λ. RD+スタイルでプラグイン引数がエスケープされる

以前、tDiaryのRDスタイルに同様の問題を発見したときに、hikiにも同様の問題がないか疑うべきだった。不覚。

【2008-06-08 追記】 Hiki Issue Tracking System - Ticket-96 に登録。

【2008-07-06 追記】 [Hiki-dev:01199] で CVS HEAD に取り込んで貰えた。

λ. 100円ショップで買った携帯のストラップ

2006-01-29にダイソーで買ったストラップが壊れたので、新しいのを今度はキャンドゥーで買ってみた。 だけど、前のと比べて無駄にかさばって邪魔な感じ。

λ. 100円ショップで購入した「ハンディークリップピン」

普通にガチャダマ(中)を買うと50個500円だけど、これは30個100円でだいぶお得。

λ. 100円ショップで購入した「A4クリヤーホルダー　カラー5枚入り」

3色フォルダを試してみようと思って買ってみた。 本には数百円と書かれていたが、フォルダだけなら100円。

λ. ヘンキン文

先日、「H↔Provable([H]) な H の真偽」というクイズを書いた。 反応が全く無くて少し寂しかったのだけど、忘れないうちに簡単な解説を。

この論理式はヘンキン文(Henkin sentence)と呼ばれていて、その名の通り1950年頃にヘンキンによってその真偽が問題にされたそうだ。 そして、この論理式が真であることは Löb によって1955年に示されている。 以下に簡単に証明するが、なかなかトリッキーで面白い。

• Löb, M. H. 1955. Solution of a problem of Leon Henkin. Journal of Symbolic Logic, vol. 20, pp. 115-18.

前提

証明可能性は可導性条件(derivability conditions)と呼ばれる以下の条件を満たす。

D1

T ⊢ P ⇒ T ⊢ Provable([P])

D2

T ⊢ Provable([P→Q]) → Provable([P]) → Provable([Q])

D3

T ⊢ Provable([P]) → Provable([Provable([P])])

また、不動点定理が成り立つ。すなわち、任意の一変数論理式 P(x) に対して、ある論理式Qが存在して T ⊢ Q↔P([Q]) が成り立つ。

証明

H は T ⊢ H↔Provable([H]) を満たすとする。

まず、不動点定理によって、ある論理式Dが存在して T ⊢ D ↔ (Provable([D])→H) を満たす。

S := Provable([D])→H とすると T ⊢ D → S

D1を適用して T ⊢ Provable([D → S])

D2を適用して T ⊢ Provable([D]) → Provable([S])

Sを展開してもう一回D2を適用して T ⊢ Provable([D]) → Provable([Provable([D])]) → Provable([H])

D3より T ⊢ Provable([D])→Provable([Provable([D])]) なので、T ⊢ Provable([D]) → Provable([H])

Hの定義より T ⊢ H↔Provable([H]) なので、T ⊢ Provable([D]) → H

Dの定義より T ⊢ D ↔ (Provable([D])→H) なので T ⊢ D で、D1 より T ⊢ Provable([D])

T ⊢ Provable([D]) と T ⊢ Provable([D]) → H とにMPを適用して T ⊢ H

様相論理との関係

Provable([X]) を □X と書くことにすると、D1は必然化に、D2はKに、D3は4に対応する。 さらに不動点定理に対応するものを様相論理で公理化して……という話があるがそれはまたそのうち。

λ. かつ泉の宝山豚ロースかつ定食(中)

美味しかった。

λ. Agda Implementors' Meeting 6

Codata や Observational Equality など、Agdaの型理論に欠けていると私が思っていたものについても、きちんと議論はされているのね。ちょっと安心した。

あと、Agataが GHC 6.6 で動かないのは、GHC 6.6 の Forall-Hoisting にバグがあるかららしい。へぇ。

λ. 矛盾を表す型

<URL:http://d.hatena.ne.jp/sumii/20070912/p1> から、<URL:http://shuns.sakura.ne.jp/?%BD%B5%B5%AD> の話。そういや、OCamlの let rec はそんなことが出来るのだった*1。

それはさておき、「type void = V of void」はこのような問題はあれど、除去規則については「let rec f x = match x with V x -> f x ;;」という形で一応は帰納的に定義できる。それに対して「type void」はこのような問題はないけど、自然な除去規則「let f x = match x with ;;」が構文エラーになってしまって*2イマイチ。

また、多相ラムダ計算の表現力を持つ言語では、矛盾を「∀X. X」で表現することも出来る*3。先日の「パースの論理式」 では矛盾の表現としてこれを使ってみた。 この場合の除去規則については自明。

λ. 『寄生獣 (3)』 by 岩明 均

「ったく薄情なヤツだな」「…………情なんてないよ」という掛け合いが良かった。

λ. SLACS 2007 (1日目)

一日目。

λ. 佐藤圭祐（東工大）：λ記号の加わった様相論理に関する研究

2002年にMelvin Fittingが提唱した「λ記号の加わった様相述語論理」に対し，ツリー・シークエントによる証明体系を与え，体系Kにλ記号の加わったKλおよび，さらにいくつかの公理型が加わった諸体系について，その健全性と完全性を示す。

Melvin Fitting が提唱した「λ記号の加わった様相述語論理」というのは、Modal Logics Between Propositional and First Order か。

λ. 小島健介（京大）：next, always をもつ直観主義線形時相論理

多段階計算のための型システム λ^○□ (Yuse and Igarashi, 2006) に Curry-Howard 同型対応する論理についての考察を行う。この論理は，next と always の二つの時相演算子をもつ直観主義線形時相論理とみることができる。本発表では，その sequent calculus による定式化と Kripke semantics を与え，完全性について考察する。

λ. 田中覚次（九大）：関係代数の拡張体系の表現定理について

A.Tarski　によって考えられた二項関係を表現する代数的構造を，拡張しそこでの表現可能性について検討する。ストーンの表現定理の拡張について主に述べるが，二項関係の全体への表現へ拡張できればそれについても触れる予定である。

λ. 根元多佳子（東北大）：Infinite games from a intuitionistic point of view

無限ゲームの決定性の直感主義数学における取扱いと，2^ω×{0,1}上の長さ 2 のゲームの決定性について。

λ. 小林聡（京産大）：極限計算可能数学のためのゲーム意味論と変換意味論

極限計算可能数学(Limit Computable Mathematics, LCM)とは，おおよそ構成的数学に非常に弱い形の排中律をつけ加えたものとして与えられる体系である。本研究では，LCM の証明からアルゴリズムを抽出するための2つのアプローチを示す。1つは，1-backtrack と呼ばれる弱いバックトラック規則を持つゲーム意味論である。2つめは，Friedman 変換に類似した新しい変換による意味論である。古典的証明の研究では二重否定変換やその変種が用いられることが多いが，我々の変換はゲーム意味論にヒントを得たもので，二重否定変換とは異なる発想に基づく全く新しいものである。

λ. バケツプリン

一度挑戦してみたいものだが、写真を見ているだけで胸焼けしそう……

λ. SLACS 2007 (2日目)

二日目。

飲み会の時に、夏のプログラミングシンポジウムでの浜地さんの発表資料「Code Golf について」が少し話題になった。

SLACS 2007 への言及

• ぴらぴら週記 » SLACS 2007

λ. 菊池健太郎（東北大）：ベータ簡約を模倣するカット除去手続き

シーケント計算LJの中で型付きラムダ項全体と同型になる部分を特定し，ベータ簡約があるカット除去手続きによって健全かつ完全に模倣されることを説明する。

λ. 和手正道（了徳寺大）：直観主義論理の証明可能性の決定時間について

Gentzen流直観主義論理において与えられたsequentが証明可能か否かの判定は可能であることは明らかであるが,その判定に要する時間がsequentの長さの関数としてどの程度の時間があれば十分かを論ずる.

λ. 坂川航（東工大）：一般化された体系におけるcut除去定理の成立条件

論理記号や推論規則が一般化されたシークエント計算の体系において，cut除去定理が本質的に成り立つための必要十分条件が2006年に Ciabattoni, 照井によって与えられた。そこでは統語論的，意味論的な条件が別々に与えられ，それらの等価性も示された。本発表では特にその統語論的な条件に着目し，体系の定義をさらに一般化させた時にどのような問題が発生するかを指摘し，その解決策を述べる。

λ. 向井国昭（慶応大）：PrologへのMontague普遍文法に基づくeval述語の導入

講義資料作りのために日常的に使う主なソフト/言語は, Emacs, pTeX，HTML/JavaScript/Ajax, およびPrologである。とくにProlog(SWI-Prolog)は全体を束ねる中心的な言語として使用している。計算言語理論，数式処理，定理証明，オートマトン理論，Prologプログラミングなど，担当授業の性格上どれも，複雑な式変形を伴う計算量の多い教材作りが必要である。このためだけでもPrologは必須の道具であるが，それだけにとどまらない。Emacs バッファのLaTeX テキストの編集とコンパイル実行もPrologとEmacs-lispの間の通信により，Prologの述語として定義・制御できるようにした。つまり， Prologの限定節によりEmacs-バッファ上のテキスト編集機能を記述する。

発表では，関数型評価述語 eval，項書き換え述語 reduce 充足可能述語 models, そして，簡易版のラムダ計算 beta_liteの４つの述語を中心に紹介する。いずれの述語も問題が決まればそれに応じて個別に書けるものであるが，問題に共通するパターンを抽象化して，汎用の規則解釈述語とした。個別の問題はいわゆるソートあるいはクラスとして一定の形の規則で与える。

関数型言語としてのProlog限定節の解釈, モンタギュ普遍文法とその上の翻訳理論からのevalの解釈（発表タイトル），等式論理規則(paramodulation) の解釈器としてreduce述語の説明, など，上述の規則に明快な意味論的解釈および根拠を持たせた。　発表ではこれらの結果を，いちおうのまとまりをみせてきた現状のシステムのデモを交えて説明する。

λ. 木村大輔（NII）：Duality between Call-by-value and Call-by-name, Extended

We extend Wadler's work that showed duality between call-by-value and call-by-name by giving mutual translations between the λμ-calculus and the dual calculus. We extend the λμ-calculus and the dual calculus through two stages. We first add a fixed-point operator and an iteration operator to the call-by-name and call-by-value systems respectively. Secondly, we add recursive types, ⊤, and ⊥ types to these systems. The extended duality between call-by-name with recursion and call-by-value with iteration has been suggested by Kakutani. He followed Selinger's category-theoretic approach. We completely follow Wadler's syntactic approach. We give mutual translations between our extended λμ-calculus and dual calculus by extending Wadler's translations, and also show that our translations form an equational correspondence, which was defined by Sabry and Felleisen. By composing our translations with duality on the dual calculus, we obtain a duality on our extended λμ-calculus. Wadler's duality on the λμ-calculus was an involution, and our duality on our extended λμ-calculus is also an involution.

急病のためにキャンセル

λ. Matthew de Brecht（京大）, 小林正典（首都大）, 徳永浩雄（首都大）, 山本章博（京大）：多項式環におけるイデアルの正データからの帰納推論

多項式環のイデアルが有限基底を持つという性質が，機械学習理論の一つである正データからの帰納推論と密接に関係しているという事実は論理の視点からも注目されている。本講では，正データからの帰納推論からみた多項式環におけるイデアルの性質，さらには，その一般化を普遍代数における閉包演算を用いて行う方法について，発表者のグループが最近数年間で明らかにしてきた結果を報告する。

λ. Matthew de Brecht and Akihiro Yamamoto（京大）：Mind Change Complexity More Than ω^ω in Inductive Inference From Positive Data

In the context of machine learning, ordinal numbers are used for representing mind change complexity of classes of formal languages in inductive inference from positive data. The mind change complexity of a class means how often a learning machine is allowed to change its conjecture during the learning process. All previously investigated natural classes of languages (known to the authors) have had mind change bounds less than the ordinal ω^ω. In this talk, we will show that learning unbounded unions of a subclass of pattern languages requires ordinal mind change bound up to ω^ωω. We will also show a connection between proof theory and mind change complexity.

λ. hyさ〜ん

以前に、「Agdaの紹介Flash」というエントリに対するコメントで、hyさんという方に「Twelfでの証明行為」と「Coq-IDEでの証明行為」という動画を教えていただいたのですが、最近参照しようと思ったら消えていて残念でした。

これらの動画はこのまま見れなくなってしまうには非常に惜しい動画だと思います。 どなたか、hyさんの連絡先を知っている方や、これらの動画を保存している方はいらっしゃいませんでしょうか。もしいらっしゃいましたら、個人的に連絡を頂ければと思います。

λ. 先日交換したHDDを売却

先日交換したHDDをソフマップで売却。 不良セクタがあるのでジャンク扱いかと思っていたが、なんと満額の3,600円で売れた。 12,700円で購入したものだったので、2年で約9千円分償却したことになるか。

なお、HDDの使用期間や状態についての確認は一切無く、査定として検査を行っていた。一般に中古HDDは一定数以下の不良セクタは保証対象外として売られているようなので、それ以下の不良セクタしかなかったということかな。 ……後で気付いたのだけど、これって私には瑕疵担保責任は無いよね?

λ. 東方風神録を注文

「東方風神録」の店頭委託は9/21発売ということなので早速注文。ついでに、「うみねこのなく頃に」も一緒に注文してみた。

λ. 集合論を知らない子ども達

あまりも当たり前過ぎて21世紀に入ってから言葉にだしたことはあまりないのですが、当然のことながら、数学というのは、集合論を理解して初めて「出来る」と言うのです。 数学が出来る、という状態は「集合論が出来る」という状態の延長線上にあるべきで、集合論を理解していないということは数学を理解していない、つまり数学を理解していないのとほぼ同じだと思います。

最近は圏論とか呼ばれる、いわゆる抽象数学を用いる分野が増えてきていますが、それでも依然として、数学というのは集合論を使って構成されるもので、数学というものは全て集合論の延長上にあると思っています。 その意識がないと、たとえ公理や定理を書いていても、矛盾してしまったり、モデルがうまく作れなかったりしたときに「なぜだろう?」ということがピンとこないことになります。

まだ大学に入って無くて、圏論のような抽象数学を楽しんでいる若い人たちには、ぜひ集合論を勉強してみることを勧めます。 最近は素晴らしい時代になったもので、ごく初歩的な入門はその辺の教科書でもすることができます。 しかし本格的に集合論を遊びたくなったら、JechやKunenを使うのがお勧めです。 今の集合論は複雑になりすぎていて、初心者が全ての理論を知ろうとすると膨大な時間と労力がかかります。 しかし、最終的にはそれは全て知らなければならないことですし、知っておくべきことです。

最近は、全くの文化系の女の子が、わずか数ヶ月の研修で「ソフトウェア検証」と称して定理を書くような商売もあるらしいのですが、そんなときにもぜひ集合論を勉強してもらいたいと思います。集合論が解らないと、そもそも数学の構造やモデルの仕組みがわからないということなので、何が問題なのかわからないことの方が多くなると思います。

どれだけ数学が進化しても、その仕組みを理解していることは絶対に必要です。

筆算ができない人が電卓を使い続けたときに答えが正しいのか間違っているのかわからないのと同様、集合論ができない人が書いた公理系は、一見無矛盾なように見えたとしても、それは奇跡のようなバランス、自転車で言えば補助輪がついた状態で奇跡的に動いているに過ぎず、なにか未知の問題が発生したときに素早く公理系の内部でおきていることに直感を巡らせ、適切な処置・対応をするためには集合論の理解は不可欠と言って良いでしょう。

さらにいえば、集合論よりさらに下のレイヤーである、一階述語論理を理解しているとさらに理想的です。

昔、数学の本といえば集合論の本を意味しました。しかし、今の若い学生達は、下のような図をみても何を意味するか瞬時にわからないのではないでしょうか。

<URL:http://ja.wikipedia.org/wiki/%E3%83%99%E3%83%B3%E5%9B%B3>

数学的対象は全て集合の組み合わせでできています。 数学を構成する要素は全て集合論と一階述語論理なので、集合論を理解しないと数学の原理を理解していないことになります。 最低でも、ZFCで自然数と整数を作れる程度の理解はしておいて欲しいと思います。 集合論、一階述語論理の2つは、現在でもあらゆる数学の基礎になっているので、最低限おさえておきたいところです。

最後に参考文献をまとめておきます。 ただ読むだけでもとても面白い本ばかりです。

• Thomas J. Jech, Set Theory
• Kenneth Kunen, Set Theory: An Introduction to Independence Proofs
• Akihiro Kanamori, The Higher Infinite: Large Cardinals in Set Theory from Their Beginnings
• Keith J. Devlin, Constructibility

元ネタ

• マシン語を知らない子ども達 - Keep Crazy;shi3zの日記
• アルゴリズムを知らない子ども達 - val it: α → α = fun

λ. PPL Summer School 2007

第5回プログラミングおよびプログラミング言語サマースクール (PPL Summer School 2007) の講義資料を読んでいる。 やっぱり面白いそうだなぁ。 参加者の感想を聞きたいものだ。 zyxwvの日記(2007-09-20) を読んで、すえひろがりっっっ!のsuerさんあたりが書いてくれないかぁ、と思った(ボソッ

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

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

λ. 家計簿探し

社会人になってお金の出入りも増え、入出力をきちんと記録した方が良いと思うようになったので、何か良い家計簿ソフトはないかと探している。 とりあえず以下のような点に注目して探している*1けど、なかなか良いのはないね。

• Webベースか?
• メールで登録可能か?
• 複式か?

λ. foonance.com

最初に試したのがこのfoonance.comだけど、使い物にならない。 概念はシンプルそうで良いけど、色々とバグってるっぽい。

また、日本語をちゃんと使えない。Money Stores で Short name に日本語を使うと化けるうえに、transation を正常に追加できない。Description の方は平気。Category や Budget にも日本語は使えない(?)。Currency Symbol には円記号(YEN SIGN, U+00A5)を指定しても大丈夫だった(ただし、互換領域の FULLWIDTH YEN SIGN (U+FFE5) だと化けるっぽい)。

それから、一度作成した Money Store や Transaction は削除は出来ても編集出来ない。

λ. シンプル家計簿

特徴をみると魅力的なんだけど、登録の時にミスったようで重複した勘定項目が出来てしまい、削除しようとしたら例外が発生。 後でまた試す。

λ. GnuCache

Windows版をインストールしたが、gconfdがエラーで正しく起動しない。 これはWebベースではないけど、<URL:http://members.jcom.home.ne.jp/tanitsu/2006-10-21.html#2006-10-21-2> の記述を見る限り使いやすそうだったので残念。

λ. Wasabe.com

.

λ. Googleドキュメントで読めないCSV

某所からダウンロードしたCSVは、Excelでは読めたが、Googleドキュメントでは読めなかった。どうなってるんだと思ったら、日本語が含まれるフィールドが「="日本語"」のような感じでエスケープ(?)されていた。 RFC4180に従ってないような……　これってどのソフトの流儀なんだろう?

λ. 『寄生獣 (4)』 by 岩明 均

「あれ?　ミギー　おれのことなぐさめてくれたわけ?」 「…………そういうことになるかな?　ともかく食欲を出してもらわないとわたしも困る　必要なら　またなぐさめるネタを考えておく」 というやりとりが気に入った。

λ. [ruby-list:44057] Rubyを使った家電向けプラットフォームのデモ

へぇ。そんなものが。

λ. 誕生日

λ. UFJのスヌーピーEdyカードを解約

約2年前にスヌーピーEdyカードを作ったが、卒業した事により学生カードのメリット(年会費無料,海外旅行傷害保険,ショッピング保険)が無くなってしまうのと、あとAmazonカードを作ってからは使うこともほとんど無くなってしまっていたので、とうとう解約。 電話するのが面倒で伸ばし伸ばしにしていたが、解約は簡単だった。 カードはこちらで裁断してくれということなので、チョッキン。哀れ、スヌーピー真っ二つ。

ただ、ちょっと気になっているのは、まだ引き落とされていない支払いがちょっとだけ残っている点。 普通に考えると、期限の利益の喪失により一括で債務を返済することになると思うのだけど、どうなるのかしらん。

λ. 『寄生獣 (5)』 by 岩明 均

を読んだ。「ほんっっと情のかけらもない!!」「だからそうだってば」とか、もはやお約束のやり取り。

λ. 第 336 回 PTT 「仮想マシンを利用したプログラムの実行の監視とそのデバッガへの応用」

久しぶりにPTTに参加。 そして、初めて矢上に来た(慶應に6年もいて矢上に来るのが初めてというのもどうかと思うが)。

以下、簡単なメモ。

背景

伝統的なデバッガが共通して持つ機能は、ブレークポイント、ステップ実行、変数の値の調査等だが、これだけでは大規模で複雑なプログラムのデバッグには不十分。逆実行や、不具合に関係のある部分を抽出するスライシングの機能が必要。

仮想マシンの概観

• コード変換エンジン
  • 動的な instrumentation を用いながら個々のスレッドを実行する
• スレッドシステム
  • スレッドスケジューリングや Pthread API のエミュレートを行う
  • 実装は GNU Pth を基にした
  • GNU Pth はプリエンプションには対応していないが、 コード切り替えを起こすようなコードを dynamic instrumentation で埋め込むことで対応

コード変換

• 監視コードの挿入
  • デバッガ側の要求に従い、イベントに対応するハンドラを呼ぶ
    • イベント : デバッガの監視する挙動 (e.g. メモリの読み書き)
    • ハンドラ : C言語で記述された関数
• 分岐先の変更
  • 本来の分岐先に分岐せず、仮想マシンに制御を戻す

主な監視対象

• 基本的なもの
  • メモリの読み書き、レジスタの読み書き、分岐、関数の呼び出し、復帰、システムコール
• マルチスレッドに関連したもの
  • スレッドの作成・終了・コンテキストスイッチ・排他制御

実行の記録・再生

• 全く同じプログラムでも、実行するたびに結果が変わってしまうことがある(プログラムの実行の非決定性)
• デバッグを行う際に大きな問題となる
• ⇒ 仮想マシンに実行を記録・再生する機能を導入
  • 非決定性の要因となる振る舞いを記録・再生する (e.g. システムコール、シグナル、コンテキストスイッチ)

スライシング

• Dynamic Data Slicing
  • Forward Computation という手法を用いる
• Dynamic Data Slicing
  • 動的な依存関係を分析 (def-use chain)
• Forward Computatin
  • プログラムの実行と同時に、並行してスライスを計算する
  • backward computation に比較して消費するメモリ量が少ない

可逆実行

• ロギング方式[Chen01]と再実行方式[Boothe00]がある。
  • ロギング方式　実行時に状態履歴を保存し、後に復元
    • e.g. メモリ変更時に、変更前の内容を保存しておく
  • 再実行方式 : プログラムを先頭から再実行する
    • 適切な時点で停止させることにより、擬似的な逆実行を実現
• ロギング方式の特徴
  • 利点: 単距離の逆実行は比較的高速
  • 欠点: ログ取得のコストが大きい。マルチスレッドには対応しづらい (終了したスレッドを復元したりする必要)
• 再実行方式の特徴
  • 利点: 実装が比較的容易、ログ取得のコストもない
  • 欠点: 逆実行に時間がかかる場合がある
• 両方実装したが、スレッドを使う場合には再実行方式のみ。

追記

丁度、先日 Google Japan Blog: Debugging Backwards in Time - Google Tech Talk 紹介シリーズ ( 2 ) に逆実行出来るJavaデバッガの話が出ていた。

λ. 松下、web限定「Let'snote プレミアムエディション」は250GB HDD＆ターボメモリー搭載ジェットブラックモデル

これ欲しいなぁ。

λ. 『寄生獣 (6)』 by 岩明 均

を読んだ。

λ. 『寄生獣 (7)』 by 岩明 均

を読んだ。

λ. ベルビュー・クリーク ＠EUROPEAN BEER CAFE 新宿フリゴ

λ. 『寄生獣 (8)』 by 岩明 均

を読んだ。

λ. x < y と ∃z. S(x+z)=y

論理と計算のしくみ(萩谷 昌己/西崎 真也) の算術と不完全性定理の説明では、不等号 x < y をプリミティブな関係として扱っていたが、何故 ∃z. S(x+z)=y の省略形とはしなかったのだろうか?

【追記】 OCaml-Nagoya飲み会で話題になったので補足しておくと、x < y と ∃z. S(x+z)=y とが同値であることは証明可能(のはず)。

λ. ヨハネスブルグのガイドライン

「ヨハネスブルグのガイドライン」というのが面白いと聞いて、検索したら <URL:http://d.hatena.ne.jp/hagex/20050329> がひっかかった。 どこまで本当か知らないけど、ここでワールドカップやるのね。凄いなぁ。