日々の流転

λ. Lazy vs. strict

を読んだ。こうなったらWadlerの論文は一通り読もうか。

λ. 未読の本が溜っている場合、 FIFO で処理すべきか? それとも LIFO が適切か?

ちゃんとプライオリティ・キューを作るのが一番良いのではないかと。

λ. 研究会レポート「牌効率」

を読んだ。

λ. 鬱病認知尺度

もっと問題があるかと思ったのに、意外な結果。

あなたのうつ病認知尺度診断結果

総合得点は 55 点です。問題ありません。

以下の項目で一番得点の高い項目があなたの性格傾向です。

• 「否定的自己認知」得点は 22 点です。問題ありません。
• 「対人認知」得点は 18 点です。問題ありません。
• 「強迫的思考」得点は 15 点です。問題ありません。

λ. ベイブ2

を途中から見た。

λ. 読書

『PONとキマイラ 3』

浅野りん[画]

λ. "Institution Morphisms", Joseph Goguen, Grigore Rosu

メモ。難しい話はよくわからないが、Institution の基礎に関して割とよくまとまってる気がする。

λ. 研究計画書

書けねぇ。前の研究計画書にかいた事は熱意が冷めつつあるのだけど、それに代わるものが自分の中で育ってないのだよな。いざとなれば前の研究計画書を使いまわすのだが、しかしどうしたものか。

λ. 東方萃夢想 動作試験版

ダウンロードして試してみたのだけど、起動時にエラーが発生して遊べない。残念。

λ. コード

最近、自分のコードを書く余裕があまりない。書きかけで、ちゃんとまとめておきたいものは幾つかあるのだけど……

λ. E4X (ECMAScript for XML)

どーんとやってみよう(2005-04-27) と Derive Your Dreams (2005-04-27) より。

Erik Meijer の書いてた It's so Cool I am Freezing というエントリをちょっと思い出した。これがCωの XML Literal になったのかな。あと、HTMLをリテラルとして書くのはWASHでもやってたな。

λ. 『カイジ 2』, 福本 伸行

「限定ジャンケン」か。あれほどシンプルなルールから展開を二転三転させる技術は凄い。これまでカイジはあまり読んだことないのだけど、面白いな。

λ. 『歴代首相の経済政策　全データ』, 草野 厚

歴代の内閣の経済政策について、どういった政治環境の元でどういった意図からどのような経済政策が決定され実行されたのか。それを丹念に追っている。戦後60年の経済政策を総ざらいするには素晴らしい本だろう。

ただ、注意すべきなのは、帯には「吉田、岸、佐藤、田中、中曽根から小泉内閣まで仁政の総理、失政の宰相、全内閣の経済政策を問う」と書いてあるけれども、それらの経済政策について具体的に経済学的な分析や評価を行っているわけではないこと。「問う」と書いておいてそりゃないよなと思わないでもない。

