日々の流転

λ. 渕一博記念コロキウム『論理と推論技術：四半世紀の展開』

今年は第五世代コンピュータ・プロジェクトが始まってから25年になります．また，同プロジェクトを指揮してこられた渕一博さんが亡くなられてから１年が経過しました．

この機会に，第五世代プロジェクトや渕さんの周辺で芽生えた技術が，その後の四半世紀でどのように展開したかを概観するコロキウムを企画しました．

当時から現在に至るまで各分野の第一線で活躍を続けている研究者の方々に，「現在の視点から」当時の技術とその後の発展，およびそれを踏まえた将来展望を語っていただきます．今回は特に『論理および推論技術』に焦点をあてて，その多様な展開を紹介したいと思います．基調講演は，論理学・計算機科学者であり歴史学者でもある京都大学の林晋先生にご快諾いただきました．

本コロキウムは，第五世代プロジェクトに関係した方々はもちろんのこと，プロジェクトには直接のご関係がなかった皆様にもぜひ多数ご参加いただき，日本発プロジェクトがきっかけとなって開花した多くの技術にふれていただきたいと思います．特に，学生は参加費無料としましたので，若手の方々の積極的なご参加をお待ちしています．

10月20日(土)にこんなのがあります。 私も参加するので、是非ご参加を。

(追記: 参加した)

λ. マサラ・チャイ

λ. フレックス

今日からフレックス。 でも、しょぱなから電車が遅れて、しょぼーん。

λ. maude の protecting, extending, including の違いは?

モジュールを拡張する際の protecting, extending, including の違いは何かと気になって確認してみたら、以下のような違いを表現するためのものらしい。

• protecting : no junk, no confusion
• extending : no confusion
• including : no restriction

ここで junk は新たな要素の追加を指し、confusionは二つのコンストラクタの間に新たな等式が成り立ってしまうような場合を指す。

ところで、no junk で confusion は許すようなものは何故ないのだろうか?

λ. Googleデスクトップのサイドバーの検索ボックスを消したい

Google デスクトップのサイドバーの検索ボックスを非表示に出来ないものか。 検索するときはクイック検索ボックスの方を使うから、サイドバーの検索ボックスは使わないんだよな。 なので、スペースを占めるだけで邪魔。

<URL:http://pc11.2ch.net/test/read.cgi/software/1178771974/201-202> に同じ悩みが書き込まれているのを発見したが、結局消し方は分からず。

λ. Lightweight Language AHP をやってみた

ku-ma-meさん作の Lightweight Language AHP をやってみた。 私の結果は「sakai さんにオススメの LL は Ruby (40%) > Python (27%) > Perl (21%) > PHP (11%) です！」 だったのだけど、詳細の表が面白いな。 偏ってるけど何となく納得できるような……

λ. 起きられない

フレックスになったら、いつもの時間に起きられなくなった。 orz

λ. 東方風神録

ボロボロになりつつ、初クリア(th10_01.rpy)。 個人的には永夜抄よりも難しいと思う。

東方風神録 リプレイファイル情報
Version 1.00a
Name hiro    
Date 07/10/08 21:31
Chara ReimuA 
Rank Normal 
Stage All Clear
Score 32902232
Slow Rate 0.21

あと、以下の三枚のスペルカードがとれない……

• No.59 秘術「グレイソーマタージ」
• No.87 贄符「御射山御狩神事」
• No.95 「マウンテン・オブ・フェイス」

λ. デッドロックを起こしている交差点

Software Transactional Memory: a solution to concurrency problems というスライドの最後のページの写真。これはわかりやすいwww

λ. 『オトナ語の謎』 糸井 重里

を読んだ。 社会人になってから知った言葉が沢山載っていて面白い。

λ. 「Haskellがアセンブリになるまで」

[haskell-jp:137]でも書いたけど、10月22日(月)に情報科学なんでもセミナーというところで「Haskellがアセンブリになるまで」という発表があるそうです。 興味のある方は参加してみてはいかがでしょうか。

λ. 名古屋 (1)

たまたま名古屋に来ていたので、syd_sydさんに名古屋大学の学内を案内していただいたり、色々な人に紹介していただいたり。 あと 第66回プログラミング研究会(PRO-2007-3) の懇親会を少し覗いてみた。

関連

