扩展寻址机、显式替换、PCF、可定义性、完全抽象
摘要：扩展寻址机（EAM）已被引入以表示高阶连续计算。之前，我们已经证明了通过一种简单的编码，它们能够模拟带有显式替换的PCF的操作语义。在本文中，我们证明了这种模拟实际上是一个等价关系：一个PCF程序在一个数字上终止，当且仅当相应的EAM在相同的数字上终止。由此可得，通过将可类型化的EAM通过适当的逻辑关系进行商合，得到的PCF模型是充分的。通过一个定义性结果，即模型中的每个EAM都可以转化为具有相同观察行为的PCF程序，我们得出结论：对于PCF来说，该模型是完全抽象的。
作者：Benedetto Intrigila and Giulio Manzonetto and Nicolas Munnich
论文ID：2306.13756
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-27