日々の流転

λ. 規模が小さくてソースの読みやすいオープンソースのコンパイラってどっかに転がってないかな。

λ. 私の景気対策

What My Home Page is. の 2002/05/06(mon)02:38:01 の「私の景気対策」が素晴らしい。

Internet Archive

λ. 夢

今のうちに密かに卒論を書いておくという夢を見た。よくわからないテーマだった。

λ. monomorphismかつepimorphismはisomorphismの十分条件じゃない

monomorphismかつepimorphismはisomorphismの十分条件じゃないって事は、monomorphismであってもretractionが存在するとは限らないし、epimorphismであってもsectionが存在するとは限らないって事か。そうか、そうだよな……

λ. Java

少し勉強をはじめた。誤算があって、思ったよりも早くtomcatのソース読みの順番が回ってきそうなので。

λ. Parametric-types for Java

そういえば、以前に石原君に「Javaはstatic-typedなのにparametric-typeが無いのが嫌なんだよねぇ」と言ったら、genericityってのが入るらしいと教えてもらったのだった。なので、少し探してみたら、GJ - A Generic Java Language Extension というのを見つけた。これこれ、こーゆーのが欲しかったのよ。

それと、Parameterized Types for Java という論文を見つけた。

λ. σ-calculus

それから、Javaとは関係ないが、オブジェクト指向言語を形式化した object calculus(σ-calculusとも呼ぶらしい)という計算モデルがあるらしい。これまで、オブジェクト指向って、どうも理論的な根拠が薄弱で、宗教的というか、経験論的というか、要する胡散臭いと思ってたんだけど、ちゃんとした理屈もあるんじゃないの。

Sigma Calculus Interpreter

σ-calculusのインタプリタ。わりと面白そう。

λ. おしゃれ泥棒 (How to Steal a Million)

を見た。

λ. お勉強ノート

Atsushi Yamaguchi 氏のカテゴリー論のまとめ等がある。

λ. Rubyのこんな所は今更変えられないよねぇのこーなー

去年の11/17に書いたけど、僕も文字列の結合は「+」よりは「*」が自然だと思う。というか、むしろ繰り返しを「**」で表現したいというのが本音だけど。

λ. 借りた本

『ていうか 経済って難しいじゃないですか』

中尊寺ゆつこ[著]

『最後の特派員』

ダニエル・スティール (Daniel Steel) [著]

λ. rubyでmontague文法?

「現在取り組んでいる課題はmontague文法をRubyで表現すること」と書いてあるのをみつけて、その後どうなったのかが気になった。モンタギュー文法についてのページも興味深い。

λ. "Types for Verification"

ワークショップの"Types for Verification"一日目。5時起き。7時半羽田発8時半伊丹。園田駅で反対側の出口に出てしまったりもしたけれど、なんとか始まる前に着くことが出来た。それはそうと、関西ではスイカもパスネットもバスカードも使えないのか……なんかほんと遠くにきたって感じだ。

λ. Per Martin-Löf (Stockholm University, on sabbatical at Sato-Lab, Kyoto U.) "100 years of Zermelo's axiom of choice: what was the problem with it?"

An analysis of Zermelo's axiom of choice in constructive type theory reveals that the problem with it is not the existence of the choice function but the extensionality of it, which is not visible in an extensional framework where all functions are by definition extensional.

"Intuitionistic Type Theory"にも選択公理の話は少しは出ていたはずなのだけど、すっかり忘れている私。まずいなー。(追記予定)

後で聞いた話によると、この話は3月に三田で話した内容とほぼ同じだとか(Proof Theory and its Applicationsに関する合同セミナーかな)。

【追記】 http://comjnl.oxfordjournals.org/cgi/reprint/49/3/345も参照。というか、後で読む。

λ. Masahiko Sato (佐藤 雅彦) (Kyoto University) "A simple theory of expressions"

We propose a framework called Natural Framework, which is used to present mathematics in a formal and convenient way. We are particularly interested in formalizing not only ordinary mathematics but also metamathematics. In this talk, we present a simple theory of expressions which we use as the underlying framework for Natural Framework.

