Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2022
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2203.11341 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911197850238976 |
|---|---|
| author | Holub, Štěpán Raška, Martin Starosta, Štěpán |
| author_facet | Holub, Štěpán Raška, Martin Starosta, Štěpán |
| contents | A code $X$ is not primitivity preserving if there is a primitive list ${\mathbf w} \in {\tt lists} X$ whose concatenation is imprimitive. We formalize a full characterization of such codes in the binary case in the proof assistant Isabelle/HOL. Part of the formalization, interesting on its own, is a description of $\{x,y\}$-interpretations of the square $xx$ if $|y| \leq |x|$. We also provide a formalized parametric solution of the related equation $x^jy^k = z^\ell$. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2203_11341 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Binary codes that do not preserve primitivity Holub, Štěpán Raška, Martin Starosta, Štěpán Formal Languages and Automata Theory A code $X$ is not primitivity preserving if there is a primitive list ${\mathbf w} \in {\tt lists} X$ whose concatenation is imprimitive. We formalize a full characterization of such codes in the binary case in the proof assistant Isabelle/HOL. Part of the formalization, interesting on its own, is a description of $\{x,y\}$-interpretations of the square $xx$ if $|y| \leq |x|$. We also provide a formalized parametric solution of the related equation $x^jy^k = z^\ell$. |
| title | Binary codes that do not preserve primitivity |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2203.11341 |