配列と関数の停止

効率的なコードを書くためには、適切なデータ構造を選択することが重要です。連結リストには利点があります：アプリケーションによっては、リストの末尾を共有できることが非常に重要な場合もあります。しかし、可変長のシーケンシャルなデータコレクションを使用する場合、メモリのオーバーヘッドが少なく、局所性にも優れた配列の方が大体の場合において適しています。

しかし、配列はリストに対して2つの欠点を持っています：

配列はパタンマッチではなくインデックスによってアクセスされます。これにあたっては安全性を維持するために証明の義務が課せられます。
配列全体を左から右に処理するループは末尾再帰関数ですが、呼び出すたびに減少する引数を持ちません。

配列を効果的に使うには、配列のインデックスが範囲内にあることをLeanに証明する方法と、配列のインデックスが配列のサイズに到達した際にプログラムが終了することの証明の方法を知る必要があります。これらはどちらも命題の等式ではなく、不等式の命題を使って表現されます。

不等式

型によって順序の概念が異なるため、不等式は LE と LT と呼ばれる2つの型クラスによって管理されています。標準型クラスの節での表は、これらのクラスが以下の構文とどのように関係しているかを説明します：

式	脱糖後の式	型クラス名
`x < y`	`LT.lt x y`	`LT`
`x ≤ y`	`LE.le x y`	`LE`
`x > y`	`LT.lt y x`	`LT`
`x ≥ y`	`LE.le y x`	`LE`

言い換えると、ある型において < と ≤ 演算子の意味をカスタマイズすることができ、> と ≥ は < と ≤ から意味を派生させることができます。クラス LT と LE は Bool 値ではなく命題を返すメソッドを持ちます：

class LE (α : Type u) where
  le : α → α → Prop

class LT (α : Type u) where
  lt : α → α → Prop

LE の Nat についてのインスタンスは Nat.le に委譲されています：

instance : LE Nat where
  le := Nat.le

Nat.le を定義するにはまだ紹介していないLeanの特徴が必要です：帰納的に定義された関係です。

Nat.le は 帰納的に定義された関係 （inductively-defined relation）です。inductive は新しいデータ型を作ることに使われるのと同じように、これは新しい命題を作るのにも使われます。命題が引数を取る場合、これは述語（predicate）とよばれ、引数に対して真であるものが全てでなくいくつかだけだったりします。複数の引数を取る命題は関係（relation）と呼ばれます。

帰納的に定義された命題の各コンストラクタは、その命題を証明するための方法です。言い換えれば、命題の宣言はそれが真であることを証明する様々な形式を記述しています。1つのコンストラクタを持つ引数のない命題の証明は非常に簡単です：

inductive EasyToProve : Prop where
  | heresTheProof : EasyToProve

この証明は以下のコンストラクタから構成されます：

theorem fairlyEasy : EasyToProve := by
  constructor

命題 True もまた簡単に証明できますが、実は EasyToProve と同じように定義されています：

inductive True : Prop where
  | intro : True

引数を取らない帰納的に定義された命題は帰納的に定義されたデータ型よりは面白みに欠けます。というのもデータはそれ自体の正しさに興味があるからです。例えば自然数 3 と 35 は異なりますし、ピザを3枚注文して、30分後に35枚届いたら腹が立つでしょう。命題のコンストラクタはその命題が真になりうる方法を記述していますが、命題が証明されてしまえば、どのコンストラクタが使われたかを知る必要はありません。これが Prop の宇宙で興味深い帰納的に定義される型のほとんどが引数を取る理由です。

帰納的に定義された述語 IsThree はその引数が3であることを示します：

inductive IsThree : Nat → Prop where
  | isThree : IsThree 3

ここで使用されるメカニズムは HasCol のような添字族と同様ですが、結果として得られる型は利用可能なデータではなく証明可能な命題です。

この述語を使って、3が本当に3であることを証明できます：

theorem three_is_three : IsThree 3 := by
  constructor

同様に、IsFive は引数が 5 であることを示す述語です：

inductive IsFive : Nat → Prop where
  | isFive : IsFive 5

もしある数値が3であるなら、これに2を加えると結果は5になるはずです。これは定理の文として表すことができます：

theorem three_plus_two_five : IsThree n → IsFive (n + 2) := by
  skip

結果のゴールは関数型を持ちます：

unsolved goals
n : Nat
⊢ IsThree n → IsFive (n + 2)

そのため、intro タクティクによって引数を仮定に変換できます：

theorem three_plus_two_five : IsThree n → IsFive (n + 2) := by
  intro three

unsolved goals
n : Nat
three : IsThree n
⊢ IsFive (n + 2)

