トップ «前の日記(2002-08-26) 最新 次の日記(2002-08-28)» 月表示 編集

日々の流転


2002-08-27 [長年日記]

λ. 生保の予定利率下げ

保守党の野田党首が、生保の予定利率引き下げを容認すべきだと主張しているらしい。僕も基本的には賛成ですが、どういう形で実現しようとしているのかが気になります。これに関するリチャード・クーの提案は興味深いのですが、ちょっと現実的でないように思えます。

Tags: 時事

λ.

「クーデター未遂を利用して、腐敗した閣僚を一挙に粛清する大統領」の夢をみました。

λ. コンパイル猿

先日のパッチは「/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についての僕の理解が間違ってるのかなぁ。

Tags: gtk

λ. denotational semantics

ふむふむものすごく難解な数式には見えない気がするけど、Algebraic Specification や Categorical Specification Language も denotational semantics なのかなぁ……

【2006-04-14追記】 コメント欄を参照。Algebraic Specification や Categorical Specification Language 自体は denotational semantics ではない。

λ. 地産が更生法申請

そうか潰れちゃったのか。チサンホテルで合宿したことがあるので、少し懐かしい。

λ. 水泳

今日も近くのプールへ。先日よりはだいぶ気温も高く気持良かった。天気も良かったし、少し日焼けしたかな。

とりあえず1km。今日はまだまだ泳げそうだったけど、時間切れ。

本日のツッコミ(全5件) [ツッコミを入れる]
ψ kjana (2002-08-28 13:32)

スタックの奴はちょっと他のと記憶が混じったかも.十分に<br>意味が記述できてるんだか検証できなさそうに見えるし.<br><br>再帰的な関数の意味付けとかやりだすと浮動点定理を引っ張<br>りだしてきたり,ってことになるようです.<br><br>代数的仕様記述とその検証っていう話.

ψ さかい (2002-08-29 02:19)

少し調べてみました。<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># ……とか書いてみる。

ψ 有野 (2002-08-29 22:56)

ちらっと調べてみましたが、形式的にやろう、と<br>いうのとは反対な路線っぽい気がします。<br>λx.f(x)<br>みたいな物の性質をそのまま扱うのではなく、<br>具体的なドメインを用意してやって、<br>Dー>D<br>の写像という範囲でいろいろやっていく、というような。<br>+を結合則等から議論するのでは無く、<br>具体的なドメインを持ち込んで、<br>1+1は2じゃん、という風な、<br>直感的というかある程度いい加減な世界っぽい気がしました。<br>識者の突っ込み求む。

ψ さかい (2002-08-29 23:50)

知識処理論の講義資料を読み返してたら、<br>何となく分かってきたような気がします。<br>http://www.tom.sfc.keio.ac.jp/~hagino/kp00/

ψ 有野 (2002-08-30 09:54)

なるほど。<br>シンタックスを数学的な要素にマッピングする事ですか。