ipc_botの紹介

この記事はTheorem Prover Advent Calendarの22日めの担当記事です．

今年の僕の持ちネタの一つですが，ipc_bot というTwitter botを作りました．

https://twitter.com/ipc_bot

このbotは直観主義命題論理の命題を投げると解いてくれるbotです．

仕組み

証明を探すのは適当にやっても出来るのですが，証明が存在しないことを確認するのは結構大変です．

(古典論理の場合は与えられた命題の否定をSATソルバーにかければ正誤がわかりますが，直観主義論理命題論理だとそう簡単ではありません)

証明が存在するかどうかを有限時間内で判定するには，推論規則を色々いじる必要があります．しかしその説明をはてなブログで書くのが面倒になってしまったので過去に某所に寄稿したものを見て下さい． http://www.tsg.ne.jp/buho/305/buho305.pdf [PDF]

ソースコード

ソースコードはここにあります．

その他の応用例

Coqのtautoがこのような決定アルゴリズムを使っているようです．

試しにそこそこ複雑な命題を投げても，きちんと答えを返してくれます．

Goal forall P Q R S:Prop,
  ~~((P <-> (Q <-> (R <-> S))) <-> (((P <-> Q) <-> R) <-> S)).
Proof.
  tauto.
Qed.

Goal forall P Q R S:Prop,
  (P <-> (Q <-> (R <-> S))) <-> (((P <-> Q) <-> R) <-> S).
Proof.
  try tauto. (* fail *)
Abort.

形式的証明

かつて形式的証明を書いたことがあります．

また，Coqのcontribにも検証済みの証明探索アルゴリズムがあります．こちらについては未確認ですが，OCamlへの抽出もできるようになっており，かなりよく出来ていることが推察されます．

まとめ

随分と雑な記事になってしまってすみません．来年は精進します．

お詫びに，おもちゃの定理証明器に線形型を加えたものへのリンクを貼っておきます．

まだ型検査器しか作ってないですが一応定理証明器と言えると思います．ですが，おもちゃの定理証明器についてはkikxさんが既に記事にしていたようなのであまり書くことがありませんでした．

以上です．

情報オリンピック予選 2014

情報オリンピックの予選に参加しました．(予選は誰でも参加できます)

次のような制約で解くことにしていました．

  • 1番は Wolf RPGエディター
  • 2番は TeX
  • 3番は Scratch
  • 4番は Excel
  • 5番は APL
  • 6番は Bash

結局1と4を解きました．

1番

Wolf RPGエディターで解きました．たぶん合っていると思います．

https://drive.google.com/file/d/0B0wUgziNPuKGUlZmaG5ka0ZIYUk/edit?usp=sharing

2番

TeXでようやくできました．もしかしたら処理系依存のところなどがあるかもしれません．

手元の環境はTeX, Version 3.1415926 (TeX Live 2013)です．

%\catcode`\@=11
\immediate\write16{}
\def\fstimpl#1 #2\relax{#1}
\def\fst#1{\expandafter\fstimpl#1\relax}
\def\sndimpl#1 #2\relax{#2}
\def\snd#1{\expandafter\sndimpl#1\relax}

\read-1to\NM
\def\N{\fst{\NM}}
\def\M{\snd{\NM}}

\newcount\x
\newcount\y
\newcount\z
\newcount\w
\newcount\k

\x0
{
  \loop\ifnum\x<\N
    \read-1to\tmp
    \global\expandafter\edef\csname costs\the\x \endcsname{\tmp}
    \global\expandafter\edef\csname prefs\the\x \endcsname{0}
    %\immediate\write16{costs[x] = \csname costs\the\x \endcsname}
    \advance\x1
  \repeat
}

\y0
{
  \loop\ifnum\y<\M
    \read-1to\tmp
    \k\tmp
    {
      \x0
      \loop\ifnum\x<\N
        \w\csname costs\the\x \endcsname
        %\immediate\write16{k = \the\k, x = \the\x, w = \the\w, costs[x]=\csname costs\the\x \endcsname}
        \ifnum\k<\w
        \else
          \z\csname prefs\the\x \endcsname
          \advance\z1
          \global\expandafter\edef\csname prefs\the\x \endcsname{\the\z}
          %\immediate\write16{OK! x=\the\x, prefs=\the\z}
          \x\N
        \fi
        \advance\x1
      \repeat
    }
    \advance\y1
  \repeat
}

\x0
\w0
\loop\ifnum\x<\N
  \y\csname prefs\the\x \endcsname
  \z\csname prefs\the\w \endcsname
  \y\csname prefs\the\x \endcsname
  %\immediate\write16{prefs[\the\x] = \csname prefs\the\x \endcsname}
  \ifnum\y>\z
    \w\x
  \fi
  \advance\x1
\repeat
\advance\w1
\immediate\write16{\the\w}
\bye

3番

コンテストから1週間経ち，今更感がありますが，Scratchで書きました．ご確認ください．

http://scratch.mit.edu/projects/15970373/

入力を1列でしか受け取れないのが残念ですが仕方ないですね．

4番

Excelで解きました．一部間違ってるかもしれません．

https://drive.google.com/file/d/0B0wUgziNPuKGNVJWVWRBdXhxSG8/edit?usp=sharing

追記：間違いの理由がわかりました．n=1000のときだけ落ちるような間違いでした．

夏季セミナー参加記＆反省会

来年やる人が同じ失敗をしないために色々書いておきます

途中で「です・ます」調でなくなっているのは息切れです。めんどくさいので直していません

参加記

端的にまとめます

  • 場所：今年は埼玉の準山奥でやりました。2009年に僕が生徒として参加したときと同じです。
  • チューター：今年はチューターが8人と多く、そのうち一人は初の女性チューターでした。
  • 08/26
    • 適切な電車が30分に一本程度しかないので、参加者の多くが同じ電車で来ていました。
    • 自己紹介がgdgdだったので何とかしたい
    • 無線LAN機器が不足していた
    • 部屋割りも全然決めていなかった。事前に決めたほうがスムーズかも
  • 08/27
    • 普通にセミナーをした
    • たまに理解が進まなそうなところとかについて軽く白板を使って説明したりした
  • 08/28
    • 普通にセミナーをした
    • たまに実装が微妙にバグっている人の手助け？をしていた
    • 交流と称していろいろなことをやった(後述)
  • 08/29
    • 普通に発表準備をした
    • 定期的に発表を聞いてチェックしてた
  • 08/30
    • 発表があった(togetter参照)
    • 案の定定刻に始められるわけがなかったので反省(後述)
    • そのあと帰った

反省1: 自己紹介のgdgd感

gdgdなのが全面的に悪いわけではないけど時間は勿体無いよね。

今年は

  • 名前
  • 所属
  • 学年
  • Twitterアカウント(任意)
  • その他(任意)

を言ってもらったけど、いずれにせよ何を話してもらうか最初に宣言しておいたほうが話しやすくなるから、来年はぜひ予め検討しておくべき。

その他

など、最初の話題作りになりそう(？)なことを言ってもらうのもありかもしれない。

ちなみにこの日の全体の流れは次のような感じ。

  1. 夏季セミナーについての概略(by チューターリーダー)
    • あらかじめ話す内容を考えておいたほうがいいかも
  2. チューター自己紹介(年齢順)
    • 紹介の順番とかもあらかじめ決めたほうがgdgdしなくて済むと思う
  3. 生徒自己紹介(名簿順)
  4. 本の紹介(担当チューターによる)
  5. 本選びフェーズ
    • これについては後述
    • ここまでで90分かかった
  6. 荷物を持って宿泊棟に行き、そのあと夕食
    • 食堂と宿泊棟が近く、研修棟が遠かったのでこの順番にした。
  7. 戻ってセミナー#1

反省2: 必要な機材

今年は無線LANルーターが初日に1台しかなかったのが大変だった。

結局次の日に事務局の人が持ってきてくれたのでよかったが、あらかじめ必要な機材のリストをチューターの側でまとめておいて、事務局の人に伝えておいたほうが、混乱が避けられるかも。

なお、具体的には次のような機材があるとよい。

  • 無線LANルーター: 部屋の数だけあると良い。
    • また、セミナー終了後に使うためにもう1台あっても良いかもしれない。(これはチューターの私物でもよい。セミナーで使ったものを流用してもよいが、機材の移動はできるだけ避けたい)
    • JOIではAirMac Extremeを使うので、AirMacの設定に詳しいマカーの人をあらかじめ見つけておくといいだろう。
  • 電源タップ
    • コンセントが壁からしか生えていない部屋のほうが多いので、距離が稼げるもののほうが良い
    • 今年の感触としては、一人1コンセントあれば足りそう
  • LANケーブル・有線LANのハブ
    • 無線LANルーターが存在しているのであればその数のLANケーブルだけあればとりあえず十分
    • 念のためあっても良いかも

反省3: 部屋割り

今年は8班で3部屋にわかれてセミナーを行った。この部屋割りはその場で決めたが、事前に決めることも可能であったように思う。

ちなみに部屋は、できるだけ入れ替わるように(いろいろな班と相席するように)部屋割りをつくった。

反省4: 本決め

JOIではJMOと違って用意されている本の数=生徒の数であり、本が余ることはない。


本の決め方は

  1. 白板上に残り枠数を書いておいて、まだ確定していない生徒は希望する本の欄に名前を書いておく
    • この時点では移動可
  2. 誰も移動しなくなったら、その時点で選抜を開始する
    • 枠数より少ないところは確定
    • 枠数より多いところはじゃんけんして、勝った人から確定
  3. 手順1に戻る

を繰り返すことによって行った。最小費用流を使うという意見もあったが、人間がやるのであればこれがわかりやすくて適切だと思う。

反省5: 交流

前の年に企画したものと同様に、今年も3日目に交流という名前のついた時間を2時間用意した。

今年は特に何も用意していなかったので、次のようなことをやった。

  • 与えられた条件を満たす漢字や英単語をできるだけ多く列挙するゲーム
  • Set(iPad用)
  • 空気を読むゲーム(iPad用)

来年もやるなら、ぜひ準備万端で挑んでほしい。(gdgdにやったせいでかなり時間を浪費した気がする)

反省6: 発表時間

今年は発表時間が昼休みを挟んで3時間+2時間だったので、前半に5チーム・後半に3チームと分けることにした。

これを決めたのは交流の時間の冒頭。発表順はそのタイミングで決めるのが正解だと思うが、時間の分け方とかはあらかじめ考えておいたほうが良かった気もする。

計算上は1人あたり10分ということになったのでこれを採用したが、次の日にこれではまずいということに気づいた。
結局、1人あたり10分の計算で時間を組むが、発表にかけていい時間は1人あたり7分程度ということにした。

この時間設定は結果としては正解だった。午前の発表が始まったのは予定の30分後だった。(というか、さすがに予定時間ちょうどに始めるのは不可能)

この日は僕は食堂が開いて一番に食事を取り、8時にレアン君のスライドをチェックした後、8時半に発表会の会場に着いて配線等の作業をしていたが、たぶん生徒が9時ちょうどに着席していたとしてもその時点で発表をするのは不可能であったように思う。

以下の準備が必要なので注意すること。

  • 無線LAN。去年や今年みたいに皆でTwitterで実況しながらやる流れでいくなら今後も必須。AirMac Extreme 1台では接続数的に足りなかったので2台稼働させた。
  • 場合によっては電源タップ。
    • 今年のように、床から供給できる部屋であるほうが望ましい。
  • プロジェクター類。
    • これに関しては発表者側の環境との関係もあるので厄介(後述)
  • 発表会についての説明をするスライド
    • 「発表したらSlideshare等にぜひアップロードして」とか「ハッシュタグは#JOIss だよ」とか、そういう色々を予め連絡してから発表会を始めるとよい
  • スライドなどのデータを集めるためのUSBメモリ
    • 複数あっても良いかもしれないけどめんどくさいからやっぱり1つでいいや
  • タイマー
    • iPad/iPhoneで プレゼンタイマー というのがあって、去年と今年はこれを使った
    • 予めインストールしておこう
    • 今年は6,7,8分経過時に鳴らした
  • togetterにまとめる人の用意(やるのであれば)
    • 便利なのでやってほしい

反省7: 生徒への連絡等

  • プロジェクターとの接続テストは予め実施しておきたい。
    • 今年は接続テストは不可能だったけど、せめて接続可能なインターフェースの確認(たいていVGAだけだけど)とその周知をしておくべきだった
  • スライドやデータ(主にソースコード)は参加者への配布のため回収するということの周知
    • スライドはオリジナル(pptxやkeyやodp)とpdfの両方が用意されているとなおよい
  • 参加記はもはや義務化してもいいのでは？
    • 「参加記を書くまでが夏季セミナーです」的な

まとめると、発表会前と発表会後に以下のことは伝えるといいと思う(今年の場合の例)

  • 発表の予定時間
  • 1人あたりの発表に許された時間
  • 質疑応答のタイミング(個人の発表ごと？班ごと？)
    • 今年は、個人の発表ごとに質問があるか聞いて、10秒経ったら次の発表に移った。
  • スライドやデータを集めるということ
    • 発表中か発表前に集めたほうがいいです(終わったら解散なので)
  • スライドのアップロードのお願い
    • Slideshare/Speakerdeck等へのスライドのアップロードを是非お願いしてください。
      • 色々オフィシャルに持っておきづらいスライドが多いので個人であげてもらうほうがよい
  • ハッシュタグ
    • #JOIss
  • 家に帰ったら参加記を書いてくださいとお願いしましょう
  • 解散前に集合写真を撮るのを忘れないようにしましょう
    • 今年は忘れかけた(odan君が指摘してくれたので助かった)

あと終わった後に、次のようなことをするのもチューターの仕事です

  • 集めたスライドやデータをまとめて参加者に配布すること
    • 配布しなければいけないので予め連絡をとれる状況にしておいたほうがいいです
    • 連絡がつきそうになければ事務局の人経由でも大丈夫かもしれないけれど
  • 参加記やスライドのアップロードを催促して、ブログにまとめること

反省8: チューター会議とリーダー

ここまで書いてて思ったのだが、チューター会議みたいなのをやったほうが話がスムーズに進むのではないか？

リアルじゃなくてSkype上とかでもいいけど。

あと今年は名目上のリーダーみたいなのが決まっていた程度で、鶴の一声みたいな人がいなかったからgdgdだったところがある気がするので、もうちょっとちゃんとリーダーを決めてやったほうがいいかもしれない。

反省9: 生徒の内輪ネタ

悪いということではないが、生徒の内輪ネタには毎回ヒヤヒヤさせられるので思ったことをここに書いておく。

  • 自己紹介フェーズで内輪ネタがいっぱい出てきたので、JOIとか初めての人がドン引きしないかすごくヒヤヒヤしてた。少なくとも今年は大丈夫だったみたいだが。
  • 発表で、同じ研修施設を使っていた中学校がネタにされているのもなんかヒヤヒヤしながら聞いていた。
  • あと、離席した人のPCがロックされていなかったらTwitterで勝手に発言するという習慣も、なんとなく皆了解している感じがあるけど、あれで本気で怒る人だっていてもおかしくないだろうなあとかちょっと思う。せめてこれ以上エスカレートしないような方向性で見守るのがいいのかなあ。

反省10: JMOとの比較

JMOのに参加したときを思い出しながら比較してみる(あんまり反省っぽくないけど)

まずいちばん大きいのが日数で、JOI夏季セミナーが4泊5日なのに対してJMO夏季セミナーは6泊7日ある。

これによってセミナー時間が増えているかどうかはさておき、僕の記憶では自由時間がかなり一杯あって、毎日人狼やら何やらで遊んでいた気がする。あとバーベキューしたりとか滝まで歩いて行ったりとか。

こういう時間がJOIにもあればなーと常々思っているが、一方で、そういう自由時間があっても半分くらいの人がTwitterしながらコード書いてるだけの会になりそうな気もして、なんか微妙…と思うこともある。

人数は、JOIが生徒25名前後でチューターは今年は多くて8名だったのに対して、JMOでは生徒が35人程度、チューターが15人程度。人数が多く、チューター比率も高いようだ。ちなみに女子の人数は同じくらい。

(チューターの気持ちだけで決められる問題ではないが)人数は多いほうがいい、と僕は思っている。ただ人数が増えたらその分運営をしっかりやっていかないとだめになりそう。

本は、JMOではJOIと違って本のほうが余分にあるので、生徒の選択によっては班が消滅したりする。(余った本がどうなるのかは知らない) これはこれでアリだけど別にそうする必然性も無いんじゃないかなと思う。

まとめ

次回僕が参加できるかどうかわからないけど、次回リーダー格の人には是非、こういった内容に注意しながら、よりよい夏季セミナーを作っていってほしい。

情報オリンピック夏季セミナーの参加記一覧とか

2013/08/26 - 08/30の間、夏季セミナーというのにチューターとして参加していました。以下はその記録として参照できる各種媒体へのリンクです。

参考：去年のリンク集

slideshare等にスライドをアップロードした人・ブログに参加記を書いた人がいたら教えて下さい、リンクします

ICFPC参加記

Programming

チーム名

qnighy

メンバー

  • qnighy

(計1名)

記録

08/06

ICFPCの登録期限が目前に迫っていたのでEasyChairに登録する。

08/07

EasyChairに登録するだけではだめで、ICFPCという名前のカンファレンスに論文を登録したことにしないといけないことを知り、論文のアブストという名のチーム概要を書いて投稿。

この時点で期限は過ぎていたが登録できた。

08/08

ICFPCの問題文を読む。楽しそうだと思う。

08/09

ICFPCやらないでプログラミング言語作ってた。
https://github.com/qnighy/proofline0

08/10

コミケ楽しそうだなー

08/12

お疲れ様でした(何もやってない)

おわり

今週のContest Management System (2)

CMS (Contest Management System) の最近の動向について書いてみようかなと思います企画2週目

DBモデルの修整とインポーターのダイエット

lerks(Luca) がDBモデルの細かい問題点をチェックし、修整しています。

例えば、アクセス元の許可リストとしてIPアドレスを指定する場面があり、今まではワイルドカードを0.0.0.0として表していましたが、現在はnullで表すようになりました。

現在もTODOがいくつかあるようです。(例： SubmissionのDBエントリのコード中にLANGUAGES_MAPという定数値が埋め込まれているが、これはモデルとは関係ないので別の場所に移動する。など)

さらに、コンテストデータをインポート/エクスポートするためのツール(YamlImporterやContestExporter) に対してもlerksは修整を行う予定です。

これらのツールは、内部でDBモデルを直接使用していますが、これをできるだけ自然に行えるように直して行きたいというようなことが書かれています。

スコアタイプのUI

管理画面では、課題タイプ(バッチ、通信、出力のみなど…) にあわせて設定画面が変化しますが、スコアタイプ(グループ最小や相対評価など…)のパラメーターは常に1行のみ(JSONオブジェクトを文字列化したもの)です。

これではユーザビリティーが低いので、ScoreType内でUIを指定できるようにしたいという提案がなされています。

ボスニアチームの採用

ボスニアでCMSの採用が検討している人がMLに質問を投げていました。

  • イタリア形式をそのまま採用しようとしているが、GENファイル(テストグループを指定するファイル)の仕様がわからず困っている。行の内容にかかわらず、行数 = テストケースの数ぶんが最初のテストケースから順番に使われるのか？
    • その通りである。
  • cmsResourceServiceを使っても、全てのサービスが5秒ごとに再起動してしまう。これは何故か？
    • cms.confの中にあるprocess_cmdlineの中身が、ps axを行った時の表示と対応しているかどうかをチェックしてほしい。なおこの件については、CMS側の仕様を変更する提案がなされている。 https://github.com/cms-dev/cms/issues/142

process_cmdlineの仕様変更

上の質問に関連して、process_cmdlineの仕様変更をするという提案がありました。 ( https://github.com/cms-dev/cms/issues/142 )

process_cmdlineはデフォルトが/usr/bin/pythonになっていますが、Ubuntuでの適切な設定は/usr/bin/python2であり、この変更を忘れると全てのサービスが5秒ごとに再起動するという不可解な現象に遭遇することになります。これは多くの人が引っかかる共通のトラップになりつつあります。

そこで、psを使ってプロセスの生存確認を行うよりも良い方法を探そうというのがこの提案です。

例えば

  • 呼び出された側のプロセスがpidをどこかに記録しておき、そのpidを用いて生存確認をする。
  • Pythonのmultiprocessingモジュールを使う。これは、スレッドよりも分離度が高い平行コンピューティング用のモジュールである。

といった方法が提案されています。

翻訳できない文字列

一部の翻訳するべき文字列が、トランスレーターを経由しているにも関わらず、ソースコード中のgettextに検出されない位置に書かれているために、potファイルに出力されないという問題が提起されました、例えば、一部のHTMLテンプレートがPython中の文字列定数として表現されているものを、独立したHTMLファイルにするなどによって解決できると考えられます。

また、コンテスト全体のロケールが設定されているにも関わらず、ログイン前の画面で正しく翻訳が表示されないバグも指摘されました。これも自明な方法で直せそうだと考えられます。

今週のContest Management System

CMS (Contest Management System) の最近の動向について書いてみようかなと思います

クロアチアと日本での採用

CMSが次の大会で採用されました。

  • クロアチアの3段階ある国内大会
  • 日本の国内大会のうち、代表選抜合宿

クロアチアでの採用を報告したメールによると、クロアチアで独自に以下の機能を追加したとのことです。

  • 解析モード
  • 複数のコンテストの同時開催
  • クロアチア語用のローカライゼーション

また、日本の大会でのCMSの導入はqnighyが主導して行いました。日本で利用するにあたって、次のような機能を追加しました。

  • 双方向のやりとりをする2つのプログラムを提出させる課題タイプ
  • より柔軟なグルーピングのできるテストグループ型のスコアタイプ
  • Imojudgeで使われる問題フォーマットをインポートするプログラム
  • 提出の詳細ページからソースコードを閲覧できる機能

クロアチアの独自機能も、日本の独自機能も、現在は本家にはマージされていませんが、そのうちパッチが作成されてマージされることでしょう。

サンドボックスに送られるシグナル番号

サンドボックス内のプログラムが何らかの間違った挙動によってシグナルを受け取った場合(例えば、プロセス自らがabort()で終了しようとした場合)に、それらが全て11番シグナル(SIGSEGV)に変換されるというバグが報告されました。

この原因は、cgroupsを利用したサンドボックス内で動作しているユーザープログラムが、プロセス番号1として扱われていることに由来しているそうです。プロセス番号1は通常のプロセスグループ上ではinitにあたる番号であり、1番プロセスはシグナルに対する既定の動作をもたないために、他のシグナルを受け取ったときに未定義の動作が実行され、それがSEGVを引き起こすのだとbblackhamは説明しています。

これに関連して、プロセスが落ちた理由をどれだけ詳細にコンテスタントにフィードバックすべきかという議題が生じました。もしシグナル番号をそのまま通知してしまえば、ユーザーはより多くのカスタムフィードバックを受けられる(各テストケースあたり32bit整数1つ分のデータが得られる)ことになり、入出力データをリバース・エンジニアリングできる機会が増えてしまいます。そこで、「MLE/TLE/RE」というような原因別の分類をすることをveluca93は提案していますが、これがどのような結論になるかはまだわかりません。