Amb算子的指称属性失效与局限：一个关键示例

本文主要探讨了麦卡锡的"amb"算子在理论计算机科学中的复杂性问题，特别是其在指称属性和操作性质方面的挑战。 amb算子与传统非确定性多程序模型(MHMJ)不同，因为它具有独特的性质，可能导致潜在的歧义和不稳定性。文章的核心关注点在于两个尚未解决的问题： 1. 应用模拟与amb的兼容性： 在非类型化的和类型化的环境中引入的应用双相似性理论，起初被认为是自洽的，但在存在amb的情况下，其有效性受到了质疑。由于amb的存在，应用性双相似性是否等同于全等性的问题仍然悬而未决。作者指出，这种不稳定性使得在amb的上下文中讨论应用模拟变得困难。 2. 上下文等价与amb的挑战： 上下文引理是一个关于环境无关性的重要原则，它声明M和MJ在任何封闭替换下的环境里应保持上下文等价。然而，当amb算子加入时，这个引理的适用性成为了一个开放问题，因为amb可能会导致程序行为在不同上下文中产生显著差异。 通过提供一个具体的例子，作者展示了一个情况，即使在最严格的上下文关系（如应用性双相似性）中，两个程序M和MJ也需要在任何环境下重新计算，看似等价，但实际上它们在amb的介入下表现出不一致的行为。这表明在amb存在的情况下，试图找到一个既满足上下文等价又保持良好指向性的指称语义是不可能的。 文章的关键贡献在于通过实例论证来揭示amb算子对现有理论的冲击，并强调了在设计处理amb的语义模型时需要考虑的复杂性。此外，它也提出了一个假设，即如果限制amb仅在地面类型上使用，那么某些操作性质（如上下文引理和细化相似性）可能得以保全。 这篇文章深入剖析了amb算子对理论计算机科学中指称属性理解的挑战，并展示了在处理这种非传统程序结构时所面临的难题。