日々の流転

λ. 同じ空の下で‥‥

サマーワで活躍する自衛隊を激励するFLASH。(logより)

λ. Re: Functor と Monad

圏論の普通の定義ではモナドは関手と二つの自然変換からなるので、MonadならばFunctorだというのはその通りです。ちなみに、[haskell-jp:51]によれば、「Goferで型クラスが導入されたとき」には「Monad になるためには、Functor でなければいけなかった」そうです。

で、両者の実装を変える理由ですが、やはり効率があるんじゃないでしょうか。例えばリストの場合、fmap f [a,b,c] が [f a, f b, f c] を計算すれば良いのに対して、liftM f [a,b,c] は [f a] ++ [f b] ++ [f c] を計算するので、多少効率が悪そうですし。

λ. "Graph Rewriting Semantics for Functional Programming Language", Marko van Eekelen, Sjaak Smetsers, Rinus Plasmeijer

Concurrent Clean とかの意味論で使われてる項グラフ書き換え系(TGRS, Term Graph Rewriting System)の説明と、その上での Uniqueness Typing の定式化。項書き換え系(TRS, Term Rewriting System)ではなく項グラフ書き換え系を用いるのは、共有を明示的に扱えて、関数型言語の実態に近いから。

そういえば、uniquenessの様な性質に関するpolymorphismのアイディアは"Quasi-Linear Types"にもあったな。

λ. 『同盟を考える—国々の生き方 』, 船橋 洋一

読了。法理論的またはイデオロギー的な議論ではなく、現実主義的で生々しい安全保障と国益追求の視点で、冷戦後の変容しつつある同盟関係を読み解く、良書だと思う。安保を議論する全ての人に読んで欲しいな。

λ. "Type Classes with Functional Dependencies", Mark P. Jones

multi-parameter type class と functional dependency を提案した論文。functional dependency は名前からしてそうかなとは思ってたけど、やっぱり関係データベースに由来していたか。

[2005-04-28 追記] あと、この論文とは関係ないけど、multi-parameter type class はMPTCと略されることもあるようだ。

λ. ムーアとブッシュとフセインのある一日。

N.* D.* E.* (2004-08-31) より

λ. 『第二次大戦とは何だったのか?—戦争の世紀とその指導者たち』, 福田 和也

読了。

λ. 人狼BBS

灼燦灼丸裏kdoo王国(2004-09-03)より。うわっ、すごいなこれ。試しに幾つかの村のログを読んでみたのだけど、むちゃくちゃ奥が深いなぁ。夏休み中に1,2回プレイしてみたいところだ。

λ. うげぇ、裸足でゴキブリを踏み潰しちまったよ。

λ. 『セクシーな数学 — ゲーデルから芸術・科学まで』, グレゴリー・J・チャイティン(Gregory J. Chaitin) [著], 黒川 利明 [訳]

読了。インタビューと講演からなっているので重複する部分が多いのは残念だった。内容も、アルゴリズム論的情報理論に興味を持つには十分だけど、もう少し技術的に踏み込んだものを読みたかったな。

λ. 「人狼」各職の基本戦略

メモ。[追記] 太田さんの自堕落記(2004-09-08)より、もう一つの「人狼」各職の基本戦略。

λ. 第2回プログラミングおよびプログラミング言語サマースクール (PPL Summer School 2004)

そうそう。来週はこれに参加します。

λ. 『慰安婦と戦場の性』, 秦 郁彦

ざっと読んだ。従軍慰安婦問題に関する非常に網羅的な本で、日本軍の「戦場の性」に限らず、従軍慰安婦問題の経過、当時の公娼制度と売買春の実態、諸外国との比較、自称慰安婦たちの証言、この問題に関する政治的環境、といった非常に幅広い内容を扱っていて圧巻だった。

で、この本にたいする反論/批判をgoogleで探してみると、林博史氏の「『慰安婦と戦場の性』批判」(『週刊　金曜日』290号、1999年11月5日)というのがあったが、他にはあまり見当たらなかった。結局、「(日本軍/日本政府による組織的な)慰安婦の強制連行はあったか?」という論争に関しては、(この本の著者も主張する)「無かった」でほぼ決着が付いてしまったと思ってよいのかな?　(……と思いたいけど、そう簡単にはいかないんだろうなぁ)

