日々の流転

λ. Cleanの定関数と定グラフ

<URL:http://d.hatena.ne.jp/lethevert/20060601/p1> より。

Haskellはグラフ書き換えによる意味論を言語仕様に採用していないので、言語仕様上はCleanの定関数や定グラフのような概念は存在しない。というか、そもそもHaskellの言語仕様は実行メカニズムをほとんど規定していない。では実際の処理系ではどうかというと、例えばGHCでは(ある種の最適化後に)ラムダ抽象以外の形をしている定義は、すべてCleanでいうところの定グラフとしてコンパイルされる。

full laziness transformation

また、full laziness transformation (full laziness optimisation, let-floating) によって、局所的な定義が大域的な定義に引き上げられることがあるので、大域的か局所的かの区別も存在しない。 この full laziness transformation は大概は有用なのだが、時々困ったことをしてくれることもある。たとえば、以下のプログラムをコンパイルして実行するとメモリを食いつぶす。

f :: Int -> Int
f n = xs !! n
    where xs = [0..]

main :: IO ()
main =
    do print (f maxBound)
       print (f 0)

何故なら、full laziness transformation によって xs がトップレベルに引き上げられ、以下のようなプログラムと等しくなるため。結果、fが生きている限りxsも生きていることになり、メモリを食いつぶしてしまう。なお、「print (f 0)」を削除するとfがGCされxsもGCされるので、メモリを食いつぶすことはない(GHCではCleanと異なりCAFもGC対象になる)。

f :: Int -> Int
f n = xs !! n

xs :: [Int]  
xs = [0..]

main :: IO ()
main =
    do print (f maxBound)
       print (f 0)

では、こういうときにはどうするかというと、「-fno-full-laziness」というオプションを使って full laziness transformation を抑制してやる。全くしょーもないバッドノウハウである。

……とはいえ、Haskellはグラフ書き換え系を意味論として採用しておらず、おそらく今後とも採用しないことを考えると、言語自体による対応ではなくオプションやプラグマによって対応するというのは妥当なところだろう。個人的にはグローバルなオプションではなく、個々の定義に対して full laziness transformation を抑制するためのプラグマを付けられると良いと思うのだが……。

Cleanの定関数を模倣する

そして、Cleanの定関数のように「計算結果を共有せず毎回計算を行いたい」ときには、

• ダミーの引数(通常はユニット型)を加えた上で
• -fno-full-laziness で full laziness transformation を抑制すればよい

(FIXME: 具体例を追記)

これも面倒なので、プラグマがあると良いのではないかと思う。

λ. Turnabout

メモ。<URL:http://d.hatena.ne.jp/tapot/20050629> より。

これまでIEでGreasemonkeyのスクリプトを使うにはTrixieを使っていたが、これはTrixieよりも良さそうだ。

λ. 人狼審問 : (1507)紡績の村

観戦中。 ボブが面白い。

(追記) 速攻で決着がついている。ボブは「ひょっとして日本人じゃね?」と薄々思ってはいたけど、日本人だったwww　あと、職場のPCで日本語が入力できないなら Ajax を使った日本語 Full IME を使うという手もあったのに、とちょっと思った。

関連リンク

• B1/1453村 - 人狼ファンWiki

λ. Re: FirefoxのEUCの独自拡張のセンスが最低な件について

確かにFirefoxは「IANAに登録されたEUC-JP*1とCP51932のどちらでもないキメラなエンコーディングのデータをサーバに送り出す」という点では非常にuglyだと思うし、それについては全く異論は無い。そういうデータをサーバが正しく処理できないのもFirefoxが悪い。

だが、IEでの文字化けはIE自身の問題だし、IE対策に補助漢字を実体参照に変換するかどうかもサーバ側の問題だろう。これらの問題は仮にFirefoxがキメラなエンコーディングではなくIANAのEUC-JPというまっとうなエンコーディングでデータを送っていたとしても*2発生するものだ。そういったものまでFirefoxのこの問題のせいにするのはどうかと思う*3。

この問題、Firefoxに関してはどうするのがベストか私には分からないが、対症療法については簡単だ。サーバ側がaccept-charset属性を指定して最初からUTF-8でデータを受け取れば良いだけのことだ。もし「現在のWeb環境でサーバ側のソフトはほぼ漏れなくUnicodeで動作している」のなら、対応してもらうのも簡単だろう。

