Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Positivity of Nearly Linearly Recurrent Sequences

Amaury Pouly, Mahsa Shirmohammadi, James Worrell

Abstract

Nearly linear recurrences are a generalisation of linear recurrences and are instances of linear time-invariant systems in control theory and linear constraint loops in program analysis. In this paper we formulate the Positivity Problem for such recurrences. This asks whether all sequences satisfying a given recurrence with given initial conditions are positive. This problem is a generalisation of the Positivity Problem for linear recurrence sequences, and is a special case of the non-reachability problem for linear time-invariant systems. Our main contribution is a decision procedure for the Positivity Problem for recurrences of order two. The termination proof of our procedure relies on a new transcendence result for infinite series that is of independent interest.

Positivity of Nearly Linearly Recurrent Sequences

Abstract

Nearly linear recurrences are a generalisation of linear recurrences and are instances of linear time-invariant systems in control theory and linear constraint loops in program analysis. In this paper we formulate the Positivity Problem for such recurrences. This asks whether all sequences satisfying a given recurrence with given initial conditions are positive. This problem is a generalisation of the Positivity Problem for linear recurrence sequences, and is a special case of the non-reachability problem for linear time-invariant systems. Our main contribution is a decision procedure for the Positivity Problem for recurrences of order two. The termination proof of our procedure relies on a new transcendence result for infinite series that is of independent interest.

Paper Structure

This paper contains 13 sections, 9 theorems, 18 equations.

Table of Contents

  1. Introduction
  2. Related Work
  3. Decidability of Positivity at Order Two
  4. Linear Recurrence Sequences
  5. Matrix-Power Formulation of NLRS
  6. Decision Procedure
  7. Approximation by Linear Recurrences
  8. Continued Fractions
  9. A Family of Recurrences
  10. Transcendence Result
  11. The Subspace Theorem
  12. Proof of Theorem \ref{['thm:main']}
  13. Conclusion

Key Result

Theorem 1

The Positivity Problem for NLRS is decidable for recurrences of order two.

Theorems & Definitions (9)

  • Theorem 1
  • Theorem 2
  • Proposition 3
  • Proposition 4
  • Proposition 5
  • Proposition 6
  • Theorem 7
  • Theorem 7
  • Proposition 8