限量子の使いようが、いまひとつ理解しきれていない。 Isabelle の集合の条件部に EX を書くと、 EX の条件を満たすものが列挙される。 lemma "{0, 1, 2, 3, 4} = {u::nat. EX j k. j <= k & k < 3 & u = j + k}" apply auto apply (rule_tac x=0 in exI) ap…

PuTTY を使っていて、外部サーバーへの接続方法が ext-server (のような) 名前で保存されているとする。 > pscp -load "ext-server" <localfile name> <ext-server-account>@<ext-server name>:.</ext-server></ext-server-account></localfile>

正月休みにも継続できるよう、 Sourceforge のシェルアカウント内に Isabelle 環境を構築。公式のインストール手順に書かれている tarball を四つ落としてくる。 $ wget http://isabelle.in.tum.de/dist/Isabelle2008.tar.gz $ wget http://isabelle.in.tum.…

とあるクラスに int と double のキャストオペレーターが定義されている。このためユニットテストフレームワークが生成する operatorコンパイルできず困る、という話を伝え聞いた。そんなときは operatorオーバーロードを定義すればいいんじゃない？ #includ…

「は」と「が」。 「は」は文の切り離し、「が」は文の接着をする。「は」は問題を設定し、後にその答えを設定する -- 花は桜。 「は」は対比をつくる -- 私は猫は嫌い。 「は」は限度をあらわす -- 百万円にはならない。 「は」は再審をおこなう -- 美しく…

IE の失効リスト確認にかかわるエラーメッセージについて。 Security certificates are issued for a particular time period. But they can be revoked at any time. The fact that they have been, and why, is supposed to be available to applications.…

なんとなく訳してみた。 A remote code execution vulnerability exists as an invalid pointer reference in the data binding function of Internet Explorer. When data binding is enabled (which is the default state), it is possible under certain …

17.4.3.1 Reserved names [lib.reserved.names] の 17.4.3.1.2 Global names [lib.global.names]: Certain sets of names and function signatures are always reserved to the implementation: Each name that contains a double underscore (__) or begins…

Flash のアップデート通知の画面なんだけれど、タイプフェイスがいかにも中国系フォント。中国では GB という文字セットが一般に使用されているという話。驚いたことに、この文字セットにはカタカナやひらがなも入っているとか。

戻り値 関数が成功すると、バッファに書き込まれた文字数（終端の NULL 文字を除く）が TCHAR 単位で返ります。戻り値が nBufferLength より大きかった場合、その戻り値は、パスを格納するために必要なバッファのサイズ（終端の NULL 文字を含む）を表してい…

