n-增长与n-浅TRS的可达性、规范化判定的不可判定逼近

本文主要探讨了在n-增长和n-浅术语重写系统（TRS）中的可达性、规范化和需要性问题。n-增长TRS是指重写规则的左侧和右侧同时包含的变量在规则的左侧深度为n，而在右侧深度必须大于n。相反，n-浅TRS的规则要求两侧同时出现的变量都在各自侧的深度为n。这些概念是对Jacquemard和Comon提出的生长TRS和浅TRS的扩展。 在一般的TRS中，可达性（判断一个术语是否可以通过一系列重写步骤达到另一个术语）、规范化（判断一个术语是否存在标准形式）以及需要性（确定一个redex是否是必要的）是不可判定的问题，这在理论计算机科学领域广为人知。然而，对于特定的TRS类别，如限制规则形式的系统，这些属性可以变得可判定。例如，如果R和S是具有相同签名的TRS，S被定义为R的近似，当它们满足→R→R并且重写关系集合相等时，可达性和规范化就变得容易处理。 尽管如此，本文揭示了一个重要的结果：在n-增长和n-浅TRS中，这些原本在浅和不断增长的TRS中可判定的属性不再适用。这意味着没有算法能够执行所需的约简策略来决定这些属性。这表明，随着规则结构的复杂性增加，特别是对变量深度的约束，我们可能需要重新评估这些基本问题在这些特殊类别的TRS中的可判定性边界。 关键词：“近似”、“不可判定性”、“可达性”、“规范化”和“需要性”揭示了研究的核心关注点，即通过探索这些概念在特定结构限制下的行为，来理解理论计算机科学中复杂TRS系统的局限性和可能的突破点。