日々の流転

λ. 『整理HACKS!—1分でスッキリする整理のコツと習慣 』 小山 龍介

読了。 この手のHACKS本にはあまり興味を持っていなかったが、いくつかは参考になりそうなものがあったので読んで良かった。

04 ドキュメントスキャナーでデジタルデータに変換する

前々から欲しかったのだけど、ScanSnap買おうと思った。

06 SugarSyncで「どこでもオフィス」を実現する

SugarSyncは知らなかった。Dropboxに似ているけど、主な違いは任意のフォルダを同期できることと、iPhoneアプリが既にあること。結構いいかも。無料版が2GBだけど、上の紹介リンクからアカウントを作ると+500MBボーナス。

WebインターフェースはDropboxの方が全体的に使いやすいと思った。ダウンロードするときにファイル名の非ASCII文字が化けたりもするし。

iPhoneアプリは使いやすい。 ただ、音楽の再生機能があるからだと思うが、起動時にiPodで再生中の音楽を停めてしまうのは、ちょっと困り者だと思うけど。

30 IMEバーは上端中央に置く

「おお、これはいい」と思ったんだけど、Chromeのウィンドウを最大化すると、ちょうどタブと重なってしまう。

40 RSSリーダーで情報収集を仕組み化する

紹介されていた、Google Reader と動機できるiPhone用のRSSリーダーのFeedsを購入した。 同種のものには、Bylineというのもあるらしいが、どっちがよいのだろう。

52 通販を活用して生活をシンプルにする

文房具等の通販をしているぽちっとアスクルは知らなかった。 今度使ってみよう。

73 マインドマップを使って情報のネットワークをつくる

そういえば、「マインドマネージャ」は勝間本でも紹介されてたな。

85 個人のオリジナル名刺をつくる

名刺作成サービスのアイボスは今度使ってみようと思った。

λ. 『洗脳原論』 苫米地 英人

読了。

λ. 江ノ島花火大会

エンドレスエイトで延々と「夏は夏らしく夏じみたことを」と言っているのを見て、なんとなく夏っぽいことをしようと思ったりして、なんとなく花火を見に行くなどしてみた。 といっても、人ごみの中には行きたくなかったので、遠くからだけど。しかし、花火の写真を撮るのは難しいな。

hanabi.mp4

λ. “New Techniques that Improve MACE-style Finite Model Finding” by Koen Claessen and Niklas Sörensson

以前に、一階述語論理のモデル発見器であるParadoxを使って、数独を解いてみたりしたが、Paradoxの実装に使われている性能を改善するためのテクニックを説明した論文。 Paradoxの使っているテクニックだけでなく、その前提となる一階述語論理の有限モデルをSATソルバーを使って解くための基本的な手法についても分かりやすく書かれている。

splitting

splittingというのは、例えば { P(x, y), Q(x, z) } という節を、新しい述語 S を導入して、

• { P(x, y), S(x) }
• { ￢S(x), Q(x, z) }

という節集合に分割することを指す。

splitting をすることによって、個々の節に含まれる変数を減らすことが出来る。 節のインスタンス化(= 基礎化(grounding)?)の際に、節の数が変数の数の指数オーダーで膨れ上がるので、節に含まれる変数の数を減らすのは非常に重要。

splittingのためのヒューリスティックは色々あるが、これまでのはあまり良くなかった。 そこで、Paradoxで採用しているのは「述語をノード、述語のリテラルが変数を共有するという関係をエッジとするようなグラフを考え、その最小の連結成分をsplittingによって分離する、ということを繰り返す」というもの。

term definition

ひとつの目の新しいテクニックは、節に含まれる変数を減らすための term definition 。

例えば、{ P(f(a, b), f(b, a)) } を普通にフラット化すると、4つの変数を含む節 {a ≠ x, b ≠ y, f(x, y) ≠ z, f(y, x) ≠ w, P(z,w)} になってしまうけど、新しい定数記号t1,t2を導入して

