日々の流転

λ. ホンカン

ホンカン発見。

λ. マージソート

安定なソートの話がどっかであったので、現実逃避に書いたマージソート。ださーい。それに、Range#begin=とRange#end=欲しいなぁ。そーいや、Range#lengthってIntegerの場合はsucc使わないのね…

class Array
  def msort!(&compare)
    tmp = Array.new(self.length)

    compare = lambda{|i,j| i<=>j} if compare.nil?

    sort = lambda{|a|
      if a.length > 1
	l = a.begin...(a.begin + a.length / 2)
	r = l.end...a.end

	sort.call(l)
	sort.call(r)

	i = a.begin
	while l.length > 0 and r.length > 0
	  if compare.call(self[l.begin], self[r.begin]) <= 0
	    tmp[i] = self[l.begin]
	    l = l.begin.succ...l.end
	  else
	    tmp[i] = self[r.begin]
	    r = r.begin.succ...r.end
	  end
	  i = i.succ
	end

	tmp[i, l.length] = self[l] if l.length > 0
	self[a.begin...r.begin] = tmp[a.begin...r.begin]
      end
    }

    sort.call(0...length)
    self
  end
end

λ. 東方紅魔郷

「よけてるんじゃない、かすりに行ってるんだ」か。

λ. ロリとは

...

λ. 買った本

週間エコノミスト 2002年11月19日号

-

λ. 論文読み会: rfc2291

資料

λ. 夕食

久しぶりに豚菜。

λ. zip, unzip

CPLで書くとどうなるかと考えてたら意外と難しい。無限リストであるinflistに対しては

zip   = fold(prod(head, head), prod(tail, tail))
unzip = pair(inflist(pi1), inflist(pi2))
      = pair(fold(pi1.head, tail), fold(pi2.head, tail))

と単純なんだけど、普通のリストであるlistに対してはなかなかうまく定義できない。多分、λ計算で定義するのも結構大変なんじゃなかろうか。

λ. 自己嫌悪。

λ. すりかえられたselfにCからアクセスするには?

instance_evalやdefine_methodを使うとselfがすりかえられた状態でブロックが実行される。rb_iterate()やrb_proc_new()を使ってCの関数をブロックとして与えた場合、Cの関数からこのselfにアクセスするにはどうしたら良いか?

まず思いつくのは ruby_frame->prev->self だけど……

って、よく見たら第三引数としてselfが渡されてるか。これもUndocumentedっぽいから大差ないかもしれないけど。

λ. 人狼審問 : (950)湿地の村

今回は確定霊能者で初回襲撃されてずっと墓下だったけど、 ようやくエピローグで皆と再会。 全然活躍できなかったけど、久しぶりの勝利なので一応嬉しい。

関連リンク

• B1/950村 - 人狼ファンWiki
• 他の人の感想
  • chizさん (ステラ)

λ. yhc - York Haskell Compiler

[Haskell] [ANNOUNCE] yhc - York Haskell Compiler , Thomas Davie より。

nhc98をベースにしたhaskellコンパイラ。 「λ」を上下反転した「y」がカッコいい。

試しに適当なコードをコンパイルしてみる。

% cat Fact.hs
module Fact where

fact :: Int -> Int
fact 0 = 1
fact n = n * fact (n-1)

main :: IO ()
main = putStrLn $ show $ fact 10

% yhc -bcodecompile Fact.hs
======  BCode after compilation:
FUN Fact;fact{188}(1/0) ["v215"]
 STACK 2
   {
    PUSH_ARG 0          1 <["215"] | {"215"}>
    EVAL                1 <[] | {}>
    INT_CASE {0 -> L_2, _ -> L_4}               1 <[] | {}>
L_2                     1 <[] | {}>
    POP 1               0 <[] | {}>
    PUSH_INT 1          1 <[] | {}>
    JUMP L_3            1 <[] | {}>
L_4                     1 <[] | {}>
    POP 1               0 <[] | {}>
    JUMP L_0            0 <[] | {}>
L_3                     1 <[] | {}>
    JUMP L_1            0 <[] | {}>
L_0                     0 <[] | {}>
    PUSH_INT 1          1 <[] | {}>
    PUSH_ARG 0          2 <["215"] | {"215"}>
    MK_AP 0 2           1 <[] | {}>
    MK_AP 1 1           1 <[] | {}>
    EVAL                1 <[] | {}>
    PUSH_ARG 0          2 <["215"] | {"215"}>
    EVAL                2 <[] | {}>
    MUL_W               1 <[] | {}>
L_1                     1 <[] | {}>
    RETURN              1 <[] | {}>
   }
---- ConstTable ---------------
0 FUN Prelude;Prelude.Num.Prelude.Int.-{213}
1 FUN Fact;fact{188}
-------------------------------

FUN Fact;main{189}(0/0) []
 STACK 2
   {
    PUSH_INT 10         1 <[] | {}>
    MK_AP 0 1           1 <[] | {}>
    PUSH_CONST 1        2 <[] | {}>
    MK_AP 2 2           1 <[] | {}>
    PUSH_CONST 3        2 <[] | {}>
    MK_AP 2 2           1 <[] | {}>
    EVAL                1 <[] | {}>
    RETURN              1 <[] | {}>
   }
---- ConstTable ---------------
0 FUN Fact;fact{188}
1 FUN0 Prelude;Prelude.Show.Prelude.Int.show{214}
2 FUN Prelude;${43}
3 FUN0 Prelude;putStrLn{45}
-------------------------------

