前回の日報で、繰り返し二乗法を実装したというお話をしました。*1
何かを実装したら、それが Mathlib 等にあるのかを確認したほうが良いです。実際に調べてみました。
Mathlib で定理や定義の検索を行うには Moogle というツールがよく使われます。
ここで "repeated squaring" で検索してみたところ、どうもヒットがないようでした。Lean search というツールもあります。これでも同様に調べたところ、ヒットがないようでした。ひょっとして Mathlib や標準ライブラリにまだ存在しないのでしょうか。
「繰り返し自乗法のような基本的なものがないのは変だが…？」と思いつつ Zulip で訊いてみたところ、やはり実際には Mathlib に存在するようでした。以下がその実装ですね。
/-- Exponentiation by repeated squaring. -/
@[to_additive existing]
def npowBinRec {M : Type*} [One M] [Mul M] (k : ℕ) (m : M) : M :=
go k 1 m
where
/-- Auxiliary tail-recursive implementation for `npowBinRec`-/
go : ℕ → M → M → M
| 0, y, _ => y
| (k + 1), y, x =>
let k' := (k + 1) >>> 1
if k &&& 1 = 1 then
go k' y (x * x)
else
go k' (y * x) (x * x)
cf: Mathlib.Algebra.Group.Defs
DocString にしっかり繰り返し自乗法であると書かれているのにヒットしなかったわけで、ライブラリ検索ツールにヒットしなかったのは不思議ですね。今後は、Moogle 等のツールを使うだけでなくソースから検索するのも一度は試した方がよさそうです。
また、繰り返し自乗法は Mathlib というよりは Lean の標準ライブラリにあった方が良い気がしますが、それは今後 upstream されるのでしょう、きっと。
更におもしろい話を教えてもらいました。
Mathlib のコミット 341d9cf で導入されているように、Mathlib.Algebra.Group.Defs においてコンパイラ実装置換の補題が登録されているため、自動的に効率的な実装に置換するということをやってくれるようです。このコミットが行われたのは今年の10月15日で、結構最近だというのもおもしろいです。
このコミットにより、今まで (3 : ZMod 49999)^49998 の計算などで起こっていた stack overflow （メモリあふれ現象）が起こらなくなったようです。めでたいですね。
（以下は有料部分になっていますが、お礼が書かれているだけです。）
*1: 繰り返し二乗法は、ある数で割った余りを求める場合にいうことも多いようですが、ここではそうではありません
