ここ最近なんとなく、電気回路などで使ってる応用数学を思い出しながら、ラプラス変換とか復習してたりしてました。どうせならということで、この機に、数式システム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 ===========…