日々の流転

λ. メディア・センタで連休中に読む本を借りようかと学校に行ったら、メディア・センタが閉ってた。

λ. ソース読み会

ゴールデンウィーク特別イベント。NetBSDのUSBドライバを読んだ……のだけど付いてけなかった…… → 加藤さんによるまとめ

ところで、grepとlessでソースを読むというのは初めて聞いたよ。

それから、とーやまさんが頭を剃っててビックリした。

λ. Haskellのパターンマッチと単一化 (ゆ〜あいの日記 4/17)

「１が((+) x 1)に単一化できるとするとx=0になるはずですね。これは(+)の逆関数が必要になりますが、処理系が逆関数を生成するは困難ですね。」とあるけど、制約論理プログラミングについて調べてみると良いと思う。

λ. ヘルシング TV版

をビデオで見た。ひっじょーに素晴らしいね、アンデルセンの扱いを除けば。つうか、こんなの作ってアンデルセン・ファンに殺されたりしないのでしょうか?

λ. screenのススメ

.

λ. 力と制度、或いはコンパクト化について

脱力するねぇ。

λ. :=<

「:>=」はオッケーなのに「:=<」はパースエラーになるのか。

λ. 圏論&オントロジー

昨日、「圏論　オントロジー」というキーワードで検索されてるけど、圏論とオントロジーって何か関係あるんでしょうか?

λ. ゲロゲロ。無様な醜態を晒してしまった。

λ. kbmj の人とお会いして色々と話を聞いてくる。悩む。それから、ご馳走様でした。

λ. Froogle

メモ。

λ. 東方永夜抄体験版スペルカード

Lunaticの残り4枚がなかなか回収できない。「高天原」以外は取れそうで取れないのが悔しい。ちなみに、「高天原」に至ってはまだ見たことすらなかったり。あぅー

• 隠蟲「永夜蟄居」
• 夜雀「真夜中のコーラスマスター」
• 野符「GHQクライシス」
• 未来「高天原」

λ. テレビ

めずらしくWWEなど見てみる。

λ. SISTER OF SCARLET

東方紅魔郷ExtraのFlash。完成版。

λ. Workshop "Types for Verification"

例によって池上さんに紹介してもらったワークショップ。内容にはかなり興味があるのだけど、諸事情により行くかどうか悩み中。

λ. 第三次国共合作?

台湾の国民党と中国共産党が接近していることが某所で「第三次国共合作」と書かかれていた。面白い。

λ. GCC 4.0.0リリース

いつの間にか出てた。すっかり見落とすところだった。

• ソースからバイナリへ: GCCの内部機構 - Diego Novillo

λ. ソードフィッシュ

を視た。技術的なとこはノーコメント。終わり方はなんとも言えないが、安っぽい結末でなくて良かったと思う。

λ. javascriptでRDFをパース

やっぱし、やっている人はいるもんだな。 何かに使えそうな気がするのでメモ。

• Simple javascript RDF Parser and query thingy
• Javascript-RDF Testbed

λ. (forall x. ((x->r)->r)->x) -> Either a (a->r)

今日ちょっと混乱したことを元にクイズにしてみた。多分その手の人にはピンとくる問題。表記はHaskellのものを使ったが、実際には多相ラムダ計算の問題と考えていい。

問題

1. 「(forall x. ((x->r)->r)->x) -> Either a (a->r)」という型を持つ関数を定義せよ。(ただし⊥が途中で現れたりする定義は禁止)
2. この関数は何を表しているのだろうか?

解答編

問題の関数はこんな感じで定義できる。

notNotEM :: ((Either a (a->r)) -> r) -> r
notNotEM k = k (Right (\a -> k (Left a)))

dn2EM :: (forall x. ((x->r)->r)->x) -> Either a (a->r)
dn2EM dn = dn notNotEM

で、これが表しているのは何かだが……二重否定除去規則から排中律(The Law of excluded middle)を導く証明の計算的な表現だったりする。型はちょっと一般化してあるので、以下のようにより具体的な型にすると分かり易いかも*1。

