Verified Solving and Asymptotics of Linear Recurrences

by Manuel Eberl

In: Proceedings of CPP 2019




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.

Download preprint PDF (652 KiB)


 author = {Eberl, Manuel},
 title = {Verified Solving and Asymptotics of Linear Recurrences},
 booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs},
 series = {CPP 2019},
 year = {2019},
 isbn = {978-1-4503-6222-1},
 location = {Cascais, Portugal},
 pages = {27--37},
 numpages = {11},
 doi = {10.1145/3293880.3294090},
 acmid = {3294090},
 publisher = {ACM},
 address = {New York, NY, USA}

Download BibTeX (479 Bytes)

(The final publication is available at ACM)