# Computable Continued Fractions #

## Summary #

We formalise the standard computation of (regular) continued fractions for linear ordered floor fields. The algorithm is rather simple. Here is an outline of the procedure adapted from Wikipedia:

Take a value `v`

. We call `⌊v⌋`

the *integer part* of `v`

and `v - ⌊v⌋`

the *fractional part* of
`v`

. A continued fraction representation of `v`

can then be given by `[⌊v⌋; b₀, b₁, b₂,...]`

, where
`[b₀; b₁, b₂,...]`

recursively is the continued fraction representation of `1 / (v - ⌊v⌋)`

. This
process stops when the fractional part hits 0.

In other words: to calculate a continued fraction representation of a number `v`

, write down the
integer part (i.e. the floor) of `v`

. Subtract this integer part from `v`

. If the difference is 0,
stop; otherwise find the reciprocal of the difference and repeat. The procedure will terminate if
and only if `v`

is rational.

For an example, refer to `IntFractPair.stream`

.

## Main definitions #

`GeneralizedContinuedFraction.IntFractPair.stream`

: computes the stream of integer and fractional parts of a given value as described in the summary.`GeneralizedContinuedFraction.of`

: computes the generalised continued fraction of a value`v`

. In fact, it computes a regular continued fraction that terminates if and only if`v`

is rational.

## Implementation Notes #

There is an intermediate definition `GeneralizedContinuedFraction.IntFractPair.seq1`

between
`GeneralizedContinuedFraction.IntFractPair.stream`

and `GeneralizedContinuedFraction.of`

to wire up things. User should not (need to) directly interact with it.

The computation of the integer and fractional pairs of a value can elegantly be
captured by a recursive computation of a stream of option pairs. This is done in
`IntFractPair.stream`

. However, the type then does not guarantee the first pair to always be
`some`

value, as expected by a continued fraction.

To separate concerns, we first compute a single head term that always exists in
`GeneralizedContinuedFraction.IntFractPair.seq1`

followed by the remaining stream of option
pairs. This sequence with a head term (`seq1`

) is then transformed to a generalized continued
fraction in `GeneralizedContinuedFraction.of`

by extracting the wanted integer parts of the
head term and the stream.

## References #

- https://en.wikipedia.org/wiki/Continued_fraction

## Tags #

numerics, number theory, approximations, fractions

Interlude: define some expected coercions and instances.

Make an `IntFractPair`

printable.

## Equations

- One or more equations did not get rendered due to their size.

## Equations

- GeneralizedContinuedFraction.IntFractPair.inhabited = { default := { b := 0, fr := default } }

Maps a function `f`

on the fractional components of a given pair.

## Equations

- GeneralizedContinuedFraction.IntFractPair.mapFr f gp = { b := gp.b, fr := f gp.fr }

## Instances For

Interlude: define some expected coercions.

The coercion between integer-fraction pairs happens componentwise.

## Equations

- GeneralizedContinuedFraction.IntFractPair.coeFn = GeneralizedContinuedFraction.IntFractPair.mapFr Coe.coe

## Instances For

Coerce a pair by coercing the fractional component.

## Equations

- GeneralizedContinuedFraction.IntFractPair.coe = { coe := GeneralizedContinuedFraction.IntFractPair.coeFn }

Creates the integer and fractional part of a value `v`

, i.e. `⟨⌊v⌋, v - ⌊v⌋⟩`

.

## Equations

- GeneralizedContinuedFraction.IntFractPair.of v = { b := ⌊v⌋, fr := Int.fract v }

## Instances For

Creates the stream of integer and fractional parts of a value `v`

needed to obtain the continued
fraction representation of `v`

in `GeneralizedContinuedFraction.of`

. More precisely, given a value
`v : K`

, it recursively computes a stream of option `ℤ × K`

pairs as follows:

`stream v 0 = some ⟨⌊v⌋, v - ⌊v⌋⟩`

`stream v (n + 1) = some ⟨⌊frₙ⁻¹⌋, frₙ⁻¹ - ⌊frₙ⁻¹⌋⟩`

, if`stream v n = some ⟨_, frₙ⟩`

and`frₙ ≠ 0`

`stream v (n + 1) = none`

, otherwise

For example, let `(v : ℚ) := 3.4`

. The process goes as follows:

`stream v 0 = some ⟨⌊v⌋, v - ⌊v⌋⟩ = some ⟨3, 0.4⟩`

`stream v 1 = some ⟨⌊0.4⁻¹⌋, 0.4⁻¹ - ⌊0.4⁻¹⌋⟩ = some ⟨⌊2.5⌋, 2.5 - ⌊2.5⌋⟩ = some ⟨2, 0.5⟩`

`stream v 2 = some ⟨⌊0.5⁻¹⌋, 0.5⁻¹ - ⌊0.5⁻¹⌋⟩ = some ⟨⌊2⌋, 2 - ⌊2⌋⟩ = some ⟨2, 0⟩`

`stream v n = none`

, for`n ≥ 3`

## Equations

- One or more equations did not get rendered due to their size.
- GeneralizedContinuedFraction.IntFractPair.stream v 0 = some (GeneralizedContinuedFraction.IntFractPair.of v)

## Instances For

Shows that `IntFractPair.stream`

has the sequence property, that is once we return `none`

at
position `n`

, we also return `none`

at `n + 1`

.

Uses `IntFractPair.stream`

to create a sequence with head (i.e. `seq1`

) of integer and fractional
parts of a value `v`

. The first value of `IntFractPair.stream`

is never `none`

, so we can safely
extract it and put the tail of the stream in the sequence part.

This is just an intermediate representation and users should not (need to) directly interact with
it. The setup of rewriting/simplification lemmas that make the definitions easy to use is done in
`Algebra.ContinuedFractions.Computation.Translations`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Returns the `GeneralizedContinuedFraction`

of a value. In fact, the returned gcf is also
a `ContinuedFraction`

that terminates if and only if `v`

is rational (those proofs will be
added in a future commit).

The continued fraction representation of `v`

is given by `[⌊v⌋; b₀, b₁, b₂,...]`

, where
`[b₀; b₁, b₂,...]`

recursively is the continued fraction representation of `1 / (v - ⌊v⌋)`

. This
process stops when the fractional part `v - ⌊v⌋`

hits 0 at some step.

The implementation uses `IntFractPair.stream`

to obtain the partial denominators of the continued
fraction. Refer to said function for more details about the computation process.

## Equations

- One or more equations did not get rendered due to their size.