• <URL:http://mixi.jp/view_diary.pl?id=590984837&owner_id=1525867>

λ. 名古屋 (2)

twitterでのsoutaroさんの、PROでの某発表に関する一連の発言が面白かった。

• これはひどいな (11:18)
• ずっとakr師匠のターン (11:18)
• まじでフルボッコだな・・・ (11:30)
• 師匠、そろそろ自重ｗｗｗｗｗ (11:32)

OCaml-Nagoyaの飲み会に参加。

• CoqとAgda
  • dependent product と dependent sum
    • dependent sum: Σa:A.B(a) = B(a1) + B(a2) + …
    • dependent product: Πa:A.B(a) = B(a1) × B(a2) × …
  • equality
    • Leibniz equality
    • Inductive equality
    • Extensional equality
  • 停止性検査
• 非同期π
• ネットカフェ遊牧民 (一体何を遊牧してるのだろう……)

javascriptでcall/ccを実現する話があったが、Concurrent.Threadのコードを流用すると簡単に実現できるのではないかと思う。

Coq上で普通の数学を展開するのはそんなに自明な話ではないと思う。

• 古典論理と直観主義論理の違い
• 一階述語論理と高階述語論理の違い
• 集合論と型理論との違い

関連

• 飲み会 - zyxwvの日記
• 飲み会 - すえひろがりっっっ!
• 本山とりとり亭でのCoq談義に捧ぐ。

λ. 観光

貨幣資料館は開いてなかった。残念。

電気文化会館のでんきの科学館で時間を潰す。 名古屋市科学館をスルーして、大須観音へ。

もどって、名古屋市美術館へ。

矢場とん本店で昼食。 25分も待たされるのかと思ったら、5分くらいで入れた。 おいしい。

ロボットミュージアムは休館していた。

オアシス21

名古屋まつり

お土産を買って帰る。

そういえば、名古屋はJR西日本だと思ってたのだけど違うのね。 Suicaへの(ビューカード以外の一般の)クレジットカードからのチャージが、JR西日本のICOCAエリア内のみどりの窓口で可能だと聞いていて、この機会にチャージしようと思っていたので、ちょっと残念だった。

そういや、喫茶マウンテンにも行くのを忘れてたなぁ。

λ. 秋祭

ひろゆきトークライブ　〜ひろゆき × ＳＦＣ〜 を聞きに秋祭に行ってきた。

SOS団SFC支部なる件の団体がメイド・執事喫茶をやっていてうけた。 仮面のメイドガイみたいな人もいたが、あれは何のコスプレだったのだろう。

萩野・服部研の企画でViPPERの体験コーナー(?)をやっていた。 子供づれの人なども沢山来ていて、盛況だった模様。

限定商品として「大学生なら誰もが持ってるキャンパスクラッチを秋祭オリジナルデザインで販売します」とかいうのがあったが、キャンパスクラッチって何?　半年前まで大学にいたけどそんなものは知らなかったお。

関連

• Paint the SFC 第16回秋祭開催 -映像で見る秋祭 (SFC CLIP)
• SFCにひろゆきが来た! -秋祭で1年ぶりの講演- (SFC CLIP)

λ. 人狼BBSに関する卒業研究アンケート

某氏のmixi日記より。 kairiさんという方が、心理学の卒業研究で人狼BBSに関する研究をしているそうで、アンケートを実施している。 興味と時間のある人狼プレーヤーは協力してみてはいかがでしょう?*1

私も答えてみようと思ったら、一年以内にプレイしているという条件を満たしていないのだった。残念。ところで、人狼で研究といえば、知人がネット上の合意形成に関する実証研究(?)で人狼BBSを対象にしようとしていたのを思い出す。

λ. “On asynchrony (...and on mobility)” by Francesco Zappa Nardelli

先日syd_sydさんに紹介していただいた非同期π計算の講義資料を読んだ。 asynchronous pi calculusでもsynchronousの同期的な通信が模倣できる点とか確かに面白い。 mobilityについては良くわからなかった。

λ. 36th Tokyo Programming Seminar (ToPS)

今度、Tokyo Programming Seminar というところで喋らせてもらう予定です。 関係各位には色々とご迷惑をおかけしております……

• <URL:http://www.ipl.t.u-tokyo.ac.jp/~tops/done_seminar07.html>