個人的な意見を言うならば、この手の問題では「あった」こと証明するには(確たる証拠のある)事例を一つでも見つければよいが、逆に全く無かったということを証明するのは実質的に不可能で、それゆえ立証責任は「あった」と主張する側にある。だが、慰安婦の問題が世間で騒がれるようになって既に十年以上経つにも関わらず、そんな事例は一つも確認されていないわけで、論争以前の問題ではないかと思う。

λ. Introduction to Proof Theory

神戸大大学院の講義録。[logic-ml 2502] よりメモ。

λ. Introduction to ordinal analyses

同じく、神戸大大学院の講義録で、[logic-ml 2502] よりメモ。

λ. 成績表

届いた。うげ、ちょっと誤算。

λ. 『DEATH NOTE (3)』, 大場 つぐみ [著], 小畑 健 [イラスト]

を読んだ。

λ. 東方永夜抄

先生!、待宵(Lunatic)がノーコンティニューでクリアできません!

λ. 『しずるさんと偏屈な死者たち』, 上遠野 浩平 [著], 椋本 夏夜 [イラスト]

正直言ってつまらなかった。トリックの奇抜さは別に気にはならなかったけど……

λ. 「ベルセルク」トレーラー

http://www.quiter.jp/news/manga/040909002161.html より。良く出来てるなぁ。(スタッフ名とか全部日本語と英語なのにタイトルだけなんでハングルで「베르세르크 - 천년제국의 매 편 성마전기의 장」って書いてるんだろう……)

λ. 『聖・高校生 1』, 小池田 マヤ

どっかで見たことある絵と思ったら、『バツイチ30ans』の人か。

λ. 「東方戰騎譚」の攻略みたいなもの

雪さんすきすき日記(2004-09-02) より。

λ. 『日本再生に「痛み」はいらない』, 岩田 規久男, 八田 達夫

読了。著者達の主張には概ね同意できるし、こういった政策パッケージを提案する政党があったら、先の参院選でも投票を考えたのになぁ……

λ. How to read and write .NS1 files

This document describes the NetStumbler file format. It is primarily intended for people wanting to read NS1 files (for example, to be able to import them into mapping software), however there may be others that want to write their own NS1 files.

メモ。chiko にっき (2004-09-11) より。

λ. 【ジョジョ】プロ市民の奇妙な冒険【ジョジョ】 (2ch)

……

λ. 制限された関数だけクラスのインスタンスにする

GHCなら-fglasgow-extsを指定すれば、インスタンス宣言での型構築子の引数は型変数でなくても大丈夫です。でも、 理由はよく知らないんですけどね。マニュアルの 7.4.4. Instance declarations でもあまり触れられてないけど、型の同義名(type synonym)をインスタンス宣言に使えるようにしたことの自然な帰結なのかな……

λ. Eastern Dawn　東方の夜明け

弾幕STG・東方プロジェクトの生みの親である上海アリス幻樂団神主ＺＵＮ氏をお呼びしてなにかれとトークをしてもらおうというイベントです。ただいまは告知期間で、申し込みは9月15日よりとなっております。尚、定員は150名となっておりますのでご了承ください。

メモ。楽しそうなイベントがあるじゃないですか。

λ. 型を返す関数

「型を返す関数」ってのは言い換えれば「値をパラメータとする型」で、ご存じかも知れませんが、一般に依存型(dependent type)と呼ばれてます。Haskell98の型システムでは依存型を直接表現することは出来ませんが、拡張機能を使ってよいのなら HaWiki:SimulatingDependentTypes のような事は一応出来ます(2006-04-23追記: GADT(2004-11-03参照)を使うことも出来ます)。また、Haskellに本物の依存型を追加しようという試みもあることはあって、こっちはJohn Hughesのスライド"Dependent Types in Haskell"(PPT,PDF)を見ると、きっとイメージがわくと思います。