• { t1 = f(a, b) }
• { t2 = f(b, a) }
• { P(t1, t2) }

という節集合に変換しておくと、フラット化したときに、

• { a ≠ x, b ≠ y, f(x, y) ≠ z, t1 = z }
• { a ≠ x, b ≠ y, f(y, x) ≠ z, t2 = z }
• { t1 ≠ x, t2 ≠ y, P(x, y) }

という、各々の節が3変数しか含んでいないような節集合に出来る。

increamental SAT

二つ目の新しいテクニックは、SATソルバーのインクリメンタルな機能の活用。 MACEスタイルの方法では、モデルのサイズnを増やしながら、サイズnのモデルの探索をSAT問題に落として、SAT solver に解かせる。これまではこれを毎回一からSATソルバーにかけていたが、SATソルバーのインクリメンタルな機能を使うことで、サイズnでの探索で得られた情報(特に conflict learning の結果)をSATソルバーがその後の探索で利用でき、探索を効率化出来る。

これをするにはSATへのエンコーディングを少し工夫する必要がある。

static symmetry reduction

三つ目の新しいテクニックは、同型なモデルを排除するような制約を制的に導入すること。 SEMのように自分で探索をする場合には探索を進めながらゴニョゴニョできるけど、SATソルバーを使うので探索を始める前に制約を静的に与えておかなくてはいけないのが難しい。

定数記号 {a_i}_i について考えると、I(a_i)≦i すなわち

• { a₁ = 1 }
• { a₂ = 1, a₂ = 2 }
• { a₃ = 1, a₃ = 2, a₃ = 3 }
• …

という節集合によって値域を制限し、さらに 1 < i ∈ D と 1 < d ≦ i について、

• { a_i≠d, a₁ = d-1, a₂ = d-1, …, a_i-1 = d-1 }

という節を導入することで、a_iの値をa₁,…,a_i-1で使われている値か、もしくはa₁,…,a_i-1で使われていない値のうちの最小のものに限定する。

関数記号がある場合についても同様だが、この場合には同型なモデルを完全に排除することは出来ない。

sort inference

四つ目の新しいテクニックはソート(型)の推論。 ソートの推論をすることで、ソート単位で symmetry reduction が出来るようになり、より細かい symmetry reduction が出来るようになる。 具体的な型推論は、関数(の引数と返り値)と述語(の引数)がすべて異なるソートを持つと仮定して、それから同じ変数が使われているところのソートを同じにしていくという、普通の方法でやっている。

λ. ぼんぼり祭

「夏は夏らしく夏じみたことを」ということで、今度は鶴岡八幡宮のぼんぼり祭に行ってみた。 ぼんぼりに灯をつけてまわる巫女さんに萌えるなどする。

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

今日は圏論勉強会。

P. Selinger, “A survey of graphical languages for monoidal categories”の 4 Autonomous categories の残り。4.2 (Planar) pivotal categories から 4.8 Compact closed categories まで。

4.3 Spherical pivotal categories の Failure of coherence が良くわからなかった。 下の図の真ん中と右の図が2次元の球面でisotopyで同一視されないというのはいいのだけど、左と真ん中の図もそうなの?

4.5 Braided autonomous categories 。 タングルとリンクの3次元isotopyは、平面に射影したときの planar isotopy にライデマイスター移動を追加したものに等しくて、そこからライデマイスター移動Iを除いたものが regular isotopy というあたりに、なるほどと思う。

4.6 Braided pivotal categories の、「On the other hand, the equation (中略) holds up to isotopy, but not up to regular isotopy (because regular isotopy preserves total curvature, as pointed out by Freyd and Yetter [9, p. 169]).」で、Total curvature って捩れのことかと思ったら、違った。Total Curvature - Wikipedia

4.8 Compact closed categories の、自明でないtwistの例で、部分圏C_〜 に制限している理由がよく分からなかった。

λ. 数学基礎論サマースクール 2009 一日目

