module Euclid: sig end
type t = R.q
val (-) : R.q -> R.q -> R.q
val euclid : R.q -> R.q -> R.q * R.q * R.q
Given two rational numbers
a,
b,
euclid finds
integers ,
y0 satisfying
a * x0 + b * y0 = (a, b),
where
(a, b) denotes the greatest common divisor of
a,
b.
For example,
euclid 1547 560 equals
(7, 21, -58)
The value of (a, b) is unchanged in the loop in euclid, since
(a, b) = (a - (a/b)*b, b); thus, using (a, 0) = a,
the first result of euclid computes (a0, b0). Other
invariants are:
c * a0 + e * b0 = a
d * a0 + f * b0 = b
Now it is obvious that a * x0 + b * y0 = (a, b).
val solve : R.q list -> R.q -> (R.q * R.q list) option
Solving a linear diophantine equation with nonzero, rational coefficients
ci, for i = 1,...,n with n >= 1:
c0*x_0 + \ldots c_n * xn = b
The algorithm proceeds by recursion on n. The case n = 1 is
trivial. Let n >= 2. Find, with the Euclidean algorithm
c' and integers d, e satisfying
a' = (c0, c1) = c0 * d + c1 * e
Next solve the linear diophantine equation (in n variables)
c'*x + c2 * x2 + ... + cn * xn = b
If equation has no integral solution,
then neither has.
Otherwise, if x,x2,...,xn is an integral solution
of, then d*x, e*x,x2,...,xn gives an integral solution of.