不保持原始性的二进制编码
摘要：码X不是原语性保持的，如果存在一个原语列表mathbf w在集合X中，它们的串联是非原语的。我们在证明助手Isabelle/HOL中形式化了这样的码在二进制情况下的全面特征化。其中一部分形式化对于它自己来说是有趣的，它描述了如果|y| ≤ |x|，方块xx的xy解释。我们还提供了有关方程x^jy^k = z^ell的形式化参数解决方案。
作者：v{S}tv{e}p''an Holub and Martin Rav{s}ka and v{S}tv{e}p''an Starosta
论文ID：2203.11341
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2022-03-23