We study a cost-aware programming language for higher-order recursion dubbed $\textbf{PCF}_\mathsf{cost}$ in the setting of synthetic domain theory (SDT). Our main contribution relates the denotational cost semantics of $\textbf{PCF}_\mathsf{cost}$ to its computational cost semantics, a new kind of dynamic semantics for program execution that serves as a mathematically natural alternative to operational semantics in SDT. In particular we prove an internal, cost-sensitive version of Plotkin's computational adequacy theorem, giving a precise correspondence between the denotational and computational semantics for complete programs at base type. The constructions and proofs of this paper take place in the internal dependent type theory of an SDT topos extended by a phase distinction in the sense of Sterling and Harper. By controlling the interpretation of cost structure via the phase distinction in the denotational semantics, we show that $\textbf{PCF}_\mathsf{cost}$ programs also evince a noninterference property of cost and behavior. We verify the axioms of the type theory by means of a model construction based on relative sheaf models of SDT.

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