日々の流転

λ. *-autonomous category

これまで「名前からしてきっと難しいに違いない!　クワバラクワバラ」とか思って近づいていなかったんだが、檜山さんの「論理とはなにか？ (4:完) -- 論理から圏へ」で出てきたので調べてみたら、単に symmetric monoidal closed category に dualizing object ⊥ を追加しただけだった。拍子抜けした……

λ. topを追加する関手

topを追加する関手 F: Cppo→Cppo を考える。

F(X) = {P(x) | x∈X} ∪ {T}
       ∀x∈X. P(x)<T
F(f)(T) = T
F(f)(P(x)) = P(f(x))

この関手は非正格性を保存するが、自然変換 F→Id は存在しない。この関手の始代数は存在するだろうか?　以下の (X,φ) は F の始代数になっているだろうか?

X = {-∞ < … < -2 < -1 < 0}

φ : FX→X
φ(T) = 0
φ(P(x)) = x - 1

いや、ならないか。(Y,ψ)を以下のように定義する。

Y = {0 < 1}

ψ: FY→Y
ψ(T) = 1
ψ(P(x)) = x

h: (X,φ)→(Y,ψ) は -∞ を 0, 1 のどちらに写してもよいので、一意には決まらない。

λ. プラグインの不正な操作

Naxosの音楽を聴いているFirefoxのウィンドウを閉じると、上記のようなダイアログが出てFirefoxの動作がおかしくなることがある。これは困る。

Windows Media Player のバージョンは10.00.00.4036。 Firefox のバージョンは1.5.0.7。

λ. Programs, grammars and arguments: a personal view of some connections between computation, language and logic by J. Lambek

rpfさんのmixi日記に書いてあったC-monoidは何だろうと思って検索したら発見した論文。しかし、こうしてみると Lambek は色々やってるねぇ。古き良き計算機科学者というかなんというか。

「The natural numbers object may be constructed in a model of polymorphic λ-calculus as a retract of Π_X (X^X)^(XX) ≅ Π_X X^(XX+1) where Π_X is a kind of formal product in a CCC.」という部分が分からん。formal product というのはその圏の対象をインデックスにするような直積のことだと思うが、正確な定義は?

【2007-10-27追記】 数学ガール(結城 浩) の p.200 で「(2⁰+2¹+2²+…)・(3⁰+3¹+3²+…)」を形式的積と呼んでいた。ミルカさんによれば「この積は正の無限大に発散する。だから形式的積と言ったんだ」とのこと。

PERもまだイマイチ良くわからん。

多重線形代数(multiliner algebra)には構造規則(structual rules)が欠けているそうだけど、多重線形代数を知らないのでこれは後で調べるか。それから、「However, in Hopf algebras and in general production grammars the tensor product and its dual coincide.」という部分についても後で調べる。

λ. 『儒教—ルサンチマンの宗教』 浅野 裕一

を読了。

λ. The Theory of Parametricity in Lambda Cube by 竹内 泉

Fωでのparametricityについて興味があったので読んでいるところ。ただ、higher-order polymorphism に対する parametricity は扱いにくいように思う。おそらく、Folds, Church Encodings, Builds, and Short Cut Fusion for Nested Types: A Principled Approach でのhfoldに対してのgfoldのようなより扱いやすい形が必要になるのではないかと思った。

参考:

• <URL:http://sakura.math.kyushu-u.ac.jp/algi/09/program.html>

関連エントリ

• 強い直和?

【2006-12-20 追記】 Definition 3.17 (Conformity Relation) では、αが種のとき「 <ΠX:α. P>^{θ} = ∀X1:αθ^l, X2:αθ^r. ∀Y:(|X:α|)^{{θlr,(X1,X2)/X}}. <P>^{{θ,(X1,X2,Y)/X}} 」と定義しているけど、Tが型のときの「<Πx:T. P>」と同じで「 <ΠX:α. P>^{θ} = λy:(ΠX:α. P)θ^l, z:(ΠX:α. P)θ^r. ∀X1:αθ^l, X2:αθ^r. ∀Y:(|X:α|)^{{θlr,(X1,X2)/X}}. <P>^{{θ,(X1,X2,Y)/X}} (y X1) (z X2) 」と定義しないとまずいはず。そうしないと、Definition 3.9 (Kind of Conformity Relation) と種が一致しない。

