TL;DR
- Lean で正規表現をオートマトンにコンパイルして実行するライブラリを作り、実装が仕様どおりであることを証明した。
- 定理証明の一番の価値は、プログラムがなぜ正しく動くのかを深く理解できることである。プログラムを深く理解するとは、良い不変条件を見つけることである。
内容
Lean とは
Lean は、純粋関数型プログラミング言語と定理証明支援系の 2 つの顔を持つ。言語としては、依存型、モナドを使った手続き的な記述、マクロを備える。定理証明支援系としては、数学の定理やプログラムの性質と、その証明を記述できる。
自作の正規表現ライブラリ
lean-regex は、正規表現をオートマトンにコンパイルして実行するライブラリで、実装が正しいことを Lean 上で検証している。ここでの「正しい」とは、マッチの仕様を厳密に定義し、実装がそれに合致することである。具体的には、検索関数について健全性と完全性を示す。健全性は見つかったマッチが仕様を必ず満たすことである。完全性は仕様を満たすマッチがあれば必ずそれを見つけることである。
Lean の最適化
Lean には 2 つの実行モデルがある。1 つはカーネルによるインタプリタで、証明の検証やエディタでの実行に使う。もう 1 つは C へのコンパイルで、ネイティブコードを生成する。後者では、オブジェクトを参照カウントで管理する。Lean は正格な純粋関数型言語なので、参照の循環は基本的に起きない。また、参照カウントを見れば、データ構造の更新を破壊的な更新に最適化できる。
なぜ定理証明か
定理証明には、信頼性の保証、証明の過程でバグが見つかることによる品質の向上、パズル的な面白さといった利点がある。中でも一番重要なのは、深い理解が得られることである。証明を書くには定理がなぜ成り立つかを理解しなければならないので、書いたプログラムがなぜ正しく動くのかを深く理解する必要がある。
発表では、プログラムが正しく動く理由を「良い不変条件が成り立っていること」に求める。不変条件を使って性質を示す手順は次のとおりである。
- 不変条件を見つける
- 各処理が、見つけた不変条件を保存することを示す
- 見つけた不変条件が、求める性質を導くことを示す
不変条件は、具体例や欲しい性質から逆算して見つける。