「夏は夏らしく夏じみたことを」ということで、数学基礎論サマースクール2009に参加。

masahiro_sakaiによる数学基礎論サマースクール実況まとめ - yoriyukiの日記

後で書く。

λ. 数学基礎論サマースクール 2009 二日目

masahiro_sakaiによる数学基礎論サマースクール実況まとめ - yoriyukiの日記

後で書く。

λ. 数学基礎論サマースクール 2009 三日目

masahiro_sakaiによる数学基礎論サマースクール実況まとめ - yoriyukiの日記

後で書く。

関連

• 数学基礎論サマースクール2009 - とりマセ(2009-08-13)

λ. “The IDP framework for declarative problem solving” by Maarten Mariën, Johan Wittocx, and Marc Denecker

以前2009-03-04に数独を解いてみたIDP(Inductive Definition Programming)フレームワークの解説。背後にあるロジック、記述言語、動作例が中心で、ソルバーの仕組みにはあまり触れていない。

IDPの背後にあるロジックは、ソート付きの一階述語論理を帰納的定義で拡張したもので、問題は「指標Σ, セオリーT, 部分指標σ⊆Σ, 有限のσ構造A_Iの組〈Σ, T, σ, A_I〉が与えられたときに、A_Iの拡張で(A|_σ = A_I)、Tを満たす(A ⊨ T)ようなΣ構造Aを求める」というモデル拡張問題(model expansion problem)として形式化される。

また、問題の記述スタイルとしては、問題の一般的なルールをΣとTによって記述し、具体的な盤面など問題のインスタンスに固有の情報をA_Iで与えるというスタイルになっているのが面白い。

実装については以下のように書いてあった。

Its algorithms consist of an adaption of the DLL algorithm to rules, augmented with a variant of Smodels' AtMost. As such, the solver incorporates techniques from state of the art SAT and ASP solvers.

読んでると、解集合プログラミング(Answer Set Programming, ASP)との比較をかなりしている一方で、MaceやParadox等の一階述語論理のモデル発見器(model finder)については全く言及してなくて、ちょっと意外な感じがした。 ASPは最小エルブランモデルの一般化であるところの解集合を求めるので、ある意味全体が帰納的定義になっている一方で、一階述語論理のモデル発見器は帰納的定義が出来ないので、比較対象としてはASPの方が適当ということなのかな。 ただ、ASPが項をエルブラン宇宙で解釈するのに対して、IDPは一階述語論理のモデル発見器は任意の解釈をするので、実装的には一階述語論理のモデル発見器に近い部分もあると思うし、帰納的定義の追加による性能への影響とかも気になることは気になる。

それから、ちょっと気になったのは、以下の部分。

A historical AI argument (e.g. [15]) against FO as a computational logic is the semi-decidability of the deduction problem (and worse, undecidability in the case of FO(ID)).

一階述語論理FOがsemi-decidableなのはいいんだけど、一階述語論理に帰納的定義を加えたFO(ID)がundedidableというのはホント?　一階述語論理と同様に証明を枚挙して証明チェッカにかけるという方法は使えないのだろうか?

λ. お墓参りなど

家族でお墓参り。渋滞にはまってウンザリ。あと、やっぱり暑い。 お昼は、竹治(たけはる)というところで、まぐろ重なるものを食べた。

それから、プールでひと泳ぎし、夜は帰省した友人らと飲み会。 はじめて飲み会後にラーメン屋にいくなど。

λ. RubyKaigi2009の記念バック壊れた

RubyKaigi2009の記念バックのハトメがとれてしまった……悲しい。

λ. iTunes Card 初購入

昨日はファミマのiTunes Card 20%OFF！キャンペーンで買おうと、近所数箇所のファミマに行ったが、在庫無しだったり、取り扱いがなかったりで、購入できなかった*1が、今日ようやく入手。 iTunes Card 買うのは初めてで、コインで銀色のスクラッチを削るのが、なんだか懐かしかった。

λ. 東京タワーなど

