日々の流転

λ. Representations of First order function types as terminal coalgebras, Thorsten Altenkirch

たまたま見かけて読んだのだけど、面白かった。α→βという関数型は、αが帰納的(inductive)な型であれば、余帰納的(coinductive)な型として表現できるという話。自然数やリストの場合までは考えたことがあったが、2分木のような線形でない型の場合も nested datatypes を使えば表現出来るというのは気づかなかったなぁ。

例:

自然数

(μX.1+X)→B ≅ νX.B×X

Aのリスト

(μX.1+A×X)→B ≅ νX.B×(A→X)

Aの2分木

(μX.A+X×X)→B ≅ (νF.ΛX.(A→X)×F(F(X)))(B)

証明は、ちょっと良く理解出来ていない所もある。セッティングは bicartesian で ω^op-limit と ω-colimit が存在する圏(cartesian-closedである必要はない)。そのままでは構成的関数からなる ω-Set のような圏へ一般化することは出来ないらしい……

関連エントリ

• [agda] ストリームの表現

λ. 雪

雪だ雪だー

写真

λ. 情報理論勉強会＠古川研

テキストは 『情報理論の基礎 — 情報と学習の直観的理解のために —』, 村田 昇 。難い。

λ. ∀A: N→*. A(zero) → (∀n: N. A(n)→A(succ(n))) → ∀n: N. A(n)

N,zero,succをそれぞれ

• N = λX: *. X→(X→X)→X
• zero = λX: *. λz: X. λs: X→X. z
• succ = λn: N. (λX: *. λz: X. λs: X→X. s (n X z s))

とする。Calculus of Constructions (CC) では、この定義からは ∀A: N→*. A(zero) → (∀n: N. A(n)→A(succ(n))) → ∀n: N. A(n) *1 という型の関数を導出できないそうだ。そこで素朴な疑問なのだが、N,zero,succ の定義を適切に変更すれば、CCでこれを導出出来るのだろうか?

ちなみに、Haskellで無理やり書くとこんな感じか。

data Z = Z
newtype S n = S n
 
class N n where
    ind :: t Z -> (forall m. N m => t m -> t (S m)) -> t n
 
instance N Z where
    ind z _ = z
 
instance N n => N (S n) where
    ind z s = s (ind z s)

これと同様の方法を使って簡単な行列ライブラリをHaskellで書いてみた(2005-04-06)。

λ. Hylomorphisms

関手Tの始代数 (μT,in) が存在して、 (μT,in^-1) が終余代数 (νT,out) になっているとする。 すると、T余代数 (A,ψ) から得られる関数 unfold(ψ):A→νT と、 T代数 (B,φ) から得られる関数 fold(φ):μT→B を合成して、 fold(φ) ∘ unfold(ψ): A→B という関数を定義できる。 これを hylomorphism と呼び、 しばしば 〚φ,ψ〛_T と書かれる。

Program Calculation Properties of Continuous Algebras, Maarten M Fokkinga and Erik Meijer には、hylo の語源について次のように書いてあった。

The prefix hylo- comes from the Greek ύλη meaning “matter”, after the Aristotelian philosophy that form and matter(= data) are one. (In conjuction with -morphism the vowel η changes into ο .)

ちなみに、日本語では、ύλη は「質料」と訳されているようだ。「質料」「形相」等で検索するとアリストテレス哲学に関する記述が沢山見つかる。

[2005-03-27 追記] WikiPedia: hylomorphism には以下のように書いてあった。

Hylomorphism (Greek υλο- hylo-, "wood, matter" + -morphism < Greek -μορφη, morph, "form") is a philosophy that highlights the significance of matter in the structure of being, regarding matter as important (or even more so) as form.

Hylomorphism served as a useful tool in medieval philosophy from (at least) Avicebron to (at least) Thomas Aquinas.

λ. Hylomorphismと不動点コンビネータ

以下のように図式を張り合わせると、この関数 fold(φ) ∘ unfold(ψ): A→B は x = φ ∘ Tx ∘ ψ の解の一つであることがわかる。

一方、cartesian closed でかつ不動点コンビネータが存在するのなら、fix(λf. φ ∘ Ff ∘ ψ) *1 によって別の解を定義することが出来る。この二つは等しいか?

homsetがCPOでかつ合成が正格かつ連続で不動点コンビネータが最小不動点を返すならば、等しいことは簡単に言える。α,β,γを次のように定義する。

