2001-09-13
λ. だらだら。(￣¬￣)
λ. 読んだ本
- 「D・N・エンジェル - 人魚の涙」 岡崎純子[著] 杉崎ゆきる[原作]
- 「心に星の輝きを」 1巻 松葉博[著]
- 「ジャングルはいつもハレのちグゥ」 3巻 金田一蓮十郎[著]
λ. 「イスラム教徒への暴行事件相次ぐ 米国各地」
予想はしてたけど、まったく気分悪ぅ。
2002-09-13
λ. exp(A,B)のvariance
exp(A,B)のvarianceが「(-,+)」(つまりexpは Cop×C → C のfunctor)だなんて当然じゃないか。何でこれまで理解できなかったんだ……。くやしいので、なんとなく図にしてみる。
考えてみれば On Understanding Types, Data Abstraction, and Polymorphism での関数の type inclusion のルールも「s→t ≦ s'→t' iff s'≦s and t≦t'」だったし、ちゃんと符号してるんだなぁ。
λ. Re: BASTARDのキャラクター名の綴
画集([haq:3098])と小説「悪魔の褥に横たわりて」とで綴りがあっていないことに気が付いた。
| 画集 | 小説 |
|---|---|
| GARA | GALLA |
| ARSHES・NEI | ARSHESS・NEI |
| ABIGAIL | AVIGALE |
| KALL=SU | KAL=SU |
2005-09-13
λ. Windows用バイナリ
を作ったので適当に放置しておく。現在のCVSのソースからビルドしたものは振る舞いが変だったので、5月の時点のソースからビルドした。これらのファイルとemacsさえあれば最低限のことは出来る。あとライブラリは適当にCVSからとってくるべし。
2006-09-13
λ. Pangoで縦書テキストが表示可能に
射撃しつつ前転 (2006-09-13)より。素晴らしい。
以前に「starts at bottom of page」というエントリでは「縦書きの日本語の中にアラビア文字を埋め込む時には、改行方向を合わせるために下から上へ書く気がする」と書いたけど、リンク先のスクリーンショットではアラビア文字を上から下へと書いているな。実際の例を見たことがないので、どちらが正しいかは知らんけど……
【追記】……とか書いていたら、小熊さんから「左縦書きのモンゴル語（蒙古文字）にローマンアルファベットが混じる場合」の事例が。 ありがとうございます。
λ. Haskellのリストとはそもそも何者かという問題
Haskellの代数的データ型の解釈は、OCamlのような正格な言語での解釈よりも確かに複雑だけど、使っていて悩んだ経験はあまり無い。そもそも、Haskellのデータ型にどんな値が存在するかを考えるときに、いちいち領域理論を使って考えたりしないし。……複雑に感じるかどうかには慣れの問題も大きいのではないかと思います。
OCamlでのリスト型の領域は⊥を除けば、全ての有限リストのみからなる集合、すなわち帰納的に定義される集合になっている。一方、Haskellでのリスト型の領域は「⊥を含む値」を除けば、全ての有限および無限のリストからなる集合、すなわち余帰納的に定義される集合になっている。したがって、始代数になっているかはさて置き、帰納的というよりは余帰納的なものとして理解したほうが良いと思います。
ところで、<URL:http://d.hatena.ne.jp/taisuke_h/20060827#1156687935> によると、OCamlでも無限リストがリスト型に属するようです。ということは、きちんと意味論を考えるのならOCamlの場合にもHaskellと同様の領域を考えなくてはいけないような……。それとも「lazy」はHaskellでの「unsafe〜」のように意味論を無視したバックドアなのでしょうか……
【追記】 <URL:http://d.hatena.ne.jp/yoriyuki/20060915/p1> で、Lazyモジュールは型が変わるので問題ないとの指摘。うわー、恥ずかしいことを書いてしまったー orz
【さらに追記】 いや、lazyについては間違いだったけど、「let rec a = 1 :: 2 :: a」は結局無限リストになるのだから、無限リストを含む領域を考えなくてはならないというのは変らないはず。
【追記】 sumiiさんの人から借りてきた２セントも参照のこと。
2008-09-13
λ. 手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み
手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み, 古市祐樹, 西田直樹, 酒井正彦, 草刈圭一朗, 坂部俊樹, 信学技報 SS2006-41 (KBSE2006-17), 電子情報通信学会 (2006年-10月).
項書換えの分野では帰納的定理の証明手法として潜在帰納法や書換え帰納法などが広く研究されている．2つの異なる関数が任意の入力に対して同様の出力を返すことは帰納的定理として捉えられるので,帰納的定理の証明法は関数型プログラムの等価性の検証に利用できる．本研究では,項書換えにおける帰納的定理の証明法を利用して手続き型プログラムの等価性の検証を試みる．具体的には,手続き型プログラムから書換え系への変換を与え,その変換により手続き型プログラムの等価性を項書換え系の関数の等価性に帰着できることを示す．
項書き換え系はこんな使い方も出来るのかと驚いた論文。 項書き換え系について詳しくないので、細かい議論はあまり追えてないのだけど、アイディアがとても面白かった。
手続き型のプログラムから、プログラムカウンタと変数の値とを項で表した、(決定可能)条件付き項書き換え系へと変換する。例えば、
int sum1(int x){
int i=0; int z=0;
while(i<x){
i=i+1; z=z+i;
}
return z;
}
という関数は
sum1(x) → U1(x, 0) U1(x, i) → U2(x, i, 0) U2(x, i, z) → U3(x, i, z) <== i < x U3(x, i, z) → U4(x, Add(i, S(0)), z) U4(x, i, z) → U5(x, i, Add(z, i)) U5(x, i, z) → U2(x, i, z) U2(x, i, z) → U6(x, i, z) <== i >= x U6(x, i, z) → U7(z) U7(y) → y
という項書き換え系になる。
さらに、項書き換え系で書いた仕様
sum0(0) → 0 sum0(S(x)) → Add(sum0(x), S(x))
を用意して、sum0(x) = sum1(x) が帰納的定理であることを、潜在帰納法を使って証明する。
項書き換え系に変換して何が嬉しいかというと、普通なら帰納法が必要な定理の証明を、直接帰納法を用いずに出来る潜在帰納法等の方法があって、自動化がしやすいところ。ただ、この論文の時点ではまだ自動化は出来ていないけど。
ちなみに、こないだの第68回情報処理学会・プログラミング研究会で、同じ著者らの「潜在帰納法を利用した手続き型プログラム検証の試み」という題の発表があった。
2009-09-13
λ. Google Code Jam 2009: Round 1B
参加はしてないけど、Qualification Round と Round 1A に続いてまたプラクティスを解いてみた。 やっぱり、二時間半の時間内に全問解ける気がまるでしないなぁ……
A. Decision Tree
簡単。 特に工夫は不要で、書いてあるとおりにやるだけで何の問題もなかった。
B. The Next Number
数字がすべて降順に並んでいたら繰り上がり。 そうでなかったら、降順になっていない最短のサフィックスを持ってきて、ごにょごにょ。 こういう、単純だけど落ち着いて考える必要がある問題っていいよね。 落ち着いて考えればそんなに難しくはないけど、実際に参加して解いていたら、焦って時間内に解けなかったと思う。
C. Square Math
かなり手間取った。時間内には絶対解けなかったと思う。 望ましい解き方がわからなかったので力技で書いたら、C-small-practice.in はすぐに処理が終わるけど、C-large-practice.in は数十分かかることに……orz なんか、賢い解き方があるんだろうけどなぁ……
【2009-09-23 追記】 ちゃんと考えて解きなおした。 といっても、特に工夫はしてなくて、ただのDFSだけど。 そしたら、C-large-practice.in でも一分程度で終わるようになった。
λ. 第五十六回圏論勉強会
P. Selinger, “A survey of graphical languages for monoidal categories”の 5 Traced categories の最初から 5.5 Braided traced categories の途中まで。
Some notes on monads. Andrea Schalk