n が3であるという仮定を使って、IsFive のコンストラクタを使って証明を完成させることができるはずです：

theorem three_plus_two_five : IsThree n → IsFive (n + 2) := by
  intro three
  constructor

しかし、これはエラーになります：

tactic 'constructor' failed, no applicable constructor found
n : Nat
three : IsThree n
⊢ IsFive (n + 2)

このエラーは n + 2 が 5 と定義上等しくないために起こります。通常の関数定義では、仮定 three への依存パターンマッチによって n を 3 に絞り込むことができます。依存パターンマッチに相当するタクティクは cases で、これは induction と似た構文を持っています：

theorem three_plus_two_five : IsThree n → IsFive (n + 2) := by
  intro three
  cases three with
  | isThree => skip

これによって得られるケースにおいて n は 3 に絞り込まれます：

unsolved goals
case isThree
⊢ IsFive (3 + 2)

3 + 2 は 5 に定義上等しいため、これでこのコンストラクタを適用可能です：

theorem three_plus_two_five : IsThree n → IsFive (n + 2) := by
  intro three
  cases three with
  | isThree => constructor

標準的な偽についての命題 False はコンストラクタを持ちません。これによって偽を証明するために直接根拠を提供することは不可能になっています。False の根拠を提供する唯一の方法は、仮定自体が不可能である場合です。これは nomatch を使って、到達不可能であることが型システムによってわかっているコードをマークすることができることと同様です。証明に関する最初の幕間で説明したように、否定 Not A は A → False の略です。Not A は ¬A と書くこともできます。

4は3ではありません：

theorem four_is_not_three : ¬ IsThree 4 := by
  skip

証明の初期のゴールは Not を含みます：

unsolved goals
⊢ ¬IsThree 4

これが実際には関数型であることは simp を使って明らかにできます：

theorem four_is_not_three : ¬ IsThree 4 := by
  simp [Not]

unsolved goals
⊢ IsThree 4 → False

ゴールは関数型であるため、intro を使って引数を仮定に変換することができます。intro は Not の定義をのものを展開することができるため、simp を使う必要はありません。

theorem four_is_not_three : ¬ IsThree 4 := by
  intro h

unsolved goals
h : IsThree 4
⊢ False

この証明では、cases タクティクによってゴールが即座に解決されます：

theorem four_is_not_three : ¬ IsThree 4 := by
  intro h
  cases h

Vect String 2 のパターンマッチに Vect.nil のケースを含める必要がないように、IsThree 4 のケースによる証明に isThree のケースを含める必要はありません。

整数の不等式

Nat.le の定義にはパラメータと添字が含まれます：

inductive Nat.le (n : Nat) : Nat → Prop
  | refl : Nat.le n n
  | step : Nat.le n m → Nat.le n (m + 1)

パラメータ n は小さい方の数であり、添字は n 以上となるはずの数です。両方の数値が等しい場合は refl コンストラクタを使用し、添字が n より大きい場合は step コンストラクタを使用します。

根拠の観点からすると、 \( n \leq k \) の証明は \( n + d = k \) ¹となるような \( d \) である数を見つけることから構成されます。Leanでは、この証明は Nat.le.step の \( d \) についてのインスタンスでラップされた Nat.le.refl コンストラクタから構成されます。各 step コンストラクタはその添字引数に1を加えるため、 \( d \) 回の step コンストラクタは大きい数に \( d \) を加算します。例えば、4が7以下である根拠は refl を囲む3つの step で構成されます：

theorem four_le_seven : 4 ≤ 7 :=
  open Nat.le in
  step (step (step refl))

未満関係は左の数字に1を足すことで定義されます：

def Nat.lt (n m : Nat) : Prop :=
  Nat.le (n + 1) m

instance : LT Nat where
  lt := Nat.lt

4が7未満であるという根拠は refl の周りにある2つの step で構成されます：

theorem four_lt_seven : 4 < 7 :=
  open Nat.le in
  step (step refl)

これは 4 < 7 が 5 ≤ 7 と等しい訳です。

停止性の証明

関数 Array.map は配列を関数で変換し、入力配列の各要素に関数を適用した結果を含んだ新しい配列を返します。これを末尾再帰関数として書くと、出力配列をアキュムレータに渡すような関数に委譲するといういつものパターンになります。アキュムレータは空の配列で初期化されます。アキュムレータを渡す補助関数は配列の現在のインデックスを追跡する引数を取り、これは 0 から始まります：

def Array.map (f : α → β) (arr : Array α) : Array β :=
  arrayMapHelper f arr Array.empty 0

