日々の流転

λ. 明日は、「経済理論演習」と「記号処理プログラミング」の試験。「記号処理プログラミング」の方は簡単なリファレンスみないなプリントを持ち込みできるんで、多分大丈夫。問題は「経済理論演習」なんだよな。LS/IM分析とかわかんな杉。やばいよー

λ. 無理数

なるほど、ruby-math見てみます。でも、コーシー列とかグレブナー基底とかって、例によって名前だけしか知らないなり。

λ. マックロソフトに補助金を

あの企業が独占的企業であることは多くの人が同意するだろう。で、独占的行為の問題の一つに、資源配分の観点から、それによって財の供給が過小に抑えられるってのがある。あれはソフトウェアだから、量の供給が過小だって事は無いんだけど、品質考えると思いっきり過小だよな〜とか思うんだ。バグフィックス版みたいなので金取ったりしてるしね。

ところで、独占的行為による過小生産の解決法の一つに、(マイナスの課税である)生産補助金を与えるというのがある。(他には価格規制とかかな。まあ、根本的に独占自体を解決すんのが筋かもしんないけどね。)

どうだろう。マックロソフトに補助金を出せと主張する人はいないのだろうか?

λ. Rouge(る〜じゅ)

さりげなく公開。

λ. 落ち込んでます。こんな事とりあえず今は忘れて、今すべき事に集中すべきだとは思うのだけど、なかなか手につかない。

その不器用さが腹立たしい。

λ. 井関先生の講演を見た。Orgel's Monologue III (2002-06-26)より。

λ. あるn(≧2)点を囲むような円があるとする。このとき、円をずらすことで、それらの点を全て囲んで、かつその内の2点が円周上にくるようにすることが出来る

反応が遅くなってしまって申し訳ない*1のですが、例の Circle and Points の問題で使った「あるn(≧2)点を囲むような円があるとする。このとき、円をずらすことで、それらの点を全て囲んで、かつその内の2点が円周上にくるようにすることが出来る」という性質について、sheepman さんから証明を頂きました。

なるほど、確かにそれで言えますね。シンプルで分りやすい証明だと思います。

それから、私はこの手の証明について良く知らないので、「数学の証明っぽくするには、点 A と円周との距離を d(A, S¹) = inf{ |A - x| | x ∈ S¹} で定義するだとか、円周は有界閉集合だから、inf を attain する点が存在するとか言えばいい」という点も「なるほど」と思いました。Sの肩に乗っている「1」は円の半径の1かな

λ. カタツムリを用いた高速データ転送について

面白い。Letter from Yochomachi より。

λ. Towards a monadic semantics of quantum computation, Thorsten Altenkirch

というのをたまたま読んだ。probabilistic computation をモナドで扱うのは自然な発想で理解できるのだけど、そこから先がいまいちよく分らなかった。量子計算について良く知らないんだから当たり前だが。

λ. 内定

先日某社から内々定の連絡がありました。これで就職活動は一応おしまいです。 お世話になった方々、応援していただいた方々、本当にありがとうございました。

λ. 『ふつうのHaskellプログラミング』読書会

I attended RHG*1 reading club and we read section 5, 6, 7 and 8.1〜8.3 of “ふつうのHaskellプログラミング”. We studied lazy evaluation, basic values, basic syntax, higher-order functions and anonymous functions. We had read to page 208.

英語の勉強にリーダーズ・ダイジェストという雑誌を教えてもらった。

BTW: ICFP Programming Contest had began and the subject seems interesting. I regret that I don't have time in this weekend.

λ. 『すべての日本人に感じてほしい魂の昭和史』 福田和也

を読んだ。 いい本だ。 中学生か高校生の時に読んでいたかったな。

Quotation

p.14

だから、歴史のもっとも大事なことは、共感ということだ。自分にとって関係のない出来事や固有名詞を覚えるということではない。あるいは他人ごととして、裁くことでもない。自分につながる、今、ここで生きている自分にとって他人事ではない事柄として、過去を振り返り、その実感のなかで、前の世代との絆を確認すること。そして、その絆のなかで、君たちの先人が、何をのぞみ、何をこころみ、そして成功したり、失敗したということを理解しようとこころみてほしい。そうすれば、君たちが生きている現代という時間が、けして薄っぺらなものでないことがわかるだろう。

p.97

