日々の流転

λ. またSFC

いい天気なので、SFCに行ってみる。

萩野服部研では ICPC の過去問を解いていた。ちょうど、今週金曜がICPCの国内予選だとか。解いていた問題は2005年国内予選の Problem E - Earth Observation with a Mobile Robot Team で、これは参加したときに解けなくて悔しい思いをした問題だった。 家に帰ってから一応Haskellで解いたけど、やっぱりこれ面倒くさい問題だな。ハイブリッドシステムを扱える言語とか、制約を扱える言語とかで簡単に解けたりしないものだろうか。

IT-Systemでは、VIPS: a Vision-based Page Segmentation Algorithm とかその辺りの話。

BLOGRANGER TG というのを教えてもらった。面白いらしい。

久しぶりにニューオリンズ。

λ. Erlang で HelloWorld

Erlangは少し前に流行していたけど、プログラミングErlang(Joe Armstrong/榊原一矢) を借りたので、ちょっと遊んでみる。 現在の最新版は Erlang/OTP R12B というバージョンのようなので、これをインストールしてまずはHelloWorld。

#!/usr/bin/env escript
main(_) -> io:format("Hello, World!~n").

エスケープシーケンスはまんまPrologなのね。

それから、Erlangの等号は単一化ではなくただのパターン照合なので、以下のようなコードはエラーになるのか。

1> [1, X] = [Y, 2].
* 1: variable 'Y' is unbound

λ. A brainf*ck interpreter in Erlang

HelloWorld を書いたので、次は brainf*ck のインタプリタでも。

-module(brainfuck).
-export([brainfuck/1]).

brainfuck(Src) ->
    Prog=parse(Src), seq(Prog, {[], [0]}).

parse(X) -> {Y,_} = parse(X, []), Y.

