[isabelle-dev] Exponentiation by squaring

[Thiemann, René]

Dear Manuel,

in the AFP there is Subresultants/Binary_Exponentiation.thy. Perhaps your changes make this theory obsolete.

The Binary_Exponentiation algorithm is then later on used in Berlekamp-Zassenhaus in modular arithmetic to compute inverses in prime-fields.

Cheers,
René


> Am 05.02.2019 um 09:52 schrieb Manuel Eberl <eberlm at in.tum.de>:
> 
> Hello,
> 
> If I'm not mistaken, the default code setup for the "power" operation in
> HOL is linear in the exponent (it just does multiplication n times). I
> didn't find anything on faster exponentiation in the distribution or the
> AFP. so in 154cf64e403e, I committed some material about exponentiation
> by squaring that works in logarithmic time in the exponent for monoid_mult.
> 
> I wonder if this should be a code_unfold or code_abbrev rule for
> monoid_mult in general, or perhaps just for some instances like nat and int.
> 
> There's also setup in HOL-Number_Theory to do modular exponentiation "a
> ^ n mod m" and congruences of the form "[a ^ n = b] (mod m)" using this,
> at least for int and nat. I'm not sure if the rules I set up are the
> best ones and, again, this could be generalised to
> euclidean_semiring_cancel but I'm not sure if I should.
> 
> Does anyone have any stakes in/opinions on this?
> 
> Manuel
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev