一句话：证明 EAM 对 PCF 的模拟是终止等价的，并借助可类型化 EAM 与可定义性给出 PCF 的完全抽象模型。
本文研究 PCF 的语义模型与完全抽象性。扩展寻址机器（EAM）被用于表示高阶顺序计算，此前工作已给出一种简单编码，使 EAM 能模拟带显式替换的 PCF 操作语义。本文证明该模拟实际上是等价关系：PCF 程序在某个 numeral 上终止，当且仅当对应 EAM 在同一 numeral 上终止。由此，将可类型化 EAM 按合适的逻辑关系取商所得的 PCF 模型是可靠的（adequate）。作者进一步证明可定义性结果：模型中每个 EAM 都能转换成具有相同观察行为的 PCF 程序。结合可靠性与可定义性，该模型对 PCF 是完全抽象的。
Extended addressing machines (EAMs) have been introduced to represent higher-order sequential computations. Previously, we have shown that they are capable of simulating -- via an easy encoding -- the operational semantics of PCF, extended with explicit substitutions. In this paper we prove that the simulation is actually an equivalence: a PCF program terminates in a numeral exactly when the corresponding EAM terminates in the same numeral. It follows that the model of PCF obtained by quotienting typable EAMs by a suitable logical relation is adequate. From a definability result stating that every EAM in the model can be transformed into a PCF program with the same observational behavior, we conclude that the model is fully abstract for PCF.arXiv admin note: text overlap with arXiv:2212.11147
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{IntrigilaMM25,
title = {A Fully Abstract Model of PCF Based on Extended Addressing Machines},
author = {Benedetto Intrigila and Giulio Manzonetto and Nicolas Munnich},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 3},
year = {2025},
doi = {10.46298/lmcs-21(3:17)2025}
}