【2006-04-23追記】 依存型を直接サポートする他の関数型言語にはAgda(カテゴリ:agda参照)やEpigram(2004-09-27参照)があります。 また、依存型をサポートする型理論はカリーハワードの同型対応(Curry-Howard isomorphism, Curry-Howard correspondence)によって、ある種の述語論理に対応します。そのような型理論には例えばCC(Calsulus of Construction)やITTがあります。

関連エントリ

• Pattern matching with dependent types.
• Lectures on the Curry-Howard Isomorphism

λ. 萩野服部研合宿

今日明日と修善寺。

λ. 『蕎麦ときしめん』, 清水 義範

を読んだ。

λ. 第2回プログラミングおよびプログラミング言語サマースクール (PPL Summer School 2004)

先週予告したように、これに行って来た。この手の集まりに参加するのは初めてだったのだけど、参加者は30人ちょいくらいを予想していたので、80人くらいいてビックリした。それから、Haskell Marathonのときにお会いした横山さん(最初そうだと気付かずにすいませんでした)と、Rubyのコミッタのうえの かつひろ さんに会うことが出来た。あと、tradさんからツッコミをもらっていたので、会えるのを楽しみにしていたのだけど、見つけることが出来ず残念だった。

λ. プログラム変換入門, 高野 明彦 先生 (国立情報学研究所)

本当に入門だった(講義の一回目と二回目相当だそうだ)ので、少々物足りなかった。 個人的にちょっと面白いと思ったのは、酸性雨定理(Acid Rain Theorem)が Eric Meijer の命名で、Theorems for Free によって只で得られる、森林破壊(Deforestation)のための定理だからという話。それから、「こういったプログラム変換の技術によって、アルゴリズムをどう表現しておくかを選べるようになったらいいなぁ」とか「オブジェクト指向言語のクラスライブラリは人間側に媚びすぎ。中間データ型のチョイスが違うだけで問題の本質は変わらない、といったことを見抜ける形にはなっていない。関数言語が貢献できるのはそういった点ではないか」といった事も言っていた。

参考文献

• Algebraic and Coalgebraic Methods in the Mathematics of Program Construction: International Summer School and Workshop Oxford, Uk, April 10-14, 2000, Revised Lectures (Lecture Notes in Computer Science, 2297)
• Advanced Functional Programming (?)

λ. お昼

大衆魚料理 つかさ。ネギトロ丼。

λ. XMLとスキーマ, 村田 真 先生 (日本IBM)

参考文献

• XYZ第一回の資料
• XMLとスキーマ言語, コンピュータソフトウェア (掲載予定)
• Taxonomy of XML Schema Language using Formal Language Theory, ACM TOIT (投稿中)

λ. よくわかる定理証明ーIsabelle/HOLを用いた定理証明入門ー, 南出 靖彦 先生 (筑波大学)

実はこのチュートリアルに一番期待してたのだけど、とてもわかりやすいチュートリアルだった。Isabelle/HOLとSML/NJは以前何かの機会にインストールしてたんだけど、全然使ってなかった。これを機に使ってみようかなぁ。

λ. Java Just-In-Time　コンパイラ, 石崎 一明 先生 (日本IBM)

へぇ、こんなに色々最適化技法があるもんなんですねぇ。このうちのどれだけがYARVやSTGマシンに適用可能かなぁとか思いながら聴いていた。

λ. 『百億の昼と千億の夜』, 光瀬 龍

読了。萩尾望都による漫画版はずいぶん前に読んでいて、原作もそのうち読もうとずっと思っていたんだが、ずいぶん経ってしまった。

λ. Eastern Dawn　東方の夜明け

申し込み開始ですよ。とりあえず申し込んでみた。

λ. ヴァン・ヘルシング(VAN HELSING)

を観てきた。スタイリッシュな映像と音楽がいい感じで、結構盛り上がれた。ストーリーはご都合主義的な点が目に付くが、あまり気にならなかった。

λ. 「東方戰騎譚」エキスパート攻略のようなもの

