2001-09-02
λ. ポアロの「エッジウェア卿の死」(Lord Edgware Dies)をビデオで見た。クリスティはやっぱミステリの女王と呼ばれるだけあるなぁ。それから、いまさらだけど"A Leap in the Dark" (The New York Times, 2001.7.8)を読んだ。ニューヨークタイムズって登録しないと読めないのね…
λ. eval-expression
EmacsはM-:でeval出来るんだ。知らんかった。便利。
2002-09-02
λ. starts at bottom of page
縦書きの日本語の中にアラビア文字を埋め込む時には、改行方向を合わせるために下から上へ書く気がします*1が、その事なのかなぁ……
*1 縦書き日本語の中にアラビア文字を埋め込んだ例を実際に見たことがないので、実際のところはわからないけど。アラビア語の授業を取っている知人に聞いても良くわからなかった。
λ. mozilla 1.1
入れてみた。若干変な部分や不安定な部分があるような気がするけど、概ね快適。
λ. キャラクター・アート展
フジサワ名店ビルでやってたのを見に行こうと思っていたのに、すっかり忘れてしまったいた。
λ. DRbにセキュリティ・ホール
DRbにセキュリティ・ホールを見つけました。DRbServer#threadの$SAFEを上げてない限り、何でも出来てしまいます。これは後で咳さんに報告せねば……
λ. 夢
どっかの駅にいる。まだ朝早く人はまばら。プラットフォームへと階段を降りると、すぐ近くに何か黒いものがぶら下がっている。見てみると人だった。首を吊ったようだ。黒っぽいセーラー服を着ているのを見ると、どこかの学生だろうか。顔は良く見えない。何だかカラスよけに吊されているカラスの死体を連想させる。
いつのまにかやってきていた電車に乗ると、シートを占領して寝そべって雑誌を読んでいる女性がいる。その隣しか空いていなかったのでそこに座る。瞳が綺麗。話してみると、先ほどの首吊り死体の姉らしい。
ψ 咳 [むー。報告まってます。]
ψ なひ [dRubyはそういうもんだと理解してます。「$SAFEがあがってなければなんでもできます」というRubyの機能を、そ..]
ψ さかい [たしかに、もとのRubyが「何でもあり」だから、 そこから制限していってセキュリティを確保しようというアプローチには..]
ψ 咳 [privateは呼べないようにするけど、メソッドの制限はなくそうかと 思います。2.0ではsslとかunixドメイン..]
ψ さかい [そうなると、DRbAuthじゃ認証するのが遅すぎる事になりますよね。 やっぱり認証に関しても、下のレイヤでやることに..]
ψ 咳 [$SAFE=1ならだいぶよくなりそうですが、DRbAuthをだめかなあ。 うーん。検証しなきゃならないなあ。]
2003-09-02
λ. 昼食
「角で」で。
λ. 東方妖々夢
久しぶりにプレイ。魔理沙でようやくクリア。
これでノーマルは一応全員ノーコンテニュークリアしたわけだし、しばらく妖々夢は封印の予定。
……と思ったが、その前にExtraを一回だけプレイ。むずい。でも、最初のプレイでボスまでたどり着けたことを考えると、やっぱ紅魔郷よりはだいぶ簡単かな。
2004-09-02
λ. Re: Functor と Monad
圏論の普通の定義ではモナドは関手と二つの自然変換からなるので、MonadならばFunctorだというのはその通りです。ちなみに、[haskell-jp:51]によれば、「Goferで型クラスが導入されたとき」には「Monad になるためには、Functor でなければいけなかった」そうです。
で、両者の実装を変える理由ですが、やはり効率があるんじゃないでしょうか。例えばリストの場合、fmap f [a,b,c] が [f a, f b, f c] を計算すれば良いのに対して、liftM f [a,b,c] は [f a] ++ [f b] ++ [f c] を計算するので、多少効率が悪そうですし。
λ. "Graph Rewriting Semantics for Functional Programming Language", Marko van Eekelen, Sjaak Smetsers, Rinus Plasmeijer
Concurrent Clean とかの意味論で使われてる項グラフ書き換え系(TGRS, Term Graph Rewriting System)の説明と、その上での Uniqueness Typing の定式化。項書き換え系(TRS, Term Rewriting System)ではなく項グラフ書き換え系を用いるのは、共有を明示的に扱えて、関数型言語の実態に近いから。
そういえば、uniquenessの様な性質に関するpolymorphismのアイディアは"Quasi-Linear Types"にもあったな。
![[眉間に風穴の開いたモリゾー]](./images/20050902_0.jpg)
2012-09-02
λ. Omega test and beyond
ProofSummit2012 にて、Omega test and beyond という題での発表を行いました。内容は Coq の omega タクティック他で広く使われている Omega test という決定手続きの概要とその周辺の簡単な紹介です。Keynote使うのが初めてだったので、スライド作りにはちょっと苦戦してしまった。
関連
- ProofSummit2012 - Togetter
- 昨年のProofSummit2011での発表(LT)「自動定理証明の紹介」
