日々の流転

λ. TODOが溜り気味。とりあえずメールは、適当な言い訳を付けたうえで早めに返事を書かねば。

λ. 新大掃除&席替え

今年は例年に比べてずいぶん手際よく済んだ気がする。

それから、某氏のハブの置き場所が面白かった。ただ、地震とかには弱いかも。

λ. ［地価公示］「都心での反転が地方にも及んだ」

「へぇ」という感想しかないが、土地の価値が正しく評価されるようになり、その上で下げ止まっているのなら、それはまあ望ましいことなんだろう。ただ、政策的後押し、特に「民間の資金とノウハウを活用する新しいタイプの公共事業の推進」というのは良く分からないな。

ところで、土地の有効利用を進めるための政策として、私がすぐに思いつくのは以下のような政策だが……

• 土地譲渡益税の減税
• 土地固定資産税の増税
• 一物四価とか一物五価とか言われる馬鹿げた制度の整理
• 借地借家法の改正
• 容積率規制の緩和

λ. 「東方花映塚」情報 キタ━━━━(゜∀゜)━━━━ッ!!

• 東方花映塚　〜 Phantasmagoria of Flower View.

こりゃまた楽しみだ。

次回作で咲夜さんが消えない事だけを願ってたけど……スクリーンショットに咲夜さんがいるよー。よかったー。よかったよー。これだけでもうかなり満足(ぉぃ。

λ. 『ブギーポップ・デュアル　負け犬達のサーカス』 - 高野真之 (作画)　上遠野浩平 (原案)

微妙。続きを読めば印象変わるかも知れないけど、あまり続きを読む気になれない。ところで、左右非対称な表情の描写を楽しみにしてたのだけど、そういった描写はなかったな。

λ. 入社式

今日から社会人に。 集合時間が朝早かったこともあり、今日は少し疲れた。

λ. スライスのスライスはスライス

Γを圏Cの対象とすると、そのスライスである圏C/Γが定義できる。 さらに、σを圏C/Γの対象とすると、そのスライスである圏(C/Γ)/σが定義できる。

さらに、Cにプルバックが存在するとき、σ^* : C/Γ → C/dom(σ) を id_Γ ∈ |C/Γ| に適用すると、σ^* id_Γ ∈ |C/dom(σ)| と dom(σ^* id_Γ) ∈ |C| が得られる。 dom(σ^* id_Γ) を Γ・σ と書くことにすると、(C/Γ)/σ と C/(Γ・σ) は等しい。

LCCC(locally cartesian closed category, 局所デカルト閉圏)の名前は、全てのスライスがCCC(cartesian closed category, デカルト閉圏)であることからきているが、LCCCにはプルバックがあるので、LCCCのスライスはCCCであるだけでなく、それ自体LCCCになっている。

Categories for Everybody のLCCCの話に関係して小ネタ。

λ. Ninjava meeting “Risk-driven architectural decomposition”

日下部さんから今日渋谷でAlloyの勉強会があると聞いたので行ってみたら、Ninjavaというグループの集まりだった。 Meeting April 2 (Thu) - "Risk-driven architectural decomposition"

• 発表スライド等

話はセキュリティの要件と(セキュリティの側面の)アーキテクチャをAlloyで書いて、詳細化とかしながら、要件を守るために必要な仮定を考えたり、リスクアセスメントをしたりという話。 本題ではないけど、セキュリティに関するデザインパターンであるセキュリティパターン(security patterns)というのがあるらしく、面白そうだと思った。 あと、Alloyにprivateというキーワードがあることを初めて知った。

それから、参加者にポーケン.jpの人がいたので、飲み会でポーケンをゲット。ポーケンはこないだの萩野服部研の納会で知ったばかりだったので驚いた。

それにしてもみんな日本語うまいなぁ。今日の発表者の Thomas Heyman さんとか、日本に来たばかりとはとても信じられん……

λ. Haskellers Meeting 2010 Spring のお知らせ

Haskell 界の大御所 Simon Peyton-Jones さんが、来日します。ご好意で、お話しを聞く機会を設けることができました。日本側からもいくつかの発表をする予定です。東京近郊の Haskell 好きは、全員集合しましょう！

4月16日にこういうイベントがあります。

λ. 「異様に難しいドラクエの謎解き」を整数線形計画問題として解く

「異様に難しいドラクエの謎解き」をモデル検査器で解く の続き。 元の「人生を振り返る - 異様に難しいドラクエの謎解き」に「押す順番はどうでも良くて、四隅のボタンを押す回数の問題でしたね」とあって、この洞察を使えば整数線形計画問題として定式化して、もっとスマートに解けるなぁ、と思った。

整数線形計画問題による定式化

x1, x2, x3, x4 をそれぞれ左上、右上、右下、左下の石を押す回数とすると、最短の手順を求める問題は、以下の最適化問題として定式化できる。

Minimize
  x1 + x2 + x3 + x4
Subject To
  3 + x1 + x2 + x3 ≡ 0 mod 4  (左の像の条件)
  3 + x2 + x3 + x4 ≡ 0 mod 4  (上の像の条件)
      x3 + x4 + x1 ≡ 0 mod 4  (右の像の条件)
      x4 + x1 + x2 ≡ 0 mod 4  (下の像の条件)
  x1, x2, x3, x4 ≧ 0
  x1, x2, x3, x4 ∈ Z

追加的な変数を導入してmodを取り除けば、これは整数線形計画問題になる。その結果の問題をLPファイル形式にすると以下ようになる(baroque_tower.lp)。

Minimize
  x1 + x2 + x3 + x4
Subject To
  c1: x1 + x2 + x3 - 4 n1 = -3
  c2: x2 + x3 + x4 - 4 n2 = -3
  c3: x3 + x4 + x1 - 4 n3 = 0
  c4: x4 + x1 + x2 - 4 n4 = 0
Bounds
  0 <= x1
  0 <= x2
  0 <= x3
  0 <= x4
  0 <= n1
  0 <= n2
  0 <= n3
  0 <= n4
General
  x1 x2 x3 x4 n1 n2 n3 n4
End

MIPソルバで解いてみる

これをMIPソルバのlpsolveを使って解かせてみる。

> lp_solve.exe -rxli xli_CPLEX.dll baroque_tower.lp
set_XLI: Successfully loaded 'xli_CPLEX.dll'

Value of objective function: 6.00000000

Actual values of the variables:
x1                              1
x2                              2
x3                              2
x4                              1
n1                              2
n2                              2
n3                              1
n4                              1 

ということで、(x1,x2,x3,x4)=(1,2,2,1)という最適解が得られ、これは左上を1回、右上と右下を2回ずつ、左下を一回という、前回得られたものと同じ解が得られる。

実は最初はGLPKでも解こうと思ったけれど、GLPKだと、有界でない整数変数のせいで無限にブランチして止まらないっぽい。各変数に適当な上界を加えれば解ける。 あと、自分が以前に書いたオモチャのMIPソルバでも楽勝で解けた。

最適解の一意性

最適解の一意性については、MIPソルバを使うよりも、論理結合子を自由に使えるSMTソルバの方が便利なので、SMTソルバのZ3で確認してみることにする。

以下の内容(baroque_tower.smt2)をZ3に与える（オンラインでも Z3 online at RiSE4Fun で試せる）ことで、6手の他の解が存在しないことを確認できる。 詳しくは以下のコメント中にて。

; baroque_tower.smt2
(set-option :produce-models true)
(set-logic QF_LIA)

; 変数の宣言
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(declare-fun x3 () Int)
(declare-fun x4 () Int)

; 前述の制約条件の追加
(assert (>= x1 0))
(assert (>= x2 0))
(assert (>= x3 0))
(assert (>= x4 0))
(assert (= (mod (+ 3 x1 x2 x3) 4) 0))
(assert (= (mod (+ 3 x2 x3 x4) 4) 0))
(assert (= (mod (+ x3 x4 x1) 4) 0))
(assert (= (mod (+ x4 x1 x2) 4) 0))

;; まずは適当に解を求めてみる
(check-sat)
; sat と出力され、解が存在することが分かるので、解を表示させる
(get-value (x1 x2 x3 x4))
; ((x1 1)
;  (x2 4946)
;  (x3 4990)
;  (x4 9749))

;; 既に最適解での目的関数値が6と分かっているので、その条件を加えて再度解いてみる  
(assert (= (+ x1 x2 x3 x4) 6))
(check-sat)
; 今度もsatと出力され、解が存在することが分かるので、 解を表示させる
(get-value (x1 x2 x3 x4))
; ((x1 1)
;  (x2 2)
;  (x3 2)
;  (x4 1))

;; 更に、今見つかった最適解を除外する制約を加えて、再度解いてみる
(assert (not (and (= x1 1) (= x2 2) (= x3 2) (= x4 1))))
(check-sat)
; 今度はunsatと出力され、従って今除外された以外の解がないことが分かる

関連リンク

• 『「異様に難しいドラクエの謎解き」をモデル検査器で解く』代わりに数学で解く - Elliptium

ひょっとしたら関係するかもしれない書籍など