ウォンツテック

そでやまのーと

Deep Learning

Deep Learningの勉強

今日からO'REILLYの「ゼロから作る Deep Learning」を読み始めます。

ブラックボックスは極力使わずにゼロから積み上げるコンセプトが気に入りました。

python 3系のインストール

本で使用しているpythonのversionは3系で、手持ちのmacbookはpython2だったのでupgradeしておく

環境を切り替えられるようにpyenvのインストール

brew install pyenv

.zshrcに以下を追記して読み込み

export PYENV_ROOT="$HOME/.pyenv"
export PATH="$PYENV_ROOT/bin:$PATH"
eval "$(pyenv init -)"

インストール可能なlistの表示

pyenv install --list

本推奨のanacondaをインストール

pyenv install anaconda3-2.4.0

anacondaをインストールする事によって本書に必要なNumPyとMatplotlibもインストールされるとの事

インストールの確認

環境の切り替え

pyenv global anaconda3-2.4.0

確認

python --version

こんな感じに表示されればOK

Python 3.5.0 :: Anaconda 2.4.0 (x86_64)

ヤフオクAPIラッパーを作ってgemに登録してみた

ここ最近

暇つぶしで、嫁のやってる事を楽にするための超嫁得Webサービスrailsで立ち上げて遊んでました。

yahooが提供しているヤフオクapiをごにょごにょしていい感じに表示させるWebサービス(ユーザーは嫁のみ)なんですが

http://developer.yahoo.co.jp/yconnect/

このyconnectを使ってoauthで認証する系のAPIの使い方が分からなくて手こずってました。

omniauthってので認証してaccess tokenをゲットするまではある程度すんなり出来たけど、その先のtokenを使ってどうやってAPI叩けばいいの?ってのに嵌りました。

認証が必要ない場合のAPIを叩くgemはあったんですが、認証が必要な場合のが無かったので自分で作ってついでにgemとして登録してみました。

https://rubygems.org/gems/yahoojp-auction-api

ただのラッパーなんだけど慣れてないとこんな情報あるだけで助かるんですよ。

配列(リスト)の逆順に関する性質の証明

https://gist.github.com/4243787

最近、プログラマの採用面接で解かす問題集みたいな本が出て
その中に「ある配列がユニークであるかどうかを示すコードを書け」という問いがあり、Coqで書いてみました。
下記のようなコードになるんだけどついでに配列を逆にした場合も結果は同じであろうという直感を証明しようと思ったらすごく嵌りました。

Require Import Bool.
Require Import Lists.List.
Require Import String.
Require Import Ascii.

Definition eqc (x y : ascii) : bool :=
  if ascii_dec x y
    then true
    else false.

Fixpoint list_of_string (s : string) : list ascii :=
  match s with
  | EmptyString => nil
  | String c s => c :: (list_of_string s)
  end.

Fixpoint contain (c : ascii) (chars : list ascii) : bool :=
  match chars with
    | nil => false
    | x :: xs =>
      if eqc x c then
        true
      else
        contain c xs
  end.

Fixpoint snoc (l: list ascii) (v: ascii) : list ascii :=
  match l with
  | nil => v :: nil
  | h :: t => h :: (snoc t v)
  end.

Fixpoint rev (l: list ascii) : list ascii :=
  match l with
  | nil => nil
  | h :: t => snoc (rev t) h
  end.

Fixpoint uniq_i (chars : list ascii) : bool :=
  match chars with
    | nil => true
    | x :: xs => 
      if contain x xs
        then false
        else uniq_i xs
  end.

Definition uniq (str : string) : bool :=
  uniq_i (list_of_string str).

配列の先頭に付与する場合は帰納法で素直に解けるんですが、appendする場合は素直にいかない。
パターンマッチさせる場合 x::xsのように先頭でマッチさせるような関数を書いているのが原因だけど、配列の後尾から帰納的証明が行えるような機能が必要に思う。

証明は配列にappendした際の性質 in_app_or_congtain がキモ。

(* 配列に要素をappendした際の重要な補題 rev系の証明では必須 *)
Lemma in_app_or_contain:
  forall (l : list ascii) (a b : ascii),
    contain a (snoc l b) = (contain a l) || eqc b a.
Proof.
  intros l b a.
  induction l.
  simpl.
  case (eqc a b).
  reflexivity.
  reflexivity.
  simpl.
  rewrite -> IHl.
  case (eqc a0 b).
  reflexivity.
  reflexivity.
Qed.

証明の全容は
https://gist.github.com/4243787
にあります。
最後の定理が目的のものです。

存在の証明 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でサービス開発

http://stkr.dip.jp/maps

 先週の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で行います。

コンパイラ関連
 # yum install gcc glibc gcc-c++
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
mysql関連
 # yum install mysql-server
 # yum install mysql-devel 
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
Rails関連
 # gem install rails
 # ln -snf /opt/ruby-1.8.7-p299/bin/rails /usr/local/bin/rails
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関連 (railsapache経由で使用するため)
 # gem install passenger
 # /opt/ruby-1.8.7-p299/lib/ruby/gems/1.8/gems/passenger-3.0.5/bin/passenger-install-apache2-module
railsでプロジェクトを作成する
 # cd /var/www/html
 # rails new stokker
 # cd stokker
 # rails generate scaffold maps
 # rake db:migrate
rails ルーティングの定義 (stokker/config/routes.rb)
  match 'maps/hoge' => 'maps#hoge'
  match 'maps/hoge/:twitter_id' => 'maps#hoge'

scaffoldで作ったmapsコントローラに新しいメソッドを定義した場合、ルーティングが通って無いのでそのメソッドを使用したリンク等をクリックするとエラーとなります。
上記のように適宜ルーティング定義を追加します。

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を再起動します。

http://xx.xx.xx.xx/

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&amp;v=2&amp;
 sensor=true&amp;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)))

のようになる。ふむ、これは正しい。


最後の方の解釈が間違えてる。 今夜再思考しよう。