Lean4 で ICan'tbelieveItCanSort を書く
はじめに
この記事は nesken7777 さんによる「Lean4でバブルソートを書く」に深く感銘を受けて、バブルソートよりももっと簡単なソートアルゴリズムなら、自分でも Lean4 で実装できるのではと取り組んでみたものになります。実装ではほとんど nesken7777 さんの記事に基づいて行っていますので、理論的・技術的に有用な情報はぜひともそちらをご覧ください。(ということで、本記事は「やってみた」の報告です。)
ソートアルゴリズム
今回、実装に取り組むソートアルゴリズムは Stanley P. Y. Fung が arXiv, "Is this the simplest (and most surpring) sorting algorithm ever?" にて発表した、ICan'tbelieveItCanSort です。
疑似コードを示します。サイズ n の配列 A の要素が非減少順にソートされます。
# A[1..n]を非減少順にソートする
for i = 1 to n do
for j = 1 to n do
if A[i] < A[j] then
swap A[i] , A [j]
特徴は外側のループだけでなく内側のループも 1 から n まで回るところです(n は配列 A のサイズ)。そのおかげでアルゴリズムが非常に単純な形となっています。
一見、本当にソートされるのか不明ではあるのですが、非減少順にソートされることが Fung の論文でも証明されています。
書く
なんと普通にforで書けました!
-- 境界チェック無し バージョン
def ICantBelieveItCanSort! {α : Type} [Inhabited α] [Ord α] (arr : Array α)
: Array α := Id.run do
let mut arr := arr
for i in [0:arr.size] do
for j in [0:arr.size] do
match Ord.compare arr[i]! arr[j]! with
|.lt => arr := arr.swapIfInBounds i j
|.gt |.eq => pure ()
arr
#eval ICantBelieveItCanSort! #[3,1,4,1,5,9,2,6,5,3]
-- #[1, 1, 2, 3, 3, 4, 5, 5, 6, 9]
驚きました。(nesken7777 さんの記事のコードをほぼそのまま流用しました)
境界チェック
次のステップは、for の繰り返しを再帰に書き換えたうえで、その再帰が停止することを証明することですが、今回はそこはさぼります。私ではまだ実力不足でした[1]。
代わりに(?)ここでは for の形のままで、配列の要素を取得する際の境界チェックだけを行います。
index i が配列 arr の範囲内にあることの証明を与えることができれば(範囲外アクセス時にpanicを起こすarr[i]! ではなく)、 arr[i] によって i 番目の要素を得ることができます。
証明項 hi' : i < arr.size と hj` : j < arr.size がうまく取れれば、次のようなコードで境界チェックの証明が付いたコードが得られるはずです。
-- 境界チェックのお気持ちコード
def ICantBelieveItCanSort' {α : Type} [Ord α] (arr : Array α) : Array α := Id.run do
let mut arr := arr
for hi : i in [0:arr.size] do
for hj : j in [0:arr.size] do
have hi' : i < arr.size := sorry
have hj' : j < arr.size := sorry
match Ord.compare arr[i] arr[j] with
|.lt => arr := arr.swap i j
|.gt |.eq => pure ()
arr
あとは、sorry のところの証明をちゃんと書けば大丈夫なはず。なのですが、nesken7777 さんの記事でも検討されているように、事はそう単純ではないようです。
nesken7777 さんの記事の Discussion での、ebi_chan さんのコメントにて、Subtype を使って Array の size に関する情報を入れておくとよいとありました。
そのコメントでのコードを参考に、修正したのがこちらになります。
-- 境界チェック証明あり バージョン
def ICantBelieveItCanSort {α : Type} [Ord α] (arr : Array α) : Array α := Id.run do
let size := arr.size
let mut arr : {arr : Array α // arr.size = size } := ⟨arr, rfl⟩
for hi : i in [0:size] do
for hj : j in [0:size] do
have hi' : i < size := hi.upper
have hj' : j < size := hj.upper
match Ord.compare arr.val[i] arr.val[j] with
|.lt => arr := ⟨arr.val.swap i j, by rw [Array.size_swap, arr.property]⟩
|.gt |.eq => pure ()
arr.val
#eval ICantBelieveItCanSort #[3,1,4,1,5,9,2,6,5,3]
-- #[1, 1, 2, 3, 3, 4, 5, 5, 6, 9]
無事に境界チェックの証明が入った ICantBelieveItCanSort を得ることができました。
俺たちの戦いはこれからだ!
次に取り組むべきことは、再帰の形にしてループが停止することを証明することになるでしょうか[2]。
また、ICan'tBelieveItCanSort がソートアルゴリズムであること自体を証明したわけではありませんので、その証明もいつの日か取り組みたいと思います。
追記：末尾再帰バージョン
ループを末尾再帰の形に書き換えることができました。
再帰の停止証明については、nesken7777 さんの記事で追記された Functional Induction を用いて行いました。
def Tail.iCantBelieveItCanSort {α : Type} [Ord α] (arr : Array α) : Array α :=
let rec loop_i [Ord α] (arr : Array α) (i : Nat) : Array α :=
let rec loop_j [Ord α] (arr : Array α) (i : Nat) (j : Nat) (inBounds_i : i < arr.size): Array α :=
if inBounds_j : j < arr.size then
match Ord.compare arr[i] arr[j] with
| .lt =>
-- i < arr.size の証明から i < (arr.swap i j).size の証明を作る
have inBounds_i' : i < (arr.swap i j).size := by
simp [Array.size_swap]
assumption
loop_j (arr.swap i j) i (j + 1) inBounds_i'
| .gt | .eq => loop_j arr i (j + 1) inBounds_i
else
arr
if inBounds_i : i < arr.size then
loop_i (loop_j arr i 0 inBounds_i) (i + 1) -- 内側のループ loop_j に i < arr.size の証明を渡す
else
arr
termination_by arr.size - i
decreasing_by
have loop_j_size_eq (arr : Array α) (i : Nat) (j : Nat) (inBounds_i : i < arr.size)
: (iCantBelieveItCanSort.loop_i.loop_j arr i j inBounds_i).size = arr.size := by
-- Functional induction を用いて証明
-- https://lean-lang.org/blog/2024-5-17-functional-induction/
induction arr, i, j, inBounds_i using iCantBelieveItCanSort.loop_i.loop_j.induct
<;> (unfold iCantBelieveItCanSort.loop_i.loop_j ; simp [*])
rw [loop_j_size_eq]
exact Nat.sub_succ_lt_self arr.size i inBounds_i
loop_i arr 0
#eval Tail.iCantBelieveItCanSort #[3,1,4,1,5,9,2,6,5,3]
-- #[1, 1, 2, 3, 3, 4, 5, 5, 6, 9]
ソースコード
今回のソースコードはこちらに置いています。
Discussion