存在の証明 1
Coqをインストールしたので
http://d.hatena.ne.jp/qnighy/20101220/1292829222
この辺を参考に勉強中です。
ついでに自分で命題を考えて証明してみた。
命題は forall (x : nat), x > 1 -> x < x * x. というもの。
こんなもの直感的だろ!
といいたい所ですが、論理学の世界では公理系から演繹(証明)出来ないものは全て不定な存在です。
戦略的にはSearchPatternで (_ < _ * _) を調べ見つけた
mult_lt_compat_r: forall n m p : nat, n < m -> 0 < p -> n * p < m * p
の定理を使う方針で証明していきます。
pをx、nを1、mをxとすると仮定から p n mはnatであり、n < mとなるので定理より命題は成り立ちます。
が、 x < x * x と 1 * x < x * xが同値な命題かどうかを証明しなければなりません。
要は x = 1 * xを証明する必要があります。
証明の途中で仮定化したい補題が発生した場合はassert tacticsでがしがし仮定化し証明していきます。
では証明
Lemma square_is_big: forall (x:nat), x > 1 -> x < x*x. Proof. intros. (* x = x * 1 の証明 *) assert (G: x = x * 1). assert (G1: x * O = O). apply (mult_0_r x). assert (G2: x = x + O). apply plus_n_O. rewrite G2 at 1. assert (G3: x + O = O + x). apply plus_comm. rewrite G3. rewrite <-G1 at 1. apply (mult_n_Sm x O). (* x < x * x を 1 * x < x * x に変換 *) rewrite G at 1. assert (G4: x * 1 = 1 * x). apply mult_comm. rewrite G4. (* x > 1 は仮定に存在しているので,後は仮定にx > 0が必要なので証明 *) assert (G5: x > 0). assert (G6: 1 > 0). apply neq_O_lt. apply O_S. apply (gt_trans x 1 O). exact H. exact G6. (* 条件が整ったので最後の仕上げ *) apply mult_lt_compat_r. exact H. exact G5. Qed.
x = x * 1とか 1 > 0とかの証明が意外に難しかった。
まぁただ欲しい仮定はassertでどんどん証明していくという事を掴めればなんとかなる。
普通に数学の命題を証明する時と同じ思考回路を使うんだけど SearchPatternで公理、定理を検索出来るからかなり便利。
VPSとRailsでサービス開発
先週の3連休、私は家にひきこもって酒を飲みながらemacsの誰得的な記事を書きつつVPSで遊んでいました。
そこで作ったtwitterを利用したサービスが出来るまでの流れをざっくり公開しようかと思います。
作ったサービスは http://stkr.dip.jp/maps 上で公開してます。
twitter idを入力するとI'm atアプリ等でtweetした文書を取得し、だいたいの場所をGoogle map上にプロットします。
このくらいであれば1日もあれば一から作れます(酒があれば)
VPSの登録
世の中には様々なVPSサービスがありますが、今回使用したのはServersMan@VPSというサービスです。
このサービスは月額490円でメモリ256MB(MAX768MB)でHDDが10GBほどのリソースが使え、
root権限もあるのである程度遊ぶには十分な環境と言えます。
このサービスが出た直後は登録するのに1ヶ月待ちとかだったのですが、今なら登録直後に使用出来るのもいいですね。
http://dream.jp/vps/index.html
へ行きお好きなプランを選んで登録してみてください。
登録したメールアドレスに環境情報が送られてきます。
開発環境の設定
rootユーザーで作業するのは何かと危険なのでまずはユーザーを作りましょう。
% ssh -P 3843 root@xx.xx.xx.xx
でログインし、useraddコマンドでユーザーを作成します。
作成したユーザーを以下「user」とします。
次にsshまわりの環境を整えます。
ServersManではsshのポートが標準の22から3843に変わっているので普通にログインしようとしたら上記のように打ち込む必要があるので非常に面倒です。
そこで ローカル(VPS上ではない)の~/.ssh/config ファイルに以下のような設定をします。
Host vps HostName xx.xx.xx.xx Port 3843 User user
HostNameはServerManから与えられた固定IPアドレス、Portがsshのポート番号で、UserがログインユーザーIDです。
この設定をしておくことで
% ssh vps
と打つだけで済むようになります。
emacsを使っている方はtrampというリモートサーバのファイルを編集出来る機能を設定しておきましょう。
% wget http://ftp.gnu.org/gnu/tramp/tramp-2.2.0.tar.gz % tar zxvf tramp-2.2.0.tar.gz % ./configure --with-contrib % make % sudo make install
.emacs.elに以下を追加
(require 'tramp) (setq tramp-shell-prompt-pattern "^.*[#$%>] *") (setq tramp-default-method "ssh")
設定終了後はemacs上で
C-x C-f /vps:
と入力しましょう。パスワードの入力をするとVPS上のファイルを編集出来るようになります。
Ruby on Railsのインストール&設定
ServerManでRailsが動くようになるまで以下のアプリ群をインストールしてください。
以下の作業はすべてrootで行います。
Ruby関連
# yum install readline-devel openssl-devel zlib-devel # wget ftp://ftp.ruby-lang.org/pub/ruby/1.8/ruby-1.8.7-p299.tar.gz # tar xvzf ruby-1.8.7-p299.tar.gz # cd ruby-1.8.7-p299 # ./configure --prefix=/opt/ruby-1.8.7-p299 # make # make install # ln -snf /opt/ruby-1.8.7-p299/bin/ruby /usr/local/bin/ruby # ln -snf /opt/ruby-1.8.7-p299/bin/rake /usr/local/bin/rake # ln -snf /opt/ruby-1.8.7-p299/bin/irb /usr/local/bin/irb
RubyGems関連
# wget http://rubyforge.org/frs/download.php/70696/rubygems-1.3.7.tgz # tar xvzf rubygems-1.3.7.tgz # cd rubygems-1.3.7 # ruby setup.rb # ln -snf /opt/ruby-1.8.7-p299/bin/gem /usr/local/bin/gem
sqlite関連
# wget http://www.sqlite.org/sqlite-autoconf-3070500.tar.gz # tar xvzf sqlite-autoconf-3070500.tar.gz # cd sqlite-autoconf-3070500 # ./configure # make # make install # gem install sqlite3-ruby mysql dbi dbd-mysql
passenger関連 (railsをapache経由で使用するため)
# gem install passenger # /opt/ruby-1.8.7-p299/lib/ruby/gems/1.8/gems/passenger-3.0.5/bin/passenger-install-apache2-module
apacheの設定
ServerManはデフォルトでApacheが入っているのでconfの設定だけをします。
/etc/httpd/conf/httpd.conf の以下の行のコメントアウトを外します。
NameVirtualHost *:80
起動ユーザーとグループはデフォルトだとdaemonですが、適切なユーザーに変えておきます。
User user Group user
/etc/httpd/conf.d/stokker.confファイルを以下のように作成します。
DocumentRoot /var/www/html/stokker/public ServerName stkr.dip.jp RailsEnv development AllowOverride none Options -MultiViews Order allow,deny Allow from all
DocumentRootはrailsでプロジェクトを作った際に出来るpublicディレクトリを指定します。
/etc/httpd/conf.d/passenger.confファイルを以下のように作成します。
LoadModule passenger_module /opt/ruby-1.8.7-p299/lib/ruby/gems/1.8/gems/passenger-3.0.5/ext/apache2/mod_passenger.so PassengerRoot /opt/ruby-1.8.7-p299/lib/ruby/gems/1.8/gems/passenger-3.0.5 PassengerRuby /opt/ruby-1.8.7-p299/bin/ruby
apacheを再起動します。
でrailsが生成した画面が表示されている事を確認してください。
Google maps api
http://code.google.com/intl/ja/apis/maps/signup.html
ここでgoogle maps apiを使用するドメインを登録しKEYを取得します。
取得したKEYは以下のように使用します。
<script src="http://maps.google.com/maps?file=api&v=2& sensor=true&key=XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX" type="text/javascript"> </script>
マップは
<div id="map_canvas" style="width: 728px; height: 400px"></div>
というdiv要素上に表示されます。
twitter4r
twitterの発言を取得するのにtwitter4rを使用しました。
% sudo gem install twitter4r
twitter4rをインストールしたら使用するrubyのファイルで以下のように宣言しておきます。
require "rubygems" gem "twitter4r" require "twitter"
公開発言を取得するだけであれば以下のような簡易なコードで取得出来ます。
@MAX_COUNT = 500 @twitterid = ... last_month = Time.now - 60*60*24*30 tw_client = Twitter::Client.new tw_client.timeline_for(:user, :id => @twitterid, :count => @MAX_COUNT).each do |status| created = status.created_at if created > last_month then ... end end
その他
ロゴ
twitter風のロゴは http://www.twitlogo.com/ で作成しました。
LET OVER LAMBDA Reading
昨日の続きでバッククォートでネストされているマクロを追ってみる。
macroexpand-1がマクロを1回分だけ展開する関数なのでこれを使ってみてみよう。
(macroexpand-1 '(defmacro! square (o!x) `(* ,g!x ,g!x)))
このようにmacroexpand-1に展開させたいマクロS式をクォートして渡す。
(DEFMACRO/G! SQUARE (O!X) (LIST 'LET (MAPCAR #'LIST (LIST G!X) (LIST O!X)) (PROGN `(* ,G!X ,G!X))))
展開するとこのようになっていて、これをバッククォートを使って書き換えると
(defmacro/g! square (O!X) `(let ,(mapcar #'list (list G!X) (list O!X)) ,(progn `(* ,G!X ,G!X))))
のようになる。こいつをさらにmacroexpand-1に渡してあげる
(macroexpand-1 '(defmacro/g! square (O!X) `(let ,(mapcar #'list (list G!X) (list O!X)) ,(progn `(* ,G!X ,G!X)))))
展開結果は
(DEFMACRO SQUARE (O!X) (LET ((G!X (GENSYM "X"))) `(LET ,(MAPCAR #'LIST (LIST G!X) (LIST O!X)) ,(PROGN `(* ,G!X ,G!X)))))
このS式でdefmacroにとってのbodyは
`(LET ,(MAPCAR #'LIST (LIST G!X) (LIST O!X)) ,(PROGN `(* ,G!X ,G!X)))
なので展開後は
(LET ((#:X8704 O!X)) (* ,G!X ,G!X))
のようになる。PROGNを包んでいた括弧はアンクォートされたいたので展開時に評価されてなくなり、中のバッククォートされたS式は評価されずにそのまま残る。
だから、昨日言っていた,@なんたらのくだりは解釈の間違いで、バッククォートはそのまま残った形でdefmacroに渡る。
LET OVER LAMBDA Reading
マクロを定義するマクロを定義するには,しばしば入れ子になった逆クォートが必要になる.逆クォートの入れ子は理解し辛いことで悪評が高い.よく使われる形にはいつか慣れるだろうが,逆クォートの付いた任意の式を見て,どのように展開されるかを言えるようになるとは思うべきではない.そうなるのはLispの欠陥ではなく,ましてや表記の欠陥でもない.込み入った積分の数式を見て値が何か知ることができないのと同じことだ.困難は問題の中にあり,表記の中にあるのではない.
http://www.komaba.utmc.or.jp/~flatline/onlispjhtml/macroDefiningMacros.html
LOL リスト2.6 & リスト2.8
(defmacro defmacro/g! (name args &rest body) (let ((syms (remove-duplicates (remove-if-not #'g!-symbol-p (flatten body))))) `(defmacro ,name ,args (let ,(mapcar (lambda (s) `(,s (gensyms ,(subseq (symbol-name s) 2)))) syms) ,@body)))) (defmacro defmacro! (name args &rest body) (let* ((os (remove-if-not #'o!-symbol-p args)) (gs (mapcar #'o!-symbol-to-g!-symbol os))) `(defmacro/g! ,name ,args `(let ,(mapcar #'list (list ,@gs) (list ,@os)) ,(progn ,@body)))))
Paulはこんな感じのマクロを理解するのは積分を解くのと同じって事を言いたいのか?
言いたい事はなんとなく分かるが積分の方が100倍楽だと思うね僕は。
バッククォートはアンクォート(,)が無ければただのクォート。つまり評価しないって識別子と考える。
内側のバッククォートは評価されないと考えると最初のdefmacro!の展開は
(defmacro/g! name args `(let ,(mapcar #'list (list '(gs1 gs2)) (list '(os1 os2))) ,(progn body)))
みたいになる(o!-symbol-pを満たすargsが2個の場合と仮定) たぶん。。
defmacro/g!に渡されるbody部分が
`(let ,(mapcar #'list (list '(gs1 gs2)) (list '(os1 os2))) ,(progn body))
でこれをdefmacro/g!に適用するんだけどgs1とgs2がgensymで生成された変数に変換される。
でもbodyのところにバッククォートが残るな。。
わからない寝よう
いや、まて
,@bodyの,@って「継ぎ合わせアンクォート」って読み方で別に特殊な記号じゃない。ただのアンクォートだ。
って事はdefmacro/g!からの展開した時のbodyは
(let ,(mapcar #'list (list '(gs1 gs2)) (list '(os1 os2))) ,(progn body))
が正解だね、たぶん。
これからdefmacro/g!全体
(defmacro defmacro/g! (name args &rest body) (let ((syms (remove-duplicates (remove-if-not #'g!-symbol-p (flatten body))))) `(defmacro ,name ,args (let ,(mapcar (lambda (s) `(,s (gensyms ,(subseq (symbol-name s) 2)))) syms) ,@body))))
の,@bodyにさっきのbodyが渡る。
って事は展開すると
(defmacro name args (let ((#:X1633 os1) (#:X1634 os2)) (progn body)))
のようになる。ふむ、これは正しい。
最後の方の解釈が間違えてる。 今夜再思考しよう。
On Lisp
Paul GrahamのOn Lispの訳ってネットで公開されてたんだね。
知らなかったよ。http://www.komaba.utmc.or.jp/~flatline/onlispjhtml/
最近買ったDoug HoyteのLET OVER LAMBDAによく引用が出てきていたから、ちょっと読んでみようかな。
複数call/ccに対応
GitHub - sodeyama/slisp: lisp interpreter
sLispの以下の点を改善しました。
- コメントを可能にしました
- call/ccで生成するラムダ式で使う変数名をgensymで作るようにしました(変数名の衝突を防ぐ目的)
- call/ccを複数書けるようにしました。(ただし、トップレベルの各S式中に1つのみ)
- slisp-mode(emacsメジャーモード)。ファイル開いてC-c nで評価
各々の対応するコードは以下
コメント
(defun slisp-get-src-string (filename) (let ((pre-buffer (current-buffer)) (ret "")) (find-file filename) (setq str (buffer-substring-no-properties (point-min) (point-max))) (let ((lines (split-string str "\n"))) (dolist (line lines) (if (not (string-match "^;" line)) (setq ret (concat ret line))))) (switch-to-buffer pre-buffer) ret))
ファイルを開いたバッファからslisp-get-tokensに渡す文字列を生成する段階でコメント行を排除。
call/ccで生成するラムダ式で使う変数名をgensymで生成
(defmacro with-gensyms (syms &rest body) (declare (indent 1)) `(let ,(mapcar (lambda (sym) `(,sym (gensym))) syms) ,@body))
Common Lispでよく使われるwith-gensymsをelispのmacroで再現してます。
(with-gensyms (a b c) body)
のようなコードは
(let ((a (gensym)) (b (gensym)) (c (gensym))) body)
に展開されます。gensymは一意なシンボルを生成するelispのmacro。
call/ccを複数書けるように
(defun slisp-callcc-parse (exp env) (dolist (seed (cdr exp)) (with-gensyms (variable) (let* ((ret (slisp-callcc-getcc seed variable env)) (find (slisp-get-findcallcc ret)) (cc (slisp-get-callcc ret))) (if find (progn (let ((sexp (list "lambda" (list variable) (list "throw" cc)))) (slisp-callcc-fifo-set sexp))))))))
slisp-callcc-fifoをcall/ccで生成された継続を保存するfifoデータとしslisp-callcc-fifo-set, slisp-callcc-fifo-getでセット、ゲットしただけ。