例のCALの内部で使った表現なのかな。どの辺りがうれしいのかいまいちよく分からなかった。(追記予定)

λ. Peter Dybjer (Chalmers University of Technology, visiting AIST CVS) "Martin-LöF type theory and the logic of functional programs"

Martin-Löf type theory is a foundational framework for constructive mathematics and computer programming which is based on the Curry-Howard interpretation of propositions as types. This interpretation can be extended to an interpretation of Heyting arithmetic can in Martin-Löf type theory. In the opposite direction we have the interpretation of Martin-Löf type theory in a first-order theory of combinators given by Aczel 1974. This interpretation is closely related to the informal meaning explanations underlying Martin-Löf type theory.

In this talk I will review Aczel's interpretation and discuss its relevance for the CoVer project (Combining Verification Methods in Software Developement). The goal of this project is to build a tool where functional programs can be verified by a combination of testing and interactive and automatic theorem proving. The functional programs are written in Haskell and thus the underlying logic need to contain inference rules for reasoning about general recursive and lazy programs, and I will discuss some possible approaches.

Coverプロジェクトの一部であるAgda/Alfaで用いるロジックの話。(追記予定)

λ. John Hughes (Chalmers University of Technology, visiting AIST CVS) "Random Testing with QuickCheck"

One important use of formal specifications is in software testing: specifications can be used both as test oracles, and also for test case selection. The latter may require manual analysis of the specification, though, making this step relatively costly and indirect.

In this talk I will describe a tool we have developed, which provides a restricted (but surprisingly powerful) formal specification language in which specifications can be interpreted directly as test suites. The key idea is to interpret universal quantification in properties as random test case generation. The tool works well in practice, and the ideas have been used to test functional, imperative, and concurrent code. The original implementation is now distributed along with the standard Haskell compilers, and the ideas have been ported to (at least) ML, Scheme, Erlang, Python, and Mercury.

QuickCheckの紹介。 QuickCheckのアイディア自体は非常に単純。QuickCheckはテストのためのフレームワークなのだけど、個々のテストデータはユーザが記述するのではなく、システムがランダムに自動生成する。そして、ユーザによって記述された性質が、それらのランダムに生成されたテストデータに対して満たされているかをチェックする。もちろん、実際には色々な問題があるのだけど、それらはHaskellらしい方法で解決されてる。(追記予定)

Erlang, C. Scheme, Common Lisp, Python, Mercury, ML, ... に移植されているそうだ。Pythonに負けるのは癪なのでRubyにも移植しよう。

それはそうとプレゼンがとても上手だった。私もこんな発表が出来るようになりたいものだ。(追記予定)

λ. Yoshiki Kinoshita (AIST Research Center for Verification and Semantics) "Is modal mu calculus enough for verifying reactive systems?"

(追記予定)

λ. WWW2005　2日目

今日は少し寒いな。朝食は近くのサンエトワールというところでパンを食べた。比較的美味しかったが、かかっている音楽が微妙っぽかった。

で、今日のしょっぱなは Tim Berners-Lee の基調講演「Web for real people」。彼が話すのを直接見るのは初めてなのだけど、想像してたよりもずっと面白い人だった。 ところで、会場で黒子のかっこをした人*1を見かけたのだけど、その頭の後ろにCSSの書かれた紙が張ってあって面白かった。いわく、

@media real{
  kuroko{
    display: none;
  }
}

お次はCan semantic web be made to flourish? というパネルセッションにお手伝いに入った。神崎さんを目撃。

参考

• WWW2005パネル・ディスカッション (The Web KANZAKI)

お弁当の配布を手伝って、それからお弁当を食べる。その後 Yuji Inoue 氏の基調講演を訊いて、それから「Web Application Design」へ。

最後に、「Foundations And Future Directions of Web Services」。このトラックでは、Choreographyに少し興味を持った。なんでも formally based on π-calculus らしいので。

