# 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