Euclidean Algorithm/Formal Implementation

From ProofWiki
Jump to navigation Jump to search


The Euclidean algorithm can be implemented as a computational method $\struct {Q, I, \Omega, f}$ as follows:

Let $Q$ be the set of:

all singletons $\tuple n$
all ordered pairs $\tuple {m, n}$
all ordered quadruples:
$\tuple {m, n, r, 1}$
$\tuple {m, n, r, 2}$
$\tuple {m, n, p, 3}$

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

Let $I \subseteq Q$ be the set of all ordered pairs $\tuple {m, n}$.

Let $\Omega$ be the set of all singletons $\tuple n$.

Let $f: Q \to Q$ be defined as follows:

\(\ds \map f {\tuple {m, n} }\) \(=\) \(\ds \tuple {m, n, 0, 1}\)
\(\ds \map f {\tuple n}\) \(=\) \(\ds \tuple n\)
\(\ds \map f {\tuple {m, n, r, 1} }\) \(=\) \(\ds \tuple {m, n, \map \rem {m, n}, 2}\)
\(\ds \map f {\tuple {m, n, r, 2} }\) \(=\) \(\ds \begin{cases} \tuple n & : r = 0 \\ \tuple {m, n, r, 3} & : r \ne 0 \end{cases}\)
\(\ds \map f {\tuple {m, n, p, 3} }\) \(=\) \(\ds \tuple {n, p, p, 1}\)

where $\map \rem {m, n}$ denotes the remainder of $m$ on division by $n$.