Euclidean Algorithm/Formal Implementation

From ProofWiki
Jump to navigation Jump to search


The Euclidean Algorithm can be implemented as a computational method $\left({Q, I, \Omega, f}\right)$ as follows:

Let $Q$ be the set of:

all singletons $\left({n}\right)$
all ordered pairs $\left({m, n}\right)$
all ordered quadruples:
$\left({m, n, r, 1}\right)$
$\left({m, n, r, 2}\right)$
$\left({m, n, p, 3}\right)$

where $m, n, p \in \Z_{> 0}$ and $r \in \Z_{\ge 0}$.

Let $I \subseteq Q$ be the set of all ordered pairs $\left({m, n}\right)$.

Let $\Omega$ be the set of all singletons $\left({n}\right)$.

Let $f$ be defined as follows:

$f \left({\left({m, n}\right)}\right) = \left({m, n, 0, 1}\right)$
$f \left({\left({n}\right)}\right) = \left({n}\right)$
$f \left({\left({m, n, r, 1}\right)}\right) = \left({m, n, \operatorname{rem} \left({m / n}\right), 2}\right)$
$f \left({\left({m, n, r, 2}\right)}\right) = \begin{cases}\left({n}\right) & : r = 0 \\ \left({m, n, r, 3}\right) & : r \ne 0 \end{cases}$
$f \left({\left({m, n, p, 3}\right)}\right) = \left({n, p, p, 1}\right)$

where $\operatorname{rem} \left({m / n}\right)$ denotes the remainder of $m$ on division by $n$.