ProofSummit 2014 & JSSST Coq Tutorial


名古屋で開催された ProofSummit 2014 と、同じく名古屋大学で開催されている日本ソフトウェア科学会のチュートリアル:定理証明支援系Coq入門 に参加しました。

ProofSummit は各種の定理証明系(今年は Coq, Agda, Mizarの話がありました)とその応用について年に一回(大体8月末〜9月初に)開催しているイベントで、2010年に開催された Coq庵 から数えると今年で5回目です。「Coq を使ってみた」的な初心者の発表から、定理証明系を使って計算機科学の研究をしているような研究者による発表など幅広い内容の発表があります。今年の発表のかなりの部分に付いては、上記リンクから発表資料が参照出来ると思います。
ProofSummit 今年は定理証明イベントと一緒に開催する関数型言語イベントが中止になったり、東京で ScalaMatsuri が開催されていたりなどで、ちょっと参加人数が減りましたが、来年もまた開催したいし、来年こそはなんかネタを用意して参加したいです。

Coq チュートリアルは、産総研でCoqを使って研究されている Affeldt さんによる、Coq を使う意義/Coqについて/Coqの拡張であるssreflectのチュートリアル、でした。聞きに行った主眼はssreflectのチュートリアルだったのですが、前半の定理証明系やCoqについての話の部分も非常に面白かったです。発表資料は Affeldt さんのページから取得出来ます。
Coq チュートリアルは、100人以上が参加の、非常に盛況なチュートリアルでした。

その前の NII Shonan Coq セミナーと合わせて、この夏は Coq が熱い夏でした。今年のイベントとしてはあと、12/3-5に「高信頼な理論と実装のための定理証明および定理証明器」というのが九州で開催されます。

NII Shonan School on Coq 参加報告


NII Shonan School on Coq に参加して来ました。

Coq というのは定理証明支援系のソフトウェアです。関数型言語に興味のある方の中にはカリー=ハワード対応という言葉をご存知の方もいるのではないかと思いますが、これはプログラム⇔証明、型⇔命題という対応がある、というものです。Coq は依存型という、通常の静的型付け言語 (Haskell とか Scala など) より強力な型システムを用いることで、述語論理 (「全てのεに対して、あるδが存在して、どうのこうの」の様な量化子を含んだ式を表現出来る論理) の証明に対応するプログラムを書き、そしてその証明が正しいかを型検査することで機械的に確認出来ます。

じゃあ Coq を使うと何が良いのかというと、まず数学的な定理の証明を機械検証可能な形で証明出来ます。最近だとケプラー予想の機械的証明が話題になりましたね。他にも四色問題などが定理証明系の上で証明されています。どちらも数学者の人力では証明の検証が難しい問題です。
それとは別に、ソフトウェアが満たすべき仕様を述語論理で記述して、プログラムを実装し、実装が仕様を満たすことを証明出来ます。ユニットテストなどのテストでは網羅的でなかったりなどの問題がありますがCoqを使えばそのような問題はありません。
では、そんな素晴らしいツールがなぜ世の中で広く使われていないのかというと…単純に証明を書くのは難しいからです。Coqで証明を書くにはCoqの技術を磨く必要があります。
そしてその機会が、今回のセミナーという訳です。

セミナーは、葉山のセミナーハウスにて合宿形式5日間コース(半日の鎌倉見物含む)で開催され、内容はCoqの開発元のINRIAから訪れた講師によるCoqチュートリアルでした。
朝から夕食の時間までCoqに関する授業あるいは課題による実習、その後も解けなかった問題を寝るまで解く、というハードな毎日でした。私自身はここんとこあまりCoqで何かを証明してなかったので、多少錆び付いていたCoqのスキルを取り戻す良い機会でした。

残念ながら講義資料は参加者以外に公開されていない様です(パスワードで保護)。ただ、Coq については名古屋のProofCafeや、東京だとSF読み進捗ダメです会議 #9 #readcoqart #Coq(こちらは私も参加しています)といった勉強会が定期開催されているので、興味があれば参加されるとCoqについて学べると思います。

ScalaNLP/Breeze入門 2


ScalaNLP/Breezeの使い方の第2回です。

ScalaNLP/Breezeが何かとか、インストール方法などについては第1回をご覧下さい。

Breezeを用いた行列とベクトルの復習