• α(f) = φ ∘ Tf ∘ in^-1
• β(f) = out^-1 ∘ Tf ∘ ψ
• γ(f) = φ ∘ Tf ∘ ψ

すると、

• fold(φ) = ∨_n<ω αⁿ(⊥_μT→B)
• unfold(ψ) = ∨_n<ω βⁿ(⊥_A→νT)
• fix(λf. φ ∘ Ff ∘ ψ) = ∨_n<ω γⁿ(⊥_A→B)

であり、帰納法によって αⁿ(⊥_μT→B) ∘ βⁿ(⊥_A→νT) = γⁿ(⊥_A→B) が証明でき、合成は連続なので fold(φ) ∘ unfold(ψ) = fix(λf. φ ∘ Ff ∘ ψ) が言える。

λ. Hylo Shift Law

自然変換 η: F→G に対して、 μη = fold_F(in_G ∘ η_μG): μF→μG と定義する。すると、fold_F(φ ∘ η_B) = fold_G(φ) ∘ μη が成り立つ。

同様に νη = unfold_G(η_νF ∘ out_F): νF→νG と定義すると、unfold_G(η_A ∘ ψ) = νη ∘ unfold_F(ψ) が成り立つ。

T∈{F,G} について (μT,in^-1)=(νT,out) ならば、μη=νη となるので、fold_F(φ ∘ η_B) ∘ unfold_F(ψ) = fold_G(φ) ∘ μη ∘ unfold_F(ψ) = fold_G(φ) ∘ νη ∘ unfold_F(ψ) = fold_G(φ) ∘ unfold_G(η_A ∘ ψ) が言える。

この等式 fold_F(φ ∘ η_B) ∘ unfold_F(ψ) = fold_G(φ) ∘ unfold_G(η_A ∘ ψ) によって、自然変換ηを移動させることが出来る。これを Hylo Shift Law と呼ぶ。

λ. Hylomorphismの三つ組み表現 (Hylomorphisms in triplet form)

Hylo Shift Law によって自然変換を自由に移すことが出来るので、fold_F(φ ∘ η_B) ∘ unfold_F(ψ) = fold_G(φ) ∘ unfold_G(η_A ∘ ψ) を φ: GB→B, η: F→G, ψ:A→FA の三つ組みによって 〚φ,η,ψ〛_G,F: A→B と表すことがある。

λ. 酸性雨定理 (Acid Rain Theorem)

パラメトリシティを仮定すると、

• C→μF ≅ C→(∀X.(FX→X)→X) ≅ ∀X.(FX→X)→(C→X)
• νF→C ≅ (∃X.(X→FX)×X)→C ≅ ∀X.(X→FX)→(X→C)

が成り立つのだが、 それぞれの右辺の型にパラメトリシティを適用することで以下を導ける。

Acid Rain : Catamorphism

∀g:∀X.(FX→X)→(C→X), φ:FA→A. fold(φ) ∘ (g_μF in_F) = g_A(φ)

Acid Rain : Anamorphism

∀h:∀X.(X→FX)→(X→C), φ:A→FA. (h_νF out_F) ∘ unfold(φ) = h_A(φ)

これらを酸性雨定理と呼ぶそうだ。

パラメトリシティを仮定すると色々な事が言えてとても楽しいのだけど、不動点コンビネータやseqの存在と相性が悪いという問題がある。

• パラメトリシティと不動点
• Free Theorems in the Presence of seq

λ. Cata-HyloFusion / Hylo-AnaFusion

τ:∀A.(FA→A)→(FA→A) にパラメトリシティを適用すると、 ∀A,φ:FA→A,B,ψ:FB→B,h:A→B. (h ∘ φ = ψ ∘ Fh) ⇒ (h ∘ τ_A(φ) = τ_B(ψ) ∘ Fh) が言える。ここで、fold(ψ) ∘ in = ψ ∘ F(fold(ψ)) なので、fold(ψ) ∘ τ_μF(in) = τ_B(ψ) ∘ F(fold(ψ)) 。 universality (cata-fusion) により、 fold(ψ) ∘ fold(τ_μF in) = fold(τ_B ψ) 。