このように定義を修正すると、例えば、

Nat : (*->*)->(*->*)->*
Nat = λF,G:*->*. ΠX:*. FX->GX

の Conformity Relation は以下のようになり、種がきちんと一致する。

• <Nat> : (|Nat|)
• (|Nat|) =
  ΠF1,F2:*→*, FR:(ΠX1,X2:*. (X1→X2→*) → (F1 X1 → F2 X2 → *) ).
  ΠG1,G2:*→*, GR:(ΠX1,X2:*. (X1→X2→*) → (F1 X1 → F2 X2 → *) ).
  (Nat F1 G1) → (Nat F2 G2) → *
• <Nat> =
  λF1,F2:*→*, FR:(ΠX1,X2:*. (X1→X2→*) → (F1 X1 → F2 X2 → *) ).
  λG1,G2:*→*, GR:(ΠX1,X2:*. (X1→X2→*) → (G1 X1 → G2 X2 → *) ).
  λα1:Nat F1 G1, α2:Nat F2 G2.
  ∀X1,X2:*, XR:X1→X2→*.
  ∀x1:F1 X1, x2:F2 X2.
  FR X1 X2 XR x1 x2 → GR X1 X2 XR (α1 X1 x1) (α2 X2 x2)

λ. 実写版エヴァンゲリオン？

をぐまさんのmixi日記より。良くできてるなぁ。

• <URL:http://www.youtube.com/watch?v=75GoCvuB8Ow>
• <URL:http://www.youtube.com/watch?v=mRB2woVxcQ4>

λ. A note on inconsistencies caused by fixpoints in a cartesian closed category by H. Huwig and A. Poigné

以前に不動点と有限直和を持つCCCというエントリで「取り寄せるのが面倒」とか書いたが、SFCのメディアセンタにもちゃんとあった。そのエントリでは始対象と不動点を持つCCCは縮退しているということを書いたが、それだけでなくほかにも色々言っている。

• Let C be a cartesian closed category with fixpoints and an initial object. Then C is inconsistent.
• Let C be a cartesian closed category with fixpoints and coproducts. Then C is inconsistent.
• Let C be a cartesian closed category with fixpoints and with a NNO. Then C is inconsistent.
• Let C be a bicartesian closed category with and object D such that [D⇒2] is a retract of D. Then C is an order category with D ≅ 1.

inconsistentな圏というのは全てのオブジェクトが同型な圏。order category は、どのオブジェクトの間にも射が高々1つしか存在しない圏のこと。

Carl Gunter の profinite domains とSFPの話については後で調べる。

λ. コンマ圏と極限錘

図式 F: D→C の錘の圏は、F を 1→C^D の関手と考え、Δ:C→C^D を対角関手とすると、コンマ圏 (Δ↓F) になっている。この圏の終対象が極限錘。まあ当たり前の事実なんだけど、コンマ圏(comma category)って案外便利だなぁと思った。

λ. GTD (Getting Things Done) を試す

池上さんが最近紹介していたこともあり、GTDが気になっていたので、試してみることにした。まずは池上さんも紹介していたHoriさんの記事を読んだ。それから、とりあえずたださんの記録を参考にRTMのアカウントを取得し、タスクを適当に登録してみる。GTD Style Wikiというのも便利そうだ。

λ. 第二十三回圏論勉強会

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

問題が結構難しい。

Exercise 3 (p.343):

直観的には明らかだけど、どう示せばよいのかな。

Exercise 4 (p.343):

を可換にする g: T→Y×Y が与えられたとき、φ_X が characteristic map であることから、ある h: T→X が存在して、

ここで、X→Y×Yはsymmetricなので、


となり、条件を満たす射 σ ∘ h が存在するので、φ_X ∘ s も X→Y×Y の characteristic map である。 characteristic map は一意なので φ_X = φ_X ∘ s。カリー化して、curry(φ_X) = curry(φ_X ∘ s) : Y→Ω^Y 。

λ. FreeMind

MindMapは存在は知っていたが、これまで試したことはなかった。 しかし、先週の「伊藤洋一のRound Up World Now!」でFreeMindというツールが紹介されていたので、いい機会と思って試してみることにする。

参考:

• FreeMind活用クラブ - マインドマップをフリーソフトで

λ. Haskell Bowling by Ron Jeffries

