日々の流転

λ. 買った本

• 「中央公論」 2002年1月号
• 「ダ・ヴィンチ」 2002年1月号

λ. 来年度予算案

歳出を減らして税収が減ってるんだから世話ねえよな。

λ. どうして数には必ず一を足せるんでしょうか？ そもそも足すってどういう事？

自然数よりも大きな集合に対しては面倒なのでパス。自然数に限って言えば、1を足すってのはsuccessorを作ること。算術公理を満たすためには、0に対応する元が存在して、かつ任意の元に対してsuccessorが存在しなければならないので、自然数であれば1を足せる事は自動的に保証されてるはず。で、2以上の数の加算はそこから帰納的に定義出来るはず。

λ. 算術公理

反射律  x = x
対称律  x = y → y = x
推移律  x = y → (x = z → y = z)
代入律  x = y → (A → A[x/y])
 
算術の和と積の公理
 
¬(0 = s(x))
s(x) = s(y) → x = y
x + 0 = x
x + s(y) = s(x + y)
x × 0 = 0
x × s(y) = x × y + x
 
数学的帰納法
 
(P(0) ∧ ∀x(P(x) → P(s(x)))) → ∀x(P(x))

λ. そういえば、春学期の論理プログラミングで似たことをやったような……あ、あったあった。→ Prologで作る数字の世界

λ. 上海

調子悪いなぁ。打つ手打つ手が裏目に出る。つーわけで惨敗。ぬぅ、正月を見ておれよ!

λ. 朝鮮語

あの 치카 씨 (チカさん) がアイドルだったということを初めて知った。しかも写真集まで出していたとは……
→ 尾羽智加子

λ. 研究会

「最近、型推論とか興味あるんですけど、どうっすか?」と某H先生に訊いたら、「型推論って面白いけど現実には役に立たないかも」とか言われてしまった。うぐぅ。

λ. 言語の意味論

PTQはオントロジー(存在論)が貧弱。例: 裸の複数名詞句

• Soldiers are brave. (兵士一般についての文)
• Soldiers are drank. (特定複数の兵士についての文)
• ゴキブリはどこにでもいる。Cockroaches are everywhere.

個体概念だけでは不足。 => Greg Carlson の存在論

kind,object,stageのいずれに働くかという情報を動詞句が持っていると考える。

自由Σ代数系は記号としての式の全体そのもの。 自由Σ代数系とオントロジーは深く結び付いている。

• 「オントロジーは自由Σ代数を作る手続き」-- P.Aczel

λ. 東方紅魔郷

ようやくノーマルをノーコンテニューでクリア!!。霊夢の「夢の御札」を使いました。86215060点で、中村さんには約8万点ほど及ばなかったけど、これで心置き無く冬休みに入れます。(笑)

λ. 借りた本

『状況と態度』

ジョン・バーワイズ (Jon Barwise), ジョン・ペリー (John Perry) [著]
土屋 俊, 白井 英俊, 向井 国昭, 鈴木 浩之, 片桐 恭弘 [訳]

『自然言語の意味論 - モンタギューから「状況」への展開』

白井英俊[著]

λ. 買った本

• Software Design 2003年1月号
• BSD Magazine 2002 No.14

λ. ニューラルコンピューティング

基礎教養としての Logic と Thermo Dynamics の重要性をずいぶん強調してた。

それと、何でも熱力学では最近Adrian Bejan教授らの Constructal Law というのが熱力学の第四法則と言われてるそうだ。この Constructal Law を使うと、試行錯誤したりせずに、最初から最も効率のよいものを設計できるそうだ。って、本当かよ?

あと、Logic についての説明には色々とツッコミたくて仕方なかったけど、我慢我慢。なんというかハッタリが巧いなぁと思いますた。

λ. ι棟五階からみる富士山

携帯電話のカメラだとやっぱり暗いところが潰れるし、全体的に階調が綺麗に出ないな。すごく綺麗だったのに残念。

λ. ゆで卵だと思って割ったら

ゆで卵だと思って割ったら、温泉卵だった。しょぼーん。勢い良く回転するのも確認したのに……

λ. 頭の体操: 3引数flip

現実逃避にやってみる。当たり前だけど、({id,flip31,flip32,flip33,flip34,flip35}, (.), id)は群をなし、{a,b,c}上の置換群と同型。

flip31 :: (a -> b -> c -> d) -> (a -> c -> b -> d)
flip31 = map flip
  where
    map :: (x -> y) -> ((z -> x) -> (z -> y))
    map = (.)

flip32 :: (a -> b -> c -> d) -> (b -> a -> c -> d)
flip32 = flip

flip33 :: (a -> b -> c -> d) -> (b -> c -> a -> d)
flip33 = flip31 . flip32

flip34 :: (a -> b -> c -> d) -> (c -> a -> b -> d)
flip34 = flip32 . flip31

flip35 :: (a -> b -> c -> d) -> (c -> b -> a -> d)
flip35 = flip32 . flip33

λ. お菓子を少し買い込んでみた

λ. OCaml-Nagoya の人たちと飲み会

OCaml-Nagoya の人たちとの飲み会に参加。

関連

• OCaml-Nagoya の人たちと飲み会 - まめめも

λ. 落ち込んでいる

最近色々あってちょっと落ち込んでいる。 何かしてれば平気だけど、ふとしたときに思い出して、やるせない気分になる。 相変わらず打たれ弱いなぁ…… (ため息

λ. Universal Shell Programming（USP）向けシェル機能と実装 by 片山善夫 and 當仲寛哲

Unixのシェルスクリプトで業務開発というのを見て驚いた。 現状のUnix上のシェル環境では、たとえ拡張したとしても、やっぱり無理がある*1と思うが、元々のUnixの思想としては確かにこうあるべきなんだろうなぁ。

• 第162回 ソフトウェア工学研究発表会
• Universal Shell Programing Laboratory
• CiNii - Universal Shell Programming (USP)向けシェル機能と実装(シェルプログラミング・Webアプリケーション)
• 情報処理学会電子図書館 - Universal Shell Programming (USP)向けシェル機能と実装(シェルプログラミング・Webアプリケーション)