We define generalised, simple, and regular continued fractions and functions to evaluate their convergents. We follow the naming conventions from Wikipedia and [wall2018analytic], Chapter 1.
numerics, number theory, approximations, fractions
We collect a partial numerator aᵢ and partial denominator bᵢ in a pair ⟨aᵢ,bᵢ⟩.
Make a gcf.pair printable.
Coerce a pair by elementwise coercion.
A generalised continued fraction (gcf) is a potentially infinite expression of the form
a₀
h + --------------------------
a₁
b₀ + --------------------
a₂
b₁ + --------------
a₃
b₂ + --------
b₃ + ...
where h is called the head term or integer part, the aᵢ are called the partial numerators and the bᵢ the partial denominators of the gcf. We store the sequence of partial numerators and denominators in a sequence of generalized_continued_fraction.pairs s. For convenience, one often writes [h; (a₀, b₀), (a₁, b₁), (a₂, b₂),...].
Returns the sequence of partial numerators aᵢ of g.
Returns the sequence of partial denominators bᵢ of g.
A gcf terminated at position n if its sequence terminates at position n.
It is decidable whether a gcf terminated at a given position.
A gcf terminates if its sequence terminates.
Coerce a sequence by elementwise coercion.
Coerce a gcf by elementwise coercion.
A generalized continued fraction is a simple continued fraction if all partial numerators are equal to one.
1
h + --------------------------
1
b₀ + --------------------
1
b₁ + --------------
1
b₂ + --------
b₃ + ...A simple continued fraction (scf) is a generalized continued fraction (gcf) whose partial numerators are equal to one.
1
h + --------------------------
1
b₀ + --------------------
1
b₁ + --------------
1
b₂ + --------
b₃ + ...
For convenience, one often writes [h; b₀, b₁, b₂,...]. It is encoded as the subtype of gcfs that satisfy generalized_continued_fraction.is_simple_continued_fraction.
Lift a scf to a gcf using the inclusion map.
A simple continued fraction is a (regular) continued fraction ((r)cf) if all partial denominators bᵢ are positive, i.e. 0 < bᵢ.
A (regular) continued fraction ((r)cf) is a simple continued fraction (scf) whose partial denominators are all positive. It is the subtype of scfs that satisfy simple_continued_fraction.is_regular_continued_fraction.
Lift a cf to a scf using the inclusion map.
Lift a cf to a scf using the inclusion map.
Returns the next numerator Aₙ = bₙ-₁ * Aₙ₋₁ + aₙ-₁ * Aₙ₋₂, where predA is Aₙ₋₁, ppredA is Aₙ₋₂, a is aₙ₋₁, and b is bₙ₋₁.
Returns the next denominator Bₙ = bₙ-₁ * Bₙ₋₁ + aₙ-₁ * Bₙ₋₂``, where predBisBₙ₋₁andppredBisBₙ₋₂, aisaₙ₋₁, and bisbₙ₋₁`.
Returns the next continuants ⟨Aₙ, Bₙ⟩ using next_numerator and next_denominator, where pred is ⟨Aₙ₋₁, Bₙ₋₁⟩, ppred is ⟨Aₙ₋₂, Bₙ₋₂⟩, a is aₙ₋₁, and b is bₙ₋₁.
Returns the continuants ⟨Aₙ₋₁, Bₙ₋₁⟩ of g.
Returns the continuants ⟨Aₙ, Bₙ⟩ of g.
Returns the numerators Aₙ of g.
Returns the denominators Bₙ of g.
Returns the convergents Aₙ / Bₙ of g, where Aₙ, Bₙ are the nth continuants of g.
Returns the approximation of the fraction described by the given sequence up to a given position n. For example, convergents'_aux [(1, 2), (3, 4), (5, 6)] 2 = 1 / (2 + 3 / 4) and convergents'_aux [(1, 2), (3, 4), (5, 6)] 0 = 0.
Returns the convergents of g by evaluating the fraction described by g up to a given position n. For example, convergents' [9; (1, 2), (3, 4), (5, 6)] 2 = 9 + 1 / (2 + 3 / 4) and convergents' [9; (1, 2), (3, 4), (5, 6)] 0 = 9
Two gcfs g and g' are equal if and only if their components are equal.