日々の流転

λ. たむちゃんと塚が久しぶりにやってきて、急に出かけることになった。とりあえず、海岸の方をブラブラ。昼食は「珊瑚礁」で「ナスとひき肉のカレー」。おいしかった。評判になるだけはある。で、さらにブラブラ。逗子辺りまで海岸を歩こうか思ったけど、由比が浜でダウン。鎌倉駅へ行って、そっから横浜こども科学舘に行きプラネタリウムを見た。

λ. GIMP 1.2.2 is finally out

おぉ。

λ. 飲み

大学のクラス会。湘南台なので、行く途中に藤沢のθでKondara 2.0を買った。これで僕もMaryさ。…ってのはおいておいて、ジンが効いたのか、今日は生まれて初めて酔っ払った。ホントにまっすぐ歩けなくなるんだぁ。ちょっと感動。でも、何かフワフワして自分が自分じゃないみたいで、気持ち悪いよぉ。おえぇ〜

λ. 今日の迷言

「何が飲みたい?」「君が飲みたい」

λ. 寝坊。

λ. 田中先生飲み

田中先生と「線形の理論」「数学基礎」のSAで新宿へ飲みに行く。「さいぞう」(ozmall,Yahoo!グルメ)というちょっと変わった雰囲気の居酒屋へ。伊藤君が数学を熱く語るので、応戦してみたり。それにしても、伊藤君がこんなに天然だとは知らなかった。

帰りは、最後のモノレールに間に合わないかと思ったけど、和田さんに教えてもらって、なんとか最後のモノレールに間に合う。おかげで藤沢から歩いて帰るという事態を回避できた。感謝感激なり。

λ. ⊂⌒~⊃。Д。）⊃

気持ち悪い。早速、夏バテか。

λ. Enumerating the Rationals.

LtU より。既約分数を効率的に列挙するアルゴリズムの話+α。数学的には新しい話ではないそうだけど、例の既約分数クイズの解答の Stern-Brocot Tree に興味を持った人は読んでみると面白いかも。

λ. Categories List in Japanese

一応subscribe。

λ. 欧州で短期村に初参加

hatoさんが企画した欧州の短期村に参加してきた。いやー、短期はむずいね。二回とも寡黙吊りっぽい感じで吊られてしまった。

• 人狼@欧州 252村 皆で短期に慣れる村
• 人狼@欧州 255村 続・皆で短期に慣れる村
• 関連
  • 狼）欧州短期をしませんか (hatoさん)
  • 狼）欧州短期建てます。 (hatoさん)
  • 狼）はじめてのおうしゅう (hatoさん)

λ. 『イリアと魔法の図書館』 木島 麻貴

を読んだ。 図書館を舞台にしたファンタジーということとあと表紙に惹かれて手にとった本。ご都合主義な気がするが、子供向けのファンタジーだとこんなものなのかも。

λ. 各要素が「0または1をとる乱数」から成る長さnのリスト

勝手にどう書く0.0 より。あまり興味を惹かれるお題ではないけど、一応。

Prelude> :module +Random
Prelude Random> :module +Monad
Prelude Random Monad> xs <- liftM (take 10 . randomRs (0,1)) newStdGen
Prelude Random Monad> xs
[1,0,0,1,1,0,1,1,0,1]

λ. 空集合から空集合への関数空間 ∅^∅

空集合から空集合への関数空間 ∅^∅ は当然 {∅} だと思っていたのだが、論理と計算のしくみ(萩谷 昌己/西崎 真也) の問題の解答(p.245)には「∅^∅ は定義されない」と書いてあった。

∅^∅ は定義されない(これは関数の定義にもよる．A から B への関数を A×B の部分集合と考えるならば，∅^∅ = {∅} と考えることもできよう．しかし，A≠∅ ならば，A^∅ は一つの関数からなる集合であり，一方 ∅^A=∅ でもあるので，これらの二つの場合が交錯する ∅^∅ という式は，矛盾していると考えることも出来る)．

この本では関数を「集合 A から集合 B への関数(function)とは，A の各要素に B の要素を与える対応のことである」としか定義しておらず、この定義では通常 ∅^∅={∅} なのに、「これは関数の定義にもよる」と言われてもなぁ。 しかも、A≠∅ ならば A^∅ と ∅^A は重ならないし(言いたいことはわからんでもないけど)。

それにしても、∅^∅ を未定義とするというのは初めて見たのだが、これってどこかの分野の流儀なのだろうか?　こうしてしまうと、 Set を圏にするときに hom(∅, ∅) をどうするかとか、色々と不都合があるように思うのだが……

【8/8追記】 sumiiの日記 - 0の0乗 の追記で知った*1のですが、<URL:http://nicosia.is.s.u-tokyo.ac.jp/pub/staff/hagiya/shikumi/errata.html> に訂正があって、∅^∅={∅} に訂正されている。丁度、質問メールを書こうとしていた矢先だったのだけど、もし私の指摘が原因で訂正されたのだとしたらちょっと嬉しいなぁ。

λ. Setoidの訳は亜集合?

帰りの電車の中でふと「Groupoidの訳語が『亜群』ならば、Setoidの訳語は『亜集合』なのだろうか?」と思ったのだけど、後で検索した限りではそのような訳語は使われていなかった。ちょっと残念。

Groupoid

射が全て同型射である(小さな)圏

Setoid

集合(Set)に同値関係を加えたもの。

λ. 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 していけば良かったな。そこはちょっと失敗。

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

λ. 携帯の番号が変わります

最近、携帯を変えました。MNPを使わなかったので番号が変わります。新しい番号は前の番号(090〜)から、電卓で1003227378をマイナスしたものです。また、メールアドレスはgmailのものを使っています。