日々の流転

λ. おみくじ

λ. 「友人のいない自作改造マリオ」

ニコニコ動画の友人のいない自作改造マリオpart1のシリーズの動画にはまる。 後になると飽きてくるし、最初の方が面白いな。 って、こんなことしている場合じゃないのに……

λ. アクトレイザー2 動画

むかしはまったアクトレイザー2の動画をたまたまYouTubeでみかけて、懐かしさからつい見入ってしまった。私もHardを普通にクリアするくらいは出来たけど、この動画はなんと全てノーダメージ、すごいなぁ。それに音楽がまた懐かしい。

• Diligence
  • Industen
  • Benefic
• Altheria
  • Tortoise Isl.
  • Altheria
• Temponia
  • Modero
  • Demon's cave
• Justania
  • Death Field
  • Almetha
• Lovaous
  • Palace (1)
  • Palace (2)
• Leon
  • Gratis
  • Stormrook
• Humbleton
  • Tower of Souls
• Death Heim

λ. 最近のAmazon.co.jpのキャンペーン

「和書＆洋書 あわせて買うとその場で割引!」キャンペーン というのをやっていて、和書と洋書を一緒に買うと洋書が10%割り引きになるそうなので、欲しかった洋書を注文。 あと、Amazon.co.jpでEdyキャンペーン ― 今なら最大1万円分の賞品が当たる!というキャンペーンもやっていたので、支払いはEdyにしてみた。 AmazonでEdyを使う人はそんなに多くはないだろうから、何か当たるといいなぁ。

【追記】 ちなみに、買ったのは Scooped!: The Third Piled Higher & Deeper Comic Strip Collection(Jorge Cham) 。 作者から直接買うと、サインと素敵な Fridge Magnetがつくのだけど、送料をいれると $23.00USD になってしまう。 それに対して Amazon.co.jp だと¥1,432だった。

λ. (ttweb) agdaを使ってみる

メモ。置換公理から分出公理を証明したり等。

λ. 第三十六回圏論勉強会

今日は今年最初の圏論勉強会。 写真。

今回もスコットドメインとかの話で、前回「Topology via Logic (Cambridge Tracts in Theoretical Computer Science)(Steven Vickers) を持ってきておけばよかった」と書いたけど、今日も忘れてしまった(・ω・)

λ. “Foundations for structured programming with GADTs” by Patricia Johann and Neil Ghani

この論文、年末年始に読もうと思って印刷したまま積読になっていたのだけど、稲葉さんのmemo: POPL 3 - d.y.dと住井さんの POPL 2008メモ3日目 - sumiiの日記 で言及されていたのをきっかけに読んだ。

まず、基本的なGADTは以下のような形で定義される。

data G a where
   GCon :: F G a → G (H a)

このデータ型は、K t a = ∃b. (Eql (H b) a, F t b) とおく*1と、以下で定義されるデータ型と同型。

data NG a where
   NGCon :: K NG a → NG a

で、F, H がそれぞれ F : (|C|→C)→(|C|→C), H : |C|→|C| という関手のとき、K は (|C|→C)→(|C|→C) の関手となり、入れ子データ型の場合(c.f. 20061005#p02)と同様に、NG は K の始代数としてみなせる。そのため、fold/buildの定義とそのshortcut融合変換が出来る(c.f. 20060926#p02)。

圏論的に考えると、GCon と NGCon の対応は、GとNGが同型であることと、K t が「left Kan extension of Ft along H」(Lan_H Ft) であることによって与えられている。

いずれも言われてみれば当たり前なんだけど、収まるべきところに収まっている感じがする。 それと、やっぱり論文の書き方が上手いなぁ。 Haskellの構文を使いながら圏論的な議論をするやり方とかは見習いたいと思った。

λ. 米田の補題とCPS変換

檜山さんのところで米田の補題とCPS変換の関係の話が紹介されていた。まだ読んでいないのだけど、多分こういう話だろうと思うので、読む前にちょっとメモ。

「locally-small な圏 C、関手 F : C→Set、対象 A∈|C| について自然同型 Nat(hom(A,-), F) ≅ FA が成り立つ」というのが米田の補題。 ところで、自然変換と多相関数は似たようなものなので、これを多相ラムダ計算の型で書くと、大体 ∀X. (A→X)→FX ≅ FA となる。 ここで、Fとして恒等関手を用いると ∀X. (A→X)→X ≅ A となり、同型は以下のΦとΨによって表現される。

id : ∀X. X → X
id = ΛX. λx:X. x

Φ : (∀X. (A→X) → X) → A
Φ = λα:(∀X. (A→X) → X). α A (id A)

Ψ : A → (∀X. (A→X) → X)
Ψ = λa:A. ΛX. λk:A→X. k a

これはまさにある種のCPS変換になっている。

これが同型であることを多相ラムダ計算で示すには、通常の簡約規則と関数の外延性だけでは不十分で、パラメトリシティが必要になる(証明は Theorems for free! (20050218#p03) を参照)。 また、元の ∀X. (A→X)→FX ≅ FA も同様にパラメトリシティを用いて証明可能。→ 米田の補題と多相ラムダ計算

【2009-07-15 追記】 CPS A = (∀X. (A→X) → X) とおくことにする。 型 A と型 CPS A が同型なわけだけど、そうすると A→B と CPS A → CPS B も同型対応するようになる。

Φ' : (CPS A → CPS B) → (A→B)
Φ' = λg : CPS A → CPS B. λa : A. Φ (g (Ψ a))
    = λg : CPS A → CPS B. λa : A. (g (ΛX. λk:A→X. k a)) B (id B)

Ψ' : (A→B) → (CPS A → CPS B)
Ψ' = Ψ (f (Φ α))
    = λf : A → B. λα : CPS A. ΛX. λk : B→X. α (λa : A. k (f a))

ついでにHaskellで書いておく。

{-# LANGUAGE RankNTypes #-}

type CPS a = forall x. (a -> x) -> x

-- 値のCPS変換
psi :: a -> CPS a
psi a = \k -> k a

phi :: CPS a -> a
phi x = x id

-- 関数のCPS変換
psi' :: (a -> b) -> (CPS a -> CPS b)
psi' f = \x k -> x (k . f)

phi' :: (CPS a -> CPS b) -> (a -> b)
phi' g = \a -> g (\k -> k a) id

λ. Thinkpad X61 が届いた

2007-12-15 に注文した Thinkpad X61 が昨日ようやく届いたので、環境を移行中。 以下、適当にセットアップメモ。

キーマップ

まず、いつものようにCapsはCtrlに置き換える。 それから、Page Down キーと Page Up キーが右上の離れた場所にある一方、カーソルキーに隣接してブラウザキーというブラウザの「進む」「戻る」に対応するキーがあった*1ので、これまで使っていた Let's note CF-T1 にあわせて、ブラウザーキーを Page Up と PageDown にしてしまった。

Windows Registry Editor Version 5.00

[HKEY_LOCAL_MACHINE\SYSTEM\CurrentControlSet\Control\Keyboard Layout]
"Scancode Map"=hex:00,00,00,00,00,00,00,00,\
  04,00,00,00,\
  1d,00,3a,00,\
  49,e0,6a,e0,\
  51,e0,69,e0,\
  00,00,00,00

あと、Escキーも遠すぎてホームポジションから指が届かないため、F1キーか「半角/全角」キーと入れ替えてしまおうかと悩み中。

それと、Fn + ← を Home にしたいのだけど、Fn + ← のスキャンコードが分からず、まだ出来ていない。 【追記: 出来た! → Thinkpadのメディアコントロールキーの置き換え】

参考

• WindowsNT4.0にて Ctrl と Capslock を入れ替える方法。
• s30のナビゲーションキー | ThinkPad Club Archive (200/i1124/s30/is30系(13))

ホームディレクトリ

Vista になって、c:\Documents and Setting\sakai が c:\Users\sakai になったので、Cygwinのホームディレクトリも、/home/sakaiではなく/cygdrive/c/Users/sakai にししてみた。 当たり前だが、設定は環境変数HOMEだけでなく/etc/passwdにも設定が必要。 それをやっていなくて ssh ではまった。

既定のブラウザ

Googleデスクトップの設定などでブラウザが開かれる際に、既定のブラウザに設定してあるFirefox*2 ではなく、IEで開かれてしまって困った。 既定のブラウザ - 利用方法に関する質問 | Google グループの質問と同じ症状。 結局、Firefoxを既定のブラウザにしていますが、GoogleデスクトップはなぜかIE７で開かれてしまいます。 - 教えて！goo にあった方法で対処。

iTunes

iTunesはiTunesディレクトリをコピーするだけだと、iTunes管理下に置いてなかった一部のファイルが見つからなくなる。正しい対処かは知らないけど、iTunes Music Library.xml を手で書き換えたら解決した。

ついでに、幾つかのファイルのジャンルが、勝手に日本語に書き換わっている(e.g. 「Jazz」→「ジャズ」)ことに気づく。調べてみると、iTunes 7.5 の問題のようだ。7.5 が出てから二ヶ月以上経つのにまだ修正されていないのね……

【追記】 iTunes for Windows まとめ - ジャンル日英対応表 の方法で回避できるらしい)

Microsoft圧縮フォルダ (LZH)

Microsoft圧縮フォルダ (LZH) は XP 用のものが Vista でもそのまま使えるようだ。

Page Defrag

Page Defrag は Vista では使えないようだ。残念。

λ. Vista重い

しかし、Vista重いよ。 ユーザーインターフェースは着実に使いやすくなっていると思うので、この重さは残念。

メモリがたくさん必要とは聞いていたが、普通に使っているだけなのにページファイル(= 実メモリ+スワップ領域?)が2.8Gとかなっていて驚いた。 実メモリは1Gしかないので当然スラッシングが起こって、ほとんど使い物にならない。 一体どの部分がこんなにメモリを使っているのだろうか*1。

とりあえず、「コントロールパネル > システムとメンテナンス > パフォーマンスの情報とツール」の「視覚効果の調整」で「パフォーマンスを優先する」にしてみたが、気休めにしかならない……

もっとも、今のところメモリがボトルネックに思えるので、メモリを2G増設すれば快適になりそうだが……

ちなみに、Windows エクスペリエンス インデックスは以下の通り。

基本スコア

3.1

プロセッサ

5.1

メモリ

4.5

グラフィックス

3.1

ゲーム用グラフィックス

3.3

プライマリハードディスク

4.7

λ. お菓子買いだめ

先月、20071220#p01でお菓子を買いだめしたけど、また買いだめしてみた。

λ. 不吉

以前に作って使っていた腰リールのリールが切れた。不吉だ……

λ. 風邪ひいた

こりゃ風邪ひいたっぽい。

λ. X61にメモリ増設

元々メモリは自分で増設するつもりでメモリ1GBしか積んでいないモデルを選んでいて、「メモリを2GB増設すれば快適になりそう」と思ったので、価格ドットコムで一番安かったトランセンドJM667QSU-2Gを購入。5,480円 + 送料580円 = 6,060円。 安かったので相性とか少し心配だったけど、何の問題もなく認識され、Vistaが見違えるほど快適になった。

以下、Windows エクスペリエンス インデックス の変化。

基本スコア

3.1 → 3.3

プロセッサ

5.1 → 5.1

メモリ

4.5 → 4.8

グラフィックス

3.1 → 3.3

ゲーム用グラフィックス

3.3 → 3.4

プライマリハードディスク

4.7 → 4.7

λ. Re: えっと

あ、本当だ。「Thinkpad X61 を注文」と書いたときにはちゃんとX61と書いてたのに、いつのまにかX60だと勘違いしてました。こっそり修正しておこう……

「Fn + ←」は入れ替えられないのね……それはちょっと残念。 ちなみに、Windowsキーはスタートメニューの表示と Windows + D とで結構使ってます。 Vistaになって Alt + Tab でデスクトップにも切り替えられるようになったので、Windows + D はもうそんなに必要ないかも知れないけど。 あと、たまに　Windows + R とか。

λ. RHG読書会 Practical Common Lisp 第四回

7章〜10章。 Commmon Lisp のマクロ面白いな。 ONCE-ONLYマクロ、読めねぇw

関連

• [mixi] 日下部；）さん | RHG

λ. MiniSat binding for GHC

ちょっとSATソルバを使って遊んでみたいことがあったのと、ku-ma-meさんのruby-minisat とパズルのソルバ に触発されたのとで、MiniSatのバインディングを作成してみた。

• MiniSat2-0.0.1.tar.gz

C-SourcesにC++のファイルを指定しているので、GHCの使っているGCCがC++に対応していない場合、ビルドできないはず。 C-SourcesにC++のファイルを指定するというのもどうかと思うが、Distribution.Makeモジュールを使う方法は面倒くさすぎるし。

あと、インターフェースはRubyバインディングに比べてイマイチ。 特に、変数からリテラルに明示的に変換しなくてはいけないのが面倒くさい。 リテラルを変数のスーパータイプとして定義できると良いのだが……

【追記】 Githubにレポジトリを作成しました。 <URL:https://github.com/msakai/haskell-minisat>

λ. ProLogICA: a practical system for Abductive Logic Programming by Oliver Ray and Antonis Kakas

PrologICA は SICStus Prolog 上にメタインタプリタとして実装された発想論理プログラミング(Abductive logic programming, ALP)の処理系。特徴は変数を含む仮説(non-ground abducibles)を扱わず、複雑な制約解消も行わない点。そのため、複雑な最適化問題等は扱えないが、そうでない実際の問題については他の処理系よりもかなり高速みたい*1。 また、light-weight なので組み込みやすいとか。

それから、Kakas and Mancarella のアルゴリズムと高速化のテクニックが分かりやすく、勉強になった。

参考

• 知識発見法(2007年度)

λ. 連言標準形への変形

ふと、論理式の連言標準形(Conjunctive normal form, CNF)への変形を素朴に書いてみたのだけど……イマイチ。

type Var = Int

data Formula
    = Var Var
    | Not (Formula)
    | And [Formula]
    | Or [Formula]
    | Imply Formula Formula
    | Equiv Formula Formula

data Lit = Pos Var | Neg Var
type Clause = [Lit]
type CNF = [Clause]

toCNF :: Formula -> CNF
toCNF = f
  where
    f :: Formula -> CNF
    f (Var v)     = [[Pos v]]
    f (Not a)     = g a
    f (And xs)    = concatMap f xs
    f (Or xs)     = cnfOr (map f xs)
    f (Imply a b) = f (Or [Not a, b])
    f (Equiv a b) = f (And [Imply a b, Imply b a])

    g :: Formula -> CNF
    g (Var v)     = [[Neg v]]
    g (Not a)     = f a
    g (And xs)    = cnfOr (map g xs)
    g (Or xs)     = concatMap g xs
    g (Imply a b) = g (Or [Not a, b])
    g (Equiv a b) = g (And [Imply a b, Imply b a])

    cnfOr :: [CNF] -> CNF
    cnfOr = foldr (\xs ys -> [x++y | x <- xs, y <- ys]) [[]]

Imply や Equiv の処理で再帰呼び出しの部分は、定義を展開して特殊化したコードを出力してほしかったのだけど、inline 組み込み関数を使ってもそれは無理だった。しょうがないと言えばしょうがないけど、うまい方法はないものか。

λ. MinCamlコンパイラ by 住井英二郎

MinCamlについての「ソフトウェア論文」 - sumiiの日記 より。 これは分かりやすい。

ところで、「本稿では学部3年生程度の教育を目的とした、非常に単純な関数型言語のコンパイラであるMinCamlについて解説した」って「学部3年生程度」というのが妙に細かい気がw

関連

• 2時間で真似(まね)ぶ関数型言語のコンパイラ - ヒビルテ(2006-09-12)

λ. ベジダイニング

野菜がおいしい。