A Verified Cost Model for Call-By-Push-Value

The $\lambda$-calculus [7] is a fundamental model of computation that represents functions as abstractions over variables. It provides a foundation for computability, mathematical logic, and functional programming. Functional programming supports a concise, declarative style of programming that is ideal for reasoning about functional correctness properties.

Besides functional correctness, another important property of a program is its computational complexity. It addresses the vital questions: How fast does my program produce an output? How much space will my program use in order to produce that output?

In complexity analysis, we describe the asymptotic behaviour of cost functions that model the cost of the program mathematically. But where do cost functions come from? In practice they are often constructed in an ad hoc manner with no formal connection to any program semantics. Cost models bridge that gap.

Creating cost models for functional programming languages is thus an essential topic. It is also a significant challenge due to the abstract nature of functional programming. As $\lambda$-calculus is the basis of functional programming languages, a vital question is whether we can create cost models for the $\lambda$-calculus. There has been a large body of research [18, 8, 2, 1, 11, 12, 3] dedicated to solving this problem. An important parameter in a cost model for the $\lambda$-calculus is the choice of evaluation strategy. One strategy is call-by-value, where function calls are applied once the arguments are fully evaluated, as in Standard ML [23]. Another strategy is call-by-name, where the evaluation of arguments is deferred and the function call happens first.

The call-by-push-value $\lambda$-calculus (CBPV) [19] is a variant of $\lambda$-calculus where the evaluation strategy can be set on a call-by-call basis. In particular, CBPV has syntactic constructs that enable delaying or forcing the evaluation of specific terms. Various evaluation strategies, including call-by-value and call-by-name, can be encoded within this subsuming paradigm.

This high expressive power of CBPV has resulted in a long line of work on the language since its inception [10, 9, 24, 22, 13, 15, 6, 16]. Prior work has studied and extended the calculus [16, 27, 22], related it to other calculi [10, 6, 14], and formalised it [24, 13]. The fine-grained control CBPV provides has proved useful to verify compiler optimisations [24].

There are foundational results that demonstrate that CBPV aids in recurrence extraction, which can in turn be used for analysing the complexity of functional programs, with various evaluation strategies [15].

This demonstrates that CBPV can serve as a basis for further research on analysing the complexity of functional programs with various evaluation strategies. As such, it is vital to establish time and space cost models for CBPV. Naturally, such cost models must satisfy some property that demonstrates that they are fit for purpose.

Our goal is to show that CBPV is reasonable. This section is a high-level overview of our proof strategy, which is detailed in Section 6. The main theorems involved are:

That is, we must model the cost of CBPV using Turing machines and prove that the resulting simulation is cost-bounded (Theorem 1). Moreover, we must show that CBPV provides sufficient expressivity to reasonably simulate any Turing machine (Theorem 2).

The CBPV $\lambda$-calculus [19, 20] allows encoding the order of evaluation as part of the syntax of a program. Hence, it serves as a subsuming paradigm that enables studying evaluation strategies, and combinations thereof, using a single set of reduction rules. Levy provides semantic-preserving translations from call-by-name and call-by-value into CBPV [20].

For simplicity, we use a core fragment of CBPV that is sufficient for demonstrating reasonability. As such we omit, for instance, the general pair types, and instead introduce a simpler double sequencing operation that will be discussed later. Furthermore, while most presentations of CBPV are typed, ours is untyped CBPV. We consider types an orthogonal concern to cost: the well-typed CBPV terms are a strict subset of the untyped CBPV terms, so a cost model for the latter immediately suggests a cost model for the former.

The CBPV terms are defined below as two mutually recursive sets: the values $𝚅$ and the computations $𝙼$. The mutual recursion adds some technical difficulties in our formalisation as all relevant functions need to be mutually recursive too. For instance, the substitution function for CBPV, and the compilation function for compiling CBPV terms into programs are both defined mutually recursively, which complicates proofs. To simplify the presentation, we will often use a single overloaded name for two such mutually recursive functions.

Fine-grained control over evaluation can be achieved using the $\mathrm{𝖿𝗈𝗋𝖼𝖾}$ and $\mathrm{𝗍𝗁𝗎𝗇𝗄}$ operators. $\mathrm{𝗍𝗁𝗎𝗇𝗄}$ suspends a computation, and $\mathrm{𝖿𝗈𝗋𝖼𝖾}$ resumes a suspended computation.

Note that we have an extra $\mathrm{𝗉𝗌𝖾𝗊}$ that is absent in the standard presentation of CBPV. An example of $\mathrm{𝗉𝗌𝖾𝗊}$ computation is $\mathrm{𝗉𝗌𝖾𝗊}{m}_2{m}_{1}n$. It allows us to evaluate two computations $m_1$ and $m_2$ and use the results in a third computation $n$. Note that the notation within $\mathrm{𝗉𝗌𝖾𝗊}$ follows the convention and binds to the right. This can of course be encoded with nested $\mathrm{𝗌𝖾𝗊}$, but at the cost of higher binding depth: $\mathrm{𝗌𝖾𝗊}{m}_2(\mathrm{𝗌𝖾𝗊}{m}_{1}n)$. Avoiding this higher binder depth will turn out to be crucial for obtaining constant space overhead in Section 6.2. Including pairs in the language would have solved the problem too, but $\mathrm{𝗉𝗌𝖾𝗊}$ suffices for our purposes.