data Absurd
type Not p = p -> Absurd
type Or = Either

notNotEM :: Not (Not (p `Or` Not p))  
dn2EM :: (forall x. Not (Not x) -> x) -> p `Or` Not p

で、面倒なので詳しい説明は省略するが、例えばNK(自然演繹の体系NJに二重否定除去規則を追加した体系)で排中律を証明すると、この関数の構造を反映した証明図が得られる*2。

[1: P]
------------- (∨I左)
  P ∨ ¬P              [2: ¬(P ∨ ¬P)]
------------------------------------------- (¬E)
  ⊥
------------- (¬I{1})
  ¬P
------------- (∨I右)
  P ∨ ¬ P             [2: ¬(P ∨ ¬P)]
------------------------------------------- (¬E)
  ⊥
------------------ (¬I{2})
  ¬¬(P ∨ ¬P)
------------------ (¬¬E)
  P ∨ ¬P

他の体系での証明は誰かにまかせた。あろはさんはこの証明をCoqで表現してみると良い勉強になるかも。ついでに古典論理のうさんくささをもっと感じられるかもw

余談

ちなみに、色々と細かいことを抜きにすれば、否定は継続に対応し、二重否定除去規則に対応するものはcall/ccで実現できる。Haskellにはそれらは存在しないので多少回りくどい表現になっているが、一級継続とcall/ccが存在する言語では直接それらを使って排中律に相当するものを表現することが出来る。例えばSchemeだと以下のような感じだろうか*3。

