日々の流転

λ. あけましておめでとうございます。

本年も是非よろしくお願いします。

最近更新が滞ってましたが、ぼちぼち再開してきます。

λ. 初詣

成田山, 金龍山浅草寺, 柴又帝釈天へツアーで行ってきた。えっ? 全部お寺なのに何が初詣だって? ノン、ノン、ノン、モナミ。成田山には巫女さんがいたのですよ。どう見てもバイトの人とはいえ、巫女さんがいるのだから、初詣で全然問題ないのですよ。ええ!! (以下略)

……とりあえず神仏習合バンザイって事で。

λ. newtype/datatype (was efficiency)

そうか、単純に pointed CPO だけじゃだめなのか。なるほどねぇ。Haskellのデータ型の意味についてちょっとナイーブに考えすぎてたな。それから、「undefined :: a->b」と「λx.undefined :: a->b」が異なっているという話で、Topology via Logic に以下のように書かれていたのを思い出した。

However, we get something more interesting if we try to solve

  D = [D→D]⊥

This has been studied by Abramsky [87,90], and also, following him, by Ong [88], in connection with the lazy λ-calculus. The effect of the lifting is to make a distinction between ⊥, a completely divergent object, and λx.⊥, which is known to be a function but which diverges whenever it is applied to an argument.
Computationally, this corresponds to not trying to evaluate a function beyond the λ until application time, and is the way things are generally done in practice.

---

• S.ABRAMSKY
  • [87] Domain Theory and the Logic of Observable Properties, PhD Thesis, Queen Mary College, University of London, 1987.
  • [90] "A domain equation for bisimulation", Information and Computation, 1990.
• C-H L. ONG
  • [88] The Lazy λ-Calculus: An Investigation into the Foundations of Functional Programming, PhD Thesis, Imperial College, University of London, 1988.

ちょっとこれらの論文を読んでみたくなった。『A domain equation for bisimulation』はPSファイルが見つかったのでまずこれを読んでみよっかな。

関連エントリ

• newtypeはHaskellの仕様に不要では?

λ. 小泉首相の靖国神社参拝

少し前に『「いつ参拝しても批判されるなら、公約通りに断行した方が潔い」(首相周辺)との判断に傾きつつある』という記事を読んで、今年は終戦記念日に参拝してくれるんだろうと期待してたので、元旦の参拝にはビックリした。元旦に参拝するのも悪くはないと思うけど、年一回参拝という公約を考えると、今年も終戦記念日には参拝しないんだろうなぁ。はぁ(ため息)