gcd is:module
This module defines the
GCDMonoid subclass of the
Monoid
class.
The
GCDMonoid subclass adds the
gcd operation which
takes two monoidal arguments and finds their greatest common divisor,
or (more generally) the greatest monoid that can be extracted with the
</> operation from both.
The
GCDMonoid class is for Abelian,
i.e.,
Commutative monoids.
Non-commutative GCD monoids
Since most practical monoids in Haskell are not Abelian, the
GCDMonoid class has three symmetric superclasses:
- LeftGCDMonoidClass of monoids for which it is possible to
find the greatest common prefix of two monoidal values.
- RightGCDMonoidClass of monoids for which it is possible to
find the greatest common suffix of two monoidal values.
- OverlappingGCDMonoidClass of monoids for which it is
possible to find the greatest common overlap of two monoidal
values.
Distributive GCD monoids
Since some (but not all) GCD monoids are also distributive, there are
three subclasses that add distributivity:
Computing GCD symbolically, and generating C code for it. This example
illustrates symbolic termination related issues when programming with
SBV, when the termination of a recursive algorithm crucially depends
on the value of a symbolic variable. The technique we use is to
statically enforce termination by using a recursion depth counter.
Proof of correctness of an imperative GCD (greatest-common divisor)
algorithm, using weakest preconditions. The termination measure here
illustrates the use of lexicographic ordering. Also, since symbolic
version of GCD is not symbolically terminating, this is another
example of using uninterpreted functions and axioms as one writes
specifications for WP proofs.