簡単な例として、2行2列の例で説明しましょう。

オブジェクトの生成

breezeでは下記のような(密)ベクトル

\( \displaystyle x = \left( \begin{array}{c} 1 \\ 2 \end{array} \right) , \; y = \left( \begin{array}{c} 3 \\ 4 \end{array} \right) \)

と書く事が出来ます。

下記のような(密)行列

\( \displaystyle A = \left(\begin{array}{cc}
2 & 3 \\
1 & 2
\end{array}\right), \;
B = \left( \begin{array}{cc} 3 & 4 \\ 2 & 3 \end{array}\right)\)

を定義するには、行ベクトル(横ベクトル)を縦に並べて表現します。

加減算、積など

行列の加減算は通常の +, - といった演算子が使用出来ます。また行列の積も * で計算出来ます。

\( \displaystyle
x+y = \left( \begin{array}{c} 4 \\ 6 \end{array}\right), \;
A+B = \left( \begin{array}{cc} 5 & 7 \\ 3 & 5 \end{array}\right), \;
AB = \left( \begin{array}{cc} 12 & 17 \\ 7 & 10 \end{array}\right), \;
Ax = \left( \begin{array}{c} 8 \\ 5 \end{array}\right)
\)
は、

となります。

要素の取得、スライス

行列 \(A\) の要素を取り出したり、その部分(slice)を取り出す事も出来ます。行列 \(A\) をa で表すならば、\(A_{ij}\) は a(i,j) で表現されます。但し数学と違って添字が1-originではなく0-originであることに注意する必要があります。要素やスライスを取得する例は下記の様になります。(ここだけ判り易い様に3行3列の行列を使ってます)

各行や各列のsliceを作るには別の記法もあります。こちらの方が判り易いかもしれません。

mutable object

行列やベクトルは、メモリ使用量や効率を考えmutable objectとして作成されます。従って要素を変更可能です。またsliceは元のobjectを参照しているので下記の様にzの変更を通じてcが変更されます。また*=の様な自分自身を更新する演算子も多数用意されています。

逆行列

逆行列などを計算するにはDouble型の行列である必要があります。

\( \displaystyle A = \left(\begin{array}{cc}
2 & 3 \\
1 & 2
\end{array}\right), \;
B = \left(\begin{array}{cc}
3 & 4 \\
2 & 3
\end{array}\right),
\;x = \left(\begin{array}{c}
1 \\
2
\end{array}\right)
\)

を下記の様に定義します。

\(A\) の逆行列 \(A^{-1}\) はinv(a)で計算出来ますが、\(A^{-1}B, \; A^{-1}x\) と逆行列を用いて計算したいだけの場合は、a \ b, a \ x\ という演算子を用いて逆行列を計算しない事が推奨されています。

\( \displaystyle A^{-1} = \left(\begin{array}{cc}
2 & -3 \\
-1 & 2
\end{array}\right), \;
A^{-1}x = \left(\begin{array}{c}
-4 \\
3 \end{array}\right), \;
A^{-1}B = \left(\begin{array}{cc}
0 & -1 \\
1 & 2
\end{array}\right)
\)
は下記の様になります。

FLOPS2014報告


 FLOPS2014 に行ってきました、といっても発表しに行った訳でなく単に話を聞きに行っただけなんですが。

 FLOPS 2014 は二年に一回、日本で開催される関数型および論理型プログラミングに関する国際会議です。今年は6/4-6の日程で石川県金沢市で開催されました。
 弊社はアドテクの会社で開発言語もScalaだったりと、まぁほとんど会社の業務と関係無いのだけど、やはりせっかく日本で関数型言語の国際会議があるなら是非聞きに行かないとね、ということで聞きに行きました。

 以下、感想などです。各発表内容に関しては、プログラムのページから発表スライドを見る事ができるはず。

第1日目

★ “Liquid Types For Haskell” 招待講演
 今回のFLOPSで一番興味を持っていたのがこの話です。
 Liquid = Logically Qualified Data の略、のつもりらしく、liquid type というのは、{v: Int | v >= 0} の様に、論理式で修飾された型のことです。Coq などの依存型を用いた定理証明系でもこのような述語を伴った型を使ってプログラミングを出来るところは同じなのですが、liquid type は述語を決定可能なPresburger算術の範囲に限定し、SMTソルバーを用いて自動証明をさせようというところが大きく違います。まぁCoqの証明を書くのは大変だし、開発の現場で必要とされる検証課題はほぼPresburger算術で充分なのだとしたら、自動証明の方が普及までの敷居が低いのは自明。
 LiquidHaskell がどんなものか試したい人はオンラインでどんなものか試すことが出来ます。
