トップ «前の日(08-11) 最新 次の日(08-13)» 追記

日々の流転


2001-08-12

λ. 朝方の生活に戻したと思ったら、眠れなくて、寝たのが朝の9時ごろ。で、起きたのが夜の7時。だめだこりゃ。明日こそは早起きして「猿の惑星」見るぞ。

λ. NArrayの次元順序

現在のFORTRANスタイルだと、例えばGimpで扱っているようなメモリ形式の画像データで、RGBを次元として扱う場合に、こんな風に書くことになるのか。…微妙。

Tags: ruby
  img = NArray.byte(bpp, width, height)
  img[0, x, y] # R
  img[1, x, y] # G
  img[2, x, y] # B

λ. Gimp-Ruby

libgimpってまずいことがあると内部で勝手にgimp_quit()内でexit(0)しちゃうからRuby側でどう対処すべきか悩んでた。結局、PLUG_IN_INFO.quit_procが、gimp_close時に呼ばれるので、そこでruby_finalizeする事にした。したがって、Gimp::mainは帰って来なくしちゃった。えへっ。なんか不味いような気もするが、exit!の例もあるからまあいっか。というわけで今後は終了処理にはensureぢゃなくてat_exitを使ってくれたまえ。

Tags: gimp ruby

λ. とか思って安心してたらSegmentation Faultだ。なんじゃこりゃ? gimphelpuiが内部で持ってるtooltipsウィジェットがどっかで既に破壊されてるのか? しかし、一体どこで?

Gtk-WARNING **: invalid cast from `(unknown)' to `GtkObject'
/usr/lib/gimp/1.2/plug-ins/sphere.rb:101:in `main': file gtkobject.c: line 236 (gtk_object_destroy): assertion `GTK_IS_OBJECT (object)' failed. (Gtk::Error)
        from /usr/lib/gimp/1.2/plug-ins/sphere.rb:101
ruby: fatal error: セグメンテーション違反です
ruby (pid:1284): [E]xit, [H]alt, show [S]tack trace or [P]roceed: S
#0  0x402c5d8c in g_on_error_stack_trace () from /usr/lib/libglib-1.2.so.0
#1  0x402c596f in g_on_error_query () from /usr/lib/libglib-1.2.so.0
#2  0x402a1a69 in gimp_plugin_sigfatal_handler ()
#3  <signal handler called>
#4  0x40790888 in gimp_help_free () from /usr/lib/libgimpui-1.2.so.0
#5  0x4076a172 in _done ()
#6  0x4004c3a8 in rb_protect () at eval.c:88
#7  0x40056a66 in rb_exec_end_proc () at eval.c:88
#8  0x400443f9 in ruby_finalize () at eval.c:88
#9  0x40044503 in ruby_stop () at eval.c:88
#10 0x40044663 in ruby_run () at eval.c:88
#11 0x080486c2 in main () at eval.c:88
#12 0x4014f1be in __libc_start_main (main=0x8048694 <main>, argc=7, 

2002-08-12

λ. 一日ごろごろ。

λ. テレビで新宿鮫をやっていたので見た。鮫島ってこんなにオヤジだっけ?


2004-08-12

λ. iconv-io 0.0.4

readpartialキター ([ruby-dev:24058]) ってことで、iconv-ioをreadpartialを使うようにする。

知らない人のために紹介すると、iconv-io はIOもどきの1つで、他のIOっぽいオブジェクトをラップし、エンコーディングを変換しながら読み書きするためのものです。例えば、以下はSTDINをラップしてshift_jisからutf-8にエンコーディングを変換しながら読む例です。


io = Iconv::Reader.new(STDIN, "shift_jis", "utf-8")
io.each_line{|l|
  ...
}
Tags: ruby

λ. "Purely Functional Data Structures", Chris Okasaki

読了。感想は後ほど追記予定。

[2005-01-27 追記] 計算量の表を時々参照したくなるので、ここに転載しておく。

