Sabine Bauer: List Constraints

Sabine Bauer
List Constraints

We consider satisfiability of constraints of a certain sytax over infinite lists labelled with nonnegative real numbers. These constraints were first introduced for general trees by Martin Hofmann and Dulma Rodriguez in the context of amortized analysis.

Our starting point is linear homogeneous recurrence relations with constant rational coefficients, which we show to correspond to list constraints in a one-to-one-relationship. Such recurrent sequences can be seen from the view of generating functions, and also in connection to the Skolem-Mahler-Lech Theorem.

First we show that each set of constraints can be rewritten as a set of recurrences, and that it has a rational generating function. Then we observe that the satisfiability of our constraints is at least as hard as the positivity problem for recurrence sequences, a well known and yet unsolved problem.