はてなブックマーク

第２回です。前回は「forall」と「->」の扱い方でした。今回は、「ならば (->)」以外の定番の論理演算、「and」「or」「not」のお話です。 実は、Coq の本当に言語組み込みの命題構成子は forall と -> だけで、「and」「or」「not」は、Coq使いなら自分で同じ機能のものを簡単に作れてしまう「ユーザー定義命題」です（もちろん、共通のものがないと不便なので標準ライブラリで真っ先に定義されてますけど）。逆に言うと、もっと本格的なCoqコードで出てくる複雑そうな命題も、全部、「and」「or」「not」と同じユーザー定義型の仕組みで定義されてますので、「and」「or」「not」の扱いさえマスターすれば、他のどんなユーザー定義の命題の証明も同じ道具で書けちゃいますよ。

証明支援系Coqの遊び方の入門を書いてみるよ。すでに世の中に何個も入門記事ありますけど、増えて困ることはなかろう…ということで。まず、インストール方法については、id:yoshihiro503 による紹介記事 http://d.hatena.ne.jp/yoshihiro503/20070706#p1 最近パソコンを買ったんだけど、使い方がよく解らない。という人のために、今日はCoqのインストールの方法を紹介しよう。 を参照のこと。現時点では最新の安定版の Coq 8.2 がおすすめ。

適当にまったりと。今回は下準備みたいなものだけです。 入力 せっかくなのでデータ形式は SAT Competitions の形式と揃えておこうかと思いました。出せるようなものはとても作れないですけど、比較する時にその方が便利そう。 まず、入力はConjunctive Normal Formの論理式で与えるとのこと。 (x1 or !x5 or x4) and (!x1 or x5 or x3 or x4) and (!x3 or !x4)こういう、『「変数か変数の否定 (= リテラル)」をorで繋いだもの (= 選言節)』をandで繋いだもの、という形の式です。ファイル形式としては、DIMACS形式というので与えられるらしい。こんなテキストファイルです。 c c コメント〜 c p cnf 5 3 1 -5 4 0 -1 5 3 4 0 -3 -4 0 最初に何行かコメント (c XXXX

RealLibの実装がどういう原理になってるのか解明しようシリーズです。シリーズといいながら、読み始めてみたらかなりシンプルだったので1回で終わらせちゃいます！ 実数オブジェクトの構造 // Real.h class Real { private: RealObject *m_pObject; ... }; 普段ユーザーが直接さわる Real クラスは、RealObject クラスを単純にラップしたものになっています。RealObject は、計算式の形をそのままツリー状に表現するためのクラスです。 // RealObject.h class RealObject { ... protected: virtual Encapsulation Evaluate() = 0; public: Encapsulation GetEstimate(); ... virtual RealObject

RealLib のソースコード読みを始めるはずだったんですが、なんだか全然進んでないので適当なまとめエントリでお茶を濁します！ RealLib が普通にかっこよすぎるので紹介しまくりたくなりましたので紹介記事です。 実数計算と誤差 たいていのプログラミング言語の「実数 = 浮動小数点数」の計算には「誤差」があります。たとえばPythonのばあい： Python 2.5 (r25:51908, Sep 19 2006, 09:52:17) [MSC v.1310 32 bit (Intel)] on win32 Type "help", "copyright", "credits" or "license" for more information. >>> 0.1 + 0.1 + 0.1 - 0.3 5.5511151231257827e-017 0.1 を 3 回足しても 0.3 にはな

ここ「ひとり勉強会」は、会と言いつつひとりで勉強した記録を残してます。 今度は The Programming Language Lua のソースコードを読みます 履歴 (0): 参考資料まとめ (1): データ構造。main から VMメインループまで (2): スタック構造や命令フォーマットCALL/RETURN (3): 演算子・ジャンプ・ループ・クロージャ (4): コルーチン・環境 成果物 LuLu : Lua VM on Lua @ LuaForge LUAソースコード勉強会は2008/06/08に無事終了しました。

こちらで見かけた話題・・・ http://natu.txt-nifty.com/natsutan/2008/06/vm_e3c7.html http://shinh.skr.jp/m/?date=20080624#p01 Lua の VM は 4.0 でのスタックマシンから 5.0 でレジスタマシンに変更されたらしく、その時の理由が Lua: papers の "The implementation of Lua 5.0" の 第 7 節 にいくつか書いてありました。そこで書いてあることには・・・、の前に Lua 5.0 の「レジスタ」の仕様を簡単にまとめるておくと、こんな風になってます。 レジスタは最大 256 本 ローカル変数１つにつきレジスタ１本割り当てる 高度なレジスタ割り当ては一切ナシ 実機のレジスタに対応づけることも考えられていない ローカル変数が 200 個以上ある関数を定義

今日は、LuaのVMに使われてるデータ構造をさささっと眺めてみます。 あと、mainからはじまってVMのメインループに到達するまでの流れを確認しちゃいます。 値を表すデータ構造 // lua.h #define LUA_TNIL 0 #define LUA_TBOOLEAN 1 #define LUA_TLIGHTUSERDATA 2 #define LUA_TNUMBER 3 #define LUA_TSTRING 4 #define LUA_TTABLE 5 #define LUA_TFUNCTION 6 #define LUA_TUSERDATA 7 #define LUA_TTHREAD 8 // lobject.h typedef union { GCObject *gc; void *p; lua_Number n; int b; } Value; ... #define TV

これで今日のYARV勉強会はおしまいです。 って、これではやけに短くなってしまったので、おまけとして、るびま で触れられていた 本当は、今回何か簡単な言語のコンパイラを作ろうと思っていたのですが、間に合いませんでした。誰か Scheme あたりで挑戦してみませんか。かなり簡単だと思いますよ。 これをやってみようと思います。 yasm.rb 記事で紹介されているyasmモジュールがRubyのtrunkに見つからなかったので、旧YARVのレポジトリ http://www.atdot.net/svn/yarv/trunk/lib/yasm.rb から拾ってきて適当に修正して使っています。変えたのは、YARVの仮想マシンオブジェクトを表すクラス名と - module YARVCore + class VM - YARVCore:: + VM:: メソッド名としてSymbolを渡すと怒られるみたいだ