雪さんすきすき日記 (2004-09-11) より。ちなみに私はいまだノーマルの「死霊の舞踏」が抜けれていませぬ(最近はあんま挑戦してないけど)。

λ. 『世界から見た大東亜戦争 — The Holy Mission of DAI-TOA』, 名越 二荒之助 [編]

読了。

λ. 人狼BBS 57 谷底の村

人狼BBS初参加で、ここ一週間ほどこの「谷底の村」に参加してました。この一週間は長いようで本当に短かったです。この感動をどう表現したらよいか分らないし、もうこの村では一緒に参加した他のプレーヤーと話すことが出来ないことを思うと、名残惜しくてたまりません。このゲームを生み出したにんじんさん、そして何よりも一緒に参加した全てのプレーヤーに心から感謝します。

心残りの一つは、最後のリーザさん(パントさん)のセリフに対して、「……ッ！！　くッくくッ　上等じゃないか　女！！　上等ぉ！！」と返す事が出来なかったことです。別のネタを考えていたせいで、とっさに反応できなかったんです。「画竜点睛を欠く」とはまさにこういうことを言うんでしょうね。本当に悔しいなぁ。

• 人狼BBS まとめサイト - 57村
• 人狼BBS まとめサイト - msakai

λ. 『迷宮百年の睡魔』, 森 博嗣 [著]

読了。森博嗣の作品の中ではこのシリーズ(?)が一番好きかも。それと、読んでるあいだ頭に浮かぶ情景は全部スズキ ユカの絵でした。『女王の百年密室』に続いてこれもスズキ ユカの絵で漫画化されないかなぁ。

λ. 友達達と、夕食を食べて、それから映画見てきた。

λ. 夕食

とんかつ 新宿さぼてん。

λ. バイオハザードⅡ アポカリプス

期待してたほどではなかったけど、それなりには面白かった。ミラ・ジョヴォヴィッチ(Milla Jovovich) かっこいいね。

λ. let age' = age + 1 in ...

というわけで、今日は誕生日でした。ささやかに祝ってもらった。

λ. 今日から授業開始。

λ. 東方永夜抄のスペルカード取得率

スペルプラクティスで取得/挑戦可能/総数が199/207/222。残りは6Aの禁薬「蓬莱の薬」のHardとLunatic、6BのLuntatic全部、Extraの「インペリシャブルシューティング」、それに Last Word が半分くらいか……。いまだに「深弾幕結界　-夢幻泡影-」を見れねぇ。

λ. 本宮ひろしと集英社に抗議を！！

ヤングジャンプで連載中の「国が燃える」での南京事件の過激な誇張に抗議しようって話。フィクションとはいえ、私もこの描写はあまりに酷いと思う。

λ. Epigram

Epigram is a dependently typed programming language and an interactive programming environment. Epigram has got a type system which is strong enough to express the behaviour of programs, the type checker then guarantees that the program is well behaved. However, you don't have to go as far, you can write ordinary programs and refactor them into more trustworthy, formally checked deliverables -- Epigram supports a pay as you go approach to formal methods.

Epigram is a dependently typed functional programming language.って事で少し興味をひかれる。誰か使ったことあるひといない?

【2006-04-22 追記】 xemacsが必要なのと、自然演繹のスタイルでプログラムを書かなくてはいけないのが、ちょっと嫌かも。

関連エントリ

• 型を返す関数
• Why Dependent Types Matter
• Epilogue for Epigram

リンク

• Wikipedia: Epigram programming language

λ. 今朝の夢

ゴキブリの群れにたかられる夢を見た。身体中ゴキブリだらけですよ。気持ち悪くて心臓が止まるかと思った。

λ. 今朝の夢

「俺は負け犬じゃ無い!!」と執拗に叫び続ける夢を見た。俺はきっと負け犬なんだろうな。

λ. 東方永夜抄のスペルカード取得率

「幻朧月睨(ルナティックレッドアイズ)」ゲット。これで取得/挑戦可能/総数が200/207/222。

λ. 『輝ける日々』, ダニエル・スティール(Danielle Steel) [著], 畑 正憲 [訳]

読了。

λ. 研究

しなくちゃなぁ。