日々の流転

λ. What Languages Fix

おまぬけ活動日誌(2003-10-31) より。面白すぎ。ついでに幾つか考えてみる。

ML

Lisp is not type-safe

Haskell

ML is not pure

Clean

Monads are scary

【2007-02-15 追記】 らいおんの隠れ家 - ポール・グレアム「プログラミング言語が解決するもの」 で日本語訳されている。
あと、Cleanについて「Monads are scary」と書いたが、 CleanとHaskellの宣言スタイルの違い と Concurrent Clean : FGRS vs. lambda calculus あたりの話から、それは本質ではない気がしてきた。

λ. 借りた本

小説すばる 2003年2月号

-

『シャイニング　上』

スティーヴン・キング(Stephen King)[著], 深町 真理子 [訳]

『R.O.D　第5巻』

倉田 英之 [著], 羽音 たらく [イラスト]

『水素エコノミー — エネルギー・ウェブの時代』

ジェレミー・リフキン(Jeremy Rifkin) [著], 柴田 裕之 [訳]

λ. 順序対

順序対(a,b)を集合にエンコードする時には通常{a,{a,b}}という表現を使うそうだ。けど、この表現だと a = {b,1}, b = {a,0} とおいたときに、(a,0) = {a,{a,0}} = {a,b} = {{b,1},b} = {b,{b,1}} = (b,1) となってしまい、(a,0)と(b,1)の区別がつかなくなってしまう。well-founded な集合だけを扱ってる場合には問題にならないけど、これってどうなんだろう?

……というようなことを、例の集合クラスでストリームとかを表現してて思った。

【2005-10-23追記: この件に関して、白のカピバラの逆極限 S144-3のnucさんがより詳しいことを書いている。http://d.hatena.ne.jp/nuc/20051007/p4 と http://d.hatena.ne.jp/nuc/searchdiary?word=*[順序対] を参照のこと。】

λ. Re: FreeBSDのRubyとRuby-GNOME2

以前にruby-gnome2-devel-enで Installing ruby-gnome on FreeBSD というスレッドがあったので参考になると思います。

「/usr/libexec/ld-elf.so.1: /usr/local/lib/libgthread-2.0.so.200: Undefined symbol "pthread_getschedparam"」の原因は、libgthreadがlibc_rをリンクしていなくて、しかも`pkg-config --libs gthread`にも-lc_rが含まれていないことです。最近のglibだと直っていると聞きました。

それと、「ruby_r -I/usr/local/lib/ruby/site_ruby/1.8/i386-freebsd4 base.rb」で「Undefined symbol "rbgutil_sym_g2r_func" - /usr/local/lib/ruby/site_ruby/1.8/i386-freebsd4/gtk2.so (LoadError)」になるのは、おそらくは-Iを指定したために「require 'gtk2'」でgtk2.rbではなくgtk2.soが読み込まれてしまうのが原因です。gtk2.soはglib2.soに依存しているので、先にglib2.soがrequireされていないとこのようなエラーになります。

λ. 読書

『マンガ金正日入門−北朝鮮将軍様の真実』

李 友情 [著], 李 英和 [訳]

『REC 1』

花見沢 Q太郎 [著]

どっかで見たことある絵だなぁと思ったら、花見沢Q太郎ってベルウッドハウス描いてる人だったか。

λ. hyperset

まだまだ完成度は低いけど例の集合クラスをこっそり公開。マニュアルは面倒だったので、とりあえずfinite-set.rbからパクってしまいました。(もしまずかったらすいません > 原先生)

λ. ruby-ffcall

0.0.2をリリースしました。 今回の変更はruby-1.8対応などのマイナーな変更です。また、msvcrt用とcygwin用のバイナリパッケージも用意しました。

ruby-ffcallはruby-dlのDL.callbackを強化する拡張ライブラリです。DL.callbackでは使えるコールバック数に制限がありますが、FFCall.callbackにはそのような制限はありません。また、DL.callbackで作成したコールバック関数を開放するにはDL.remove_callbackを明示的に呼ぶ必要がありますが、FFCall.callbackではGCによって自動的に開放されます。

λ. 『ももいろさんご (5)』 花見沢 Q太郎

を読んだ。

λ. 教育方法の研究者が教育者として優れているとは限らない。

すごく同感です。あえて誰とは言わないけど……

λ. finite-set