(以下色々と書こうとしたが削除)

それにしても、文字コードというのはやっかいなものだな。

λ. 限量子の書き方色々

限量子の書き方にも色々な流儀がある。

1. ∀x∈D. P(x)
2. (∀x∈D)(P(x))
3. ∀_x∈D P(x)

僕はこの最初のやつを普段使っていて、他のは廃れて欲しいとかねがね思っているのだけど、欝っぽい日記(2006-05-22)で「プリンキピア・マテマチカにさかのぼる由緒ある記法」と書かれているのを見つけて、何だか少し嬉しかった。まあ、どうでも良い話ではあるが。

λ. 共通部分式の除去 (CSE, Common Subexpression Elimination)

命令型言語であっても共通部分式の除去が必ずしも性能を向上させるとは限らないが、純粋関数型言語では特にそうである。例えば、以下のようなリストの「冪集合演算」を考えてみる。

power :: [a] -> [[a]]
power []     = [[]]
power (x:xs) = power xs ++ map (x:) (power xs)

main :: IO ()
main = print (length (power [0..30]))

このpowerの二つ目の等式の右辺には power xs が二回現れているので、これを一度変数に束縛して以下のようにすることが考えられる。しかし、こうするとxssがなかなかGC対象にならないのでメモリを食いつぶしてしまう。

power :: [a] -> [[a]]
power []     = [[]]
power (x:xs) = xss ++ map (x:) xss
    where xss = power xs

このようなことを避けるためにGHCはCSEを行わない……のかな(?)。FAQの Does GHC do common subexpression elimination? には「同じ式が既に変数に束縛されている場合」にのみCSEを行うという "opportunistic CSE" について書いてあるが、ちょっと試した限りでは実際にこれが起こるのを確認できなかった。

いずれにしても、、プログラマは計算結果を共有したい時には明示的に変数に束縛すべきだろう。なお、-fno-cseオプションを使うことでCSEを完全に無効化出来るようだ。

より効率の良い冪集合演算

なお、冪集合演算については、より効率の良い定義が存在する。 ただし列挙される順序は異なるが。

power :: [a] -> [[a]]
power []     = [[]]
power (x:xs) = xss /\/ map (x:) xss
    where xss = power xs

-- interleave
(/\/) :: [a] -> [a] -> [a]
[]     /\/ ys = ys
(x:xs) /\/ ys = x : (ys /\/ xs)

λ. 人狼審問閉鎖

9月一杯くらいで閉鎖予定か……

少し寂しいな。

• <URL:http://jbbs.livedoor.jp/bbs/read.cgi/game/17792/1096682947/98>
• mixi:人狼審問:審問9月で閉鎖

λ. Kconv.kconv と Iconv.conv の引数の順序

似た機能なのに引数の順序が Kconv.kconv(str, to, from) と Iconv.conv(to, from, str) で異なっている。ちと紛らわしい。

λ. 知識発見法

Alephを使った実習。 バイアスの設定、正例のみからの学習、一貫性制約の発見。 Alephの挙動がなにやら不思議。

しかし、モード宣言で入力が「+」で出力が「-」というのは、ちょっと直観に反するような。……圏論での exponential functor の variance と、CPLでのvarianceの表記法から、入力が「-」で出力が「+」だとつい連想してしまうので。

λ. 古川研:Abduction勉強会

Hierarchical planning に関して。

• from first principles = 元々の原理から
• circumscription
  • <URL:http://en.wikipedia.org/wiki/Circumscription>
  • 極小限定?
  • どういう場合に predicate completion に落ちるのか?

λ. OrdのcompareでNaNを比較

OrdクラスのcompareメソッドでNaNを比較してみたら、何と比較しても常にGTが帰ってきた。

Prelude> let nan = 0/0
Prelude> nan
NaN
Prelude> compare nan nan
GT
Prelude> compare nan 0
GT
Prelude> compare 0 nan
GT

そこで、Ordのインスタンスが全順序集合であることを期待しているコードにNaNを放り込むと、変なことが起こる。例えばData.Map。

Prelude> :module +Data.Map
Prelude Data.Map> let m = insert nan 0 empty
Prelude Data.Map> m
{NaN:=0}
Prelude Data.Map> insert nan 1 m
{NaN:=0,NaN:=1}
Prelude Data.Map> lookup nan m
*** Exception: user error (Data.Map.lookup: Key not found)