補助関数は各繰り返しにて、インデックスがまだ範囲内にあるかどうかをチェックする必要があります。もし範囲内であれば、変換された要素をアキュムレータの最後に追加し、インデックスを 1 だけ加算して再度ループする必要があります。そうでない場合は終了してアキュムレータを返します。このコードの初期実装ではLeanが配列のインデックスが有効であることを証明できないため失敗します：

def arrayMapHelper (f : α → β) (arr : Array α) (soFar : Array β) (i : Nat) : Array β :=
  if i < arr.size then
    arrayMapHelper f arr (soFar.push (f arr[i])) (i + 1)
  else soFar

failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is perfomed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
α : Type ?u.1704
β : Type ?u.1707
f : α → β
arr : Array α
soFar : Array β
i : Nat
⊢ i < Array.size arr

しかし、この条件式ではすでに配列のインデックスの有効性が要求する正確な条件（すなわち i < arr.size ）をチェックしています。if に名前を追加することで、配列のインデックスのタクティクが使用できる仮定が追加されるため、問題は解決します：

def arrayMapHelper (f : α → β) (arr : Array α) (soFar : Array β) (i : Nat) : Array β :=
  if inBounds : i < arr.size then
    arrayMapHelper f arr (soFar.push (f arr[i])) (i + 1)
  else soFar

しかし、Leanはこの修正されたプログラムを受け付けません。なぜなら、再帰呼び出しが入力コンストラクタの1つの引数に対して行われていないからです。実際、アキュムレータもインデックスも縮小するのではなく、むしろ増大します：

fail to show termination for
  arrayMapHelper
with errors
argument #6 was not used for structural recursion
  failed to eliminate recursive application
    arrayMapHelper f✝ arr (Array.push soFar (f✝ arr[i])) (i + 1)

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

とはいえこの関数は停止するため、単に partial とマークするのはあまりに残念です。

なぜ arrayMapHelper は停止するのでしょうか？各繰り返しはインデックス i が配列 arr の範囲内にあるかどうかをチェックします。もし真であれば、i が加算され、ループが繰り返されます。そうでなければプログラムは終了します。arr.size は有限な値であるため、i を加算できる回数も有限回です。関数を呼び出すたびに引数が減らない場合でも、arr.size -i は0に向かって減っていきます。

Leanは定義の最後に termination_by 節を記述することで、停止について別の式を使うように指示することができます。termination_by 節には2つの要素があります：関数の引数の名前と、その名前を使っており各呼び出しのたびに値が減るべき式です。arrayMapHelper の場合、最終的な定義は以下のようになります：

def arrayMapHelper (f : α → β) (arr : Array α) (soFar : Array β) (i : Nat) : Array β :=
  if inBounds : i < arr.size then
    arrayMapHelper f arr (soFar.push (f arr[i])) (i + 1)
  else soFar
termination_by arrayMapHelper _ arr _ i _ => arr.size - i

同様の停止証明を使って、ある真偽値関数を満たす配列の最初の要素を見つけ、その要素をインデックスの両方を返す関数 Array.find を書くことができます：

def Array.find (arr : Array α) (p : α → Bool) : Option (Nat × α) :=
  findHelper arr p 0

ここでもまた、i が増加すると arr.size - i が減少するのでここでも補助関数は終了します：

def findHelper (arr : Array α) (p : α → Bool) (i : Nat) : Option (Nat × α) :=
  if h : i < arr.size then
    let x := arr[i]
    if p x then
      some (i, x)
    else findHelper arr p (i + 1)
  else none
termination_by findHelper arr p i => arr.size - i

すべての停止引数がこれほど単純であるとは限りません。しかし、関数の引数に基づいで呼び出しのたびに減少する式を特定するという基本的な構造は、全ての停止証明で発生します。時には関数が停止する理由を解明するために想像力が要求されることもありますし、またLeanが停止引数を受け入れるために追加の証明を必要とすることもあります。

演習問題

末尾再帰のアキュムレータを渡す関数と termination_by 節を使って配列に対して ForM (Array α) インスタンスを定義してください。
termination_by を 必要としない 末尾再帰のアキュムレータを渡す関数を使用して配列を反転させる関数を実装してください。
恒等モナドの for ... in ... ループを使って Array.map ・Array.find ・ForM インスタンスを再実装し、結果のコードを比較してください。
配列の反転を恒等モナドの for ... in ... ループを使って再実装してください。またそれを末尾再帰版と比較してください。

原文では \( n + d = m \) となっていたが、mとkの書き間違いと思われる。

Functional Programming in Lean 日本語訳

配列と関数の停止

不等式

帰納的に定義された命題・述語・関係

整数の不等式

停止性の証明

演習問題