2001-08-12
λ. 朝方の生活に戻したと思ったら、眠れなくて、寝たのが朝の9時ごろ。で、起きたのが夜の7時。だめだこりゃ。明日こそは早起きして「猿の惑星」見るぞ。
λ. NArrayの次元順序
現在のFORTRANスタイルだと、例えばGimpで扱っているようなメモリ形式の画像データで、RGBを次元として扱う場合に、こんな風に書くことになるのか。…微妙。
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を使ってくれたまえ。
λ. とか思って安心してたら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,
2004-08-12
λ. iconv-io 0.0.4
readpartialキター ([ruby-dev:24058]) ってことで、iconv-ioをreadpartialを使うようにする。
知らない人のために紹介すると、iconv-io はIOもどきの１つで、他のIOっぽいオブジェクトをラップし、エンコーディングを変換しながら読み書きするためのものです。例えば、以下はSTDINをラップしてshift_jisからutf-8にエンコーディングを変換しながら読む例です。
io = Iconv::Reader.new(STDIN, "shift_jis", "utf-8") io.each_line{|l| ... }
λ. "Purely Functional Data Structures", Chris Okasaki
読了。感想は後ほど追記予定。
[2005-01-27 追記] 計算量の表を時々参照したくなるので、ここに転載しておく。
| 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のコードが加わっているとか。
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)
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 }](tex/3f9b7cee876ecac53c8b09df323baa05.png "\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 }](tex/8babf88d37750599ce5d3ae3009d101c.png "\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] }](tex/49e9f9dc8ea37c97bde41a957570c4e3.png "\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] }")
λ. お菓子買いだめ
今月は少なめで。
![[お菓子]](./images/20080812_0.jpg)