parse([], Acc) -> {lists:reverse(Acc), []};
parse([H|T], Acc) -> 
    case H of
      $] -> {lists:reverse(Acc), T};
      $> -> parse(T, ['>'|Acc]);
      $< -> parse(T, ['<'|Acc]);
      $+ -> parse(T, ['+'|Acc]);
      $- -> parse(T, ['-'|Acc]);
      $. -> parse(T, ['.'|Acc]);
      $, -> parse(T, [','|Acc]);
      $[ -> {Prog,X}=parse(T, []), parse(X,[{Prog}|Acc]);
      _  -> parse(T, Acc)
    end.

seq(Prog, T) ->
    lists:foldl(fun (P,T1) -> step(P,T1) end, T, Prog).

step('>', {L,[X|R]}) ->
    {[X|L], case R of [_|_] -> R; _ -> [0] end};
step('<', {[X|L],R}) -> {L, [X|R]};
step('+', {L,[X|R]}) ->
    {L, [ case X of 255 -> 0; _ -> X+1 end | R ]};
step('-', {L,[X|R]}) ->
    {L, [ case X of 0 -> 255; _ -> X-1 end | R ]};
step('.', {L,[X|R]}) ->
    io:put_chars([X]), {L, [X|R]};
step(',', {L,[_|R]}) ->
    [X] = io:get_chars("", 1), {L, [X|R]};
step({W}, T) -> while(W, T).

while(_, {_,[0|_]}=T1) -> T1;
while(W, T) -> while(W, seq(W, T)).

といっても、前にPrologで書いたもの を適当に翻訳しただけ。

Erlang shell から実行してみる。

% erl
Eshell V5.6.3  (abort with ^G)
1> c(brainfuck).
{ok,brainfuck}
2> brainfuck:brainfuck("
>+++++++++[<++++++++>-]<.>+++++++[<++++>-]<+.+++++++..+++.[-]>++++++++[<++
++>-]<.>+++++++++++[<+++++>-]<.>++++++++[<+++>-]<.+++.------.--------.[-]>
++++++++[<++++>-]<+.[-]++++++++++.").
Hello World!
{[],[10,0]}

λ. Erlangでリファレンスを実装

Erlangの並行処理は最低限以下の三つを知っていれば使えるようだ。

• プロセスの生成 Pid = spawn(Fun)
• メッセージの送信 Pid ! Message
• メッセージの受信 receive Pattern1 -> Expression1; Pattern2 -> Expression; ... end

これはちょー簡単で良さそうですな。 ということで、まずは試しに変更可能なリファレンスを作ってみた。

-module(ref).
-export([new/1, get/1, set/2]).

new(Val) ->
  {ref, spawn(fun () -> loop(Val) end)}.

loop(Val) ->
    receive
      {From, get} -> From!{self(), Val}, loop(Val);
      {set, NewVal} -> loop(NewVal)
    end.

get({ref, Pid}) ->
    Pid!{self(), get},
    receive
      {Pid, V} -> V
    end.

set({ref, Pid}, Val) -> Pid!{set, Val}, true.

使ってみると、ちゃんと変更可能なリファレンスとして振舞ってくれる。やった!

% erl
Eshell V5.6.3  (abort with ^G)
1> c(ref).
{ok,ref}
2> X=ref:new(1).
{ref,<0.46.0>}
3> ref:get(X).
1
4> ref:set(X, 2).
true
5> ref:get(X).
2
6> 

λ. Morph Endo!: Report on the Tenth Interstellar Contest on Fuun Programming

“Morph Endo!: Report on the Tenth Interstellar Contest on Fuun Programming” by Eelco Dolstra, Jur Hage, Bastiaan Heeren, Stefan Holdermans, Johan Jeuring, Andres Löh, Arie Middelkoop, Alexey Rodriguez, John van Schie, Clara Löh

を読んだ。今年の ICFP Programming Contest ももうすぐだけど、これは昨年の ICFP Programming Contest 2007 (c.f. 参加記録)の出題者らによるテクニカルレポート。 昨年参加したときには丁度入り口付近に辿りついたところで終了という感じで悔しかったのだけど、この先にはこんなに作りこまれた世界が広がっていたのね。 改めて凄いと思った。

去年悔しい思いをした人は、このレポートをガイドにして再挑戦してみるのも楽しいかも。DON'T PANIC!

λ. RHG読書会::東京 Practical Common Lisp 第八回

.

λ. 第四十二回圏論勉強会

今日は圏論勉強会だった。写真

λ. サンタクロース問題

お約束ということで、サンタクロース問題に挑戦してみた*1。

-module(santa).
-compile(export_all).

santa([_,_,_,_,_,_,_,_,_]=Reindeers, Elves) ->
   work("delivering", 3000, Reindeers), santa([], Elves);
santa(Reindeers, [_,_,_]=Elves) ->
   work("meeting", 1000, Elves), santa(Reindeers, []);
santa(Reindeers, Elves) ->
    receive {reindeer, X} -> santa([X|Reindeers], Elves)
    after 0 ->
       receive
          {reindeer, X} -> santa([X|Reindeers], Elves);
          {elf, X} -> santa(Reindeers, [X|Elves])
       end
    end.

work(What, N, XS) ->
   io:format("Santa Claus starts ~s.~n", [What]),
   random_wait(N),
   io:format("Santa Claus ends ~s.~n", [What]),
   lists:foreach(fun (X) -> X!leave end, XS).

srand() -> {X,Y,Z}=erlang:now(), random:seed(X,Y,Z).

random_wait(N) ->
    receive
    after random:uniform(N) -> true
    end.

loop(Santa, Kind, Name) ->
    random_wait(2000),
    io:format("~s comes.~n", [Name]), Santa!{Kind, self()},
    receive
       leave ->
          random_wait(1000), io:format("~s leaves.~n", [Name]),
          loop(Santa, Kind, Name)
    end.

start() ->
    Santa = spawn_link(fun () -> srand(), santa([], []) end),
    [ spawn_link(fun () -> srand(),
         loop(Santa, K, S ++ erlang:integer_to_list(X, 10)) end)
     || {S,K,N} <- [{"Elf", elf, 10}, {"Reindeer", reindeer, 9}]
      , X <- lists:seq(1,N) ].

タイムアウト節を持つreceiveを使うことで、指定した時間だけ待ったり、優先順位付きの受信をしたりといったことが出来るのが少し面白かった。 それから、プロセスのリンクやモニタのような機能は、他の言語の並行処理でも結構欲しくなることがあるので、これが組み込みであるのはいいなぁ。

λ. GHCの“Generalised derived instances for newtypes”便利かも

これまでGHC拡張の Generalised derived instances for newtypes はそんなに便利だとは思っていなかったけど、<URL:http://lambda-the-ultimate.org/node/2749#comment-41075> の以下の例を見て、これは便利かもと思った。

newtype X a = X (ReaderT XConf (StateT XState IO) a)
  deriving (Functor, Monad, MonadIO, MonadState XState, MonadReader XConf)

λ. 文脈自由文法のパーサの計算量

文脈自由文法のパーサで良く知られているのは CYK algorithm や Earley parser で、これらの計算量は O(m³) なのだけど、文脈自由文法の計算量は O(m^2.???) だという話を以前に向井先生から聞いたことがあった。 これはどうやるんだろうなぁとずっと思っていたが、Boolean Matrix Multiplication (BMM) というものを使うそうだ。

(後で書くかも)

参考: Fast context-free grammar parsing requires fast boolean matrix multiplication

λ. “Reasoning support for Semantic Web ontology family languages using Alloy” by Hai H. Wang, Jin Song Dong, Jing Sun and Jun Sun

Semantic Web (SW), commonly regarded as the next generation of the Web, is an emerging vision of the new Web from the Knowledge Representation and the Web communities. To realize this vision, a series of techniques has been proposed. Semantic Web Ontology Langauge (OWL) and its extension Semantic Web rule Language (SWRL) and Semantic Web Logic Language (SWRL-FOL) are some of the most important outputs from the SW activities. However the existing reasoning and consistency checking tools for those languages are primitive. This paper proposes using the existing formal modelling tool, in particular Alloy, to provide an automatic reasoning service for the Semantic Web ontology family languages (OWL/SWRL/SWRL-FOL).

ふと、「OWL から Alloy に変換して Alloy Analyzer を推論に活用したら面白いんじゃなかろうか。両方とも二項関係がベースだし、Semantic Web では厳密な推論よりは実用性が重要から、相性良さそうだし」とか思ったのだけど、探したらやってる人は既がいた。残念。

Alloyへの変換は straight forward だけど、当時の Alloy は今と少し違っていて、extend した signature 同士を排反(disjoint)にするために、明示的に disj を書く必要があったようだ。

λ. デジカメ購入 (EX-V7BK)

カシオの EXILIM Hi-ZOOM (EX-V7BK) を勢いで買ってしまった。実のところそんなにデジカメを使うあてもないんだけどね……

λ. ICFP Programming Contest 2008 終了

結局、結果はだせなかったけど、72時間とても楽しかった。

【2008-10-05 追記】 最後にsubmitしたアーカイブを一応晒しておく。icfp08.tgz

λ. お菓子買いだめ

あまり沢山買ったつもりはなかったけど、予算オーバー。

λ. 3 not problem

x,y,zの3入力, x',y',z'の3出力を持つブラックボックスがある. 入出力の関係は

• x' = not x
• y' = not y
• z' = not z

である. ブラックボックスには, andとorは好きなだけ使われているが, notは2つしかないことが分かっている. 内部はどうなっているか.

ささださんのだいありー(2008-07-15)と、 3 not の問題 - まめめも(2008-07-16)経由で。 例によってAlloyで解こうとしたら、Alloy Analyer のバグを踏んだっぽい(追記: どうもバグではなく仕様だったっぽい)。 あと、昔Otter関係で聞いたことのある話だなと思ったら、<URL:http://www-unix.mcs.anl.gov/AR/otter/examples33/program/two_inv.in> にあった。

λ. Alloy で 3 not problem を解く

以下のような感じで書いたのだけど、Alloy Analyzer にかけたところ、残念ながら数時間程度では解けない感じだった。Otterでやっているように、真理値表を8bit整数で表してビットごとのandやorで操作できると、もうちょっと効率よくなりそうなんだけど、今のAlloyにはそれらのビット演算はないのだった。ビットシフトはあるのに……(涙

/*
The 2-inverter puzzle.

The problem is to build a combinational circuit with 3 inputs
and 3 outputs, such that the outputs negate the inputs; we can
use as many AND and OR gates as we wish, but at most 2 NOT gates.
*/

abstract sig Bool {}
one sig True, False extends Bool {}

abstract sig Node {
   t : set (Bool -> Bool -> Bool)
}
sig Not extends Node {
   i : Node
}
abstract sig Op2 extends Node {
   i1 : Node,
   i2 : Node,
}
sig And, Or extends Op2 {}
one sig X,Y,Z extends Node {}

pred v[n : Node, a : Bool, b : Bool, c : Bool] {
   (a->b->c) in n.t
}

fact {
   no n : Node | n in n.^(i + i1 + i2)
   all a,b,c : Bool {
      v[X,a,b,c] <=> (a=True)
      v[Y,a,b,c] <=> (b=True)
      v[Z,a,b,c] <=> (c=True)
      all n : Not | v[n,a,b,c] <=> !v[n.i,a,b,c]
      all n : And | v[n,a,b,c] <=> (v[n.i1,a,b,c] && v[n.i2,a,b,c])
      all n : Or  | v[n,a,b,c] <=> (v[n.i1,a,b,c] || v[n.i2,a,b,c])
   }
}

pred show() {}
run show for 10

pred two_inv {
   some n1,n2,n3 : Node {
      all a,b,c : Bool {
         v[n1,a,b,c] <=> !v[X,a,b,c]
         v[n2,a,b,c] <=> !v[Y,a,b,c]
         v[n3,a,b,c] <=> !v[Z,a,b,c]
      }
   }
}
run two_inv for 25 Node, exactly 2 Not

λ. Otter で 3 not problem を解く

20080716#p02で紹介したように、3 not problemを定理証明機のOtterに解かせる例が <URL:http://www-unix.mcs.anl.gov/AR/otter/examples33/program/two_inv.in> にあるので、実際に実行してみた。以下ネタバレ注意!!

• 実行ログ
• 証明から抽出した回路をGraphvizで適当に整形したPNG (.dot)

今だと25秒で解けているが、当時の486マシンで40分かかったそうで、大体100倍高速化した計算か。

Otterの入力ファイルをまじめに読んだのは初めてだったのだけど、Prologみたいに結構汚いことが出来るのね。$VARなんてPrologのvarメタ述語そのものじゃないか。そして、汚いけど、このリソースの扱い方は非常に巧妙で感心した。 記述する論理を線形一階述語論理にすれば、もっと素直に書けるだろうとも思うが、そういえば線形論理の定理証明機とかってあまり聞かないな。 線形一階述語論理に基づいた線形論理プログラミングよりも更に聞かないけど、なんでなんだろうね。

ついでに、Otterの後継のProver9でも試そうと思ったのだけど、Prover9はOtterよりも純粋な定理証明機のようで、同じテクニックは使えなさそうだった。うーむ。

λ. 時をかける少女

テレビでやっていたので観た。 筒井康隆の小説とはぜんぜん違う話なのね(こっちも読んでないけど)。

λ. 泳いできた

近くのプールに行って、今年初めて泳いできた。 軽く1km泳いだだけだけど、早速筋肉痛になってしまった。 普段運動してないからなぁ。 去年、20070511#p02では筋肉痛になったのを大胸筋(Pectoralis major muscle)と書いたけど、これはむしろ小胸筋(Pectoralis minor muscle)という気もする。自分の筋肉がわからん……

λ. 『それがぼくには楽しかったから』 by Linus Torvalds and David Diamond

非常に今更なのだが、友人に薦められて『それがぼくには楽しかったから』読んだ。オープンソースの勃興期の非常にワクワクした雰囲気を思い出して懐かしくなった。 この日記を検索したら、この本は2002-10-19に借りて読んでいるはずなのだけど、読んだのを全然覚えてないや。

λ. 泳いできた (2)

先週の20080721#p01に続いて、今日も近くのプールに泳ぎに行ってきた。 今日は1.3kmくらい泳いで、ひざ上の内側あたり(内側広筋Vastus medialis?)がつりそうになった。

午後は昼寝と読書をしてすごす。

それから、逆転裁判、最後までやった。

λ. 『投資信託にだまされるな! Q&A―投信の疑問・解決編』 by 竹川 美奈子

投資信託にだまされるな! Q&A―投信の疑問・解決編(竹川 美奈子)を読んだ。これまで手数料が高い投資信託しか知らなかったけど、インデックスファンドなどではずいぶん手数料が安いものもあるのね。 これくらいの手数料なら長期の分散投資に非常に良さそうなので、この本で薦められていた投信の一つの セゾン・バンガード・グローバルバランスファンドを少し買ってみようと思う。

λ. MONAで正規表現にマッチする例を生成する

論理と計算のしくみ(萩谷 昌己/西崎 真也) にWS1S(Weak Second-order monadic logic of 1 Successor, 後継者のみの単項二階論理)の論理式と有限状態オートマトンとが対応するとか書いてあった。 それなら、正規表現に対応する有限状態オートマトンをWS1Sの論理式で記述して、モデル探索を行えば、与えられた正規表現からマッチする文字列の例を生成するようなことが出来るんじゃないかと思ったのだった。

『論理と計算のしくみ』の場合

ただ、『論理と計算のしくみ』での説明は良く分からなかった。 この本での説明は、萩谷先生の講義録「高階述語論理とその部分体系」でなされている以下の説明とほぼ同じなのだけど、「i>j ==> not i∈Xj」という条件をどう考えればよいのかが分からない。

n個の自然数の集合X1,...,Xnと、{0,1}^nをアルファベットとする語wを対応させる。

X1,...,Xn  <-->  w=a0a1a2...am  where

    ai = (b1,...,bn)

        bj=1  iff  i∈Xj

    i>j  ==>  not i∈Xj

しばらく考えてもわかんなかったので、とりあえずWS1Sの検査などを行えるシステムとして有名なMONAを見てみることにした。

MONAの場合

MONAについてはよく知らなかったのだけど、MONAのサイトを見てみると、以下のように書いてあった。なるほど、オートマトンに変換してやっているのね。モデル検査っぽいなぁ。

MONA is a tool that translates formulas to finite-state automata. The formulas may express search patterns, temporal properties of reactive systems, parse tree constraints, etc. MONA analyses the automaton resulting from the compilation and prints out "valid" or a counter-example.

で、ダウンロードして見てみると、regexp.mona として正規表現「a*(ab*)」を WS1S にエンコードしている例があった。 これが非常に分かりやすくて、ごく一部のMONA固有の機能を除けば、前提知識無しで読むことが出来るものだった。 また、「論理と計算」での取り扱いよりも単純で分かりやすい。

ポイント:

• 位置 p で性質 P が成り立つことを、二階の変数 P を用いて、p∈P で表現する。
• そのような性質として、bit1,…,bit7 を用意して、各ビットが1であることを表現する。
• WS1Sだと(一階の)領域は自然数全体なのに対して、文字列の場合には位置は有限なので、下に閉じた二階の変数 $ を用意して、通常の変数は $ の要素や部分集合のみを動くようにする。(そうしないと、全ビットが0であるような文字の繰り返しが終端に現れるような文字列を正しく扱えない)
• 正規表現は、「開始位置」と「終了位置+1」をとって、開始位置から終了位置までの文字列が正規表現にマッチする場合に真になるような述語として表現。(差分リスト方式)
• 正規表現全体を表現した述語(この場合にはis_a_star_ab_star)を使って、「is_a_star_ab_star(0, max($)+1)」という論理式にする。これで文字列全体がこの正規表現にマッチすることが表せる。

MONAの実行例

で、「mona.exe regexp.mona」を実行してみる。 そうすると、色々出てくるが、結果の中の以下のような部分が正規表現にマッチする具体的な文字列を表している。

A satisfying example of least length (0) is:
bit0            X 
bit1            X 
bit2            X 
bit3            X 
bit4            X 
bit5            X 
bit6            X 
bit7            X 

bit0 = {}
bit1 = {}
bit2 = {}
bit3 = {}
bit4 = {}
bit5 = {}
bit6 = {}
bit7 = {}

この場合だと空文字列になっている。 これだと面白くないので、「5 in $」という論理式を加えて、長さが6以上のものを探させると、こんなのが出てくる。

A satisfying example of least length (6) is:
bit0            X 101010
bit1            X 010101
bit2            X 000000
bit3            X 000000
bit4            X 000000
bit5            X 111111
bit6            X 111111
bit7            X 000000

bit0 = {0,2,4}
bit1 = {1,3,5}
bit2 = {}
bit3 = {}
bit4 = {}
bit5 = {0,1,2,3,4,5}
bit6 = {0,1,2,3,4,5}
bit7 = {}

最初の行からこの具体例の長さが6であることがわかり、続く表の各カラムを見ると各位置の文字のビットパターンがわかる。これをデコードすると「ababab」という文字列になっている。 で、後半部分は変数の割り当て。

あとは、複数の具体例を順番に出したりする機能があると面白いのだけど、残念ながらMONAにはそういった機能はないようだ。

参考

• 細谷研究室 演習３課題 「MONAを使おう」
• 正規表現にマッチする文字列をAlloyで生成する - ヒビルテ (2008-04-28)

λ. 今日の日記

午前中、近くのプールでまた1km泳ぎ、午後は第6回 RHGの逆襲へ参加。 こっちの読書会にはどんな人が参加しているのかな、という好奇心で参加してみたのだけど、色々な人に会えて、やっぱり楽しかった。でも、行く前に svn update していけば良かったな。そこはちょっと失敗。

あと、新橋の駅前で小銭入れを買った。

λ. 大洗

大洗に行き、海鮮市場で回転寿司でお昼を食べて、その後大洗水族館などに行ってきた。

こないだ買ったデジカメは一応動画も撮れる様なので、ためしに海月など撮って見て、ffmpegでmp4に変換してみたのだけど、どうもFlowPlayerで再生できないなぁ。とほほ。 kurage.mp4

【2008-08-16追記】 再生できなかった原因が分かった。ビデオファイルを相対URLで指定すると、FlowPlayerのswfファイルからの相対URLとして解釈されるのね。なまじa要素のhref属性で書けるようになっているから気づかなかった……orz　 DOMではhref属性の値は常に絶対URIだけど、FlowPlayerのjavascriptではjQueryでattr("href")としてとっていて、これだと相対URIがそのまま返ってきてしまうっぽい。

【2008-08-17追記】 このファイルは単に ffmpeg -i foo.mov -vcodec copy -an foo.mp4 したものにだったんだけど、でっつ :: Entries :: FlowPlayerで再生するためのファイル件 を参考に、qt-faststartとAtomicParsleyで処理したものにしてみた。

λ. 依存型とcatamorphism

Agda2ことはじめ - ラシウラ の記述を読んで、そういえば依存型を用いた除去規則って、(弱)始代数の普遍性とはどう関係するんだろうか、と思ったので、category with attributes で考えてみた……んだけど、書いてたら混乱してきたので、何回かに分けて書くことにする。

1. Categories with attributes (cwa)
2. cwaでのユニット型の解釈