繰り返し自乗法による高速化

[Seasawher]

/-- notation class for `1` -/
class One (α : Type) where
  one : α

instance {α : Type} [One α] : OfNat α 1 where
  ofNat := One.one

/-- repeated squaring algorithm -/
def RepeatedSquare {α : Type} [Mul α] [One α] (x : α) (n : Nat) : α :=
  if n = 0 then
    1
  else if n % 2 = 0 then
    (RepeatedSquare (x * x) (n / 2))
  else
    x * (RepeatedSquare x (n - 1))

/-- naive power algorithm (tail recursive) -/
def naivePower (x n : Nat) :=
  aux x n 1
where
  aux (x n acc : Nat) :=
    match n with
    | 0 => acc
    | n + 1 => aux x n (acc * x)

instance : One Nat where
  one := 1

-- Question: the execution times of the two functions are not very different. why?
#time #eval RepeatedSquare 2 135000
#time #eval RepeatedSquare 2 135000

[Seasawher]

Zulip: repeated squaring algorithm

[Seasawher]

長大な数値の出力に時間がかかっているからだった