トップ «前の日(03-03) 最新 次の日(03-05)» 追記

日々の流転


2002-03-04

λ. Gimp-Ruby 0.7.0

一息つきたかったので出してしまったり。

gettext周りでちょっと悩んでいるのでmingw用のバイナリは用意してないです。

次から、mingw用のバイナリのアーカイブにはtar+bzip2じゃなくてzipを使おっと。

Tags: gimp ruby

λ.

どっかの大学祭でエッチな映画をみる夢。やたら立体的な構成のキャンパスで疲れた。でも、あちこちにあった噴水が、光を反射してて綺麗だった。

λ. categories

Conceptual Mathematics の最初の60ページほどを読んだ。確かにこれは勉強会の教科書として使うには簡単すぎるな。この本は春休み中に読み終えて、春学期には Mac Lane の方のやつで勉強したいところ。

ふむ、permutationの圏か。

Tags: 圏論

λ. アクトレイザー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

Tags: cygwin

λ. 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」という型の関数を考えるらしい。うーみゅ。

λ. Sodipodi for Windows

Sodipodiがバージョン 0.29 からWindowsに対応したそうだ。GIMP掲示板より。

λ. Ruby/FFCall

2/19[ruby-ext:02156] ruby-dl with ffcall は少なくとも当面は取り込まれることはなさそうなので、とりあえずは独立した拡張ライブラリにしておこう。[ruby-ext:2165]

Tags: ruby

2004-03-04

λ. 借りた本

『アリソン』
時雨沢恵一[著] 黒星紅白[イラスト]
『クリスティーン 上』
スティーヴン キング (Stephen King) [著], 深町 眞理子 [訳]
小説すばる 2003年8月号
-
『ホーキングとペンローズが語る時空の本質—ブラックホールから量子宇宙論へ』
スティーヴン・ホーキング(Stephen Hawking), ロジャー・ペンローズ(Roger Penrose) [著], 林 一 [訳]
『ホロコーストの真実 上』
デボラ・E・リップシュタット(Deborah E. Lipstadt)[著] 滝川 義人 [訳]
Tags:

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で数独を解く

数独をParadoxDarwinMaceで解いてみたので、ついでにIDPでも試してみた*1

IDPの特徴は帰納的定義が出来ることのようだ(普通の一階述語論理では帰納的な定義は出来ない)。 具体的には { R(t1,…,tn) <- 論理式. } 等と書けて、論理式の中でRを使うことで、関係Rを帰納的に定義出来る。 帰納的定義が出来るということは、例えば推移閉包を公理化出来るので、グラフが関係してくるようなパズルを解くのには向いていそうだ。

あと、記述言語では例によって、感嘆符「!」と疑問符「?」がそれぞれ全称量化子と存在量化子として用いられている。

*1 同じネタをひっぱり過ぎ