自动序列与 Zip 规范
计算机科学中的逻辑
2012-04-17 v2
摘要
我们考虑无限符号序列（也称为流），以及以受限格式定义的流之间相等性的可判定性问题。该受限格式包括在流头部前缀一个符号、流函数 `zip' 以及递归变量。此处 `zip' 以交替顺序交错两个流的元素，从第一个流开始。例如，Thue-Morse 序列可通过 `zip-规范' {M = 0 : X, X = 1 : zip(X,Y), Y = 0 : zip(Y,X)} 获得。我们对此类系统的分析采用了项重写和余代数技术。我们基于适当选择的余基，利用观察图的互模拟性，确立了这些 zip-规范的可判定性。zip-规范的重要性在于其与自动序列的紧密联系。我们建立了自动序列的一种新的简单刻画。因此，对于二元 zip，我们得出：当且仅当使用余基 (hd,even,odd) 的观察图有限时，流是 2-自动的。推广到 zip-k 规范及其与 k-自动性的关系是直接的。事实上，zip-规范可被视为自动序列的项重写语法。我们将 zip-规范的研究置于更广阔的视角中，通过在动态逻辑设置中运用观察图，从而得出自动序列的另一种刻画。我们还获得了自动序列类的一个自然扩展，即通过使用不同元数的 zip 的 `zip-mix' 规范获得。我们也表明，对于带有如 even 和 odd 等投影的 zip-mix 格式的简单扩展，其等价性是不可判定的。然而，zip-mix 规范是否具有可判定的等价性问题仍然开放。
引用
@article{arxiv.1201.3251,
title = {Automatic Sequences and Zip-Specifications},
author = {Clemens Grabmayer and Joerg Endrullis and Dimitri Hendriks and Jan Willem Klop and Lawrence S. Moss},
journal= {arXiv preprint arXiv:1201.3251},
year = {2012}
}