| Issue |
RAIRO-Theor. Inf. Appl.
Volume 57, 2023
|
|
|---|---|---|
| Article Number | 4 | |
| Number of page(s) | 22 | |
| DOI | https://doi.org/10.1051/ita/2022011 | |
| Published online | 31 March 2023 | |
Automatic sequences in negative bases and proofs of some conjectures of shevelev
School of Computer Science, University of Waterloo,
Waterloo, ON
N2L 3G1,
Canada
** Corresponding author: shallit@uwaterloo.ca
Received:
6
September
2022
Accepted:
22
December
2022
We discuss the use of negative bases in automatic sequences. Recently the theorem-prover Walnut has been extended to allow the use of base (—k) to express variables, thus permitting quantification over ℤ instead of ℕ. This enables us to prove results about two-sided (bi-infinite) automatic sequences. We first explain the theory behind negative bases in Walnut. Next, we use this new version of Walnut to give a very simple proof of a strengthened version of a theorem of Shevelev. We use our ideas to resolve two open problems of Shevelev from 2017. We also reprove a 2000 result of Shut involving bi-infinite binary words.
Mathematics Subject Classification: 68R15 / 11B85 / 11A63 / 68Q45 / 03D05
Key words: Automatic sequence / representation in negative base / Fibonacci representation / combinatorics on words / logic / decision procedure / Thue-Morse sequence
© The authors. Published by EDP Sciences, 2023
This is an Open Access article distributed under the terms of the Creative Commons Attribution License (https://creativecommons.org/licenses/by/4.0), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.