  Recurrence equations have played a central role in static cost analysis,
where they can be viewed as abstractions of programs and used to infer resource
usage information without actually running the programs with concrete data.
Such information is typically represented as functions of input data sizes.
More generally, recurrence equations have been increasingly used to
automatically obtain non-linear numerical invariants. However, state-of-the-art
recurrence solvers and cost analysers suffer from serious limitations when
dealing with the (complex) features of recurrences arising from cost analyses.
We address this challenge by developing a novel order-theoretical framework
where recurrences are viewed as operators and their solutions as fixpoints,
which allows leveraging powerful pre/postfixpoint search techniques. We prove
useful properties and provide principles and insights that enable us to develop
techniques and combine them to design new solvers. We have also implemented and
experimentally evaluated an optimisation-based instantiation of the proposed
approach. The results are quite promising: our prototype outperforms
state-of-the-art cost analysers and recurrence solvers, and can infer tight
non-linear lower/upper bounds, in a reasonable time, for complex recurrences
representing diverse program behaviours.
