Module Arith.Euclid


module Euclid: sig  end


type t = R.q
val (-) : R.q -> R.q -> R.q
Parameters:
a : R.q
b : 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).

Parameters:
a0 : R.q
b0 : R.q
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.
Parameters:
cl : R.q list
b : R.q