<URL:http://d.hatena.ne.jp/machi_pon/20061104> より。 実はこれまでボーリングのスコアの定義を知らなかったのだけど、こういう風に定義されているのか。

λ. 強い直和?

強い直和(strong sum)とCCに関して混乱中。

強い直和と弱い直和

以下の推論規則からなる型を「強い直和」と呼ぶ。

Γ, a : A ├ B : *
──────────
Γ ├ (Σa:A. B) : *

Γ ├ t : A   Γ ├ u : B[a := t]
─────────────────
Γ ├ (t,u) : Σa:A. B

Γ ├ t : (Σa:A. B)
───────────
Γ ├ fst t : A

Γ ├ t : (Σa:A. B)
──────────────
Γ ├ snd t : B[a := fst t]

それに対して、この推論規則の最後の二つを以下の推論規則で置き換えたものを「弱い直和」と呼ぶ。

Γ ├ t : (Σa:A. B)  Γ ├ C : *  Γ ├ e : (Πa:A. B→C)
─────────────────────────────
Γ ├ elimSum t e : C

CCと強い直和

CCには強い直和は含まれないが、弱い直和は以下のようにCC内で定義できる。

Σa:A. B = ΠX:*. (Πa:A. B → X) → X
(t,u) = λX:*. λe:(Πa:A. B → X). e t u
elimSum t e = t C e

そして、CCに強い直和を追加するとGiraldの逆説が成り立つことになっている。

が

しかし、強い直和も以下のようにCC内で定義できる気が……間違っているのはどこだ?

fst t = t A (λa:A. λb:B. a)
snd t = t ((λa:A. B) (fst t)) (λa:A. λb:B. b)

まとめ

sumiiさんの指摘でようやく理解できたが、(λa:A. λb:B. b) の型付けに問題があるのが原因だった。実際、Agdaで以下のように書いてみても、最後のゴールがrefine出来ない。AgdaはCCのようなimpredicativeな言語ではないけど、この例が型付けできないことを示すには十分だろう。

Sum :: (A::Set) -> (A->Set) -> Type
Sum A B = (X::Set) -> ((a::A) -> B a -> X) -> X

