Re: [isabelle] Code equations for "power"

Dear Manuel,

I just noticed that the "power" function is exported as

power :: forall a. (Power a) => a -> Nat -> a;
power a n =
   (if equal_nat n zero_nat then one
     else times a (power a (minus_nat n one_nat)));

This looks pretty inefficient to me; something like iterated squaring should be much
faster, and it's pretty easy to do. However, this only works in the type class
mult_monoid; power, on the other hand, is defined in the type class "power". (the
difference is essentially that the latter does not demand associativity, if I am not
mult_monoid assumes associativity of and neutrality of 1 for times. power does not impose any constraints; it is a superclass of mult_monoid.

Is it still possible to use the more efficient iterative squaring when applicable? I
attached something using code_unfold, but I'm not sure if that really does what one would
want it to do.
The code_unfold works if the call to power in the code equations is types with something of sort mult_monoid. So if the code equation uses power on one of the standard numeric types, everything is fine. But if you use power polymorphically for some 'a, then this does not work if mult_monoid is not a supersort of 'a's sort. For example, if you have something like

  definition map_power :: "'a :: power list => 'a list"
  where "map_power = map power"

then if you use map_power, you will end up with the original slow implementation.

Moreover, for rational numbers, one could optimise this even futher: multiplication on
rational numbers reduces the numerator and denominator after the multiplication. In the
case of "power", this is unnecessary, since the numerator and denominator of the result
will always be coprime if they were coprime before. Perhaps this would be a worthwhile
Custom implementations for power are not possible with the current setup. You can have type-dependent implementations for a function only if that function is a type class parameter (unless you play some sophisticated tricks like in the Containers AFP entry). From what I can see, it does not seem reasonable to make power a type class parameter, because then power cannot be a superclass of mult_monoid any more (you'd have to add power as a type class parameter to the whole algebraic type class hierarchy). But you could achieve something similar like this:

class power_impl = power +
  fixes power_impl :: "'a => nat => 'a"
  assumes power_impl: "power = power_impl"

declare power_impl [code]

Then, of course, you have to instantiate the new class power_impl for all types that instantiate power and all users have to do the same for their own types. Unfortunately, we do not (yet) have a mechanism to instantiate such definitional type classes automatically. With this approach, you could declare custom code equations for instances like rat.

Lastly, I was wondering whether there was something like "divmod" in Isabelle, i.e. an
operation that returns both the quotient and the remainder, since most languages have a
corresponding operation that is more efficient than computing the two separately.
There are various specialised divmod constants in HOL, e.g., divmod_integer, semiring_numeral_div_class.divmod and Divides.divmod_nat, but no systematic, algebraic treatment.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.