Decalf: A Directed, Effectful Cost-Aware Logical Framework

Abstract

We present <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mstyle mathvariant="bold"> <mml:mtext>decalf</mml:mtext> </mml:mstyle> </mml:math> , a d irected, e ffectful c ost- a ware l ogical f ramework for studying quantitative aspects of functional programs with effects. Like <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mstyle mathvariant="bold"> <mml:mtext>calf</mml:mtext> </mml:mstyle> </mml:math> , 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 <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mstyle mathvariant="bold"> <mml:mtext>calf</mml:mtext> </mml:mstyle> </mml:math> , the present language takes account of effects , such as probabilistic choice and mutable state. This extension requires a reformulation of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mstyle mathvariant="bold"> <mml:mtext>calf</mml:mtext> </mml:mstyle> </mml:math> ’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 cost recurrence and readily extends to higher-order, effectful programs. The development proceeds by first introducing the <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mstyle mathvariant="bold"> <mml:mtext>decalf</mml:mtext> </mml:mstyle> </mml:math> 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 <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mstyle mathvariant="bold"> <mml:mtext>decalf</mml:mtext> </mml:mstyle> </mml:math> via a model in the topos of augmented simplicial sets.

Topics & Concepts