Termination of Continued Fraction Computations (gcf.of) #

Summary #

We show that the continued fraction for a value v, as defined in algebra.continued_fractions.computation.basic, terminates if and only if v corresponds to a rational number, that is ↑v = q for some q : ℚ.

Main Theorems #

• generalized_continued_fraction.coe_of_rat shows that generalized_continued_fraction.of v = generalized_continued_fraction.of q for v : α given that ↑v = q and q : ℚ.
• generalized_continued_fraction.terminates_iff_rat shows that generalized_continued_fraction.of v terminates if and only if ↑v = q for some q : ℚ.

Tags #

rational, continued fraction, termination

Terminating Continued Fractions Are Rational #

We want to show that the computation of a continued fraction generalized_continued_fraction.of v terminates if and only if v ∈ ℚ. In this section, we show the implication from left to right.

We first show that every finite convergent corresponds to a rational number q and then use the finite correctness proof (of_correctness_of_terminates) of generalized_continued_fraction.of to show that v = ↑q.

Technical Translation Lemmas #

Before we can show that the continued fraction of a rational number terminates, we have to prove some technical translation lemmas. More precisely, in this section, we show that, given a rational number q : ℚ and value v : K with v = ↑q, the continued fraction of q and v coincide. In particular, we show that

    (↑(generalized_continued_fraction.of q : generalized_continued_fraction ℚ)
      : generalized_continued_fraction K)
  = generalized_continued_fraction.of v`

in generalized_continued_fraction.coe_of_rat.

To do this, we proceed bottom-up, showing the correspondence between the basic functions involved in the computation first and then lift the results step-by-step.

First, we show the correspondence for the very basic functions in generalized_continued_fraction.int_fract_pair.

Now we lift the coercion results to the continued fraction computation.

Continued Fractions of Rationals Terminate #

Finally, we show that the continued fraction of a rational number terminates.

The crucial insight is that, given any q : ℚ with 0 < q < 1, the numerator of int.fract q is smaller than the numerator of q. As the continued fraction computation recursively operates on the fractional part of a value v and 0 ≤ int.fract v < 1, we infer that the numerator of the fractional part in the computation decreases by at least one in each step. As 0 ≤ int.fract v, this process must stop after finite number of steps, and the computation hence terminates.