日々の流転

λ. coLinux

Cooperative Linux(coLinux)のメモ を参考にしてラップトップのWindowsXP上にインストール。これまでこのマシンではVirtualPCでLinuxを使ってたのだけど、どうにも重かったのでcoLinuxを試してみたというわけ。やはり、VirtualPCよりも体感的にはだいぶ軽い気がする。VirtualPCだと仮想マシンの状態を保存したり復元したり出来るのが便利だったけど、あまり活用してなかったし、ラップトップのLinux環境はこのままcoLinuxに乗り換えよう。

λ. N-gram

某日記(2005-03-18): N-gram の原理 を読んだときに書いたコード。イマイチ。NGram.hs

λ. GHC 6.4 ソースコードHacking: メモ

[haskell-jp:590]によるとテーマは「多言語化」らしいので、そのための個人的メモ。

HaskellのCharはUnicodeなので、同じく文字をUnicodeで扱っているJavaや.NET等のモデルが参考になるはず。

Unicode文字列⇔マルチバイト文字列 の変換

選択肢:

iconv + nl_langinfo(CODESET)

-

libcのmb⇔wc変換関数

現在の Hugs は --enable-char-encoding=locale でコンパイルするとこれを使う。wchar_tがUnicodeである環境(WindowsやLinux)では問題ないが、*BSD等はそうではないので問題となる。wchar_t がUnicodeかどうかを調べるには defined(_WIN32) || defined(__STDC_ISO_10646__) で良いと思う。

その他のライブラリ

the m17n library 等。libm17nはちょっと使ってみた感じでは結構良さそう。

自前でテーブルを持つ

これは出来たら避けたいな

IO周りで、Unicode⇔マルチバイト の変換

基本的には GHC.IO を書き換えればよい。GHC.IOBase と GHC.Handle も参照。

FFI周りで、Unicode⇔マルチバイト の変換

Foreign.C.Stringを書き換えればよい。参考: Hugsへのパッチ

Text.Regex

参考: GHC 6.2 で Oniguruma を使うためのパッチ

コンパイラがマルチバイトで書かれたソースファイルを処理できるように?

IO周りを対応すれば自動的に対応できる?　プリプロセッサでエスケープするようにすればコンパイラ自体に手を入れる必要はない?

複数のエンコーディングを同時に使うためのAPI?

-

the m17n library のGUI周りと Input Method 周り?

-

CHISE とのインターフェース?

-

HsLocale

アレな部分もあるけど、パクれそうなコードがある。 HsLocale-win32.diff

λ. 第六回圏論勉強会

圏論勉強会も今回で六回目。今回はブラウワー(Brower)の不動点定理のセクションだったのだけど、このセクションは何度読んでも面白い。今回も、これまで「なんとなく」で読み飛ばしてしまっていたところを掘り下げることが出来て興味深かった。やっぱり、色々な視点があるっていいな。

それから、たけをさんがmixiにコミュニティを作ってくれました。mixi:圏論勉強会。

写真

λ. GHC ソースコードハッキング 1日目

圏論勉強会後にちょとと遅めの昼食をとり、そのままGHCソースコードハッキングへ。

とりあえず、the m17n library を使ってみる流れに。

λ. 博麗神社例大祭

行ってきます。

ちょっと朝ゆっくりしすぎて、会場の列に並んだのが11:20。40分入れ替え制になったそう。入場したのが13:10過ぎ。体験版はすでに完売していましたとさ。orz

戦利品(?)

「東方烈華伝」体験版

-

「anima I 東方」

-

「幻想電奏響」

-

「幻奏蓄音機」

「幻奏譜」

ドメインがkeioだったのに驚いた

「アリスといっしょ」

これは○○○さんへのお土産　;-)

カリスマ扇

「komkom.com 通信 vol.3」

komkom.com

グラス (アリス)

-

「東風味　参」

福交感神経

「はるのうたげ」

かぐらみずき＠かぐら堂

「御粗末」

羽毛布団

「五月バカ」

オレブリスカ
ページを開いてたまたま目に入ったパチュリーの絵が気に入って買ってしまった。

「住所不定夢職」

夢見ごこち

「my best friend」

graceful fool