λ. RubyでSTM

後で書く。

【2008-02-11 追記】 後で書こうと思いつつ、ずっと忘れていたが、ようやくまとめた。

<URL:http://www.tom.sfc.keio.ac.jp/~sakai/archives/ruby-stm-0.0.1.tar.gz>

使い方

STM.atomically{ ... } でトランザクションの実行。必要な条件が満たされていない場合などには、STM.retry で現在のトランザクションの再試行。STM.or(proc1, proc2, ...) は引数のProcを順番に試行して最初に成功した結果になる。全ての引数が再試行になったら、STM.or全体として再試行になる。

STM::Var が Haskell の TVar 相当で、トランザクションの対象となる「変数」。トランザクション中に、STM::Var.new(value) で作って、STM::Var#get, STM::Var#set(val) で読み書き。

STM::Array というのも用意してあって、こちらはトランザクションの対象となる「配列」。Rubyの配列で使える操作はほぼそのまま使える。

それから、STM::MVar が Haskell の TMVar 相当。

実装

シンプルな実装。

トランザクション中で最初に STM::Var を読み込んだときの値と、そのトランザクション中で更新した結果の値を、トランザクションのオブジェクトに記録。コミット時にはグローバルなロック*1をかけて、記録された値と現在の値に齟齬がないことを確認し、それから実際の STM::Var に対して書き込む。もし齟齬があった場合には最初からやり直し。

再試行が起こった場合には、それまでに読んだ変数に対してそのトランザクションを登録し、それらの変数に対して変更がコミットされるまで待つ。

他の実装

実装後に気づいたのだけど、<URL:http://www.atdot.net/~ko1/diary/200701.html#d25> で笹田さんも実装していた。 また、<URL:http://moonbase.rydia.net/mental/blog/programming/ruby-stm> というものもあるようだ。

λ. KAMONジェネレーター

綾鷹（あやたか） KAMONジェネレーター なるものを試してみたところ、四葉 になった。ちょっと意外な感じ。

【四葉】 四葉紋のあなたは争いごとを遠ざけ、平和を好む温和な性格。周りとの調和を大切にし、多くの人々と手に手をとって生きてゆけば必ずや、あなたも、そしてあなたを取り巻く人々も平穏で素敵な人生を送れることでしょう。持ち前の優しさと協調性を大切にして、素敵な日々を過ごしてください。

ちなみに、うちの実際の家紋は丸に片喰。

λ. “Algebraic laws for nondeterminism and concurrency” by Matthew Hennessy and Robin Milner

先日、syd_syd さんに紹介してもらった Hennessy-Milner Logic の論文。ざっと読んだ。

プログラムを様相のラベルに使う様相論理は私もどこかで見たと思っていたのだけど、それは First Steps in Modal Logic の Chapter 13 SLL Logic で扱われていた Dynamic Logic だった。 ただ、この論文の p.141 には以下のようにあるので、ちょっと違うのかな。

Although we do not here develop L into a logic for reasoning about programs, it is worth noting that as a language it is endogenous by Pnueli's classification [8]. This means that a formula states something about the `world' of a single program, in contrast to exogenous logics such as Dynamic Logic [9] where parts of programs may be constituents of formulas.

【2008-03-17】 Dynamic logic (modal logic) - Wikipedia, the free encyclopedia を読んでも、この違いをどう考えれば良いのかわからない…… orz

λ. 渕一博記念コロキウム『論理と推論技術：四半世紀の展開』

渕一博記念コロキウム『論理と推論技術：四半世紀の展開』 に参加。 ICOT関係者など流石に年配の人が多いな。 遅刻して基調講演は最後しか聞けなかった。 他の発表に関しては内容が盛りだくさんのわりに発表時間が短かったのが少しもったい。 発表資料公開されないかなぁ(2007-11-23追記:公開された)。 それと、F川研の面々に久しぶりに会えて楽しかった。

懇親会には参加せず、RHG読書会の飲み会へ合流。

λ. Googleブックマーク + GMarks

ブラウザのブックマークを Googleブックマーク + GMarks に乗り換えた。

最初はspurlにしようと思っていたのだけど、bookmark.htmlをインポートしても「Allow up to 24 hours before your bookmarks show up in your Spurl.net account.」と出るばかりでいつまでもインポートされないので、やめたのだった。

