日々の流転

λ. 防衛相、現役空幕長を更迭　政府見解に反すると判断

アパグループ第一回「真の近現代史観」懸賞論文募集 から田母神俊雄氏の「日本は侵略国家であったのか」を読んでみたけど、論文というよりはエッセイとかそういった部類のものだと思った。 同意できる部分もあるけど、全体としてはかなり微妙。

田母神俊雄氏のしたことは非常に軽率な行動だし、「防衛省は職員が外部に職務に関する意見を発表する際、書面による届け出を義務づけているが、田母神氏は届け出ず防衛相は知らなかった」ということで内規違反ということなら、まあ更迭も仕方がないかなと思う*1。

関連

• jpn1_rok0/ただ暇だったから田母神空幕長論文を読む - NAVER総督府

λ. 『ダメな議論—論理思考で見抜く』 飯田 泰之

読了。

λ. derivors

(後で書き直す)

Seven Trees 問題を定理自動証明器を使って解く - ヒビルテ(2008-10-29) でやったことを少し形式的に考えると、

• 指標 Σ1 = {+, T0, T1, …} と
• 公理 E1 = { +の可換/結合則, T1=T0+T2, T2=T1+T3, … }

からなるセオリー (Σ1, E1*) での定理 T1=T7 を、

• 指標 Σ2 = {+, ×, 1, T} と
• 公理 E2 = { +の可換/結合則, ×の可換/結合則, 分配則, 1×x=x, T=1+T×T }

からなるセオリー (Σ2, E2*) での定理 T=T⁷ へと写したことになる。

私は institution の thoery ってのはこういうのを扱うためにあるのかと思ったのだけど、theory morphism は指標射の一種なので演算子を演算子に写すのに対して、ここで使った写像は演算子である Tk を演算子ではなくただの項でしかない T^k に写しているので、theory morphism にはなっていないのだった。

derivors

institutionではこういうのにどう対処しているのかな思って、Joseph A Goguen, Rod M Burstall. Institutions: abstract model theory for specification and programming. J. ACM, Vol. 39, No. 1. (January 1992), pp. 95-146. を読むと、以下のようなことが書いてあった。

For equational logic, there is another category with theories as objects, but with derivors, which map operators in Σ to derived operators in Σ', that is, to Σ'-terms, as morphisms [45]; in fact, this kind of morphism agrees with the usual morphism notion for Lawvere theories [69].

---

• 45. GOGUEN, J., AND BURSTALL, R. Some fundamental algebraic tools for the semantics of computation. Part 1: Comma categories, colimits, signatures, and theories. Theoret. Comput. Sci. 31, 2 (1984), 175-209.
• 69. LAWVERE, F. W. Functorial semantics of algebraic theories, Proc. Nat. A cad. Sci., U.S.A. 50 (1963), 869-872.

普通の theory morphism の代わりにこのderivorというのを使えば扱えそうだ。 ただ特定のinstitutionに依存してしまっているのが嫌な感じではあるけど。

さらに、Burstall, R. M. and Goguen, J. A. (1980): The Semantics of Clear: A Specification Language. Internal Report CSR-65-80, Department of Computer Science, University of Edinburgh. には、もう少し詳しいことが書いてあった。

(Note that this category of theories has certain signature morphisms as its morphisms, another category with the same objects would have as its morphisms derivors which map operators in Σ to derived operators in Σ' i.e. terms in Σ' with a binding sequence for their variables; but we shall not need this more complicated category. For a discussion of derivors see Goguen and Burstall [1978].)

---

• Goguen, J.A. and Burstall, R.M. (1978) Some fundamental properties of algebraic theories: a tool for semantics of computation. DAI Research Report No. 53, Dept. of Artificial Intelligence, University of Edinburgh.

え? 「shall not need this more complicated category」ということはderivorは結局不要なの?　Goguen and Burstall [1978] は入手できなかったので、仕方ないので自分で考えてみた。

考えてみた

I=(Sig,Sen,Mod,|=) を単一ソートの代数セオリーのinstitutionとする。

まず、signature morphism の拡張として derivor を定義する。 derivor f : Σ1→Σ2 は、Σ1のn引数演算子σをΣ2のn引数の派生演算子(λx1,…,xn. …)へと写すものとする。 また、文e∈Sen(Σ1)についてe中の演算子σをf(σ)で置き換え正規化したものを f(e)とする。f(e)にはラムダ式は現れないのでf(e)∈Sen(Σ2)になっている。 また、E⊆Sen(Σ1)に対して f(E) = {f(e) | e∈E} と定義する。