関係ないけど、この本を持っていたら某氏に「日帝の陰謀ニダw」と言われた。どうやら俺の読んでいる新書は韓国関係と思われているらしいw。でも、それは誤解ニダ。ウリの読んだことのある韓国関係の本なんて、『親日派のための弁明』,『親日派のための弁明 2』,『竹島は日韓どちらのものか』, 『独島／竹島　韓国の論理』 くらいしかないニダ。だから、それこそ日帝の陰謀に違いないニダ。謝罪と賠償を(ry

λ. 関数プログラミングの妙味

[haskell-jp:589] 会誌「情報処理」 Vol.46 No.4 のスレッドより。

ここで Backus の FP を見るとは思わなかったよ。ちなみに FP には変数がなく Haskell でいうところの point-free な書き方をするのだけど、この点ではCPLとも似てたりする。なお、FP の詳細については Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs, John Backus を参照。

λ. 「耐100キロ級ボディ」の新キャビネットモデルも登場したLet's note新製品発表

ほすぃ。……といっても今ので別に困ってるわけでもないから買わんとは思うけど。

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

今日は圏論勉強会。

会場はいつもの所ではなく、びぎねっと様のトレーニングルーム。大きいディスプレイがあり、ネットワーク環境もあり、便利だった。感謝。

Wikiにあがっていない話では、「braidは環境(ambient)の次元を上げればsymmetryになる」という話が面白かった。

λ. Advanced Topics in Programming Languages Series: Parametric Polymorphism by Phil Gossett

syd_sydさんのらくがきえんじん(2007-04-24)で紹介されていたので観た。Girard-Reynolds Isomorphism と Djinn の簡単な紹介。

Djinn は Reynolds embedding : F2→P2 に基づいている?　扱われている例は単純な命題論理の範囲を超えてないので、普通に直観主義命題論理の決定手続きを応用すれば良いんじゃないかとも思ってしまう。

関連

• Wadler's Blog: Google Tech Talk: Parametric Polymorphism

λ. 正規表現にマッチする文字列をAlloyで生成する

• 正規表現からその正規表現にマッチするような例を生成する - soutaro#nikki()
• 正規表現にマッチする例 - d.y.d.
• 大人げ - sumiiの日記

辺りの話を思い出し、そういえばこれってモデル生成の話だから、Alloy Analyzer で出来そうだなと思ってやってみた。 結果としては特に面白くもなかったけど。 Regex.als

まず、文字列を表すための指標を用意。 個々の文字はCharをextendsする指標として定義する。

abstract sig Char {}

abstract sig String {}
one sig Nil extends String {}
sig Cons extends String {
　 head : one Char,
   tail : one String
}
fact {
   all s : Cons | not (s in s.^tail)
}

でもって、正規表現を文字列に関する論理式に変換するのだけど、DCG方式で差分リストに対する述語として定義する。 そうすると、大体以下のような感じで解釈することになる。

• [[ ]](x,y) = (x==y)
• [[ . ]](x,y) = (x.tail==y)
• [[ c ]](x,y) = (x.tail==y && x.head==c)
• [[ e1 e2 ]](x,y) = some z : String | [[ e1 ]](x,z) && [[ e2 ]](z,y)
• [[ e1|e2 ]](x,y) = ([[ e1 ]](x,y) || [[ e2 ]](x,y))
• [[ e? ]](x,y) = ([[ e ]](x,y) || x==y)
• [[ e* ]](x,y) = some r : String -> String { (all x,y : String | y in x.r <=> [[ e ]](x,y)) && y in x.*r }
• [[ e+ ]](x,y) = some r : String -> String { (all x,y : String | y in x.r <=> [[ e ]](x,y)) && y in x.^r }
• [[ [ab...] ]](x,y) = (x.tail==y && x.head in a+b+...)

Alloyでは述語の帰納的な定義が出来ないので、繰り返しはreifyした関係の(反射)推移閉包を使って表現するのがポイント。 というか、それをしたかったので差分リストに対する述語として形式化したんだけどね。 なお、今回は否定や補集合は扱っていないけど、それらを扱う際には関係rの量化と定義を否定の内側ではなく一番外側に持ってくる必要があるので注意。

そうすると、例えば「goo+gle」という正規表現は以下のようになる。

pred google(x : String) { google[x, Nil] }
pred google(x, y : String) {  
  some a, b, c, d, e : String {
    x.head==C_g
    x.tail==a
    a.head==C_o
    a.tail==b
    many1_o[b,c]
    c.head==C_g
    c.tail==d
    d.head==C_l
    d.tail==e
    e.head==C_e
    e.tail==y
  }
}

-- o+
pred many1_o(x, y : String) {
  some r : String -> String {
    all x, y : String | y in x.r <=> x.head==C_o && x.tail==y
    y in x.^r
  }
}

でもって、テスト。

pred test_google() {
  some x : String {
    google[x]
    all y : String | y in x.*tail
  }
}

run test_google for 10

runすると、それっぽい結果が出てくる。

お題の正規表現についても同様。

λ. 世にも奇妙な物語 — SMAPの特別編

懐かしいなぁ。 最初の「エキストラ」の話は以前は見逃していた気がする。

λ. 「形式的体系の定理証明支援系上での実現法」資料

を読んだ。 AgdaによるHoare論理の形式化と、whileプログラムの遷移系での解釈に対するHoare論理の健全性の証明の話。 ところで、「ホア論理」という呼び方は初めて見た……

λ. Thinkpadの互換バッテリーを購入

ROWA JAPAN で売っていた ThinkPad X60 シリーズ用の互換バッテリーを購入した。 純正品の40Y7003が¥13,780〜¥18,354なのに対して、こいつは¥8,400でかなり安かった。 バッテリー容量は純正品が5.2Ahなのに対して、これは4.6Ahらしいのでちょっと少ないけど、それはまあ仕方ないか。 まだ使い出したばかりだけど、やっぱり新しいバッテリー快適だ。

あらすじ

先日、「ご使用のバッテリーでは充電できません。」というメッセージが出てしまい、ダメモトでサポートに電話してみたが、(PC本体の保障期間は三年にしてあっても)バッテリーの保証期間は1年とのことで、保証での交換等にはならなかった。 高いけど新しいバッテリーを買うしかないかと思ってたら、ちょうどThinkPad X60 互換バッテリー購入 - ひげぽん OSとか作っちゃうかMona-で互換バッテリーのことを知ったのだった。

λ. PLDIr #8

PLDIの論文を読むPLDIrの第八回に参加。 今回はPLDI2002とPLDI2003の論文をやるはずが、参加者が少なすぎたために雑談モードに。

• Debugging Temporal Specification with Concept Analysis (PLDI2003)
• FLTVの「未来言語Alloy」の紹介
• 鵜川さんのISMM論文 Improved Replication-Based incremental Garbage Collection for Embedded Systems. Tomoharu Ugawa, Hideya Iwasaki (The University of Electro-Communications), and Taiichi Yuasa (Kyoto University) の話
• 水島さんのPASTE論文 Packrat parsers can handle practical grammars in mostly constant space. Kota Mizushima, Atusi Maeda and Yoshinori Yamaguchi (University of Tsukuba) の話
• 水島さんの、 Scala Days の話。ろーざんぬ！ - Onion開発しつつ、PEGEXを開発する日記
• A type and effect system for atomicity (PLDI2003)

λ. FSIJ 4月の定例会 「g新部、バグを追う旅 2010」

難しい……。 マルチスレッドとforkの話は、抽象化の破れを連想した。 普通にプログラムを書いていてこういうのに出会うということは、言語なりOSによる抽象化というのが、普段思っているほど堅牢なものではないということなんだろうな、などと思う。

λ. Google Code Jam 2012 : Round 1A

A-Largeの予想外の不正解で Rank: 1274 Score: 43 となってしまいパスできず。(id: sakai で参加中)

• Participant Details: sakai ― Code Jam 2012 Statistic

Problem A. Password Problem

即座にenterを押して全文字入力し直すのと、バックスペースを何回か押して残りを入力するのと、全部期待値を計算して、その最小を取れば良い。 Smallは超素朴に計算(A.hs)。 Largeは適当に実験すると非常に時間がかかったので、全部の確率の積を毎回計算しないようにした(A2.hs)。 ただ、全部の積を計算してから要らないやつで割るという方法を取ってしまっていて、そのせいで計算誤差が蓄積してしまったようで不正解を食らってしまっていた。 逆に順番に掛けていくようにしたら、正しく計算できるようになったようだ(A3.hs)。 浮動小数点数の誤差でハマったのは生まれて初めてかもしれない。 あるいはいっそ有理数で計算していればよかったかも。

Problem B. Kingdom Rush

2-star rating でまだクリアしていなくて今クリアできるレベル(1-star rating でクリア済みのものを含む)がある場合には、それを選んでいけば良い。 問題は 2-star rating でクリアできるレベルが存在しない時に、どのレベルを 1-star rating でクリアするか。 Smallはまずは全通り試して最短手数のものを選択する方法で解いた(B2.hs)。 Largeはそれだと解けないので、レベル選択をちゃんと考える必要がある。 直観的には、(今 1-star rating でクリアできる未クリアのレベルのうち) 2-star rating に必要なスター数が大きいものは、その後スターが増えても一気に 2-star rating でクリアできる見込みは小さい。そこで、2-star rating に必要なスター数が最大のものを(諦めて) 1-star rating でクリアするようにしたら、Smallのデータセットの範囲では結果が一致したので、それで(B3.hs)。

Problem C. Cruise Control

任意の二つの車について初期位置と速度から隣り合ってもしくは重なってしまう時間を計算し、これを各車ごとに車線変更不可能な時間として保持。 その上で、初期時刻および何れかの車が車線変更不可能な時間に入るタイミングを順番に見ていき、そのタイミングであり得る車の車線の配置の全可能性を考える。 全可能性を考えるには、前のタイミングで在り得た配置をもとに、そのタイミングで車線変更可能な車を任意に車線変更したものを考えれば良いはず。 そうやって初期時刻から順に見ていき、可能な全ての配置で衝突状態になっている最初の時刻が答え。 車線変更不可能なタイミングに入るタイミングを全部見終わってそういう時刻がないなら、Possible が答え。

……と思ったんだけど、実装は間に合わず。