Euclid’s algorithm

Showing results in 'Publications'. Show all posts
Ferreira JF.  2010.  Designing an Algorithmic Proof of the Two-Squares Theorem. Mathematics of Program Construction (LNCS 6120). Abstract

We show a new and constructive proof of the two-squares theorem, based on a somewhat unusual, but very effective, way of rewriting the so-called extended Euclid’s algorithm. Rather than simply verifying the result—as it is usually done in the mathematical community—we use Euclid’s algorithm as an interface to investigate which numbers can be written as sums of two positive squares. The precise formulation of the problem as an algorithmic problem is the key, since it allows us to use algorithmic techniques and to avoid guessing. The notion of invariance, in particular, plays a central role in our development: it is used initially to observe that Euclid’s algorithm can actually be used to represent a given number as a sum of two positive squares, and then it is used throughout the argument to prove other relevant properties. We also show how the use of program inversion techniques can make mathematical arguments more precise.
Backhouse R, Ferreira JF.  2011.  On Euclid's Algorithm and Elementary Number Theory. Science of Computer Programming. 76(3):160-180. Abstract2011-oneuclidsalgorithm.pdf

Algorithms can be used to prove and to discover new theorems. This paper shows how algorithmic skills in general, and the notion of invariance in particular, can be used to derive many results from Euclid’s algorithm. We illustrate how to use the algorithm as a verification interface (i.e., how to verify theorems) and as a construction interface (i.e., how to investigate and derive new theorems). The theorems that we verify are well-known and most of them are included in standard number-theory books. The new results concern distributivity properties of the greatest common divisor and a new algorithm for efficiently enumerating the positive rationals in two different ways. One way is known and is due to Moshe Newman. The second is new and corresponds to a deforestation of the Stern-Brocot tree of rationals. We show that both enumerations stem from the same simple algorithm. In this way, we construct a Stern-Brocot enumeration algorithm with the same time and space complexity as Newman’s algorithm. A short review of the original papers by Stern and Brocot is also included.