2002-03-04
λ. Gimp-Ruby 0.7.0
一息つきたかったので出してしまったり。
gettext周りでちょっと悩んでいるのでmingw用のバイナリは用意してないです。
次から、mingw用のバイナリのアーカイブにはtar+bzip2じゃなくてzipを使おっと。
λ. 夢
どっかの大学祭でエッチな映画をみる夢。やたら立体的な構成のキャンパスで疲れた。でも、あちこちにあった噴水が、光を反射してて綺麗だった。
λ. categories
Conceptual Mathematics の最初の60ページほどを読んだ。確かにこれは勉強会の教科書として使うには簡単すぎるな。この本は春休み中に読み終えて、春学期には Mac Lane の方のやつで勉強したいところ。
ふむ、permutationの圏か。
λ. アクトレイザー2
bofの曲を聴いてたら、アクトレイザー2のも聴きたくなってきた。googleでMIDIを探してみたけど、アクトレイザー1のはあっても2のは無いなぁ。やっぱ2はマイナなんだねぇ。僕は2の方が断然好きだけど。
と、ESAF official Homepageというところで、SPCという形式のファイルを見つけた。
とりあえず、そこで勧められていたKBmediaPlayerで試しに聴いてみる。うーん、これも懐かしいなぁ。
XMMSのプラグインもあるようで、ちょっといじってみようかな。
2003-03-04
λ. TODOを一個ずつ片ずけていこう...
λ. gtk2 for cygwin
gtk+-2.2.1がこれまでx11でうまく動作していなかったのだけど、新PCでコンパイルしなおしたら直ってしまった。
それから、わたなべさんの所を真似してsetup.iniを作ってみたので、http://web.sfc.keio.ac.jp/~sakai/cygwin/ を"Other URL"に指定することで、setup.exeからインストールする事が出来るようになった(はず)。わたなべさん、ありがとうございました。
ついでに、送ってなかったx11関係のパッチを送ってしまう。#107623
λ. functor category とデータ型
「data GRose f a = GBranch a (f (GRose f a))」のGRoseを Funct(C,C) × C -> C の functor と考えれば、射の写像mapGRoseの型は「∀f g. (∀a. f a -> g a) -> (b -> c) -> (GRose f b -> GRose g c」であると考えられる。しかし、Generic Haskell は違っていて「∀ f g. (∀a b. (a -> b) -> (f a -> g b)) -> (c -> d) -> (GRose f c -> GRose g d」という型の関数を考えるらしい。うーみゅ。
λ. Ruby/FFCall
2/19の [ruby-ext:02156] ruby-dl with ffcall は少なくとも当面は取り込まれることはなさそうなので、とりあえずは独立した拡張ライブラリにしておこう。[ruby-ext:2165]
2004-03-04
λ. 借りた本
- 『アリソン』
- 時雨沢恵一[著] 黒星紅白[イラスト]
- 『クリスティーン 上』
- スティーヴン キング (Stephen King) [著], 深町 眞理子 [訳]
- 小説すばる 2003年8月号
- -
- 『ホーキングとペンローズが語る時空の本質—ブラックホールから量子宇宙論へ』
- スティーヴン・ホーキング(Stephen Hawking), ロジャー・ペンローズ(Roger Penrose) [著], 林 一 [訳]
- 『ホロコーストの真実 上』
- デボラ・E・リップシュタット(Deborah E. Lipstadt)[著] 滝川 義人 [訳]
2005-03-04
λ. 情報理論勉強会＠古川研
テキストは 『情報理論の基礎 — 情報と学習の直観的理解のために —』, 村田 昇 。難い。
λ. ∀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)。
*1 正確に書くなら ∏A: (∏n: N. *). A(zero) → (∏n: N. A(n)→A(succ(n))) → ∏n: N. A(n)
2009-03-04
λ. IDPで数独を解く
数独をParadoxとDarwinとMaceで解いてみたので、ついでにIDPでも試してみた*1。
- 入力ファイル sudoku-idp.idp
- ログ sudoku-idp.txt
IDPの特徴は帰納的定義が出来ることのようだ(普通の一階述語論理では帰納的な定義は出来ない)。 具体的には { R(t1,…,tn) <- 論理式. } 等と書けて、論理式の中でRを使うことで、関係Rを帰納的に定義出来る。 帰納的定義が出来るということは、例えば推移閉包を公理化出来るので、グラフが関係してくるようなパズルを解くのには向いていそうだ。
あと、記述言語では例によって、感嘆符「!」と疑問符「?」がそれぞれ全称量化子と存在量化子として用いられている。
*1 同じネタをひっぱり過ぎ