Sigの射をderivorに拡張した institution I' を考えることが出来る。 そして、この I' で derivor f : Σ1→Σ2 がセオリー Th1=(Σ1,E1^・) からセオリー Th2=(Σ2,E2^・) への theory morphism になっている、すなわち f(E1)⊆E2^・ が成り立っているとする。 このとき φがTh1の定理(φ∈E1^・)ならばf(φ)はTh2の定理(f(φ)∈E2^・)になるのだけど、これをI'やderivorを直接使わずに言いたい。

そこで、以下からなるセオリーTh3=(Σ3, E3^・)を新たに考える。

• Σ3 = Σ1 + Σ2
• E3 = in2(E2) ∪ Ef
• where Ef = { in1(σ)(x1,…,xn)=in2(f(σ))(x1,…,xn) | σ∈Σ1 }

in2は明らかに Th2→Th3 の theory morphism になっていて in2(E2)⊆E3^・ が成り立つ。 また、fの条件から f(E1)⊆E2^・ なので、in2(f(E1))⊆in2(E2^・)⊆in2(E2)^・⊆E3^・ 。 ここで、Efより in1(φ)∈E3^・ ⇔ in2(f(φ))∈E3^・ なので in1(E1)⊆E3^・ となり、in1はTh1からTh2への theory morphism 。

次に、忘却関手 Mod(in2) : Mod(Th3)→Mod(Th2) には逆 F : Mod(Th2)→Mod(Th3) が存在するので、 in2(φ)∈E3^・ ⇔ ∀M3∈Mod(Th3). M3|=in2(φ) ⇔ ∀M2∈Mod(Th2). F(M2)|=in2(φ) ⇔ ∀M2∈Mod(Th2). Mod(in2)(F(M2))|=φ ⇔ ∀M2∈Mod(Th2). M2|=φ ⇔ φ∈E2^・ 。

これらを使うと、φ∈E1^・ から

• まず in1 : Th1→Th3 によって Th3 に移動して in1(φ)∈E3^・ を得て
• Th3 でそこから in2(f(φ))∈E3^・ を得て、
• 最後に in2 を逆に辿って f(φ)∈E2^・ を得る

という流れで考えることが出来る。

結局、トートロジーみたいなことしか言っていないのだけど、derivorを考える代わりに、Th2を拡張したセオリーTh3と theory morphism Th1→Th3 を考えれば、同様の推論は出来ると。

Seven Trees の場合

最初の問題を考えると、Th3=(Σ3, E3^・) は以下のようになる。

• Σ3 = {in1(+), in1(T0), in1(T1), …} ∪ {in2(+), in2(×), in2(1), in2(T)}
• E3 = { in2(+)の可換/結合則, in2(×)の可換/結合則, 分配則, in2(1)in2(×)x=x, in2(T)=in2(1)in2(+)in2(T)in2(×)in2(T) } ∪ {x in1(+) y = x in2(+) y, in1(T0)=in2(1), in1(T1)=in2(T), …}

そして、以下のように推論することが出来る。

• T1=T7 ∈ E1^・
• ⇒ in1(T1)=in1(T7) ∈ E3^・
• ⇔ in2(T)=in2(T⁷) ∈ E3^・
• ⇔ T=T⁷ ∈ E2^・

λ. 携帯へのspamが急に増えた

携帯へのspamが急に増えて困っている。 Subjectや本文に明らかな特徴があるメールなので、簡単なパターンマッチではじけると思うのだけど、auのメールフィルタはFromとかでしかフィルタ出来ないっぽい。 いつの時代のメールサービスだよ。 使えなさ過ぎる。

λ. なりすまし規制?

ついでに言うと、携帯のネットワーク外から携帯のアドレスで届くメールをフィルタするための「なりすまし規制」とかいう設定があるのだけど、これの振る舞いも納得がいかない。 外部から携帯に転送する場合に、Resent-From を追加して envelope from も書き換えていても、Fromが携帯のアドレスだとフィルタされてしまうっぽい。

λ. ロシアンマスターズ！EX

というのを紹介された。 元ネタはわかんないけど凄いなぁ。

λ. 水泳

今日も1km泳いできた。 気のせいかも知れないけど、なんだか水温が少し上がっていた気がする。

λ. Election Results 2008

オバマ候補の大勝か。素晴らしい事だとは思うけど素直に喜べない自分がいる。ブッシュ政権はアレだったかも知れないけど、一方でその前のクリントン政権がどうだったかを思い出すと、ね。

λ. Agda2での複数引数のパターンマッチと definitional equality の落とし穴

