Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory

TL;DR

The paper develops a cost‑aware higher‑order recursion language within synthetic domain theory and proves a cost‑sensitive computational adequacy theorem, relating a denotational cost semantics to a novel internal computational semantics defined in an SDT topos with a phase distinction. It introduces PCF_cost, a call‑by‑push‑value style language parameterized by a cost monoid, and constructs a denotational model based on a partial cost monad and a derived cost algebra, together with a dynamic semantics that yields an intrinsic noninterference between cost and observable behavior. The internal SDT model is justified via a relative sheaf construction over a phase‑distinguished presheaf topos, and the adequacy proof uses formal approximation relations and admissibility to connect syntax, cost, and computation. Overall, the work provides a rigorous foundation for cost analytics in higher‑order recursion within SDT, enabling internal reasoning about cost profiles and their impact on program behavior while preserving noninterference properties. The results have implications for verifying cost bounds and instrumented optimizations in dependently typed settings, with potential extensions to richer recursive and phase‑aware cost analyses.

Abstract

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.

Figures (5)

• Figure 1: The grammar of types and terms in . We will often omit $\kw{Tm}^{\{+,\ominus\}}$ in the case of closed terms and write $\Gamma \vdash \{A, X\}$ for the type $\kw{Tm}^{\{+, \ominus\}}(\Gamma, \{A, X\})$. Given $e : \U{\F{A}}$ and $f : \U{(A \to X)}$, we also write $e; f$ for $\kw{bind}(e, f) : \U{X}$.
• Figure 2: Left: distributive law; right: monad structure of $\mathbb{T}$.
• Figure 3: Selected clauses of the model; in the above we write $U(X)$ for the carrier of a $\mathbb{T}$-algebra $X$.
• Figure 4: Rules for the small-step transition relation.
• Figure 5: Formal approximation relations. We write $\overline{-} : 2 \to \kw{ans}$ for the function sending $0$ to no and $1$ to yes. The relation $\mathsf{adq} \subseteq \kw{T}(1) \times \tmv{\U{\F{1}}}$ is the "ground relation" that generates the formal approximation relations at higher types.

Theorems & Definitions (120)

• proposition 1
• remark 1
• definition 1
• definition 2
• definition 3
• definition 4
• definition 5
• definition 6
• definition 7
• definition 8