ChromeにはGoogle Gearsが組み込まれてます。 http://code.google.com/apis/gears/ Gearsは単なるrdbのAPIと思ってたけど、Desktop/LoacalServer/Workerなどいろいろあるようで、順次試してみようと思う。 まずは、databaseだが、ResultSetがnext()でカーソ…

pythonにはリスト用のmapやreduce組み込み関数もあるけれど、generatorを使って平行プログラミング風にGoogleのMapReduce風サーバを書いてみた。サーバと入ってもgeneratorなので、実際の実行はシングルスレッド上で処理されるです。generatorはsendメソッド…

1.X系から大きく変わってます。 http://llvm.org/releases/2.2/docs/LangRef.html Cコードhellostruct.c int puts(const char*); struct Hello { int age; char* name; }; int main() { struct Hello hello; hello.age = 15; hello.name = "Taro"; puts(hell…

Agda2では、dataで定義したデータ型は有限で、それを利用する再帰関数も停止性が証明できないといけないけれど、codataは、停止しない再帰関数を記述することができます。定義は、ラベルがcodataである以外、dataと同じです。以下のStream Aは、List Aと同じ…

なるほどなと思った A Neighborhood of Infinity: MSFP 2008 より HaskellでのListデータ型の定義 data List A = Nil | Cons A (List A) 各項を以下の数式記号に、置き換える List A => L(A) a | b => a ＋ b Nil => 1 Cons A b => A × b L(A) = 1 ＋ A × L(…

参考は http://www.cs.chalmers.se/~ulfn/darcs/AFP08/LectureNotes/AgdaIntro.pdf とAgda2添付のexamples、そしてソースコード。一応emacsインタフェースで、コード補完(別名、証明補助)できるUIがあるのですが、自分はまったく使ってません。一応、こうい…

Haskell風構文のDependently Typed Programming LanguageであるAgda2を少し学んでみました。 The Agda Wiki - Agda インストールとか ubuntu intrepidで使う場合、依存ライブラリのうち、zlibとQuickCheckだけは別途makeして入れる必要がありました。あとはd…

PDFのユーザー間の共有は可能だけど、PDFの公開はまだ無理のもよう。 PDF文書は、ブラウザ上では画像で大きめに表示される。その画像の上で矩形選択&Ctrl+Cで文字をコピーできる少しきもちわるい仕様。slideshareは表示が小さかったり処理が重かったりといろ…

この辺の話題の調査というかまとめというか。発表で使ったLaTeXで作ったスライドを少し追加修正。想定時間とか大幅に間違えてるので、バランス的な面でいろいろ中途半端かもしれない。Survey around Semantics for Programming Languages, and Machine Proof…

ブックマークに書いたけど、自分の認識を明確にするため、少し詳しく書いておくことにしてみた。 はてなブックマーク - Reading C type declarations - Eli Bendersky's website C言語で、 char *(*(**foo [][8])())[] みたいな型はどういう意味を持つかは、…

Radeon: http://ati.amd.com/support/driver.html Vista x64: Explore AMD Featured Games | AMD BIOS、チップセットドライバ: GIGABYTE Japan BIOS: マザーボード | サポート - GIGABYTE Japan Chipset: マザーボード | サポート - GIGABYTE Japan LAN: htt…

ついにX4ですよ、X4。マザーボードはGIGABYTEのGA-MA78GM-S2H(rev1.1)。店頭においてあったのはrev1.0ばかりだけど、T-ZONEで山積みされてるなかにrev1.1が少し混じってたので購入(9681円)。Phenom 9350eはツクモEXで23980円。マザーは結構大きめなのでMicro…

Official Google Blog: Lively no more まずは人が集まるかどうか、かな。このようにアバターはSecondLifeよりなじみやすいとは思うけれど。 Windowsにインストール、ブラウザ上で実行 移動はドラッグのみ(WASD移動はない) 矢印キーとマウスホイールで視点切…

Vistaのおまけがパスタってのはどうなんだろうか。時代は4コアだなと、Phenom X4 9350eと対応マザーボードを買おうと久しぶりに秋葉原にいったけど、9350eがどこも入荷まちだった。 http://ja.wikipedia.org/wiki/AMD_Phenom : 9350eは24000円前後 GIGABYTE …

オンラインでマインドマップ――無料Webアプリ6選 - ITmedia エンタープライズ よりmind42を試してみた。 http://www.mind42.com/ なかなかいいと思う。ちなみに画像形式でのEXPORTでは日本語文字列は入らない。(はてなダイアリーへのiframe貼り付けは、iframe…

http://www.icfpcontest.org/rules.htmlにある言語のうち、ひときわマイナーで目立ってました。 http://www.cs.mu.oz.au/research/mercury/ Mercury (programming language) - Wikipedia 関数型論理言語にはCurryもありますがCurryがHaskellに論理プログラミ…

たまたまみかけた http://d.hatena.ne.jp/aqvi/20080624 より、まず「副作用」の使い方が変な気がしますがそれは置いといて、erlangでは、ガードでかける式が限定されるのは初めて知ったので勉強になりました。 http://www.erlang.org/doc/reference_manual/…

VMWare上でだけれど。システムはamd64です。amd64上のサガでflash pluginはやはりSCIMが効かない。コピペはできるし、ニコニコだとフォームと同期するgreasemonkeyを使えばいいのであまり気にならないです。最近気になるのは、Unicode記号のフォントが少ない…

ここ最近なんとなく、電気回路などで使ってる応用数学を思い出しながら、ラプラス変換とか復習してたりしてました。どうせならということで、この機に、数式システムmaximaを使ってみることにしました。 http://maxima.sourceforge.net/ たとえば、ラプラス…

証明戦略unfoldとfoldの練習です。 Coq < Lemma pluszero: forall n:nat, plus n 0 = n. 1 subgoal ============================ forall n : nat, n + 0 = n pluszero < intros. 1 subgoal n : nat ============================ n + 0 = n pluszero < indu…

Pythonで Bloom filter - Wikipedia Bloom Filterはデータが入ってるかどうかを問い合わせるもの。一種のSetのようなものだが、確率的に誤検出の可能性がある。特徴は、保持するデータが固定長のビットフィールドで元データが不要であり、ビット和で足し合わ…

λ式の構文ルール E = \x.E | E1 E2 | V | C V = 変数 C = 定数Combinator Logic(CL)はS K Iコンビネータ。CLで計算を表現すると、束縛変数がなくなるのがいいところ。λ式をCLに変換するルール []\x.E => [x]E [](E1 E2) => []E1 []E2 []v => v [x]\y.E => [x…

ビット演算の練習もかねて、ghciでputStrLnで日本語文字が出せないのもつらいので書いてみた。ghcのCharはunicode（16bit）だけど、putChar等がバイト列でのみしか扱えないので。 import Data.Char import Data.Bits utf8 :: String -> String utf8 s = conc…

圏論続き。 図式(diagram) 圏論では、h = f.g のことを、hとf.gは「可換」といいます。 圏Setでは、{(x,h(x))|∀x} と {(x, f(g(x)))|∀x}が等しいことを指します。 射それぞれf:Y->Z, g:X->Y, h:X->Zとすると、 という「図式」が書けます。図式は以下の性質を…

圏論の続き。equaliserとcoequaliser。 Equaliser (mathematics) - Wikipedia Coequalizer - Wikipedia equaliserの例 対象X,Yで、射e:E->Y = equaliser(f:X->Y,g:X->Y) の定義 f.e = g.e （つまり∀a:E, f(e(a)) = g(e(a))となる） f.h = g.hを満たす任意の…

圏論の学習で、始対象と終対象の理解でつまづかせるのは、書籍等でのその例に挙げられる圏Setでの対象である空集合に対する射の説明がないからだとわかった。 始対象、終対象ともに定義なのでそれ自体は特に難しくないのだが、例が無説明で挙げられるのみな…

LLVM-1.x系の文書です。コマンドラインツールの使い方は同じですが.llの構文が2.2では通らないです。 インストール ubuntuでLLVMのパッケージを入れます。 apt-get install llvm llvm-cfe llvm-libs LLVMについて LLVMは仮想マシンですが、そのバイトコード…

Pythonでのlambdaの構文自体は中途の改行を許さないけど、括弧でくくれば途中ではインデントも改行ありなしも関係なくなる: print (lambda x: x + x) (10) #=> 20 そう考えると、PythonでもいわゆるDSL風なことも結構できるんじゃないだろうかと思う。たとえ…

例としてand除去を含む証明。 Coq < Goal forall A B : Prop, A /\ B -> B. ... Unnamed_thm < intros. 1 subgoal A : Prop B : Prop H : A /\ B ============================ B Unnamed_thm < elim H. 1 subgoal A : Prop B : Prop H : A /\ B ===========…

例は、forall (A B: Prop), A->(A->B)->B。これはintrosをすると、A, A->B ┣ Bとなる。これはcoqでは自動的に解決できるものであり、証明戦略的には、->除去である。 http://adam.chlipala.net/itp/tactic-reference.html によるとapplyする状況なのだが、仕…