以下のような関数があったとする。

f : Bool -> Bool -> Bool
f true true = true
f _ _ = false

このとき、f false x と false の間には definitional equality は成り立つが、f x false と false の間には definitional equality は成り立たないのね。 例えば、以下のようなゴールはそのままではrefine出来ない。

test : forall x -> f x false ≡ false
test x = {! ≡-refl !} -- Oops!, can't refine!

パターンマッチは構文的には全ての引数に対して同時にパターンマッチしているかのように見えるが、実際には左の引数から順に1引数毎にしかパターンマッチしていなくて、どの節を用いるかが決定できていないということだろうか。 こうなっていることには何か理由はあるのだろうけど、非常に直観に反する振る舞いだと思った。

また、単に直観に反するだけでなく実際に困ることもあって、上の例のようなものを証明するときには、先行する全ての引数について場合わけして具体化しなくてはならない。 上の例であれば以下のようにすれば良いのだけど、これは引数の個数や構築子の種類が多い場合には非常に面倒だ。

test : forall x -> f x false ≡ false
test true  = ≡-refl
test false = ≡-refl

λ. 『統計・確率のしくみ』　郡山 彬, 和泉沢 正隆

読了。

λ. haskell-jpのアーカイブ

nobsunに協力していただき、haskell-jpメーリングリストのアーカイブを <URL:http://www.sampou.org/cgi-bin/w3ml.cgi/haskell-jp/> に作りました*1。 ご活用ください。

λ. パーセンテージ

たとえば、最近の銀行の利息は0.1％くらいまで下がっているが、これなどは、1/1000と分数でいった方が直感的にわかりやすいのではないだろうか。パーセントを用いているのに、そのうえ少数を使うのは、いかがかと思う。しばらくは好景気にはならないだろうから、この際、利息には千分率のパーミルを使う習慣にしてはどうだろう？

金利の差分等については、0.01%を表すベーシスポイント(basis point, bp)が普通に使われていると思うが。

λ. 『大学の話をしましょうか—最高学府のデバイスとポテンシャル』 森 博嗣

読了。

λ. 第四十六回圏論勉強会

今日は圏論勉強会だった。 写真

今回は 6.4節 The Temperley-Lieb Category の前半部分で、結合演算と恒等射を定義してテンパリー・リーブ圏(TL)が圏になっていることを確認。今回もやっぱり定義が巧妙で感心した。前回やったP(n,m)の定義とかを半分忘れていて大変だったが。

今回やり残した6.4節の残りは、TL が pivotal category であるという話と、TLと3節で定義したDが strict pivotal dagger category として同型であるという話になるようだ。

雑談では、この6節の「Planar Geometry of Interaction and the Temperley-Lieb Algebra」という名前にも含まれている Geometry of Interaction に関係して、 檜山さんに Int Construction というもののイメージの紹介をしてもらった。Int Construction は自然数から整数を構成する構成を一般化し、トレース付きモノイダル圏からコンパクト閉圏を構成する。そういえば、 「再帰プログラムの幾何」にもそんな話があったなぁ……

二次会では白石先生とかDHMOとか。

λ. ストリーム上のキモい関数

Wadler's Blog: A bizarre function over streams の関数がキモくて面白い。

(後で書く)

λ. デジタルネイティブ度チェック

そんなに大げさに騒ぐような話でも無いとは思うけど、なんか流行っているようなのでやってみた。

らしい。

λ. Information Flow: The Logic of Distributed Systems (ペーパーバック)

チャネル理論(Channel Theory)の教科書である Information Flow: The Logic of Distributed Systems (Cambridge Tracts in Theoretical Computer Science)(Jon Barwise/Jerry Seligman) のペーパーバック版が最近出版された。チャネル理論は情報の流れやその背景にある規則性といったものを扱おうとする理論で、定性的情報理論などと呼ばれることもある。まあ、そういう大げさなお題目はどうでも良いのだけど、シンプルでちょっと面白い理論だ。

向井先生がチャネル理論を気に入っていたこともあって、私もこの本は昔途中まで読んだことはあるんだけど、そのときには最後まで読み終えてはいなかった。 今回ペーパーバック版が出て、しかも今は円高で少し安く買えるので、これを機にまた久しぶりに読んでみようかと思い、購入してみた。

