トップ 最新 追記

日々の流転


2009-03-02 [長年日記]

λ. PPL2009参加します

今更ですが、今年もPPL2009に参加する予定です*1。色々な人にお会いできるのを楽しみにしていますので、見かけたら是非お気軽に声をかけてくださいませ。

*1 二日目の セッション8 (萌芽的研究) で発表します

λ. Maceで数独を解く

ParadoxDarwinで解いてみたので、ついでにMace4でも試してみたのだけど、どうもうまくいかなかった。

ちなみに、Mace4はこんなやつ。

Mace4 is a program that searches for finite models of first-order formulas. For a given domain size, all instances of the formulas over the domain are constructed. The result is a set of ground clauses with equality. Then, a decision procedure based on ground equational rewriting is applied. If satisfiability is detected, one or more models are printed. Mace4 is a useful complement to first-order theorem provers, with the prover searching for proofs and Mace4 looking for countermodels, and it is useful for work on finite algebras. Mace4 performs better on equational problems than our previous model-searching program Mace2.

【追記】 Sudoku with Mace4 にMace4を使って数独を解く話があった。 これを参考に入力ファイルに「assign(domain_size, 9).」を加えて、数字の9を0に置換したら普通に解けた。 Mace4では非負整数nはモデルのn番目の要素を指す項になっていて、その関係でちょっと注意が必要ということのようだ。

本日のツッコミ(全2件) [ツッコミを入れる]

ψ ささだ [いいなぁ.]

ψ さかい [ささださんは不参加? それは残念……]


2009-03-04 [長年日記]

λ. IDPで数独を解く

数独をParadoxDarwinMaceで解いてみたので、ついでにIDPでも試してみた*1

IDPの特徴は帰納的定義が出来ることのようだ(普通の一階述語論理では帰納的な定義は出来ない)。 具体的には { R(t1,…,tn) <- 論理式. } 等と書けて、論理式の中でRを使うことで、関係Rを帰納的に定義出来る。 帰納的定義が出来るということは、例えば推移閉包を公理化出来るので、グラフが関係してくるようなパズルを解くのには向いていそうだ。

あと、記述言語では例によって、感嘆符「!」と疑問符「?」がそれぞれ全称量化子と存在量化子として用いられている。

*1 同じネタをひっぱり過ぎ


2009-03-07 [長年日記]

λ. 「ご使用のバッテリーでは充電できません。」

「ご使用のバッテリーでは充電できません。」「PCバッテリーの寿命が近づくと、充電する能力が衰えてきます。まもなくプラグを抜いた状態では作業できなくなります。引き続き ThinkPad をモバイルマシンとしてご利用いただく場合は、すぐにバッテリーを取り替えてください。」

最近、どうもバッテリーが一時間くらいしか持たないと思ったら、こんなの出てきた。使い始めてまだ一年くらいしか経っていないのに……ちょっとバッテリーの劣化早すぎない? (泣

Tags: thinkpad

2009-03-08 [長年日記]

λ. 第五十回圏論勉強会@NII

今回は、DEX-SMI Workshop on Quantum Statistical Inference のために来日していた、量子情報の研究者を迎えて、量子情報のセミナーみたいな感じだった。 量子情報やっぱりよくわからんなぁ、面白いけど。

何か話したらという事だったので、「Functional Reactive Programming の事についてでも話すか、これもお絵かきに関係するし」と思ってたのだけど、ちょっとそういう感じでも無かったので、とりあえず Thorsten Altenkirch の A functional quantum programming language (c.f. ヒビルテ(2008-06-30))を拝借して、QMLの紹介などしてみた。*1

ちょっと勿体無かったと思ったのは、量子テレポーテーションのコンパイル例を説明したときに、単に出力された量子回路のテキスト表現だけ見せるのではなくて、QMLから量子回路へのコンパイル - ヒビルテ(2008-08-23) の図を見せれば良かったということ。 あと、発表中ちょっとテンパっていたときに、salmonsnareさんの「まあ、おちつけ。」というtweetがポップアップして、うけた。

それから、記念撮影をしようという話をしてたのに、するのをすっかり忘れていて後悔。

関連


2009-03-16 [長年日記]

λ. 部分継続でDelegateMap

ku-ma-meさんの map が面倒なので DelegateMap を読んで、なんか部分継続(delimited continuation, 限定継続)っぽいなと思ったので、shift/resetで書いてみた。 (shift/reset自体の実装については、call/ccによるshift/resetの表現 - ヒビルテ(2003-05-03)まめめも(2008-04-17) を参照のこと)

module Enumerable
  def dmap2
    # Object.__fcall__(:shift) {|k| map {|e| k[e] } }
    Object.__send__(:shift) {|k| map {|e| k[e] } }
  end
end

p reset { 1 + [1, 2, 3].dmap2 }
#=> [2,3,4]

p reset { 1 + [[1,2], [2,3], [3,4]].dmap2.dmap2 }
#=> [[2, 3], [3, 4], [4, 5]]

まあ、自然言語の「任意の」とかの量化子はまさにこんな感じなので、当たり前といえば当たり前な感じだけど。 参考: “Continuations in Natural Language” by Chris Barker - ヒビルテ (2008-03-13)


2009-03-25 [長年日記]

λ. お菓子補充

お菓子を補充した。しかし、大学芋味のキットカットって……

Tags:

2009-03-29 [長年日記]

λ. 研究室の納会

Tags: tom