liquid type の型定義は、{-@ type Even = {v:Int | v mod 2 = 0} @-} みたいにHaskell のコメントとして、実際のHaskellのコードに註釈します。すると double xs = [x + x | x <- xs] のようなHaskellの実装について、{-@ double :: [Nat] -> [Even] @-} の様な仕様を満たすことを自動証明してくれる、というのを試せます。
 個人的には Coq で証明を書くの好きなんだけど、やはり前の会社(SIer)や今の会社で仕事をしてみた印象としては、自動証明器も必要なのかなぁとも思います。ならば Why3 とか使って開発すれば良いかなとも思うけど、Haskell みたいに既にメジャーな言語でこの手のツールが使えるというのは、やはり強みなのかなぁと思います。

他の発表は簡単に(というか専門家じゃないから解説なんか出来ない)。詳しくは、proceedings読んで下さい。

★ “PrologCheck – property-based testing in Prolog”
 オブジェクト指向言語界隈では具体的なテストケースに対してユニットテストをすることが多い様ですが、関数型言語ではランダムにテストデータを生成して仕様(=満たすべき性質)を満たすことを確認するようなproperty-baseのテストツールが標準的です。(ScalaでもScalaCheckというのが有りますが、開発現場ではあまり使われてないみたい。勿体ない話です。)
 で、Prolog版のを作った、という話(だと思う)。

★ “Generating Constrained Random Data with Uniform Distribution”
 で、その手の XXX Check系のテストツールには、「もし入力データが◯◯という性質を満たすなら△△」みたいなのをテスト出来るのですが、◯◯という条件を満たすランダム入力データを作るのはなかなか面倒だったりします。その辺を工夫したよ、という話(だと思う)。

★ “Guided Type Debugging”
 関数型言語のエラーメッセージは、(C++ほどではないと思ってはいますが)Javaとかに比べると判りにくいところがあります。その原因の一つの、型の不整合の時のエラーのデバッグを容易にしようとする工夫(だと思う)。

★ “Using big-step and small-step semantics in Maude to perform declarative debugging”
 Maude (という項書き換え系言語)の上に、何か言語の big-step あるいは small-step semantics を定義して実行とかデバッグとか出来るフレームワークを作った、という研究の様に思えた。確かに small-step semantics とか Maude の上に定義すると便利そうに思えますね。

★ “Faustine: a Vector Faust Interpreter Test Bed for Multimedia Signal Processing – System Description -”
 Faust というのは信号処理用のDSLらしいのですが、これを使ったギターアプリ(タブレット上で動くギター風に演奏出来るアプリ)の動画デモが。こんな研究してる人もいるんだなー、と思いました。

★ “The Design and Implementation of BER MetaOCaml: System Description”
★ “On Cross-Stage Persistence in Multi-Stage Programming”
 MetaOCaml というのは OCaml を拡張して型安全 eval を使える様にしたようなものなのですが、それに関する発表が2件。

第2日目

★ “Programming Language Methodologies for Systems Verification” 招待講演
 L4 microkernel を作ってる研究機関での形式手法仕様に関する報告。当初OS班と形式手法班がIsabelle/HOLを使おうとして失敗し、Haskellを両者の共通言語として選択したら成功して、両者の共通言語としてのHaskellからIsabellあるいはC++を作る様になった(しかしその後、各班がHaskellをメンテしなくなって云々)みたいな報告。
 この手の話聞くと、OS班とはいえ研究者の方々でも、やはり Isabelle などの形式手法(定理証明系)とかで仕様記述するの嫌なのか、と思ってしまいますね。。。IsabelleはZとかほど抽象的ではないと思うのだけれどなぁ。あと、線形型は勉強した方が良さそうだなと思った。

★ “Lightweight higher-kinded polymorphism”
 OCamlには無いhigher-kinded polymorphismをdefunctionalizationすることで実現したよ、という話。

