日々の流転

λ. A Categorical Programming Language

A Categorical Programming Language を眺めてみる。萩野せんせの Ph.D. thesis

λ. W3Cオープンレクチャー

ほんとは昨日だったのに、今日だと思ってました。お馬鹿です。

λ. 『最低!!』, 二宮ひかる

を読んだ。

λ. 安田さんのサーベイページ

安田さんのサーベイページに色々な人の日記からリンクされているのを見て、少し驚く。

λ. 「世界はRESTfulなんかじゃない。そしてそれ故に、REST萌え。(意味不明)」

ひょっとして「キノの旅」?、とか少し驚く。

λ. 同姓同名

同姓同名の方が未踏に採択されて驚いた話を書いたら、忘れた頃に、本人からツッコミをもらってしまって、少し驚く。(ツッコミのURL修正しました。ZnZさんの指摘に感謝)

未踏は、適当なネタがあれば応募してみたいところ。

λ. 『ニニンがシノブ伝 2』, 古賀 亮一

を読んだ。

λ. 聞かなければ良かった

聞かなければ良かった……

λ. "Categories for Everybody", Steve Awodey

圏論の入門。William Lawvere and Steve Schanuel, "Conceptual Mathematics: A First Introduction to Categories" を読み終わったぐらいの人がいたら薦めてみようか。一応、米田の補題とかAdjointとかMonadも扱ってるし。

ドラフト

【2006-09-29追記】本として出版され、PDFでの公開は停止してしまったようだ。出版は目出度いがWebで読めなくなるのは結構残念。

λ. 借りた本

『クリス・クロス—混沌の魔王』

高畑 京一郎 [著], きがわ琳 [イラスト]

『次元の秘密—自然単位系からDプレーンまで』

竹内 薫 [著]

『デッド・ゾーン (上)』

スティーヴン キング (Stephen King) [著], 吉野 美恵子 [訳]

『第61魔法分隊』

伊都 工平 [著], 水上カオリ [イラスト]

小説すばる 2003年12月号

-

λ. The “Curry view” and the “Church view” of polymorphic λ-calculus

the “Curry view” of polymorphic λ-calculus

Pure terms of the λ-calculus are assigned type expressions involving universal quantifiers.

the “Church view” of polymorphic λ-calculus

Terms and types are defined simultaneously to produce typed term.

という二つの見方があるんだそうな。 Type reconstruction in finite-rank fragments of the polymorphic λ-calculus. より。

λ. 初給料日

というわけで、初給料。 さて、何に使うか。

λ. 2/3 SFP と algebraicity

Topology via Logic では 2/3 SFP を以下のように定義している。

For each finite set S of compact points there is another such M (a complete set of upper bounds for S) such that

• each m∈M is an upper bound for S, and
• if m´ is any compact upper bound for S, then m´ ⊒ m for some m∈M.

この定義はm´はcompactであることを要求しているが、対象となる半順序集合が algebraic dcpo であれば、この条件は外せる。

証明

m´ を S の upper bound とする。 対象となる半順序集合 P が algebraic dcpo なので、T = {c∈KP | c⊑m´} とおいて、 ∀x∈S. x ⊑ m´ = ⨆^↑T 。 xのコンパクト性より、 ∀x∈S. ∃c_x∈T. x ⊑ c_x 。

C = {c_x | x∈S} とおくと、CはTの有限部分集合なので、Cのupper bound c∈T が存在する。

1. c∈Tなので m´ ⊒ c 。
2. 一方、c は Sの compact upper bound なので、2/3 SFP を適用して、ある m∈M について c ⊒ m 。

よって、m´ ⊒ c ⊒ m 。

λ. 連休前に

連休前に色々片付けたかったが、あんまし片付かなかった。

λ. 『本物のプログラマはHaskellを使う』読者の集い 開催案内

[haskell-jp:309] 『本物のプログラマはHaskellを使う』読者の集い 開催案内 より。

5/4（月、祝）に、ITPro連載『本物のプログラマはHaskellを使う』筆者のshelarcyさん（白石さん）を囲んで、掲題のような集いをやろうと計画してます。〜中略〜 参加ご希望の方は、下記サイトよりエントリーをお願います。詳細もこちらのサイトに記載しています。

• <URL:http://atnd.org/events/580>

一応、連載記事を中心にshelarcyさんに紹介をお願いしようかと思っていますが、何か聞きたいこと・ご意見・ご要望などあれば是非教えてください。