日々の流転

λ. 新聞記事の展示は上映権の侵害?

展示会などで新聞記事の展示をすると上映権の侵害になるという話を先日耳にしたが、著作権法第二条(定義)で以下のように定義されているのだから、少なくとも上映権ではないのではないかと思った。

十七　上映 著作物（公衆送信されるものを除く。）を映写幕その他の物に映写することをいい、これに伴つて映画の著作物において固定されている音を再生することを含むものとする。

あと、可能性のあるのは展示権ではないかと思ったが、明らかに原作品ではないし、

（展示権） 第二十五条　著作者は、その美術の著作物又はまだ発行されていない写真の著作物をこれらの原作品により公に展示する権利を専有する。

λ. 天井裏のハチの巣

以前にアブが大量発生した我が家。天井を開けたら今度はミツバチの巣が。おいしそうに見えるが、殺虫剤を撒いてしまったので、蜂蜜は食べられない。

【追記】 取り外したらこんな感じに。やっぱりおいしそうだ……

λ. Google Code Jam 2009 Qualification Round

Google Code Jam には参加してないけど、どんな問題が出てるのかなと気になったので、試しに解いてみた。 Qualification Round だったからか、特に難しい問題は無かった。 Aは普通に。Cも普通にDP。少し面倒だったのがB。 一度各セルから水の流れる先のシンクへの写像を定義して、それから北西から順にセルを辿りながら、対応するシンク(に代表される同値類)にアルファベットを割り当てるという風にしたが……

• A.hs
• B.hs
• C.hs

λ. 天井裏から発見されたスズメバチの巣

ミツバチの巣に加えて、スズメバチの巣も天井裏から発見された。スズメバチは巣を一年しか使わないそうで、これは何年か前の巣らしい……

λ. Google Code Jam 2009: Round 1A

参加はしてないけど、また解いてみた。 Qualification Round は楽勝な感じだったけど、今回はさすがに難易度があがってるのね。 私には二時間半の時間内に全問解ける気がまるでしない……

A. Multi-base happiness

素朴に、各基底に対してその基底でハッピーな数の集合を昇順の無限リストとして定義しておいて、それらの共通部分の最初の要素として解を定義した。 Largeは数分かかってしまったけど、なんとか解けた。 基底に対するハッピーな数の集合だけじゃなくて、基底の集合に対する解の集合も再利用するようにすれば、テストケースを越えて計算を共有できて、Largeももっと速くなるかなぁ。

• A.hs

B. Crossing the Road

