Lean Proverのuniverse polymorphismの罠

このようなコードをLean Proverで検査しようとすると、補題test2でエラーが出る。1

gist.github.com

いくら考えても原因がわからなかったのでGitHubのレポジトリにバグとして報告したところ、バグではなく仕様である、という返答を頂いた。 github.com

ここに書いてあることを要約する。constant t: Sort uと宣言すると、宇宙uごとに型t.{u}: Sort uができ、constant f: t -> tという宣言によって、 宇宙のペアu,vそれぞれに対しf.{u v}: t.{u} -> t.{v}ができる。

この状態でf x = f xという式の型付けおよび型検査を行うと、もっとも一般的な型付けは@eq.{v} t.{v} (f.{u1 v} x.{u1}) (f.{u2 v} x.{u2})である(v,u1,u2は宇宙、返答にあるものとは名前を変えている)。等式の左右で型が等しいという条件はあるが、中身の関数およびその引数の型が等しいという条件はないことに注意。変数f, xのパラメータとなる宇宙が違うため、両辺が構文的に等しくなくなってしまい、reflexivity tacticが失敗したのである。(補題testではreflexivityが成功するが、これはx = xの型付けを行うと@eq.{u} t.{u} x.{u} x.{u}となるためである。)

この問題の解決法は2種類ある。1つ目はissueの返答にも書いてあるように、universe polymorphismを使うのをやめ、t: Typeと宣言することである。もう一つは、universe polymorphismを使うが、問題となる全ての変数について、それのパラメータとなっている宇宙を指定することである。例えば以下のコードは正しく検査される。 gist.github.com

なお、この手の問題を解決するには、pretty printingの設定を変えるのが有効である。set_option pp.all trueを実行すれば、エラーメッセージやgoalの表示などで詳細な情報を表示してくれる。


  1. 実はlemmaではなくexampleとして証明するとエラーが出ない。原因は不明である。set_option pp.all trueを使ってもよく分からない。

Lean Proverのinaccessible termについて

最近Lean Prover (Lean 3)で原始再帰的関数について証明を書いているので、それによって得られた知見を一つ紹介する。

gist.github.com


inaccessible termとは何か

".(項)"の形のパターンはinaccesible termと呼ばれ、パターンマッチを行う際に、この部分はパターンとしてではなく、項として一致するかどうかの検査が行われる。(つまり、パターン以外の項が書ける。)
項の部分は同じパターン内ですでに定義されている変数でなければならない。項の内部で新しい変数を導入することはできない。

使用例

埋め込んだコードのprim_evalの定義(ll. 36-48)でパターンマッチを行なっているが、これのl.40, l.42で使用されている。
典型的な使用例として、同じ値が複数個出現することがわかっているパターンマッチ(l.40のマッチングではmが2回登場する)で使用できる。(パターン内で同じ変数名を複数回使うことはできない。)
また単にパターンが複雑になってしまったり、マッチさせなくても自動で推論できる場合にマッチを省略する目的でも使用できる。(l.42のマッチングでは".(_)"というパターンがあるが、これはprim_evalの第一引数はk + 1であることが推論できるため合法である。)

なお、ここでの本題とは外れるが、l.40のパターンに含まれている"@prim_rec.prec"の"@"は、@演算子と呼ばれ、implicit parameter (l.5のkとm)を陽に引数にとる、という効果を持つ。これがないとkをパターンマッチさせることができず、この場合はfの型が推論できないというエラーが出る。

参考文献

Theorem Proving in Leanの8.5 Inaccessible Terms (inaccessible terms), 2.9 Implicit Arguments, 6.8 Displaying Information (@演算子)

yukicoder No.551 夏休みの思い出(2)

問題:
No.551 夏休みの思い出(2) - yukicoder

想定解は
https://yukicoder.me/problems/no/551/editorial
だが、原始根を無視してmod_sqrtを使って解いた。
mod_sqrtは(多分)O(log(p)^2)-timeで解けると思う。
gist.github.com

Rustでtreapと2-3 treeを実装してブログを書きました

Rustでtreapと2-3 treeを実装してブログを書きました。

treap: Treap on Rust - Codeforces

2-3 tree: 2-3 tree on Rust - Codeforces

(Codeforcesなので英語です)

機械学習初心者がIndeedの機械学習コンテストに参加した話

Hackerrankの
Indeed Machine Learning CodeSprintに参加しました。

