Proving properties of some greedily-defined integer recurrences via automata theory

TL;DR

This paper introduces a finite automata-based method to prove properties of certain greedy-defined integer sequences, simplifying lengthy case-based proofs and enabling new insights into their structure and connections.

Contribution

It presents a novel automata-theoretic approach to analyze and prove properties of integer recurrences, replacing complex case analysis with a decision procedure in Walnut.

Findings

Automata-based proofs match previous results

Discovered new connections between sequences and Hofstadter's functions

Proved a conjecture of Quet using automata methods

Abstract

Venkatachala on the one hand, and Avdispahi\'c & Zejnulahi on the other, both studiied integer sequences with an unusual sum property defined in a greedy way, and proved many results about them. However, their proofs were rather lengthy and required numerous cases. In this paper, I provide a different approach, via finite automata, that can prove the same results (and more) in a simple, unified way. Instead of case analysis, we use a decision procedure implemented in the free software Walnut. Using these ideas, we can prove a conjecture of Quet and find connections between Quet's sequence and the "married" functions of Hofstadter.