時の旅人　個人サークルペーパー「壊れた時計はいりませんか?」

壊れた時計

「Mystic Wanderer」

川代 拓 (Mysticmaker)

「紫のないしょ」

ゐとはたかいき

「We are Prismriver」

みょふ〜会

「門番の仕事」

月見箱

λ. GHC ソースコードハッキング 2日目

2時過ぎに例大祭を抜けて四ツ谷へ。

Foreign.C.String 相当の関数をでっち上げた。I/O周りはかなり面倒そうなことが分かってきた。

鬼車(Oniguruma)を使ってText.RegexをUnicode対応にするパッチ を GHC-6.4 用に更新。鬼車の同梱は評判悪かったので、分離した。鬼車は別途インストールしてくれ。

[2005-05-06 追記] なんで以前に鬼車のソースを取り込んでいたのか理由を思い出した。GHCi対策だ。鬼車のライブラリは.soではなく.aにコンパイルされるが、GHCiのリンカがリンクできるのは.soや.oだけで、.aはリンク出来ないのだ。したがって、単にghc-6.4-oniguruma3-1.patchのようにすると、baseパッケージがGHCiで使えなくなってしまって致命的。

これを回避する一つの方法は、ld -r --whole-archive -o onig.o libonig.a として onig.o を作り、library-dirs のリストに含まれているディレクトリ(e.g. $prefix/lib/ghc-6.4)に置いてやること。別の方法はlibHSbase_cbits.aとHSbase_cbits.oにlibonig.aの中身を最初から取り込んでしまうこと。ただ、どっちもfptoolsのビルドシステムでやるにはどうしたら良いのか分からん。困った。

λ. filofax

一瞬firefoxに見えた。

λ. 禁煙席と喫煙席

GHCソースコードハッキングの後、某ファミレスで夕食を食べたのだけど、禁煙席がいっぱいなのに喫煙席がガラガラで驚いた。禁煙席と喫煙席の境界を適応的に変化させることが出来たら、より多くの客が利用できるのではないかと思った。

λ. GHC ソースコードハッキング 3日目

I/O周りをいじろうとするが、なかなか思うようにいかない。

どうでもいいが、Handle型の定義が GHC.Handle でなく GHC.IOBase にあるってのも何か間違ってるよな。他にも色々と暗黒面を見た気がするよ。

それと、GHCのI/O は nonblocking mode が基本なのか。

あと、例のText.Regexの鬼車(Oniguruma)パッチをちょっと変更して、Hugs98-Mar2005向けのパッチも一応作った(hugs98-Mar2005-oniguruma3-1.patch)のだけど、実際にコンパイルして実行すると、何故か鬼車ではなくlibcのregcomp/regexec/regfreeが呼ばれてしまう。そしてregex_tのサイズが違うので落ちる。

実際にregcomp/regex/regfreeを呼んでいるコードはPosix.soにあって、こいつは-lonig付きでビルドしてある。で、このPosix.soをhugs本体からdlopen("Posix.so", RTLD_LAZY | RTLD)みたいな感じでロードして使っている。環境は普通のLinux。きっとシンボルを探す場所の順序の問題なんだろうけど、どうしたものかな……

[2005-05-07 追記] [Gauche-devel-jp] 動的リンカのシンボル解決 のスレッドに全く同じ問題が書かれていた。しかし、ダイナミックリンカのこの仕様って考えれば考えるほど使いにくい仕様だな。さすが Unix、腐ってます。それはともかく、このスレッドによると ld の -Bsymbolic オプションを使えば一応は回避出来るようだ。試してみたら上手くいった。hugs98-Mar2005-oniguruma3-2.patch

λ. 創作童話「博士(はくし)が100にんいるむら」

生存記録 (2005-05-05) 経由で、「博士が100人いるむら」のオチはマジなのか? より。

うはぁ……

λ. ファンタジージョブ占い

石沢セソセイの白黒ウェブより。オアイーブってなんだか懐かしい名前だな。結果は「あなたはシーフです」だった。

あなたは盗みで培った素早さをいかし、戦いに役立つシーフ。良識派に目覚めた盗賊で、仲間を助けるためにその力を振るいます。そしてあなたの力は戦いだけではなく、仲間の心を潤す重要な役割を果たすでしょう。しかし非常に気まぐれな性格で、仲間を振り回すこともります。