同様に、σ:∀A.(A→FA)→(A→FA) にパラメトリシティを適用すると、 ∀A,φ:A→FA,B,ψ:B→FB,h:A→B. (Fh ∘ φ = ψ ∘ h) ⇒ (Fh ∘ σ_A(φ) = σ_B(ψ) ∘ h) が言える。 ここで、out ∘ unfold(φ) = F(unfold(φ)) ∘ φ なので、F(unfold(φ)) ∘ σ_A(φ) = σ_νF(out) ∘ unfold(φ)。 universality (ana-fusion) により、 unfold(σ_νF out) ∘ unfold(φ) = unfold(σ_A φ) 。

この二つを hylomorphism を使った形で表現すると、以下を得る。

Cata-HyloFusion

τ: ∀A.(FA→A)→FA→A ⇒ 〚φ,η₁,out_F〛_G,F ∘ 〚τ(in_F),η₂,ψ〛_F,H = 〚τ(φ ∘ η₁),η₂,ψ〛_F,H

Hylo-AnaFusion

σ: ∀A. (A→FA)→A→FA ⇒ 〚φ,η₁,σ(out_F)〛_G,F ∘ 〚in_F,η₂,ψ〛_F,H = 〚φ,η₁,σ(η₂ ∘ ψ)〛_G,F

……と、ここまで書いてきて気づいたのだけど、酸性雨定理から証明できるな。

λ. fold/build shortcut deforestation

パラメトリシティを仮定すると C→μF ≅ ∀X.(FX→X)→(C→X) が成り立つと上で書いた。 この同型は具体的には次の関数で表現される。

• build : (∀X.(FX→X)→(C→X)) → (C→μF)
  build g = g_μF in_F
• unbuild : (C→μF) → (∀X.(FX→X)→(C→X))
  unbuild f = ΛX. λφ. fold_X(φ) ∘ f

したがって、関数 f: C→μF を build g の形で書いておけば fold_X(φ) ∘ f = fold_X(φ) ∘ build g = (unbuild (build g))_X φ = g_X φ という書き換えが出来る。 これは酸性雨定理からも明らか。

リストの場合については、GHC等のHaskellコンパイラで最適化のために広く使われている。以下はGHC.Baseから引用。

foldr :: (a -> b -> b) -> b -> [a] -> b
foldr k z xs = go xs
             where
               go []     = z
               go (y:ys) = y `k` go ys
 
build :: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a]
build g = g (:) []
 