【2006-04-28追記】 Unicodeの文字はまだ扱えないようだ。hbcファイルのフォーマットがUnicodeの文字を扱えるようになっていない。

% cat UnicodeTest.hs
main = print ('\x10ffff')
$ yhc UnicodeTest.hs
Compiling Main             ( UnicodeTest.hs )
yhc.exe: wUByte of 1114111

λ. GTD (Getting Things Done) を試す

池上さんが最近紹介していたこともあり、GTDが気になっていたので、試してみることにした。まずは池上さんも紹介していたHoriさんの記事を読んだ。それから、とりあえずたださんの記録を参考にRTMのアカウントを取得し、タスクを適当に登録してみる。GTD Style Wikiというのも便利そうだ。

λ. 『HELLSING (9)』 by 平野 耕太

HELLSING 9 (ヤングキングコミックス)(平野 耕太) を読んだ。 10巻で完結らしいし、最後に向けて盛り上がってきたなあ。

λ. SPASS を試す

SPASS: An Automated Theorem Prover for First-Order Logic with Equality という一階述語論理の定理証明機を見つけたので、ちょっと試してみる。

Smullyan's drinkers' paradox

まずは、こないだ20070828#p02でAgdaで証明を書いた Smullyan's drinkers' paradox を試してみる。

begin_problem(Drinker).

list_of_descriptions.
name({* Smullyan's drinkers' paradox *}).
author({* Masahiro Sakai *}).
status(unsatisfiable).
description({* Smullyan's drinkers' paradox *}).
end_of_list.

list_of_symbols.
predicates[(Drink,1)].
end_of_list.

list_of_formulae(axioms).
end_of_list.

list_of_formulae(conjectures).
formula(exists([x], implies(Drink(x), forall([y], Drink(y))))).
end_of_list.

end_problem.

Webから試せるようになっているので、これを-DocProofオプションと共に与えると何やら証明らしきものが得られるが、読み方が良くわからない。

パースの論理式(Peirce's formula)

命題論理の例として、先日20070814#p01でHaskellで証明したパースの論理式(Peirce's formula)を試してみる。当然何の問題もない。

begin_problem(Peirce).

list_of_descriptions.
name({* Peirce's formula *}).
author({* Masahiro Sakai *}).
status(unsatisfiable).
description({* Peirce's formula *}).
end_of_list.

list_of_symbols.
predicates[(P,0), (Q,0)].
end_of_list.

list_of_formulae(axioms).
end_of_list.

list_of_formulae(conjectures).
formula(implies(implies(implies(P, Q), P), P)).
end_of_list.

end_problem.

様相論理の例 (2007-11-23追記)

命題様相論理の論理式は、「世界」の集合を個体領域とする一階述語論理の論理式に変換することが出来る。 そのため一階述語論理の定理証明器等を様相論理に対して使うことが出来る。 そして、SPASSには様相論理を扱う機能があり*1、変換を自動的に行って証明をしてくれる。

以下の例は、到達可能性関係が反射的であることを仮定して、□A→A を証明する例。 ここでは反射的であることを明示的に公理としているが、オプションで -EMLTheory=2 を指定すれば全ての様相の到達可能性関係が反射的であることは自動的に仮定される。 その方が効率は良いかも。

begin_problem(Reflexivity).

list_of_descriptions.
name({* T from Reflexivity *}).
author({* Masahiro Sakai *}).
status(satisfiable).
description({* T from Reflexivity *}).
end_of_list.

list_of_symbols.
predicates[ (R, 2), (r, 0), (A, 0) ].
translpairs[ (r, R) ]. % r is interpreted as R
end_of_list.

list_of_special_formulae(axioms, eml).
formula( forall([x], R(x, x)) ).
end_of_list.

list_of_special_formulae(conjectures, eml).
prop_formula( implies(box(r, A), A) ). % T
end_of_list.

end_problem.

λ. Information Flow: The Logic of Distributed Systems (ペーパーバック)

チャネル理論(Channel Theory)の教科書である Information Flow: The Logic of Distributed Systems (Cambridge Tracts in Theoretical Computer Science)(Jon Barwise/Jerry Seligman) のペーパーバック版が最近出版された。チャネル理論は情報の流れやその背景にある規則性といったものを扱おうとする理論で、定性的情報理論などと呼ばれることもある。まあ、そういう大げさなお題目はどうでも良いのだけど、シンプルでちょっと面白い理論だ。

向井先生がチャネル理論を気に入っていたこともあって、私もこの本は昔途中まで読んだことはあるんだけど、そのときには最後まで読み終えてはいなかった。 今回ペーパーバック版が出て、しかも今は円高で少し安く買えるので、これを機にまた久しぶりに読んでみようかと思い、購入してみた。

……のだけど、Amazonのページをみたら「あわせて買いたい」と「この商品を買った人はこんな商品も買っています」とで、例の郡司ペギオ-幸夫氏の「時間の正体 デジャブ・因果論・量子論」*1が挙げられていて微妙に脱力した。一緒にしないでくれよぉ。もきゅ (´・ω・`)

λ. コナミスポーツクラブ

コナミスポーツクラブに先日会員登録して、今日もまた行ってきた*1。 今日はまず30分くらいでの器具の使い方のインストラクションを受けてきた。それが終わったあとは何をしようかと思ったのだけど、とりあえずサイクリングマシンで体力測定して、あと500mだけ泳いできた。 しかし、体力測定で体力年齢48歳とかでたのはまいったね。確かに体力のある方ではないけど、最近は一応定期的に運動しているのになぁ。この測定の基準データの母集団、どんだけ健康なんだよ。