Verified Solving and Asymptotics of Linear Recurrences
by Manuel Eberl
In: Proceedings of CPP 2019
DOI:
10.1145/3293880.3294090Abstract:
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)
BibTeX:
@inproceedings{eberl19cpp,
author = "Eberl, Manuel",
title = "Verified Solving and Asymptotics of Linear Recurrences",
booktitle = "Certified Programs and Proofs, {CPP} 2019",
year = "2019",
isbn = "978-1-4503-6222-1",
pages = "27--37",
numpages = "11",
doi = "10.1145/3293880.3294090",
publisher = "ACM"
}
(The final publication is available at ACM)