Linear Recurrences

 

Title: Linear Recurrences
Author: Manuel Eberl
Submission date: 2017-10-12
Abstract:

Linear recurrences with constant coefficients are an interesting class of recurrence equations that can be solved explicitly. The most famous example are certainly the Fibonacci numbers with the equation f(n) = f(n-1) + f(n - 2) and the quite non-obvious closed form (φn - (-φ)-n) / √5 where φ is the golden ratio.

In this work, I build on existing tools in Isabelle – such as formal power series and polynomial factorisation algorithms – to develop a theory of these recurrences and derive a fully executable solver for them that can be exported to programming languages like Haskell.

BibTeX:
@article{Linear_Recurrences-AFP,
  author  = {Manuel Eberl},
  title   = {Linear Recurrences},
  journal = {Archive of Formal Proofs},
  month   = oct,
  year    = 2017,
  note    = {\url{https://isa-afp.org/entries/Linear_Recurrences.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Count_Complex_Roots, Polynomial_Factorization