初めての検証済み命令的プログラム

元記事 My first verified (imperative) program

コード例 https://github.com/leanprover/lean4/blob/master/tests/lean/run/pairsSumToZero.lean

次期 Lean 4.22 リリースで追加される多くの新機能のひとつに、命令的プログラムの性質を証明するための新しい検証基盤のプレビューがあります。 この記事では、この機能を紹介し、簡単な例を通じてその可能性を示し、さらに類似のツールと比較してみます。

導入的な例

この記事では一貫して、次のような簡単なプログラミング課題を例として用います。 「整数のリストが与えられたとき、リスト内の異なる位置にある 2 つの整数の和が 0 になるかどうかを判定する」というものです。

たとえば、リスト [1, 0, 2, -1] が与えられた場合、 $1 + (-1) = 0$ となるので結果は真となります。 また、リスト [0, 0] が与えられた場合も結果は真となります。 一方、リスト [1, 0, -2] が与えられた場合は、そのような組が存在しないので結果は偽となります。

この問題を最も単純に解く方法は、2 重ループを使ってすべての異なる位置の組を走査することです。 しかしこれは二乗時間を要し、効率がよくありません。 これを改善する方法はいくつかありますが、ここでは次の手法を使います。 リストを順に走査し、これまでに見た要素を集合（データ構造）として保持しておきます。 そうすれば、ある数 $x$ に出会ったとき、$-x$ をすでに見ているかどうかを効率的に確認することができます。 もし見つかれば答えは真です。 リストの終わりまで到達した場合は答えは偽となります。ハッシュ集合を用いると期待時間は $O(n)$、二分探索木を用いると最悪時間は $O(n \log n)$ となります。 Lean では両方が利用可能で、それぞれ Std.HashSet および Std.TreeSet という名前で提供されています。

局所的に命令的プログラムとして書く

Lean は関数型プログラミング言語ですが、命令的（状態を持つ）プログラミングに対しても良好なサポートを備えています。 これは、単一関数内でのローカルな利用（do 記法による）と、関数をまたいだ利用（モナド変換子による）の両方が可能です。この記事では、ローカルな命令的手法のみを用います。

このローカルな命令的手法を使えば、先ほど説明した集合ベースのアルゴリズムを簡単に記述することができます。

import Lean
import Std.Tactic.Do
import Std.Data.HashSet.Lemmas

open Std

/-- 与えられた整数のリストに、足して0になるような異なる２つの要素があるか？を判定する -/
def pairsSumToZero (l : List Int) : Bool := Id.run do
  let mut seen : HashSet Int := ∅

  for x in l do
    if -x ∈ seen then
      return true
    seen := seen.insert x

  return false

コードの最初の行にある Id と do は、Lean に対して「ローカルに命令的」なモードで作業したいことを伝えています。 これにより、可変状態・for ループ・早期リターンといった、命令的プログラミングでおなじみの機能を備えた Python 風の構文を利用できるようになります。

ローカルな命令的手法によるプログラミングの性質を証明する

ローカルな命令的手法はプログラムを書くうえで非常に便利であり、実際 Lean 自体の多くの部分もこのスタイルを使って Lean で実装されています。 しかし Lean は単なるプログラミング言語ではなく、対話型定理証明支援系でもあります。 Lean の核心的な機能のひとつは、自分の書いたプログラムが正しいことを証明できる、という点にあります。

従来、ローカルな命令的プログラムについて性質を証明するのは、ごく単純な場合を除いて困難でした。 そのため、もし証明に関心がある場合には、通常は Haskell のような関数型言語で行うのと同様に、プログラムを関数型スタイルで書くのが最も容易でした。

Lean 4.22 では、Lean 標準ライブラリ内の配置場所にちなんで Std.Do と呼ばれる新しいフレームワークがプレビューされます。 これは、局所的にも大域的にも、命令的プログラミングを検証付きで容易に行えるようにすることを目的としています。

まだ不足している主なものはドキュメントです（そして本記事がそれを実質的に補うわけではありません）。 しかし、少し調べてみれば、すでに初歩的な実験を行うことは可能です。

Std.Do の基盤となっているのは、古典的な ホーア三つ組 (Hoare triples) の考え方です。 つまり、命令的プログラムに関する主張は常に「もし前提 $P$ が成り立ち、コマンド $C$ を実行したならば、事後条件 $Q$ が成り立つ」という形式になります。 たとえば、ある変数が少なくとも 1 以上であるとき、それをデクリメントすれば、その変数は少なくとも 0 以上である、というような形です。

ホーア三つ組の良い点は、それが 合成可能 であることです。 大きなプログラムは、多くの小さな関数から構成されており、それらは大域的な状態に作用したり、他の副作用を持ったりすることがあります。 ホーア三つ組を用いれば、小さなプログラムについて証明した性質をそのまま利用して、より大きなプログラムの性質を証明することができます。 今回の例は単一の関数から成り立っているため、この合成性は直接的には重要ではありません。 しかし、この仕組みが Std.Do の汎用性を示していることは明らかであり、将来の記事でさらに探究してみる価値があるでしょう。

Lean は対話的なシステムなので、これから示す解説を理解するには Lean を開いて一緒に試すのが一番わかりやすいです。 ここをクリックすると、証明があらかじめ入力されたオンライン Lean Playground が開きます。 証明中のさまざまな箇所にカーソルを置くことで、その時点で Lean がどのように認識しているかを確認できます。

Lean におけるホーア三つ組の構文は

⦃前提条件⦄ コマンド ⦃事後条件⦄

という形で書かれます。 これを用いて、先ほどの pairsSumToZero 関数の正しさの性質を次のように述べることができます。

open Std Do

/-- `l.ExistsPair P` は、添字 `i` と `j` が存在して `i < j` かつ `P l[i] l[j]` が成り立つことを主張する。 -/
structure List.ExistsPair {α : Type} (P : α → α → Prop) (l : List α) where
  not_pairwise : ¬l.Pairwise (¬P · ·)

theorem pairsSumToZero_correct (l : List Int) : pairsSumToZero l ↔ l.ExistsPair (fun a b => a + b = 0) := by
  sorry