日々の流転

λ. 買った本

『危険な話』

広瀬隆[著]

『東京に原発を』

広瀬隆[著]

関連(?)リンク

• 大東京計画

『詭弁論理学』

野崎昭弘[著]

λ. アッカーマン関数と高階原始帰納関数

アッカーマン関数は原始帰納的でないので計算できないと思っていたら、萩野先生に「アッカーマン関数は高階原始帰納関数なので、exponentialを使えば書ける」と言われてしまった。ガーン。

自然数上での primitive recursion の定義は知っているけど、自然数に限定しない意味での primitive recursion はどのように定義されるのだろう?

2002-07-12に原始帰納関数と末尾再帰について書いたけど、nobsunさんはきっと自然数以外に対するprimitive recursionも考えていたんだろうなぁと想像。

λ. YARV + Ruby/TCC

YARVの出力したバイトコードを、実行時にC言語に落としてRuby/TCCでコンパイルしてみる(そのためのパッチ)。でも、そしたらかえって遅くなってしまった (T_T)

青木さんの「これを使ってJITコンパイラ作れるかな」というツッコミを見てから、実行時にrb_eval()を部分計算してRuby/TCCでコンパイルというのをずっと考えてたのだけど、rb_eval()がでか過ぎてこれは挫折してたのでした。YARVはまだ小さいので簡単に試せて楽しかった。

λ. 読書

『進め！聖学電脳研究部』

平野 耕太 [著]

λ. First Steps in Modal Logic の Proposition 11.16

p.153 の Proposition 11.16 の証明はおかしい気がする。ψ∈Γ だとは言えないんじゃないだろうか。証明を直すとしたらこんな感じかな。

11.16 PROPOSITION

If the set of formulas Γ is essentially finite then the two relations |Γ|^▼ and |Γ^□| coincide.

Proof.

By Lemma 11.12 we know already that |Γ|^▼ ⊆ |Γ^□|. Thus it suffices to show the converse inclustion, assuming that Γ is essentially finite.

Let γ₁,...γ_n be the given spanning members of Γ. Consider any a∈A and b∈B with a |Γ^□| b (hence a |Γ^B□| b). Consider also any x≺_ia (for some label i). We must produce some y≺_ib with x |Γ| y.

Set ψ := ±γ₁∧...∧±γ_n where each ±γ_j is γ_j or ¬γ_j with the sign chosen so that x ⊩ ±γ_j.

Note that x ⊩ ψ , ψ∈Γ^B, [i]¬ψ∈Γ^B□.

Now x ⊩ ψ ⇒ a ⊩ <i>ψ ⇔ a ⊮ [i]¬ψ ⇔ b ⊮ [i]¬ψ ⇔ b ⊩ <i>ψ (a ⊮ [i]¬ψ ⇔ b ⊮ [i]¬ψ is verified using a |Γ^B□| b and [i]¬ψ∈Γ^B□). This gives some y≺_ib with y ⊩ ψ. It suffices to show that x |Γ|y. But for each φ∈Γ there is some γ with x ⊩ (φ↔γ), y ⊩ (φ↔γ) and hence x ⊩ φ ⇔ y ⊩ φ by the relationship of x and y to φ. ∎

λ. TrueCrypt

Free open-source disk encryption for Windows XP/2000/2003

Features:

• It can create a virtual encrypted disk within a file and mount it as a real disk.
• It can encrypt an entire hard disk partition or a device, such as USB memory stick, floppy disk, etc.
• Provides two levels of plausible deniability, in case an adversary forces you to reveal the password:
  1. Hidden volume
  2. No TrueCrypt volume can be identified (TrueCrypt volumes cannot be distinguished from random data).
• Encryption algorithms: AES-256, Blowfish (448-bit key), CAST5, Serpent (256-bit key), Triple DES, and Twofish (256-bit key). Supports cascading (e.g., AES-Serpent-Twofish).
• Based on Encryption for the Masses (E4M) 2.02a, which was conceived in 1997.