% ruby -rfinite-set -e 'p (Set[true,false] == Set[true])'
true

なんじゃこりゃ。……と思ったら速攻で原因発見。falseやnilを値として含み得る場合はEnumerable#findはEnumerable#any?の代用にはならないのか。考えてみれば当たり前だ。ついでに1.8でwarningが沢山出ていたのとかも含めてパッチ。

λ. 学校の帰り

駅前で民主党の候補が演説してた。たしか、今日は管直人と小沢一郎が来ると言ってたな。ちょっと見てみようかと思ったけど人多すぎ。そういえば今週末はもう選挙なんだよね。

λ. Relators, Fans and Membership

を見た。後ろの方はよく分からなかった。後で読み返さねば。

λ. Ruby-GNOME2のcygwin用パッケージ

これまでのパッケージはcygwin-ruby18.dllではなくcygruby18.dllをリンクしていたため、リリース版のRubyで利用できないと問題がありました。なので、パッケージを作り直しました。これでリリース版のRubyでも動作するようになるはずです。

λ. puncTure

設定は少し面白いと思った、拷問ゲームだけどなー。って、こういうことを書くと、また誰かさんに「酒井君って実は怖い人だったのね」とか言われてしまうんだろうか……

λ. 論文積読

積読しまくり。

λ. [ruby-ext:02242]

.

λ. Gunslinger Girl

先週に続いて今週も録画するのを忘れる。欝だ。

λ. Coalgebras and Monads in Semantics of Java

を読んだ。これをRubyに応用するには何が必要だろう。あと、coalgebraって面白いかも、と今頃になって思った。

λ. Ruby/TCC

Ruby/FFCall 0.0.2 をリリースしたら、Mitchell N Charity さんという方が Tiny C Compiler というコンパイラがライブラリとしても使えると教えてくれたので、ちょっと試しに拡張ライブラリにしてみた。以下は Tiny C Compiler の付属サンプルをRubyに移植したもの。

require 'tcc'
 
tcc = TCC.new
tcc.set_output_type(TCC::OUTPUT_MEMORY)
 
tcc.compile_string <<END
int fib(int n)
{
    if (n <= 2)
        return 1;
    else
        return fib(n-1) + fib(n-2);
}
 
int foo(int n)
{
    printf("Hello World!\n");
    printf("fib(%d) = %d\n", n, fib(n));
    printf("add(%d, %d) = %d\n", n, 2 * n, add(n, 2 * n));
    return 0;
};
END
 
tcc.add_symbol("add", DL.callback("III"){|a,b| a + b })
tcc.relocate
foo = tcc.get_symbol("foo", "II")
foo.call(32)

このスクリプトを実行すると以下のような出力が得られる。

Hello World!
fib(32) = 2178309
add(32, 64) = 96

結構面白いかも。

それから、TinyCCはTinyCC-Win32というWin32移植版もあるそうだ。えとせとら(2003-11-03)とシュッ・シュッ(2003-10-29) より

λ. 知識ベース論

やべー、レポートの提出って今日だったのか。うわー、やってもうた。欝だ。何が最悪かって、わたしゃ昨日日付を確認して来週だなと思っていたのですよ。何を確認してたんだろね俺は。あー、気分最悪。

λ. OBJは等式論理を使ってるらしい。

subtree が有限であるような木を rational tree というそうだ。

λ. 借りた本

『経済学を知らないエコノミストたち』

野口 旭 [著]

λ. 衆議院選挙

投票してきた。

λ. 「メタ」と「高階」

これを読んで気になったのだけど、私は「高階(higher-order)」の「階(order)」って『A,Bのorderをm,nとすると、「Aに依存したB」のorderは max(m+1,n)』という条件で定義される数だと漠然と思ってたのだけど、これって正しいだろうか? 幾つか例を考えてみる。

λ. (例1) 関数

(関数でない通常の)値を0階の関数と考える。通常の関数は値に依存した値だから、max(0+1,0) = 1 より1階の関数。引数が一階の関数であるような関数は max(1+1,0) = 2 より二階の関数。二階以上の関数をまとめて高階関数と呼ぶ。

この定義だと引数が通常の値で返り値が一階の関数であるような関数は、max(0+1, max(0+1,0)) = 1 から一階の関数になってしまい、ちょっと直感に反する気もする。でも、カリー化によって階が変わらないのは逆に本質を捉えている気もする。

