合成域理论中高阶递归的成本敏感计算充分性

我们在合成域理论（SDT）的框架下研究了一种名为$\textbf{PCF}_\mathsf{cost}$的面向成本的高阶递归编程语言。我们的主要贡献在于将$\textbf{PCF}_\mathsf{cost}$的指称成本语义与其计算成本语义联系起来，这是一种新的程序执行动态语义，作为SDT中操作语义的数学上自然的替代方案。特别地，我们证明了Plotkin计算充分性定理的一个内部、成本敏感的版本，给出了基类型完整程序的指称语义和计算语义之间的精确对应关系。本文的构造和证明发生在SDT拓扑斯的内蕴依赖类型理论中，该理论通过Sterling和Harper意义上的相位区分进行了扩展。通过控制指称语义中通过相位区分的成本结构的解释，我们证明了$\textbf{PCF}_\mathsf{cost}$程序也展示了成本和行为的不干涉性质。我们通过基于SDT的相对层模型构造验证了类型理论的公理。