★ “Generic Programming with Multiple Parameters”
 HaskellのGeneric programmingでパラメータを複数個使える様に、という話。うーむ、Haskellのgeneric programmingの話、ちゃんと復習しないとなー。

★ “Type-Based Amortized Resource Analysis with Integers and Arrays”
 計算量というリソースを型として表現するという話。こういうことも出来るのか、と。

★ “Linear Sized Types in the Calculus of Constructions”
 CoqのInductionの停止性、CoInductionのproductivityの判定の為に、それらを表現出来るような型を、という話。

★ “Dynamic Programming via Thinning and Incrementalization”
 ナップザック問題を例にとってDPの解法アルゴリズムを、融合変換とかアルゴリズム変換とかを使ってアルゴリズムを最適化する話。この手の話に興味がある人は、”semiring fusion” とか “第三準同型定理” とかのキーワードでググると良いと知人より教わりました。勉強すること多いなー。

★ “POSIX Regular Expression Parsing with Derivatives”
 微分を用いて正規表現を扱う話は知っていたのですが、POSIX準拠のはずの各種正規表現ライブラリが、どこで部分文字列をマッチすべきかについて正しく無い答えを返す、という話は知りませんでした。ちゃんとPOSIX仕様に基づいて、部分マッチ箇所を計算するアルゴリズムの話です。Proceedingsにはプレゼンでは端折ってあった箇所が書かれてて面白そうなので、あとでちゃんと復習しよう。

★ “Semantics for Prolog with Cut – Revisited”
 Cut有りのPrologのsemanticsをCoqでやってる、という話。すみません、Prolog良く解らないので、どの辺が重要なポイントなのか判りませんでした。

★ バンケット
 コース+追加で寿司、天ぷら、日本酒という立派なバンケットでした。線形論理の話とか面白い話を聞けました。

第3日目

★ “Relating Computational Effects by TT-Lifting” 招待講演
 計算(computation)を扱う理論的枠組みとしてdenotational semanticsというのがあるのですが、圏論を使って色々統一的に議論出来るよという話で、最初は判る話だったんですが、後半はさすがに振り落とされました。が、こういう話聞くと、また圏論勉強しよう、という気分になりますね。

★ “A New Formalization of Subtyping to Match Subclasses to Subtypes”
 継承とジェネリクスと両方ある Java とか Scala みたいな言語だと、型宣言の際に共変反変の両方の制約を満たす為に(例えばScalaなら) sealed abstract class List[+A] extends ... { def ::[B >: A] (x: B): List[B] = ... } みたいなイディオムを使わざるを得ないとか色々不便なところもあるのですが、この論文は新しい subtyping の定式化をしてみたよという話。OO言語関係に近い話題はこの一件だけでした。Scala などに興味がある人は ECOOP とか聞きに行くべきなんですかね。。。

★ “Type Soundness and Race Freedom for Mezzo”
Mezzo というのはML風の言語なんですが、線形型を用いることでマルチスレッドプログラミングでロック取得の必要性などをコンパイル時にチェック出来る様にした言語で、言語の正しさ(型検査が通ればデータ競合が起きない事)を Coq で証明した、という話。Java とか Scala とかだとプログラマが正しくロックを取ってる事を保証しなくてはいけないので、Mezzo のこういう機能は素晴らしいと思います。

★ “Proving Correctness of Compilers using Structured Graphs”
 木構造ではなく(非循環)グラフを用いてコンパイラを改善するみたいな話で、グラフを用いてコンパイル&実行するのと、木も用いてとが等価だと言う証明の話(だと思う)。

★ “Constraint Logic Programming for Hedges: a Semantic Reconstruction”
 すみません、これは良く判りませんでした。semantics と solver のアルゴリズムについて話してたと思うのだが。

★ “How many numbers contains a lambda-term?”
 λ式でk-tupleとかを作った場合、λ式の型を決めると、そこに含む事の出来る自然数の個数には上限がある、という話(だと思う)。これも難しくて判りませんでした。

★ “AC-KBO Revisited”
 項書き換え系にはクヌース・ベンディックス完備化アルゴリズムという完備化アルゴリズムがありますが、結合則 x+(y+z) = (x+y)+z や交換則 x+y=y+x のような規則を満たす演算子に関する場合にどうするかという話。Steinbach という人の論文が間違っているという論文があったけど実はそれは正しくてみたいな話とか、順序付けがNP-hardなことはこうやってSATに変換してとか、(詳細は理解出来ない)門外漢にも楽しめる発表でした。