わはは。

λ. ギャング・オブ・ニューヨーク

野蛮で奔放で残虐で、もー、わくわくするね。

λ. Agda

Agda をインストールした。AgdaはCoqやIsabelle/HOLなんかと同様の定理証明系(証明支援系)。特徴は証明を関数型言語のプログラムとして書く点だろうか。文法はHaskellに似ているが、dependent type も扱える。証明を独自の言語で書くのではなく、関数型言語の一般的な notation で書けるのは、私のようなプログラマには嬉しそうだ。

使ってみてまず驚いたのは再帰的な定義が好き勝手に出来る点。例えば、bottom (P :: Set) :: P = bottom P なんて定義も出来てしまう。Isabelle/HOL なんかでは「再帰呼び出しのときに、引数がある意味で必ず小さくなることを示すことが必要」だったけど、Agdaはこれで問題ないのだろうか!?

[2005-05-19 追記] Why Dependent Types Matter. Thorsten Altenkirch Conor McBride James McKinna には次のように書いてあった。

It's reasonable to allow arbitrary recursion in type-level programs, provided you have some sort of cut-off mechanism which interrupts loops when they happen in practice. This is the approach taken by the Agda proof system, Cayenne and by Haskell with `undecidable instances' —Haskell's overloading resolution amounts to executing a kind of `compile-time Prolog'. Agda restores logical soundness by a separate termination check, performed after typechecking. The basic point is that you include recursive programs in types at your own risk: mostly they're benign and typechecking behaves sensibly.

[2006-03-25 追記] 上記の bottom のような定義は、C-c C-x C-t で agda-check-termination にかけると "The call: bottom\n might lead to non-termination" と判定してくれる。停止性の保障に使ってるアルゴリズムは何なんだろう? Size Change Termination (SCT)?

もっとも、以下のように定義すると停止性チェックは通ってしまう。 このような場合をちゃんと扱うにはどうすればよいか?　また、これは GHCのinlinerの問題と似ているように思うがどうなのか?

data T (P::Set) = PsiInv (x :: T P -> P)
 
psi (|P::Set) (x::T P) :: T P -> P
  = case x of
    (PsiInv y) -> y
 
fix (|P::Set) (f::P -> P) :: P
  = let g (x::T P) :: P = f (psi x x)
    in g (PsiInv g)
 
id (|P::Set) (x::P) :: P = x
 
bottom (P::Set) :: P = fix id

[2006-03-25 追記] いや、以下のアッカーマン関数の停止性を認識できないので、SCTではないか。ソースを見ると、src/Termination.hs には「Based on "foetus" type checker of Andreas Abel and Thorsten Altenkirch (Ludwigs-Maximilians-University, 1997-1999).」と書いてあるので、Andreas Abel. foetus Termination Checker for Simple Functional Programs が元になっているのかな。まあ、どうでもいいけど。

data Nat = Zero | Succ (m::Nat)
 
