日々の流転

λ. Haskellers Meeting 2010 Spring のお知らせ

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

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

λ. Haskellers Meeting 2010 Spring

色々な人に会えた。 ICFP Programming Contest 2007 にチームAyaCFPとして一緒に参加した@Maki_Daisukeさん、@tyasunaoさんにも直接お会いできた。

OSConのスライドにあった Direct Update STM が気になって、聞いてみたら、Tim Harris がC#でやった仕事だったそうだ。 探してみると Optimizing Memory Transactions っぽい。

参考

• kazuさんの発表資料
• nobsunの発表資料
• O'Reilly Village／オラの村 - 150人のHaskellerが感動！「Haskellers Meeting 2010 Spring」

λ. CLTT読書会第一回

Cartesian Morphism の定義がああなっている動機がわかって良かった。 今のところ、難易度は Preliminaries > Chapter 0 > Chapter 1 のような気がする。

λ. GLPKで数独を解く

去年はいろんなソルバやモデルファインダーを使って数独を解いて遊んでいて、最後にやったのが、丁度一年前の記事の「ASPで数独を解く」。 一年ぶりにまたふとやってみたくなったので、今度はフリーの線形計画法ソルバの GLPK (GNU Linear Programming Kit) を使ってやってみた。

まずは問題の構造を記述したファイル SudokuGLPK.mod:

set Number := 1..9;

param Data{Number, Number, Number} binary default 0;

var Ans{Number, Number, Number} binary;
s.t. GIVEN{x in Number, y in Number, n in Number}: Data[x,y,n] <= Ans[x,y,n];
s.t. FILLED{x in Number, y in Number}: sum{n in Number} Ans[x,y,n] = 1;
s.t. COL{n in Number, x in Number}: sum{y in Number} Ans[x,y,n] = 1;
s.t. ROW{n in Number, y in Number}: sum{x in Number} Ans[x,y,n] = 1;
s.t. BLOCK{n in Number, x0 in 0..2, y0 in 0..2}:
      sum{x1 in 1..3, y1 in 1..3} Ans[3*x0+x1, 3*y0+y1, n] = 1;

「座標(x,y)の数がnであること」をAns[x,y,n]が1であることで表現して、その組み合わせに関する条件を算術的に表現している。 やっている事自体はSATで解く場合と大して変わらないんだけど、結構直観的に書けて良かった。

次に、具体的な問題のデータを記述したファイル SudokuGLPK.dat:

param Data := 
  1 1 1 1
  1 4 2 1
  1 7 3 1
  2 2 2 1
  2 5 3 1
  2 8 4 1
  3 3 3 1
  3 6 4 1
  3 9 5 1
  4 1 6 1
  4 4 4 1
  4 7 5 1
  5 2 7 1
  5 5 5 1
  5 8 6 1
  6 3 8 1
  6 6 6 1
  6 9 7 1
  7 1 8 1
  7 4 9 1
  7 7 7 1
  8 2 9 1
  8 5 1 1
  8 8 8 1
  9 3 1 1
  9 6 2 1
  9 9 4 1;

このファイルは配列Dataに対する値の割り当てを表していて、「a b c 1」という行は Data[a,b,c] が 1 であることを表している。

これで glpsol.exe -m SudokuGLPK.mod -d SudokuGLPK.dat -o ans.txt と実行すると、ans.txtのようなファイルが得られる。 このファイルの途中を見ると、以下のような感じで配列Ansに対する値の割り当てが得られる。 たとえば、Ans[1,2,4]のActivityが1なので、座標(1,2)の数が4であることが分かる。

…
   No. Column name       Activity     Lower bound   Upper bound
------ ------------    ------------- ------------- -------------
     1 Ans[1,1,1]   *              1             0             1 
     2 Ans[1,1,2]   *              0             0             1 
     3 Ans[1,1,3]   *              0             0             1 
     4 Ans[1,1,4]   *              0             0             1 
     5 Ans[1,1,5]   *              0             0             1 
…
    13 Ans[1,2,4]   *              1             0             1 
…

参考

• GLPKで楽しく最適化しよう！
• 整数計画法によるパズル解法（実習報告）

λ. 告知: Oleg さんや 單中杰（Chung-chieh Shan）さんを交えての会合

明日4/24(土)に Oleg さんや 單中杰 (Chung-chieh Shan)さんを交えての会合が企画されています。 参加したい人は @shelarcy さんに連絡をとってみると良いと思います。

• <URL:http://www.sampou.org/cgi-bin/haskell.cgi?HaskellEvent>

λ. Functional Programming Meeting 2010

昨日紹介した、Oleg さんや 單中杰（Chung-chieh Shan）さんを交えての会合に参加。

λ. 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による抽象化というのが、普段思っているほど堅牢なものではないということなんだろうな、などと思う。

λ. 第4回FormalMethods勉強会

に途中から参加。

ken.coba さんの Alloy の話。

komagatime さんによる CEGAR の話。

tmiyaさんによる Certified Programming with Dependent Types の解説。

関連

• Functional Programming Memo: [Coq][FM] Fomal Methods Forum #4
• Functional Programming Memo: [Alloy][FM] Sample code: Addressbook