メモ。やねうらお−AIとかC#,3D,数学,compiler,disassembleとかについて書いちゃうぞ、と。(2005-01-14) より。

Hidden volume ってのは面白いな。一つのファイルの中に複数のボリュームを持っておいて片方をダミーにする。パスワードを明かすよう強いられた場合には、ダミーの方のパスワードを言うことで、本当に隠したかったデータを守る。もちろん、ダミーの方にも一見重要そうに見えるデータを保存しておかなくてはならない。

Hidden volume はCrossCryptと比較してTrueCryptの優れている点だな。

λ. CrossCrypt

Open Source AES and TwoFish Linux compatible on the fly encryption for Windows XP and Windows 2000.

CrossCrypt Features

• On the fly and offline encryption of Containers CD's compatible to standard Linux systems under Win2000 / XP
• Strong Encryption: Supporting /aes256 , /aes192, /aes128 (SingleKey Mode aes-loop compatible) and TwoFish (Use /2f) (160 Bit Key) (SuSE Linux compatible)
• GNU GPL License comes with full source .
• Denaiablity: You will not be able to tell that this file has been encrypted by filedisk as it looks completely random and can have any extension you wish.
• Encrypted CD Rom support. You can mount unencrypted CD Rom iso files as well. And you can dump ISO Images form existing CD's.
• Large files support theoretically more than 9.000.000 GB (dependig on your filesystem)
• No backdoors there is no master key or anything else that could be used to gain access to your files

メモ。同じく やねうらお−AIとかC#,3D,数学,compiler,disassembleとかについて書いちゃうぞ、と。(2005-01-14) より。

λ. 眞子様詔勅Flash

.

λ. 知への欲求

(『What is Science?』の感想をIRCから転載)

そもそも科学の起源とは何だったのか?
アシモフは言う、「Almost in the beginning was curiosity.」と。 そう。好奇心、あるいは何かを知ったり理解することに対する本質的な欲求こ そが全ての始まりだったのだ。

原始の生物、単細胞生物のような単純な生物ですら、生存のために食物を求め て周囲を探し回ったりといった、外界への好奇心と呼びうる衝動を持っていた。 進化が進むにつれて、そういった生存のための外界への好奇心は発達していき、 やがて単なる生存に必要な範囲を超えても止まらず、その余剰の好奇心が芸術 や技術や神話へ向い、そしてギリシャ哲学や科学へと至ったのだそうだ。

また、好奇心が我々のような生物にとっていかに本質的な欲求であるかとして、 アシモフは次のようにも言っている。

A human being, forced into a situation where one has no opportunity to utilize one's brain except for minimal survival, will gradually experience a variety of unpleasant symptoms.

こうした科学の起源の考え方は誤りではないと思うが、どこまで正しいのかは 正直良くわからない。しかし、とてもSF作家でもあるアシモフらしい見方で あるのは間違いないだろう。

そして、さらに現代の科学に見られるような「世界は確固とした法則によって 支配されているという世界観」「抽象化と一般化」「演繹」「帰納」「科学的 発見の一般への公開」といったものが如何にして現れ、科学を発展させ、現代 に至ったかについて、歴史を追いながらこれまた実に生き生きと論じている。

ことに、公理からの演繹によって幾何学で大きな成功を得たギリシャ人が、 公理からの演繹を重視するあまり観察や実験を軽視し行き詰ってしまい、 それがルネッサンス期に実験と帰納によって覆される過程は面白い。

The present general viewpoint is just the reverse of the Greeks. Far from considering the real world an imprefect representation of ideal truth, we consider generalizations to be only imperfect representatives of the real world.

見方がまるっきり逆になってしまったのである。まさにパラダイムシフトと呼 ぶにふさわしいし、ひょっとしたらこの変化は天動説から地動説への変化より も重要だったのではなかろうか。

Quotation

Seduced by the success of the axioms in developping a system of geometry, the Greeks came to think of the axioms as “absolute truths” and to suppose that other branches of knowledge could be developed from similar “absolute truth.”

Excellent Translation

幾何学の体系を構築する際の公理の成功に魅了されたギリシャ人たちは、公理を「絶対的真実」と考え、他の知識体系も同様の「絶対的真実」から構築できると考えるようになった。

Explanation

ギリシャ人たちは抽象化と一般化という強力な武器を使うことによって、数学と幾何学において成功を収めたのだが、それに驕ったのかギリシャ人たちは実験や観察を軽視してしまい、その結果誤りを犯すことになってしまったのだ。

λ. 君はアインシュタインを知っているか?

(『Who Was Albert Einstein?』の感想をIRCから転載)

アインシュタインの名を知らぬものはいない。そう。あの相対性理論の生みの 親である。また、今年2005年はアインシュタインが最も輝かしい業績を挙げた 「奇跡の年」から100年目にあたることもあり、注目を集めている。

だが、彼の業績は知っていても、彼がどのような人物で、どのように生きたか を知っている人はあまり多くはないのではないか。

果たして君は知っているだろうか?　アインシュタインがバイオリンを愛した ことを。考えることが好きで、教師の答えられない質問をしすぎたせいで、高 校を追い出されたことを。大学時代は苦学生だったことを。何故教師の仕事を 得ることを諦め、特許局に勤めたかを。彼がメディアにさらされ注目を集める ことを好んでいなかったことを。etc...

この本はアインシュタインの業績だけでなく個人的な魅力までを余すところな く伝える伝記である。この本はきっと君の知らないアインシュタインの一面を 見せてくれるはずだ。アインシュタインは、もちろん天才ではあったが、それ 以前に悩むことも苦しむこともある一人の人間だった。

ここで、私が個人的にアインシュタインの個性を最も感じさせられた部分を一 つ挙げよう。青年時代のアインシュタインの人生や結婚に関する哲学である。

Albert also decided that the freedom to think, to explore his own ideas, would always be the most important thing in life. If he got married and had children, his wife and family would matter to him, of course. But they would never matter as much, he realized, as his ability to think freely.

この考え方を自分勝手で自己中心的と考えることも出来る。だが、アインシュ タインにとってそれ以外の人生には意味が無かったし、彼にはそういう生き方 しか出来なかったのだ。結果として、後に最初の妻 Mileva とも離婚すること になってしまう。

私には、アインシュタインの価値観の是非については判断できないし、アイン シュタインの人生が幸福だったかどうかもわからない。ただ、人並みはずれた 好奇心が彼にもたらした成功と、同じ好奇心が彼にもたらした代償には、業を 感じずにはいられないのだ。

また、アインシュタインはとうとう亡くなる時まで考える事を止めなかった。

On April 17, 1955, he asked that his eyeglasses, some paper, and a pen be brought to his hospital bed. He had work thinking to do. The next day he died with a sheet of equations next to him. To the very end Albert was thinking.

天才と呼ばれる人の中には、不幸な最後を遂げている人が少なくない。そんな 中で、アインシュタインが最後まで思うように生き、そして安らかになくなっ たことを知ることが出来たのは、私にはとても嬉しかった。

Quotation

Albert also decided that the freedom to think, to explore his own ideas, would always be the most important thing in life. If he got married and had children, his wife and family would matter to him, of course. But they would never matter as much, he realized, as his ability to think freely.

Excellent Translation

またアルベルトは自由に思考しアイディアを追及することは常に人生で最も重 要なこととしようと決めた。もちろん結婚し子供を持てば妻や子供は心を捕え るだろう。だが、それとて自由に考えることほど自分の心を捕えたりはしない だろうと、悟ったのだ。

Explanation

ドイツの高校から追われスイスの高校に入学するまでの間アインシュタインは イタリアに滞在していた。彼はハイキングしながら色々なことを考え、自分の 人生について色々なことを決めた。この考えを自己中心的と考える人もいるだ ろうが、彼にとってそれ以外の人生には意味が無かった。

