ProofSummit 2014 & JSSST Coq Tutorial

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

ProofSummit は各種の定理証明系(今年は Coq, Agda, Mizarの話がありました)とその応用について年に一回（大体８月末〜９月初に）開催しているイベントで、2010年に開催された Coq庵 から数えると今年で５回目です。「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 参加報告

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

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

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

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

FLOPS2014報告

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

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

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

第１日目

★ "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 <- code="" 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 を使える様にしたようなものなのですが、それに関する発表が２件。

第２日目

★ "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良く解らないので、どの辺が重要なポイントなのか判りませんでした。

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

第３日目

★ "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 のような日本の学会とかなら敷居が低く感じるかと思います。

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

[Coq] Coq Tutorial on 1/12, 2/2, 2/9, and 2/16

イベントレポート：「Coqチュートリアル#1」 @ InfoQ

今回、豆蔵様より会場を提供していただけることになって、前々から計画していた平日夜の複数回開催のCoqチュートリアルを 1/12, 2/2, 2/9, 2/16 という予定で開催します。
参加申し込みについては上記リンクから辿って頂ければと思います。

[Coq][Formal Methods] Proof Assistant Day 2011 on 9/25(Sun)

　今年の９月は東京で ICFP 2011 が開催されることもあり、その前後の週末も公式/非公式な関数型言語イベントが多数開催される見込みです。

　我々の形式手法勉強会 Formal Methods Forum も、名古屋の ProofCafe と一緒に、昨年開催された Coq庵 と同様の定理証明系イベントを開催したいと計画しています。

　会場は新宿の豆蔵セミナールームを予定しています。（豆蔵様、会場提供ありがとうございます）

　諸々決まりましたら、また報告します。

[Event] Recent Days

今週は、Step by Step Scala [vol.04]@scala-beで話をしたり、Haskellナイトを見に行ったり、Scala Hack-a-thon #1に参加したり、でした。

Step-by-Step Scalaは、（少なくとも何人かの方には）Swarmについて興味を持ってもらえた様なので満足。この先の仕事の状況がまだ確定しないのだけど、また機会があればScalaの講師を出来ればなぁ、とか。

Haskellナイトは、本の話がちょっと多過ぎたかなぁとは思うのだけど、出版合わせのイベントだから仕方がないのかなぁ。もうちょっとHaskellの話を聞きたかったかも。

Scala Hackathonは存在を知った時には既に満員になっていて参加を諦めてたんですが、当日朝見たらキャンセルが大量に出たみたいで慌てて家を出た次第。yuroyoroさんの作成したテキストが良く出来ていて、みんな黙々とそれを読んでいたのかな？かつ、質問はtwitterで主として行われていたみたい。懇親会も楽しく参加させて頂きました。

[Event] Type-Level Programming Meeting

型レベルプログラミングの会

定員がすぐいっぱいになってしまって会場参加は出来ず、自宅からustreamで拝聴。
発表された皆さん、どれも興味深い話でした。ありがとうございます。

• Scala : Scalaの型プログラミングの話は前にも聞かせて頂いたような気がするけど、更に話題が広がっていたような。


• C++ : 定番ではありながら、私はC++は経験が少ないので興味深く聞けました。


• Haskell : フォロー出来ない話も多かったですが勉強になりました。勉強すべき事、多いなぁ。


• D : 型プログラミングの為のような言語ですね。興味深い。


• 依存型プログラミング : プレゼン資料が大変面白いというか芸達者というか。April Foolの予告のGirardの逆理の話では無かった。


• G'Caml : 存在を始めて知りました。OCaml関係も色々あるなぁ。

この手の勉強会に参加すると、今まで知らなかったことがいっぱいあると判り、もっと勉強しなくちゃ、と思う。
日々の仕事は非技術的な作業ばかりが増えているので、知的好奇心の刺激の為にもこの手の勉強会に積極的に参加しないと。