絶対にとりかえしのつかないことの積み重ねが「歴史」ということなんだから。そして君たちは、みんな、その積み重ねの結果としてここにいる。

λ. ICFP Programming Contest 2007 (3)

DNA→RNA の変換が遅くて話にならないので、高速化しようとごにょごにょしてたら、バグってやる気をなくす。

(中略)

他の方がRNAを実行する部分を完成させていたので、ふと遅いままのDNA→RNAの変換機を例のprefixに対して適用してみたら、予想に反してすぐに終わった。こんなことならもっと早く試していればよかった。結果のRNAを実行してもらったら(略)。

ようやく入り口という感じだが、ちょっとやる気が出てきたし、方針も少し見えてきた。 しかし、もう夜。明日は会社だし、もう無理か。 無念。

それにしても、やはり私にはプログラミングの才能は無いんだな。

λ. 『それがぼくには楽しかったから』 by Linus Torvalds and David Diamond

非常に今更なのだが、友人に薦められて『それがぼくには楽しかったから』読んだ。オープンソースの勃興期の非常にワクワクした雰囲気を思い出して懐かしくなった。 この日記を検索したら、この本は2002-10-19に借りて読んでいるはずなのだけど、読んだのを全然覚えてないや。

λ. “Generic Programming with Adjunctions” by Ralf Hinze

2010-04-24 の Functional Programming Meeting 2010で紹介されていたもの。

Ψ : Nat(C(-,A), C(F-,A)) が与えらたときに、x ∘ in = Ψ x を満たす一意な x = (|Ψ|)_Id : μF→A が、Mendler-style fold (Mendler-style catamorphism) 。

これを拡張し、随伴 L ⊣ R と Ψ : Nat(C(L-,A), C(L(F-),A)) が与えられたときに、x ∘ L(in) = Ψx を満たす一意な x = (|Ψ|)_L : L(μF) → A を定義し、これを Adjoint fold と呼んでいる。 これは、随伴を Φ: C(LA, B) → D(A, RB) とすると、(|Ψ|)_L = Φ^-1 (|Φ ∘ Ψ ∘ Φ^-1 |)_Id という風に通常の Mendler-style fold に還元できる。

Adjoint fold の良いところは、引数にμFが直接現れずにコンテキストの中に現れているような再帰関数でも、そのコンテキストを表す関手が右随伴を持てば扱えること。 例えば、

append :: ([a], [a]) → [a]
append ([], ys) = ys
append (x:xs, ys) = x : (append xs ys)

を考えると、F(X) = Maybe (A, X) とおいて μF ≅ [a] で、L(X) = (X, μF) は右随伴 R(X) = (μF ⇒ X) を持つので、

Ψ : ∀X. (LX → μF) → (LFx → μF)
Ψ f (Nothing, ys) = ys
Ψ f (Just (a,x), ys) = a : f (x,ys)

append : (μF,μF) → μF
append = (|Ψ|)_L

という風に、Adjoint fold の形で書ける。

Fusion for adjoint folds から Type fusion へのつながりがイマイチよく分からなかった。 Fusion for adjoint folds が α(|Ψ|)_L = (|Ψ'|)_L' ⇐ α∘Ψ = Ψ'∘α なのに対して、 Type fusion が L(μF) ≅ μG ⇐ L∘F ≅ G∘L と、 νF ≅ R(νG) ⇐ F∘R ≅ R∘G で、 同じ形になっているのは分かるし、後者の証明に前者が使えるのもわかるのだけど、形の上での類似性だけで本質的な関係が何かあったりしないのだろうか?

Type fusion の証明は、以下で十分なのではないかと思った。 swap : L∘F ≅ G∘L が与えれているとき、ψ: GB→B に対して、Ψ ∈ Nat(C(L-,B), C(LF-, B)) を、Ψ(h) = ψ ∘ Gh ∘ swap とおくと、(|Ψ|)_L : LμF → B は h ∘ Lin_F = ψ ∘ Gh ∘ swap すなわち h ∘ Lin_F ∘ swap^-1 = ψ ∘ Gh を満たす一意な射なので、Lin_F ∘ swap^-1 は G の initial algebra 。

Type fusion を利用してのメモ化の導出も面白かった。

参考

• Categorical programming with inductive and coinductive types - ヒビルテ(2004-06-29)