日々の流転

λ. 近代思想の補講を受けにきたので、土曜日なのに学校にいる。土曜の1限なのでやはり出席者は少なくて10人くらいで、雑談ぽい感じで結構楽しかった。授業後にビールで乾杯。

λ. Ruby Hotlinks

に登録されたみたい。

λ. 風邪

だるくてフラフラする。無理をしすぎたらしく、風邪をひいてしまったようだ。脇の下で体温を測ると37.8°Cだったんだけど、医者のところに行って鼓膜で一瞬で測ると36.9°C。前に、風邪ひいたときもそうだったな。しかし、注射する際に腕に触って「やっぱ熱いわ」とか言われた。鼓膜の体温が低い体質なのだろうか・・・

λ. ドイツ語

今日は発話試験。あらかじめ指定されていた3つのテーマのうちから一つを指定されて、それについて会話を先生の前で発表する形式。内容が発表されてから一週間なかったので、パートナーともなかなか都合が合わず、あまり準備出来なかったのだけど、なんとか無事に済ませることが出来た。結構緊張したのだけど、先生がクンスト先生で助かった。

ちなみに、指定されたテーマは「Was hast du in den Sommerferien vor?」で、 一番ネタな会話を用意していたテーマだけあって、結構先生もうけてた。

λ. Re: Collatz予想

無限リストでメモ化すること自体は考えたのですが、私の考えたのは再帰呼び出し毎に(!!)を使って値を取り出すもので、かなり遅かったために書きませんでした。稲葉さんのコードは面白いですね。ただ、私ならこう書くかな。

-- まったくもってこれ以上ないくらいごくごく普通の何の変哲もないinterleave
(/\/) :: [a] -> [a] -> [a]
(x:xs) /\/ ys = x : (ys /\/ xs)
[] /\/ ys     = ys

-- g!!n == 自然数(n+1)が収束するまでのステップ数
g :: [Int]
g = 1 : map (+1) (g /\/ map head (iterate (drop 6) (drop 9 g)))

-- h!!n == [1..n+1] の中で一番収束にかかるステップ数がでかいの
h :: [Int]
h = map fst $ scanl1 phi (zip [1..] g)
    where phi a@(_,gk) b@(_,gk')
              | gk' > gk  = b
              | otherwise = a

main = print h

追記

そっか、タプルの順番を入れ替えれば、scanl1に渡す関数は単にmaxで良いのか……気づかなかった。

2006-09-14 追記: 顔文字に見える件について

中置演算子を普通の関数として書くためには括弧で囲う必要があるので、こんなことになってます。しかし、まあ顔文字には見えますよね。特にこんなのとか。

Main> :t (^^)
(^^) :: (Integral b, Fractional a) => a -> b -> a
Main> 2 ^^ (-1)
0.5

λ. 『θは遊んでくれたよ』 森博嗣

を読んだ。トリックは予想通りだが、犯人の特定が少し面白かった。しかし、もはやキャラ萌え小説だよなぁ。キャラクタや先の展開が気になるから読むけど、単体で楽しむには辛くなってきたように思う。

Quotation

物理的な証拠が、仮説を少しずつ揺るぎないものにしていくだろう。事実とはこうして後から形成されるものだ。しかし、人の心の中の、その時々の葛藤かっとう)は、二度と正確に再現されることはない。たとえ、本人の口が語ったとしても、その言葉は明らかに虚構である。理由も動機もすべて、光が当てられたときに現れる影に過ぎない。光の当て方によっては、影はどちらにも現れ、形の歪ひず)み方も変わり、幾つもが同時に現れることさえある。

λ. ひぐらし解

今日こそ見ようと思っていたが、うとうとして気付いたら28:30くらいだった。しょぼーん。というか、色々ダメ過ぎ。

λ. 推移閉包が一階述語論理では表現できないことをAlloyで確認する

Alloy - 言語ゲーム(2009-05-27) にコメントした話から。

以前「推移閉包は一階述語論理では表現できないのね」と書いたが、 Alloyは一階述語論理に推移閉包を加えて拡張した論理なので、推移閉包の機能を使わずに書いた関係と、推移閉包の機能を使って書いた関係が等しいかをAlloy上で検査すれば、イメージしやすくなるのではないかと思った。

まず、集合UとU上の二項関係R1,R2を定義。

sig U {
  R1 : set U,
  R2 : set U
}

次に、R2がR1の推移閉包であることを、推移閉包の機能を使わずに記述してみようとする。

fact {
  all x, y : U {
    y in x.R2 <=> (y in x.R1 || (some z : U | z in x.R2 && y in z.R2))
  }
  //// 関係演算を直接使った書き方
  // R2 = R1 + R2.R2
}

そして、Alloyの推移閉包の機能を使うと、R1 の推移閉包は ^R1 と書けるので、R2 が ^R1 と一致するかを検査してみる。 ただし、あまりに trivialな例でも面白くないので、R1が空でないという制約を追加しておく。

fact { some R1 }

assert R2_is_TC_of_R1 {
  R2 = ^R1
}

check R2_is_TC_of_R1

で、検査してみると、例えば以下の図が反例として出てくる。

R2はR1を含む推移的関係になっているけど、推移閉包すなわち「R1を含む最小の推移的関係」にはなっていない。 こういった最小性や最大性は一般に一階述語論理では表現できない。