東京タワー。お盆中とはいえ、やっぱり人多いなー。 売店で東京タワー型のミネラルウォーターが売っていて、面白かった。 それから、ディナークルーズに。

λ. 靖國神社参拝など

「夏は夏らしく夏じみたことを」ということで、靖國神社に参拝してきた。 終戦記念日だったので、神社周辺は色々な団体が演説やビラ配りをしていて、警官も沢山いたりと、かなり物々しかったが、神社の中は普通の人が普通に参拝している様子で、それを見てなんとなく安心した。 しかし、去年2008-08-17に参拝したときと違って、人が無茶苦茶沢山いた。去年は終戦の日でなかったし、雨も降ってたからなぁ。 今年もまた遊就館を見てきた。

帰るときにはちょうど周辺の団体が撤収中で、なんだかコミケから撤収するサークルみたいだな、などと思った。帰りにはサマーウォーズを見に行こうと、席をネットから予約しようとしてたのだけど、ちょうど売切れてしまって席が取れなかったので、諦めて帰る。

λ. サマーウォーズ

後で書く。

λ. Yahoo! Know Your Mojo!

流行っているようなので、@masahiro_sakaiで試してみたら、Wallflowerだった。 うーん、Wallflowerかぁ……

λ. GabaでLevel 6のLPAを受けた

今日はgabaで Level 6 のLPA(Learning Progress Assessment)というのを受けてきた。わたしは、どうも間接話法(reported speach)が苦手のようだが、他には特に問題なし。 終了後にインストラクタの人と記念撮影もしたのだけど、記念撮影するなら、初めてのインストラクタじゃなくて、いつも受講しているインストラクタを選択して、LPAを受ければよかったな。

λ. Real World Haskell読書会 2009-08

衆院選の期日前投票を済ませてからRWH読書会に参加。 今回は6章「型クラスを使う」から7章「入出力」の7.2「ファイルおよびハンドルを使う」まで。型クラス周りはHaskell98に対する色々な拡張があるので、それらの関係がやはりややこしいと思った。 それから、6.9「重複インスタンスのないJSON型クラス」のmapEitherはmapMを使えばいいじゃんと思ったが、モナドはまだ出てきてないのだった。が、その割にはControl.Arrowのsecondを使っていたりして、なんというか……

• Chapter 6. Using Typeclasses (原著オンライン版)
• Chapter 7. Input and output (原著オンライン版)
• 前回

λ. 東方紅○○

λ. LLTV

プログラムを事前にチェックしてなかったので、Language Update がなかったのにビックリした。 プロトタイピングの話が面白く、その場でIDEOの本を注文した。 LTはいつも通りのノリだったが、全体的にはどうも熱気にかけたという印象。

プレゼントで「AWKを256倍使うための本 (Ascii 256倍)(志村 拓/鷲北 賢/西村 克信)」と「ゼロから学ぶ!最新データベース (日経BPパソコンベストムック)(日経ソフトウエア編集)」を頂きました。わーい。

終了後は、不思議な集団で土木土木という不思議なお店へ。 その日はお祭りだったとかで、目当てのジンギスカンはなかったけど、その代わり秋刀魚が食べ放題だった。おいしかった。

λ. 未来言語Alloy

FLTV(Future Language TV)でAlloyについて発表しました。

発表資料 (PDF):

使用したファイル:

• grandpa.als
• sudoku.als
• minilifegame.als

ustream:

他の発表については FLTVの当日のまとめ - Yet Another Ranha を参照。

λ. Future Language TV 感想

感想等についてはこちらに。 (書きかけ)

11:00ちょっと前に着いたら数人しかいなくて驚いたw 自己紹介などして、11:30からヤドカリの人の「真っ黒Scheme」の発表開始。「かいじょう」で変換してSchemeの階乗プログラムが出てくるのに笑った。

