Linear Recurrences

Manuel Eberl 🌐

October 12, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Linear_Recurrences

Session Linear_Recurrences_Solver