Algorithmic problems for linear recurrence sequences

Abstract

Linear recurrence sequences (LRS) are among the most fundamental and easily definable classes of number sequences, encompassing many classical sequences such as polynomials, powers of two, and the Fibonacci numbers. They also describe the dynamics of iterated linear maps and arise naturally in numerous contexts within computer science, mathematics, and other quantitive sciences. However, despite their simplicity, many easy-to-state decision problems for LRS have stubbornly remained open for decades despite considerable and sustained attention. Chief among these are the Skolem problem and the Positivity problem, which ask to determine, for a given LRS, whether it contains a zero term and whether it contains only positive terms, respectively. For both problems, decidability is currently open, i.e., whether they are algorithmically solvable. In this thesis, we present the following results. For the Skolem problem, we introduce an algorithm for simple LRS whose correctness is unconditional but whose termination relies on two classical, widely-believed number-theoretic conjectures. This algorithm is implementable in practice, and we report on experimental results. For the Positivity problem, we introduce the notion of reversible LRS, which enables us to carve out a large decidable class of sequences. We also examine various expansions of classical logics by predicates obtained from LRS. In particular, we study expansions of monadic second-order logic of the natural numbers with order and present major advances over the seminal results of Büchi, Elgot, and Rabin from the early 1960s. Finally, we investigate fragments of Presburger arithmetic, where, among others, we establish the decidability of the existential fragment of Presburger arithmetic expanded with powers of 2 and 3.

Lineare rekursive Folge (LRF) gehören zu den grundlegendsten und am einfachsten zu definierenden Klassen von Zahlenfolgen und umfassen viele klassische Folgen wie Polynome, Zweierpotenzen und die Fibonacci-Zahlen. Sie beschreiben auch die Dynamik iterierter linearer Abbildungen und tauchen in zahlreichen Kontexten der Informatik, Mathematik und anderer quantitativer Wissenschaften auf. Trotz ihrer Einfachheit bleiben jedoch viele leicht zu formulierendes Entscheidungsprobleme für LRF trotz erheblicher und anhaltender Aufmerksamkeit seit Jahrzehnten hartnäckig o en. Dazu gehören vor allem das Skolem-Problem und das Positivitätsproblem, bei denen es darum geht, für eine gegebene LRF zu bestimmen, ob sie einen Nullterm enthält bzw. ob eine LRF nur positive Terme enthält. Für beide Probleme ist die Entscheidbarkeit derzeit o en, d.h., ob sie algorithmisch lösbar sind. In dieser Doktorarbeit präsentieren wir die folgenden Ergebnisse. Für das Skolem- Problem stellen wir einen Algorithmus für einfache LRF vor, dessen Korrektheit nicht an Bedingungen geknüpft ist, dessen Terminerung aber von zwei weithin akzeptierten zahlentheoretischen Vermutungen abhängt. Dieser Algorithmus ist in der Praxis implementierbar, und wir berichten über experimentelle Ergebnisse. Für das Positivitätsproblem führen wir den Begri der umkehrbaren LRF ein, der es uns ermöglicht, eine groÿe, entscheidbare Klasse von Sequenzen zu bestimmen. Wir untersuchen auch verschiedene Erweiterungen klassischer Logiken durch Prädikate, die aus LRF gewonnen werden. Insbesondere untersuchen wir Erweiterungen von monadische Prädikatenlogik zweiter Stufe der natürlichen Zahlen mit Ordnung und präsentieren wichtige Fortschritte gegenüber den bahnbrechenden Ergebnissen von Büchi, Elgot und Rabin aus den frühen 1960er Jahren. Schließlich untersuchen wir Fragmente der Presburger Arithmetik, wo wir unter anderem die Entscheidbarkeit des existentiellen Fragments der Presburger Arithmetik, erweitert mit Potenzen von 2 und 3, beweisen.