その後はポスターレセプション。チケットの引き換えが大変だった。ポスターは結構面白いのがあった。論文をそのまま張ってだけというのもあって少し面食らったけど。発想が面白かったのは「Detecting of Phishing Webpages based on Visual Similarity」。タイトル見ただけで内容がわかっていいね。ポスターが面白かったのは「Does learning how to read Japanese have to be so difficult, and can the Web help!」かな。それから「Soundness Proof of Z Semantics of OWL Using Institution」なんて濃いポスターもあった(こんな濃ゆいポスターを見るとは思わなかった)。あと、PageRank系のポスターも結構あったな。

λ. Types for Verification から一年

そういえば、去年の今頃(2004-05-11,2004-05-12)は Types for Verification というワークショップに参加していたが、最近 Agda を触るようになって、そのときに聴いた Martin-Löf や Peter Dybjer の話への理解がようやく深まってきた気がする。

λ. Game Semantics. Samson Abramsky and Guy McCusker.

• <URL:http://www.cogs.susx.ac.uk/users/guym/papers.html>
• <URL:http://citeseer.ist.psu.edu/abramsky99game.html>
• <URL:http://jp.citeulike.org/article/625286>

だいぶ前にsyd_sydさんのところで紹介されていたのでざっと読んだ。後半面倒くさくなって真面目に追ってないが、雰囲気は分かったし面白かった。ただ、形式化があまり直観的でないと感じた。もっと分かり易い形式化が可能なのではないかという気がしてならない。あと、big-stepの操作的意味論は存在は知ってたけど初めて見たよ。

λ. 久しぶりに向井先生と雑談

久しぶりに向井先生と雑談してきた。 以下メモ。

• TeX
  • Powerdot
  • \begin{proof}\end{proof}で囲むと最後にQEDの四角がつく
  • 集合の内包表記では \mid を
  • \align
• 斜体(skew field)
  • どの辺りが skew なんだろう
• イデアル(ideal)
  • 連続関数全体のなす環　連続関数環
    • 元の空間がコンパクト(?)だと、連続関数環から元の空間が復元できる?
    • 連続関数環の極大イデアルが元の空間の点を表す?
    • ある点で0にするような多項式の全体は極大イデアル
    • 極大でないイデアルは想像上の(fictionalな)点を表してると考える
  • forcing と generics
  • idealとfilterが双対
  • 昔はこういう話は良く分からなかったけど、CABAの極大フィルタ(ultra filter)が集合の点に対応する話とかを知った今は、だいぶイメージ出来るようになった気がする。
    • Stoneは凄い
      • 「1930年代に M.H. Stone はブール代数の表現定理を証明し，ブール代数が豊かな数学的内容を持つことを示した．当時まだ一般的概念としては存在しなかった可換環の素イデアルの空間(スペクトル)とカテゴリーにおけるアジョイントの概念が実質的に用いられているという，時代に先駆けた結果である．」(田中俊一『位相と論理』より引用)
• プロセス代数
  • 関係を保存する代数という意味で「代数」と呼んでいるのか?　例えば自然数と不等号の場合 a≦b ならば a+c ≦ b+c 成り立つが、同様のことがプロセスと遷移関係についても言えるので。
• クリフォード代数 <URL:http://en.wikipedia.org/wiki/Clifford_algebra>
• 検証
  • 様相論理での program = modal operator という見方
  • ホーア論理はもう古いと、ホーアさん本人が言ってたとか
• indexed-category, fibration, Grothendieck construction
• Higher Operads, Higher Categories. <URL:http://www.maths.gla.ac.uk/~tl/book.html>
• 『入門Haskell—はじめて学ぶ関数型言語』
  
• 『数学基礎論講義—不完全性定理とその発展』
  

λ. E*TRADEのキャンペーン

E*TRADEがフレッシュマンキャンペーンと称して、抽選でAmazonギフト券が3,000円当たるというのをやっていたので、久しぶりに取引した上で申し込んでみた。

