2002-03-08
λ. 徹夜した理由として「眠るのが面倒くさかったから」というのは、どうやら通じないようだ。
λ. Geek Chicks: 第2考
あのyomoyomoさんの所からリンクが張られているのを偶然見つけてビックリした。既に存在を忘れていたファイルだし、今読み返すと恥ずかしい部分だらけだけど、世の中色々あるもんだなぁ。
(「URIはひみちゅ」とか書いておきながらしっかりサーチエンジンに捕捉されてるんだから我ながら間抜けなものだ)
今日の発見：女子高生が作った（？）ウィルスが話題になった今日偶然発見した Geek Chicks: 第2考。これは興味深い。日本でもこういう文章を書く女性ハッカーっていないのかなぁ
λ. ポトリスの発音
日本語が「f」と「h」をあまり区別しないのと同じように(?)、韓国語では「f」と「p」を区別しないっす。なので、韓国人の「Fortress」と「버트리스 」の発音は同じだったりします。
λ. C-Mix
[ruby-dev:16263]でcmixというのを知る。
2003-03-08
λ. gtk2 on cygwin
急に色々なところから注目されてビックリする。柴田さん、早田さん、CyGnomeのBiju G. C.さん、むとうさん、安部さん、たむらさん、どうもありがとうございます。
それから、スクリーンショットに足永さんのGImageViewの画像を加えてみたり。プラグインをDLL化したりとかは面倒そうだけど、バータリーになら簡単にコンパイル可能。
λ. Rucheme / Scheme(subset) interpreter on Ruby
のコードを眺めていて、以前に書いたSchemeもどきのRougeを思い出す。当時はSchemeに関する知識も言語処理系の実装に関する知識もほとんど無かったこともあって、Rougeのコードは今見返すと随分ひどいなぁ。
しかし、末尾再帰の除去ってどうやって実装するんかな。うーん。しかし、properly tail recursive : 正しく末尾再帰を行う、という表現、なんか不思議。
SchemeをRubyで実装する場合、Ruby自身が末尾再帰の除去に対応していない以上、例えばトランポリンを使う形に変換するとか……(以下略)
λ. OHMSS
って、「On Her Majesty's Secret Service」の略なのね。知らなかった。
ψ ささだ [はじめまして。とりあえず悩んでます。いかに楽に仕様準拠するか。というかマクロ無理っぽいです。面倒で。]
ψ さかい [R5RSはそんなに大きな仕様ではないですけど、 真面目に準拠するのはやはり結構大変みたいですね。 私はマクロは_仕..]
ψ むとぽん [おーい、オレが忘れられてるよ〜(T_T) ＞ gtk2 on cygwin]
ψ なかだ [redoを使うとか。 とまったく見もせずに書いてみるテスト。]
ψ さかい [や、申し訳ない。追加しときました。> むとうさん # 単にむとうさんの日記を見るよりも先に書いてしまっていただけなの..]
ψ ささだ [とりあえずやってみました。末尾再帰除去。いろいろアレでナニでいやーんなソースになりました。 redo はなんとなく嫌..]
ψ ささだ [ついでに、いまだにscheme/言語処理系の知識は十分でないです。私。処理系作ってると新たな発見があって面白い。って..]
ψ さかい [そうですね。 実装して初めて気付く事って結構ありますよね。 最近もCPL(Categorical Programm..]
ψ ささだ [eval って定義(define) 駄目なんですか。知らなかった。仕様読んで無いじゃん、私。コンパイラにそんなに向か..]
ψ さかい [evalの説明に以下のような下りがあるので、定義を許す必要は無いというだけで、別に許したって構わないと思います。 ..]
ψ ささだ [げ、definitions って non-expression だったのか！(駄目じゃん俺・・・) lambda の..]
2005-03-08
λ. 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 ∘ ψ の解の一つであることがわかる。
![\xymatrix@+25pt{
A \ar[d]_{\psi} \ar[r]^{\mbox{unfold}_T(\psi)} \ar@{}[dr]|*++{\circlearrowleft}
& {\nu T = \mu T} \ar@<-1ex>[d]_{\mbox{out}_T} \ar[r]^{\mbox{fold}_T(\phi)} \ar@{}[dr]|*++{\circlearrowleft}
& B
\\
TA \ar[r]_{T(\mbox{unfold}_T(\psi))}
& T{\nu T} = T{\mu T} \ar@<-1ex>[u]_{\mbox{in}_T} \ar[r]_{T(\mbox{fold}_T(\phi))}
& TB \ar[u]_{\phi}
}](tex/38b55cc8435f305118b1d65102974517.png "\xymatrix@+25pt{
A \ar[d]_{\psi} \ar[r]^{\mbox{unfold}_T(\psi)} \ar@{}[dr]|*++{\circlearrowleft}
& {\nu T = \mu T} \ar@<-1ex>[d]_{\mbox{out}_T} \ar[r]^{\mbox{fold}_T(\phi)} \ar@{}[dr]|*++{\circlearrowleft}
& B
\\
TA \ar[r]_{T(\mbox{unfold}_T(\psi))}
& T{\nu T} = T{\mu T} \ar@<-1ex>[u]_{\mbox{in}_T} \ar[r]_{T(\mbox{fold}_T(\phi))}
& TB \ar[u]_{\phi}
}")
一方、cartesian closed でかつ不動点コンビネータが存在するのなら、fix(λf. φ ∘ Ff ∘ ψ) *1 によって別の解を定義することが出来る。この二つは等しいか?
homsetがCPOでかつ合成が正格かつ連続で不動点コンビネータが最小不動点を返すならば、等しいことは簡単に言える。α,β,γを次のように定義する。
- α(f) = φ ∘ Tf ∘ in-1
- β(f) = out-1 ∘ Tf ∘ ψ
- γ(f) = φ ∘ Tf ∘ ψ
すると、
- fold(φ) = ∨n<ω αn(⊥μT→B)
- unfold(ψ) = ∨n<ω βn(⊥A→νT)
- fix(λf. φ ∘ Ff ∘ ψ) = ∨n<ω γn(⊥A→B)
であり、帰納法によって αn(⊥μT→B) ∘ βn(⊥A→νT) = γn(⊥A→B) が証明でき、合成は連続なので fold(φ) ∘ unfold(ψ) = fix(λf. φ ∘ Ff ∘ ψ) が言える。
*1 CCCの射としてちゃんと書くのは面倒なのでラムダ式で書いておく
λ. Hylo Shift Law
自然変換 η: F→G に対して、
μη = foldF(inG ∘ ημG): μF→μG
と定義する。すると、foldF(φ ∘ ηB) = foldG(φ) ∘ μη が成り立つ。
![\xymatrix@+25pt{
F(\mu F) \ar[r]^{F(\mu\eta)} \ar[dd]_{\mbox{in}_F} \ar@{}[ddr]|*++{\circlearrowleft}
& F(\mu G) \ar[r]^{F(\mbox{fold}_{G}(\phi))} \ar[d]_{\eta_{\mu G}} \ar@{}[dr]|*++{\circlearrowleft}
& FB \ar[d]^{\eta_B}
\\
& G(\mu G) \ar[r]^{G(\mbox{fold}_G(\phi))} \ar[d]_{\mbox{in}_G} \ar@{}[dr]|*++{\circlearrowleft}
& GB \ar[d]^{\phi}
\\
\mu F \ar[r]_{\mu\eta}
& \mu G \ar[r]_{\mbox{fold}_G(\phi)}
& B
}](tex/7696115a83b967ba6e064066bbde7405.png "\xymatrix@+25pt{
F(\mu F) \ar[r]^{F(\mu\eta)} \ar[dd]_{\mbox{in}_F} \ar@{}[ddr]|*++{\circlearrowleft}
& F(\mu G) \ar[r]^{F(\mbox{fold}_{G}(\phi))} \ar[d]_{\eta_{\mu G}} \ar@{}[dr]|*++{\circlearrowleft}
& FB \ar[d]^{\eta_B}
\\
& G(\mu G) \ar[r]^{G(\mbox{fold}_G(\phi))} \ar[d]_{\mbox{in}_G} \ar@{}[dr]|*++{\circlearrowleft}
& GB \ar[d]^{\phi}
\\
\mu F \ar[r]_{\mu\eta}
& \mu G \ar[r]_{\mbox{fold}_G(\phi)}
& B
}")
同様に νη = unfoldG(ηνF ∘ outF): νF→νG と定義すると、unfoldG(ηA ∘ ψ) = νη ∘ unfoldF(ψ) が成り立つ。
T∈{F,G} について (μT,in-1)=(νT,out) ならば、μη=νη となるので、foldF(φ ∘ ηB) ∘ unfoldF(ψ) = foldG(φ) ∘ μη ∘ unfoldF(ψ) = foldG(φ) ∘ νη ∘ unfoldF(ψ) = foldG(φ) ∘ unfoldG(ηA ∘ ψ) が言える。
この等式 foldF(φ ∘ ηB) ∘ unfoldF(ψ) = foldG(φ) ∘ unfoldG(ηA ∘ ψ) によって、自然変換ηを移動させることが出来る。これを Hylo Shift Law と呼ぶ。
λ. Hylomorphismの三つ組み表現 (Hylomorphisms in triplet form)
Hylo Shift Law によって自然変換を自由に移すことが出来るので、foldF(φ ∘ ηB) ∘ unfoldF(ψ) = foldG(φ) ∘ unfoldG(η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 inF) = gA(φ)
- Acid Rain : Anamorphism
- ∀h:∀X.(X→FX)→(X→C), φ:A→FA. (hνF outF) ∘ unfold(φ) = hA(φ)
これらを酸性雨定理と呼ぶそうだ。
パラメトリシティを仮定すると色々な事が言えてとても楽しいのだけど、不動点コンビネータや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 ψ) 。
![\xymatrix@+30pt{
{F\mu F} \ar[d]_{\mbox{in}} \ar[r]^{F(\mbox{fold}(\tau_{\mu F}\mbox{in}))} \ar@{}[dr]|*++{\circlearrowleft}
& {F\mu F} \ar[d]|{\tau_{\mu F} \mbox{in}} \ar[r]^{F(\mbox{fold}(\psi))} \ar@{}[dr]|*++{\circlearrowleft}
& FB \ar[d]^{\tau_B \psi}
\\
{\mu F} \ar[r]_{\mbox{fold}(\tau_{\mu F}\mbox{in})}
& {\mu F} \ar[r]_{\mbox{fold}(\psi)}
& B
}](tex/39dabfd4955261a1ae3719c0028a59dc.png "\xymatrix@+30pt{
{F\mu F} \ar[d]_{\mbox{in}} \ar[r]^{F(\mbox{fold}(\tau_{\mu F}\mbox{in}))} \ar@{}[dr]|*++{\circlearrowleft}
& {F\mu F} \ar[d]|{\tau_{\mu F} \mbox{in}} \ar[r]^{F(\mbox{fold}(\psi))} \ar@{}[dr]|*++{\circlearrowleft}
& FB \ar[d]^{\tau_B \psi}
\\
{\mu F} \ar[r]_{\mbox{fold}(\tau_{\mu F}\mbox{in})}
& {\mu F} \ar[r]_{\mbox{fold}(\psi)}
& 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 φ) 。
![\xymatrix@+30pt{
A \ar[d]_{\sigma_A \phi} \ar[r]^{\mbox{unfold}(\phi)} \ar@{}[dr]|*++{\circlearrowleft}
& {F\nu F} \ar[d]|{\sigma_{\nu F} \mbox{out}} \ar[r]^{\mbox{unfold}(\sigma_{\nu F}\mbox{out})} \ar@{}[dr]|*++{\circlearrowleft}
& {\nu F} \ar[d]^{\mbox{out}}
\\
FA \ar[r]_{F(\mbox{unfold}(\phi))}
& {F\nu F} \ar[r]_{F(\mbox{unfold}(\sigma_{\nu F}\mbox{out}))}
& {F\nu F}
}](tex/e27585ac30ad32e6b24bd7722c3d54c4.png "\xymatrix@+30pt{
A \ar[d]_{\sigma_A \phi} \ar[r]^{\mbox{unfold}(\phi)} \ar@{}[dr]|*++{\circlearrowleft}
& {F\nu F} \ar[d]|{\sigma_{\nu F} \mbox{out}} \ar[r]^{\mbox{unfold}(\sigma_{\nu F}\mbox{out})} \ar@{}[dr]|*++{\circlearrowleft}
& {\nu F} \ar[d]^{\mbox{out}}
\\
FA \ar[r]_{F(\mbox{unfold}(\phi))}
& {F\nu F} \ar[r]_{F(\mbox{unfold}(\sigma_{\nu F}\mbox{out}))}
& {F\nu F}
}")
この二つを hylomorphism を使った形で表現すると、以下を得る。
- Cata-HyloFusion
- τ: ∀A.(FA→A)→FA→A ⇒ 〚φ,η1,outF〛G,F ∘ 〚τ(inF),η2,ψ〛F,H = 〚τ(φ ∘ η1),η2,ψ〛F,H
- Hylo-AnaFusion
- σ: ∀A. (A→FA)→A→FA ⇒ 〚φ,η1,σ(outF)〛G,F ∘ 〚inF,η2,ψ〛F,H = 〚φ,η1,σ(η2 ∘ ψ)〛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 inF -
unbuild : (C→μF) → (∀X.(FX→X)→(C→X))
unbuild f = ΛX. λφ. foldX(φ) ∘ f
したがって、関数 f: C→μF を build g の形で書いておけば foldX(φ) ∘ f = foldX(φ) ∘ build g = (unbuild (build g))X φ = gX φ という書き換えが出来る。 これは酸性雨定理からも明らか。
リストの場合については、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 outF -
undestroy : (νF→C) → (∀X.(X→FX)→(X→C))
undestroy f = ΛX. λφ. f ∘ unfoldX(φ)
したがって、関数 f: νX→C を destroy h の形で書いておけば、 f ∘ unfoldX(φ) = destroy h ∘ unfoldX(φ) = (undestroy (destroy h))X φ = hX φ という書き換えが出来る。 これは酸性雨定理からも明らか。
リストの場合、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)
2008-03-08
λ. sized-list の append
PPL2008の懇親会でzyxwvさん、yoshihiro503さんと話していたときに出た話(の一つ)。
以下で定義される、サイズ情報を型に持つようなリスト型があったとする。
data Z
data S n
data List n a where
Nil :: List Z a
Cons :: a -> List n a -> List (S n) a
このリスト型に対して連結(append)を定義したいのだが、どうやって型を付けるかというのが自明ではない。
関数従属性を使う方法 (ダメな方法)
class Plus m n o | m n -> o instance Plus Z n n instance Plus m n o => Plus (S m) n (S o) append :: Plus m n o => List m a -> List n a -> List o a append Nil ys = ys append (Cons x xs) ys = Cons x (append xs ys)
これは一見うまくいきそうだが、第一引数がNilの場合であっても、GHCは List n a と List o a が同じ型であることを認識してくれず、型エラーとなる。 これは関数従属性の落とし穴と同じ問題。
GADT の type refinement を利用する方法
data Plus m n o where
PlusZ :: Plus Z n n
PlusS :: Plus m n o -> Plus (S m) n (S o)
append :: Plus m n o -> List m a -> List n a -> List o a
append PlusZ Nil ys = ys
append (PlusS n) (Cons x xs) ys = Cons x (append n xs ys)
関数従属性の場合と違って、GADTのパターンマッチ時にはちゃんと type refinement が起こるので、型付け出来る。 が、適用する際にわざわざPlus型の値を与えなくてはならないのが面倒くさい。
専用の型クラスを使う方法
class Append a b c where
append :: a -> b -> c
instance Append (List Z a) (List n a) (List n a) where
append Nil ys = ys
instance Append (List n a) (List m a) (List o a) =>
Append (List (S n) a) (List m a) (List (S o) a) where
append (Cons x xs) ys = Cons x (append xs ys)
そりゃ出来るけどさぁ……何か色々負けた気分。
もう少し賢い定義も出来るけど、本質的にはあまり変わらないと思う。
型関数を使う方法
type family Plus m n type instance Plus Z n = n type instance Plus (S m) n = S (Plus m n) append :: List m a -> List n a -> List (Plus m n) a append Nil ys = ys append (Cons x xs) ys = Cons x (append xs ys)
GHCの開発版に導入されている型関数(type function)を使う方法が一番スマートか。GHCの型関数の詳細については Towards open type functions for Haskell と GHC/Type families - HaskellWiki を参照。
2009-03-08
λ. 第五十回圏論勉強会＠NII
今回は、DEX-SMI Workshop on Quantum Statistical Inference のために来日していた、量子情報の研究者を迎えて、量子情報のセミナーみたいな感じだった。 量子情報やっぱりよくわからんなぁ、面白いけど。
何か話したらという事だったので、「Functional Reactive Programming の事についてでも話すか、これもお絵かきに関係するし」と思ってたのだけど、ちょっとそういう感じでも無かったので、とりあえず Thorsten Altenkirch の A functional quantum programming language (c.f. ヒビルテ(2008-06-30))を拝借して、QMLの紹介などしてみた。*1
ちょっと勿体無かったと思ったのは、量子テレポーテーションのコンパイル例を説明したときに、単に出力された量子回路のテキスト表現だけ見せるのではなくて、QMLから量子回路へのコンパイル - ヒビルテ(2008-08-23) の図を見せれば良かったということ。 あと、発表中ちょっとテンパっていたときに、salmonsnareさんの「まあ、おちつけ。」というtweetがポップアップして、うけた。
それから、記念撮影をしようという話をしてたのに、するのをすっかり忘れていて後悔。
関連
- たけをさん
- hiroki_fさん
- 圏論勉強会スペシャル：Tokyo Quantum Meeting - 檜山正幸のキマイラ飼育記(2009-03-09) (檜山さん)
