2001-11-09
λ. 情報数学Ⅰ 中間レポート
問3に出題ミスがあったので問3だけは提出期限が2日延びた。問3の証明はきちんと書けていなかったので助かった。問2は結局証明できなかったので、問1と問4の回答だけを提出。
λ. Namazuによる日記検索
現実逃避にnamazuをインストールして日記検索を出来るようにした。とりあえず、こんな感じで過去の日記データもテキスト化。
require './tdiary.rb'
TDiary.new(nil, nil).instance_eval{
Dir["#{@data_path}??????"].each{|fname|
PStore.new(fname).transaction{|db|
db['diary'].each_value{|d| text_save(d)}
db.abort
}
}
}
それで気がついたんだけど、PStore#abortを呼ぶとちょこっと効率が良くなるのでは? > たださん
--- tdiary-1.2.1/tdiary.rb~ Fri Oct 12 22:42:42 2001 +++ tdiary-1.2.1/tdiary.rb Sat Nov 10 22:18:53 2001 @@ -437,6 +437,7 @@ end yield db['diary'] = @diaries if @dirty + db.abort unless @dirty end File::delete( filename ) if @diaries.empty? end
λ. お昼
タイ風野菜カレー
2003-11-09
λ. 衆議院選挙
投票してきた。
λ. 「メタ」と「高階」
これを読んで気になったのだけど、私は「高階(higher-order)」の「階(order)」って『A,Bのorderをm,nとすると、「Aに依存したB」のorderは max(m+1,n)』という条件で定義される数だと漠然と思ってたのだけど、これって正しいだろうか? 幾つか例を考えてみる。
λ. (例1) 関数
(関数でない通常の)値を0階の関数と考える。通常の関数は値に依存した値だから、max(0+1,0) = 1 より1階の関数。引数が一階の関数であるような関数は max(1+1,0) = 2 より二階の関数。二階以上の関数をまとめて高階関数と呼ぶ。
この定義だと引数が通常の値で返り値が一階の関数であるような関数は、max(0+1, max(0+1,0)) = 1 から一階の関数になってしまい、ちょっと直感に反する気もする。でも、カリー化によって階が変わらないのは逆に本質を捉えている気もする。
λ. (例2) 命題と論理
真偽値を0階の命題と考える。一階の命題は通常の命題。一階の命題に依存して真偽値が定まるような命題は max(1+1,0) = 2 より二階の命題。一階の命題と二階の命題の両方を扱う論理体系は二階論理、orderに制限のない論理体系は高階論理。
λ. (例3) 算術
真偽値を0階の対象と考える。一階の対象は自然数。自然数の集合は(特性関数によって「自然数に依存した真偽値」と考えられるので)二階の対象。自然数を扱う「Q」や「ペアノ算術」等の体系は一階の算術ともいわれる。自然数と自然数の集合の両方を対象とするZ2等の体系は二階算術といわれる。
λ. (例4) 型
「data Bool = True | False」で定義される型Boolのような引数を持たない型は一階の型。「data List X = Nil | Cons X (List X)」で定義されるような型は一階の型を引数に取るので二階の型。「data Fix f = In (f (Fix f))」で定義されるようなFixは二階の型を引数に取るので三階の型(?)。
ポリモルフィック・ラムダ計算(polymorphic lambda calculus) が、二階ラムダ計算(second-order lambda calculus)と呼ばれるのは二階の型を扱えるから?
λ. 高階型?
それはそうと「型の型」と言うと普通は「種(kind)」のことで、型をパラメータにとる型という意味での「高階型」とは違う気がします。
2006-11-09
λ. 『儒教—ルサンチマンの宗教』 浅野 裕一
を読了。
λ. The Theory of Parametricity in Lambda Cube by 竹内 泉
Fωでのparametricityについて興味があったので読んでいるところ。ただ、higher-order polymorphism に対する parametricity は扱いにくいように思う。おそらく、Folds, Church Encodings, Builds, and Short Cut Fusion for Nested Types: A Principled Approach でのhfoldに対してのgfoldのようなより扱いやすい形が必要になるのではないかと思った。
参考:
関連エントリ
【2006-12-20 追記】 Definition 3.17 (Conformity Relation) では、αが種のとき「 <ΠX:α. P>{θ} = ∀X1:αθl, X2:αθr. ∀Y:(|X:α|){θlr,(X1,X2)/X}. <P>{θ,(X1,X2,Y)/X} 」と定義しているけど、Tが型のときの「<Πx:T. P>」と同じで「 <ΠX:α. P>{θ} = λy:(ΠX:α. P)θl, z:(ΠX:α. P)θr. ∀X1:αθl, X2:αθr. ∀Y:(|X:α|){θlr,(X1,X2)/X}. <P>{θ,(X1,X2,Y)/X} (y X1) (z X2) 」と定義しないとまずいはず。そうしないと、Definition 3.9 (Kind of Conformity Relation) と種が一致しない。
このように定義を修正すると、例えば、
Nat : (*->*)->(*->*)->* Nat = λF,G:*->*. ΠX:*. FX->GX
の Conformity Relation は以下のようになり、種がきちんと一致する。
- <Nat> : (|Nat|)
- (|Nat|) =
ΠF1,F2:*→*, FR:(ΠX1,X2:*. (X1→X2→*) → (F1 X1 → F2 X2 → *) ).
ΠG1,G2:*→*, GR:(ΠX1,X2:*. (X1→X2→*) → (F1 X1 → F2 X2 → *) ).
(Nat F1 G1) → (Nat F2 G2) → * - <Nat> =
λF1,F2:*→*, FR:(ΠX1,X2:*. (X1→X2→*) → (F1 X1 → F2 X2 → *) ).
λG1,G2:*→*, GR:(ΠX1,X2:*. (X1→X2→*) → (G1 X1 → G2 X2 → *) ).
λα1:Nat F1 G1, α2:Nat F2 G2.
∀X1,X2:*, XR:X1→X2→*.
∀x1:F1 X1, x2:F2 X2.
FR X1 X2 XR x1 x2 → GR X1 X2 XR (α1 X1 x1) (α2 X2 x2)
λ. 実写版エヴァンゲリオン？
をぐまさんのmixi日記より。良くできてるなぁ。
2008-11-09
λ. 第四十六回圏論勉強会
今回は 6.4節 The Temperley-Lieb Category の前半部分で、結合演算と恒等射を定義してテンパリー・リーブ圏(TL)が圏になっていることを確認。今回もやっぱり定義が巧妙で感心した。前回やったP(n,m)の定義とかを半分忘れていて大変だったが。
今回やり残した6.4節の残りは、TL が pivotal category であるという話と、TLと3節で定義したDが strict pivotal dagger category として同型であるという話になるようだ。
雑談では、この6節の「Planar Geometry of Interaction and the Temperley-Lieb Algebra」という名前にも含まれている Geometry of Interaction に関係して、 檜山さんに Int Construction というもののイメージの紹介をしてもらった。Int Construction は自然数から整数を構成する構成を一般化し、トレース付きモノイダル圏からコンパクト閉圏を構成する。そういえば、 「再帰プログラムの幾何」にもそんな話があったなぁ……
二次会では白石先生とかDHMOとか。
ψ ただただし [がーん、PStore#abortなんて知らなかったよ。1.7系からは自動的に保存されなくなるって聞いてたし……。明日..]
ψ さかい [1.7から自動的に保存されなくなるってのは初耳っす。 XPStoreのリードオンリートランザクションの話じゃないです..]
ψ ただただし [幻想かもしれないから(笑)。ただを信じてはいけない。]