レビューをお願いされたプログラム中に、以下のようなコードがあって、いろいろ気になった次第。 typedef std::basic_string<TCHAR> tstring; const tstring get_temppath() { tstring result; int length = ::GetTempPath(0, NULL); TCHAR *buffer = new TCHAR[len</tchar>…

たまに Windows Update にのきなみ失敗して困ることがあるのでメモ。カレントユーザーの Proxy 設定を Windows Update に叩き込む方法。XP では "proxycfg -u"、 Vista では "netsh winhttp import proxy source=ie"。Windows Update がネットワーク接続をす…

gcc に組み込みの「実行時算術オーバーフロー検出」機能 (-ftrapv) について除算に対応していないことを確認した。 $ gcc -ftrapv -x c -S -o - - << EOF > void calc(int a, int b) { > int w = a + b; > int x = a - b; > int y = a * b; > int z = a / b;…

エクスプローラーで落としてきたファイルなどが「ブロック解除」しないと制限がかかるという仕組みの基礎。 INI ファイル形式で ZoneTransfer というセクションに ZoneId というキーをつくり値 0 から 4 のいずれかを指定する。 IE などでは 3 を設定するよ…

と、直前の文章を書いた後でふとおもったんだけれど、こと、家事育児について「手伝う」は禁句というのをどこかで読んだな…。家事も育児も自分たちの仕事であって、そうであれば「手伝う」などという発想はでてこないはずだ、と。…だからといって、ほかにど…

わかっちゃいるけど、どうしてもごめんなさいと言ってしまう。「疲れて帰って、それから休む暇もなく夕飯を作って食べさせて、大変だったんだから…」これがあかの他人のことばだったら、「うーん、そりゃあほんとに大変だねえ」などと返せる、というか、それ…

トレーニングで emacs というマニアックなエディターを使わざるをえず、ばかりか UTF-8 で日本語が埋め込まれた文書が渡され、開いてみたら、ところどころカナ交じりの、ほとんどエスケープされた数字の羅列という悲しい状態に。いろいろ漁って ~/.emacs に…

uncurry なる関数が Excercise に出てて、コリャなんだ？と疑問符が頭の中を飛び交い中。とりあえず型を問い合わせてみた。ついでに uncurry があるなら curry もあるのか？って。あった。 Prelude> :t uncurry uncurry :: (a -> b -> c) -> (a, b) -> c Pre…

http://msdn.microsoft.com/en-us/library/ms175759(VS.80).aspxマクロが三つあって、結局のところそれぞれどれがどうなるんだ？というのがようやっと腑に落ちた。規定で有効になっている _CRT_SECURE_CPP_OVERLOAD_SECURE_NAMES は、追加された _s 系関数に…

10 章の DETAILS に "The operator ($) is …. In other words it is the ``apply'' operator" という記述を発見。なんと！ ($) は apply だったのかっ！Exercise 9.4 のことをおもいだし、うわ、こんな簡単な答えになるよってんで感動。 applyEach fs v = ma…

fix 関数の型はどんなものかってのと、 fix を使って remainder を再帰でない形に書き直しなさいって問題。 fix と remainder の定義はそれぞれ以下のとおり: fix f = f (fix f) remainder :: Integer -> Integer -> Integer remainder a b = if a < b then …

9.1 Curring, More About Higher-Order Functions, "Haskell School of Expression" から引用。 This method of applying functions to one argument at a time, yielding intermediate functions along the way, is called currying, after the logician Ha…

foldl の型は: foldl :: (a -> b -> a) -> a -> [b] -> aこれの第一引数を foldl で束縛しようとすると何が起きるかを考えてみる。第一引数に束縛できるはずなので foldl を (a -> b -> a) にマッチさせなければならない。 foldl の型を三つの部分に分解する…

SOE の Exercise 5.2 は、部分適用済み高階関数の型を問う問題。 map map foldl foldl map foldl公式サイトの Errata に foldl foldl は principal type がなかったごめんという訂正があったので実質二問。いずれにせよ、さらっと流せない難しい問題と感じた…

The Haskell School of Expression (通称 SOE) という書籍を大購入して読み中。なかなか楽しい。http://www.haskell.org/soe/software1.htm にて SOEGraphics (旧称) モジュールの最新版が配布されている。インストラクションにしたがって 6.8.2 Haskell を…

ZeroMemory や CopyMemory などの Win32 API は CRT (C Runtime Library) の呼び出しに置き換えられる模様です。 // Winbase.h より抜粋 #define MoveMemory RtlMoveMemory #define CopyMemory RtlCopyMemory #define FillMemory RtlFillMemory #define Zero…

1>entry.obj : error LNK2019: unresolved external symbol ___security_cookie referenced in function _wWinMain@16 1>entry.obj : error LNK2019: unresolved external symbol @__security_check_cookie@4 referenced in function _wWinMain@16 1>entry.o…

; a. (define outliner (segments->painter (list (make-segment (make-vect 0 0) (make-vect 1 0)) (make-segment (make-vect 1 0) (make-vect 0 1)) (make-segment (make-vect 0 0) (make-vect 0 1)) (make-segment (make-vect 0 1) (make-vect 1 0))))) ;…

(define (make-segment o v) (list o v)) (define (start-segment s) (car s)) (define (end-segment s) (add-vect (car s) (cadr s)))

リストによる実装に対するセレクター: (define (origin-frame f) (car f)) (define (edge1-frame f) (cadr f)) (define (edge2-frame f) (caddr f)) cons による実装に対するセレクター: (define (origin-frame f) (car f)) (define (edge1-frame f) (cadr f…