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 中可作为操作语义在数学上更自然的替代方案。特别地，我们证明了一个内部的、代价敏感的普洛特金计算充分性定理，为基础类型上的完整程序在指称语义与计算语义之间给出了精确的对应关系。本文的构造与证明均在 SDT 拓扑斯的内蕴依赖类型论中进行，该类型论按照斯特林和哈珀的意义通过相位区分进行了扩展。通过在指称语义中利用相位区分来控制代价结构的解释，我们证明了 $\textbf{PCF}_\mathsf{cost}$ 程序还展现出代价与行为的非干涉性质。我们基于 SDT 的相对层模型构造来验证该类型理论的公理。