GMarksは編集機能がイマイチだけど、それでもなかなか便利。

若干不便な点は Personal Toolbar Folder を置き換えられない点。

λ. リプレイの動画化失敗

カハマルカの瞳で動画作成 を参考に、リプレイを動画化しようとしてみたが、マシンスペックが足らないらしくコマ落ちしまくってた。 5fpsで録画しようとして3fpsって……

【追記】 Fraps や Dxtory も試したが、これらは何故か録画出来なかった。 Dxtoryの場合には以下のようなエラーが発生していた。

[Module]
Dxtory.exe 1.0.18

[Process]
ID: 2596

[Thread]
MainThread (1)

[Environment]
OS: Microsoft Windows NT 5.1.2600 Service Pack 2

[Error Message]
External component has thrown an exception.

[StackInfo]
   at b.ap.DxCore_SetOptionParam(ak A_0, bg& A_1, IntPtr A_2)
   at Dxtory.MainForm.d()
   at Dxtory.MainForm.ai(Object A_0, EventArgs A_1)
   at b.bb.a(Message& A_0)
   at c.c.a.b.a(Message& A_0)
   at c.c.a.b.b.a(Message& A_0)
   at System.Windows.Forms.Control.ControlNativeWindow.OnMessage(Message& m)
   at System.Windows.Forms.Control.ControlNativeWindow.WndProc(Message& m)
   at System.Windows.Forms.NativeWindow.Callback(IntPtr hWnd, Int32 msg, IntPtr wparam, IntPtr lparam)

λ. 「Haskellがアセンブリになるまで」 (不参加)

「Haskellがアセンブリになるまで」に参加しようと思っていたのだけど、開始に間に合わなくなってしまったのと、疲れていたので結局不参加。 だけど、ku-ma-meさんの記事や発表者のMaDさんの記事を読んでると、非常に楽しそうで……やっぱり参加すれば良かったかなぁ。

後で内容について少し書くかも

【追記】 資料が公開されている。 なんでもセミナーの資料を公開します。 - mad日記

λ. 正格性フラグを使ってseqを定義する

たまたま気づいたのだが、正格性フラグを使えば seq を書くこともできるのだな。

data T a = T !a

seq' :: a -> b -> b
seq' a b = case T a of T _ -> b 

正格性フラグの意味を定義するのに seq を使うものは見たことがあったが、これは考えたことがなかった。 まあ、考えてみれば当たり前なんだけど。

「seqを特定の型クラスに属する型に対してしか適用できなくしよう」という意見は時々あるが、その場合には正格性フラグが用いられる型定義に関しても、同じ型クラスの文脈が必要になるだろう。しかし……

λ. 東方風神録、封印装備でノーマルクリア

封印装備でもクリア(th10_02.rpy)。 相変わらずボロボロ。No.59 秘術「グレイソーマタージ」は一応とれた。

東方風神録 リプレイファイル情報
Version 1.00a
Name hiro    
Date 07/10/27 16:35
Chara ReimuC 
Rank Normal 
Stage All Clear
Score 32824661
Slow Rate 0.31

λ. Amazon.co.jp、3000円以上の和書ポイント5倍還元

Amazonが 和書ストア 3000円（税込）以上の商品【Amazonポイント5倍還元】（一部商品を除く） というキャンペーンをやっていたので、前から欲しかった本を一冊購入。

Amazonポイント最大5倍還元Amazon.co.jp 和書ストアでは、通常1％のポイント還元のところを、3000円（税込）以上の商品に限り、【Amazonポイント5倍還元】キャンペーンを実施中（一部商品を除く） 。2008年1月31日（木）まで。

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

今日は圏論勉強会だった。 “Categories, Types and Structures” Section 2.3.6 Propositionより

写真

【2007-11-13追記】 Proposition 2.3.6 では reflexisive object V に V×V を埋め込めることを示すために、非常に面倒くさい計算をした。 CCCの射として明示的に書き下しているので煩雑すぎて本質が見えにくかったが、落ち着いて考えてみれば簡単で、CCCのinternal languageとしてラムダ計算を使うならば、単に直積型のチャーチエンコーディングに過ぎない。

関連

