Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Equality of morphic sequences

Hans Zantema

TL;DR

This work addresses the problem of confirming that different morphic representations describe the same infinite sequence, focusing on equalities of the form $\tau(f^\infty(0)) = \rho(g^\infty(0))$. It introduces a constructive main theorem: if suitable words $u_i,v_i$ and decompositions $f(u_i), g(v_i)$ exist with $\tau(u_i) = \rho(v_i)$, then equality holds, proven by induction on the exponent. An automatic tool is developed to implement this theorem, including scaling of morphisms to align dominant eigenvalues and systematically building the $u_i,v_i,w_i$ to produce a formal proof. The approach is applied to subsequences of the Fibonacci word, notably the even and odd subsequences, yielding fully automatic proofs and revealing minimal representations in several cases. The work highlights both practical effectiveness and limitations, including open questions about the decidability of HD0L $\omega$-equivalence beyond primitive morphisms.

Abstract

Morphic sequences form a natural class of infinite sequences, typically defined as the coding of a fixed point of a morphism. Different morphisms and codings may yield the same morphic sequence. This paper investigates how to prove that two such representations of a morphic sequence by morphisms represent the same sequence. In particular, we focus on the smallest representations of the subsequences of the binary Fibonacci sequence obtained by only taking the even or odd elements. The proofs we give are induction proofs of several properties simultaneously, and are typically found fully automatically by a tool that we developed.

Equality of morphic sequences

TL;DR

This work addresses the problem of confirming that different morphic representations describe the same infinite sequence, focusing on equalities of the form . It introduces a constructive main theorem: if suitable words and decompositions exist with , then equality holds, proven by induction on the exponent. An automatic tool is developed to implement this theorem, including scaling of morphisms to align dominant eigenvalues and systematically building the to produce a formal proof. The approach is applied to subsequences of the Fibonacci word, notably the even and odd subsequences, yielding fully automatic proofs and revealing minimal representations in several cases. The work highlights both practical effectiveness and limitations, including open questions about the decidability of HD0L -equivalence beyond primitive morphisms.

Abstract

Morphic sequences form a natural class of infinite sequences, typically defined as the coding of a fixed point of a morphism. Different morphisms and codings may yield the same morphic sequence. This paper investigates how to prove that two such representations of a morphic sequence by morphisms represent the same sequence. In particular, we focus on the smallest representations of the subsequences of the binary Fibonacci sequence obtained by only taking the even or odd elements. The proofs we give are induction proofs of several properties simultaneously, and are typically found fully automatically by a tool that we developed.
Paper Structure (9 sections, 3 theorems, 58 equations)

This paper contains 9 sections, 3 theorems, 58 equations.

Table of Contents

  1. Introduction
  2. Morphic sequences
  3. Notations and preliminaries
  4. The main theorem
  5. Scaling up
  6. The tool
  7. Limitations
  8. Subsequences of ${\sf fib}$
  9. Concluding remarks

Key Result

Theorem 1

If $f,g$ are primitive and $\tau(f^\infty(0)) = \rho(g^\infty(0))$ is not periodic, then there exist $k,m$ such that $f^k$ and $g^m$ have the same dominant eigenvalue.

Theorems & Definitions (4)

  • Definition 1
  • Theorem 1
  • Theorem 2
  • Theorem 3