2001-08-29
λ. この一週間
やや放心気味だったけど、ようやくちょっとやる気になってきた。
λ. H2OH2Aロケット
打ち上げに成功したようでなにより。
λ. 「いずれ檸檬は月になり」岩井志麻子 (小説すばる5月号より)
舞台の××市が素敵。インスマウスのような陰欝さを内包する現代的な都市、それでいて幻想的。こういうの好きだなぁ。
λ. SPAN
本文がM$ Word のファイルになってるSPAMを初めて受け取った。そういやmewはwvHtmlとw3mを使って表示してくれて良い感じだね。だけど、SPAMでしかもWordなんて、やっぱ2重に腹が立つよ。送った奴は「デスおじや」でも食らって、逝ね!
2004-08-29
λ. 金沢の方へ旅行に行ってきます。
λ. 『「知財」で稼ぐ！』
飛行機の中で読んだ。
λ. 旅行
.
λ. 永平寺
そうそう。永平寺にも行きました。先生、eiheiですよ、eihei。(補足: 研究室で僕の使っているマシンの名前がeiheiなのです)
λ. "Compiling Haskell to Java", Mark Tullsen
GHCにSTGのコードを吐かせてそれをJavaに変換してJVMで動かす話で、デザインディシジョンについての議論がメイン。このデザインディシジョンは全く順当だと思う。ああ、そうだ。Mondrian関係のドキュメントを読んで、こっちの方面では代数的データ型はこういう場合にはサブタイピングで代用するのが流行りなんだと思っていたが、ここでは整数でタグをつけてるな。あと、速度は GHC > この実装 > Hugs みたい。
2005-08-29
![[モリゾーとキッコロ]](./images/20050829_0.jpg)
λ. HDD(Seagate ST3250823A)購入
銀座まで行ったついでに、HDDを購入しに秋葉原へ。そういや、秋葉原に一人で行くのは初めてだ。どの店で何を買ったら良いかわかんなかったので、適当に見つけた店で適当に Seagate ST3250823A というのを買った。¥12,700なり。デスクトップのHDDをこいつに交換。ddで古いハードディスクの内容を丸ごとコピーして、parted, fdisk, ntfstools 等で適当にパーティションを編集。これで、ラップトップのデータをバックアップしておくスペースが出来た。
2006-08-29
λ. 太陽 The Sun
ずいぶん遅くなってしまったが、横浜ムービルで観てきた。 席はガラガラだったので見やすい位置で観れた。観客には年配の方が多かったが、私ぐらいの人もチラホラいた。内容については、私には小熊さんのような感想は書けないが、素晴らしい映画だった。
追記
<URL:http://smallbear.sakura.ne.jp/tron/btm20068.html#20060830>
空いていたのは、平日の真昼間だったからと、あと東京と横浜の差ではないかと。
λ. PPL Summer School 2006 に参加申し込み
SLACSと重なっていたので迷ったが、申し込んでしまった。 色々な人に会うのが楽しみ。
2007-08-29
λ. W-typesによる帰納的データ型の表現
まずは W-types の定義と除去規則を示す。
data W (A::Set) (B::A->Set) = sup (a::A) (x::B a->W A B)
elimW (|A::Set) (|B::A->Set)
(!C::W A B -> Set)
(!d::(a::A) -> (f::B a -> W A B) ->
(g::(b::B a) -> C (f b)) -> C (sup a f))
(!c::W A B)
:: C c
elimW = case c of (sup a f)-> d a f (\(b::B a)-> elimW C d (f b))
W-types という名前は Wellorderings から来ていて、順序数(っぽい何か)を整礎な木として構成したものになっている。Martin-Löf の Intuitionistic Type Theory での説明:
The concept of wellordering and the principle of transfinite induction were first introduced by Cantor. Once they had been formulated in ZF, however, they lost their original computational content. We can construct ordinals intuitionistically as wellfounded trees, which means they are no longer totally ordered.
この型それ自体も面白いのだけど、この型を使った面白い事として外延的な型理論ではこれを使って帰納的なデータ型を表現する事が出来るという事が知られている。なので、これをagdaでも表現してみたい。 だが、agdaの型理論は外延的ではないので、まずは「関数は全ての引数に対する値が等しければ等しい」ことを公準として追加する。 ついでに後で使う定義も追加。
postulate ext :: (X,Y::Set) |-> (f,g::X->Y) ->
((x::X) -> Id (f x) (g x)) -> Id f g
data Empty =
data Unit = tt
uu (X::Set) :: Empty -> X
uu e = case e of { }
uu_lemma (X::Set) (!f::Empty -> X) :: Id uu f
uu_lemma = let eid (!e::Empty) :: Id (uu e) (f e)
eid = case e of { }
in ext uu f eid
tt_lemma (X::Set) (!f::Unit -> X) :: Id (\(t::Unit)-> f tt) f
tt_lemma = let eid (!t::Unit) :: Id (f tt) (f t)
eid = case t of (tt)-> refId (f tt)
in ext (\(t::Unit) -> f tt) f eid
リストの例
例えばリスト型は以下のように表現する事が出来る。
data Maybe (X::Set) = Nothing | Just (x::X)
L (A::Set) :: Maybe A -> Set
L x = case x of
(Nothing)-> Empty
(Just a )-> Unit
List' :: Set -> Set
List' A = W (Maybe A) L
Nil' (A::Set) :: List' A
Nil' = sup Nothing uu
Cons' (A::Set) :: A -> List' A -> List' A
Cons' x xs = sup (Just x) (\(t::Unit) -> xs)
elimList' (X::Set)
(!C::List' X -> Set)
(!n::C Nil')
(!c::(x::X) -> (xs::List' X) -> C xs -> C (Cons' x xs))
(!xs::List' X)
:: C xs
elimList' =
let h :: (a::Maybe X) ->
(f::L a -> W (Maybe X) L) ->
(g::(b::L a) -> C (f b)) ->
C (sup a f)
h a f g =
case a of
(Nothing)->
substId (\(f'::Empty -> W (Maybe X) L) ->
C (sup Nothing f'))
(uu_lemma f) n
(Just x )->
let lem :: C (Cons' x (f tt))
lem = c x (f tt) (g tt)
in substId (\(f'::(t::Unit) -> W (Maybe X) L) ->
C (sup (Just x) f'))
(tt_lemma f) lem
in elimW C h xs
ちなみに、substId が必要になっているのは、agdaでは Unit や Empty→X の要素が自動的に同一視される(それらの間に definitional equality が成り立つ)ことはないため。外延的な型理論の中にはこれらが自動的に同一視されるものもある。
コンテナ
コンテナ(Container)の概念を使った場合について後で書く。
参考
- “Representing inductively defined sets by wellorderings in Martin-Löf's type theory” by Peter Dybjer
- “Representing Nested Inductive Types using W-types” by Michael Abbott, Thorsten Altenkirch, and Neil Ghani
2008-08-29
λ. ETでワンのアルゴリズムを……挫折
せっかくだから、あろは先生を問い詰める会の前にETと「搾り出し方」を試してみるかと思い、昔Haskellで書いて微妙だった Wang's Algorithm (ワンのアルゴリズム) を試してみることにする。
仕様
仕様は以下の組 (D,Q) で表される。
- ホーン節で書かれた背景知識 D
- ホーン節で書かれたクエリーの集合 Q
まずは背景知識D。これは実行可能性は考えなくて良いはずなので、まあ適当にアルゴリズムではなく定義っぽい感じで。
valid(X) ← valid([], [X]). valid(Gamma, Delta)) ← member(X, Gamma), member(X, Delta). valid(Gamma, Delta) ← permutation(Gamma, Gamma1), valid(Gamma1, Delta). valid(Gamma, Delta) ← permutation(Delta, Delta1), valid(Gamma, Delta1). valid(Gamma, [and(A,B)|Delta])) ← valid(Gamma, [A|Delta]), valid(Gamma, [B|Delta]). valid(Gamma, [or(A,B)|Delta])) ← valid(Gamma, [A,B|Delta]). valid(Gamma, [not(A)|Delta])) ← valid([A|Gamma], Delta). valid([and(A,B)|Gamma, Delta)) ← valid([A,B|Gamma], Delta). valid([or(A,B)|Gamma], Delta)) ← valid([A|Gamma], Delta), valid([B|Gamma], Delta). valid([not(A)|Gamma, Delta)) ← valid(Gamma, [A|Delta]). valid(Gamma, [imply(A,B)|Delta]) ← valid(Gamma, [or(not(A),B)|Delta]). valid([imply(A,B)|Gamma], Delta) ← valid([or(not(A),B)|Gamma], Delta). member(X, [X|_]). member(X, [_|T]) ← member(X,T). permutation([], []). permutation(L, [X|L2]) ← select(X, L, L1), permutation(L1, L2). select(X, [X|L], L). select(X, [Y|L], [Y|L1]) ← select(X, L, L1).
お次はクエリーの集合Q。
prb1
ans(X) ← valid(X).
prb2
s ← valid(imply(imply(a,b), imply(imply(a,imply(b,c)), imply(a,c)))).
prb3
k ← valid(imply(a, imply(b, a))).
prb4
peirce ← valid(imply(imply(imply(p, q), p), p)).
Q = {prb1, prb2, prb3, prb4}
処理系のダウンロード
<URL:http://assam.cims.hokudai.ac.jp/et/indexj.html>
搾り出し方
早速、論文の手順に基づいて搾り出してやるぜ! と思って喜び勇んではじめたら、肝心のパターンの決定とルールの生成の部分がこの論文には書いていないのだった。しょぼーん。
もちろん、アルゴリズムを直接書くのは難しくないと思うけど、それをETでやっても仕方がないと思うし。
2009-08-29
λ. LLTV
![[LLTV 試験電波発射中]](./images/20090829_2.jpg)
プログラムを事前にチェックしてなかったので、Language Update がなかったのにビックリした。
プロトタイピングの話が面白く、その場でIDEOの本を注文した。
LTはいつも通りのノリだったが、全体的にはどうも熱気にかけたという印象。
プレゼントで「AWKを256倍使うための本 (Ascii 256倍)(志村 拓/鷲北 賢/西村 克信)」と「ゼロから学ぶ!最新データベース (日経BPパソコンベストムック)(日経ソフトウエア編集)」を頂きました。わーい。
![[「AWKを256倍使うための本」 + 「ゼロから学ぶ！ 最新データベース」]](./images/20090829_0.jpg)
終了後は、不思議な集団で土木土木という不思議なお店へ。
その日はお祭りだったとかで、目当てのジンギスカンはなかったけど、その代わり秋刀魚が食べ放題だった。おいしかった。
![[土木土木]](./images/20090829_1.jpg)