λ. 今日のITシステム

• -
• -
• A Diagrammatic Inference System for the Web

僕は参加しなかったが、今日のITシステム後には人生ゲームをしていたらしい。人工知能学会創設20周年記念の「Happy Academic Life 2006: 研究者の人生ゲーム」というやつ。

λ. 正則性公理

<URL:http://d.hatena.ne.jp/kururu_goedel/20060608/1149748301>

数学ではともかく計算機科学では、正則性公理が直接役に立っている話はあまり聞かないし、むしろ循環構造を素直に集合として表現出来なくなるので、計算機科学では正則性公理はあんまし嬉しくない気がします。

そのような構造として例えばストリームがあります。 ストリームを集合論で扱うには、集合Aの要素からなるストリームの全体を「S = A×S を満たす最大のS」として、0,1,0,1,… というストリームは s = (0,(1,s)) という集合で扱うのが直観的で自然だと私は思います。しかし、これは反基礎の公理(AFA, Anti-Foundation Axiom)を公理にした集合論では可能ですが、正則性公理=基礎の公理(FA, Foundation Axiom)を公理にした集合論では不可能ですし。まあ、S = A×S ではなく S ≅ A×S に弱めれば正則性公理にも矛盾しないので、本質的な問題というよりはむしろ利便性の問題と思いますが。

おまけ

『反基礎の公理』について書こうとしたら、Myブログ軍師に「我が君･･･。『反基礎の公理』についてですか？　炎上も覚悟の上でしょうな 」と言われたので、やめておく。

追記 (2006-06-20)

くるるの数学ノート - Antifoundation で、Aczelの『Non-well-founded sets』のPDFが公開されていることを知った。原典は向井先生の本棚にあったのをパラパラめくったことしかなかったので、後でちゃんと読んでみたいところだ。

それから、かがみさんの日記に以下のように書かれていた。「推移的崩壊」(transitive collapse)って何だろう。

Axiom of regularity に関してもちょっと書きたいことありなのですが、ぼろぼろになりそうなので今度機会があったら...。ただし、AFA を認める立場で Axiom of regularity が adhoc であるという批判 は成り立たないと思います(もちろん nuc さんが AFA を認めないというなら話は別ですが)。明らかに AFA の方が adhoc だと思うし、そもそも Axiom of regularity からのアイディアと思われる「推移的崩壊」をちゃっかり借用してるし。

fj.sci.math のこのスレッドには以下のように書かれていて、transitive collapse というのは Mostowski's collapsing lemma に関係した概念のような気がするが…… Mostowski's collapsing lemma 自体よく知らないのでした……とほほ。

「うそつき」では、AFA のことを、「Mostowski の Collapsing Lemma を、グラフが well-founded という仮定をはずした形に拡張したようなものだ」というような感じ(この通りの書き方ではない)で説明していました。これはちょっと公理的集合論を知っている人にはわかりやすい説明だと思います。

追記 (2006-06-21)

<URL:http://en.wikipedia.org/wiki/Mostowski_collapse> 読んで、Mostowski's collapsing lemma がどういうものか少し分かってきた。

λ. 『ハツカネズミの時間』 冬目 景

閉塞感を淡々と描いているという印象を受けた。

λ. 中間リストの除去とRULESプラグマ

<URL:http://haskell.g.hatena.ne.jp/nobsun/20060609>

「map f $ zip xs ys」を「zipWith (uncurry f) xs ys」に書き換えたくなるという話。実はGHCだと、前者のコードでもRULESプラグマによって最終的には「foldr2 (\x y r -> f (x,y) : r) [] xs ys」のようなコードに変換されるので、いちいち手で書き換える必要はない。

GHCではリストに関する有用な書き換え規則がRULESプラグマとして大量に定義されている。ただ、最適化のためにRULESプラグマを大量に用いるというのはやはりアドホックだと私は思うし、こういうことが出来るのはリストが標準のライブラリで、かつ非常によく使われるデータ構造だからだろう。これらの規則と同等の規則を自分で作ったデータ型に対して定義するのは非常に大変で、しかもGHCの最適化のフェーズについて理解している必要がある。

λ. outer product と cross product