……のだけど、Amazonのページをみたら「あわせて買いたい」と「この商品を買った人はこんな商品も買っています」とで、例の郡司ペギオ-幸夫氏の「時間の正体 デジャブ・因果論・量子論」*1が挙げられていて微妙に脱力した。一緒にしないでくれよぉ。もきゅ (´・ω・`)

λ. 定額給付金

なんかもうグダグダだな。 ところで、景気対策としての有効性とかは置いておくとして、素朴な疑問がひとつある。 「高額所得者に自発的な辞退を求める」という話があったが、何で基準は資産とかではなく所得なのだろうか。 これって何か経済学的な理由とかがあるのかな。

【追記】 単に資産よりも所得の方が限界消費性向に対する相関が大きいということか。

λ. Algebraic Topology: A guide to literature

池上さんが Inemuri nezumi diary(2008-10-20) で信州大学玉木研究室の Algebraic Topology: A guide to literature を紹介している。 圏論勉強会で参照したことはなかったと思うけど、個人的にはこのサイトには何度かお世話になっていて、本当に素晴らしいと思う。

λ. 水泳

今日も帰りに1km泳いできた。

λ. お菓子

今回は少なめ。

λ. “Functorial Semantics of Algebraic Theories” by F. William Lawvere

ちょっと前に読んだ論文。 代数セオリーやそのモデルの形式化を最初に見たときは「へぇー」と思った。 言われてみれば当たり前なんだけどね。 どう形式化するかというと、代数セオリーを自然数を対象とし対象nが対象1*1のn個の直積となっている小さな圏Aとして定義する。 例えば群であれば、この条件と以下から自由生成される圏がセオリーになる。

• e : 0→1
• inv : 1→1
• μ : 2→1
• μ∘〈e, id〉 = id
• μ∘〈inv, id〉 = id
• μ∘〈μ, id〉 = μ∘〈id, μ〉

同様に束を考えると、前述の条件と以下から自由生成される圏がセオリーになる。

• ∨, ∧ : 2→1
• true, false : 0→1
• ∧∘〈π₂, π₁〉 = ∧
• ∨∘〈π₂, π₁〉 = ∨
• ∧∘〈∧, id〉 = ∧∘〈id, ∧〉
• ∨∘〈∨, id〉 = ∨∘〈id, ∨〉
• ∧∘〈id, true∘!〉 = id
• ∨∘〈id, false∘!〉 = id
• ∧∘〈id, id〉 = id
• ∨∘〈id, id〉 = id
• ∧∘〈π₁, ∨〉 = π₁
• ∨∘〈π₁, ∧〉 = π₁

そして、セオリー間の射を対象を保存する関手とし、これらのなす圏をJとする。 セオリーAのモデルとなる代数はAからSetへの直積を保存する関手と考えられるし、準同型は関手の間の自然変換と考えられるので、A代数の圏は一種の関手圏。Jの射 f : A→B に対して関手 Set^f : Set^B→Set^A はB代数の圏からA代数の圏への忘却関手になり、この関手の左随伴が存在する。

さらに、ある圏があるセオリーの代数の圏になっているための条件、などなど。

【2008-11-19追記】 ところで、どっかで見たような話だなぁと思ったら、Conceptual Mathematics: A First Introduction to Categories(F. William Lawvere/Stephen Hoel Schanuel) の ARTICLE III: Examples of categories の 11. Types of structure あたりでこういう話は散々やったのだった。 もちろん、Conceptual Mathematics ではこんなにシステマティックにやってはいないけど。

λ. 「プログラムの安全性を高めるために—今注目を集める関数型言語に迫る—」

『圏論の基礎』の翻訳等で有名な三好先生による関数型言語の紹介。 三好先生の写真初めて見た。

λ. “Seven trees in one” by Andreas Blass

Following a remark of Lawvere, we explicitly exhibit a particularly elementary bijection between the set T of finite binary trees and the set T⁷ of seven-tuples of such trees. “Particularly elementary” means that the application of the bijection to a seven-tuple of trees involves case distinctions only down to a fixed depth (namely four) in the given seven-tuple. We clarify how this and similar bijections are related to the free commutative semiring on one generator X subject to X = 1 + X². Finally, our main theorem is that the existence of particularly elementary bijections can be deduced from the provable existence, in intuitionistic type theory, of any bijections at all.

Seven Trees やっと解けた - ヒビルテ(2008-10-28) のツッコミと、Seven Trees：最後のヒント＋もっと面白い話 - 檜山正幸のキマイラ飼育記 から。 例の Seven Trees を詳しく扱った論文で、多項式P(X)とQ(X)に関して以下が同値だという話。

1. Tを二分木の集合としたときに、P(T)とQ(T)の間に very explicit な全単射が存在する (combinatorial equivalence)
2. 半環 N[X]/(X=1+X²) でP(X)=Q(X) が 成り立つ (algebraic equivalence)
3. P(T) と Q(T) の間の全単射の存在を構成的に証明できる

t=1+t² の複素数解 t = (1 + i√3)/2 の性質に関しては、P(t)を多項式P(X)の“Euler characteristic”と呼んでいて、それとP(ℵ₀)を{0, 有限, 無限}の3値で解釈した「次元」とをあわせたものが、jointly injective だと言っている。つまり、両方とも等しければ P(X)=Q(X) 。

例えば、P(X)=X⁷ と Q(X)=X の場合には、P(t)=Q(t)=t でかつ P(ℵ₀)=Q(ℵ₀)=ℵ₀ なので、P(X)=Q(X) 。 一方で、P(X)=X⁶ と Q(X)=1 の場合には、P(t)=Q(t)=1 だけど、P(ℵ₀)=ℵ₀≠1=Q(ℵ₀) なので、P(X)≠Q(X) 。

最後の構成的集合論の話は面白そうだけど難しいね。一応グロタンディークトポスとか定義は調べて分かったけど、分類トポスやらグロタンディーク位相での強制法やらの話で挫折。

• <URL:http://dx.doi.org/10.1016/0022-4049(95)00098-H>
• <URL:http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.8517>

λ. Arrays without bounds

Haskellの普通の配列はサイズを指定して作るので、リストと違って無限の長さを持つ配列は作れないのだけど、こいつは無限の長さの配列を実現したものだそうだ。 実装はとてもシンプル。メモ化とかに便利。

ただ、内部の各リサイズでサイズが幾何的にしか増えないというだけでは、要素アクセスの償却計算量が O(1) であることは保証出来ないような。 というのも、配列はランダムアクセスされるので、十分な「引当」が行われる前に次のリサイズが起こりえると思うので。

λ. iKnowの「プロの英語（ファイナンス編）」が終わった

iKnowで「プロの英語（ファイナンス編）」が終わった。次は 「プロの英語（企業会計編）」に進もうかと思ってたんけど、近いうちに初めての海外旅行に行きそうなので、先に「英語で旅行シリーズ」をやることにした。

ところで、私の知り合いで iKnow をやってる人がいましたら、よかったら一緒にやりませんか?
(⇒ 私のアカウント: <URL:http://www.iknow.co.jp/user/sakai>)

λ. 「勝間和代の日本を変えよう」

読了。

λ. “Conceptual Mathematics: A First Introduction to Categories” 第二版

そういえば、Conceptual Mathematics: A First Introduction to Categories の第二版が出るらしい。発売予定は来春 2009/2/28 。

• ハードカバー版
• ペーパーバック版

第一版ではハードカバー版は374ページ、ペーパーバック版は376ページだったのが、第二版では両方とも408ページになってる。内容も追加されてるのかな。

λ. TOEICの結果

そういえば、先日受けたTOEICの結果が出ていた。

Total Score

885 (前回 840)

Listening Score

435 (前回 420)

Reading Score

450 (前回 420)

前回2006年に受けたときからほぼ2年ぶり。 前回と違って見直している時間がなかったから、絶対下がってると思ってたんだけど、実は上がってた。 ちょっと前に、iKnowでおしごとの英語シリーズをやってて、ビジネス系の語彙が増えていたのが良かったのかも。 あと、前回「次に受けるときは900点を目指したい」と書いたけど、この目標は次に持ち越し。

λ. 舎利禮文 【初音ミク×M＠STER_fonts Pv】

このセンスは凄いな。

λ. 今日も泳いできた

今日も帰りに泳いできた。 だんだん、1km泳いでもそんなにバテないようになってきた。

λ. ビックカメラSuicaカード

Amazonクレジットカードが終了してしまうので移行先として考えていたのだけど、今日帰りにビックカメラで申し込んでしまった。 ただ、ポイントをこのカードのSuica部分にしかチャージ出来なくて、かつこのカードのSuica部分には定期券を載せられないというのが、微妙かも知れない。

λ. グーグル、絵文字を世界共通化へ—オープンソースプロジェクト開始

素晴らしい！　しかし、グーグルのような会社が手を出すまで、誰もこういった取り組みをきちんとやろうとはしていなかったのは、やっぱりキャリア主導の垂直統合モデルの負の面じゃなかろうかと思う。

• Emoji Symbols (Unicode Symbols)

λ. RHG読書会::東京 Practical Common Lisp 第十二回

Latin-1には両手で数えられるくらいの文字しかないとか、二本かけてもまだ大丈夫だとか……