SVMで分類しようと試みましたが、結果は芳しくありませんでした。(175.33/1000点!w)
この得点は、最初すべてのrowに対して"2-4-years-experience-needed"を返す実装を投げたことによって達成されました。そのあと色々試しましたが、これを超える性能を出すことはできませんでした。

やったこと

Job descriptionを何らかの方法でベクトルにして、12種類のタグそれぞれに対して、そのタグがつくかつかないかの2値分類をSVMでやろうと思いました。
文章のベクトル化は、単純に記号を除去し、大文字をすべて小文字にして、単語の頻度を計算することで行いました。
ソース:
gist.github.com

結果

さんざん(説明文を変えてもほとんど線形変換の後のベクトルに差が出ず、全て同じ値に分類された)
以下のスクリーンショットでは、800個ごとに分類結果を表示していますが、class (タグのありなしを+1/-1で表した分類結果)は全て同じで、Ax+b (ソース158行目)の値(classの1行下に表示)もほとんど変化がないという結果になっています。
f:id:koba-e964:20170413132437p:plain

反省

もう少し勉強が必要でした。まだ原因究明ができていないので、他の人のコードを実行したりしながら勉強します。

lighttpd(ライティー)で数独サーバーを作った話

tl;dr: Apacheで数独サーバーを作った話 - koba-e964の日記の続きです。

きっかけ

前回(Apacheで数独サーバーを作った話 - koba-e964の日記)の制作途中でいただいた以下のようなコメントがきっかけで、lighttpdでも作ってみることにしました。


完成品は変わらず
https://sparkle-sudoku-solver.herokuapp.com/
にあります。

概要

http://koba-e964.hatenablog.com/entry/2017/03/11/033819:title:前回Apache 2.4を使っていたところを、代わりにlighttpd (バージョンは現在apt-getで手に入る1.4.33)を使って作りました。
これにより、完成品のDocker imageの大きさが628MB (Apache版) -> 356MB(lighttpd版)になり、大幅に軽量化できました。
https://sparkle-sudoku-solver.herokuapp.com/から遊べます。

バージョン情報:

root@87a939323768:/# lighttpd -v
lighttpd/1.4.33 (ssl) - a light and fast webserver
Build-Date: Jan 28 2014 17:26:04
root@87a939323768:/# date
Sun Mar 12 15:19:00 UTC 2017

imageのサイズ:

$ docker images sparklenumberplace_lighttpd
REPOSITORY TAG IMAGE ID CREATED SIZE
sparklenumberplace_lighttpd latest 5f5683b70260 10 hours ago 356 MB
$ docker images sparklenumberplace_web
REPOSITORY TAG IMAGE ID CREATED SIZE
sparklenumberplace_web latest 797b93561b96 23 hours ago 628 MB

記事執筆時点でのソース:
GitHub - koba-e964/sparkle-number-place at a30029f7cfc4897b9fbcc2eaa26f52356512ca5e

ハマったポイント

  • 起動スクリプト(start-lighttpd.sh)を/tmp/以下において、CMDで実行しようとしたら、手元では動くもののheroku上では動かないという事態になりました。これはおそらく、docker imageのビルド時に見える/tmp/とheroku上で書き込みできる/tmp/が異なる場所を指しているためだと思われます。(herokuは一時ファイル保存のため、/tmp/以下にのみファイルの書き込みを許しています。 *1 参考: Stack Overflowの質問)
    結局起動スクリプトを/tmp/ではなく/opt/に配置することにして解決しました。
  • Dockerfileの仕様で、Dockerfileの配置してあるディレクトリの外のファイルは参照できないのですが*2、この仕様のせいでサーバーごとにディレクトリを分割することと共通のファイルを再利用することが両立できませんでした。ここではDockerfile.*という名前のファイルにdocker scriptを書き、docker-compose.ymlでサーバーごとに参照するDockerfileを変えることにしました。なおこの方法だとheroku container:pushができない(Dockerfileという名前のファイルを参照するため)ので、push用のスクリプトpush-lighttpd.shを用意することにしました。*3

今後やりたいこと

  • lighttpd版で使うLinux distributionを特に何も考えずUbuntuにしましたが、他のdistributionだとどのくらい軽量化できるのかが気になります。またApache版はDebianだったので、Debianでもやってみて公正な比較をしてみたいと思っています。
  • 前回の「今後やりたいこと」はまだできていないので、それらにも取り組みたいと思っています。

