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:

• DistributiveGCDMonoidSubclass of GCDMonoid with symmetric distributivity.
• LeftDistributiveGCDMonoidSubclass of LeftGCDMonoid with left-distributivity.
• RightDistributiveGCDMonoidSubclass of RightGCDMonoid with right-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.