# Verified Solving and Asymptotics of Linear Recurrences

by Manuel Eberl

In: *Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs* (2019)

### DOI:

10.1145/3293880.3294090### 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.

Download preprint PDF (652 KiB)

### BibTeX:

```
@inproceedings{eberl19cpp,
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}
}
```

(The final publication is available at ACM)