TL;DR
- 等式推論は、プログラムの間に成り立つ等式を使ってプログラムを変形する手法で、実装の高速化・導出や性質の証明に使える。
- Lean は正格で純粋なので、Lean 上の
a = bをそのままプログラムの等しさと見なせ、等式の証明も Lean が検証してくれる。
内容
等式推論とは
等式推論は、プログラムを数式のように扱う考え方である。プログラムの間には等式が成り立つので、その等式を使ってプログラムを変形できる。主な使い道は、実装の高速化・導出と、プログラムの性質の証明である。
高速化・導出の例として、reverse してから map して再び reverse したものが map と等しいことや、高速な List.scanl の導出が紹介された。後者では計算量を から に改善し、元の関数と等しいことも証明できる。性質の証明の例としては、scanl f init xs の i 番目の要素が (xs.take i).foldl f init と等しいことが示された。
等式の意味
a = b は、a と b を置き換えてもよいという意味である（ライプニッツ則）。Lean の rw タクティクが使えるのもライプニッツ則のおかげである。
では、関数が等しいとはどういうことか。Lean では関数外延性により、入出力の関係として等しい関数は等しい。このときアルゴリズムや計算量の違いは無視される。一方、等式推論での等しさは、プログラムが同じ値に評価されることである。つまり、等しい式で置き換えても、プログラムの観測できる振る舞いが変わらないことを指す。
関数型と等式推論
一般的な手続き型言語では、副作用があると等式推論が難しい。関数型プログラミングでは等式推論を扱いやすく、純粋関数なら簡単で、副作用を分離できるとうれしい。ただし言語にもよる。Haskell では undefined の扱いが問題になり、OCaml や SML には Benign effects がある。一方 Lean は正格で純粋なので、プログラムの等しさが単純である。Lean 上の a = b とプログラムの等しさが一致していると考えてよく、等式の証明も Lean が検証してくれる。
Lean で証明することの限界
Lean が最近よく話題になるのは、証明の信頼を「誰が言ったか」から「機械的に検証できるか」へ移せるからで、これ自体は良いことである。ただし、Lean は定義が正しいことを保証しない。形式的な定義が、人間の頭の中の定義と同じ意味を持つとは限らない。Lean ができるのは、与えられた定義のもとで厳密に議論することまでである。定義は人間がチェックすればよいが、人間も間違える。
発展
さらに学ぶ題材として、次のものが挙げられた。
- コンパイラ・プログラム変換の導出（融合変換で中間データ構造を最適化で消す）
- Recursion schemes（
fold/unfoldを代数的データ型に一般化したもの） - Datatype-generic programming
- Traversable、Lens
- Functional Pearls