Add doubling algorithm for exponentiation in `Algebra`

[mechvel]

lib-2.0-rc1 has Algebra/Properties/Semiring/Exp

I undertsand it so that it defines _^_ for a semiring via importing _^_ from `*-monoid'.

If so, than this has sense, because most of the properties of ^ can be proved for Monoid, and one has not to prove them twice. Then, there follows TailRecursiveOptimised.agda, which gives a certain optimization for ^ -- which I do not understand, so far.

But it is possible optimization of _^_ via the binary method for exponentiation.

For Monoid :

private                                                                           
  _^'_ : C → ℕ → C                                                                
  _ ^' 0       =  ε                                                               
  x ^' (suc n) =  x ∙ (x ^' n)                                                    
  --                                                                              
  -- An auxiliary and naive method for `power'. It is used to provide proofs      
  -- for _^_, which is equivalent to _^'_.                                        

  -- First prove the properties of  ^' :
  
  ^'1 :  (x : C) → x ^' 1 ≈ x
  ...
  ε^' :  (n : ℕ) → ε ^' n ≈ ε
  ...
  ^'homo+ :  (x : C) (m n : ℕ) →  x ^' (m + n) ≈ (x ^' m) ∙ (x ^' n)              
  ...
  ^'congˡ :  {x : C} → (x ^'_) Preserves _≡_ ⟶ _≈_ 
  ...

open ℕᵇ                                                                           
infixl 8 _^ᵇ_                                                                     
                                                                                  
_^ᵇ_ : C → ℕᵇ → C    -- binary method for exponentiation
_ ^ᵇ zero     =  ε                                                                
x ^ᵇ 2[1+ n ] =  p ∙ p        where p = x ∙ (x ^ᵇ n)                              
x ^ᵇ 1+[2 n ] =  x ∙ (p ∙ p)  where p = x ^ᵇ n                                    

infixl 8 _^_                                                                      
                                                                                  
_^_ : C → ℕ → C     -- use  _^ᵇ_  compose with  fromℕ            
_^_ x =                                                                           
      _^ᵇ_ x ∘ fromℕ                                                              

I believe this is faster (for large n) than the naive method for powering.
Because  fromN  for ℕᵇ  takes  O(log(n))  operations, and _^ᵇ_ also takes O(log(n)) multiplications.

Then, it is proved 
  ^≗^' :  ∀ x n → x ^ n ≈ x ^' n 

And all the properties for _^_ are proved by porting the proofs for _^'_ by using ^≗^'. ?

[MatthewDaggitt]

I'm afraid I don't quite understand what your question is. Please could you state it explicitly?

[mechvel]

The `?' symbol meant ``What people think of this?''.

1. Exponentiation x ^ n in Monoid can be optimized to work faster at run time. i suggest this optimization. This is by converting n to binary nB : ℕᵇ and applying x ^ᵇ nB,
   where _^ᵇ_ : Carrier → ℕᵇ → Carrier is implemented as shown above (the binary method for exponentiation). This is shown above. The computation takes O(log(n)) operations, while the naive method takes O(n) operations. The property proofs for this _^_ are implemented as shown above. And the whole design is simple.

2. Further, exponentiation ^ in Semiring R can be implemented as ^ of its monoid Semiring.*-monoid R -- I have an impression that this is already in lib-2.0-rc1.

[MatthewDaggitt]

The `?' symbol meant ``What people think of this?''.

Thanks. In general, it'll definitely go faster if you explicitly state the question you wanted answered, rather than sticking a ? at the end of a long block of text.

Yup, if you want to add the optimised version of exponentiation then there's no problem with that. However, I think I would recommend doing it using the standard ℕ rather than ℕᵇ.