基于扩展寻址机的 PCF 完全抽象模型
计算机科学中的逻辑
2025-08-13 v5
摘要
扩展寻址机（EAMs）被引入用于表示高阶顺序计算。此前，我们已表明它们能够通过简单的编码模拟扩展了显式替换的 PCF 的操作语义。在本文中，我们证明该模拟实际上是一种等价：一个 PCF 程序恰好在某个数上终止，当且仅当相应的 EAM 在同一个数上终止。由此可知，通过对可类型化 EAMs 按合适的逻辑关系作商所获得的 PCF 模型是充分的。由一个可定义性结果——即模型中的每个 EAM 都可转化为具有相同的观测行为的 PCF 程序——我们得出结论：该模型对 PCF 是完全抽象的。
引用
@article{arxiv.2306.13756,
title = {A Fully Abstract Model of PCF Based on Extended Addressing Machines},
author = {Benedetto Intrigila and Giulio Manzonetto and Nicolas Munnich},
journal= {arXiv preprint arXiv:2306.13756},
year = {2025}
}
备注
arXiv admin note: text overlap with arXiv:2212.11147