Conao3 Notes

Lean 4で証明した関数をClojureから呼べるlean-cljを作った

Lean 4 で書いて証明した関数を Clojure から呼び、Clojure で書いた関数の性質を Lean で証明するためのライブラリとして lean-clj を作りました。 リポジトリは conao3/lean-clj で、ライセンスは Apache-2.0 です。 Clojars に io.github.conao3/lean-clj として公開していて、この記事は 0.3.0 をもとに書いています。

lean-clj は Lean のコンパイラの中間表現 (IR) を Clojure のソースに変換します。 JVM の上では、Lean の C backend がビルドするのと同じプログラムから型と証明を消したものが動きます。

conao3/lean-cljLean 4 IR to Clojure backend and Lean embedded in Clojure via S-expressionsClojureStar

3 つの使い方

lean-clj には次の 3 つの使い方があります。

img

  1. Clojure のファイルの中に Lean で関数と定理を書き、Clojure から呼ぶ ( deflean )。
  2. 既存の Lean のプロジェクト (lake のプロジェクト) を、Clojure の namespace の集まりに変換する (CLI)。
  3. Clojure で書いた関数を Lean のモデルに変換し、その性質を Lean で証明する ( lean-clj.typed )。

1 と 2 は Lean から Clojure への向き、3 は Clojure から Lean への向きです。 以下、この順に例を挙げます。

Lean で書いて Clojure から呼ぶ

deps.edn に lean-clj を追加します。

{:deps {io.github.conao3/lean-clj {:mvn/version "0.3.0"}}}

deflean のブロックを最初に展開するときは、Lean 4.35.0 ( lean と lake ) と lean-clj の CLI が PATH に要ります。 CLI は nix でインストールできます。

$ nix profile install github:conao3/lean-clj/v0.3.0

deflean の本体には Lean の構文を S 式にしたものを書きます。

(ns demo.core
  (:refer-clojure :exclude [double])
  (:require [lean-clj.core :refer [deflean]]))

(deflean arith
  (def double [n Nat] Nat
    (+ n n))

  (theorem double_eq [n Nat] (= (double n) (* 2 n))
    (by (unfold double) omega))

  (structure Account [owner String balance Nat])

  (def deposit [a Account n Nat] Account
    (with a {:balance (+ (.balance a) n)})))

def で関数を、 theorem で定理を定義し、 (by ...) の中に証明を書きます。 double_eq では、 double の定義を展開してから、自然数と整数の線形算術を解くタクティク omega で等式を示しています。 namespace を読み込むと、lean-clj はブロックを Lean のソースに変換して lake build を実行し、証明まで検査します。 検査が通ると、ブロックの関数がその namespace の Clojure の関数になります。 structure の値は keyword を key に持つ map として受け渡します。

(double 21)                                ;=> 42
(deposit {:owner "ann" :balance 10} 5)     ;=> {:owner "ann", :balance 15}

証明が通らないと、namespace のコンパイルが止まります。 定理の右辺を (* 3 n) に書き換えて namespace を読み込むと、次のエラーになります。

Syntax error macroexpanding deflean at (demo/wrong.clj:5:1).
lean-clj: Lean rejected deflean arith
error: demo/wrong.clj:9: deflean arith:3:75: omega could not prove the goal:
a possible counterexample may satisfy the constraints
  a ≥ 1
where
 a := ↑n

Lean source of the block:
   1 | def double (n : Nat) : Nat := (n + n)
   2 |
   3 | theorem double_eq (n : Nat) : ((double n) = (3 * n)) := (by unfold double; omega)

エラーのメッセージには Clojure のファイルと行 ( demo/wrong.clj:9 ) と、ブロックから作った Lean のソースが含まれます。

S 式で書けない構文は (lean "...") で Lean のソースを文字列のまま混ぜて書けます。 サンプルの word-count は、 do 記法の関数をこの形で書いています。 生成した Clojure のコードは .lean-clj/cache/ に保存されます。 ブロックを変えなければ、2 回目からは Lean を呼ばずにキャッシュから展開するので、キャッシュをリポジトリに入れておけば Lean の無い環境でも動きます。

Lean のプロジェクトを Clojure の namespace にする