• 圏論勉強会 - たけをの日記＠天竺から帰ってきたよ
• デカルト閉圏におけるお絵描き計算の基礎 - 檜山正幸のキマイラ飼育記

λ. seqはHaskellの意味論では扱えない?

• <URL:http://alohakun.blog7.fc2.com/blog-entry-812.html#comment1712>
• Haskell: seqってよくわからない - lethevert is a programmer

seqの意味がHaskellの標準的な意味論で扱えないかのように思われがちなのは何故だろうかと思った。

【追記】 lethervertさんの場合は、Haskellの公式の意味論でseqの操作的意味を確定出来るかという疑問だったので、実際には違う話ではあったけど。

λ. Google デスクトップの説明わかりにくい

Google デスクトップで「複数のコンピュータ上のデータ検索」を有効にした場合の説明として、「インデックスに登録されたファイルのテキストが Google デスクトップサーバーに転送され、お客様の他のコンピュータにコピーされます」とある。 それは当然なのだけど、その上で「他のコンピュータから検索できるこのコンピュータのデータ」を「なし (他のコンピュータのみを検索します。このコンピュータのファイルは他のコンピュータから検索できません。)」にしても、テキストはGoogleのサーバに転送されるのだろうか?

説明がわかりにくいよ……

λ. 『数学ガール』 結城浩

読了。

λ. 携帯ストラップ壊れた

9/15にキャンドゥーで買った携帯のストラップ がもう壊れた。 当り外れもあるのだろうが、前にダイソーで買ったやつが1年半以上もったのに比べると、随分壊れやすいなぁ。

λ. “Faster laziness using dynamic pointer tagging” by Simon Marlow, Alexey Rodriguez Yakushev, Simon Peyton Jones

• <URL:http://research.microsoft.com/~simonpj/papers/ptr-tag/index.htm>

を読んだ。

これはGHCのcase式の新しい最適化に関する論文。 面白かったので、少し紹介。

例えば、以下のような関数があるとする。

map :: (a -> b) -> [a] -> [b]
map f xs = case xs of
             [] -> []
             (x:xs') -> f x : map f xs'

この関数が呼び出されたときには、大雑把には以下のように実行される。

• この関数はxsを呼び出して、
• xsは自身がwhnfになるまで実行したらリターンして、
• この関数はxsがどのコンストラクタの形かを調べて、対応する分岐を実行する

問題はxsが最初からwhnfの場合。この場合にはxsは即座にリターンするが、この呼び出し・リターンという間接ジャンプは分岐予測が効かず非常にコストが大きい。

それに対処するため、xsを呼び出す前にxsのinfo_tableを参照し、評価済みかどうかと、評価済みならどのコンストラクタかを調べ、もし評価済みであることが分かれば直接分岐先にジャンプするようにすることが考えられる。これがsemi-taggingで、OpteronとXeonで7.2%と9.4%の性能向上。

semi-taggingにも効率の悪い点があって、それは必要な情報を得るために遠くにあるinfo_tableを一度だけ参照し、キャッシュ汚染を引き起こす点。 これを改善するためにxsを指すポインタの下位ビットにそれらの情報をエンコードするのがpointer-tagging。 評価前のサンクが評価結果に書き換わったときには、そのサンクを指すポインターのタグを書き換えないと意味がないのだけど、これはガベージコレクションのタイミングでガベージコレクタが行う。 というのも、copying GC なのでどうせアドレスの書き換えは必要なので。 pointer-taggingを適用した結果、OpteronとXeonで13.7%と12.8%の性能向上。

あと、個人的に驚いたのは、vectored returns が最早有効ではないという話。 数年前のベンチマークでは正味5%程度のメリットがあったが、現在では正味ではマイナスだとか。 実行環境も変わってきているんだねぇ。

λ. itojun氏、逝去

帰りに何気なくmixiを見ていたら、遠山さんの日記にitojunさんが亡くなったとのことが書かれていて、非常に驚いた。 私も直接の面識はなくて、ただ一方的に憧れていただけだったのだけど、それにしても本当に残念です。 謹んでご冥福をお祈り申し上げます。

• <URL:http://www.hoge.org/~koyama/itojun.txt>
• <URL:http://www.wide.ad.jp/news/press/20071031-itojun-j.html>
• <URL:http://slashdot.jp/article.pl?sid=07/10/31/0311203>