*1:heroku上のファイルシステムはephemeralなので、一度作ったテンポラリファイルがずっと残っていることを前提にプログラミングをしてはいけません。(dynoが停止または再起動するタイミングで消えます。) またファイルシステムはdynoごとに作られるので、/tmp/を介して別のdynoと通信をすることはできません。参考: 公式Herokuで一時ファイル保存 - 木木木

*2:GitHubのissueで議論がされているので、興味があったら是非読んでみてください。

*3:DockerfileをDockerfile.lighttpdへのsymbolic linkにして、herokuの目を欺くやり方です。こんな小手先の対策とりたくなかったです…

Apacheで数独サーバーを作った話

tl;dr: Apache + Dockerでサーバーを作ってherokuにdeployしました。ソルバーは
https://sparkle-sudoku-solver.herokuapp.com/
にあります。

作ったもの

数独パズルを解く、Web上で動くソルバーを作りました。(https://sparkle-sudoku-solver.herokuapp.com/)
0から9までの数字を9行に81個空白区切りで並べたものを与えると、それを数独パズルとみなして、可能な解を一つ返します。*1
この記事を書いた時点でのソースはここにあります。

ソルバー

ソルバーは以前書いてあったものを流用しました。数独のパズルを受け取ってCNFの論理式に変換し、minisatに投げて結果(充足する真偽値割り当て)を受け取り、そこから解となる盤面を計算します。今回はナイーブな実装を行ったので、どんな場合でも729変数、3240節のCNFになります。ソースはgen-cnf.rbです。
追記(3/11 12:21): SATソルバーについてはProgramming on SATというわかりやすい記事があります。

サーバー

サーバーはApache 2.4を使用しました。Docker imageをここから取得して、その上にrubyとminisatをインストールしてサーバーを起動します。Dockerfile
最小のコストでCGIサーバーを動かすことを目標にしてソフトウェアを選びました。*2これより簡単な方法でサーバーを作る方法をご存知の方は、教えていただけるとありがたく思います。

最終的に作ったdocker imageをherokuにデプロイすることでheroku上でサーバーが動くようになります。heroku container:pushを実行した時の出力は次のようになります(ソースより前のバージョンのpushなので、ソースとの整合性はありません):

$ heroku container:push
Sending build context to Docker daemon 186.4 kB
Step 1/13 : FROM httpd:2.4
---> f316d5949bb0
Step 2/13 : ENV MINISAT_VERSION 2.2.0
---> Using cache
---> 8b96b7e5836c
Step 3/13 : RUN apt-get update && apt-get install -y curl g++ gem make ruby yum zlib1g-dev
---> Using cache
---> 01c356dcace4
Step 4/13 : RUN curl -L http://minisat.se/downloads/minisat-${MINISAT_VERSION}.tar.gz >/tmp/minisat-${MINISAT_VERSION}.tar.gz && cd /tmp && tar zxf minisat-${MINISAT_VERSION}.tar.gz
---> Using cache
---> 420f926984f1
Step 5/13 : RUN cd /tmp/minisat && export MROOT=`pwd` && cd core && make rs && cd .. && cd simp && make rs && cd .. && cp -p core/minisat_static /usr/local/bin/minisat22_core && cp -p simp/minisat_static /usr/local/bin/minisat22_simp
---> Using cache
---> 66a7d907bc81
Step 6/13 : RUN cd /usr/local/bin && ln -s minisat22_core minisat
---> Using cache
---> 3e81832a1ba6
Step 7/13 : RUN sed -ri 's/#LoadModule cgid_module/LoadModule cgid_module/g; s/Options Indexes FollowSymLinks/Options Indexes FollowSymLinks ExecCGI/g; s/#AddHandler cgi-script .cgi/AddHandler cgi-script .rb .pl .cgi/g' /usr/local/apache2/conf/httpd.conf
---> Using cache
---> 93ac06565e51
Step 8/13 : EXPOSE 80 80
---> Using cache
---> 31dea6708dd8
Step 9/13 : COPY files/gen-cnf.rb /usr/local/apache2/htdocs/gen-cnf.rb
---> 89a66d1a6689
Removing intermediate container dc206958f995
Step 10/13 : RUN chmod a+x /usr/local/apache2/htdocs/gen-cnf.rb
---> Running in 7dd0626c9d96
---> 1064c2ac079f
Removing intermediate container 7dd0626c9d96
Step 11/13 : COPY files/handler.rb /usr/local/apache2/htdocs/handler.rb
---> 46c1ed0f2dda
Removing intermediate container fb6381e4e384
Step 12/13 : RUN chmod a+x /usr/local/apache2/htdocs/handler.rb
---> Running in ca1a7fa67491
---> 7af09916047e
Removing intermediate container ca1a7fa67491
Step 13/13 : COPY files/index.html /usr/local/apache2/htdocs/index.html
---> 1e7a71852b93
Removing intermediate container f93929edeec6
Successfully built 1e7a71852b93
The push refers to a repository [registry.heroku.com/sparkle-sudoku-solver/web]
68422698f5cc: Pushed
af543c01d744: Pushed
5cfa10e2d863: Pushed
81cafbc89c7a: Pushed
d7ffb6f22450: Pushed
38625d3b26b6: Pushed
3aba0ea84b6e: Pushed
5f0c09555780: Pushed
e39e2811255e: Pushed
9ce897855b2e: Pushed
e62aea9889eb: Pushed
efe6d8194a9f: Pushed
d4d164dfebb6: Pushed
cd0e01770f2a: Pushed
9feccb840a3a: Pushed
c86b3fdc78cf: Pushed
d17d48b2382a: Pushed
latest: digest: sha256:8a060a2ceba13a4db2fe25106025dcdbcc8c3b9133fe65515979f223d5c48de2 size: 3867

ハマったポイント

試行錯誤を繰り返していたので、ハマったポイントは無数にあるのですが、その中でも知識があれば大幅に時間を短縮できたポイントを挙げます。

(1) JavaScriptjQueryをインポートしたのですが、herokuはhttpsでページを提供しているのにjQueryのライブラリをhttpで参照していて、

Mixed Content: The page at 'https://sparkle-sudoku-solver.herokuapp.com/' was loaded over HTTPS, but requested an insecure script 'http://ajax.googleapis.com/ajax/libs/jquery/1.8.1/jquery.min.js'. This request has been blocked; the content must be served over HTTPS.

というエラーが発生していましたが、なかなか気づけませんでした(サーバーの不具合だと思っていました)。参考: teratailの質問

(2) herokuの仕様で、開くポートは80番ではなく、heroku側で動的に決定され環境変数$PORTに渡されるのですが、これをどうやってApacheサーバーに渡せばよいかわからず苦労しました。そもそも何を満たすべきだったかというと、

  1. Dockerfile内のCMD文の直前までは、$PORTに依存せずにビルド可能である
  2. CMD文で実行されるファイルは、$PORTを受け取って$PORT番で指定されたポートをlistenすることができる

の2点を満たす必要がありました。これを満たすために、httpd.confの設定はDockerfileの内部では行わず、最後にCMD文で実行されるスクリプト(start-server.sh)でhttpd.confの設定を行う、という形にしました。この形にすると、ローカルでのテストもやりやすくなります。(docker-compose.ymlの中でenvironment: PORT=80と設定すれば良いため)
参考: Container Registry and Runtime | Heroku Dev Center (公式ドキュメント)


(3) Dockerfileの設定について
途中まで、Dockerfileにいきなりコマンドを書いてトライ&エラーを繰り返す、というやり方で開発していたのですが、これは非効率的でした。試行錯誤する場合は、ベースイメージを起動して内部でシェルを起動し、その中で試行錯誤を繰り返すほうが効率的です。参考: 効率的に安全な Dockerfile を作るには - Qiita

今後やりたいこと

  • いずれ画像認識の機能もつけることを目標にしています。数独パズルの盤面を撮影した写真を読み込めるようにする機能をつけたいと思っています。
  • パフォーマンスの測定をまだ実装していないので、測定機能をつけようと思っています。また、minisatのconflictやpropagationの回数で数独パズルの難易度を測れそうなので、これらのパラメータも表示するようにしたいです。
  • 数独はCNFへの変換が比較的容易なので、今後はカックロなどの、よりCNFへの変換が難しい問題のWebソルバーを作ることも目標です。

*1:解が存在しない場合の挙動は未定義です。いずれ直したい…

*2:最初はnginxとか使おうとしてたんですがCGIを動かすのが大変すぎて数時間溶かしたのでやめました。