lake のプロジェクトとして書いた Lean のコードも、CLI で Clojure の namespace に変換できます。 サンプルの roman-numerals は、整数とローマ数字の変換を Lean で書き、1〜999 の数をローマ数字にして戻すと元の数になることを証明しています。

def toRoman (n : Nat) : String := toRomanAux (n + 13) numerals n

def fromRoman (s : String) : Option Nat :=
  if s.isEmpty then none else fromRomanAux s.toList

theorem roundtrip : ∀ n, n < 1000 → fromRoman (toRoman n) = if n = 0 then none else some n := by
  decide +kernel

lake build で証明を検査したあと、CLI で module を namespace に変換します。

$ lean-clj module generate-namespace --module-name Roman --namespace roman.core \
    --search-path lean/.lake/build/lib/lean --output-file src/roman/core.clj

公開している関数は名前を kebab-case にした Clojure の関数になります。 Option の値は some の中身か nil になります。

(require '[roman.core :as roman])

(roman/to-roman 1994)        ;=> "MCMXCIV"
(roman/from-roman "MMXXVI")  ;=> 2026
(roman/from-roman "hello")   ;=> nil

生成した src/roman/core.clj は普通の Clojure のファイルなので、リポジトリに commit すれば、使う側に Lean は要りません。 プロジェクトの module をまとめて変換するときは lean-clj project generate を使います。

Clojure で書いて Lean で証明する

3 つ目の使い方では、実装を Clojure で書きます。 次の例では、0 から n までの和を閉じた式で計算する Clojure の関数が、和の定義どおりに再帰する Lean の仕様と等しいことを証明します。

(ns demo.sum
  (:require [lean-clj.core :refer [deflean]]
            [lean-clj.typed :as lt]))

(lt/defn sum-to-fast [n Nat] Nat
  (quot (* n (inc n)) 2))

(deflean sums
  (clojure sum-to-fast)

  (def sum-to [n Nat] Nat
    (match n
      0 0
      (+ k 1) (+ (sum-to k) (+ k 1))))

  (theorem two-sum-to [n Nat] (= (* 2 (sum-to n)) (* n (+ n 1)))
    (by (on-all (induction n) (simp only [sum-to Nat.mul_add Nat.add_mul] at *) omega)))

  (theorem sum-to-fast-eq [n Nat] (= (sum-to-fast n) (sum-to n))
    (by (simp only [sum-to-fast Clj.quot_nat Clj.mul_nat Clj.inc_nat])
        "have := twoSumTo n"
        omega))

  (theorem ^{:attrs [csimp]} sum-to-eq [] (= (the (-> Nat Nat) sum-to) sum-to-fast)
    (by (funext n) (exact (.symm (sum-to-fast-eq n))))))

lt/defn は普通の Clojure の関数を定義し、引数と戻り値の Lean の型 (signature) を var に記録します。 ブロックの中の (clojure sum-to-fast) は、その関数を Lean の定義に変換します。 この記事では、変換した Lean の定義をモデルと呼びます。 quot や inc のような clojure.core の関数のモデルは、lean-clj に同梱した Lean のライブラリ Clj にあります。

sum-to-eq に付けた @[csimp] は、 sum-to をコンパイルするときに sum-to-fast へ置き換えることを Lean に許す属性です。 置き換えてよい根拠は、2 つの関数が等しいという証明です。 そのため、Clojure から sum-to を呼ぶと、再帰ではなく Clojure の sum-to-fast が実行されます。

(sum-to 1000000)  ;=> 500000500000

この形は Leanで書く証明付きの日付と税計算 で紹介した lean-ritsuryo の書き方を、Clojure の実装に当てはめたものです。 実装と仕様の関係ごとに、次のサンプルがあります。

実装と仕様の関係 lean-clj での書き方 サンプル
仕様をそのまま実行する deflean の定義を呼ぶ todo-cli
速い実装がすべての入力で仕様と一致する 等しいことを証明し、 @[csimp] で置き換える verified-clojure ( sum-to )
速い実装が仮定のもとで仕様と一致する 仮定付きで証明し、仮定を満たす呼び出し側が実装を呼ぶ sorted-search
実装が結果の条件を満たす 条件を定理にして証明する verified-clojure (挿入ソート)、inventory

本物の関数とモデルを生成テストで比べる

証明が示すのはモデルの性質です。 モデルの挙動が Clojure の関数と食い違っていれば、本物の関数では成り立たない定理も証明できてしまいます。 そこで、 lt/check を使って本物の関数とモデルを同じ入力で呼び、結果を比べます。

(lt/check #'sum-to-fast {:seed 1})
;=> {:result true, :pass? true, :num-tests 100, :time-elapsed-ms 7, :seed 1}

lt/check は signature から、テストの入力を作る test.check の generator を生成します。 結果が食い違ったときは、引数と両方の戻り値を :counterexample に入れて返します。 lt/defcheck を使うと、同じ検査を clojure.test のテストとして定義できます。 lean-clj のテストでも、 Clj のモデルを clojure.core の関数と生成テストで照合していて、照合の表は 156 行あります。

定理は Clojure の関数が値を返す呼び出しについて成り立ちます。 Long の overflow、0 での除算、範囲外の index のように例外を投げる呼び出しは、モデルの対象外です。

生成テストで見つかったモデルの誤り

照合の生成テストで、モデルの誤りがいくつも見つかりました。 誤りの一部は、本物の関数では成り立たない定理を証明できるものでした。

多相の関数の真偽

次の member? は、任意の型 α のリスト xs に x があるかを調べます。

(lt/defn member?
  [(implicit α Type) (inst (BEq α)) x α xs (List α)]
  Bool
  (if-let [y (first xs)]
    (or (= x y) (member? x (rest xs)))
    false))

Clojure の if-let は、束縛した値が false か nil のときに else の分岐を取ります。 そのため、 false だけのリストで false を探すと false を返します。

(member? 1 [1])          ;=> true
(member? false [false])  ;=> false

以前のモデルは、型の変数 α の値を真偽の判定で常に真として扱っていました。 Nat や String の値は Clojure でも常に真なので、多くの型ではこの扱いで結果が Clojure と同じになります。 しかし α = Bool のときは false が偽になるので、モデルと Clojure の関数の結果が食い違います。 このモデルでは、「先頭に x があれば member? は true を返す」という次の定理が、すべての α について証明できました。

(theorem member-head [(implicit α Type) (inst (BEq α)) (inst (LawfulBEq α)) (inst (Clj.Truthy α)) x α xs (List α)]
  (= (member? x (cons x xs)) true)
  (by (rw [member?]) simp))

x = false のとき、Clojure の関数は false を返すので、この定理は本物の関数では成り立ちません。

いまのモデルは、型の変数ごとに [Clj.Truthy α] という instance を引数に取り、 α に入る具体的な型の instance で値の真偽を決めます。 同じ定理を証明しようとすると、 x が真であることを示すゴールが残り、証明が失敗します。

error: demo/member.clj:15: deflean proofs:3:128: unsolved goals
...
x : α
xs : List α
⊢ Clj.truthy x = true

サンプルの generic-search は、 nil だけを偽とする if-some で member? を書き、同じ定理を証明しています。

そのほかの誤り

ほかにも、生成テストで次の 3 つの Clojure の挙動がモデルと食い違いました。

(:k {:k nil} 0)                  ;=> nil
(str [12345678901234567890N])    ;=> "[12345678901234567890N]"
(get [0 1] 4294967297)           ;=> 1
  • (:k m default) は、key があって値が nil なら nil を返します。default を返すのは key が無いときだけです。モデルは nil のときにも default を返していました。
  • str は vector の中の BigInt に N を付けます。モデルは N を付けていませんでした。generator は Long に収まらない整数も作るので、この違いが見つかりました。
  • vector の get は、index を int の下位 32 bit に切り詰めます。 4294967297 は 2^32 + 1 なので、index 1 の要素を返します。

どれも、モデルを Clojure の挙動に合わせて直しました。

作らなかったもの

Long の overflow まで含めて、関数が例外を投げないことも証明するモード ( ^:total ) は作りませんでした。 このモードでは、式全体を Option のような例外を表す型の計算として書き直す必要があります。 この書き直しを Lean の do 記法で行うと、評価の順序が Clojure と食い違います。

def half (n : Nat) : Option Nat :=
  if n % 2 == 0 then some (n / 2) else none

def g (n : Nat) : Option Bool := do
  pure (n == 1 || (← half n) == 0)

#eval g 1  -- none

Clojure の (or (= n 1) ...) は、 n が 1 なら右辺を評価せずに true を返します。 Lean は (← half n) を式の外へ出して先に実行するので、右辺の half 1 が失敗し、 g 1 は none になります。 and や or のように途中で評価をやめる式を、すべて Clojure と同じ順序で書き直す必要があり、このモードは変換の手間に見合わないと判断しました。

overflow を避けるには任意精度の +' の系列を使い、見つけるには lt/check に :throws :fail を渡して、例外を投げる入力を失敗として数えます。

仕組み

生成するコードの形式には、Java のソースや JVM のバイトコードではなく Clojure のソースを選びました。 Lean の Array は Clojure の永続ベクタと意味が合い、要素の更新が O(log n) で済みます。 Nat の計算は +' で BigInt に切り替わり、Lean のクロージャは IFn を実装した Clojure の値にできます。 JIT がバイトコードを最適化するので、バイトコードを直接生成しても速さの利点は小さいと考えました。

実行時に動くのは JVM だけです。 Lean が動くのは deflean のブロックを展開するときと、CLI でモジュールを変換するときだけで、実行時は Lean の C の runtime の代わりに、その関数を Clojure で書き直した runtime を使います。 Lean のプロセスも FFI も別のヒープもないので、2 つの runtime のあいだで状態を共有する場面はありません。 Clojure と生成したコードのあいだで受け渡す値はどれも immutable です。 Lean の可変な状態は Clojure の仕組みで動きます。 IO.Ref は atom、 Task は future、 Thunk は delay になり、標準出力は *out* に書くので binding で差し替えられます。

生成した Clojure が正しいことは、Lean の C backend との差分テストで確かめています。 同じテスト用の関数を、C backend がビルドした実行ファイルと、生成した Clojure の両方で実行し、出力の 182 行を比べます。 浮動小数点数の無限大を、C は inf 、Java は Infinity と表示する違いも、このテストで見つかりました。

生成したコードが、JVM の 1 メソッドあたり 64KB という上限を超えたこともありました。 Lean の IR の join point (関数の中で複数の分岐が合流する先) を呼び出し箇所ごとに展開していたため、生成したコードが 36,000 行に膨らみ、 Std.Format の関数の読み込みが「Method code too large!」で失敗しました。 いまは呼び出しが 1 か所の join point だけを展開し、2 か所以上のものは letfn にしています。 自己末尾呼び出しは loop と recur に、相互再帰は trampoline にして、スタックを積まずに実行します。

Clojure の型のライブラリとの関係

Clojure には、clojure.spec、malli、Plumatic Schema のように、値を実行時に検査するスキーマのライブラリがあります。 これらは値を検査する述語を組み合わせて書く仕組みで、型の変数を持たず、map は既定で開いていて、整数の固定精度と任意精度を区別しません。 Typed Clojure と clj-kondo の型検査は、それぞれ独自の型の言語と、 clojure.core の関数の型の注釈を持っています。

lean-clj では型を Lean で書き、その型から malli のスキーマ、test.check の generator、clj-kondo の型を生成します。 deflean で定義した structure Account からは、次の malli のスキーマができます。

(require '[lean-clj.types :as t])

(t/malli-schema 'Account)
;=> [:map {:closed true} [:owner :string] [:balance [:and integer? [:>= 0]]]]

Nat は 0 以上の整数に、structure は同じ key を持つ閉じた map になります。 証明を書かなくても、signature からこれらを使えます (サンプルの typed-schemas)。

近い領域のプロジェクトに、whilo さんの ansatz があります。 ansatz は Lean のカーネルを Java で実装し、JVM だけで型の検査を済ませます。 lean-clj は本物の Lean で検査し、Lean の構文と標準ライブラリ、既存の lake のプロジェクトをそのまま使います。 その代わり、 deflean の初回の展開には Lean の toolchain が要ります。

おわりに

lean-clj は Clojars の io.github.conao3/lean-clj から入手できます。 samples には使い方ごとの小さなサンプルがあり、 deflean は todo-cli から、Clojure の関数の検証は verified-clojure から読むのがおすすめです。 Issue / PR 大歓迎です。