Summary of Implementations
(Worst-case running times are marked with †.
All other running times are amortized.)
Name Running Times of Supported Functions Page
banker's queues snoc/head/tail: O(1) 26
physicist's queues snoc/head/tail: O(1) 31
real-time queues snoc/head/tail: O(1) 43
bootstrapped queues head: O(1), snoc/tail: O(log× n) 89
implicit queues snoc/head/tail: O(1) 113
banker's deques cons/head/tail/snoc/last/init: O(1) 56
real-time deques cons/head/tail/snoc/last/init: O(1) 59
implicit deques cons/head/tail/snoc/last/init: O(1) 116
catenable lists cons/snoc/head/tail/++: O(1) 97
simple catenable deques cons/head/tail/snoc/last/init: O(1), ++: O(log n) 119
catenable deques cons/head/tail/snoc/last/init/++: O(1) 122
skew-binary random-access lists cons/head/tail: O(1), lookup/update: O(log n) 79
skew-binomial heaps insert: O(1), merge/findMin/deleteMin: O(log n) 83
bootstrapped heaps insert/merge/findMin: O(1), deleteMin: O(log n) 102
sortable collections add: O(log n), sort: O(n) 35
scheduled sortable collections add: O(log n), sort: O(n) 47

[追記] ちなみに、この論文を元にした本が出版されています。 より一般向けの話とHaskellのコードが加わっているとか。
Purely Functional Data Structures(Chris Okasaki)

Tags: 論文

2007-08-12

λ. ¬(∀x.P(x)) → ∃x.¬P(x)

非常にしょーもないのだが、ふと ¬(∀x.P(x)) → ∃x.¬P(x) の証明を自然演繹で書こうとして苦戦。こんな基本的な事で苦戦するなんて色々やばいな。 結局、callccを使ったプログラムを思い浮かべて証明した。 古典論理はやっぱり変態的だと思った。

Agdaでの証明

postulate callCC (|X::Set) :: Not (Not X) -> X

prop (!D::Set) (!P::D->Set)
    :: Not ((x::D) -> P x) -> Exist (\(x::D)-> Not (P x))
prop k1 =
    callCC (\(k2::Not (Exist (\(x::D) -> Not (P x)))) ->
        let f :: (x::D) -> P x
            f x = callCC (\(k3::Not (P x)) ->
                      let e :: Exist (\(x::D) -> Not (P x))
                          e = struct
                                fst :: D
                                fst = x
                                snd :: Not (P x)
                                snd = k3
                      in k2 e)
        in k1 f)

自然演繹での証明

Agdaによる証明をそのまま翻訳したもの。

[¬P(x)]:3
───── (∃I)
∃x.¬P(x)    [¬∃x.¬P(x)]:2
─────────────── (¬E)
⊥
───── (¬I{3})
¬¬P(x)
───── (¬¬)
P(x)
───── (∀I)
∀x. P(x)       [¬∀x.P(x)]:1
─────────────── (¬E)
⊥
─────── (¬I{2})
¬¬∃x.¬P(x)
─────── (¬¬)
∃x.¬P(x)
─────────────── (→I{1})
¬∀x.P(x) → ∃x.¬P(x)

シーケント計算での証明

自然演繹だとややこしかったけど、シーケント計算だと実は簡単。

P(a) ├ P(a)
──────── (├ ¬)
├ P(a), ¬P(a)
──────── (├ ∃)
├ P(a), ∃x.¬P(x)
────────── (├ ∀)
├ ∀x.P(x), ∃x.¬P(x)
──────────── (¬ ├)
¬∀x.P(x) ├ ∃x.¬P(x)
─────────────── (├ →)
├ ¬∀x.P(x) → ∃x.¬P(x)
Tags: agda logic

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

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

Tags: 圏論

λ. 『ηなのに夢のよう』 森博嗣

ηなのに夢のよう (講談社ノベルス)(森 博嗣)

Gシリーズはやっぱり西之園萌絵の成長がテーマだったのだなと思った。 綺麗な終わり方。 肝心のところは引っ張っるだけ引っ張ってそのままだけど。

Tags:
本日のツッコミ(全2件) [ツッコミを入れる]

ψ ささだ [顔文字にしか見えない。]