λ. 諸君 夜が来た

諸君 夜が来た
無敵のM2諸君
最古参のM2諸君
万願成就の夜が来た
修論完成の夜へようこそ!!

λ. 子の二つ

修論完成の夜は始まったばかり。 今宵は短い夜になりそうだ。

λ. 丑の刻

草木も眠る何とやら。 英文アブストラクトを書いてみた。

λ. 寅の二つ

最近、私は毎日大体この時間に寝ます。 次の日の修論書きに影響が出ないギリギリの時間。

λ. 寅の四つ

うっすらと、外が白くな……らない。 こんな時間に発狂している学生を見たら間違いなくM2だ。

λ. 夜明け

修論完成の夜はあっという間に明け、朝になった。 まさかこの位で、M2の夜は明けてはいないよね。

λ. 世明け (39:00)

……というわけで、無事提出完了。

色々と思うところはあるけど、長かった12月もようやく終了という感じ(笑　みなさん、明けましておめでとうございます。今年もよろしくお願いいたします。

λ. “Foundations for structured programming with GADTs” by Patricia Johann and Neil Ghani

この論文、年末年始に読もうと思って印刷したまま積読になっていたのだけど、稲葉さんのmemo: POPL 3 - d.y.dと住井さんの POPL 2008メモ3日目 - sumiiの日記 で言及されていたのをきっかけに読んだ。

まず、基本的なGADTは以下のような形で定義される。

data G a where
   GCon :: F G a → G (H a)

このデータ型は、K t a = ∃b. (Eql (H b) a, F t b) とおく*1と、以下で定義されるデータ型と同型。

data NG a where
   NGCon :: K NG a → NG a

で、F, H がそれぞれ F : (|C|→C)→(|C|→C), H : |C|→|C| という関手のとき、K は (|C|→C)→(|C|→C) の関手となり、入れ子データ型の場合(c.f. 20061005#p02)と同様に、NG は K の始代数としてみなせる。そのため、fold/buildの定義とそのshortcut融合変換が出来る(c.f. 20060926#p02)。

圏論的に考えると、GCon と NGCon の対応は、GとNGが同型であることと、K t が「left Kan extension of Ft along H」(Lan_H Ft) であることによって与えられている。

いずれも言われてみれば当たり前なんだけど、収まるべきところに収まっている感じがする。 それと、やっぱり論文の書き方が上手いなぁ。 Haskellの構文を使いながら圏論的な議論をするやり方とかは見習いたいと思った。

λ. 『デッドライン—ソフト開発を成功に導く101の法則』 by Tom DeMarco

読了。デマルコの本はこの分野では非常に有名だと思うけど、これまで読んだこと無かった。読むのは初めてだったけどこれは面白いね。

この本は、主人公トムキンスが旧東側のモロビア共和国というところでソフトウェア開発プロジェクトを率いる物語で、その中で彼が学んだことが「101 の法則」としてまとめられている。 物語仕立てになっていることで、プロジェクトの運営に関する様々な要因と成功の鍵を、単に知るだけでなく納得することが出来るようになっている。 また、ユーモアと優しさにあふれていて、単に読み物としても楽しく読めるのが、素晴らしい。

これまでソフトウェア開発プロセスほげほげだとかソフトウェア工学だとかは、官僚的でかつ実態に即していない無意味な指標ばかりが踊っているという印象があったけど、こういった形で説明されて初めて、もともとは納得できる目的と意味があったのだなと感じた。結局、重要なのは手法そのものじゃなくて、その背景にあるこういった考え方なんだろうな。

そういえば、トムキンスという名前はガモフの『不思議の国のトムキンス』からだそうだけど、『不思議の国のトムキンス』は Simon Singh の Big Bang でも言及されてたな。 あと、NNLがいいキャラしてるなぁ。

λ. 泳いできた

今日も帰りに泳いできた。 今日は調子が良く、1km泳ぐのに25分をきった。 今年通算で2km。