■
A modular formalisation of finite group theory
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.122.5995
という論文を眺めたりした。CoqとCoqのライブラリであるSSReflectを使って、Feit-Thompsonの定理の証明を形式化しようという話らしい。試みとしては面白いけど、研究としてはどうなんだろうっていう。まあ、頑張ればきっと書けるのは書けるんだろうし(とてもしんどいとは思うけど)。
こういうのは、Wikipediaみたいに、ヒマ人がちょこちょこCoqのコードを投げていくと、そのうち証明が完成するというスタイルがいいんじゃないかとか思ったりもした。Wikipediaスタイルで、有志で完全にformalな数学辞典を作るとかは結構面白い気がする。名前は、Bourbakipediaとかで(
call/cc in Lua
http://stackoverflow.com/questions/2827620/call-cc-in-lua-possible
であったネタ。
前提知識(?)
[1]Coroutines in Lua
http://www.inf.puc-rio.br/~roberto/docs/corosblp.pdf
[2]Revisiting Coroutines
http://www.inf.puc-rio.br/~roberto/docs/MCC15-04.pdf
[3]Some Proofs about Coroutines
http://www.dbd.puc-rio.br/depto_informatica/08_04_ierusalimschy.pdf
[1]~[3]で言われてるのは、
asymmetric coroutine(Luaのcoroutine,semi-coroutine)=symmetric coroutine=one-shot continuation
は全部等価とかいう話。
あと、"one-shot delimited continuation"とも一緒だよみたいなことが書いてあるけど、実際に使ってるのは、subcontinuationとかいうよく知らない代物。論文では、spawn/controllerとか使ってるけど、これはprompt/controlと同じっぽい?が、これらが、shift/resetと同等なのかとか、知らない。
call/1ccは実装してるScheme処理系がChezSchemeしかないし、使ってるコードとかも全然ないので、なんかよく分からないけど、
(call/1cc (lambda (k) (k 0)))
などはOKだけど、
(define cont #f)
(begin (display "hoge")
(call/1cc (lambda(c) (set! cont c)))
(display "fuga")
(display "piyo"))
(cont)とかやると、Exception: attempt to invoke shot one-shot continuationといわれる。Luaによるcall/1ccの実装は[2]に書かれてる。
で、じゃあcall/ccと、こいつらの差は何?みたいな疑問があって、coroutineの複製が作れれば、call/cc作れるんじゃねという話。
coroutineの複製をできるようにしたというLua処理系のpatchが
http://lua-users.org/lists/lua-l/2006-01/msg00652.html
らへんにあって、これを使って作ったというcall/ccが
https://github.com/torus/lua-call-cc/blob/master/callcc.lua
複製できるというのは、
local co = coroutine.create(function () for i=1,100 do
print(i)
coroutine.yield(i) end end)
coroutine.resume(co)
coroutine.resume(co)
local co2 = coroutine.clone(co)
coroutine.resume(co)
coroutine.resume(co)
coroutine.resume(co2)
coroutine.resume(co2)とか実行すると、1,2,3,4,3,4が返ってくるという意味。
pythonのitertools.teeは似たようなことができるけど、あれは結果をキャッシュしているだけらしいので、
import itertools
x = 0
def gen():
for i in xrange(1,100):
yield (i+x)
co = gen()
co.next() #yield 1
co.next() #yield 2
co,co2 = itertools.tee(co)
co.next() #yield 3
co.next() #yield 4
x=10
co2.next() #!?
co2.next() #!?とかいうケースで困る。
で、以下のようなコードが動く。
require "callcc" function add(x,y) return x+y end --(display (call/cc (lambda (c) (+ 2 (c 3))))) function test() local r = callcc (function (cont) add(2,cont(3)) end) print(r) end --(display (+ 2 (call/cc (lambda (k) (k (k 0)))))) function test2() local r = callcc(function (k) k(k(3)) end) print (2+(r)) end --(call/cc (lambda (c) ((c 0) (c 1)))) function test3() local r = callcc(function(k) k(0)(k(1)) end) print(r) end callcc_run(test) callcc_run(test2) callcc_run(test3)
callcc_runとかどうなの?っていうのと、それを除いてもほんとにこれがcall/ccと等価って言ってよいのか確信がない。実際のとこ
http://d.hatena.ne.jp/m-a-o/20060915#p3
にあるような
(let ((f (call/cc call/cc))) (f (lambda (x) 1)))
というコードは動かないっぽい。どこで死んでるか真面目に調べてはいないけど。
callcc_runをなくすには、VMの実体であるlua_Stateをthreadにしてやれば、ほんとのcurrent continuationを取ることができて、それで同じようなことをしてやればよい気がする(けど、それが実際に動くのかは試してない)。そういうのなしには、callcc_runを消すことは多分できない
実用的な観点からすると、もし本当にcall/ccがcoroutine+cloneと等価なら、後者のほうがずっと標準的な頭脳の人類に優しいsemanticsになる。等価でないなら(後者のほうが強力ということはないだろうから)call/ccに届くには、何が足りないのか知りたい。ていうか、call/ccをprimitiveにしようとか、最初に思いついた人は、どうかしてる
ちなみに処理系を改変するのは気分的に避けたかったので、Luaのソースから、lstate.hだけ持ってきて、以下のようなコードを書いてテストした
#include <stdio.h>
#ifdef __cplusplus
extern "C"{
#endif
#include "lua.h"
#include "lauxlib.h"
#include "lualib.h"
//illegal
#include "lstate.h"
#ifdef __cplusplus
}
#endif
int clonethread(lua_State *L){
lua_State *src,*dst;
if(!lua_isthread(L,1)){
luaL_argerror(L , 1 , "coroutine expected");
}
src = lua_tothread(L , 1);
lua_lock(L);
if(!(src->status==LUA_YIELD || (src->status==0 && src->ci==src->base_ci))){
luaL_error(L , "attempt to clone uncloneable coroutine");
}
lua_unlock(L);
dst = lua_newthread(L);
lua_lock(dst);
luaD_reallocstack(dst , src->stacksize - EXTRA_STACK - 1);
luaD_reallocCI(dst , src->size_ci);
/* Copy stack slots */
{
TValue *f,*t;
for(f = src->stack,t=dst->stack ; f < src->top ; f++,t++)
setobj2s(dst , t, f);
dst->top = t;
for(; f < src->ci->top ; f++,t++)
setnilvalue(t);
dst->base = (src->base - src->stack) + dst->stack;
}
/* Copy stack slots */
{
TValue *f,*t;
for(f = src->stack,t=dst->stack ; f < src->top ; f++,t++)
setobj2s(dst , t, f);
dst->top = t;
for(; f < src->ci->top ; f++,t++)
setnilvalue(t);
dst->base = (src->base - src->stack) + dst->stack;
}
/* Copy Frames */
{
CallInfo *f,*t;
for(f = src->base_ci,t=dst->base_ci ; f <= src->ci ; f++,t++){
t->base = (f->base - src->stack) + dst->stack;
t->func = (f->func - src->stack) + dst->stack;
t->top = (f->top - src->stack) + dst->stack;
t->nresults = f->nresults;
t->savedpc = f->savedpc;
t->tailcalls = f->tailcalls;
}
dst->ci = (src->ci - src->base_ci) + dst->base_ci;
}
/* Copy misc fields. Hooks are deliberately not copied. */
dst->status = src->status;
dst->savedpc = src->savedpc;
lua_unlock(dst);
return 1;
}
static const struct luaL_Reg _coroutineLib [] = {
{"clone" , clonethread},
{NULL,NULL}
};
int main(int argc, char **argv){
if(argc==1)return 0;
lua_State *L = luaL_newstate();
luaL_openlibs(L);
luaL_register(L , "coroutine" , _coroutineLib);
luaL_dofile(L , argv[1]);
lua_close(L);
return 0;
}
Coqで圏論
CLTT読書会で最近話題になるネタ。
ConCaT
http://coq.inria.fr/pylons/contribs/view/ConCaT/v8.3
というライブラリがあるんで、これをベースにCLTTの証明なんかを書いていけば、色々よいんじゃないか的な。
ドキュメントらしいものはないけど、論文を読むと、結構詳しい解説がある。あと、どういう順番でソースを追いかけるべきかが分かる。元になった論文は、
Constructive Category Theory
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.4193
10年以上前の論文。
実は、昔読んだらしい。
http://d.hatena.ne.jp/m-a-o/20070202#p3
基本的に、「集合」としてSetoidというものを使っていくんだけど、それで普通の圏論と同じと考えていいのか、よく分からない。この構成的圏論で証明できることは、普通の圏論でも証明できるということが担保されてれば、それでいいのだけど。
が、まあ、差し当たっては、そんな細かいことは気にしないで先に進む強い心をこの数年で得たのだった。
論文と今では微妙にnotationが変わってたりするので、思い出すのも兼ねて、メモ。
・Chapter2
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.RELATIONS.Relations.html
らへんの話。内容は同値関係の定義。等号関係は同値関係なので、そのために必要になる。
・Chapter3.1/Chapter3.2
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.SETOID.Setoid.html
らへんの話。Setoidの定義。Setoid自体は、型理論の範疇で、集合の代替物を作る常套手段の一つらしい。
http://en.wikipedia.org/wiki/Setoid
例として、自然数のSetoidを定義している。
Inductive Nat : Type := Z : Nat | Suc : Nat -> Nat.
が自然数の型。等号関係の定義は、Haskellでderiving Eqした時のと同じもの。これが同値関係になることは別途証明する必要がある。
Setoidは
Structure > Setoid : Type :=
{Carrier :> Type;
Equal : Relation Carrier;
Prf_equiv :> Equivalence Equal}.という定義になってる。:>とかは、
http://pauillac.inria.fr/cdrom_a_graver/www/coq/doc/node.3.3.8.html#Coercions-and-records
とかに説明されているもので、暗黙のうちにSetoidをCarrierに型変換してくれる感じらしい。このように定義すると、
Coq < Check Equal.
Equal
: forall s : Setoid, Relation sとなるのに対して、
Structure > Setoid : Type :=
{Carrier : Type;
Equal : Relation Carrier;
Prf_equiv : Equivalence Equal}.だと、
Coq < Check Equal.
Equal
: forall s : Setoid, Relation (Carrier s)になる
あとは、Structureの後の>のおかげで、
Definition Set_of_nat : Setoid := Eq_Nat_equiv.
で、Setoidが定義できてしまう。
Definition Set_of_nat := Build_Setoid Nat Eq_Nat Eq_Nat_equiv.
と書いても同じことのはず。こっちの方が分かりやすいと思うけどな
・Chapter3.4
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.SETOID.Map.html
らへん。Setoid間の写像の定義。Mapの定義は普通に。自然数の時と同様、Mapという型を作っただけでは、Setoidにはならないので、適切な等号関係を定義してやる。これは単に「f=g<=>forall x.f(x)=g(x)]という外延性に基づく通常の定義
・Chapter4.1
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.CATEGORY.Category.html
圏の定義。Objectの集まりは、Ob:Typeで、射は、Hom:Ob->Ob->Setoidとして定義される。圏論では、対象が等しいかどうかは問題にしないので、Objectの集まりは、Setoidである必要はない。
・Chapter4.2
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.CATEGORY.Hom_Equality.html
圏論では、対象が等しいかどうかは問題にならない(というか、問題にしてはいけない)けれど、射が等しいかどうかは定義できる必要がある。
Definition Equal_hom (C : Category) (a b : C) (f g : a --> b) := (f =_S g). Lemma Equal_hom_refl :forall (C:Category),forall(a b :C),forall(f : a-->b),Equal_hom C a b f f. Proof. intros;unfold Equal_hom in |- *. apply Refl. Qed.
etc.とかでもよいような気はするけど、ライブラリの作者は、f : a-->bとg : c-->dの比較がしたいらしい。それができて嬉しい状況が分からないけれど。ナイーブには、aとcが等しくて、bとdが等しい時とか書きたいけど、Objectが等しいかどうかの判定はできないので、複雑な定義になってる。まあ、正直この定義でよい理由は、あんまり分からない
このへんまで理解すると、圏論を知ってる人には、あとは割と自動的なので、さくっと。
・Chapter4.3
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.CATEGORY.Dual.html
categoryのdualの話。
・Chapter4.4
http://www.lix.polytechnique.fr/coq/V8.2pl1/contribs/ConCaT.CATEGORY_THEORY.CATEGORY.CONSTRUCTIONS.CatProperty.html
epi/mono/isoの定義。
・Chapter4.5
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.CATEGORY.SET.html
Setoidの圏を定義する。ライブラリには、Setoidを使った群やモノイドの定義があるので、それを利用して、群の圏やモノイドの圏も定義することができるはず
・Chapter5.1
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.FUNCTOR.Functor.html
関手の定義。
・Chapter5.2
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.FUNCTOR.HomFunctor.html
Hom Functorの定義。
・Chapter5.3
http://coq.inria.fr/distrib/8.2/contribs/ConCaT.CATEGORY_THEORY.FUNCTOR.CAT.html
あたり。圏の圏。2-category的なもの
・Chapter5.4
ただのExcercise
・Chapter6.1
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.NT.Ntransformation.html
自然変換
・Chapter6.2
自然変換の例。
・Chapter6.3
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.FUNCTOR.CAT.html
関手圏。そろそろ「モナドは単なる自己関手の圏におけるモノイド対象だよ。何か問題でも？」とか、どや顔で語るべきところ
・Chapter7
謎
・Chapter8
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.NT.YONEDA_LEMMA.YonedaEmbedding.html
米田の補題
・Chapter9
論文には、極限や随伴の定義はなかったけど、ちゃんとできるよ！という話が書いてある。今は、ライブラリにも含まれている。
極限
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.LIMITS.Limit.html
余極限
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.LIMITS.CoLimit.html
随伴
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.ADJUNCTION.Adjunction.html
とりあえず、CLTTを形式化するのに、必要なものは一通り揃っていそう(少なくとも、一章に関する限り)。とりあえず、練習として、
・モノイドの圏を定義する
・モナドを定義して、Setoidの圏上でList functorを定義して、こいつがList Monadになることを言う
とかやってみようかと思う
別に難しいことはないはず(続く
インメモリDBはT-treeインデックスだから速いという話
が、
http://www.publickey1.jp/blog/09/rdb_vs.html
とかに書いてあって、だからTimesTenは速いんだ、キャッシュでかい普通のRDBMSとは違うよ!って書いてある。
のだけど、
http://en.wikipedia.org/wiki/T-tree
には、
Although T-trees seem to be widely used for main-memory databases, recent research indicates that they actually do not perform better than B-trees on modern hardware
とか、今時のアーキテクチャでは、B-treeもT-treeも変わんないよとか書いてある。T-treeは1986年の論文らしいし、そういうこともあるかもしれない
Oracleめ！嘘か
『1行の検索であれば数マイクロ秒、1行の更新であっても数十マイクロ秒もかかりません。ディスク型RDBMSではどんなにチューニングしたとしてもミリ秒が限界と言われていますので、TimesTenのレスポンスタイムがけた違いに速いことがわかります。』
とかあるけど、ミリ秒とかどこで言われてるのか知らないけど、HDDアクセスのレイテンシから出てきた数値なんじゃないだろうか。全部キャッシュに載ってるなら、もっと速度が出てもおかしくはない気がする。
T-tree index使ってるOSSのRDBMSとしては、MySQL Clusterがあるけど、あれは結構歴史が古いものなので、それをひきずってるだけの気もする。Innodbでも、データが全部メモリに載って、NDB APIと同じレイヤーで叩けば、memcachedを超えるとかいう話もあるし(てか、このケースだと、一行の検索に数マイクロ秒でできてる計算)
http://www.publickey1.jp/blog/10/nosqlmysqldenamemcached75.html
あとは、VoltDBなんかもB-treeインデックスとハッシュインデックスしかないっぽいので、まあメモリに載るか否かだけが重要なんか