pair (|A::Set) (|B::A->Set) :: (a::A) -> B a -> Sum A B
pair a b = \(X::Set) -> \(f::(a'::A) -> B a' -> X) -> f a b

elimSum (|A::Set) (|B::A->Set) (|X::Set)
    :: Sum A B -> ((a::A) -> B a -> X) -> X
elimSum t f = t X f

fst (|A::Set) (|B::A->Set) :: Sum A B -> A
fst t = t A (\(a::A) -> \(b::B a) -> a)

snd (|A::Set) (|B::A->Set) :: (t::Sum A B) -> B (fst t)
snd t = t (B (fst t)) (\(a::A) -> \(b::B a) -> {! b !})

ちなみに、The Theory of Parametricity in Lambda Cube でも同じ間違いをしていた。

関連

• ECC, an Extended Calculus of Constructions - ECCはCCを拡張して強い直和を導入した型理論

λ. 『隣の家の少女』　ジャック・ケッチャム(Jack Ketchum)

を読んだ。

λ. 聖諦

バイト先で「聖諦」の意味を質問されて困ってしまった。太宰治の『お伽草子』の「浦島さん」を題材にした教材だったのだが……

参考

• 四諦 - Wikipedia
• 四聖諦 - Memorandum of Experiments | Shojiro Nomura Blog チベット仏教研究日誌

λ. Indexed types families in GHC

GHCの開発版には既に associated data type が実装されていたのね。 試してみよう。

λ. 『小さな政府を問い直す』 岩田 規久男

を読んだ。「機会の平等 vs. 結果の平等」や「小さな政府 vs. 大きな政府」といった問題を論じるための、経済学の標準的な「見方」を教えてくれる良書。

λ. MAD PEOPLE β01: EPISODE 1066 「不沈艦ケイト vs. 奇跡の連携」

<URL:http://straws.sakura.ne.jp/madb01/index.cgi?bid=1066>

衝動的に参加してしまった。EPISODE 1007 以来の久しぶりに参加だったので、結構ついていくのが大変で、特に状況を評価することに苦しんだ。

(後で書く)

他の方の感想など

• ナンシー(i-saintさん)

λ. 雑記

病院へ祖父を見舞う。

λ. 腰リール

腰リールを作ってみた。 リールは有隣堂にあった Dr.ion のマルチストラップ リールホルダー (165DRBK-1200)。ペンポッドとプチモと安物の単語カードを装着。このリールは耐荷重が約30gしかなく巻取りのパワーが足らない感じ。

【追記】 ……と書いたが、結局プチモは外してしまったこともあり、巻取りのパワーは全然問題なかった。

λ. ラップトップの新しいバッテリー

これまで使っていたバッテリーが寿命っぽかったので、11/08にヨドバシ.comで新しいバッテリーを注文していたのだが、これがようやく届いた。店頭には在庫があっても通販用には在庫がなかったので時間がかかってしまった。在庫が分かれているのはユーザーにとっては不便なだけだが、会計上の都合だろうか?

<URL:http://win-nie.net/> や <URL:http://www.batterymart.jp/> 等でやっているバッテリーのセルの交換の方が安かったのだけど、交換するために送っている間はバッテリーが使えないのが嫌で今回は新品を買ってしまった。次にバッテリーがダメになったらこれらを利用するかも。まあ、それまでにラップトップ自体を買い替えているだろうけど。

λ. 人間は判断材料が揃う後半になるほど深く考え、理由付けが強くなる傾向がある

i-saintさんのmixi日記より。なるほどと思ったのでメモ。 人狼BBS:D D188 日の沈まぬ村 5日目 少女 リーザ 午後 5時 48分。

人間は判断材料が揃う後半になるほど深く考え、理由付けが強くなる傾向がある。少なくとも弱くなることはほとんどない。逆に、常に理由をでっちあげる必要がある人狼は、理由漬けが弱くなって行ったり、強弱の変化が激しかったりする傾向がある。

そして能力者の真贋、状況からの考察、これらは人狼視点でも言うに難くないのだよな。事前に全てを知っているのだから。

人狼BBS まとめサイト - 村人・狼要素考察-peppy でも取り上げられている。

λ. Reading Notes: Why is Cpo Cocomplete? by Jean Goubault-Larrecq

をざっと読んだ。ここで言っているCpoは directed-join の定義されている半順序集合でボトムがあるとは限らない。で、Cpoと連続関数からなる圏が余完備であることを示すのに必要なもののうち、直和(coproduct)は自明だけど、余等化子(coequalizer)は自明ではないので、余等化子の構成を詳しく説明している。余等化子の構成が面白かったので図を載せておく。

• 半順序集合と単調関数の圏Ord
• OrdとCpoとの随伴 F ┤ |_|
• Ordでの |f|, |g| の余等化子 i: |B|→C
• F(i)∘η_B の Epi-Mono factorization (e,m)
• eがf,gの余等化子

λ. Agate—an Agda-to-Haskell compiler by Hiroyuki Ozaki, Makoto Takeyama and Yoshiki Kinoshita

を読んだ。型システムの違いをどう吸収するのかを期待していたら、untypedなものに変換してしまっていた。変換はHOASに基づいたstraightforwardなもの。AgateでHaskellに変換してGHCでコンパイルしたものは、GHCで直接コンパイルしたものに比べて、2倍〜6倍の実行時間。

• Agate

λ. 今日のITシステム

• SVG関係で研究になりそうなことはあるか?
• 太田メソッド「スライドがないなら、発表しながら作れば良いじゃない」
• Bloom filter
  • <URL:http://chasen.org/~taku/blog/archives/2006/01/bloom_filter_1.html>
  • <URL:http://dev.ariel-networks.com/modules/xfsection/article.php?articleid=18>

λ. 『The Code Book』 by Simon Singh

を読了。

次は何を読もうか。『Big Bang: The Origin of the Universe』は500ページ以上あるのでちょっと分量が多すぎるし……

λ. るびま 0017 号

Rubyist Hotlinks で青木さんが「名前から実体を作るのはよろしくない」「名前になんかすると実物が存在するようになるというのは (Ruby 哲学的に) 許せん。名前はあくまでもすでに存在するモノにつけるべきでしょ。少なくともプログラミングでは、モノが先にあってそれに名前を付けるという順番を維持すべき」と言っているのが興味深かった。

そういえば、RubyConf2006のMP3ファイルとかって、どこかで公開されてないのかなぁ。

λ. MARIPPY

おお、懐かしい。