We then formalise the big-step cost semantics of closed CBPV provided by Levy [20]; that is, we only consider terms with no free variables at the top level. Similar to the change we made in the syntax, we also add $\mathrm{𝗉𝗌𝖾𝗊}$ as a special case of the pair type into our semantics.

In order to define the semantics for closed CBPV, we need to first provide a closed substitution function for $\beta$-reductions. The following function $m_v^i$ substitutes all the variables with de Bruijn index $i$ by $v$ in $m$ by recursively visiting all the inner terms of $m$:

Note the special cases such as ${(\lambda .m)}_u^i$, where we need to increment the targeted variable index $i$ accordingly because we are entering extra layers of abstractions. A more special case is ${(\mathrm{𝗉𝗌𝖾𝗊}{m}_2{m}_{1}n)}_u^i$, we increment $i$ by two for this substitution because $n$ needs to leave two free variable names for the two computations $m_1$ and $m_2$.

We then define time cost and space cost semantics for CBPV. For the time cost semantics, we use a judgement $m{\Downarrow }_{k}n$ to mean that the computation $m$ reduces to $n$ in $k$ steps. The rules are given in Figure 1.

For space, the judgement $m{\Downarrow }^{s}n$ says that $m$ reduces to $n$ with space cost $s$. Note that the time and space cost semantics judgements coincide if the cost annotations are ignored.

We define a size function $\Vert m\Vert$ for CBPV terms $m$ as follows. Note that we account for the size of a de Bruijn index $x$ in the term size.

Figure 2 gives inference rules of the space cost semantics. It tracks the maximum intermediate term size of an evaluation. For instance, for the $\mathrm{𝗉𝗌𝖾𝗊}$ case, there are three different evaluation stages: (1). Evaluating $m_1$; (2). Evaluating $m_2$ (3). Substituting results $v_1$ and $v_2$ into $n$. The space cost is the maximum size among these stages.

As a first step in bridging the gap between CBPV and Turing machines, we define a flat data structure to represent programs that correspond to CBPV terms. A program $P$ is formed of a list of tokens, $\mathrm{𝖳𝗈𝗄}$ that are defined as follows:

The de Bruijn index $x$ counts towards the token size because larger indices require more tape cells to store on Turing machines. The size of a program is simply the sum of the size of its tokens plus $1$ (which is the size of the empty program on a Turing machine).

Definitions 4 and 5 define compilation to the substitution and heap machines, respectively.

We use pairs of delimiter tokens (like $\mathrm{𝗌𝖾𝗊𝖳}$ and $\mathrm{𝖾𝗇𝖽𝖲𝖾𝗊𝖳}$) when necessary, to preserve the tree structure of the original term. The development of these compilers was fiddly, since the right balance needs to be struck between including enough structure to prevent different subterms from being conflated or evaluated prematurely, yet not too much structure, because extra structure takes space, and must be accounted for in the space cost bound proofs. $\gamma$ and ${\gamma }^{\prime }$ make slightly different tradeoffs in this respect. We could change the substitution machine to use ${\gamma }^{\prime }$, but the overall proof does not require the machines to use the same syntax.

The following lemma is useful for our space cost analysis. It states that the size of a compiled program is linear wrt. term size. (Note that the same lemma also works for ${\gamma }^{\prime }$.)

We write $P\gg m$ to state that $P$ is the corresponding program for $m$.

Recall from Section 2 that our proof strategy relies on interleaving two simulation strategies to achieve reasonability in time and space. The substitution-based strategy has reasonable overhead for space, but not for time due to the size explosion problem. The heap-based strategy has reasonable overhead for time, but not for space due to the pointer explosion problem. These two explosion problems do not occur at the same time. Thus, by interleaving the respective Turing machines for each of these two strategies, we can obtain a reasonable simulation. In order to achieve this, we first implement two abstract machines that represent these two strategies respectively in this section. We then construct the corresponding Turing machines and finish the rest of the proofs in Section 6. Note that the size of intermediate terms and the complexity differs between the abstract machines and their corresponding Turing machines.

In this section, we first introduce an auxiliary extraction function that is used by both abstract machines (Section 5.1). We then introduce the substitution machine (Section 5.2) and the heap machine (Section 5.3), and investigate their cost in relation to CBPV.

In this section, we use the results from Section 5 to prove that CBPV is reasonable. We achieve this by providing two simulations between CBPV and Turing machines, as elaborated in Figure 6.

Section 6.1 describes how Turing machines can simulate CBPV with polynomial time overhead and constant factor space overhead, fulfilling Theorem 1 in Section 2. Note that this simulation goes through the abstract machines we implemented and formalised in Section 5.

Section 6.2 describes how CBPV can reasonably simulate WCBV. We adapt the result that WCBV can reasonably simulate Turing machines from existing literature [11]. Together, we have that CBPV can simulate Turing machines with polynomial time overhead and constant factor space overhead, fulfilling Theorem 2 in Section 2.