2001-10-31
λ. 日の出
- 6:12:58
- 6:13:00
- 6:16:20
λ. 弔いの哲学
こないだ借りて読んだんだけど、僕にはかなり難しかった。残念だけど10分の1も理解できてないと思う。とりあえず、「弔いは、誰かの死と私の生の断絶を思い知ることである」という事、それから「戒律を宗教制度の下から解き放つこと、言いかえれば、戒律を無神論者が哲学的に考え抜くこと、このことが、殺された者の弔いと殺した者の贖罪の道を指し示すはずである」という一文は印象的だった。そのうちまた読んでみたい。
λ. EXTERN
というわけで試してみたら、EXTERN無しで宣言されているシンボルもちゃんとexportされてるみたい。gccのオプションなのかな。まあ、それはそうとして、拡張ライブラリ側はやっぱりEXTERN付きで宣言する必要があるんだけどね。
λ. つーわけで、Gimp-Rubyの方もruby_errinfoを使うように書き換えてみたり。rb_protect内でrb_rescue2を使う嫌らしいコードが無くなったので、気分が良い。
λ. Amaya
gtk+版はこないだコンパイルできることを確かめたので、今度はMotif版をLesstifを使ってコンパイルしてみた。で、動かそうとしたら早速落ちた。やれやれ、まだ殆どコードをいじってないというのに……先が思いやられる。
Program received signal SIGSEGV, Segmentation fault.
__XmStringSegmentExtent (flist=0x874a740, comp=0x874a7c8, width=0xbfffc564,
height=0xbfffc566, ascent=0xbfffc568, descent=0xbfffc56a) at XmString.c:946
946 XmString.c: No such file or directory.
in XmString.c
(gdb) bt
#0 __XmStringSegmentExtent (flist=0x874a740, comp=0x874a7c8,
width=0xbfffc564, height=0xbfffc566, ascent=0xbfffc568, descent=0xbfffc56a)
at XmString.c:946
#1 0x40110af2 in _XmStringExtent (fontlist=0x874a740, string=0x874a760,
width=0x874a5b0, height=0x874a5b2) at XmString.c:1808
#2 0x400953ca in _XmCalcLabelDimensions (w=0x874a4b0) at Label.c:1799
#3 0x40093985 in initialize (request=0xbfffc890, new_w=0x874a4b0,
args=0xbfffcff0, num_args=0xbfffc730) at Label.c:674
#4 0x401a9994 in XtAppCreateShell () at eval.c:88
#5 0x401a8bc0 in XtInitializeWidgetClass () at eval.c:88
#6 0x401a90e6 in _XtCreateWidget () at eval.c:88
#7 0x401a96e4 in XtCreateWidget () at eval.c:88
#8 0x4005c606 in XmCreateCascadeButton (parent=0x8749a48,
name=0x86d4400 "File", arglist=0xbfffcff0, argcount=6) at CascadeB.c:1355
#9 0x0816a28a in MakeFrame () at eval.c:88
#10 0x08185ba0 in OpenCreatedView () at eval.c:88
#11 0x081b999a in TtaOpenMainView () at eval.c:88
#12 0x08080bd6 in InitDocView () at eval.c:88
#13 0x080842f6 in GetHTMLDocument () at eval.c:88
#14 0x08084a9a in CallbackDialogue () at eval.c:88
#15 0x08080889 in GoToHome () at eval.c:88
#16 0x08086b23 in InitAmaya () at eval.c:88
#17 0x08166dea in CallAction () at eval.c:88
#18 0x08166ef5 in CallEventType () at eval.c:88
#19 0x0817c7f1 in TtaMainLoop () at eval.c:88
#20 0x080506ca in main () at eval.c:88
#21 0x403601be in __libc_start_main (main=0x804d770 <main>, argc=1,
ubp_av=0xbffff82c, init=0x804c2c4 <_init>, fini=0x81fbef0 <_fini>,
rtld_fini=0x4000ddf0 <_dl_fini>, stack_end=0xbffff81c)
at ../sysdeps/generic/libc-start.c:129
2002-10-31
λ. 言語の意味論のレポートのアイディアを考えて夜更かし。でも、徹夜してしまうと今晩頑張れないので4時くらいには寝ることに。
λ. 寝坊、しかも腹いてー
λ. ミクロ経済Ⅱ
つうわけで遅刻。あぁ、パレート効率の話ね。ということは、ようやく厚生経済学の第一定理か。
λ. 予算編成論
.
λ. 認知科学
少し前に紹介されていたビデオで「臓器移植を受けた患者の性格や好みがドナーのものに近くなる」という話がちょこっと出てきていたけど、それって、『内臓が生みだす心』の話だったのかしら。(黒木のなんでも掲示板(0079)より)
λ. 萩野服部研
少なくともlinuxのfile_operations構造体にはopenがあるのですが……、VFSという言葉の指している部分に関して僕の理解が間違ってる?
それから、linuxにはvnodeって無いんだよなぁ。
ypって「Yellow Page」のacronymなのね。知らなかった……
2003-10-31
λ. 集合クラス
既にset.rbが標準で配布されてるし原さんのfinite-set.rbもあるのに何をいまさらと思われるかもしれないけど、ふと集合クラスを書いてみたくなった。どうせなので、AFAを満たすようにしてみる。とりあえず簡単なコードは動くようになった。
a = Variable.new
b = Variable.new
# 等式系
# a = {a}
# の解(Quine atom)を求める
atom = Set.solve(a => Set[a])[a]
assert_equal(atom, Set[atom])
assert(atom.member?(atom))
# 等式系
# a = {0, b}
# b = {b, 0}
# の解を求める
set1 = Set.solve(a => Set[0, b], b => Set[b, 0])[a]
# 等式系
# a = {0, a}
# の解を求める
set2 = Set.solve(a => Set[0, a])[a]
assert_equal(set1, set2)
λ. 100の質問
そういえば、こないだ読んだ筒井康隆の『文学部唯野教授のサブテキスト』に「文学部唯野教授に100の質問」というのがあって思ったのだけど「100の質問」って誰が最初に考えたのだろう?
気になって気になって、夜も眠れません。
2004-10-31
λ. A155 幻の村
に参加していましたが、ようやく決着が付きました。残念ながら私は途中で死んでしまい、あまり勝負に貢献することは出来なかったのですが、結果としては勝利でした。詳しい感想は忘れないうちにちゃんと書いておきたいなぁ……。
2005-10-31
λ. [ruby-dev:27596]
そういや、Numeric#quo ってなんだか認知度が低いような気がする。 なんでだろ。
2006-10-31
λ. CPO圏で始代数が存在しないための条件
CPO圏CとCPO関手F:C→Cを考える。 もしCに非正格な t:1→E と自然変換 ε: F→Id が存在するならば、 Fの始代数は存在しない。
証明
任意の e: 1→E と φ: FX→X とについて、 (e o !) : X→E は φ: FX→X から ε_E: FE→E への準同型になっていることがわかる。
![\xymatrix{ FX \ar[r]^{F!} \ar[d]_\varphi & F1 \ar[r]^{Fe} \ar[d]|{! = \varepsilon_1} & FE \ar[d]^{\varepsilon_E}\\ X \ar[r]_{!} & 1 \ar[r]_e & E \\ }](tex/4b5356cdef3c5bf6692c9efb6f2714fb.png "\xymatrix{ FX \ar[r]^{F!} \ar[d]_\varphi & F1 \ar[r]^{Fe} \ar[d]|{! = \varepsilon_1} & FE \ar[d]^{\varepsilon_E}\\ X \ar[r]_{!} & 1 \ar[r]_e & E \\ }")
ここで t:1→E は非正格なので、少なくとも二つの異なる準同型が存在する。
- t o ! = t o ⊥_{X→1} ≠ ⊥_{X→E}
- ⊥_{1→E} o ! = ⊥_{X→E}
よって、φは始代数では有り得ない。
具体例
- Fがcomonadの場合
- 直積 F(X) = A×X
- 恒等関手 Id
- ストリーム Stream(A) = νX. A×X
- (constant) exponential functor F(X) = A⇒X
- a: 1→A を適当に選べば、自然変換 ev o <id_{A⇒X}, a o !> : FX→X が得られるので、条件を満たす。
疑問
これは十分条件だけど、この方向で必要十分条件は存在するか?
適用例 (1)
Haskellでは以下のような product comonad を考えることがある。
class Functor w => Comonad w where extract :: w a -> a duplicate :: w a -> w (w a) extend :: (w a -> b) -> (w a -> w b) extend f = fmap f . duplicate duplicate = extend id instance Comonad ((,) a) where extract (c,x) = x duplicate (c,x) = (c,(c,x))
もし (A,B) を厳密に(A×B)_⊥と解釈すると、以前の議論から F(X) = (A×X)_⊥ には始代数が存在し、背理法により extract :: (a,x) -> x は自然変換ではないことになる。したがって、この場合には厳密にはcomonadになっていない。
適用例 (2)
Akihito Takano と Erik Meijer の Short-cut deforestation in Calculational Form では F代数を正格な FA→A と定義していて、始代数が存在すると言っているが、これは誤り。代数を正格に制限しても、準同型は正格なものに制限されていないので、前述のような関手に対しては始代数が存在しない。
しかし、Erik Meijer は Program Calculation Properties of Continuous Algebras では準同型も正格なものに制限してたはずなのに、この論文ではどうしてやめたんだろうね。
λ. 多相関数≠自然変換
多相関数が自然変換にならないことがあるというのは、漠然と知ってはいたけど、実際に直面してみると嫌らしいな。以前は yoriyukiさんの「Haskellは複雑すぎる気がする」という意見に同意できなかったけど、今なら完全に同意出来るよ(苦笑)
λ. 自然変換 ε: F→Id の性質
幾つかメモ。
ε_X: FX→X は正格
![\xymatrix{ F1 \ar[r]^{F\bot} \ar[d]|{! = \varepsilon_1} & FX \ar[d]^{\varepsilon_X}\\ 1 \ar[r]_{\bot} & X \\ }](tex/d686f17d9d11e0fd60c3e293579bfdc5.png "\xymatrix{ F1 \ar[r]^{F\bot} \ar[d]|{! = \varepsilon_1} & FX \ar[d]^{\varepsilon_X}\\ 1 \ar[r]_{\bot} & X \\ }")
⇒ (⊥ o !) is strict ⇔ (ε_X o F⊥) is strict ⇒ ε_X is strict
したがって、任意のXについて ε_X は正格。
F は非正格性を保存
f: X→Yとする。
![\xymatrix{ FX \ar[r]^{Ff} \ar[d]_{\varepsilon_X} & FY \ar[d]^{\varepsilon_Y}\\ X \ar[r]_{f} & Y \\ }](tex/15e27fea188532a9e3ee7abf17940c00.png "\xymatrix{ FX \ar[r]^{Ff} \ar[d]_{\varepsilon_X} & FY \ar[d]^{\varepsilon_Y}\\ X \ar[r]_{f} & Y \\ }")
Ff is strict ⇒ (ε_Y o Ff) is strict ⇔ (f o ε_X) is strict ⇒ f is strict
対偶をとって「f is not strict ⇒ Ff is not strict」。
λ. CPO圏での自然変換の性質
上記の ε: F→Id についての話はもう少し一般化できるか。
α: F→G を自然変換とする。
正格性
![\xymatrix{ FX \ar[r]^{F\bot} \ar[d]_{\alpha_X} & FY \ar[d]^{\alpha_Y}\\ GX \ar[r]_{G\bot} & GY \\ }](tex/ff5e61441eeedbd81a486754b0c73c97.png "\xymatrix{ FX \ar[r]^{F\bot} \ar[d]_{\alpha_X} & FY \ar[d]^{\alpha_Y}\\ GX \ar[r]_{G\bot} & GY \\ }")
α_X is strict ⇒ G⊥ o α_X is strict ⇔ α_Y o F⊥ is strict ⇒ α_Y is strict
よって「任意のXについて α_X は正格」もしくは「任意のXについて α_X は非正格」。
αとFfがstrictならGfも正格
![\xymatrix{ FX \ar[r]^{Ff} \ar[d]_{\alpha_X} & FY \ar[d]^{\alpha_Y}\\ GX \ar[r]_{Gf} & GY \\ }](tex/e8fab3794bb2847acda93afadcc3ca77.png "\xymatrix{ FX \ar[r]^{Ff} \ar[d]_{\alpha_X} & FY \ar[d]^{\alpha_Y}\\ GX \ar[r]_{Gf} & GY \\ }")
αが正格だとする。
Ff is strict ⇒ α_Y o Ff is strict ⇔ Gf o α_X is strict ⇒ Gf is strict
2007-10-31
2009-10-31
λ. 数学基礎論講演会 「ゲーデルの不完全性定理」
- 講師
- 田中 一之 （東北大学大学院理学研究科数学専攻教授）
- 題目
- ゲーデルの不完全性定理
- 内容
- ゲーデルの定理はどこまで自己言及的か？ 本質的決定不能性と証明の加速性，新しい独立証明など，ゲーデル以降の発展のポイントを概観すると共に，この定理の誤用例など負の部分にも触れる．
6月にあった田中一之先生の講演「数学基礎論の考え方・学び方」の盛況を受けて第二弾が企画されていたので、参加してきた。 ゲーデルの不完全性定理なんて、いまさらなテーマのように思えたけど、後半のΣ無矛盾性やゴールドバッハ予想に関する話は「おおっ、そうなのか」と思った。
ゴールドバッハ予想はΠ1文なので、無矛盾な体系でゴールドバッハ予想が証明できればそれは(標準モデルで)真。一方で、ゴールドバッハ予想の否定の証明から(標準モデルで)偽であることを導くには、Σ健全性が必要。 さらに、双子素数予想はΠ2文なので、証明されたときにそれが真であることを主張するには、公理系にさらに強い要請が必要となる。
本質的決定不能性や加速定理についても、考えたことがなかった話なので、非常に新鮮だった。ヘンキン文とLöbの定理については、この日記でも以前に ヘンキン文 - ヒビルテ(2007-09-16) で少し取り上げたけど、Löbの定理の系として第二不完全性定理を導出できるというのも、気づいておらず「おおー」と思った。
主な参考文献として以下の3つが挙げられていた。
- Feferman他編 Kurt Gödel Collected Works, Vol.1, Oxford University Press, 1986
-
<URL:http://books.google.co.jp/books?id=5ya4A0w62skC> - 田中一之編 『ゲーデルと20世紀の論理学』 全4巻 東大出版会, 2006-7.
-
- Torkel Franzén 著 (邦訳書来年出版) Gödel's Theorem: An Incomplete Guide to Its Use and Abuse, A K Peters, 2005.
-
<URL:http://books.google.co.jp/books?id=71pK8Zz9Dd8C>
なお、次回は2010年5月ごろに「不完全性定理 その後」というテーマで予定しているとのこと。「ランダムネスと不完全性定理」「クリプキの別証明」「パリス・ハーリントンの独立命題」ということで、また面白そうだ。
終了後に、かがみさんの紹介で igarisさんにお会いしたのだけど、僕はすぐに Real World Haskell 読書会の方に移動してしまったので、あまりお話できずに残念だった。 あと、下の写真は帰りにキャンパス内で見かけたもの。
![[年齢∝時間。価値＝f(時間)、fは、キミだ。By ほ、ほーっ、ホアアーッ!!さん 心はいつまでも永遠の二十歳です。By 生涯一学徒さん]](./images/20091031_2.jpg)
関連
λ. Real World Haskell読書会 2009-10
前回の読書会が8月で、9月はお休みだったので2ヶ月ぶり。
前回、7章「入出力」の7.2「ファイルおよびハンドルを使う」まで読んでいたので、今日は多分7.3「規模の大きい例：関数的入出力と一時ファイル」から7章の残りと、8章「効率的なファイル処理、正規表現、ファイル名マッチング」。
- Chapter 7. Input and output (原著オンライン版)
- Chapter 8. Efficient file processing, regular expressions, and file name matching (原著オンライン版)
といっても、上記の講演会が終わってから移動したので、付いたときには既に8章の半ばまで進んでいて、最後の方しか参加できなかったのだけど(苦笑。
それから、Real World Haskell がついに出版ということで、オライリーの動物カレンダーつきで献本して頂いてしまった。
読書会には参加していたもののあまりフィードバック出来ていなかったので、ちょっと申し訳なくもあるのだけど、ありがとうございました。
![[Real World Haskell とオライリーの動物カレンダー]](./images/20091031_3.jpg)
以下いろいろ
末尾再帰的でない (++) :: [a] -> [a] -> [a] の定義が「なぜ問題ないのか?」「なぜ固定空間で評価できるのか?」について、個人的には違和感をまったく感じなくなってしまっていたのだけど、他の参加者にとってはそうでもなかったみたいだった。
それと、「このような形の関数に何か名前がなかったっけ?」という話があったが分からず。個人的に思い浮かぶのは「余帰納法(coinduction)」、「余再帰(corecursion)」、「anamorphism」とかだけど、これらは多分違うよなぁ……
System.FilePath が (</>) :: FilePath -> FilePath -> FilePath という演算子を提供していて、パスの連結を "foo" </> "bar" のように書けることに感心した。
これは記号の使い方がうまい。
それから、The Typeclassopedia 日本語訳 の話で盛り上がるなどしたが、私は未読なのでちょっと疎外感を感じるなどする(笑。それに関係してかどうかは分からないけど、Real World Haskell の16章「Parsecを使う」でなぜApplicativeを使うのかという話があった。 Real World Haskell って既存の便利な関数はできる限り使う主義みたい(たとえば、前回もArrowをちゃんと紹介せずにsecondだけ使ってみたりしてたし)なので、単に便利な関数として使っているだけではないかという気がする。
ただ、モナドはパーサーの記述には提供されている演算が強力すぎるので、パーサコンビネータの実装側としては、より制限された演算しか持たないApplicativeを抽象化として用いるのは、あり得る選択肢と思う。 John Hughes が Generalising Monads to Arrows でArrowを導入した際にも、モナドベースのパーサライブラリでは Swierstra and Duponcheel のテクニックが利用できないがArrowベースなら利用できるという例が挙げられていたので。
それから、Traversableについては The Essense of the Iterator Pattern がまとまった資料だと思う。
ψ maoe [最近ちょうどhaskell-cafeでこの話題を見かけました。corecursionであっているようです。 http..]
ψ さかい [おお。末尾再帰と対比されるような概念だろうから違うと思ってたのですが、corecursionで良かったのですね。 あ..]
ψ maoe [http://www.haskell.org/haskellwiki/Tail_recursionを見るとguard..]
ψ さかい [coinduction/corecursionはどちらかというと意味論的な性質で、guarded recursion..]
ψ maoe [なるほど。ありがとうございます。]