ack (m::Nat) (n::Nat) :: Nat
  = case m of 
    (Zero   )-> Succ n
    (Succ m')->
      case n of 
      (Zero   )-> ack m' (Succ Zero)
      (Succ n')-> ack m' (ack m n')

λ. ホーンティング

安直で分かりやすい構図。ホラーという感じはあまりしないな。

λ. 五月病!?

どうもやる気が出ない。やらなくちゃいけないことは幾つかあるのだけど、取り掛かる気が億劫で仕方ない。困った。——困っていたら、これがひょっとしていわゆる五月病って奴なのではないかと思った。なるほど。そう考えたら、なんだか少し気が楽になった。気が楽になっただけで、問題は一切解決してないけど。

λ. WWW2005 前日

ボランティアのオリエンテーション、電源とネットワークのセットアップなどの各種の準備。

λ. 『リサイクル幻想』, 武田 邦彦

を読んだ。

なんでもリサイクルすれば環境によいというような安易な発想への批判。そのような発想で何でもリサイクルすると、かえってエネルギーを消費し、環境を破壊することにもなる。リサイクルを考えるには、材料工学を初めとする工学的視点が欠かせない。

リサイクルの過程には分離工学の考え方が適用できる。純度が高くまとまっているものはリサイクルが容易だが、純度が低く分散してるものをリサイクルしようとすると高くつく。

金属はリサイクルに向いているが、鉄に混入した銅を取り除くのは不可能といった問題もある。紙をリサイクルするのに(遺産型の資源である)石油を使うのは循環型社会の観点からは本末転倒。プラスチックは素材としては比較的劣化しやすいが、燃やすと石油とほぼ同じ熱量を発生するので、素材として使用した後に燃やして熱量を得るのが良い……

工学的な議論は、ラフな議論ではあるがまあ大体納得がいく。ただ、そこから著者の主張する循環型社会像へは飛躍が過ぎると思った。

参考

• 環境市民　武田邦彦氏著「リサイクルしてはいけない」のおおいなる問題点

λ. WWW2005 1日目

朝ごはんは近くのロッテリアで食べた。

あうぅ。(経験者の)パートナーがいるはずだから何とかなるだろうと思ってたら、独りでアサインされてしまった。困った……、もう頭が真っ白ですよ。ぁぅぁぅ。至らないボランティア・スタッフでホント申し訳ないです。一日目にして早速逃げ出したくなってきた (T_T)

お昼は伊太利亜小料理 東風房というところでスパゲティを食べた。

夜はマハラジャというところで、インドカレー。美味しかった。

λ. Draft Agda Document, Agda-documentation team at AIST CVS

Draft Agda Document, Agda-documentation team at AIST CVS を読んで、例を色々試した。対話的な証明環境がとても面白い。以前にCoqを使ったときはゴールの管理が最初良くわからなくて困った記憶があるけど、Agdaのはとても分かりやすい。

Agdaではデータコンストラクタを使うときには、cons@_ のように、名前の後に @_ を付けなくてはならないけど、これは何故だろう?　ただし、パターンに書く場合には不要。何故こうなっているのだろう。むしろ、普通に使うときにはそのまま使えて、パターン内で使うときに(パターンによって束縛される変数と区別するために)特別な表記を用いるのが自然に思える。こうなっているのは型推論の都合?　caseの枝からcase対象の型を推論しないようになっていたり、型推論はHaskellとはちょっと違うところもあるので、その辺りが理由なのかな?

それから、現在のAgdalibはこのドキュメントとは多少異なっている部分もあった。たとえば、Existの定義は Exist (|X::Set)(P::Pred X) :: Set = Sum X P になっていて、型も (X::Set) |-> (P::X -> Set) -> Set になっている。(|->) の第一引数は暗黙のパラメタとなる型で、型推論によって与えられる?　普通に明示的に引数を渡そうとするとエラーになる。

それと、「compute to depth 100 by C-c *」と書いてあるけど、実際には C-c C-x + (agda-nfC100) なので注意。

λ. Ruby Magazine 0006号

.

λ. WWW2005　2日目

今日は少し寒いな。朝食は近くのサンエトワールというところでパンを食べた。比較的美味しかったが、かかっている音楽が微妙っぽかった。

で、今日のしょっぱなは Tim Berners-Lee の基調講演「Web for real people」。彼が話すのを直接見るのは初めてなのだけど、想像してたよりもずっと面白い人だった。 ところで、会場で黒子のかっこをした人*1を見かけたのだけど、その頭の後ろにCSSの書かれた紙が張ってあって面白かった。いわく、

@media real{
  kuroko{
    display: none;
  }
}

お次はCan semantic web be made to flourish? というパネルセッションにお手伝いに入った。神崎さんを目撃。

参考

• WWW2005パネル・ディスカッション (The Web KANZAKI)

お弁当の配布を手伝って、それからお弁当を食べる。その後 Yuji Inoue 氏の基調講演を訊いて、それから「Web Application Design」へ。

最後に、「Foundations And Future Directions of Web Services」。このトラックでは、Choreographyに少し興味を持った。なんでも formally based on π-calculus らしいので。

その後はポスターレセプション。チケットの引き換えが大変だった。ポスターは結構面白いのがあった。論文をそのまま張ってだけというのもあって少し面食らったけど。発想が面白かったのは「Detecting of Phishing Webpages based on Visual Similarity」。タイトル見ただけで内容がわかっていいね。ポスターが面白かったのは「Does learning how to read Japanese have to be so difficult, and can the Web help!」かな。それから「Soundness Proof of Z Semantics of OWL Using Institution」なんて濃いポスターもあった(こんな濃ゆいポスターを見るとは思わなかった)。あと、PageRank系のポスターも結構あったな。

λ. Types for Verification から一年

そういえば、去年の今頃(2004-05-11,2004-05-12)は Types for Verification というワークショップに参加していたが、最近 Agda を触るようになって、そのときに聴いた Martin-Löf や Peter Dybjer の話への理解がようやく深まってきた気がする。

λ. WWW2005　3日目

寝坊した。ピンチ。朝飯を食わずに急いだところ、なんとか集合時間には間に合ったが、Assignment は既に埋まっていた。しょぼーん（´・ω・｀）

今日もお弁当の配布を手伝う。配布してて思ったのは、ベジタリアン用のお弁当を希望する人の割合が多かったこと。なんでだろうと思って訊いて見たら、「ベジタリアンでなくても、アレルギーや宗教上の理由で食べれないものがある人が、無難な選択としてベジタリアン用を選んでいるのでは?」とのこと。なるほど、たしかに。

あと、お弁当を配っているときに、黒子さんを指して「彼は何で帽子を被ってるのか?」と英語で訊かれて困ってしまった。とりあえず、「It's a costume of Kuroko. Kuroko is 〜」とか言っては見たのだけど、黒子の説明で詰まってしまった。後で本人にも訊いてたけど、本人は「Do you know Kabuki? Kuroko is 〜」と返していた。そうか。僕は黒子といえば文楽というイメージを持っていたのだけど、歌舞伎にも黒子がいるのか。

Lorrie Cranor 氏の基調講演。時間が昼と言うこともあるけど、Timの時よりも人が入ってる気がする。

O'REILLY のブースで和書が10%オフ、洋書が2000円均一だったので、とりあえず RELAX NG を買った。そしたら、O'REILLYメモ帳を貰えた。

Web Internationalization Developments。これまでの中で一番理解できたセッションだった。

ニューオークラで、ディナーパーティ。今回はチケット関係のトラブルもなかったし楽だった。料理、特にケーキは美味しかった。それから、ステージで能をやっていた。舞噺子「船弁慶」というのだそうだ。あまり見れなかったが、やっぱり凄いなぁ。ちゃんと見たくなった。

それと、昨日も書いた黒子さんの後ろ姿の写真。

λ. 『スナーク狩り』, 宮部 みゆき

を読んだ。

λ. WWW2005 4日目

には出ずに、千葉国から日本へ帰国。疲れたので速攻で寝る。

色々大変だったけれど、ボランティア・スタッフの仕事はいい経験になった。本当に参加してよかったと思う。

あと、ロッテの試合を見に行く機会がなかったのがちと残念といえば残念だ。

λ. Agda による選択公理の証明

--#include "Hedberg/Logic/Set.alfa"
open LogicSet use Prop, Forall, Exist
 
AC (|A::Set) (|B::A->Set) (|C::(x::A)->(y::B x)->Prop)
   (z :: Forall A (\(x::A) -> Exist (\(y::B x) -> C x y)))
  :: Exist (\(f::(x::A)->B x) -> Forall A (\(x::A) -> C x (f x)))
  = struct
      fst = \(x::A) -> (z x).fst
      snd = \(x::A) -> (z x).snd

以前に「ITT₀では選択公理も証明できる」と書いたが、その証明と本質的に同じもの。

ところで、Forallは量化される型が明示的な引数なのに、Existは量化される型が暗黙の引数なのは何故?　とても気持ち悪い。

ところで、この形の選択公理は証明できるけど、ZF集合論での場合と違って、選択公理から排中律を証明することは出来ない。何故ならば外延性公理に相当するものが仮定されていないから。

λ. ジョンQ —最後の決断—

を視た。

λ. RHG読書会: 鈴木さんを囲む会

寝坊したので諦めた。しょぼーん（´・ω・｀）

λ. case on non-var!?

Propositional Equality の型である Id の使い方がいまいち良くわからない。例えば、

Cat :: #2
  = sig
      Obj :: Type
      Hom :: (A::Obj) -> (B::Obj) -> Set
      id  :: (A::Obj) |-> Hom A A
      o   :: (A::Obj) |-> (B::Obj) |-> (C::Obj) |->
             (f::Hom B C) -> (g::Hom A B) -> Hom A C
      leftUnit  :: (A::Obj) |-> (B::Obj) |-> (f::Hom A B) -> Id (id `o` f) f
      rightUnit :: (A::Obj) |-> (B::Obj) |-> (f::Hom A B) -> Id (f `o` id) f
      Assoc :: (A::Obj) |-> (B::Obj) |-> (C::Obj) |-> (D::Obj) |->
               (f::Hom C D) -> (g::Hom B C) -> (h::Hom A B) ->
               Id ((f `o` g) `o` h) (f `o` (g `o` h))
 
test1 (C::Cat) (A,B::C.Obj) (f::C.Hom A B) :: { }150
  = {C.leftUnit f }151
 
test2 (C::Cat) (A,B::C.Obj) (f,g::C.Hom A B) (z::Id f g) :: { }152
  = {z }153

という状態で、goal 151 で C-c C-c しても、「case on non-var C.leftUnit |? |? f」と言われてしまう。「C.leftUnit f」を「C.leftUnit |A |B f」としても、やはり「case on non-var C.leftUnit |A |B f」と言われてしまう。letを使って一度変数に入れても同じエラーが出る。一方、goal 153 で C-c C-c すると、ちゃんとcaseが挿入される。どっちも型は同じなのに、何故このようになるのだろう?

(2005-09-11 追記) 「型は同じ」と書いたが全然同じじゃないな(汗)。
ところで、落ち着いて考えてみて、何らかの制約があること自体は当然だと気づいた。何故ならば、「case (Id α β) of { ref x -> ... }」という式の「...」の部分はα=β(=x)を仮定して型検査を行うわけだけど、α,βに任意の式を許すと型検査が決定可能でなくなってしまうから。
では、どのくらいの制約が必要か?　αとβがユニフィケーション可能な式であるならば良さそうに思える。だが、実際にはAgdaはαとβが相異なる変数の場合しか受け付けない。これは必要以上に強い制約に思えるが、何故こうなっているのだろうか?

ちなみに、HaskellのGADTはユニフィケーション可能な型でありさえすれば良かったはず。なので、例えば以下のような定義は正しい。

data T a b where
    T :: x -> T x x
 
test :: (T (a,Int) (Int,b)) -> Int
test x =
    case x of
    T (a,b) -> a+b

(2005-09-18 追記) 「ユニフィケーション可能な式ならば〜」というのは安易だった。Haskellの型の場合と違って、higher-order unification が必要だから、決定不可能になってしまう。Functional Programming with Overloading and Higher-Order Polymorphism には higher-order unification が不要な理由として「This is possible because the language of constructors is built up from constants and applications; in particular, there are no abstractions.」と書いてあったのを読んでいたのに、何を馬鹿なことを考えてるんだ、俺は……

——となると、残る疑問はαとβが同じ変数の場合が何故ダメかだな。池上さんが紹介してくれたスライドに「Use elimination rules and not case for inductive families.」と書いてあったし、単に「idata に対しては case よりも elimination rule を使わせる方針なので、case は elimination rule を実装するのに十分な最小限の実装しかされていない」という可能性もあるけど、何か他の理由はあるだろうか?

(2005-09-28 追記) あ、いや、αとβが同じ変数の場合も、一般のidataを考えると無理っぽいな。だいたい納得。

λ. Saunders Mac Lane 1909-2005

亡くなっていたとは知りませんでした。ご冥福をお祈りします。

λ. 『産直あづまマガジン 3』, 吾妻 ひでお

を読んだ。

λ. C365 幻の村 (ネタばれ注意)

ここ一週間ほどまた人狼BBSに参加してました。

参加するときに残っていたのがヤコブとトーマスだったので、とりあえずヤコブを選んで参加してみた。参加時点では人数のことをすっかり忘れていたのだけど、人数が15人で、ということは共有者がいないにも関わらず人狼は3人という、最も狼側有利な人数だった。で、役職は「おまかせ」を選んでいたにも関わらず「人狼」。……なんだか後ろめたくて仕方が無い。ごめんよ、村人のみんな。初参加だった57村でも、ヤコブで人狼だったし、因果だなぁ。

2日目の投票で占い師の投票COを行い、オイラもCOしたんだけど、同じくCOしていた真占い師を襲撃してしまって、ほぼ黒状態に。どうせ吊り回避は無理とは思ったけど、精一杯頑張ってみた。そして吊られた。推定黒の能力者をやるのは初めてだったので、なかなか楽しかったけど、弁明は今から考えると反省点が多い。

• 「ルーレットで真占い師を打ち抜く確率は1/5だよ。自分を除く13人のうちオットー,ディーター,ヴァルター,レジーナは非占い師宣言しているし、ペーター,ジムゾンと仲間2人も除けるからね」という発言はあまりに不注意だった。これは仲間2人がディーターとヴァルターとは別の人であると言ってしまっている様なものだ。もしこの発言にツッコミを入れられていたら超ヤバかった。この発言が注目されなかったのは幸運以外の何者でもなかったと思う。
  • 次に人狼になったときにはマジで気をつけよう。たった一つの失言が敗北に繋がると覚悟する。
  • 逆にこういった失言の振りをしてミスリードするのもいいかもしれない。独断で非占い師宣言するような村人がそうそういるはずが無いので、そのまま使えることは無いかも知れないけど、考え方は応用出来そう。
  • そして、村人になったときには、こういった発言を見逃さないように気をつけよう。
• 「自分が狼ならこんなことしないよ」的発言は、理屈が苦しかった。言いたかったのは、C301村のヨアヒムも言っていた「翌日投票COの場合能力者っぽいやつを襲うことは人狼にとって不利なんじゃないかと俺は思う」ってことだったんだが、言葉は難しいな。言い回しを変えればよかっただろうか?　それともこの発言自体をやめて別の発言に置き換えた方がよかっただろうか?
• 特別議題に発言を費やしすぎて、対立していた霊能者の神父を追求するための発言が出来なかったこと。神父を追及するためのネタはいくつか用意してたのに……
• 「もしオイラが吊られてしまったら、明日は絶対に神父を吊ってほしい」という言い方よりも、「神父を残しておいたら村が負けてしまう。神父を最後まで残すようなことは止めてほしい」的な言い方の方が良かったかも。
• その他色々

実力不足を実感したので、これから暫らくはログ読みに専念しようかと思う。

(追記予定)

関連URL

• 人狼BBS:C C365 幻の村
• 人狼BBS まとめサイト - C365村
• 人狼BBSの事をぐだるページ:C365村, yuragiさん(ヨアヒム)のブログ

λ. BREWシミュレータ

Windows版のBREWシミュレータで動かすにはVC++でコンパイルすることが想定されてるみたいだけど、VC++使うの面倒なんで、SDKに BREW-3.1.2-mingw.patch のようなパッチをあてて、mingw用のgccでコンパイルする。普通に動いた。

λ. Why Dependent Types Matter. Thorsten Altenkirch, Conor McBride, James McKinna

LtUより。2004-09-27の日記でも紹介したEpigramというHaskell風のdependent-typeをサポートした言語の話なんだけど、Epigram固有の話と言うよりはdependent-typeの有用性についての論文。面白い。

Future Work の Observational Type Theory に興味を惹かれる。僕も Intentional Type Theory と co-data の相性の悪さはうっすらと感じていたので、我が意を得たりという感じ。

λ. C110村

を読んだ。 超おすすめログ に載っているだけのことはある。色々勉強になった。

• 人狼BBS:C C110 悲しみの村
• 人狼BBS まとめサイト - C110村

λ. 永夜抄スペカ取得率: 214/222/222

久し振りに東方永夜抄をプレイ。Lunaticを頑張ってノーコンテニュークリア。7機で始めてクリア時に残機0・ボム0という惨状だけどね。で、Lunatic 6Bのスペルカードを中心に何枚か回収したので、取得済み/挑戦可能/総数 が 214/222/222 になった。残るは以下の8個。取れそうな気がするのは「ライフスプリングインフィニティ」と「永夜返し　-丑の四つ-」くらいか……

• 禁薬「蓬莱の薬」 (Lunatic)
• 神宝「ライフスプリングインフィニティ」 (Lunatic)
• 神宝「蓬莱の玉の枝　-夢色の郷-」 (Lunatic)
• 「永夜返し　-丑の四つ-」
• 「インペリシャブルシューティング」
• 「エンシェントデューパー」
• 「夢想天生」
• 「深弾幕結界　-夢幻泡影-」

ところで、「永夜返し　-子の四つ-」は「子の刻」「子の二つ」「子の三つ」よりも簡単な気がする。

λ. Extensional Equality in Intensional Type Theory. Thorsten Altenkirch

を読んだ。問題意識は良くわかるのだけど、モデルの構成がイマイチよく分からなかった。

• The implementation of a setoid model in LEGO

(2005-09-17 追記) 読み返したらあらかた理解できた。けど、まだ幾つか理解できていない概念がある。large elimination とか。

(2005-09-30 追記) Agdaでも実装してみた。An Implementation of a setoid model in Agda.

(2006-05-30 追記) large elimination は多分 elimination した結果が要素ではなく集合などになるような elimination 。

λ. デスノート

新登場の死神シドウたん、かわいいよ。

λ. predicativeな型理論であるということ

Agdaで(2階ラムダ計算の)パラメトリシティに関する命題を証明してみようと思い、以下のようなコードを書き始めたのだが、Forallのところで「Sort comparison failed」と怒られてしまった。

Rel (X,Y::Set) :: Type
  = X->Y->Set
 
FunRel (|A,B,C,D::Set) (R::Rel A B) (S::Rel C D) :: Rel (A->C) (B->D)
  = \(f::A->C)-> 
     \(g::B->D)-> 
       ((a::A) |-> (b::B) |-> R a b -> S (f a) (g b))
 
Forall (F::Set->Set) :: Set
  = (X::Set) -> F X
 
ForallRel (|F,G::Set->Set) (R::(A,B::Set)|->Rel A B->Rel (F A) (G B))
  :: Rel (Forall F) (Forall G)
  = \(f::Forall F)-> 
     \(g::Forall G)-> 
      ((A,B::Set) |-> (S::Rel A B) -> R S (f A) (g B))

しばらく悩んで、ようやくAgdaがMartin-Löf流のpredicativeな型システムであることを思い出した。FやCCのようなimpredicativeな型システムと違って、こういう定義は出来ないのだった。関数の型のソートに関する規則を、Adga の Structured Type Theory と、λ-cubeのスタイルで形式化したCC とで比べてみると良くわかる。λ-cubeでは返り値の型のソートが関数の型のソートになる。一方、Structured Type Theory では直観的には引数の型のソートと返り値の型のソートの最小上界が関数の型のソートになる。

アホだなオレ。しかし、impredicativeな型システムに慣れてる人が使うと絶対ハマると思うよ、これ。

それで思ったが、そうなるとGHCのCore言語をAgdaのコードに変換してゴニョゴニョってのは問題が起こりそうな気がするな。GHCのCore言語は一応Fω風のimpredicativeな型システムだったと思うので。

λ. Describing and Reasoning on Web Services using Process Algebra. Gwen Salaün, Lucas Bordeaux, Marco Schaerf

を読んだ。

ITシステムでbisimulationの説明をしていたときに、bisimulationの意味がわからないが使ってみた というのを誰かが見つけてきて面白かった。

bisimulationの(余代数的/圏論的な)定義は知っているけど、weak bisimulation と strong bisimulation については知らない。調べなくては。weak bisimulation は behavioral equivalence とは違うよね?

(2005-09-16 追記) strong bisimulation が普通のbisimulation。τアクションによる違いを無視するのが weak bisimulation 。http://www.lix.polytechnique.fr/~catuscia/teaching/DEA/General/Exercises_James/exercises.pdf の「4 Definition: CCS operational equivalences」が分かりやすかった。