{-# RULES
"fold/build"    forall k z (g::forall b. (a->b->b) -> b -> b) . 
                foldr k z (build g) = g k z
#-}

λ. destroy/unfold shortcut deforestation

パラメトリシティを仮定すると νF→C ≅ ∀X.(X→FX)→(X→C) が成り立つと上で書いた。 この同型は具体的には次の関数で表現される。

• destroy : (∀X.(X→FX)→(X→C)) → (νF→C)
  destroy h = h_νF out_F
• undestroy : (νF→C) → (∀X.(X→FX)→(X→C))
  undestroy f = ΛX. λφ. f ∘ unfold_X(φ)

したがって、関数 f: νX→C を destroy h の形で書いておけば、 f ∘ unfold_X(φ) = destroy h ∘ unfold_X(φ) = (undestroy (destroy h))_X φ = h_X φ という書き換えが出来る。 これは酸性雨定理からも明らか。

リストの場合、destroy/unfoldr として知られているものになる。

unfoldr :: (b -> Maybe (a,b)) -> b -> [a]
unfoldr phi b =
  case phi b of
  Just (a,b') -> a : unfoldr phi b'
  Nothing     -> []
 
destroy :: (forall b. (b -> Maybe (a,b)) -> b -> c) -> [a] -> c
destroy g = g psi
  where psi []     = Nothing
        psi (a:as) = Just (a, as)

λ. インスタンスの列挙

[Haskell-cafe] Is it possible to print out types of instances in scope で知ったのだが、新しいGHCiの:infoコマンドは、型クラスの名前を与えるとインスタンスのリストを表示してくれるし、型の名前を与えると属しているクラスのリストを表示してくれる。Hugsには前からあったので、GHCiでも使えるようになって嬉しい。

λ. 構成的な関数からなる圏

よく出てくるのは

• PER
• ω-Set
• effective topos

くらいか。どれもあまり知らないや。

キーワード

• Kleene の実現可能性解釈 (realizability interpretation)
• 実現可能性宇宙 (realizability universe)
• 総合的領域理論 (Synthetic Domain Theory)

λ. Extensional PERs, Peter J. Freyd, P. Mulry, Giuseppe Rosolini, D. Scott

を読んだ。

λ. An introduction to fibrations, topos theory, the effective topos and modest sets, Wesley Phoa

メモ。

λ. 卒業発表 & 大学院入学手続き

ちょっとドキドキしてたのだけど、卒業発表のリストの中に自分の学籍番号を発見して一安心。なんとなくスクリーンショットを撮っておく。

それから、大学院の入学手続きを済ます。今更だけど、学費高いね。

λ. 代数的データ型の領域

data N = Z | S N の場合だとこんな感じのCPOか。

こいつのスコット位相は……書くの面倒なんで略。

で、このCPOにはtopはないけれど、こいつに無理やりtopを追加したらどうなる?

[2005-03-13追記] topが存在するとしたら、それは必然的に全てのパターンにマッチするはずだ。というのも、そのような点が存在したら、それはスコット位相における(空集合を除く)全ての開集合に含まれるはずだから。

そう考えると、擬データを用いた対話的関数プログラミングに関する研究では、未確定の擬データをbottomではなくむしろtopとして扱った方が自然だったのではないか、という気がしないでもない。単なる思い付きだけど。

λ. 風邪

ひいたっぽい。だるい。鼻水が出る。

λ. Scott is not Always Sober. By Peter T. Johnstone, in Continuous lattices, Lecture Notes in Mathematics, 871 (1981), pp. 282--283.

Scott topology は Sober だと何となく思ってたけど、違うのか。

λ. runghc

CVS版のGHCにはrunghcコマンドが含まれていて、runhugsコマンドと同じように使える。ちと起動が遅いけれど、Haskellのパッケージのセットアップ/インストール用のスクリプトをHaskell自身で書いたりするのに便利そうだ。

% cat hello.lhs
#!/usr/bin/env runghc
> main :: IO ()
> main = putStrLn "Hello World"
% ./hello.lhs
Hello World

λ. ANNOUNCE: GHC version 6.4

キタ━━━━(゜∀゜)━━━━ッ!!

過去の日記

• GADT (Generalized Algebraic Data Types)
  • ghc の新しい機能 Generalized Algebraic Data Types (GADT)
  • AVL木でGADTを試してみる
  • AVL木でGADTを試してみる (2)
• STM (Software Transaction Memory)
  • Composable memory transactions
• ライブラリ
  • GHC 6.4 のライブラリ
• その他
  • (GHCiの:infoコマンドで)インスタンスの列挙

明示的にforallで束縛した型変数を scoped type variable として使えるようになったのは、STモナドを使うときなんかに、地味に便利そうだ。これまでそういうときには不自然なコーディングを強いられてきたからなぁ。

λ. 独裁者占い

２０世紀の独裁者であなたを占います。

Good Wrappers For People Who Love Bad Know-Hows (2005-03-09) より。

で、結果。

さかいさんは イディ＝アミン です！

• あなたを独裁者にたとえると、ウガンダの独裁者イディ＝アミンです。ガタイのいいあなたは、国民の畏怖のシンボルとなります。肉料理は好きですか？しばらくすると「食人大統領」なんていうタイトルであなたの映画ができるかもしれません。っていうかできます。あなたは亡命先でひっそりと息を引き取るでしょう。
• さかいさんの開運一人称は、「あたち」です！
• そんなあなたの本日の運勢はこちらです！

アミン様かよ…… orz
でも、ボカサ様でなくてまだ良かったと喜ぶべきなのかしらん。

λ. スズバキってなんだかブルバキみたいだ

とふと思った。suzuvakiとBourbakiで綴りは違うけれど。

λ. 読むのに手頃なHaskellのコード

いきなりGHCのコードを読むのはどうかと思うけれど、標準ライブラリは結構勉強になると思います。

あと、個人的に勉強になったものですぐに思いつくのは、Lazy Depth-First Search and Linear Graph Algorithms in Haskell とか Typing Haskell in Haskell のコードとかかなぁ。

λ. 第２回東方最萌トーナメント

紅美鈴が優勝しちまったよ……びっくり。

λ. PrettyLambda

素敵だ。Misc Change Log (2004-12-05) より。

λ. メガネっ娘図鑑オールスターズ

• メガネっ娘図鑑オールスターズ 1st
• メガネっ娘図鑑オールスターズ 2nd

λ. インソムニア

白夜の雰囲気や不安感を盛り上げる演出は悪くないんだが、いかんせん先が読めるんだよなぁ。

λ. 花粉症?

このところ目が何か変な感じ。これって、ひょっとして、ひょっとすると、花粉症ってやつ?

λ. Parametricty and Mulry's Strong Dinaturality - A. Eppendahl

20061013#p03 を参照。

λ. Free Theorems in the Presence of seq - P. Johann and J. Voigtländer

スライド

The Impact of seq on Free Theorems-Based Program Transformations, Janis Voigtländer

seqが存在すると、関係を連続かつ正格なものに制限してもパラメトリシティは成り立たない。

foldr c n (build g) = g c n の反例

• g = seq, c = ⊥, n = 0
• g = λc n → seq n (c ⊥ ⊥), c = (:), n = ⊥

そこで、関係にさらに制約を加えることが考えられるが、 この論文では等式的な論理関係(equational logical relation)ではなく、不等号的な論理関係(inequational logical relation)にしている。 foldr/build に関する新しい定理は次にようになる。

• foldr c n (build g) ≧ g c n
• if c ⊥ ⊥ ≠ ⊥ and n ≠ ⊥, then: foldr c n (build g) = g c n

関係に対する幾つかの概念:

正格性(strictness)

(⊥,⊥)∈R

連続性(continuity)

∀i.(x_i,y_i)∈R ⇒ (∨x_i,∨y_i)∈R

全域性(totality)

∀(x,y)∈R. x≠⊥ ⇒ y≠⊥

left-closedness

≦;R = R

λ. (co)free でない代数的データ型

• 難しい点
  • word problem (語の問題)
  • (co)induction に証明が必要

λ. 蔵王で遭難の韓国人一行、捜索費用の支払い拒む

（・Д・）ポカーン・・・　　（⊇⊆）ゴシゴシ　　（・Д・）ポカーン・・・

「文化、国民性の違い」ってのはいいとしても、何でそこで「竹島」が出てくるんだか。

λ. モナディックシューティング　Shu-thing

純粋関数型雑記帳(2005-03-15) と think physically about computation. think computationally about physics. (2005-03-15) より。おー、すげー。

数回プレイして一応クリア出来た。ステージ半ばの7-Way弾を撃ってくる敵が出てくる辺りが一番難しかった。それから、ボスのヤ○○に笑いますた。

λ. 島根県議会、「竹島の日」条例を可決

島根県議会GJ

細田重雄県議の「日韓友好は大切だが、日本の立場や主張を鮮明にする必要がある。国民に竹島問題が広く認識されるよう期待する」という言葉には全く同感。

それから、「竹島の韓国領有権を主張する団体「独島郷友会」の会長で、同県議会を訪れていた韓国の崔在翼ソウル市議が議会棟の玄関付近でカッターナイフを取り出し、近くにいた警察官らに取り押さえられた」というのに驚いた。仮にも公職にあるものが一体何をしてるんだか。

基礎知識

外務省 : 竹島問題

日本側の主張

All About : 竹島問題の基礎知識

とてもわかりやすくまとまってる

『竹島は日韓どちらのものか』, 下條 正男

より詳しい歴史的経緯を知りたい場合にお勧め

λ. Jan Johannsen's cute title collection

cuteな論文タイトルのコレクション。

λ. i-know.jp

i-know.jp のアンテナを試しにちょっと使ってみる。http://i-know.jp/sakai/

ブックマークレットでアンテナに登録出来るのは存外に便利だなぁ。はてなアンテナとどっちがいいのかな。

λ. CMSC 451 Lecture 12, Myhill-Nerode minimization

メモ。マイヒル・ネロード(Myhill-Nerode)の定理 のわかりやすい説明。

λ. 花粉症?

目が痒くて仕方ない。スギ花粉ムカつく、ムカつくー。うがぁぁぁ。大体スギが多すぎるからいかんのじゃ。政府は公共事業でスギを切れちゅーに。それから、スギ花粉は環境汚染物質なので、スギに対して環境税をかけて、それを財源に花粉症対策でもしてくれ。

λ. Announce: 圏論勉強会(第五回)

そうそう。今週末は圏論勉強会の五回目がありますよ。堅苦しい集まりではないので、圏論に興味のある人は是非お気軽に御参加下さい。(初参加の方は mixi:圏論勉強会(第五回) か haskell-jpメーリングリスト で参加を表明しておくと良いと思います)

ちなみに、Session 6-9 は一度飛ばしてしまって、今回は Session 10 のブラウアーの不動点定理の話から始めるそうです。このセッションはこの本の前半最大の見せ場なので、お楽しみに!

日時 (今回はいつもと時間が違うので注意!!)

2005年3月19日(土曜) 10:00〜

場所

タイムインターメディア様 2階会議室 (地図)

テキスト

Conceptual Mathematics: A First Introduction to Categories

λ. 靖国参拝、対中戦略に有効　日米同盟強化への注意そらす　米の中国専門家見解

へぇ(3)。

λ. Linear Logic complements Classical Logic - Vaughan Pratt

だいぶ前にどこかのメーリングリスト*1で、「古典論理と線形論理は共に二重否定をキャンセル出来るという特徴を持っていて、ある意味で双対になっている*2」という話を見かけたのをふと思い出して検索してみた。結局そのメールは見つからず、この論文が見つかった。

内容は興味深いのだけど、たとえが多くて、僕にはいまいち良くわからない。

へぇ(3)。順序数を対象、順序数を集合としてみたときの関数を射とするような圏は、普通の集合の圏と同値なのか。これは、選択公理を仮定すれば von Neumann cardinal assignment を使って言えるのかな?

それから、CABA (complete atomic boolean algebra) というのがあって、その圏は集合の圏の双対圏になっているというのも初めて知った。completeってのはmeetとjoinが(有限集合に限らず)任意の部分集合に対して定義されてるって意味だろうけど、atomic ってのはどういうことを意味してるのだろう?

http://plato.stanford.edu/entries/boolalg-math/ によると、アトムとは false*3 ＜ x ＜ a を満たすような x が存在しない a のこと。ブール代数が atomic であるのは、任意のxについて、false ＜ x ならば、あるアトム a が存在して a ≦ x を満たすということ。なるほど、なるほど。でも、この定義は代数的でないので、CABA homomorphism が満たすべき性質が良くわからないな。アトムであることを保存するとかそんな感じか。 まあいいや。細かいところはおいておくとして、反変冪集合関手 Pow: Set^op→CABA と hom_CABA(-,2): CABA^op→Set によって、CABAとSet^opは圏同値になってるんだろう。きっと。

【2006-02-08 追記】 檜山さんが「反対圏の実現」というエントリで Set と AtomfulLat が反変圏同値ということを示していたのを見て、もう一度考え直したところ、上記は CABA homomorphism の条件以外は正しかった。CABA homomorphism は単にCABAの間の complete boolean algebra homomorphism で良いみたい。すると、CABA に「アトムが十分ある」ことと、CABA homomorphism が「アトム被覆性」を満たすことは証明でき、つまり CABA ならば AtomfulLat であることが言える。あとは檜山さんのと本質的に同じ構成になる。本質的に同じといっても、檜山さんの説明が代数を前面に出した説明だったのに対して、私は頭の中では(Locale と Frame の双対性を念頭に置いて)空間的なイメージで考えていたので、個人的な印象はちょっと違うけど。

…とりあえず、あとでちゃんと計算しよう。

関連リンク

• http://d.hatena.ne.jp/bonotake/20060208/1139373344

λ. 自衛隊動画

カッコ良すぎ。すばらしい。STAR.GAZER.1208. (2005-03-18) と ひろぶろ より。

【2006-06-14追記】 このリンク先は消えてしまったが、以下で見れるようだ。

• http://www.geocities.jp/isharejp/Japan_self_defense_force.html
• http://www.geocities.jp/isharejp/Japan_self_defense_force1.html

【2006-11-27追記】 YouTubeには他のバージョンも色々あった。 「YouTube軍事動画まとめ：日本国」を参照。

λ. hugsで日本語文字列をエスケープしないためのパッチを更新

hugsのshowや:typeで日本語文字列をエスケープしないためのパッチ を hugs98-Mar2005 用に更新した。

λ. 日本版ポリティカルコンパス (ドラフト1版)

日記っぽく (2005-03-22) より。たしかに本家の結果よりはしっくりくる。

判定結果は下記の通りです。

保守・リベラル度	0.31
(経済的な)右・左度	3

あなたの分類は保守右派です。
保守は伝統や公共の福祉を重視し、リベラルは個人の自由を重視する価値観です。
右派は小さな政府、左派は大きな政府を志向する価値観です。
いわゆる右翼は保守に、左翼はリベラルに対応しますので、ご注意ください。

ついでに、周りの人の結果を表にしてみた。 うーん、保守がいないなぁ(笑

λ. 卒業式

λ. 半落ち

泣いた。

λ. Hugs の Foreign.C.String での Unicode⇔locale の変換パッチを更新

Hugs の Foreign.C.String での Unicode⇔locale の変換を行うためのパッチ を hugs98-Mar2005 用に更新。

λ. 日本版ポリティカルコンパス (ドラフト2版)

先日この日記でも紹介した日本版ポリティカルコンパス。ドラフト2版が出たようなので早速やってみました。結果は前とほとんど変わらず(同じ人間がやってるんだから当たり前だ)。

判定結果は下記の通りです。

保守・リベラル度	0.21
(経済的な)右・左度	2.73

あなたの分類は保守右派(グローバリスト)です。

ところで、判定結果の分類は以下の4つなのだけど、ナショナリストが保守左派のこととは知らなかった。そうなの?

• 保守右派(グローバリスト)
• 保守左派(ナショナリスト)
• リベラル右派(リバタリアン)
• リベラル左派(リベラリスト)

λ. お絵描き圏論

コンパクト閉圏(compact closed categories)、これまであまり興味がなかったけれど、なにやら面白そうじゃないですか。

Chimaira.orgには他にも興味深い文章が沢山ある。著者の檜山正幸さんの日記「檜山正幸のキマイラ飼育記」はアンテナに追加しておこう。

λ. ETBダイアグラム

Arrows の説明でよく使われているのもこれですな。Arrows は monoidal じゃなくて pre-monoidal なので、そこはちょっとだけ違うけれど。

[2005-03-27 追記] Boxes-and-wires diagrams という呼び方もあるようだ。

λ. Traced Premonoidal Categories - Nick Benton and Martin Hyland

スライド

メモ。 Haskell の Arrows でいう ArrowLoop クラスが、traced premonoidal category に相当する。premonoidal category 一般については Premonoidal categories and notions of computation を見よ。

λ. キチガイ将棋戦法

http://d.hatena.ne.jp/yaneurao/20050328#p1 より。

面白すぎ。将棋はしばらくやってないけど、またやりたいなぁ。

λ. ソースからバイナリへ: GCCの内部機構 - Diego Novillo

Good Wrappers For People Who Love Bad Know-Hows より。

GIMPLE は A-Normal form*1 みたいなもんで、GENERIC -> GIMPLE の変換は A-normalization みたいなものだと考えればいいのかな。 静的単一代入(SSA, Static Single Assignment)の方は、そういった話とはちょっと違うか。SSAの発想は興味深いと思った。

• Efficiently computing static single assignment form and the control dependence graph

[2005-04-10 追記] お花見の時に、福盛さんに Modern Compiler Implementation in ML を見せて貰ったのだけど、SSAについて触れいている章もちゃんとあった。

λ. ＮＨＫ番組問題で安倍氏、朝日新聞を改めて批判

どっちが正しいかは知らんけど、朝日新聞は虚報を流したことに対して訂正と謝罪を行うか、もしくは安部中川両氏とNHKに対して正面から反論すべきだと思うよ。

λ. SNOW WHITE

くろりぼんドールガール の SNOW WHITE をプレイした。白雪姫を下敷きとした短編なんだけど、原作の怖さとは違った黒さがあって、とても良いです。

λ. 『真夜中の水戸黄門』, しりあがり寿

しりあがり寿は天才だよ。間違いないね。

λ. 『セマンティック・ウェブのためのRDF/OWL入門』, 神崎 正英

入門書として、とてもよく書けていると思う。

個人的にはこの本で新しく知ったことはあまりないけれど、自分の知識を確認できて良かったかな。

• サポートページ

λ. 卒業式「君が代」で５２人を戒告・減給処分　都教委

個人的には卒業式での国歌斉唱は当然と思うし、教師としての当然の職務を遂行しないのだから処分も当然と思う。が、それにしても、こういった処分者を出さなくてはいけないのはなんとも嫌な気分だ。 本来法律で強制なんかせずとも、国歌斉唱くらいは自然と実施出来るべきだと思うし、それが一番良いんだけどなぁ……

λ. Algebraically compact functors - Michael Barr

メモ。

Theorem 1.6 の証明、αが limit ordinal のときの h^α_α: A_α→B_α の構成が分からない。

1→T0 が重要だという点で Final Coalgebras are Ideal Completions of Initial Algebras と少し共通していると思った。