2002-08-27 [長年日記]
λ. 生保の予定利率下げ
保守党の野田党首が、生保の予定利率引き下げを容認すべきだと主張しているらしい。僕も基本的には賛成ですが、どういう形で実現しようとしているのかが気になります。これに関するリチャード・クーの提案は興味深いのですが、ちょっと現実的でないように思えます。
λ. 夢
「クーデター未遂を利用して、腐敗した閣僚を一挙に粛清する大統領」の夢をみました。
λ. コンパイル猿
先日のパッチは「/dev/windowsを使うのはどう?」とのこと。そういえば、そんなのもあったなぁ。cygwin-1.3.12-4/winsup/cygwin/fhandler_windows.ccを見ると以下のように書いてあるので、確かに使えそうだ。内部でバッファリングもしていないようなので、gdk側でPeekMessage()/GetMessage()等が使われている部分もそのままで良いのかな?
The following unix-style calls are supported:
open ("/dev/windows", flags, mode=0)
- create a unix fd for message queue.
O_NONBLOCK flag controls the read() call behavior.
read (fd, buf, len)
- return next message from queue. buf must point to MSG
structure, len must be >= sizeof (MSG). If read is set to
non-blocking and the queue is empty, read call returns -1
immediately with errno set to EAGAIN, otherwise it blocks
untill the message will be received.
write (fd, buf, len)
- send a message pointed by buf. len argument ignored.
ioctl (fd, command, *param)
- control read()/write() behavior.
ioctl (fd, WINDOWS_POST, NULL): write() will PostMessage();
ioctl (fd, WINDOWS_SEND, NULL): write() will SendMessage();
ioctl (fd, WINDOWS_HWND, &hWnd): read() messages for
hWnd window.
select () call marks read fd when any message posted to queue.
撤退するはずが…… (苦笑)
試してみると、前のパッチよりも具合いが良いようだ。うーん、GSourceについての僕の理解が間違ってるのかなぁ。
λ. denotational semantics
ふむふむ。ものすごく難解な数式には見えない気がするけど、Algebraic Specification や Categorical Specification Language も denotational semantics なのかなぁ……
【2006-04-14追記】 コメント欄を参照。Algebraic Specification や Categorical Specification Language 自体は denotational semantics ではない。
λ. 地産が更生法申請
そうか潰れちゃったのか。チサンホテルで合宿したことがあるので、少し懐かしい。
スタックの奴はちょっと他のと記憶が混じったかも．十分に<br>意味が記述できてるんだか検証できなさそうに見えるし．<br><br>再帰的な関数の意味付けとかやりだすと浮動点定理を引っ張<br>りだしてきたり，ってことになるようです．<br><br>代数的仕様記述とその検証っていう話．
少し調べてみました。<br><br>代数的仕様といっても、<br>Algebraic specification 的なものではなくて、<br>むしろ Domain theory 的なものを指すのかな……<br><br>"A Categorical Programming Language" の論文でも<br><br>Algebraic specification methods were first developed to describe what<br>programs do. They are not like operational semantics or denotational<br>semantics. These semantics also describe what programs do but in a<br>different way. They describe it by giving meaning to each part of<br>programs. They need to know how programs are written, that is, they<br>need actual codes. Whereas, algebraic specification methods never talk<br>about how programs are implemented. They describe their behaviour<br>abstractly viewing from outside.<br><br>とか、<br><br>Domain theory was started with denotational semantics [Stoy 77, Scott<br>76]. In order to give denotational semantics to programs, we need<br>several domains to which the denotations are mapped. Those domains are<br>often interwoven and recursively defined. The most famous example of<br>this is the following D.<br> D =~ D -> D<br>This domain D was necessary to give denotational semantics to the<br>untyped lambda calculus. In general, we would like to solve the<br>following domain equation:<br> D =~ F(D)<br>where F(D) is a domain expression involving D.<br><br>とか書いてありました。<br># 「=~」は同型記号のつもり<br><br>> スタックの奴はちょっと他のと記憶が混じったかも．十分に<br>> 意味が記述できてるんだか検証できなさそうに見えるし．<br><br>このスタックの定義はAlgebraic specificationっぽいですね。<br>上記論文では Algebraic specification に基づいたCLEARという言語が<br>紹介されていて、以下のようなリストの定義が載ってました。<br><br>constant List =<br> theory<br> sorts element, list<br> opns nil : list<br> cons : element, list -> list<br> head : list -> element<br> tail : list -> list<br> eqns all e : element, l : list, head(cons(e,l)) = e<br> all e : element, l : list, tail(cons(e,l)) = l<br> endth<br><br>> 再帰的な関数の意味付けとかやりだすと浮動点定理を引っ張<br>> りだしてきたり，ってことになるようです． <br><br>この辺りの話は良く聞くのですが、僕はまだ良く分かってなかったり。<br>lattice theory や domain theory ってすっごく重要だと思うのですが、<br>なかなかきっかけが無くて……<br><br># きっと、原さんとかはこの辺り詳しいんだろうなぁ。<br># ……とか書いてみる。
ちらっと調べてみましたが、形式的にやろう、と<br>いうのとは反対な路線っぽい気がします。<br>λx.f(x)<br>みたいな物の性質をそのまま扱うのではなく、<br>具体的なドメインを用意してやって、<br>Dー＞D<br>の写像という範囲でいろいろやっていく、というような。<br>+を結合則等から議論するのでは無く、<br>具体的なドメインを持ち込んで、<br>1+1は2じゃん、という風な、<br>直感的というかある程度いい加減な世界っぽい気がしました。<br>識者の突っ込み求む。
知識処理論の講義資料を読み返してたら、<br>何となく分かってきたような気がします。<br>http://www.tom.sfc.keio.ac.jp/~hagino/kp00/
なるほど。<br>シンタックスを数学的な要素にマッピングする事ですか。