(define (left x)  (list #t x))
(define (right x) (list #f x))

(call-with-current-continuation
  (lambda (k) (k (right (lambda (a) (k (left a)))))))

しかし、それにしても奇妙な定義と振る舞いである。これに関係して、Philip Wadler, Call-by-value is dual to call-by-name. Proc. ICFP 2003, pp. 189-201. <URL:http://homepages.inf.ed.ac.uk/wadler/topics/dual.html> に載っていたお伽噺が面白かったので、引用する。

Once upon a time, the devil approached a man and made an offer: “Either (a) I will give you one billion dollars, or (b) I will grant you any wish if you pay me one billion dollars. Of course, I get to choose whether I offer (a) or (b).”

The man was wary. Did he need to sign over his soul? No, said the devil, all the man need do is accept the offer.

The man pondered. If he was offered (b) it was unlikely that he would ever be able to buy the wish, but what was the harm in having the opportunity available?

“I accept,” said the man at last. “Do I get (a) or (b)?”

The devil paused. “I choose (b).”

The man was disappointed but not surprised. That was that, he thought. But the offer gnawed at him. Imagine what he could do with his wish! Many years passed, and the man began to accumulate money. To get the money he sometimes did bad things, and dimly he realized that this must be what the devil had in mind. Eventually he had his billion dollars, and the devil appeared again.

“Here is a billion dollars,” said the man, handing over a valise containing the money. “Grant me my wish!”

The devil took possession of the valise. Then he said,“Oh, did I say (b) before? I’m so sorry. I meant (a). It is my great pleasure to give you one billion dollars.” And the devil handed back to the man the same valise that the man had just handed to him.

関連リンク

• 等価変換な日々
  • The Coq Proof Assistant A Tutorial (9) 排中律の証明
  • The Coq Proof Assistant A Tutorial (11) 排中律の証明 (完結編)
• sumiiの日記 - callccによる排中律の証明
• d.y.d.
  • d.y.d. - Curry-Howard Isomorphism
  • カリー・ハワード
• 欝っぽい日記 - ブラウアーの考えたこと

λ. Messenger が落ちる

最近、Windows Live Messenger が頻繁に落ちる。 メインウィンドウで表示されているFlashが原因のようで、Flashプラグインの内部で落ちているようだが……困った。

• Flash Player が原因で発生した問題

λ. ACミラングッズ プレゼントキャンペーン

住信SBIネット銀行が「ACミラングッズ プレゼントキャンペーン」なるものをやっていたので、定期で5万円預けてみた。

λ. 黄泉比良坂(よもつひらさか)の岩戸

ディスコミュニケーションの第9話「まなつのよるのゆめ」に「千年ぶりに黄泉への岩戸が開く瞬間を……」というセリフがあったのだけど、古事記の舞台は千年前よりもずっと昔の話だし、ここで千年前に岩戸が開いたと言っているのは何を指しているのだろう?

λ. A Bisimulation for Type Abstraction and Recursion by Eijiro Sumii and Benjamin C. Pierce

住井さんが第７回船井情報科学奨励賞という賞を受賞した*1とのことで、よい機会なので、記事で関連論文としてあがっていた A Bisimulation for Type Abstraction and Recursion のPOP2006のときのスライドを眺めてみる。 以前に少し伺ったこともあったけど、これは想像以上に面白そう。

λ. 第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

λ. MPSファイルのフォーマットは酷すぎる

線形計画(LP)や混合整数計画(MIP)の問題の記述に標準的に使われているMPSというファイル形式があるのだけど、そのフォーマットが酷すぎて呆れた話。

経緯

MIPLIB2010の簡単な問題ということで、enlight13 を色々なソルバに食わせて遊んでいたら、GurobiとSCIPは解を見つけるのに、自作ソルバは解がないと言ってきて、どんなバグを埋め込んでしまったかとかなり焦った。 焦ってしばらくバグ探しをした後に、ふとGLPKでも解いてみると、GLPKも解がないと言ってくる。それで、自作ソルバに食わせるためにGLPKでファイルをMPSファイルからLPファイルに変換していたのを思い出し、GLPKのMPSファイルの解釈がGurobiやSCIPと違うのではないかと疑った。 GLPKで変換したファイルをGurobiやSCIPに解かせて解がないという結果になるのを確認。さらに色々見ていると、GLPKのログメッセージでは変数は全部binaryなことになっているけれど、Gurobiの出力した解をみてみると2とかになっているのがある。これだ！

分かったこと

それで、「GLPK MPS bug」で検索してみると、 Re: [Bug-glpk] GLPK 4.46 fails to find solution with enlight13.mps というメールを発見し、原因箇所が判明。件のファイルのBOUNDSの指定に問題があるらしい。

ただ、それだけだと、GurobiやSCIPと解釈が違う理由は分からなかったので、MPSファイルについてさらに調べてみる。 すると、CPLEX では Special Records in MPS Files: ILOG CPLEX Extensions によれば、「MARKERで整数変数を指定する場合、その変数の範囲指定がBOUNDSセクションに存在しない場合には、範囲は[0,1]になる」ということらしいが、その辺りが解釈が違っているのが分かった。

問題のMPSファイルではBOUNDSセクションで変数の下限のみしか指定していなかった。GLPKの実装は、範囲をまず[0,1]で初期化した上で、BOUNDSセクションに記述された上下限でそれらを上書きするという実装になっていたため、上限は1のままになってしまっていた。 それに対して、GurobiやSCIPはどうも下限だけとはいえ範囲が指定されているので[0,1]というデフォルトはそもそも用いないようだ。 ついでに、lp_solve の MPS file format によると、lp_solveはBOUNDSセクションで下限だけでも指定されていればデフォルトは用いないようだが、ただしデフォルトは[0,1]ではなく[0,∞)だとか……

感想

歴史的経緯はあるのだろうけど、元のフォーマットをアドホックに拡張し続けて結果、歪な仕様になった上に、各ツールの解釈が全く違うというひどい状態。こんな腐ったフォーマットが現役で使われているとは酷すぎる……

参考

• MPS (format) - Wikipedia, the free encyclopedia
• Special Records in MPS Files: ILOG CPLEX Extensions
• MPS file format (lp_solve)