当一个问题似乎无法克服时，解决方案通常是公开宣布您认为该问题有多难。然后，您会立即意识到问题是微不足道的，而您只是让自己看起来像个白痴-这基本上就是我现在的位置；-)
正如问题中所建议的，要对两个自动机进行词汇排序，我需要考虑两件事。两组可能的第一个标记，以及两组可能的所有其他尾部。尾部可以表示为有限自动机，并且可以从原始自动机推导出来。
所以比较算法是递归的 - 比较头部，如果不同你有你的结果，如果相同然后递归比较尾部。
问题是证明一般规则文法等价所需的无限序列。如果在比较过程中出现一对自动机，相当于您之前检查过的一对，则您已证明等价，您可以停止检查。这是有限自动机的本质，这必须在有限数量的步骤中发生。
问题是我仍然有相同形式的问题。为了找出我的终止标准，我需要将我的当前自动机对与迄今为止在比较期间发生的所有过去自动机对进行比较。这就是一直让我头疼的事情。
事实证明，那篇论文是相关的，但可能只带我到这一步。常规语言可以使用连接运算符形成一个组，而左陪集与我一直在考虑的 head:tail 事物有关。
我是白痴的原因是因为我一直在强加一个过于严格的终止条件，我应该知道这一点，因为 WRT 自动机算法的问题并不罕见。
我不需要在自动机对的第一次重复出现时停下来。我可以继续，直到我找到一个更容易检测到的重现——一个具有某种结构等价和逻辑等价的复现。只要我的衍生尾自动机算法是健全的（特别是如果我在每个步骤中最小化并进行其他清理），我就不会在比较过程中生成无限序列的等效但看起来不同的自动机对。结构变化的唯一来源是原始的两个自动机和尾自动机算法，它们都是有限的。
关键是，如果我比较了太多的词汇，这并不重要——我仍然会得到正确的结果，虽然我稍后会终止，但我仍然会在有限的时间内终止。
这应该意味着我可以使用对自动机结构敏感的散列或有序比较来使用不可靠的递归检测（允许一些假阴性）。这是一个比结构不敏感比较更简单的问题，我认为这是我需要的关键。
当然还有性能问题。基于此处涉及的问题，使用标准等价算法的线性搜索可能是一种更快的方法。当然，我希望这种比较是比现有算法效率更低的等价测试，因为它正在做更多的工作 - 非等价案例的词汇排序。真正的问题是基于关键字的搜索的整体效率，这可能需要一些令人头疼的分析。我希望非等效自动机倾向于快速比较（检测前几个步骤中的差异，如传统的字符串比较）这一事实将使这成为一种实用的方法。
此外，如果我达到怀疑等价的程度，我可以使用标准等价算法进行检查。如果该检查失败，我只需继续比较我离开的顺序，而无需检查重复出现的尾部语言 - 我知道我会在有限数量的步骤中找到差异。