<URL:http://d.hatena.ne.jp/w_o/20060607#p3> へのコメントとして、「内積や外積は inner product や outer product の直訳ではないかと」と書いたが、outer product と corss product、そして innter product と dot product は厳密には等しくないという話がある。後で読む。

• <URL:http://groups.google.com/group/sci.math/msg/836ab7a3551a6866>

λ. RubyKaigi2006 (1日目)

• 参加者の1/4くらいは知った顔じゃないかと勝手に思ってたが、ぜんぜんそんなことはなかった。世間は広い(ぉぃ
• BTSで個人的な案件管理というのは自分でも考えたことはあったが、gotokenさんの発表を聞いて、実践してみたくなった。とりあえず、影舞いれるか。
• 「お知らせ」のような案件じゃないものもカテゴリとして登録しておいて、一番上に表示するというノウハウが面白い。
• akrさんの発表の「自発的にライブラリを作ろうと思い立つ人は自分自身の望みを持っているはず。初心忘れるべからず。規格を調べるうちに忘れてしまうことが多い」というのに耳が痛い。
• Rails の Binding.of_caller の実装が邪悪すぎて感動した。継続とtrace_func との組み合わせなんて良く考えたものだ。
• Ruby/Tkの 永井 秀利 さんと、Ruby/Tk や Ruby-GNOME2 のことについて話す。
• gotokenさんと、樋口さんのnonameの話
  • inductiveなデータ型とcoinductiveなデータ型の区別。totalな言語なら当たり前。partialな言語で両者をきちんとサポートしつつ区別している言語は存在するか?
• 隠蔽代数(Hidden Algebra)とCafeOBJ。勉強しようと思いつつ手を付けられていない。檜山さんが<URL:http://d.hatena.ne.jp/m-hiyama/20060119/1137641539>で紹介していた Joseph Goguen, Grant Malcolm “A Hidden Agenda” (1997) [citeseer,CiteULike] を読むのが良いのかな?
• その他色々な人にお会いした。

λ. x² + y² = r であるような (x,y) の列挙

<URL:http://d.hatena.ne.jp/mzp/20060603/1149861488> より。

与えられた自然数 r に対して x² + y² = r であるような， (x,y) (ただし x >= y >= 0)の組を全てリストとして列挙する関数 squares r を定義せよ．(検算用資料: r = 48612265 の時 32 個の解があるそうです．)

リンク先の解答では 0 ≦ x ≦ √r の範囲でxを列挙しているが、ここでは 0 ≦ y ≦ √(r/2) ≦ x ≦ √r なので、列挙する範囲をより小さくし、同時にチェックも削ることが出来る。

import Control.Monad

squares :: Integer -> [(Integer, Integer)]
squares r =
    do y <- [0 .. floor (sqrt (fromIntegral r / 2))]
       let x2 = r - y*y
           x  = floor (sqrt (fromIntegral x2))
       guard (x*x == x2)
       return (x,y)

λ. Fast and loose reasoning is morally correct. Nils Anders Danielsson, Jeremy Gibbons, John Hughes and Patrik Jansson.

を読んだ。

• <URL:http://portal.acm.org/citation.cfm?id=1111320.1111056>
• <URL:http://jp.citeulike.org/article/665357>
• <URL:http://www.cs.chalmers.se/~nad/publications/danielsson-et-al-popl2006.html>
• スライド
  • <URL:http://www.cs.chalmers.se/~nad/publications/danielsson-popl2006-talk.pdf>
  • <URL:http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/wg21/meeting61/PJ/>

λ. RubyKaigi2006 (2日目)

• dRubyは最近使ってなかったので懐かしいな。
• Railsで日本語を使う際の話なんかも出ていたので、むとうさんも来てRuby-Gettextを宣伝すればよかったのに、と思った。
• ActiveRecordでSyslogという名前のテーブルを作ってロギングするという話が少し面白かった。
• Haskellで書いたパーサをrubyから利用出来ないかと聞かれる。CからHaskellを呼ぶことは出来るので、拡張ライブラリを書けばRubyからHaskellを呼ぶことも出来る。ただ、パース結果のデータ構造をRuby側で扱える形に変換するのが結構大変そうな気がする。
• DHHの講演は英語は聞き取りやすかったし内容も面白かった。ただ、マイクの音が大きくて耳が痛くなった。
• しかし、Rails使いがこれほど多いとは思わなかった。別にRailsに文句があるわけではなく、Webアプリケーションに関わっている人がこれほど多いということに驚いた。
• RubyCocoaのhisaさんとお話した。
• Haskell で Cocoa を使うための HOC というものがあるそうだ。
• 

λ. 時相論理メモ

萩谷先生の時相論理メモを読んだ。

練習問題

3人の哲学者問題に関して，(経路πにおいて) 0番目の哲学者が飢餓に陥るということをPLTLで表せ．

π |= G(¬eating0) もしくは π |= ¬F(eating0)

0番目の哲学者が飢餓に陥る経路が存在するということをCTLによって表せ．

s |= EG(¬eating0) もしくは s |= ¬AF(eating0)

PLTLにおいて，経路πに対して「G F q」が成り立つことと，πの中でqが無限回成り立つことが等価であることを説明せよ．

π |= G F q iff (∀k. πk |= F q) iff (∀k. ∃l. π(k+l) |= q) だから。ってことで説明になってる?

3人の哲学者問題に関して，PLTLでstrong fairnessを表せ．たとえば，0番目の哲学者が左のフォークを取るというアクションに対して，enabledとchosenはどのように表せるか．(picking0やeating2などを用いて表せ．)

よくわかんない。後で考える。

Petersonのアルゴリズムに対するunconditional fairnessを書き下せ．

Petersonのアルゴリズムを知らないので、後で考える。

λ. 知識発見法

SVM(サポート・ベクタ・マシン)。 考えは分かるんだけど、こまかい部分がいまいち追っていけないなぁ。

λ. 古川研:Abduction勉強会

• floundering in negation-as-failure
• fluent range restricted condition
• range-restricted でないものに対して、否定をとってはいけない
• deductive databaseでは常識
• combination ではなく、permutation なのは何故?

λ. 100円スピーカー

ダイソーで100円のスピーカーが売っていたので、買ってきて iPod nano に繋げてみる。音質も当然相応のものでしかないけど、100円と思えば不満もない。

λ. evaluate a と a `seq` return a の違い

Control.Exception の evaluate :: a -> IO a と evaluate' a = a `seq` return a で定義した evaluate' :: a -> IO a の振る舞いは異なる。evaluate ⊥ ≠ ⊥ = evaluate' ⊥。しかし、これがControl.Exceptionモジュールにあるのは何でだろうね。

λ. 今日の IT system

• Ghost Researcher
• 修論をブログで書く。Web 2.0

λ. 融合変換の簡単な例

N = μX.1+X として、double = fold [zero, succ.succ] : N -> N という関数があったときに、double . double を融合することを考える。double は (N, [zero,succ]) から (N, [zero, succ.succ]) への準同型であると同時に、(N, [zero, succ.succ]) から (N, [zero, succ.succ.succ.succ]) への準同型でもあるので、double . double = fold [zero, succ.succ.succ.succ] であり、これが目指す結果である。

具体的にどう変換するか。 doubleを(N, [zero, succ.succ]) からの準同型にするような代数を探すのは中々面倒だけど、ここでは double = build (λ[z,s]. fold [z, s . s]) が成り立っているので、以下のように変換することができる。

double . double
= fold [zero, succ . succ] . build (λ[z,s]. fold [z, s . s])
= { fold/build shortcut deforestation }
  fold [zero, (succ . succ) . (succ . succ)]
= fold [zero, succ . succ . succ . succ]

なお、ここでのbuildは以下で定義される関数である。

build : (∀X. (1+X -> X) -> X) -> N
build h = h [zero, succ]

関連エントリ

• 酸性雨定理 (Acid Rain Theorem)
• fold/build shortcut deforestation

λ. どんな場合にポイントフリースタイルを使うべきか

<URL:http://d.hatena.ne.jp/lethevert/20060613/p3> より。

私の場合、ポイントフリースタイルを使うのは圏論の概念に基づいて考えるとき。だから、射の結合, 関手, 随伴, etc と解釈できるものについてはそれぞれ射になるまで必要な引数を明示的に与える。

例

• f . g
• map h
• either f g
• foldr c n
• unfoldr phi
• arr f >>> g

結局、関数型の値はポイントフリーにせずに明示的に受け渡すのがほとんど。もちろん、cartesian closed category で考えれば、関数型の値をポイントフリースタイルで受け渡すことに何の問題もないけど、それによってコードが分かりやすくなることはあまりないと思う。

実際、rmap = map . flip ($) のような書き方はかなり気持ち悪いと感じる。圏論の何らかの概念を利用できているわけでもないのだから、愚直に rmap a fs = [f a | f <- fs] と書いた方が良い。どうせ、長さは数文字しか違わないし、これなら誰にでも一目で意味がわかる。

追記 (2006-06-21)

ところで、A New Notation for Arrowsのページには以下のように書かれていたりする(強調は私によるもの)。

Recently, several workers have proposed a generalization of monads, called variously “arrows” or Freyd-categories. The extra generality promises to increase the power, expressiveness and efficiency of the embedded approach, but does not mesh as well with the native abstraction and application. Definitions are typically given in a point-free style, which is useful for proving general properties, but can be awkward for programming specific instances.

λ. 発表練習

とても勉強になりました。 本当にありがとうございます。

λ. 『ふつうのHaskellプログラミング』読書会

第一部を読んだ。 p.26でIOアクションについて「アクションもHaskellの値ですが、不思議なことに、その値を評価すると入出力などが実行されます」と書かれているのが気持ち悪かった。それ以外はとても良く書けていた。

λ. reallyUnsafePtrEquality# :: a -> a -> GHC.Prim.Int#

GHC.Extsに reallyUnsafePtrEquality# :: a -> a -> GHC.Prim.Int# という素敵な関数を発見した。ただ、これは同じサンクであるかを比較するもので、例えばaとid aは同じとみなされない。さらに、id aをwhnfに簡約した後も同じとは見なされないようだ。実装を考えれば当然か。サンクのupdateにindirectionを使う場合なら、GCでindirectionが除去されることで同じになることもありそうな気がするが、どうだろう。

λ. 知識発見法

• SVMのカーネル法
• 主成分分析と回帰の違い

λ. 古川研:Abduction勉強会

• <URL:http://casbah.ee.ic.ac.uk/~mpsha/planners.html>
• graphplan
• イタリア人は I don't know nothing. のような言い回しをしてしまうことがあるとか。

λ. 『お笑い北朝鮮—金日成・金正日親子長期政権の解明』　伊藤 輝夫

を読んだ。

λ. 発表で気をつけること

メモ。

• スライド一枚一枚に目的を
• purpose と objective
• ゆっくり落ち着いて話す

使ったスライド: interview1.ppt

λ. 今日のITシステム

• SweetDeal: Representing Agent Contracts with Exceptions using XML Rules, Ontologies, and Process Descriptions. <URL:http://citeseer.ist.psu.edu/grosof03sweetdeal.html>
• P2PMetaShare

λ. 人狼SNS

というのが出来たそうだ。OpenPNEを使ってる。

どんな感じなのか知りたいので招待きぼー

λ. That Logic Blog: Linear Logic - Naturally!

を読んだ。

λ. 『自由は進化する』 ダニエル・C・デネット(Daniel C. Dennett) 著　山形浩生 訳

読もうと思ってたが途中で挫折。予想される反論を潰すのにかなりスペースを費やしているが、しょーもない説に対する反論をいちいち読むのは、時間の無いときにはイライラするな。他の説への反論は良いからあんたのアイディアを早く聞かせてくれよ、と言いたくなる。

それから、最上さんが以前に日記に書いていた「意識については西洋哲学はかなり酷いドグマの集合」というのにはまったくもって同感だ。この本で否定されている考えにはしょーもないものが多すぎる。

λ. IMAPに移行

これまでサーバ(kencho)にログインしてmewでメールを読むというoldtypeだったのだけど、最近色々と嫌になったのでIMAPを使うことにした。まず、「mh2maildir -courier -f -r -R Mail Maildir MH」でMH形式からMaildirに変換。これが10時間くらいかかった。単に適当な名前でコピーするだけかと思ったら、色々やってるのね。で、メーラには何を使おうか悩んだけど、とりあえずは使い慣れたMewをMeadow2上で使うことに。ネットワークが遅いと結構辛いが、Stunnelに「compression = zlib」という設定を加えたら少し快適になった。

そういや、ximapdも便利そうだなぁ。

λ. That Logic Blog: Proofs as Games

を読んだ。

λ. 『私の脳科学講義』 利根川 進

を読んだ。 自分が何をすべきか判断出来、そしてそれを基準に物事を決めていける人間は強いな。 やってみれば別にたいしたことでもないことを、面白いと勘違いして、時間を浪費している暇などない。

Quotation (p.146)

人生は面白く生きないといけないという価値観を至上において、リスクを負いながら自分の道を切り開いていく。そういう人が、何かをやり遂げると思います。かんたんな言い方をすると、人生はかぎられているから、何か自分のやりたいことを見つけて、それをすることに人生を賭ける。それをするために、他のすべてのことを決めていくというふうにすると、何か出来る可能性があるということです。

λ. Functional pearl: i am not a number -- i am a free variable. Conor McBride, James McKinna

を読んだ。 しかし、変数とか束縛ってのは毎度悩ましいものだね。

• <URL:http://portal.acm.org/citation.cfm?id=1017477>
• <URL:http://jp.citeulike.org/article/3319>

λ. Re: 推移的崩壊とAFA

<URL:http://evariste.jp/kagami/diary/0000/200606.html#20060624-1>

かがみさん、はじめまして。集合論雑記は以前から時々読んでいました(^^　集合論をきちんと勉強していないものにとっては非常にありがたかったです。今回も詳しい説明ありがとうございます。おかげで、推移的崩壊と Mostowski's collapsing lemma についてはだいぶよく理解できました。

で、AFAについてですが……　等号の検証はそういう形で書くと難しそうに見えるかもしれませんが、実際にはそれほど難しく感じたことはないです。coinduction proof principle では x = y を証明するために xRy が成り立つような bisimulation R が存在することを証明しますが、coinductipn proof principle はある意味 ∈-induction の双対みたいなものなので、こっちだけがそんなに難しいことはないとも思いますし。

また、decoration や AFA はたとえ正則性の公理や推移的崩壊の概念がなくとも、余代数方面のアイディアから生まれたのではないか、と個人的には思っています。というのも、集合全体を余帰納的に定めようとすると、つまり集合全体のクラスが冪集合関手(をクラスに拡張したもの)の終余代数(final coalgebra)になるようにしようとすると、結局 decoration や AFA のような概念は自然に出てきそうな気がするので。

……最初にも書いたように集合論についてはまったくの素人なので、変なことを書いていたら済みません。

追記 (2006-06-26)

<URL:http://evariste.jp/kagami/diary/0000/200606.html#20060624-1>

coalgebra等の簡単な解説は近いうちに書こうと思いますが、別に圏論の深い理解が必要とかそんなことはなくて、結構簡単な話です。とりあえず、coalgebraとcoinductionのチュートリアルとしては、B. Jacobs と J. Rutten の A Tutorial on (Co)Algebras and (Co)Induction. (<URL:http://www.cs.ru.nl/~bart/PAPERS/index.html>) あたりになるのかなぁ……

それから、私もくるるさんに集合論の中で推移的崩壊がどう使われるかを教えてもらえるのを楽しみにしています :-)

λ. 正三角形と垂線の問題

一辺の長さが6の正三角形の内側のある点から各辺に垂線を下ろしたところ、そのうち二本の長さはそれぞれ1と2だった。残り一本の垂線の長さはいくつか?

ずいぶん前に書こうと思っていたので、いまさらな感じだが。

λ. L.L.Ring の Language Update

すでに セッション内容と参戦者の一覧 に出ていますが、今年は Language Update で発表させていただくことになりました。よろしくお願いします。

そういえば、OCamlはsoutaroさんなんですね。楽しみ。

λ. 知識発見法

• MAP推定
• 最尤推定
• ナイーブベイズ
• ベイジアンネットワーク
• Rich Caruana and Alexandru Niculescu-Mizil. An Empirical Comparison of Supervised Learning Algorithms

今日はAbduction勉強会はお休み。

λ. サイコクラッシャーでマリオ

λ. 面接

面接に行ってきた。

使ったスライド: interview2.ppt

λ. 今日のITシステム

エレベータが整備中だった。

• Kademlia
• Trust Networks on the Semantic Web
• 3次元ビジュアルプログラミングシステム3DPPの構築に向けて

調子にのって、mixiで「太田さんの修論サポート」というコミュニティを作ってしまった。mixiでコミュニティ作るのは初めてなんだが、こんな感じになってるのね。しかし、半年後は我が身……

λ. 高収入アルバイト

• <URL:http://www.tg-w.com/woman/comic_00_01.html>
• <URL:http://mixi.jp/view_diary.pl?id=157319160&owner_id=609805>

wwww

λ. 『大学の話をしましょうか—最高学府のデバイスとポテンシャル』 森 博嗣

を読んだ。 森博嗣ならこう考えるだろうなという内容で、あまり驚きはなかった。

λ. 人狼審問 : (1569)沼地の村

プロローグの空白発言が面白くて、少し観戦していた。

関連リンク

• B1/1596村 - 人狼ファンWiki

λ. 一般常識診断

霞が関を大いに盛り上げるための官僚の団 (2006-06-24) より。

結果

あなたの一般常識の総合正解率は84.0 ％です
たいへん優秀な成績です。就職試験などで課せられる一般常識テストでは良い結果を得られると思います。

政治 90.0％
経済 90.0％
法律 80.0％
歴史 80.0％
国語 80.0％

たしか間違えたのは「国連への加盟時に加盟申請後，必要な手続き」「日本興業銀行の発行する割引金融商品」「通常国会は年に何回召集されるか？」「離婚前に妊娠していた場合を除き、女性が離婚後、結婚できるのは何ヶ月を経た後か？」「日米安全保障条約の内容として誤っているもの」「日本以外で、第一次世界大戦に参戦したアジアの国」「カツアイして説明する」「朝がおにつるべとられてもらい水、の作者」の問題。

特に「通常国会は年に何回召集されるか？」と「日米安全保障条約の内容として誤っているもの」と「日本以外で、第一次世界大戦に参戦したアジアの国」の三問が分からなかったのは、ちと恥ずかしい orz

知り合いの結果

• nextさん
• chikoさん
• yaizawaさん
• soutaroさん
• sydsydさん

λ. となりの８０１ちゃん

なんか、「となりの８０１ちゃん」というブログを紹介されたのだが、これ凄いね。

λ. ICPC国内予選

私は今年はもう参加できないなんだよなぁ。去年参加したときは面倒くさいとか思ってたが、悔しかったのでまた挑戦したかった。

λ. concatN

<URL:http://d.hatena.ne.jp/lethevert/20060630/p3> より。

ぁゃιぃ拡張機能を使うと出来ないこともない気がする。以下のコードの元ネタはOlegさんの Deepest functor 。なお、私はどうしてこれでうまくいくのかいまだに良くわかってない。

{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
{-# OPTIONS -fallow-overlapping-instances #-}
module ConcatN where

data Atom

-- Check if a type is a collection type. This is the only typeclass that
-- needs overlapping instances
class IsCollection  t coll | t -> coll
instance IsCollection (m a)       (m ())
instance TypeCast Atom coll => IsCollection t coll

-- our common working horse
class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b
class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
instance TypeCast'  () a b => TypeCast a b where typeCast x = typeCast' () x
instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
instance TypeCast'' () a a where typeCast'' _ x  = x

class ConcatN a c | c -> a where
    concatN :: c -> [a]

instance (IsCollection c coll, ConcatN' coll a c) => ConcatN a c where
    concatN = concatN' (undefined::coll)

class ConcatN' coll a c | coll c -> a where
    concatN' :: coll -> c -> [a]

instance ConcatN' Atom a a where
    concatN' _ a = [a]

instance (ConcatN a c) => ConcatN' [()] a [c] where
    concatN' _ = concatMap concatN

test1 = concatN [[[True]],[[False,True]],[]]
test2 = concatN [[1::Int,2,3],[4]]

深さを指定してconcat

稲葉さんのとこで色々なコードが紹介されていたので、私も少しバリエーションを。深さを指定してconcatするなら、私ならこんな感じで書くかな。

data Z   = Z
data S n = S n

class ConcatN a n l | a n -> l where
    concatN :: n -> l -> [a]

instance ConcatN a Z [a] where
    concatN _ = id

instance ConcatN a n l => ConcatN a (S n) [l] where
    concatN _ = concatMap (concatN (undefined :: n))

さらに、型クラスではなくGADTを使ったバージョン。

data N a l where
    Z :: N a [a]
    S :: N a l -> N a [l]

concatN :: N a l -> l -> [a]
concatN Z     = id
concatN (S n) = concatMap (concatN n)

λ. 某氏の筆箱の中身

まるで、雑多なものが沢山入っていて、まるで植芝理一の漫画のようだ。 感動。