2007-07-02 [長年日記]
λ. “A formulae-as-types interpretation of Subtractive Logic” by Tristan Crolard
昔読みかけて放置してた論文なのだけど、こないだのコルーチンの話で思い出して、読んでみた。色々と面白い。
複数の結論を持つシーケントを考えるので、判定(judgement)の書き方が、型理論の通常のそれと異なっているのが新鮮。例えばこんな感じ。
t : Γ ├ Δ; A ---------------------------------------------- make-coroutine t β : Γ ├ Δ, B^β; A - B
2007-07-04 [長年日記]
λ. 『入門OCaml — プログラミング基礎と実践理解』
OCamlには以前挫折したが、最近またOCamlを使いだしたので、この本を読んでいる。
関連
メモ。
p.60
直積型は、複数の型を積み上げて1つの型とすることを抽象化している。
積み上げる???
p.121 幽霊型の説明でいきなりconstraintキーワードってのが出てきて良くわからなかった。
あと、幽霊型と言われて私は James Cheney と Ralf Hinze の「Phantom Types」のようなものを想像したんだけど、違うのね。この論文を読み返したらこんな風に書いてあった。 なるほどなるほど。
The term phantom type was originally coined by Leijen and Meijer [17] to denote parameterized types that do not use their type argument(s). They use phantom types for type-safe embeddings of domain specific languages into Haskell. Their approach is, however, strictly more limited: while they can enforce type constraints when constructing values of a phantom type, they cannot make use of these constraints when decomposing a value. Our proposal exactly fills this gap.
p.157 「サブタイプへのキャストには “:>”演算子を使います」とあるけど、サブタイプではなくスーパータイプでは?
列多相(row polymorphism)。素朴な疑問なのだが、何故「行多相」ではなく「列多相」なのだろう?
p.161 の列多相性と比較されているJavaのコードが変。Javaでも(bounded polymorphism はあるし)普通に書けばダウンキャストは不要のはず。記述の簡潔さを除けば列多相の優位性を示せていないと思う。
class Base {};
class Sub1 extends Base { void cons(){} };
class Sub2 extends Base { void snoc(){} };
class Container<X extends Base> {
X x;
Container(X x_) { x = x_; }
X peek() { return x; }
};
Sub1 c = new Sub1();
Container<Sub1> container = new Container<Sub1>(c);
container.peek().cons();
Sub2 s = new Sub2();
Container<Sub2> container2 = new Container<Sub2>(s);
container2.peek().snoc();
2007-07-05 [長年日記]
λ. CLEAR FILE
「CLEAR FILE」と書かれているのを見て、代数的仕様記述言語CLEARのファイル形式か何かだと一瞬思ってしまった。疲れてるな。
ちなみに、CLEARは以下のような感じの言語。
constant Triv =
theory
sort element
endth
procedure Prod(A:Triv,B:Triv) =
theory
data sort prod
opns pair: element of A,element of B -> prod
pi1 : prod -> element of A
pi2 : prod -> element of B
eqns all a:element of A,b:element of B,
pi1(pair(a,b)) = a
all a:element of A,b:element of B,
pi2(pair(a,b)) = b
endth
この例はCPLの論文からとってきた例で、ここでは直積型の仕様を記述している。
詳しくはこの辺りの論文でもどうぞ。私は読んだことないけどね。
- Burstall, R. M. and Goguen, J. A. (1980): The Semantics of Clear: A Specification Language. Internal Report CSR-65-80, Department of Computer Science, University of Edinburgh.
- Burstall, R. M. and Goguen, J.A. (1982): Algebras, Theories and Freeness: an Introduction for Computer Scientists. Internal Report CSR-65-80, Department of Computer Science, University of Edinburgh.
2007-07-06 [長年日記]
λ. Eager Haskell
最近、たまたま Eager Haskell というものの存在を知った。 積極評価が基本で、決められたリソースの上限を超えたら遅延評価にフォールバック。Haskellの意味論を変えること無しに、遅延評価の非効率性を避けることが出来る。これがあると例えば末尾再帰のときとかに嬉しいはず。
2007-07-07 [長年日記]
λ. Ruby-GNOME2のコールバック周りを少し整理
Rubyと関係ないネイティブスレッドからコールバックが呼ばれた場合にはRubyのスレッドに転送してから実行すべきなのだが、その部分がGRClosureにべったりだったので、分離してRuby-GNOME2の他のコールバックの処理でも使えるようにしてみた。
また、これまでのコードではコールバックの転送を待っているスレッドで受け取ったコールバックをそのまま実行すると、その内部で更にコールバックが発生したときにデッドロックしてしまうという問題があった。 これを回避するために、受け取ったコールバックの実行は新たに生成したスレッドで行うようにした。 ただ、これ効率悪いな。スレッドの生成が相対的に重い1.9では特に重いはず。 スレッドプールを作ってスレッドを使いまわすべきか。
また、1.9ではis_ruby_native_thread()が機能しなくなった(参考 [ruby-dev:31166])ので、コールバックの側で現在のスレッドがRubyのネイティブスレッドなのか判別できず、たとえ現在のスレッドがRubyのスレッドだとしても転送しなくてはならなくなっている。これは切ない。なんとかならないのかなぁ。
- 現在のスレッドがRubyのネイティブスレッドで、かつGVL(Giant VM Lock)を保持しているのなら、そのまま呼び出したい。
- 現在のスレッドがRubyのネイティブスレッドで、もしGVLを手放しているのなら、GVLを再び確保した上で、そのまま呼び出したい。
……と書いたが、[ruby-dev:31162]で落ちるので、1.9ではまだ試せていないのだった。
λ. Mutexとかめんどい
Ruby-GNOME2のコールバック周りをいじったときに、久しぶりにMutexやConditionVariableを使ったコードを書いたのだけど、面倒くさいな。 せめてMVarくらいあれば良いのにと思ってしまう。
2007-07-08 [長年日記]
λ. 第三十一回圏論勉強会
今回、面白かったのは、以下の練習問題。
For n≧2, not every n-ary function which is computable in each argument needs to be computable. (Hint: take g total nonrecursive and set f(x,y) = g(min{x,y}) ).
最初、「fは各成分についても計算可能ではないのでは?」*1と思ってしまったけど、ちゃんと計算可能だった。直観的には、f(n,-) では n 以下の自然数は有限個なので、それらに対するgの値をテーブルとして持てば良い。
*1 で、この本、また間違ってるよ、と思った;-)
2007-07-09 [長年日記]
λ. haskell-jpのアーカイブ
昨日の圏論勉強会の際に、今のhaskell-jpのアーカイブが無いという話があった。移転前のquickmlのはbladeにアーカイブがあるんだけどねぇ。 仕方ないので、w3ml(+ w3ml 拡張・修正パッチ)で現在のhaskell-jpのアーカイブをでっち上げてみた。
まだ、自動更新にはしていない。 しかし、このメーリングリストは、X-ML-Countのようなヘッダも付かないし、その上Subjectにも番号が入らないときがあって、いやらしいな。
λ. ruby-gnome2-devel-jaのアーカイブ
ついでにruby-gnome2-devel-jaのアーカイブもでっち上げてみた。
2007-07-10 [長年日記]
λ. ヘッダにしかない関数
mkmf.rb を濫用して調べてみる([ruby-dev:31176])。 ささださんが「他にも、いろいろあるようですね」と言っていたが、本当に色々あるなw
λ. 油売り算
キミならどう書く 2.0 - 2007 - その 1。 どうせHaskellプログラムとかは誰か書くだろうから、モデル検査で解を探してみる。「プログラムを書け」という問題の回答にはならないけど、プログラムなんか書かずに済むのなら書かないほうが良いだろう。
モデル検査ツールにも色々あるのだけど、いつも使っているNuSMVだと変数別に規則を書かなくてはならないのが面倒だったので、今回はよりプログラミング言語っぽい記述が可能なSpinに初挑戦してみた。
Spin(Promela)でモデルを記述すると以下のような感じになる。 aburaというプロセスが非決定的に油を移している。
#define A 10
#define B 7
#define C 3
int a = 10
int b = 0
int c = 0
inline move(from, to, cap)
{
atomic{
if
:: from > 0 && to < cap ->
if
::from+to<cap -> to = from+to; from = 0
::else -> from = from+to-cap; to = cap
fi
:: else -> skip
fi
}
}
active proctype abura()
{
do
:: true -> move(a, b, B)
:: true -> move(a, c, C)
:: true -> move(b, a, A)
:: true -> move(b, c, C)
:: true -> move(c, a, A)
:: true -> move(c, b, B)
od
}
で、ここで何を検証するかというと、「任意有限ステップ後に a=5 かつ b=5 の状態に到達しない」こと。これをSpinにかけてやると、本当に到達しないなら検証に成功し、もし到達する可能性があるなら「反例」として「到達するパス」を教えてくれる。
というわけで、XSpinで「!<>(p && q)」を検査。 ただし、ここで p と q は以下のような定義。
#define p (a==5) #define q (b==5)
そうすると、「Verification Result: not valid」とか言われるので、「Run Guided Simulation」で「Run」を選んで反例のトレース見てみる。
preparing trail, please wait...done Starting abura with pid 0 spin: couldn't find claim (ignored) 2: proc 0 (abura) line 26 "pan_in" (state 1) [(1)] 4: proc 0 (abura) line 13 "pan_in" (state 2) [(((a>0)&&(b<7)))] 5: proc 0 (abura) line 16 "pan_in" (state 6) [else] 6: proc 0 (abura) line 16 "pan_in" (state 7) [a = ((a+b)-7)] < 6: proc 0 (abura) line 16 "pan_in" (state 8) [b = 7] < 8: proc 0 (abura) line 27 "pan_in" (state 17) [(1)] 10: proc 0 (abura) line 13 "pan_in" (state 18) [(((a>0)&&(c<3)))] 11: proc 0 (abura) line 16 "pan_in" (state 22) [else] 12: proc 0 (abura) line 16 "pan_in" (state 23) [a = ((a+c)-3)] < 12: proc 0 (abura) line 16 "pan_in" (state 24) [c = 3] < 14: proc 0 (abura) line 28 "pan_in" (state 33) [(1)] 16: proc 0 (abura) line 13 "pan_in" (state 34) [(((b>0)&&(a<10)))] 17: proc 0 (abura) line 15 "pan_in" (state 35) [(((b+a)<10))] < 17: proc 0 (abura) line 15 "pan_in" (state 36) [a = (b+a)] < 17: proc 0 (abura) line 15 "pan_in" (state 37) [b = 0] < 19: proc 0 (abura) line 31 "pan_in" (state 81) [(1)] 21: proc 0 (abura) line 13 "pan_in" (state 82) [(((c>0)&&(b<7)))] 22: proc 0 (abura) line 15 "pan_in" (state 83) [(((c+b)<7))] < 22: proc 0 (abura) line 15 "pan_in" (state 84) [b = (c+b)] < 22: proc 0 (abura) line 15 "pan_in" (state 85) [c = 0] < 24: proc 0 (abura) line 27 "pan_in" (state 17) [(1)] 26: proc 0 (abura) line 13 "pan_in" (state 18) [(((a>0)&&(c<3)))] 27: proc 0 (abura) line 16 "pan_in" (state 22) [else] 28: proc 0 (abura) line 16 "pan_in" (state 23) [a = ((a+c)-3)] < 28: proc 0 (abura) line 16 "pan_in" (state 24) [c = 3] < 30: proc 0 (abura) line 31 "pan_in" (state 81) [(1)] 32: proc 0 (abura) line 13 "pan_in" (state 82) [(((c>0)&&(b<7)))] 33: proc 0 (abura) line 15 "pan_in" (state 83) [(((c+b)<7))] < 33: proc 0 (abura) line 15 "pan_in" (state 84) [b = (c+b)] < 33: proc 0 (abura) line 15 "pan_in" (state 85) [c = 0] < 35: proc 0 (abura) line 27 "pan_in" (state 17) [(1)] 37: proc 0 (abura) line 13 "pan_in" (state 18) [(((a>0)&&(c<3)))] 38: proc 0 (abura) line 16 "pan_in" (state 22) [else] 39: proc 0 (abura) line 16 "pan_in" (state 23) [a = ((a+c)-3)] < 39: proc 0 (abura) line 16 "pan_in" (state 24) [c = 3] < 41: proc 0 (abura) line 31 "pan_in" (state 81) [(1)] 43: proc 0 (abura) line 13 "pan_in" (state 82) [(((c>0)&&(b<7)))] 44: proc 0 (abura) line 16 "pan_in" (state 86) [else] 45: proc 0 (abura) line 16 "pan_in" (state 87) [c = ((c+b)-7)] < 45: proc 0 (abura) line 16 "pan_in" (state 88) [b = 7] < 47: proc 0 (abura) line 28 "pan_in" (state 33) [(1)] 49: proc 0 (abura) line 13 "pan_in" (state 34) [(((b>0)&&(a<10)))] 50: proc 0 (abura) line 15 "pan_in" (state 35) [(((b+a)<10))] < 50: proc 0 (abura) line 15 "pan_in" (state 36) [a = (b+a)] < 50: proc 0 (abura) line 15 "pan_in" (state 37) [b = 0] < 52: proc 0 (abura) line 31 "pan_in" (state 81) [(1)] 54: proc 0 (abura) line 13 "pan_in" (state 82) [(((c>0)&&(b<7)))] 55: proc 0 (abura) line 15 "pan_in" (state 83) [(((c+b)<7))] < 55: proc 0 (abura) line 15 "pan_in" (state 84) [b = (c+b)] < 55: proc 0 (abura) line 15 "pan_in" (state 85) [c = 0] < 57: proc 0 (abura) line 27 "pan_in" (state 17) [(1)] 59: proc 0 (abura) line 13 "pan_in" (state 18) [(((a>0)&&(c<3)))] 60: proc 0 (abura) line 16 "pan_in" (state 22) [else] 61: proc 0 (abura) line 16 "pan_in" (state 23) [a = ((a+c)-3)] < 61: proc 0 (abura) line 16 "pan_in" (state 24) [c = 3] < 63: proc 0 (abura) line 31 "pan_in" (state 81) [(1)] 65: proc 0 (abura) line 13 "pan_in" (state 82) [(((c>0)&&(b<7)))] 66: proc 0 (abura) line 15 "pan_in" (state 83) [(((c+b)<7))] < 66: proc 0 (abura) line 15 "pan_in" (state 84) [b = (c+b)] < 66: proc 0 (abura) line 15 "pan_in" (state 85) [c = 0] < 68: proc 0 (abura) line 26 "pan_in" (state 1) [(1)] spin: trail ends after 69 steps #processes: 1 69: proc 0 (abura) line 21 "pan_in" (state 16) 1 processes created
思ったよりもだいぶ長いトレースが出てきたけど、 代入文を追いかけてみると、こんな感じになっている。
a から b に 7 升移す ((10,0,0) → (3,7,0)) a から c に 3 升移す ((3,7,0) → (0,7,3)) b から a に 7 升移す ((0,7,3) → (7,0,3)) c から b に 3 升移す ((7,0,3) → (7,3,0)) a から c に 3 升移す ((7,3,0) → (4,3,3)) c から b に 3 升移す ((4,3,3) → (4,6,0)) a から c に 3 升移す ((4,6,0) → (1,6,3)) c から b に 1 升移す ((1,6,3) → (1,7,2)) b から a に 7 升移す ((1,7,2) → (8,0,2)) c から b に 2 升移す ((8,0,2) → (8,2,0)) a から c に 3 升移す ((8,2,0) → (5,2,3)) c から b に 3 升移す ((5,2,3) → (5,5,0))
というわけで、探索をプログラムせずとも答えを得れたと。 これくらい単純な例だと探索を自分でプログラムしても大したことはないけど、扱う状態遷移系が複雑になると、自分で探索を行うプログラムを書くのは結構しんどいことになる。 そんな時にはモデル検査は非常に便利。
詳しくは4日で学ぶモデル検査 (初級編) (CVS教程 (1))(産業技術総合研究所システム検証研究センター)でもどうぞ(読書記録)。
ところで、ところで使ってみて知ったのだけど、Spinでモデル検査するときって、一回C言語のコードを出力してコンパイルして、それを使って検査しているんだな。 なんというか、それだけやっても十分割りにあうということか。
追記
masateruさんという方のmixi日記にて、別の回答が紹介されている。 assertを使う方法など、初心者の私には大変勉強になりました。
2008-07-05追記
「NuSMVだと変数別に規則を書かなくてはならない」と書いたが、これは間違い。これを書いた時点では ASSIGN で init(x) と next(x) に対する代入という形で書く方法しか知らず、その場合には変数別に規則を書く必要があるが、実際にはTRANSを使って遷移関係を直接記述する方法もあり、その場合にはこういった問題は無い。
2007-07-11 [長年日記]
λ. emacsagda-utf8
<URL:http://unit.aist.go.jp/cvs/Agda/>で配布されているWindowsパッケージ(Agda_1_0_2.exe)には emacsagda-utf8 というコマンドが付属しているのに気付いた。以下のような設定をすれば、ファイルをlatin-1ではなくutf-8で書けるようになる。
(setq agda-program "emacsagda-utf8") (modify-coding-system-alist 'process "emacsagda-utf8" 'utf-8)
latin-1 なemacsagdaでは、latin-1の記号を使う都合上ファイルを latin-1 で保存せねばならず、そのためコメントにも日本語が使えず不便だった。しかし、これでこの問題も解決。 ただし、「"ほげほげ"」のようなリテラルは通るが、「"\12411\12370\12411\12370"」のような(Haskellの文法上正しい)リテラルはエラーになってしまうなぁ。
ところで、Agdaの公式サイトがいつのまにか産総研のところになっていて少し驚いたよ。
2007-07-12 [長年日記]
λ. foldl.com と foldr.com
foldl.com と foldr.com というサイトがある。 fold好きの人は、右派、左派に関わらずどうぞ。
<URL:http://lambda-the-ultimate.org/node/1395> で知ったのだが、そこでの議論はなんか微妙ものが多いな。
λ. Basic Spin Manual 日本語訳
Basic Spin Manual の Masateru Kawaguchi さんによる日本語訳。
4日で学ぶモデル検査 (初級編) (CVS教程 (1))(産業技術総合研究所システム検証研究センター)(読書記録)は「使い方」の説明がメインで、例題を解くために必要な部分以外についてはあまり解説されていなかった。 このマニュアルでは『4日で学ぶモデル検査』に欠けていた、SpinやPromelaの基礎について知ることが出来て良かった。 訳者のMasateruさんに感謝。
2007-07-17 [長年日記]
λ. 初遅刻
初遅刻。 といっても、別に寝坊したわけではなくて電車の遅延のため。 しかし、いつもよりも20分以上長く満員電車に詰め込まれていたため、朝から疲れたよ。
2007-07-19 [長年日記]
λ. 君は修悦体を知っているか
スラッシュドット ジャパン | ガムテープによる独特なフォント「修悦体」 より。そういえば、見たことがある気がする。こうして見ると凄いな。
2007-07-20 [長年日記]
λ. ICFP Programming Contest 2007
<URL:http://save-endo.cs.uu.nl/>
今年の問題もストーリーが面白い。
しかし、Endoって名前はwwww*1 kuma--の中の人がモーフィングしている様を想像してしまって、たけをさんと二人で爆笑。
続き
- ICFP Programming Contest 2007 (2) - ヒビルテ (2007-07-21)
- ICFP Programming Contest 2007 (3) - ヒビルテ (2007-07-22)
- ICFP Programming Contest 2007 (4) - ヒビルテ (2007-07-23)
関連エントリ
- “Ropes: an Alternative to Strings” by Hans-J. Boehm, Russ Atkinson and Michael Plass - ヒビルテ (2007-07-25)
- 文字列検索の性能 - ヒビルテ (2007-08-07)
*1 もちろん、実際はendomorphismとかのendo-なんでしょうけど
![[大根そば]](./images/20070720_0.jpg)
2007-07-21 [長年日記]
λ. RHG読書会
Hikidocのコードにショックを受ける。
λ. ICFP Programming Contest 2007 (2)
AyaCFPというチームに入れてもらいました。
RHG読書会へ向かう電車で問題文を読み、帰りの電車でDNAを実行してRNAを生成する部分を書いた。が、バグってて帰ってきてからちょっとデバッグ。動くようにはなったが、遅すぎて使い物にならない。
ところで、今回初めてLingrを使ったのだけど、これ便利だね。
2007-07-22 [長年日記]
λ. ICFP Programming Contest 2007 (3)
DNA→RNA の変換が遅くて話にならないので、高速化しようとごにょごにょしてたら、バグってやる気をなくす。
(中略)
他の方がRNAを実行する部分を完成させていたので、ふと遅いままのDNA→RNAの変換機を例のprefixに対して適用してみたら、予想に反してすぐに終わった。こんなことならもっと早く試していればよかった。結果のRNAを実行してもらったら(略)。
ようやく入り口という感じだが、ちょっとやる気が出てきたし、方針も少し見えてきた。 しかし、もう夜。明日は会社だし、もう無理か。 無念。
それにしても、やはり私にはプログラミングの才能は無いんだな。
2007-07-23 [長年日記]
λ. ICFP Programming Contest 2007 (4)
なんか、諦めがつかなかったので、午後半休を取得してもう少し足掻く。 見込みもないのにこんな事の為に休むなんて、自分でもどうかしてると思うが。
昨日も書いたけど、DNA→RNA のruby版は文字列の連結(とGC)がボトルネックなのが明らかで、それをどうしようかと悩んでいた。
Rubyの文字列の連結は O(n) であり、そりゃこれだけ長大なデータの連結が大量に発生すれば重くなる。 昨日はこの問題を解決するために「文字列を単一のStringで表現する代わりに、チャンクの配列で表現して……」というのをアドホックにやろうとして、バグってやる気をなくしてたのだった。 文字列の表現を変えると Regexp なんかもそのまま適用できなくなるし、面倒くさいことこの上ない。 どうでも良いが、高速に連結可能な文字列実装すら標準ライブラリに存在しないのに、「テキスト処理関係の能力などに優れ」(「Rubyとは」)というのは何だか微妙な気がしないでもない。
流石にアドホックにやっててもなぁと思い、ちゃんとしたデータ構造を使おうと思ったのだけど、Rubyでデータ構造を書くのは面倒くさいので、とりあえずHaskellで。
最初は Purely Functional Data Structures に載っている O(1) で連結可能なデータ構造 Catenable List を実装しようとした。 で、Catenable List の実装にはキューを使うのだが、Data.Queue を使おうとしたら、「Warning: Module `Data.Queue' is deprecated: Use Data.Sequence instead: it's faster and has more operations」とか言われてしまった。 「そういや Sequence なんてのもあったな」と思って調べてみると、こいつの連結コストは O(log(min(n,m))) 。Catenable List の O(1) よりは重そうだけど、「既にある」というのは手軽なのでまずはこっちを試してみることに。
丁度、nobsun の ByteString 版のコードがあって、ByteString と Sequence はインターフェースがほぼ同じなので適当に書き換える。findSubstring だけは Sequence 側に近いコードが無かったので適当にでっち上げた(BM法すらちゃんと知らない*1ので本当に適当。なお、このコードには性能上の問題があった)。 最初少しバグっていたけど、すぐに直った。 こいつに endo.dna を食わせると1分くらいでRNAの生成が完了した。 使用メモリが心配だったのだけど、たったの150MBくらいだった。 おお、Haskellすげー。 こんなことなら私も最初からHaskellで書いていればよかった。 nobsunは正しかったよ。
で、生成されたRNAをまた描画プログラムにかけてもらった*2ら、なんか変なモアレっぽい画像が。 source.pngの画像か、もしくは何か描画ルーチンを探すのに役立ちそうなものが出てくるかと思ったのに…… ここでまた詰まってやる気を無くす。
でもまあ、これが本当に正しい描画結果かどうか分からないしな。それを確かめるためにも自分の環境で描画プログラムが動かないと不便なので、描画プログラムのソースコードをだらだらと追いかける。 そんなことをしているうちに時間切れ。
ちょうど時間切れ後に、単に入力のRNAの与え方が違っていただけということに気付く。アホ過ぎだ、こんなことに一日悩んでいたのかよ。 さらに、それより少し前に描画プログラムの修正版が出来ていたようで、修正版に食わせたら今度こそ source.png の画像が出てきた。 さらに、他の方が描画途中に最初のヒントが現れている事に気づく。 ……本当に、丁度入り口付近に辿りついたところで終了という感じ。
しかしまあ、全然歯は立たなかったけど、とても楽しかった。 AyaCFPのみなさん、そして誘ってくれたnobsun、本当にありがとう!
Random-access list?
<URL:http://shuns.sakura.ne.jp/?%BD%B5%B5%AD> の 2007-7-23 「ICFP contest(not ICFP)」に、「dna2rnaの実装についてですが、関数型なら個人的に最もエレガントな解法、というか自分ならこれで書くかなと思ったのは Random-access listかFinger-treesで」と書いてあるが、この Random-access list は catenable list か何かの間違いではないだろうか。Random-access list は連結も部分文字列取り出しも特に速くないはずなので。
2007-07-24 [長年日記]
λ. トートロジー判定問題の計算量
(古典命題論理の)充足可能性問題(SAT)がNP完全なので、その補問題である(古典命題論理の)トートロジー判定問題はco-NP完全になるそうだ。 ということは証明可能であることを検査する Wang's Algorithm も計算量は co-NP ということか。
NP や co-NP のような計算量って、あまり興味がなかったのだけど、実は結構身近な話だったんだな。
2007-07-25 [長年日記]
λ. “Ropes: an Alternative to Strings” by Hans-J. Boehm, Russ Atkinson and Michael Plass
を読んだ。
d.y.d. - ICFP Programming Contest 2007 経由で w.l.o.g - ロープ より。稲葉さんのこの記事は以前にも読んでいたはずなのに、ICFP Programming Contest 2007 の期間中は思い出すことも出来なかった。残念。
稲葉さんの記事に付け加えることはほとんどないのだけど、ロープがバランスしていることをフィボナッチ数を使って定義しているのが少し面白かった。深さ n のロープがバランスしているのは文字列として長さが fib(n+2) 以上のとき。 ちなみに、フィボナッチ数が使われる他のデータ構造にはフィボナッチヒープがある。
しかしね、Rebalanceのところを読んでいて「The resulting rope will not be balanced in the above sense」とか書いてあったのには笑った。 ちょっ、おまっwww まあ、その後には「but its depth will exceed the desired value by at most 2.」と続いてるんだけどね。
【7/30追記】 Haskellで基本的な部分だけ書いてみた。Rope.hs
λ. Shiroさんによる文字列実装の比較まとめ
だいありー (2005-07-20) から派生して、Shiroさんが [yarv-dev:541] Re: [im]mutable string で文字列実装を比較してまとめていたのを思い出した *1。 このスレッドの[yarv-dev:542] でもRopeの論文が言及されていた。
*1 lang-smith のメールだと思いこんで探していたら、yarv-devのメールだったので、ちょっと探すのに手間取った。
![[オムシチュー]](./images/20070726_0.jpg)
2007-07-27 [長年日記]
λ. 空集合から空集合への関数空間 ∅∅
空集合から空集合への関数空間 ∅∅ は当然 {∅} だと思っていたのだが、論理と計算のしくみ(萩谷 昌己/西崎 真也) の問題の解答(p.245)には「∅∅ は定義されない」と書いてあった。
∅∅ は定義されない(これは関数の定義にもよる．A から B への関数を A×B の部分集合と考えるならば，∅∅ = {∅} と考えることもできよう．しかし，A≠∅ ならば，A∅ は一つの関数からなる集合であり，一方 ∅A=∅ でもあるので，これらの二つの場合が交錯する ∅∅ という式は，矛盾していると考えることも出来る)．
この本では関数を「集合 A から集合 B への関数(function)とは，A の各要素に B の要素を与える対応のことである」としか定義しておらず、この定義では通常 ∅∅={∅} なのに、「これは関数の定義にもよる」と言われてもなぁ。 しかも、A≠∅ ならば A∅ と ∅A は重ならないし(言いたいことはわからんでもないけど)。
それにしても、∅∅ を未定義とするというのは初めて見たのだが、これってどこかの分野の流儀なのだろうか? こうしてしまうと、 Set を圏にするときに hom(∅, ∅) をどうするかとか、色々と不都合があるように思うのだが……
【8/8追記】 sumiiの日記 - 0の0乗 の追記で知った*1のですが、<URL:http://nicosia.is.s.u-tokyo.ac.jp/pub/staff/hagiya/shikumi/errata.html> に訂正があって、∅∅={∅} に訂正されている。丁度、質問メールを書こうとしていた矢先だったのだけど、もし私の指摘が原因で訂正されたのだとしたらちょっと嬉しいなぁ。
*1 ありがとうございます、sumiiさん。
λ. Setoidの訳は亜集合?
帰りの電車の中でふと「Groupoidの訳語が『亜群』ならば、Setoidの訳語は『亜集合』なのだろうか?」と思ったのだけど、後で検索した限りではそのような訳語は使われていなかった。ちょっと残念。
- Groupoid
- 射が全て同型射である(小さな)圏
- Setoid
- 集合(Set)に同値関係を加えたもの。
2007-07-28 [長年日記]
λ. 東方風神録体験版ver0.02a
キター!!
博麗神社例大祭での配布は大分から指を咥えて見ているしかなかった(20070505#p01, 20070520)ので、体験版のWebでの公開は非常に待ち遠しかった。嬉しい。早速、マニュアルも読まず初プレイ(リプレイ, スコア45127560)。速攻で被弾しまくりw
今回はスペルカード発動の瞬間に「Spell Card Attack!!」という文字列が斜めに流れる演出が入っているのが新鮮で、なんだかちょっとカッコ良い。
今日のハイスコアはノーマル霊夢(封魔針)での93461910点(リプレイ)。最後に河童「お化けキューカンバー」を落としたのと、その前に霊撃を使ってしまったのが勿体なかった。あと少しで一億だったのに。
λ. 栄光のグラスゴーHaskellコンパイルシステム利用の手引き
The Glorious Glasgow Haskell Compilation System User's Guide の日本語訳。日本語訳をしている人がいるとは知りませんでした。素晴らしい!
2007-07-29 [長年日記]
λ. animation for concepts ＠ ニコニコ
某氏の日記より。 2005年の正月に放送された「『考え方』が動きだす 〜 佐藤雅彦研究室のアニメーション・スタディ 〜」がニコニコ動画にあがっていた。 懐かしいなぁ。
【追記】
λ. “Finger Trees: A Simple General-purpose Data Structure” by Ralf Hinze and Ross Paterson
を読んだ。
こないだの ICFP Programming Contest で使った Data.Sequence の実装に使われているデータ構造が Finger Tree 。コンテスト終了後に某氏に「Finger Tree って知ってる? 純粋関数型雑記帳の田中さんはそれ使って実装したらしいよ」みたいな事を聞かれて、「へー、そんなデータ構造があるんだー」とか思ったのだけど、実は知らずに自分も使っていたという(笑
データ構造自体も面白いが、Measured クラスが面白い。
しかし、こういうnewtypeの使われ方を見ていると、HaskellにもMLのfunctorが欲しくなるね。Wearing the hair shirt: a retrospective on Haskell には、型クラス等を用いるHaskellのアプローチと比較して MLの functor は「High power, but poor power/cost ratio」だと書いてあったけどさ。
2007-07-31 [長年日記]
λ. ezmlm-idxでメールヘッダにシーケンスナンバーをつける
headerraddファイルに「X-Sequence: <#n#>」という一行を追加すれば良い。
