日々の流転

λ. PPL2009参加します

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

λ. Maceで数独を解く

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

• 入力ファイル sudoku-mace4.in
• ログ sudoku-mace4.txt

ちなみに、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番目の要素を指す項になっていて、その関係でちょっと注意が必要ということのようだ。

• 入力ファイル sudoku-mace4-2.in
• ログ sudoku-mace4-2.txt

λ. IDPで数独を解く

数独をParadoxとDarwinとMaceで解いてみたので、ついでにIDPでも試してみた*1。

• 入力ファイル sudoku-idp.idp
• ログ sudoku-idp.txt

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

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

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

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

λ. 第五十回圏論勉強会＠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がポップアップして、うけた。

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

関連

• たけをさん
  • 今日は Tokyo Quantum Meeting （圏論勉強会）でした - たけをの日記＠天竺から帰ってきたよ(2009-03-08)
  • TQM 祭りのあと：Pavia大ダリアーノ教授から - たけをの日記＠天竺から帰ってきたよ(2009-03-12)
  • Giulio Chiribellaの講義資料 - たけをの日記＠天竺から帰ってきたよ(2009-03-13)
• hiroki_fさん
  • 圏論勉強会 - hiroki_fの日記(2009-03-06)
  • Tokyo Quantum Meeting(圏論勉強会) - hiroki_fの日記(2009-03-08)
• 圏論勉強会スペシャル：Tokyo Quantum Meeting - 檜山正幸のキマイラ飼育記(2009-03-09) (檜山さん)

λ. 部分継続で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)

λ. お菓子補充

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

λ. 研究室の納会