gcd -package:monoid-subclasses

gcd x y is the non-negative factor of both x and y of which every common factor of x and y is also a factor; for example gcd 4 2 = 2, gcd (-4) 6 = 2, gcd 0 4 = 4. gcd 0 0 = 0. (That is, the common divisor that is "greatest" in the divisibility preordering.) Note: Since for signed fixed-width integer types, abs minBound < 0, the result may be negative if one of the arguments is minBound (and necessarily is if the other is 0 or minBound) for such types.

The Greatest Common Divisor is defined by:

gcd x y == gcd y x
divides z x && divides z y ==> divides z (gcd x y)   (specification)
divides (gcd x y) x

Greatest common divisor. Must satisfy

\x y -> isJust (x `divide` gcd x y) && isJust (y `divide` gcd x y)

\x y z -> isJust (gcd (x * z) (y * z) `divide` z)

Greatest common divisor. Must satisfy

\x y -> isJust (x `divide` gcd x y) && isJust (y `divide` gcd x y)

\x y z -> isJust (gcd (x * z) (y * z) `divide` z)

gcd x y is the non-negative factor of both x and y of which every common factor of x and y is also a factor; for example gcd 4 2 = 2, gcd (-4) 6 = 2, gcd 0 4 = 4. gcd 0 0 = 0. (That is, the common divisor that is "greatest" in the divisibility preordering.) Note: Since for signed fixed-width integer types, abs minBound < 0, the result may be negative if one of the arguments is minBound (and necessarily is if the other is 0 or minBound) for such types.

>>> gcd 72 60
12

Symbolic GCD as our specification. Note that we cannot really implement the GCD function since it is not symbolically terminating. So, we instead uninterpret and axiomatize it below. NB. The concrete part of the definition is only used in calls to traceExecution and is not needed for the proof. If you don't need to call traceExecution, you can simply ignore that part and directly uninterpret. In that case, we simply use Prelude's version.

It is only a monoid for non-negative numbers.

idt <*> GCD (-2) = GCD 2

Thus, use this Monoid only for non-negative numbers!

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.

Type-level greatest common denominator (GCD). Note that additional equations are provided by the type-checker plugin solver GHC.TypeLits.Extra.Solver.

Greatest common divisor for type-level naturals. Example:

>>> :kind! Gcd 9 11
Gcd 9 11 :: Natural
= 1

>>> :kind! Gcd 9 12
Gcd 9 12 :: Natural
= 3

The greatest common divisor of two type-level integers

Compute greatest common divisor.

Number of bytes allocated since the previous GC

The amount of memory lost due to block fragmentation in bytes. Block fragmentation is the difference between the amount of blocks retained by the RTS and the blocks that are in use. This occurs when megablocks are only sparsely used, eg, when data that cannot be moved retains a megablock.

Total amount of live data in compact regions

Total amount of data copied during this GC