λ. (例2) 命題と論理

真偽値を0階の命題と考える。一階の命題は通常の命題。一階の命題に依存して真偽値が定まるような命題は max(1+1,0) = 2 より二階の命題。一階の命題と二階の命題の両方を扱う論理体系は二階論理、orderに制限のない論理体系は高階論理。

λ. (例3) 算術

真偽値を0階の対象と考える。一階の対象は自然数。自然数の集合は(特性関数によって「自然数に依存した真偽値」と考えられるので)二階の対象。自然数を扱う「Q」や「ペアノ算術」等の体系は一階の算術ともいわれる。自然数と自然数の集合の両方を対象とするZ₂等の体系は二階算術といわれる。

λ. (例4) 型

「data Bool = True | False」で定義される型Boolのような引数を持たない型は一階の型。「data List X = Nil | Cons X (List X)」で定義されるような型は一階の型を引数に取るので二階の型。「data Fix f = In (f (Fix f))」で定義されるようなFixは二階の型を引数に取るので三階の型(?)。

ポリモルフィック・ラムダ計算(polymorphic lambda calculus) が、二階ラムダ計算(second-order lambda calculus)と呼ばれるのは二階の型を扱えるから?

λ. 高階型?

それはそうと「型の型」と言うと普通は「種(kind)」のことで、型をパラメータにとる型という意味での「高階型」とは違う気がします。

λ. 衆議院選挙 (2)

あッはっはッはっはっは
あの民主党がまるでボロ雑巾じゃないか
やっぱり強いなぁ!! 自民党は!! 
べらぼうに強いな!! 存外に強いな!!

とか書こうと思ってたのですが、ちょっとだけアテが外れた。……それにしても、公明党は例によっておいしい立場ですなぁ。

λ. A.D.2003

いいなぁ。っていうか、今年は存在自体をすっかり忘れていて、申し込んでなかったんだけどね。

λ. CMU student taps brain's game skills

日誌(2003-11-07) より。おもしろーい。

λ. yap - yet another prolog (sourceforgeのページ)

The Yap Prolog System is a ISO-compatible high-performance Prolog compiler. Yap is widely considered one of the fastest available Prolog systems. Yap supports coroutining, CLP(QR), CHR, and depth-bound search. Tabling and parallelism are in development.

こないだ向井先生が紹介していた処理系。freeze とか rational tree とか使えるらしい。

cygwinでビルドしようとしたら、-mno-cygwinでビルドしだした。しかし「gcc -shared」には-mno-cygwinがついていなくて、__findfirst, __findnext, __errno などのシンボルが未定義になってしまう。とりあえず安直なパッチ。

λ. すげーやる気がない今日この頃。……なんつーか、なす嫌だゴニャ

λ. 借りた本

『"戦争責任"とは何か—清算されなかったドイツの過去』

木佐 芳男 [著]

『よく見る夢　上』

シドニィ・シェルダン (Sidney Sheldon) [著], 天馬 龍行 [訳]

λ. 買った本

『魔術士オーフェンはぐれ旅—我が聖域に開け扉　下』

秋田 禎信 [著] 草河遊也[イラスト]

λ. 『親日派のための弁明』 金 完燮 (김 완섭) 著. 荒木 和博, 荒木 信子 [訳]

を借りた。

λ. 数学の基礎としての集合論 vs. 数学としての集合論

メモ。

λ. 各言語で作った簡易足し算器

あけてくれ日記(2003-11-18)より。ついでにHaskellでも書いてみる。

main :: IO ()
main =
    do s <- getContents
       putStrLn . show . sum . takeWhile (/= (0::Float)) . map read . lines $ s

λ. 『親日派のための弁明』 金 完燮 (김 완섭) 著. 荒木 和博, 荒木 信子 [訳]

読了。韓国で有害図書指定されて発禁になったと聞いていたから、どんな過激な事が書いてあるのかと内心期待していたのだけど、歴史認識に関してはそれほど驚くような記述はなかった。ちょっと拍子抜け。

Koreaという単語が「高麗」からきているというのもこの本ではじめて知ったし、いろいろと勉強にはなった。

ただ、現代の事に関する記述では「おいおい……」と思うような点が何箇所もある。たとえば p.134 - p.135 の

一九九七年、東アジアが経済危機に瀕し、新興開発国が経済恐慌におちいったとき、その四年前にこれを予見していたアメリカの経済学者ポール・クルーグマンは一躍スターになり、アジア諸国は白人の経済機構たるIMF(国際通貨基金)にあらゆる経済主権をわたしたまま、経済システムをアメリカ式に転換しなければならなかった。

しかし発想を逆転してみれば、当時ノーベル賞候補ナンバーワンといわれ、アメリカの経済政策にそうとうの影響力を行使していたクルーグマンが、東アジアはこれ以上発展できず、まもなく滅びるはずだとさんざんこき下ろすとまもなく、ジョージ・ソロス・ファンドをはじめとする国際投機資本の計略によって、東アジア諸国がつぎからつぎへと惨めな恐慌状態におちいることになったのは、果たして偶然の一致だったのだろうか。

といった記述とか。(参考: The Myth of Asia's Miracle, Whatever Happened to the Asian Miracle? / アジアの奇跡はどうなった？)

あと、ついでに2chのスレッド(1, 2, 3)からのメモ:

• 序文抜粋(正論・02年6月号)
• 金完燮が語る衝撃作『親日派のための弁明』の制作秘話
• 未翻訳部分

λ. libtool and impgen

libtool-1.5はimpgenを使わなくなっていたと思うので、libtoolのバージョンをあげてみるという手もあるかも。

λ. コンパイラの作り方 (詳解) (InternetArchive)

東大の「コンパイラ演習」の授業のレジュメ。印刷して読書中。SFCの「コンパイラ構成論」の授業では構文解析のアルゴリズムばかりがんばって教えているので、こういう授業がある東大が羨ましい。

closure conversion の導入くらいまで読んだ。ちょっとややこしいな。

あと、CPS変換は、いわゆる continuation semantics:

• 〚x〛_ρ = λk.(k (ρ x))
• 〚λx.M〛_ρ = λk.k (λν.λk'.〚M〛_{ρ[x ↦ ν]} k')
• 〚E₁ E₂〛_ρ = λk.〚E₁〛_ρ(λf.〚E₂〛_ρ(λa. f a k))

については知っていたけど、実用的には色々やらなくちゃいけないのね……

λ. 小人のパズル (関心空間)

百人の小人が怪獣に捕まってしまいました。 小人たちが怪獣に命乞いをしたところ、条件を出されました。

怪獣が小人たちを縦に一列に並べ、それぞれの小人の頭に 赤か黄色か青のうちのどれか一色の帽子を被せます。 小人たちは自分より前に並んでいる小人の帽子の色はすべてわかりますが、 自分を含め、後ろに並んでいる小人の帽子の色は全くわかりません。 （前から50番目に並んでいる小人は、49人分の帽子の色がすべてわかる）

小人たちはひとりずつ赤か青か黄色の色を一回だけ答えることができ、 それが自分の帽子の色と同じだった場合は命が助かるというものです。 答える順番はどの小人からでも構いません。

このような条件が与えられ、小人たちには作戦タイムが与えられました。 小人たちは少しでも数多く生き残れるような戦術をとるものとします。 たとえば、一番後ろの小人が目の前の小人の帽子の色を答え、 その小人は食べられてしまうとしても、次に後ろから二番目の小人が 今と同じ答えを言えば、その小人は助かります。 これを繰り返していけば、最低50人の小人は助かることとなります。

さて、小人たちは何人助かるでしょうか？ また、そのときの戦略は？

なお、被らされる帽子の順番に特徴的なもの （赤、青、黄色が順番にならんでいるとか） はないものとします。

大切なページ(2003-11-21)より。2,3分で解けた。人数の答えが書かれていなかったらもっと時間がかかったかも。\

λ. VD - Virtual Desktop for Win32

こないだ太田さんに紹介してもらった、Windows用の仮想画面ソフト。

λ. トランプの手品

同じく大切なページ(2003-11-21)より。小人のパズルよりもこっちの方が難しく感じた。いちおう自分なりの答えは考えたのだけど、いまいち自信がない。\

λ. ByteCodeRuby 0.2.0

だいありー(2003-11-19)より。ByteCodeRubyってだいぶ前に開発が止まってるのかと思ってましたが、0.2.0が出たんですね。試してみようと思ったら、ruth-0.10 が落とせないや。誰かこのファイル持ってませんかぁ〜?

λ. 借りた本

『赤緑黒白』

『臨機応答・変問自在 2』

森 博嗣 [著]

『大人のための残酷童話』

倉橋 由美子 [著]

『犬儒派だもの』

呉 智英 [著]

λ. コンパイラの作り方

抽象機械のコードを出力するところまで読んだ。そういえば、レジスタが足らなくなったらどうするんだろう。

λ. 理大祭

東京理科大の大学祭に行ってきた。たまたまるりという人のライヴを見たのだけど、なんかすごいキャラクターしてるなぁと思った。話しているときと唄っているときのこのギャップはなんなんだろう……

λ. 読書

『HELLSING 6』

平野 耕太 [著]

『ケロロ軍曹 7』

吉崎 観音 [著]

λ. 『赤緑黒白』

ぐはっ。そ、そんな伏線があったとは……。いやぁ凄いね。鮮やかだね。見事に騙されてたよ。

……あれ?　でもそうすると『ぶるぶる人形にうってつけの夜』の最後は何だったのぉ? なんか引っかかるぞぉ。読み返そうと思ったら『今夜はパラシュート博物館へ』が手元にないや、残念。失くしちゃったかな。

λ. そうだ、レコンキスタにいこう

笑った。

λ. HaskellのMonad

Haskellのモナドの話になって、原さんは「私にわからんのは(Haskellが)おかしい」と言っていた。原さんにわからないなら、私にわかるわけがないな。

原さんがわからないってのは、ちょっと信じられないです。Monadの数学的定義を知っているならば、Haskellのは単に「各種の計算体系のモデルを、適当な strong monad の Kleisli category として作れる」ということに過ぎないと思うので。

例えば、Computational lambda-calculus and monadsにも載っている例をいくつか取り上げると……

(例1) 非決定性計算

• T: C→C
  T(X)=℘(X) (℘はべき集合関手)
• η_A: A→℘(A)
  η_A(x) = {x}
• μ_A: P²(A)→℘(A)
  μ_A(S) = ⋃S

で定義される Monad (T,η,μ) の Kleisli category は非決定性計算のモデルと考えられる。非決定的な関数 A→B は決定的な関数 A→℘(B) として解釈される。

(ちなみに、amb演算子 amb: P(A)→A も決定的な関数 Id_℘(A): ℘(A)→℘(A) で解釈できる)

(例2) 副作用

• T: C→C
  T(X)=(X×State)^State
• η_A: A→(A×State)^State
  η_A(x) = λs.<x,s>
• μ_A: ((A×State)^State×State)^State→(A×State)^State
  μ_A(x) = λs. eval(x(s)) (ただし eval: Y^X×X →Y)

で定義される Monad (T,η,μ) の Kleisli category は、(State型の状態に対する)副作用をもつ計算体系のモデルと考えられる。副作用をもつ関数 A→B は副作用を持たない関数 A→(B×State)^State として解釈される。(A→(B×State)^State は A×State→B×State をカリー化した型になってる)

【2006-04-13 追記】このエントリの記述について、[教えて！goo] モナド、Kleisli triple で質問されているみたい。 とりあえず意味を理解するには http://www.ipsj.or.jp/07editj/promenade/4703.pdf でも読めばよいのではないかと。

λ. 学校に行く途中で、バスがバス停に止まり忘れてUターンしてた。

λ. 借りた本

『容赦なき戦争 ─ 太平洋戦争における人種差別』

ジョン・ダワー (John W. Dower) [著] 猿谷 要, 斉藤 元一 [訳]

『国益とは何か』

今野 耿介 [著]

小熊さんに紹介された『容赦なき戦争』を借りてきた。

λ. A topological sum of localic systems is still localic.

Topology via Logic (p.79) の「A topological sum of localic systems is still localic.」の証明で、「To show that pt p is onto, take z ∈ pt Loc(∑_λD_λ). Then z ⊨ true = ∨_λj_λ(true), so for some μ, z ⊨ j_μ(true).」の後の「It follows that if λ≠μ then z ⊭ j_λ(true).」がどうやって導かれるのか2週間前から悩んでいたのだけど、ようやく解決した。

λ≠μ で z ⊨ j_μ(true) かつ z ⊨ j_λ(true) ならば、z ⊨ j_μ(true)∧j_λ(true) = false であり、これは矛盾。

λ. 妖々夢の左右封印クリアのリプレイ

左右封印クリアのリプレイ見ました。すごすぎ。