2001-10-29
λ. 学校が休みにも関わらず本を返すためだけに学校に…
λ. SPAM
最近、こんな事が書いてるSPAMを受け取ったんだけど、これってまじっすか? 誰かおせーて。
[追記]http://www.isc.meiji.ac.jp/~sumwel_h/doc/code/bill-1998-g.htm#SEC301によるとその通りって事になりそう。(よしだむメモ(2001-11-16)より)
This message is in full compliance with U.S. Federal requirements for commercial email under bill S.1618 Title lll, Section 301, Paragraph (a)(2)(C) passed by the 105th U.S. Congress and cannot be considered SPAM since it includes a remove mechanism.
λ. Prologのパーサの話
そういや、Prologって演算子の定義が割と自由だから、パースしただけじゃ内部のデータ構造を構築出来なさそうな気がする。極端な事言えば「:-」や「,」すらも演算子だし… 最初にファイル全体をパースする時点ではトークンを節単位に切り分けておくくらいしか出来ないんじゃなかろうか。で、consultは節毎に「現在登録されている演算子から判断してトークンから有向グラフを組み立ててassertし、必要ならば新たに演算子を登録する」というのを必要なだけ繰り返す。…みたいな。
うーん。「mortal(X) :- human(X)」が「':-'(mortal(X), human(X))」なのは良いとして、「foo,bar,baz」を「','(foo, ','(bar, baz))」と表して良いものなの? それに「assert((:- op(100, xfx, @))).」みたいなのはどうなの?
……なんか混乱して来た。やっぱ、ちゃんと調べなきゃだめか…
2002-10-29
λ. 読書
- 『オフィス北極星 6』
- 『オフィス北極星 7』
- 『オフィス北極星 8』
- 『オフィス北極星 9』
- 真刈信二[著], 中山 昌亮[イラスト]
λ. 萩野服部研
SICPは問題2.1.11まで進んだ。
ところで、λm.λn.nm で church numerals の巾乗が定義できる事は、それなりに面白い事実だと思うのだけど、あまり興味を持ってはもらえなかった模様。
λ. 夢
夕食後にまどろんでいたら、許しがたい侮辱を受ける夢を見た。感情的な反論をしてしまったけど、あのような悪意を前に感情的な対処は愚かだった。というか夢で良かった……
2004-10-29
λ. 「進化論」の起源
(『The Origin of a Theory —ダーウィンとその時代』の感想をIRCから転載)
この本は専門用語なども多く、私には少々難しい本だったが、とても面白かった。
この洒落たタイトル“The Origin Of a Theory”はもちろんダーウィンの著書 “The Origin Of a Species”のもじりであり、進化論の誕生と進化を、生物 のそれになぞらえて、ダーウィンを中心として描いている。
我々が科学を学校等で学ぶとき、学びやすく整理された形で学んでいる。しか し、当たり前だが、科学は学校で学ぶような形で発展してきたのではない。進 化論もまた例外ではない。生物が神によっていきなり今ある姿で造られたので ないのと同様に、進化論もいきなり今ある姿で誕生したのではないのだ。
進化論のダーウィン以前の一つの起源はダーウィンの祖父エラズマス・ダーウィ ンの『動物論』、ラマルクの理論(獲得形質居伝説)などに求められる。そして、 ダーウィンはビーグル号の航海に博物学者として同行した際の観察と、近代地 質学の父とよばれるライエルの地質学等から、理論の着想を得た。また、マル サスの『人口論』にも触発されていたそうであり、この点には意外であり非常 に驚かされた。その点について本書では以下のように書かれており、印象に残っ た。なおここでのheとはダーウィンのことである。
"One may say", he now concluded, “there is a force like a hundred wedges trying [to] force every kind of adapted structure into the gaps in the economy of nature, or rather forming gaps by thrusting out weaker ones.” This idea of a “struggle for existence” was not new; it had been present in the wrigings of Malthus, Paley, Lyell, the Swiss botanist Augustin de Candolle (1778-1841) and others.
ところで、アイディアが最初に登場するときには荒削りであり、そして試行錯 誤があり、整理され、やがて我々の知る形になっていくと私が考えている。ダー ウィンの進化論もまさにそうして生まれたのである。彼の理論には批判も多かっ たし、宗教的な攻撃を受けることもしばしばであったが、結局のところ「生き 残った」。そして、生き残ることが出来る理論は、現実を最もよく説明する理 論、言い換えればもっとも「現実」に適応した理論だけなのであろう。今日ダー ウィンの理論が修正され洗練されつつも生き残っているのは、それが現実を最 もよく説明するからであろう。このことを考えると私はとても愉快だ。
それはそうと、この本の著者はドーキンスが好きなようで、「まえがき」にも 参考文献にもドーキンスの著書が挙がっている。ドーキンスが稀代のサイエン スライタであることは誰もが認めるところだろうが、この話題でグールドが触 れられていないのは、個人的には少々納得がいかないところである。そこで、 私からは『ドーキンス対グールド 適者生存の戦い』(原題: “Dawkins vs. Gould : Survival of the Fittest”)を薦めておきたい。
- Quotation
- Although Darwin did not, and could not, have caused such a major change single-handedly, he will always stand for the transformation and enrichment of man's understanding of his place in nature.
- Excellent Translation
- ダーウィンはこれほど大きな変革を一人でしたわけでも一人で出来たわけでもないが、常に自然の中での人間の位置づけの認識の変化と強化の象徴であるだろう。
- Explanation
- 本書の結びのことば。結局のところ、進化論が最もインパクトを与えたのは、自然の中での人間の位置づけに関する認識だったのだ。
2005-10-29
λ. 2005年度秋学期修了予定者中間発表
中間発表を見に行った。kamimooの発表に間に合うように行こうと思っていたら、寝坊して間に合わなかった。着いたときには竹内君が発表していた。亜群(groupoid)はすべての射が同型射である圏だと思っていたが、二項演算が定義された集合という意味もあるのか。知らなくて少し混乱した。調べてみるとマグマ(magma)とも呼ばれるようだ。
色々な人の発表を見ていて少し欝になる。来年は我が身。
ところで、服部先生のblogに残酷な修士のテーゼというのが載っていた。笑えるけど、笑えない。
λ. カタン
0勝4敗。 ルールを忘れてたってのもあるが、俺テラヨワス。
2007-10-29
λ. Google デスクトップの説明わかりにくい
Google デスクトップで「複数のコンピュータ上のデータ検索」を有効にした場合の説明として、「インデックスに登録されたファイルのテキストが Google デスクトップサーバーに転送され、お客様の他のコンピュータにコピーされます」とある。 それは当然なのだけど、その上で「他のコンピュータから検索できるこのコンピュータのデータ」を「なし (他のコンピュータのみを検索します。このコンピュータのファイルは他のコンピュータから検索できません。)」にしても、テキストはGoogleのサーバに転送されるのだろうか?
説明がわかりにくいよ……
λ. 『数学ガール』 結城浩
読了。
λ. 携帯ストラップ壊れた
9/15にキャンドゥーで買った携帯のストラップ がもう壊れた。 当り外れもあるのだろうが、前にダイソーで買ったやつが1年半以上もったのに比べると、随分壊れやすいなぁ。
2008-10-29
λ. Seven Trees 問題を定理自動証明器を使って解く
Seven Trees 問題を解くときに、一階述語論理の定理自動証明器を使って解けないか試していた。 そのためには、以下の等式を公理として、T = T7 を証明させれば良い。
- x+y = y+x
- x+(y+z) = (x+y)+z
- x×y = y×x
- x×(y×z) = (x×y)×z
- x×(y+z) = (x×y)+(x×z)
- 1×x = x
- T = 1+T×T
最初にSPASSで試したのが 7trees.dfg だけど、これは止まらなかった。 可換性と結合性を直接サポートしていないのが不味いのではないかと思い、The E Equational Theorem Prover で試してみたのが 7trees.lop で、これもやっぱり止まらなかった。 あと、EQPなんかも試してみたが、これは使い方がいまいち良くわからなかった*1。
ここで諦めて結局手で解いてしまったのだけど、ふと思いついて以下のような公理(を途中で打ち切ったもの)から T1 = T7 を証明させてみたところ、うまくいった。
- x+y = y+x
- x+(y+z) = (x+y)+z
- T1 = T0+T2
- T2 = T1+T3
- …
これはいわば全て展開した多項式だけを対象にすることにしたもの。 ここで Tk+1 = Tk + Tk+2 は最初の公理系の定理なので、Tk を Tk で解釈すれば、この公理系における証明から最初の公理系における証明が得られる*2。 で、実行してみたところ、SPASSでもEでも一瞬で証明できた。 出てきた証明は、「Seven Trees やっと解けた」で手で導出したものと、ほぼ同じもの。
人の目から見るとどっちの公理系も同じようなものだけど、ちょっと工夫して問題を変形してやるだけで自動定理証明には劇的な効果がある、というのが面白かった。
【2009-02-15追記】 さらに、他の定理証明器として Prover9 と Equinox でも試してみた。
- Prover9は既に試した定理証明器と同じく、元の問題7trees.inは止まらず、単純化した問題7trees2.inは一瞬で解けた。
- Equinoxは残念ながら元の問題7trees.tptpでも単純化した問題7trees2.tptpでも止まらなかった。
λ. 水泳1km
今日も帰りに1km泳いできた。 かかる時間はちょっとずつ短くなって、今日は1kmで25分くらい。
λ. 【金融危機】日銀、利下げも検討 急激な円高・株安を懸念
「金融緩和を検討する」と言いつつ、実際には「日銀は独自の施策として、金融機関が日銀に預けている当座預金に利子を付ける方針」という、まるで正反対のことをしてるのね。 意味不明すぎる。 これが日銀クオリティwww
