状态与控制算子的完全迹模型

我们考虑一个包含四种类型的按值调用语言的层次结构，其分别具有高阶或基类型引用，以及具有 callcc 或无控制算子。我们的首个结果是针对最具表达力的设定（同时具有高阶引用与 callcc）构建了一个完全抽象迹模型，其构造遵循操作博弈语义的精神。接着我们考察在上下文中抑制高阶引用与 callcc 所产生的影响，并分别为已知的博弈语义条件——可见性与括号性——提供操作解释。这使我们能够精炼原模型，从而提供与未必使用高阶引用或 callcc 的上下文交互的完全抽象迹模型。在此过程中，我们讨论了每种情形下基于错误与基于终止的上下文测试之间的关系，并将二者分别对应于迹等价与完全迹等价。总体而言，本文对所有四种情形给出了操作博弈语义的系统性发展，它们代表了所谓语义立方体中基于状态的面向。