★ “Well-structured pushdown system: Case of Dense Timed Pushdown Automata”
 Timed Pushdown Automata の話でした。これも基礎知識が無くどういう話なのか良く判りませんでした。

終わりに

 社外勉強会の効能として、「今まで知らなかった話題に触れられる」「すごい人たちのやってるすごいことを知る」「もっと勉強しようというやる気を貰ってくる」といったことを主張する人は多いです。私もその意見に賛成します。
 だとしたら、学会とか国際会議に行けば、第一線の研究者がやっている最先端の話題を知る事が出来ます。
 そして、例えばHaskellとかOCamlなどは、言語の開発者がこういう学会で発表した事を言語の新機能として追加したりします。学会で話されている事は自分が使う機能と無関係な難しい話ばかり、という訳ではありません。
 
 勿論、聞いても分からない話も一杯有りますし、周りは見知らぬ研究者ばかりで話す相手も内容も無い、などなどというところはありますが、まぁその辺は我慢するとして。判らなかった内容とかは、各種勉強会とかに行って論文コピー片手に詳しそうな人に質問するとか方法はありますし。

 2016年のFLOPSは高知で春に開催だそうです。また PPL のような日本の学会とかなら敷居が低く感じるかと思います。

 社外勉強会に行く次のステップとして、学会とか国際会議を聞きに行くのを是非お勧めします。

ScalaNLP/Breeze入門 1


はじめに

機械学習用途のOSSというと RWeka などのツールが有名かと思います。それらの分析用ツールはデータの分析を主目的としており、弊社のようにアプリケーションへの組み込み用途が主になる場合や、論文などを読んでツールに無いアルゴリズムを実装してみようと思った場合などは、多少使いにくい部分も有ります。(なお Weka は Java から呼び出し可能なライブラリとして提供されていますが。)

プログラミング言語から呼び出し易い数値計算のライブラリというと Python の SciPy, NumPy といった有名なライブラリ群があります。が、Scala を主たる開発言語としている弊社としては、出来れば JVM 上で動くライブラリを使いたいところです。

そういった目的の為のライブラリとしては Scala にも ScalaNLP/Breeze というライブラリがあります。ScalaNLP/Breeze は下位ライブラリとして netlib-java という数値計算ライブラリ経由で BLAS/LAPACK などの定評ある高速なネイティブ数値計算ライブラリを呼び出します。 (MacOSXの場合はMacにインストールされているApple版のBLAS/LAPACKが使用されます。Linux, Windows の場合は netlib-java の記述を参考として ATLAS などの導入が別途必要です)。

そこで ScalaNLP/Breeze の使い方の紹介を数回に渡って行おうと思います。

セットアップ

github上の README.md を参考にセットアップします。

ここでは scala 2.10 と sbt 0.12 が予め導入されている事を前提とします。

プロジェクトのディレクトリとして scalanlp-usage/ を作成し、その下にbuild.sbt ファイルを作成します。(ライブラリ取得先については多少無関係なものも含まれていますが、良く使うところなので。)

build.sbt 内容

上記のようなファイルを作成し、プロジェクトディレクトリ下で

$ sbt update

を実行し、[success] が表示されれば、ライブラリの導入完了です。

動作確認

動作確認をしてみましょう。下記は MacOSX 上で動作確認した場合です。

上記の様に、行列の掛け算は JNI 経由でネイティブなライブラリが呼び出されている事が判ります。

簡単な性能確認

どのくらいの規模の計算がどの程度の時間で計算出来るか、簡単に確かめてみましょう。その為に、ランダムな正方行列で定まる一次方程式を解く時間と、どの程度の大きさまで解けるのか、試してみます。

Main0.scala

引数で行列の大きさを適当に変えつつ試してみると、

と、計算時間はほぼ大きさの3乗に比例し、大きさ 1000×1000 の行列であれば 30msec 程度で解く事ができ、8000×8000 の行列であれば10秒以内には解けていることが判ります。これを試した条件は sbt起動オプションが -Xms1536m -Xmx1536m なので、ヒープサイズを多めにすればもう少し大きな問題も解けるでしょう。

次回からもう少し具体的に、ライブラリの使い方を解説します。