ψ さかい [あひゃ (├ ∀) でも、こういうの授業でやりませんでした?]


2008-08-12

λ. cwaでの自然数型の解釈

(書きかけ)

この間はユニット型について考えたので、今度は自然数型を。

自然数型の規則

自然数型に関する通常の規則は以下のようなもの。

--------------
Γ ├ N : set
Γ ├ 0 : N

Γ ├ M : N
--------------
Γ ├ s(M) : N

Γ, n : N ├ C set
Γ ├ M0 : C[n:=0]
Γ, n : N, x : C ├ Ms : C[n:=s(n)]
Γ ├ M : N
--------------------------------------
Γ ├ elim([n]C,M0,Ms,M) : C[n:=M]
Γ ├ elim([n]C,M0,Ms,0) = M0 : C[n:=0]
Γ ├ elim([n]C,M0,Ms,s(M)) =
       Ms[n:=M, x:=elim([n]C,M0,Ms,M)] : C[n:=s(M)]

なんだけど、例によって以下のように変形した規則で考える。

---------
├ N set
├ 0 : N

---------------
x:N ├ s[x] : N

Γ, x:N ├ P[x] set
Γ ├ M0 : P[0]
Γ, x:N, y:P[x] ├ Ms[x,y] : P[s[x]]
------------------------------------
Γ, x:N ├ elim(P,M0,Ms)[x] : P[x]
Γ ├ elim(P,M0,Ms)[0] = M0 : P[0]
Γ, x:N ├ elim(P,M0,Ms)[s[x]]
            = Ms[x, elim(P,M0,Ms)[x]] : P[s[x]]

省略記法

cwaでの解釈をまともに書いていると大変なので、ちょっと略記法を導入する。(後で書く)

cwaでの解釈

で、cwaで解釈するとこうなる。

  • N∈Fam(1)
  • 0∈Tm(1, N)
  • s∈Tm(1・N, N+)
  • P∈Fam(Γ・N+), M0∈Tm(Γ, P[0+]), Ms∈Tm(Γ・N+・P, P[π・N+][s+][π]) が与えられたとき、h=elim(P,M0,Ms)∈Tm(Γ・N+, P) が存在し、h[0+]=M0, h[π・N+][s+]=Ms[h] が成り立つ。

\xymatrix@+20pt{ \Gamma \ar[r]^{0^{+}} \ar[d]|{h[0^{+}]=M_0} & \Gamma\cdot N^{+} \ar[d]^h \\ \Gamma\cdot P[0^{+}] \ar[r]_{0^{+}\cdot P} & \Gamma\cdot N^{+}\cdot P }

\xymatrix@+20pt{ \Gamma\cdot N^{+} \ar[rr]^{s^{+}} \ar[d]|{h[\pi\cdot N^{+}][s^{+}]=M_s[h]} & & \Gamma\cdot N^{+}\cdot N^{+} \ar[d]|{h[\pi\cdot N^{+}]} \ar[r]^{\pi\cdot N^{+}} & \Gamma\cdot N^{+} \ar[d]^{h} \\ \Gamma\cdot N^{+}\cdot P[\pi\cdot N^{+}][s^{+}] \ar[rr]_{s^{+}\cdot P[\pi\cdot N^{+}]} & & \Gamma\cdot N^{+}\cdot N^{+}\cdot P[\pi\cdot N^{+}] \ar[r]_-{\pi\cdot N^{+}\cdot P} & \Gamma\cdot N^{+}\cdot P }

\xymatrix@+20pt{ \Gamma\cdot N^{+} \ar[d]_{M_s[h]} \ar[rr]^h & & \Gamma\cdot N^{+}\cdot P \ar[d]^{M_s} \\ \Gamma\cdot N^{+}\cdot P[\pi\cdot N^{+}][s^{+}] \ar[rr]_-{h\cdot P[\pi\cdot N^{+}][s^{+}][\pi]} & & \Gamma\cdot N^{+}\cdot P\cdot P[\pi\cdot N^{+}][s^{+}][\pi] }

λ. お菓子買いだめ

今月は少なめで。
[お菓子]

Tags: