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は提案していますが、これがどのような結論になるかはまだわかりません。

CoqのtacticをOCamlで書く話

CoqのtacticをOCamlで書いてみたので、同じようなことをしたい人のためにメモ。

なお私はOCamlについてはそれほど詳しくないので、そこの正確性については注意が必要。

同じ事をしているtacticがないか探す

同じようなことを考えている人は必ずいるはず。といっても、網羅的な探し方があるわけではないので、ある程度調べて見つからなかったら自分で書いたほうが効率が良いかもしれない。

CoqのLtacで実現できないか考える

CoqのLtacは型無しラムダ計算であり、よく理解すればかなりの処理をLtacだけで実現できる。もしOCamlで実装するにしても、Coqに既に存在しているtacticやtacticalなどを把握していれば実装は容易になる。

Ltacの機能については、Coqのリファレンスマニュアルの012番 Chapter 9 The tactic language にまとまっている。なお、Ltacに関連するコマンドとしては、"Ltac"と"Tactic Notation"が扱えればよい。これらのコマンドについては、コマンド一覧 Vernacular Commands Index を参照。

まあ、「CoqのLtacでできるはずだが、なぜかできない」(例：Anomalyが発生する)というのはよくある話なので、その機会にCoqの内部構造も理解してしまおうという軽い気持ちでOCamlに手を出すのも悪くはないかもしれない…

ビルド環境を整備する

Windows(Cygwin+MinGWなど)でも頑張ればビルドできないことはないが、大変なのでLinuxなどの使用を強く推奨する。(Windowsでビルドするノウハウについてはそのうち書きたいが…)

OCamlの処理系やCoqのヘッダなどを必要に応じて入れていけばいいだろう。一番簡単なのは、OS標準のOCamlとliblablgtkをインストールした上で、Coq自体は自分でビルドするという方法なのではないかと思う。

開発環境が整ったら、Makeファイルを書く。Makeの例は以下のとおり。

-R . MyPackage
-R ../DependentPackage DependentPackage
my_ocaml_code.ml
my_ocaml_code.mli
ocaml_extension_interface.ml4
CoqCode/InternalA.v
CoqCode/InternalB.v
Foobar.v

MyPackageはパッケージの名前である。この例の場合は、MyPackage.CoqCode.InternalAなどのモジュールが生成される。

普通のOCamlコードはmlとmliに書き、tacticを宣言するところをml4に書くのが一般的なようである。(全てを単一のml4ファイルに集約しても問題はない。)

Makefileを以下のようにして生成する。基本的には、Makeファイルはcoq_makefileへのコマンドライン引数をひとまとめにしたものに過ぎない。

$ coq_makefile -f Make -o Makefile

あとは普通にmakeと打てばビルドされるようになる。

ハローワールドを書く

greeting.ml4ファイルに次のように書く。(以下greetingは任意の名前で置き換えてよい)

TACTIC EXTEND hello
| [ "hello" ] -> Tacticals.tclIDTAC_MESSAGE (Pp.str "Hello, world!\n")
END

vファイルに次のように書く。

Declare ML Module "greeting".

Goal True.
  hello.
  auto.
Qed.

ゴールの帰結を出力する

ゴールの帰結を出力するようにしてみる。

let hello gl =
  Tacticals.tclIDTAC_MESSAGE (Termops.print_constr (Tacmach.pf_concl gl)) gl

TACTIC EXTEND hello
| [ "hello" ] -> hello
END

タクティックの基本構造

タクティックはProof_type.tactic型であるが、これはgoal sigma -> goal list sigmaである。

これは、「ゴールと環境を受け取って、ゴールのリストと環境を返す関数」という意味である。

Goal.goalの実体はただの整数である。'a Evd.sigmaは、'aに環境を付加した('a, evar_map)といった感じの型で、'aはEvd.sig_it、環境はEvd.sig_sigで取り出せる。

といっても、goal list sigmaを自分で組み立てることはまずない。Tacticalsモジュール(tactics/tacticals.mli)に、基本的なtacticalが存在しているので、これを使えば大抵の操作は組み立てられる。また、applyなどの基本的なtacticはTacticsモジュール(tactics/tactics.mli)に存在している。

なお、Proofview.tacticは全く異なる型のようであるので注意すること。これはより抽象的なモナドのようだ。

Coqのデータの操作

Coqにおける値はOCaml上ではTerm.constrという型をもつ。「Coqにおける型」を意味するTerm.typesはconstrの別名にすぎない。

constrの基本的な操作はTermモジュール(kernel/term.mli)にある。mkAppなどのmk系、isAppなどのis系、destAppなどのdest系があれば基本的に事足りる。

constr同士の比較は目的に応じて複数の関数があるが、一番身近なのはeq_constrである。自分で比較を作りたいときは、compare_constr関数が便利である。compare_constrを利用して比較を組み立てる方法は、実際にそれを使っているコードをCoq本体から探すのが早い。(eq_constr自身もcompare_constrを使っている。)

帰結の取り出し

ゴールから帰結の型を取り出す関数はTacmach.pf_conclである。ゴールから情報を取り出したいときはまずTacmachモジュールを探せばよいだろう。

ただし、こうして取り出したconstrには、「すでに確定しているevar(existential variable)」が含まれている場合がある。つまり、既に具体的な値が確定しているのに、「?1」のようなexistential variableの形で含まれている部分式が存在しうる。(具体的には、同じ命令の間(ピリオドで区切られたときに同じ区間に属する間)に、以前のtacticで値が確定したevarがこのままの形で残っている。) これを具体的な値で置換する場合は、Evarutil.nf_evarを使えばよい。

Coq内で定義された値を取り出す

いろいろな方法があるようだが、次のようにするのが簡単だろう。

let coq_Permutation =
  lazy (Coqlib.coq_constant
        "Coq.Sorting.Permutation.Permutation not found"
        ["Sorting"; "Permutation"] "Permutation")

まとめ

とりあえず自分の使った範囲では以上のようなテクニックがあった気がする。

高度な証明生成がしたくなったら、OCamlコードを書いて快適なCoqライフを送ろう。

Advent Calendar Advent Calendar (2012) 12日目

飛び入りで書きます。Advent Calendar Advent Calendar

僕が今日紹介するのはLispギャグアドベントカレンダーです。

Lispに関するギャグが、かわいい絵とともに書かれています。

ですが、このギャグ、ものによっては非常にわかりづらいです。したがって、頭の体操を行いたいという人はこのアドベントカレンダーを見るといいかもしれません。

まとめると、このアドベントカレンダーを読むと得られそうなものは

  • Lispに対する関心・Lispに関する断片的な知識
  • かわいい絵による癒し
  • アハ体験とかいうやつ

ただ、パターンが掴めてしまうとそれほど面白くはないかもしれない。でも癒されます。


これだけではつまらないので、僕なりの解答を載せておきます。どうしてもわからなかったら参考にするといいと思います。


↓

↓

↓

↓

↓

↓

↓

↓

↓

↓

↓

↓

↓

↓

↓

↓

↓

↓

2011 解答例

1日目： 格好いい = 括弧いい (括弧はLispの代名詞)
2日目： 継続は一般的な意味のほかに、主に関数型言語に見られる特徴的な実行フロー制御機構として知られている。
3日目： 「使えばルンルン」を発音するとevalが含まれている。
4日目： Lispでは、連想リストはassociation listを略してa-listと呼ばれることがある。
5日目： いーんよ = 引用 (クオートは引用符・引用のことなので)
6日目： 「こんくらい」にconc(concatenation)が含まれている。
7日目： 糖衣構文 = 遠い構文
8日目： 煮る = nil; しかし#tとnilはむしろ対照的では…
9日目：「値たち」の「たち」を「多値」と読み替える(valuesは多値関数)
10日目： ジェネリック関数 = 総称関数, 総称 = そうしよう
11日目： nthを「んす」と読み、文末の「やんす」に引っ掛ける。
12日目： 「歴史(を)軽々しく語る」に「レキシカル」が含まれている。
13日目： 「記憶させる」の末尾が「セル」。
14日目： 「ごめんなさい。嫌いなの。」を発音すると「再帰」が含まれている。
15日目： 「どーでしょう」にdoが含まれている。
16日目： 「やめたほうがいい」にMetaが含まれている。
17日目： 「速い組み込み」に eq = イク が含まれている。
18日目： 「あるから無駄」に lambda が含まれている。
19日目： 読み上げるとletが含まれている。
20日目： 「ヘイ、放課後」に閉包(クロージャ)が含まれている。
21日目： 「まっ、苦労」にマクロが含まれている。
22日目： 「書こっか」の末尾が「コッカ」で、これはしばしば「カッコ」の逆順であることから閉じカッコの意味で使われる。
23日目： 「って今日教えた」に「適用」が含まれている。
24日目： 後悔 = 高階(高階関数)
25日目： クリスマスとリスプを引っ掛けている。

2012 解答例

1日目： 「あるのでファン」にdefunが含まれている。
2日目： 「見るのか―」の末尾がCAR。
3日目： 「ついに」を「対に」ともとれる。
4日目： 「くださいって聞かれた」に「最適化」が含まれている。
5日目： 「繰り返すし綺麗」に「S式」が含まれている。
6日目： 「得るといいよ」に「elt」が含まれている。
7日目： 「混同するな」にcondが含まれている。
8日目： たっぷり = タープリ = terpri
9日目： 「窮困する」にconsが含まれている。
10日目： 「素敵よ」に適用=applyが含まれている。
11日目： 「している」にtailが含まれている (末尾再帰 = tail-recursion)
12日目： 「こうかい？」 = 高階
13日目： 「使いまくろう」にマクロが含まれている。

Re:永続データ構造が分からない人のためのスライド

この記事はCompetitive Programming Advent Calendar 2012の12/01担当分の記事です。

永続データ構造が分からない人のために、「Re:永続データ構造が分からない人のためのスライド」というスライドを頑張って作りました。

内容の概要：　永続データ構造を用いる3つの問題について検討しつつ、永続データ構造について考察します。

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

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

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