ついでに気付いたのだが、E*TRADEはウィルコムストアの優待販売なんてのもやっていた。先日6,800円で買ったAX420Nは2,800円で売ってる……不覚。

λ. 大分五日目

今日は私たちの教育担当の方がいろいろと連れて行ってくれることに。 とても楽しみ。

お昼に「天まで上がれ」というところでセキサバ・セキアジを食べる。 活作りだったので新鮮で、とても美味しかった。

その後、臼井石仏を観光。

最後に、富士見水産でお土産のお魚を検討。結局買わなかったけど。

寮に帰ってから、会社のプールで泳いできた。久しぶりなので軽く1kmくらい泳いだだけなのだけど、明日(大胸筋と上腕三頭筋あたりが)筋肉痛になりそうな感じ。体がなまりきってる。遠山さんと同じ?

λ. 関連

• <URL:http://mixi.jp/view_diary.pl?id=431288458&owner_id=1577475>

λ. Chapter 9 の練習問題6

Φ: A→B をフレーム準同型として、その右随伴 Ψ: B→A を Ψ(b) = ⋁{a∈A | Φ(a)≦b} で定義する。

このとき、Φ(a)≦b ⇔ a≦Ψ(b) が成り立つ(つまり圏論の意味での随伴になっている)。

• Φ(a)≦b ならば a ≦ ⋁{a∈A | Φ(a)≦b} = Ψ(b)
• a≦Ψ(b) ならば Φ(a) ≦ Φ(Ψ(b)) = Φ(⋁{a∈A | Φ(a)≦b}) ≦ ⋁{Φ(a) | a∈A, Φ(a)≦b} ≦ b

このとき、Ψは任意のmeetを保存する。 なぜなら a≦Ψ(⋀S) ⇔ Φ(a)≦⋀S ⇔ Φ(a)≦b for all b∈S ⇔ a≦Ψ(b) for all b∈S ⇔ a≦⋀{Ψb | b∈S} であり、 ここで a は任意なので Ψ(⋀S) = ⋀{Ψb | b∈S} を得られるので。

ただし、Ψはjoinを保存するとは限らない。 例えば、A={false < α < true}, B={false < true} として、Φ(α)=false とおくと、Ψ(false) = ⋁{a | Φ(a)≦false} = false∨α = α ≠ false となる。false すなわち empty join が保存されていない。 (binary join についての例も後で考える)

λ. サーバ障害

ここしばらくは問題なかったので安心してたが、tomのサーバがまたトラブルを起こしたらしい。復旧作業にあたった方々は本当にお疲れ様&ありがとうございました。しかし、RAID1を組んでるディスクが二つ同時にお亡くなりになるなんて、本当にあるんだねぇ。おそろしや、おそろしや……

というわけで(?)、トラブルのせいで一時 404 Not Found になっていたけど、別にtomを卒業したわけじゃないっす。

関連

• chikoさんのmixi日記
• torryさんのmixi日記

λ. Hints for Computer System Design by Butler W. Lampson

システム・ソフトウェアの講義資料にあったので読んだ。 わかっちゃいるけど、なかなかこの通りにはいかないんだよなぁ。 あと、具体例としてあがっているシステムの話が面白い。

λ. 第四十回圏論勉強会

今日は圏論勉強会。 『The Haskell Programmer's Guide to the IO Monad ― Don't Panic』を読む四回目で、Section 6.3 “An alternative definition of the monad”から最後まで。 モナドの代替的な定義としての Kleisli Triple と Haskellの定義での定義、それらの等しさ。IOモナドの説明。 次回から何をやるかは未定。

母の日ということで、帰りにシュークリームを買って帰った。 クッキーっぽいやつと、五月限定のさくらんぼのやつ。

関連

• 2008-05-11 - Countercode

λ. 新ディスプレイ

ディスプレイが壊れたので、新しいディスプレイを買ってみた。 ディスプレイのことなど何も分からないので、適当に安めだったiiyamaの20インチのやつに。¥24,800

これまでのに比べると画面が広くて綺麗だなぁ。弾幕が映える(ぉ