natsutanさんの「未来のハードウェア言語」については、仕事柄色々耳にする話ではあったが、SystemVerilogの乱数周りなどの仕様のなんでもありっぷりなどは全く知らなかったので、面白かった。 ソフトウエアとハードウェアはConcurrencyの意味が違うのも、意識していなかったのでなるほどと思った。ソフトウェアで単にConcurrencyといったら非同期的(Asynchronious)なものだけど、ハードウェアだと同期的(Synchroneous)なもの。 Bluespecは昔Haskell風の構文だったころは興味あったんだけどねぇ。(参考: Lightweight Language Spirit - ヒビルテ(2007-08-04))

朝は平気だったのに、途中から鼻水が止まらなくなって困った。 が、自分の番で発表をはじめたら嘘のように止まって、発表終わっても鼻水が復活することはなかった。

m0h1canさんのドリクラ貧乳名刺をゲット。

kinabaさんの「レトリカル・プログラミング」は、Chris Barker の Continuations in Natural Language の話がその後も進んでるのを知れて良かった。 “Wild Control Operators”のスライドどっかに落ちてないかなぁ、と思ったが、見つからなかった。残念。

λ. Agda2でクイックソート

LLTV後の飲み会でranhaさんが、クイックソートの停止性をAgda2の停止性チェッカに説得できないというような事を話していた(参考: 修行失敗 - Yet Another Ranha (2009-08-27))ので、Agdaさんを説得してみた。 基本的には length (filter p xs) ≦ length xs の証明 と Wellfounded induction in Agda2 で書いたのを組み合わせただけなんだけど、Agda2のライブラリの使い方を調べるのが面倒くさかったよ……

module Quicksort where

open import Data.Bool
open import Data.Nat
open import Data.List
open import Relation.Binary using (Rel)
import Induction.WellFounded as WF
open WF using (Acc; acc)
open WF _<′_ using () renaming (Acc to <-Acc)
open import Induction.Nat using (<-allAcc)

R : ∀ {A} → Rel (List A)
R {A} xs ys = length xs <′ length ys

R-allAcc : ∀ {A} xs → Acc (R {A}) xs
R-allAcc xs = f xs (<-allAcc (length xs))
  where
    f : ∀ xs → <-Acc (length xs) → Acc R xs
    f xs (acc rs) = acc (λ ys h → f ys (rs (length ys) h))

s≤′s : ∀ {m n} → (m ≤′ n) → suc m ≤′ suc n
s≤′s ≤′-refl = ≤′-refl
s≤′s (≤′-step h) = ≤′-step (s≤′s h)

length-filter
  : ∀ {A} → (f : A → Bool) → (xs : List A)
  → length (filter f xs) ≤′ length xs
length-filter f [] = ≤′-refl
length-filter f (x ∷ xs) with f x
... | true  = s≤′s (length-filter f xs)
... | false = ≤′-step (length-filter f xs)

length-filter′
  : ∀ {A} → (f : A → Bool) → (x : A) → (xs : List A)
  → length (filter f xs) <′ length (x ∷ xs)
length-filter′ f x xs = s≤′s (length-filter f xs)

quicksort′
  : ∀ {A} → (A → A → Bool) → (xs : List A)
  → ((ys : List A) → R ys xs → List A) → List A
quicksort′ _≤?_ [] f = []
quicksort′ _≤?_ (x ∷ xs) f = f ys ys-lem ++ [ x ] ++ f zs zs-lem
  where
    ys = filter (λ y → y ≤? x) xs
    zs = filter (λ y → not (y ≤? x)) xs
    ys-lem : R ys (x ∷ xs)
    ys-lem = length-filter′ (λ y → y ≤? x) x xs
    zs-lem : R zs (x ∷ xs)
    zs-lem = length-filter′ (λ y → not (y ≤? x)) x xs

quicksort : ∀ {A} → (A → A → Bool) → List A → List A
quicksort {A} _≤?_ = wfRec (λ _ → List A) (quicksort′ _≤?_)
  where open WF.All R R-allAcc

参考

• Coqで、クイックソート - にわとり小屋でのプログラミング日記(2008-03-08)