Decalf: A Directed, Effectful Cost-Aware Logical Framework

TL;DR

This work introduces decalf, a directed, effectful cost-aware logical framework that extends cost analysis to embrace effects such as probabilistic choice and mutable state. It achieves this by treating cost as an effect via a step-counting primitive and by enforcing a phase distinction ExtOpn that separates extensional behavior from intensional cost information, with costs represented as programs themselves using an intrinsic preorder on all types. The theory provides a dependent call-by-push-value core, a cost-inequality relation, and a presheaf/topos-theoretic model based on augmented simplicial sets, then demonstrates a suite of verification examples including pure algorithms, nondeterminism, probabilistic computations, and global state, while showing how higher-order functions and parallelism can be analyzed compositionally. The work offers a unified framework that integrates cost and behavior across effects, provides formal semantics, and outlines future directions such as amortized analysis, probabilistic reasoning, and richer effect interactions, with practical mechanization in Agda.

Abstract

We present ${\bf decalf}$, a ${\bf d}$irected, ${\bf e}$ffectful ${\bf c}$ost-${\bf a}$ware ${\bf l}$ogical ${\bf f}$ramework for studying quantitative aspects of functional programs with effects. Like ${\bf calf}$, the language is based on a formal phase distinction between the extension and the intension of a program, its pure behavior as distinct from its cost measured by an effectful step-counting primitive. The type theory ensures that the behavior is unaffected by the cost accounting. Unlike ${\bf calf}$, the present language takes account of effects, such as probabilistic choice and mutable state; this extension requires a reformulation of ${\bf calf}$'s approach to cost accounting: rather than rely on a "separable" notion of cost, here a cost bound is simply another program. To make this formal, we equip every type with an intrinsic preorder, relaxing the precise cost accounting intrinsic to a program to a looser but nevertheless informative estimate. For example, the cost bound of a probabilistic program is itself a probabilistic program that specifies the distribution of costs. This approach serves as a streamlined alternative to the standard method of isolating a recurrence that bounds the cost in a manner that readily extends to higher-order, effectful programs. The development proceeds by first introducing the ${\bf decalf}$ type system, which is based on an intrinsic ordering among terms that restricts in the extensional phase to extensional equality, but in the intensional phase reflects an approximation of the cost of a program of interest. This formulation is then applied to a number of illustrative examples, including pure and effectful sorting algorithms, simple probabilistic programs, and higher-order functions. Finally, we justify ${\bf decalf}$ via a model in the topos of augmented simplicial sets.

Figures (13)

• Figure 1: Recursive implementation of the doubling function on natural numbers, instrumented with one cost at each recursive call.
• Figure 2: Recursive implementation of the list insertion, the auxiliary function of insertion sort, instrumented with one cost per element comparison.
• Figure 3: Insertion sort algorithm, using auxiliary insert function from \ref{['code:insert']}. Cost is not directly instrumented here, but a call to isort counts comparisons based on the implementation of insert.
• Figure 4: Specification of the $\mathsf{branch}$ and $\mathsf{fail}$ primitives for finitary nondeterministic branching, which form a semilattice. The laws for interactions with the $\mathsf{step}$ primitive are included. Note that $\mathsf{fail}$ is the nullary correspondent to $\mathsf{branch}$, so just as $\mathsf{branch}/\mathsf{step}$ pushes cost into all two branches, $\mathsf{fail}/\mathsf{step}$ pushes cost into all zero branches. The laws for interactions with computation type primitives are omitted for brevity, as they are analogous to those described in \ref{['sec:cost-as-an-effect']}.
• Figure 5: Quicksort algorithm hoare:1961hoare:1962, where the choose auxiliary function chooses a pivot nondeterministically. As in \ref{['code:insert', 'code:isort']}, the cost instrumentation tracks one unit of cost per comparison.

Theorems & Definitions (33)

• proposition 1: Noninterference
• Remark 1
• theorem 2
• definition 1
• definition 2
• proposition 2: Orthogonal reflection
• definition 3: Partial order on the interval
• definition 4: Finite chains
• definition 5: Paths
• definition 6: The path relation