「Project Euler の Problem 15 をちょっと面倒にしたようなものか。これならDP一発で楽勝」と思って解いたら、サンプルは通るけど B-small-practice.in をパスしない。 数時間悩んで*1、ようやく南から北、西から東だけでなく、北から南、東から西へ移動することで時間が短縮できる場合(B-small-practice.in だと Case #5 と Case #6)があることに気づく(死亡確定)。 仕方がないので、後から逆向きも見て小さいほうを選ぶというのを収束するまで繰り返すようにした。ちょっとどうかと思ったが、一応Largeでも一瞬で解けたのでよしとする。

• B.hs

C. Collecting Cards

確率とか私には無理すぎる。 立てた式が間違っていて、何故答えが合わないのか数時間*2悩んでしまった(死亡確定)。 確率についてはもう少し慣れておくべきと思った。

• C.hs

λ. Google Code Jam 2009: Round 1B

参加はしてないけど、Qualification Round と Round 1A に続いてまたプラクティスを解いてみた。 やっぱり、二時間半の時間内に全問解ける気がまるでしないなぁ……

A. Decision Tree

簡単。 特に工夫は不要で、書いてあるとおりにやるだけで何の問題もなかった。

• A.hs

B. The Next Number

数字がすべて降順に並んでいたら繰り上がり。 そうでなかったら、降順になっていない最短のサフィックスを持ってきて、ごにょごにょ。 こういう、単純だけど落ち着いて考える必要がある問題っていいよね。 落ち着いて考えればそんなに難しくはないけど、実際に参加して解いていたら、焦って時間内に解けなかったと思う。

• B.hs

C. Square Math

かなり手間取った。時間内には絶対解けなかったと思う。 望ましい解き方がわからなかったので力技で書いたら、C-small-practice.in はすぐに処理が終わるけど、C-large-practice.in は数十分かかることに……orz　なんか、賢い解き方があるんだろうけどなぁ……

• C.hs

【2009-09-23 追記】 ちゃんと考えて解きなおした。 といっても、特に工夫はしてなくて、ただのDFSだけど。 そしたら、C-large-practice.in でも一分程度で終わるようになった。

• C2.hs

λ. 第五十六回圏論勉強会

今日は圏論勉強会。 写真

P. Selinger, “A survey of graphical languages for monoidal categories”の 5 Traced categories の最初から 5.5 Braided traced categories の途中まで。

Some notes on monads. Andrea Schalk

λ. Google Code Jam 2009: Round 1C

Round 1B に続いて、またプラクティスを解いてみた。 今回は初めて時間内に全問解けた*1。やったー!

(追記: やったー！と思ったが、ルールをちゃんと見たら、Largeは入力データをダウンロードしてから8分間だけしかsubmit出来ないのね。なら、CのLargeはアウトだったなぁ。残念。)

A. All Your Base

基本的には現れた文字の数をベースにして、最上位の文字に1、残りの文字は上位の桁に表れる数字から小さいに順に数字を割り当てていくだけ。 で、楽勝と思ったら、unitaryでないという注意を見落としててIncorrect食らった(A-small-practice.in だと Case #12 と Case #32 がこの影響を受ける)。 これ絶対狙ってる引っ掛けだよなぁ。

• A.hs

B. Center of Mass

複数の蛍のデータが与えられているけど、実際にはその平均の座標と速度だけ考えればいい。 あとは、中学数学で二次関数の最小値を求めるだけ。 なんだけど、最小になる時刻を求めるときに式の両辺を割っていたのを忘れてて距離の最小値の計算結果が合わず悩んだり、速度が0のときを忘れててIncorrect食らったりした。

• B.hs

C. Bribe the Prisoners

最初、空でないセルの区間をキーにしてメモ化して書いた。 そしたら、C-small-practice.inはすぐに解けたけど、C-large-practice.inがとても終わらなかった。 そこで、「区間ではなくパターンをキーにメモ化するようにしたら、違う区間で同じパターンが現れたときも計算を共有できて速くなるかな」とか思って適当に書き換えてみたら割とすぐ終わるようになった。

• 最初に書いたやつ C.hs
• 書き換えたやつ C2.hs

λ. tDiaryがIconv.convの呼び出しなどで落ちる

サーバーのRubyのバージョンがあがったら、tDiaryがIconv.convの呼び出しなどで落ちる。 こりゃ環境がおかしいのかと思ったら、Rubyのバグとのこと。 amazon.rb を使用して日記を更新するとRubyがSEGVる の現象と同じ。 最新版ということで ruby-1.8.7-p174 で試しても落ちたので、安定版スナップショットをいれたら、直った。

amazon.rbがSEGVする件 - 忘れたときに備えた記録(2009-05-06) の「あなたのRubyがamazon.rbでSEGVするか調べるワンライナー」が参考になった。

λ. 推移閉包が一階述語論理で表現できないことの証明

推移閉包が一階述語論理で表現できないことについて何度か書いたけど、最近になって“First-Order Logic as a Lightweight Software Specification Language - The ETPTP Toolkit”(Michel Rijnders)で、どうやって証明するかを知った。

二項関係 T が二項関係 R の推移閉包であることを論理式 φ によって表現できると仮定して、矛盾を導く。まず、

• σ₀ = ￢R(a,b)
• σ_n+1 = ∀x₁,…,x_n+1. ￢(R(a,x₁)∧R(x₁,x₂)∧…∧R(x_n, x_n+1)∧R(x_n+1,b))
• Σ = {σ_n | n∈N }
• Γ = {φ, T(a,b)}∪Σ

と定義する。 すると、 Γ の任意の有限集合 Γ' は( σ_n∈Γ' であるような任意の n よりも2以上長いパスによって)充足可能なので、コンパクト性定理により Γ も充足可能なことが言える。 しかし、実際には Σ 全体は a から b へ到達不能であることを主張しているので、 Γ は充足出来ない。 これは矛盾なので、背理法よりこのような論理式 φ は存在しない。

コンパクト性定理って、あまり応用を知らなかったけど、こういう使いでがあるのね。便利だ。

関連

• 推移閉包は一階述語論理では表現できないのね - ヒビルテ(2007-12-10)
• 推移閉包が一階述語論理では表現できないことをAlloyで確認する - ヒビルテ(2009-07-14)

λ. 有限領域での推移閉包の公理化

昨日も書いたように、推移閉包は一般には一階述語論理では表現できないので、領域を有限に限定した場合でも領域のサイズの上限 n に依存した形、たとえば以下のような形でしか表現できないと思い込んでいた。

• ∀x,y. T_k(x,y) ⇔ R(x,y) ∨ σ₁ ∨ … ∨ σ_n-2
• where σ_n := ∃z₁,…,z_n. R(x,z₁) ∧ R(z₁,z₂) ∧ … ∧ R(z_n-1,z_n) ∧ R(z_n,y)

Automating First-Order Relational Logic なんかでも、「The transitive closure is obtained by applying an operator that computes closure using iterative doubling, as explained in [15].」と、もう少し賢いけれども、やはり領域のサイズの上限に依存した形を使うとあったし……

だけど、これは誤りで、昨日も言及した“First-Order Logic as a Lightweight Software Specification Language - The ETPTP Toolkit”(Michel Rijnders) によると、モデル発見器 Paradox の作者の Koen Claessen が、(有限領域の場合の)領域のサイズに依存しないような形式化を考えた*1そうだ。 この論文では反射推移閉包の場合で説明していて、関数記号 s と関係記号 C を新たに導入して、以下のような公理を導入する。

• (I1) ∀x. T(x, x)
• (I2) ∀x, y. R(x, y) → T(x, y)
• (I3) ∀x, y, z. T(x, y) ∧ T(y, z) → T(x, z)
• (E1) ∀x, y. T(x, y) ∧ x ≠ y → R(x, s(x, y))
• (E2) ∀x, y. T(x, y) ∧ x ≠ y → T(s(x, y), y)
• (C1) ∀x, y. ￢C(x, x, y)
• (C2) ∀x, y, z, v. C(x, y, v) ∧ C(y, z, v) → C(x, z, v)
• (E3) ∀x, y. T(x, y) ∧ x ≠ y → C(x, s(x, y), y)

説明されてみれば「なるほど」と思うのだけど、こんな方法があったのかと感動した。 Koen Claessen すげー

本当に出来ているか Alloy で確認する

本当に反射推移閉包を公理化できているか、例によってAlloyで確認してみる。

まずは上記の公理をAlloyで書いてみる。今回はちょっとAlloy風に書いてみた。

sig U {
  R : set U,
  T : set U,
  s: U -> one U,
  C: U -> U
}
fact {
  all x : U | x in x.T
  R in T
  T.T in T
  all x : U, y : x.T | x!=y => (s[x,y] in x.R and y in s[x,y].T)
  all x, y: U | not (x->x in y.C)
  all v : U | (v.C) . (v.C) in v.C
  all x : U, y : x.T | x!=y => x->s[x,y] in y.C
}

pred show() { }
run show

assert T_is_RTc_of_R {
  all x : U | x.T = x.*R
}
check T_is_RTc_of_R for 6

それで、「run show」を実行すると、

Executing "Run show"
   Solver=minisat(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   939 vars. 75 primary vars. 1308 clauses. 34ms.
   Instance found. Predicate is consistent. 19ms.

というような感じで、反射推移閉包になっている例が出てくる。 Nextを押して更に幾つか例を作ってみても、どれも反射推移閉包になっているっぽい。

それならばと、今度は「Check T_is_RTc_of_R for 6」を実行すると、

Executing "Check T_is_RTc_of_R for 6"
   Solver=minisat(jni) Bitwidth=4 MaxSeq=6 SkolemDepth=1 Symmetry=20
   7640 vars. 516 primary vars. 12305 clauses. 136ms.
   No counterexample found. Assertion may be valid. 617ms.

という感じで、6要素までの領域では確かに反射推移閉包になっているようだ。

さらに、SATソルバーとして「Minisat with Unsat Core」を選択して、「Check T_is_RTc_of_R for 6」を実行すると、今度は Core というのが出てきて、以下のようにソースがハイライトされる。 ハイライトされている部分は、ここから論理式をひとつでも取り除いたら、反例(TがRの反射推移閉包になっていない例)が発見できてしまうような論理式の集合を表している。 この場合には公理全体が含まれているので、どの公理もTがRの反射推移閉包であることを表現するのに欠かせない公理であることがわかる。

λ. ICFP Programming Contest 2009 の順位

ICFP Programming Contest 2009 の Final Position List at End of Contest が出ていたとか。 Team Sampou のスコアはコンテスト終了時に書いたように 1002.1329 (8 problems solved) で、順位は 328 チーム中 165 位だった。 うーん。来年こそはもっと上位に行きたいものだ。

• 参考: ICFP Programming Contest 2008 の結果

λ. “First-Order Logic as a Lightweight Software Specification Language - The ETPTP Toolkit” by Michel Rijnders

面白かったのは以下の日記で書いた点。

• 推移閉包が一階述語論理で表現できないことの証明 - ヒビルテ(2009-09-15)
• 有限領域での推移閉包の公理化 - ヒビルテ(2009-09-16)

λ. Introduction to Categorical Programming

Haskell Annual Meeting Autumn.jp 2009 (Hama.jp 2009) で、CPL とか Haskell での Categorical Programming の紹介をしたのだけど、テーマを絞りきれなかったのと、準備が間に合わなかったので、かなりグダグダな感じに。

このままというのはあんまりだと思ったので、修正版の資料を作成した。テーマが絞れていないという、根本的な問題は直ってないので、あまり変わらないけど……

資料(修正版)

ダウンロード(PDF)

資料(当日版)

ダウンロード(PDF)

参考資料や関連情報など

• Categorical Programming Language
• Categorical programming with inductive and coinductive types
  • ヒビルテ (2004-06-29)
• The Evolution of a Haskell Programmer
• CPLの処理系のダウンロード
• ヒビルテ [CPL]
• primrecの再帰を使った定義とiterを使った定義の等しさを QuickCheck で確認 (nwnさん)

その他 HAMA.jp 関係

• ログ
• Type level programming in Haskell (keigoiさん)
  • ustream.tv
• Haskellで圧縮 (smlyさん)
• #HAMA - Twitter Search
• nono weird science : HAMA.jp

λ. ルービックキューブ

ルービックキューブを解いていたら、以下の写真のようになってしまった。 中央のマスの向きが合わなくても、絵柄はそろうんだなぁ。

λ. 誕生日

age <- arr (+1) -< age

λ. CPLに関数定義を導入

CPLのHaskell実装に久しぶりに手を入れて、関数定義を導入した。 これで、

let uncurry(f) = eval . prod(f, I)

とか

let primrec(f,g) = pi2.pr(pair(0,f), pair(s.pi1, g))
let fact = primrec(s.0, mult.prod(s,I))

とか、書けるようになった。

あとはIOをどうにかして導入すれば、変態言語として使えるようになるかな。 しかし、久しぶりにソースをいじると、昔の自分のコードがひどすぎて、一から書き直したくなるなぁ。

λ. 焼肉

大学時代からの友人と焼肉など。 肉の万世に多分初めて行った。

λ. 『自由と繁栄の弧』 by 麻生 太郎

読了。

書き下ろしのもの以外は元になった演説等がWeb上で閲覧できる。

• 外務省: 外務大臣演説 (麻生外務大臣)
• 靖国に弥栄（いやさか）あれ - 麻生太郎オフィシャルウェブサイト

λ. カレー

λ. 栗ご飯

栗ご飯おいしい。

λ. PLDIr #2

(書きかけ)

PLDIの論文を読む PLDIr の第二回に参加。 15:00開始で21時くらいまでやっていた。

今回はPLDI98の論文が対象で、私は以下の2本の論文を紹介した。

• Run-time code generation and modal-ML
• Improving performance by branch reordering

スライド:

しかし、みんな Citation Count とか、後日談とか、著者たちの動向とかちゃんとフォローしていて偉いな、と思った。 見習おう。