{'fraction_non_alphanumeric': 0.04459839452063402, 'fraction_numerical': 0.008278743893051825, 'mean_word_length': 4.370170406613801, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 20, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
On continuation-passing transformations and expected cost analysis

We define a continuation-passing style (CPS) translation for a typed λ-calculus with probabilistic choice, unbounded recursion, and a tick operator — for modeling cost. The target language is a (non-probabilistic) λ-calculus, enriched with a type of extended positive reals and a fixpoint operator. We then show that applying the CPS transform of an expression M to the continuation λ v. 0 yields the expected cost of M. We also introduce a formal system for higher-order logic, called EHOL, prove it sound, and show it can derive tight upper bounds on the expected cost of classic examples, including Coupon Collector and Random Walk. Moreover, we relate our translation to Kaminski et al.’s ert-calculus, showing that the latter can be recovered by applying our CPS translation to (a generalization of) the classic embedding of imperative programs into λ-calculus. Finally, we prove that the CPS transform of an expression can also be used to compute pre-expectations and to reason about almost sure termination.


INTRODUCTION
Randomized computation has been one of the most fruitful extensions of the standard, deterministic, computational model, since the birth of computer science [De Leeuw et al. 1956;III 1974;Rabin 1963;Santos 1969]. While randomization has been pervasive, and sometimes essential, in the design of, e.g., efficient algorithms [Motwani and Raghavan 1995] and cryptographic primitives [Goldwasser and Micali 1984], the development of a proper theory of randomized programming languages has been (starting from the pioneering works by Saheb-Jaromi [Saheb-Djahromi 1978] and Kozen [Kozen 1981]) much slower, and is still a very active research area (see, e.g., [Batz et al. 2021;Ehrhard et al. 2018]).
Among the program properties of interest, one certainly finds functional properties, like program correctness, but also nonfunctional, more intentional ones. An example of non-functional properties of particular interest are those related to the execution cost, a key property of programs and the main focus of cost analysis. In general, the intended result of cost analysis are estimates about the execution cost, which can have various levels of accuracy. A wide range of approaches for cost analyses exist, based on, e.g., abstract interpretation [Albert et al. 2012], type systems [Jost et al. 2010] and program logics [Atkey 2011;Danielsson 2008;Nielson 1987;Radicek et al. 2018]. The latter are generally more expressive, and are well suited for examples that require either value sensitivity or functional verification.
This paper is concerned about cost analysis of randomized higher-order programs, i.e. programs which can sample values from chosen distributions during execution, and at the same time are capable of treating functions as first-class citizens. The evaluation of such a program results in a distribution of values, and has an expected cost, namely the average cost the program experiences along its execution. In this setting, the intended result of cost analysis is an upper bound for the expected cost. Some of the approaches used in the deterministic setting extend to the probabilistic setting, namely type systems and program logics [Kaminski and Katoen 2017;. In a higher-order setting, the only technique which has been studied is the one based on types, which have indeed been proved to be applicable to higher-order randomized languages [Avanzini et al. 2019a;Dal Lago and Grellois 2017;Wang et al. 2020]. The main advantage of adopting type systems is the inherent compositionality of the obtained methodology. On the other hand, type systems for randomized languages are generally designed around abstractions which prevent them to prove arbitrary bounds.
A different approach to analyse a given program is driven by program transformations: the program at hand is transformed into another one, possibly written in a simpler language for which some analysis methodologies have already been provided. This, of course, requires a proof that the result of the analysis of the transformed program can somehow be lifted back to the source program. Examples of such an approach are found in the realm of deterministic programs (e.g., [Avanzini et al. 2015;Cutler et al. 2020;Wegbreit 1975]). However, the design of program transformations for (higher-order) randomized programs is a largely unexplored research area. In particular, reducing expected cost analysis to another, better analysed, and conceptually simpler kind of analysis seems natural, but to the best of the authors knowledge, has not been studied so far. This is precisely what we do in this paper. Specifically, we make the following contributions: • We provide a continuation-passing style (CPS) transformation for a probabilistic variation of Plotkin's PCF. The target of the transformation is given by the pure fragment of the source language, extended with a type of extended positive reals. We define a denotational semantics of the target language, by giving meaning to recursive definitions in terms of a non-standard interpretation of positive real numbers. Under this interpretation, the expected cost of the source program is the denotation of the target program applied to the continuation .0. This way, the expected cost of the source program can be analysed, thanks to the program transformation, by looking at the extensional behavior of the pure program, thus taking advantage of any methodology for reasoning about the latter. • As one example of such a methodology, we introduce a form of unary higher-order logic [Aguirre et al. 2017] in which statements about terms of the target language can be proved to hold in a sound way, even in the presence of recursive definitions. This crucially relies on a restriction on the kind of predicates one employs when dealing with functions defined as fixed points. Despite ruling out many logical formulas, this class includes the kind of predicates one is interested at while proving upper bounds on the expected cost. • We illustrate the overall methodology via the analysis of two classic examples, viz a random walk example and an implementation of the coupon collectors problem. • We show that the ert-calculus of  Ð a weakest pre-expectation calculus for reasoning about the expected runtime of randomized algorithms written in an imperative probabilistic language Ð is recovered through an application of our CPS transformation on a  standard embedding of (probabilistic) imperative programs within our source language. Our methodology thus strictly extends upon the strength of the ert-calculus, a calculus that is not only sound but also complete for imperative, probabilistic programs.
• We show that our methodology is not limited to expected cost analysis, but can also be used to reason about pre-expectations and almost sure termination.
Outline. We start with an informal explanation in Section 2. The target language is defined in Section 3, and the transformation Ð as well as the target language Ð is formalised and proved correct in Section 4. In Section 5 we introduce the aforementioned higher-order logic. Section 6 shows the embedding of the ert-calculus in our setting. In Section 7 we briefly discuss some further implication of our results. Finally, we draw pointers to related work in Section 8 and conclude in Section 9.

RANDOMIZED PROGRAMS AND CPS: A BIRD'S EYE VIEW
In this section, we illustrate how our continuation-passing transformation works on some concrete examples of randomized programs, and in particular on the so-called coupon-collector example. Consider the piece of code in Fig. 1a, written in a functional language. The idea is that someone wants to collect all the coupons in a list , and that she does so by keeping track of the coupons she already has in another, initially empty, list . Coupons are collected by iteratively drawing coupons from and adding them to , until all the desired coupons in are also part of .
The program at hand can be seen as a randomized program, due to the presence of the primitive draw : List(C) → C, which samples an element uniformly at random from the argument list. The program also produces another kind of effect, namely the one raised by the (·) ✓ primitive. This is meant to be a way of modeling cost from within the program: whenever a draw is made, the cost of the underlying computation is increased by 1. As an example, calling coupons with the argument list [1,2] gives rise to the recursion tree in Figure 2a. Note that, as indicated on the arrows, each recursive call happens with probability 1 /2 Ð the probability of drawing a coupon uniformly from the supplied list of coupons [1,2].
The main question now is: what is the expected cost of this program? What is the average amount of times the (·) ✓ primitive is executed? We could be very lucky, and incur a cost equal to the cardinality of , but oftentimes we get the same coupon more than once, so the number of draws required to get the whole collection would be larger. We could even be very unlucky and indefinitely continue to get the same coupon, that is, the program diverges.
One way to tackle cost analysis, going back to the seminal work of Rosendahl [1989], lies in turning the program at hand into a second one, which is structurally quite similar but computes  the cost of execution in addition. Such a program transformation thus turns an intensional property, namely the cost of execution, into an extensional one. Standard methods, such as recurrence relations employed by Rosendahl or abstract interpretations [Cousot and Cousot 1977] can establish now a cost analysis of the original, source program. While Rosendahl studied only a pure, first-order fragment of Lisp, more recently conceptually similar ideas have been successfully applied to the cost-analysis of higher-order, functional programs [Cutler et al. 2020;Danner et al. 2015]. None of these works, though, deal with randomized programs and expected cost analysis. Coming back to the coupon collector example, translating this idea directly suggests that we are searching for a function of type List(C) → List(C) × Nat, which, given an initial list of coupons returns besides the list of collected coupons also the overall cost, as a natural number. Surely, such a term can be found, by simply threading through the computation a counter that is incremented whenever the (·) ✓ primitive is encountered. However, this is only of little help to our concerns: the resulting program would still be probabilistic. How would we arrive at an expected cost analysis, where the randomized behavior has been resolved? One way to overcome this problem Ð in the context of expected runtime analysis of imperative programs Ð has been given by  in the form of a pre-expectation calculus. The expected cost of a continuation is gradually turned into that of an overall computation. In our setting, this would imply that the expected cost of a term : is indeed given in terms of a functional term : ( → Real + ) → Real + . When supplied with an argument : → Real + expressing the (non-negative) cost of the underlying continuation, this term is supposed to return the overall expected cost of evaluating followed by the continuation supplied with the result of .
Concerning the term = draw( ), for instance, such a cost transformer is given . ∈ 1 /| | * for | | the cardinality of . 1 Notice how this term simply gives the expected value of on the uniform distribution on coupons . How do we lift this idea to arbitrary programs? As it turns out, on the non-probabilistic fragment of the language a standard continuation-passing style (CPS) transformation is sufficient. In the case of (·) ✓ , we simply add one to the output, and in the case of sampling primitives we proceed as above. Thereby, we have turned a CPS transformation into an expected cost transformer, much in the spirit of the expected runtime transformer of . Indeed, the overall approach is quite reminiscent of the way Ramsey and Pfeffer [2002] give semantics to a stochastic lambda calculus within Haskell, with the main difference that we're focusing on costs and directly compute expectations.
When applied to the function coupons, the so suited CPS transformation results in the program given in Fig. 1b. In effect, couponsCPS computes the expected cost of coupons together with the one of the argument continuation when applied to the result of coupons. The sum of the two is what couponsCPS finally produces in output. Please note how the continuation is passed around from the current call to collectCPS to the next one.
But what if we are interested in the cost of coupons alone? Well, it suffices to apply couponsCPS to the continuation .0, obtaining something like the following program: At least, now, we have obtained a program which looks like it can then be used to analyse the expected cost of coupons, e.g. via standard type-theoretical tools. A careful look at couponsCost reveals that this is not really the case, at least if couponsCost is interpreted as a deterministic functional program. Indeed, if is not the empty list, then executing couponsCost produces nothing less than an infinite tree of recursive calls to collectCost. For example, the recursive calls induced by couponsCost [1, 2] forms a tree isomorphic to the one in Figure 2a. In which sense, then, does couponsCost compute the expected cost of coupons ? The answer is that it does so only up to approximations. As an example, couponsCost [1, 2] can be seen as computing a numerical expression, namely that in Figure 2b which, being infinitary, only denotes a real number (or infinity) when the type of extended positive real numbers Real + (and related operators) is interpreted in a slightly non-standard way. In other words, the fact the tree is infinite does not result in undefinedness, but rather in an approximation process.
Some questions, then, remain unanswered. In which sense is the transformation from coupons to couponsCPS correct? How could we analyse the behavior of any program in the target language of our CPS transformation? Clearly, these questions cannot be answered by the same kinds of techniques employed classically, and this is precisely the bulk of our technical contribution. To prove correctness of our CPS transformation, with the operational semantics of randomized programming languages being inherently infinitary, one has to reason up to approximations. As the source language of randomized programs is infinitary, so is the target language. To reason about programs in the target language, we introduce a higher-order logic, dubbed EHOL. Very briefly, in this logic judgments have the form that can be seen as an extension of the usual typing-judgment Γ ⊢ : with assertions Φ acting as assumptions and an assertion talking about the term through a distinguished variable r.
The novel aspect of EHOL lies in the fact that it can be used to reason about infinitary computations such as the one underlying couponsCost. This is achieved, not through constraining the logical system and therefore inherently limiting its power, but rather by considering well-behaved assertions whenever dealing with recursive definitions. In short, such predicates have to be continuous in r, thereby enabling reasoning on infinite computations, such as the one illustrated in Figure 2b, via their finite approximations. Such continuous assertions are syntactically captured in our notion of ≤-positive assertions (see Section 5). Crucially, these encompass assertions such as r ≤ that represent upper-bounds.
Typing rules, pure fragment Reduction rules, pure fragment Reduction rules, non-pure fragment Returning to our example, within EHOL we can derive validity of the judgment · | · ⊢ couponsCost : List(C) → Real + | ∀ : List(C). r ≤ | | · | | =1 1 / , yielding the optimal bound for couponsCost in terms of the provided list of coupons , which then translates to a bound on the cost of coupons.
Summing up, what we then have obtained is a novel methodology for reasoning about the expected cost of probabilistic programs. Our approach distinguishes itself through its expressiveness and Ð as we demonstrate on a non-trivial example Ð allows a form of compositional reasoning that scales well also to the presence of higher-order combinators.

A PROBABILISTIC HIGHER-ORDER LANGUAGE
In this section we define our vehicle calculus. Its pure fragment, defined first, is a mild extension of Plotkin's PCF with built-in operations and algebraic data types such as lists or trees. The impure fragment then extends upon this language with primitives for sampling and cost.

The Pure Fragment
We consider a simply-typed language, with base types drawn from a set B, such as Bool for Booleans, Int for integer numbers or List( ) for lists over elements of type ∈ B. Simple types are given by the following grammar: , ::= B | →

(Simple Types)
As usual, → binds to the right.
To define terms, we consider three disjoint sets X, C and F , of variables, constructor (symbols) and function (symbols), respectively. All three sets may be infinite but, if not mentioned otherwise, are countable. Each symbol s ∈ C ∪ F is associated with a type schema, in notation s : B 1 ×· · ·×B → B or simply s : B when = 0. While constructors serve to form ground values, any function symbol computes a function on ground values. For instance, we may use constructors i : Int ∈ C to embed integer numbers ∈ Z within the language, and introduce function symbols such as (+) : Int × Int → Int that implement arithmetic operations on such values. Without loss of generality, we also impose that primitive operations are fully applied, so for instance + is not a valid term. Values and terms with free variables X are formed from the following grammars, where c ∈ C, s ∈ C ∪ F and , , ì and range over variables in X.
In examples, and as we have already done before, we may use several standard shortcuts, such as if then else as an abbreviation for case of {true ↦ → | _ ↦ → } and let = in for ( . ) · . Throughout the following, we consider only well-typed terms, that is we tacitly assume that any term is such that Γ ⊢ : holds according to the rules from Figure 3 for some typing context Γ (a mapping from variables to simple types) and type . We denote by Λ (Γ) the set of all such terms, we use Λ ≜ Λ (∅) to denote the set of ground terms of type , and we let Λ ≜ Λ denote the set of all well-typed terms. In correspondence, the sets V (Γ), V and V denote the well-typed (ground) values (of type ).
We now turn to the semantics of expressions. To each function symbol f : B 1 × · · · × B → B we associate a primitive f I : V B 1 × · · · × V B → V B which is meant to capture the intended semantics of f. Evaluation contexts are formed from the following grammar, where s ∈ C ∪ F . C, D ::= □ | · C | C · | s( ì , C, ì ) | case C of {c( ì) ↦ → | ↦ → } (evaluation contexts).
With C[ ] we denote the term obtained by replacing the hole □ in C by . We denote by − − → ⊆ Λ×Λ ( ∈ { , , , }) the contextual closure of the reduction rules ↦ → depicted in Figure 4; with − − → we denote the union of these three relations. Notice that evaluation is right-to-left.
Up to now, the introduced language can be seen as nothing more than a standard extension of (call-by-value) PCF to a given set of base types which includes, but which is not necessarily limited to, the natural numbers. The next step consists of rendering our vehicle calculus effectful.

The Non-pure Fragment
The randomized higher-order language Λ that we are considering is an extension of the pure language Λ with primitives for sampling and cost. For the sake of simplicity, we stick to a language in which sampling can be done from discrete distributions. However, we believe all our results could be lifted to a setting in which measure theory plays a key role, see e.g. [Ramsey and Pfeffer 2002].
Preliminaries and Syntax. Let D( ) denote the set of discrete (sub)distributions over , namely the set of total functions from to R [0,1] whose sum is itself in R [0,1] and whose support supp( ) = { ∈ | ( ) ≠ 0} is countable. Moreover, let R + denote the non-negative reals, and R +∞ its extension by ∞. We denote by { } ∈ the distribution in D( ) assigning probability to ∈ for every ∈ , or simply by { 1 1 , . . . , } when the support { 1 , . . . , } is finite. The expected value of a function : → R + on ∈ D( ) is denoted by E ( ). Since we restrict ourselves to discrete distributions, this is given by ∈supp( ) ( ) · ( ). Finally, we denote by ∈ · the convex combination of distributions . Note that probabilities are expected to sum up to ≤ 1, thereby the convex combination always results in a distribution. For instance, we have To incorporate probabilistic sampling, we assume a designated set of distribution symbols D. As for constructors and functions, each symbol p ∈ D is given a type schema p : B 1 × · · · × B → B. As expected, each such p is associated with a primitive p I : . For instance, we may consider ber : Ratio → Bool ∈ D with ber I (q) ≜ {true , false 1− } for any rational 0 ≤ ≤ 1. Note that p I ( 1 , . . . , ) can be a proper sub-distribution, in which case the missing probability signals abnormal termination. Semantically, this will be interpreted identical to non-termination. For instance, we may set ber I (q) ≜ ∅ when is not in the interval [0, 1].
To endow programs with a cost model, as mentioned before, we make use of an operator (·) ✓ that incurs a cost of one to the cost of evaluating its arguments. In summary, impure terms are obtained by extending the pure terms as follows: With Λ (Γ) we denote the set of impure terms typeable under typing context Γ as (see Fig. 3) and, identical to before, Λ (Λ ) denotes the set of well-typed terms (of type ).
Example 3.1 (Random Walks). For illustration, consider the following recursively defined function: This function iterates as long as the provided predicate : Int → Bool holds, with the next recursion parameter : Int computed by a stepping function : Int → Int. The tick in the elsebranch signifies that we are interested in a cost corresponding to the number of recursive calls. While walk is itself non-probabilistic, we can apply it to several interesting probabilistic argument functions. As an example, consider geo ≜ walk · ( _.ber( 1 /2)) · ( . + 1) .
Then, for instance, the output of geo · 0 follows the geometric distribution {0 1 /2 , 1 1 /4 , 2 1 /8 , . . . }. As we will see, the expected number of iterations, i.e., the expected cost of geo 0 is constant. As another example, consider the term parameterised by a rational constant p, which performs a biased random walk over positive integers. It is folklore that such a random walk over non-negative integers is bounded only when p > 1 /2, i.e., when the walk is more likely to go down than up.
Operational Semantics. In order to capture the two effects, probabilistic sampling and cost, we express the operational semantics of the language Λ by a (probabilistic) reduction relation − − → ⊆ D(Λ )×R +∞ ×D(Λ ), defined through a (weighted) probabilistic abstract reduction system [Avanzini et al. 2020;Bournez and Garnier 2005] over terms Λ . Triples ( , , ) ∈ − − →, written as − − → , signify that the term distribution evolves in one-step to a reduct-distribution , producing an expected cost equal to . To define this relation formally, let us first extend evaluation contexts to the impure fragment by setting C, D ::= · · · | p( ì , C, ì ) (impure evaluation contexts) .
The reduction rules for the two non-pure constructs are given in the second part of Figure 4. The operator (·) ✓ produces a cost of one without evaluating its argument, thereby attributing functions such as the ticked Ω-term letrec = ( · ) ✓ an infinite cost, rather than a cost of zero. Saying it another way, we are call-by-value, but cost-by-name.
To avoid notational overhead, we may drop in − − → if = 0 and identify Dirac distributions { 1 } with terms . Thereby, all reduction rules ↦ → from Figure 4, even the pure ones, can be seen as ternary relations ↦ → ⊆ Λ × R +∞ × D(Λ ). Based on these, in Figure 5 we define the probabilistic reduction relation on distributions. Informally, − − → if is obtained by replacing in all reducible terms by corresponding reduct-distributions, preserving values. The cost is given by the average cost of all involved reduction steps. Formally, it is most convenient to define this relation through the three inference rules from Figure 5. Let us look at probabilistic rewriting defined this way on an example.
Example 3.2 (Example 3.1 continued). Reconsider the term geo and let us abbreviate ( _.ber( 1 /2)) and ( . + 1) by p and f, respectively. Thus geo = walk p f which, when supplied the integer n ∈ C, gives rise to the probabilistic reduction sequence where redexes are underlined. Reducing the redex ber( 1 /2) in the third step effectively forks the reduction into two probabilistic branches, each weighted with probability 1 /2. Continuing the reduction on the branch where ber( 1 /2) reduces to true yields the constant n. This constant now persists throughout the overall reduction. On the other branch, we eventually reach the recursive call to walk · p · f · (f · n). Here, the cost incurred by the tick, weighted with the corresponding probability 1 /2, is reflected in the reduction step. This process now repeats, ad libitum, halving however the probability of performing a recursive call at each iteration, and thereby also the imposed costs. Writing − → * for a finite sequence = 0 , a reduction of geo · 0 has overall the shape This infinite sequence gradually approaches the geometric distribution {0 1 /2 , 1 1 /4 , 2 1 /8 , . . . }, with an overall cost of 1 /2 + 1 /4 + 1 /8 + · · · = 1.
As hinted by this example, the reduction relation − − → is deterministic, i.e., for any term , there is precisely one maximal (and infinite) reduction sequence As we just saw, such a reduction sequence can be seen as gradually approaching a normal-form distribution nf ( ) ∈ D(V ) over values, giving the distribution of values to which evaluates to. From such a sequence we can also compute an element ecost( ) ∈ R +∞ which stands for the cost of the whole computation starting from . Formally, the expected cost ecost ( ) ∈ R +∞ of this evaluation is given by the sum of all the . Equivalently, ecost : Λ → R +∞ can be defined as the least function, ordered point-wise, satisfying the following equations: Note that the equations are exhaustive, since every typeable term is either a value or reducible. 2 Via a telescoping-sum argument, it can be shown that ecost ( ) coincides with the mean cost emitted along all probabilistic reduction paths, compare e.g. [Avanzini et al. 2020], thereby matching its intended meaning. In a similar spirit, nf : Λ → D(V ) can be defined as the least function such that: Here, distributions are ordered point-wise. The fact that nf ( ) is well-defined for every ∈ Λ comes from the fact that distributions form an cpo with respect to the point-wise ordering.

A Semantic Expected Cost Transformer
The expected cost transformer outlined in Section 2 lifts the expected cost : V → R +∞ of a continuation to that of evaluating a term followed by the continuation. This was done syntactically in the form of a program transformation. As we will see in the next sections, this will enable us to reason compositionally. Here, we give an alternative definition of the same function based on the operational semantics, against which we will then show correctness of the proper transformer, to be defined formally in the next section.

Definition 3.3 (Semantic Expected Cost Transformer). The function
is defined as the least function satisfying 2 To be precise, ecost is defined as the least-fixed point of the functional : This fixed-point always exists (see [Winskel 1993]), and assigns a cost ∈ R +∞ even to non-terminating programs.
It can be shown that this cost-transformer is continuous and monotone, hence well-defined, see also [Avanzini et al. 2020] where this operator is defined in a more general setting.
Example 3.4 (Example 3.2 continued). Reconsider the reduction drawn in Example 3.2. Applying Definition 3.3 for an arbitrary : V → R +∞ we have Notice how, by letting be the constant zero function, this term converges to the expected cost of walk · p · f · 0. Dual, by unticking the recursive calls, thereby eliminating all subexpression 1+, we obtain the expected value of on the distribution of its normal forms.
The last statement can be generalized, which is almost immediate to see by contrasting Definition 3.3 with the definition of ecost and nf . To this end, let us call ∈ Λ cost-free when ecost( ) = 0, e.g., when does not contain any occurrence of (·) ✓ . Then Ect[ ]{·} can be brought in correspondence to the expected cost and value on normal form distributions in the following way.
Lemma 3.5. Let ∈ Λ . The following equalities hold: Finally, the following structural properties will be exploited in the inductively defined cost transformer which will be introduced in the next section. Notable, these properties tell us how the expected cost of a term relate to that of its subterms, guiding the inductive definition of the transformer given in the next section.

COMPUTING EXPECTED COSTS
This section is devoted to defining a syntactic variant of the expected cost transformer, which differs from the semantic version from Definition 3.3 in two ways. First, it is defined by induction on the structure of terms, thereby enabling compositional reasoning. Second, it is indeed an (efficiently computable) program transformation, resulting in a (pure) PCF-term rather than a cost function, thereby enabling classical program analysis. The first step we need to make consists in extending the pure fragment of our language, so as to encompass (real-valued) cost functions. This is necessary because costs are measured by real numbers, and the latter have to be treated differently from ordinary data, as will be apparent from the underlying denotational semantics.

The Target Language and Its Semantics
The target language Λ R is given by a fragment of the pure language introduced before, endowed with a dedicated base type Real + to express real numbers ∈ R +∞ . We allow constants r ∈ C for all ∈ R +∞ as well as continuous (particularly, non-decreasing) functions on R +∞ Ð such as multiplication or addition Ð as primitive functions in D. Terms in the target language, as the image of a CPS translation, will have the restricted form where s ∈ C ∪ F . The most notable changes, in comparison to the full probabilistic language, lies in the exclusion of effectful operations Ð (·) ✓ and sampling primitives p ∈ D Ð and that -redexes are confined to head position. We furthermore restrict recursion to computations on R +∞ , particularly, all recursive definitions are constrained to letrec = ì. where is an expression of type Real + . In other words, we subject terms to the typing rules of Figure 3, where the rule governing letrec is replaced by the typing rule Γ; : 1 → · · · → → Real + ; 1 : 1 , . . . ; : Here, we use the notation letrec 1 · · · = for letrec 1 = 2 · · · . . Below, we use Λ R (Γ) to denote the terms within this target language, typeable under context Γ with type .
Denotational Semantics. The target language, being pure, would allow for a standard domaintheoretic denotational semantics. The non-standard behavior of the real-number type, however, makes it necessary to slightly diverge from the usual path. More specifically, the type Real + is interpreted as R +∞ endowed with the vertical ordering, and not by way of the discrete order, as one would possibly expect. An immediate implication is that recursive functions such as above, converge to rather than compute their result. Well-definedness is in essence given in by the Monotone Convergence Theorem. For instance, the operator ∞ ( ·) : Nat → (Nat → Real + ) → Real + defined as letrec ∞ = · + ∞ s( ) , will have the usual convergence properties of infinite sums (over monotone ), and would not return ⊥ as in the usual domain theoretic model of PCF.
Before delving into the details of the model, let us recall some basic notions and results on domain theory, using terminology from Winskel [1993, Section 8]. A partial order ( , ⊑) is called a complete partial order (cpo) (sometimes referred to as predomain) if any -chain 0 ⊑ 1 ⊑ · · · has a least upper bound ∈N in . We do not require in general that is equipped with a least element, but if so, the least element is denoted by ⊥ or ⊥ when is clear from context. Relevant examples of cpo's are discrete cpos where is equipped with the identity relation, R +∞ ordered vertically (i.e., denotes the -fold composition of . All this is nothing more than the basic machinery one needs to give a domain-theoretic denotational semantics to languages like PCF.
Finally, we can give the actual interpretation of the target language's types, each of them being put in correspondence with a cpo. More precisely, Real + is interpreted as R +∞ ordered vertically, while B ∈ B where B ≠ Real + will be put in correspondence with the discrete cpo on terms values Notice that is always a cpo, but is not guaranteed to be endowed with a least element. In particular, any base type other than Real + and any function returning one of such type is interpreted as a cpo which is not, however, pointed. In other words, since we just confined recursion to functions producing a Real + in the target language, we are permitted to interpret the remaining functions as total ones. This has significant practical implications. Later on, when we study the target language, we will not have to reason about non-termination of such functions.
Remark. Well-definedness of follows by construction, as all operators are continuous. By the typing restrictions on letrec ì = , the functional ì ↦ → ; ↦ → ; ì↦ →ì underlying its semantics lives in the space [ −→ ] where = 1 → · · · → → R +∞ , whose bottom element is the constant zero function and top element the constant ∞ function. Fixed-points of a functional, while always well-defined, are in general not reached within a finite number of unfoldings, as exemplified by the operator ∞ ( ·) : Nat → (Nat → Real + ) → Real + above. For and of type , we write ≡ when and are semantically equal, that is, when = . By slight abuse of notation, let us also write ≡ or ≡ if = . Similar, we write ≦ if ≤ , and extend this notation to ∈ as with equality. It can be shown that the denotational agree with the operational semantics in the following way. Despite the language being pure, the operational semantics does not precisely match the denotational one, even at base types.

The Cost Transformer
Our expected cost transformers, defined next, can be seen as an adaptation of the first-order, one-pass CPS transformation by Danvy and Nielsen [2003], with answer type restricted to Real + . As such, the transformer makes the evaluation order explicit. However, in the translation of a term : , rather than receiving a continuation as argument, the cost transformer receives the expected cost of the continuation, as a term : → Real + . This approach requires that for any primitive sampling operation, the expectation wrt. : B → Real + is expressible in the target language. To this end, we assume for every p : B 1 × · · · × B → B ∈ D that a term ⊢ E p( ·,...,·) (·) : B 1 → · · · → B → (B → Real + ) → Real + , exists, satisfying E p( 1 ,..., ) ( ) = E p I ( 1 ,..., ) for all ∈ V B (1 ≤ ≤ ).

Definition 4.3 (Expected Cost Transformer). The expected cost transformer
is given in Figure 7. As usual for CPS transformations, the transformer is defined by mutual recursion with a function (·) † : ∀ Γ.V (Γ) → V † R (Γ) on values. The corresponding translation on types, in notation (·) † , is also given in Figure 7. It is extended component-wise to typing contexts.
The following auxiliary lemma confirms well-definedness of the transformer. As usual for CPS transformations, the expected cost transformer may introduce administrative redexes, which do not find counterparts in the source program. For instance, ect[ · ] { } = ( .(( . · · ) · † ) · † introduces two such redexes, unlike the specialized and semantically equivalent translation † · † · . Administrative redexes can often be optimized away thanks to Lemma 4.1. Similar, but maybe less obvious, -ary functions such as . : 1 → 2 → can be translated to .ect[ ] { } : † 1 → † 2 → ( † → Real + ) → Real + without changing semantics, provided that they are not partially applied. Note that partial applications can always be resolved by -expansion. For the sake of brevity, we will apply such simplifications frequently in examples.
Before we continue with a proof of correctness for this program transformation, let us illustrate it on the running examples. To this end, let us first look on how expectations on some sampling primitives can be computed within the target language.
In the remainder of this section, we prove correctness of the expected cost transformer. This amounts to proving that the semantic transformer introduced here matches the semantic one introduced in Section 3.3. Specifically, on terms ⊢ : B of base types, this correspondence amounts to the equality: for every ⊢ : B → Real + . By Lemma 3.5, this correctness result allows us to instantiate the transformer to one for reasoning about expected costs and values. To prove the equation, we show that ect[ ] { } is bounded by Ect[ ] from above and below. This is the subject of the next two sections.

Upper Bound.
Proving that the syntactic CPS transform is an upper bound to the semantic one cannot be proved directly, unless the same statement is extended to terms of arbitrary type. While the left-hand-side of Equation (1) stays in the form ect[ ] { }, the right-hand-side becomes Ect[ ] ↦ → · † . This is because expect a result in continuation passing form † , whereas in Equation (1) we implicitly employed † = for any value of base-type. The proof essentially relies on the following auxiliary lemma, which basically states that the syntactic CPS transformation is consistent with the denotational semantics, taking costs into account.

Lower Bound.
To prove the lower-bound result, we introduce finite approximations of the expected cost transformer. The construction is similar, but carries an additional counter of type Nat, with elements of this type built from constructors 0 : Nat and s : Nat → Nat. The counter is decremented at each function application, once it reaches zero the computation is aborted.

Mapping of Types
Step-Indexed Expected Cost Transformer is given in Figure 8. As before, it is defined mutual recursively with a one place function (·) ‡ : ∀ Γ.V (Γ) → V ‡ R (Γ ‡ ) on values, and (·) ‡ is also used to transform types. In what follows we prove two properties. First, we show that the step indexed version indeed approximates the expected cost transformer, in the sense that by increasing the step-counter the result of the transformer can be brought arbitrary close to the original definition. In the limit, the two transformers thus coincide. The correspondence is made precise in the following simulation relation.
Definition 4.11 (Simulation Relation). We mutually define two type-indexed, binary relations as follows:
In turn, this relation allows us to prove the following approximation lemma by structural induction, much in the style of logical relations. (1) if ∈ V , then † ‡ ; and Second, with the following lemma we prove that independently of the stepping counter, the approximated cost transformer is bounded by the semantic counterpart: Lemma 4.13. For allˆsuch that ˆ is non-decreasing in its first argument: The lower bound result is now almost an immediate consequence of Lemma 4.12(2) and Lemma 4.13. In the two considered cases, it is not difficult to constructˆfrom with ≃ˆ.
Lemma 4.14. If ∈ Λ and let : → Real + where either = B or is constant. Then Combining this lower-bound result with the upper-bound proven in Lemma 4.9 yields now the final result of this section.

ON HIGHER-ORDER LOGIC AND EXPECTATIONS
Higher-Order Logic can be seen as a program logic for higher-order programs [Aguirre et al. 2017]. In this section, we will show that our target language can be reasoned about by way of tools of the same kind, namely by the expectation higher-order logic (EHOL), a unary higher-order logic specifically tailored for our target language. In particular, statements deriving upper bounds on the expected cost of the program at hand can be derived in EHOL and, thanks to Theorem 4.15, can be lifted back to the operational semantics. Any upper bound on ect[ ] { .0} is also an upper bound of the expected cost of .
Very informally, unary higher-order logic is a form of refinement type system where the assertions are kept separate from simple types. Assertions are derived by way of the following grammar: where ranges over a set of base predicates, including a binary equality symbol, each having a denotational semantics . Each assertion can have free term variables, and we write Γ ⊢ when is well-typed by the typing context Γ. If this holds, we can define as the naturally defined truth value, see Fig. 9. Judgments of the logic are of two forms: • The first kind of judgments derive assertions, are said to be logical judgments, and have the shape Γ | Φ ⊢ , where Γ is a typing context, Φ is a finite set of assertions, and is an assertion. When we write Γ | Φ ⊢ , then Φ and are always assumed to be well-typed under Γ. Apart from well-typedness, the assertions Φ and can be any assertions of the language, and as such talks about specific terms only through the base predicates. The judgement Γ | Φ ⊢ is said to be valid if for every ∈ Γ , if Φ then . Note that validity is well-defined, due to the well-typedness condition on Φ and .
• The second kind of judgments derive assertions about a specific program , and are called program judgments. They have the following form: Here, as above, Γ is a typing context and Φ is a set of assertions. Now however, a term is put in evidence such that has type in the context Γ (i.e., Γ ⊢ : holds) and talks about through a distinguished variable r (i.e., Γ, r : ⊢ ). For brevity, as with logical judgements we tacitly assume that all logical assertions occurring in program judgements are well-typed. Such a program judgement is valid if for every ∈ Γ , if Φ then ;r↦ → . One can give formal rules for the the logical judgments in a standard way, once axioms for the basic predicates are identified [Aguirre et al. 2017]. The soundness of the obtained formal system with respect to the aforementioned set-theoretic semantics, i.e. that derivability implies validity, can be proved by induction on derivations.
But how about program judgments? Following the literature [Aguirre et al. 2017], some syntaxdirected rules can indeed be given which remain valid under our interpretation. However, some care is required for recursive definitions. The complete system is given in Fig. 11. Here, we employ the usual convention that typing environments are juxtaposed only when they do not share any name, e.g., Γ; : is defined only when does not occur in Γ. As mentioned above, all judgements occurring in the rules are supposed to be well-typed.
To reason in an inductive style about recursive functions that converge to, rather than compute a result, we require that the assertion attached to this function through EHOL is Scott-admissible. Briefly, Scott-admissiblity simply states that an assertion holds for the bottom element of the underlying domain, and that it is closed under upper limits. A way to enforce Scott-admissibility consists of restricting to the class of assertions such that Γ ⊢ pos( ) is derivable by the rules in Figure 10. These assertions are called ≤-positive. Examples of ≤-positive assertions include r ≤ , stating that the result of a computation is bounded from above by , for an expression in which r does not occur free.
We now establish the soundness of the logic w.r.t. the denotational semantics of the language. Γ ⊢ : For an informal explanation and intuitions about EHOL, we now conclude this section with an analysis of the running examples.

Examples
Coupon collector. Let us first return to the coupon collector function, whose translated version is given in Figure 1b. For brevity, we consider the slightly simplified variant couponsCost that elides the continuation, which, removing some syntactic sugar, reads as follows: .(letrec collectCost = if ⊆ then 0 else 1 + ∈ 1 /| | * collectCost ( :: )) · [ ] The most important step in the analysis lies in the treatment of the auxiliary recursive function collectCost : List(C) → Real + , which we resolve as follows. Here, we will exploit that Ð the list of coupons drawn so far Ð consists only of coupons from the overall list of coupons. We express this as a predicate ⊆ , conceiving and as sets. What we would now like to prove is that for any such , the result of collectCost · is bounded by a function in . Let us denote this function by ( ); the concrete definition of is deferred to the end of this paragraph. In other words, we would like to verify: : for the body of collectCost. For brevity, let us omit types in universal quantification. Observe that r · ≤ ( ) is ≤-positive, and so by Rule (Letrec) this judgment boils down to where Γ ≜ : List(C); : List(C). In effect, we should thus prove that evaluating (the body of) collectCost on yields indeed a result bounded by ( ), where we may assume that this property holds for any recursive call on ⊆ . Let us collect in Φ the two logical premises of this judgment, and proceed with Rule (Case) on the desugared-conditional. Here, first one verifies that, for the guard, Γ | Φ ⊢ ⊆ : Bool | r = ⊆ , holds. In the treatment of the then-and else-branches, we can now assume true = ⊆ and false = ⊆ , respectively. Let us denote these two facts by ⊆ and ⊈ for brevity. Concerning the two branches, it is standard to check Γ | Φ; ⊆ ⊢ 0 : Real + | r ≤ 0 Γ | Φ; ⊈ ⊢ 1 + ∈ 1 /| | * collectCost ( :: ) : Real + | r ≤ 1 + ∈ 1 /| | * ( :: ) .
Coming to a concrete bound, let us define ( ) ≜ | | * (| \ |), where ( ) = =1 1 / denotes the -th harmonic number, with the convention that (0) = 0. While the first constraint can be immediately discharged, note that the latter simplifies to Now observe that, when ∈ is already in , then (| \ :: |) is simply (| \ |). On the other hand, when is a newly collected coupon, exploiting that the set of collected coupons is a proper subset of all coupons under the given assumptions, then (| \ :: It is thus the case that the above constraint is equivalent to Using the identity (| \ |) = (| \ | − 1) + 1 | \ | this last constraint is now not difficult to discharge.
Observe that couponsCost is nothing else than couponsCPS with the continuation specialized to the constant-zero function. With Theorem 4.15, the so derived bound now transfers to the probabilistic source program coupons from Figure 1a. Notice that this bound, which lies in (| | * log(| |)), is precise.
Higher-order random walks. Let us now turn our attention to the higher-order combinator function walk from Example 3.1, whose CPSed version is given in Example 4.7. As usual for many higher-order combinators and not unique to probabilistic programs, its (expected) cost Ð here the number of iterations Ð is impossible to judge by looking at walk alone: the cost depends crucially on the supplied predicate p : Int → Bool used to terminate the walk, and the function f : Int → Int picking the next position in terms of the current one. Indeed, if we instantiate walk for instance to geo, as we have done in Example 3.1, then the expected cost becomes constant, while if we instantiate walk as in randomWalk p it can even become unbounded.
Is it then even conceivable to reason about this function compositionally? With EHOL, we can answer this question in the affirmative. The logic is expressive enough to articulate the interactions between functions and its arguments in the necessary granularity on the CPSed terms, even at higher-order types. Let us illustrate this with a single EHOL proof on the CPSed term walkCPS of walk given in Example 4.7. As a second step, we then show how the derived bound can be instantiated to reason about the expected cost of geo and randomWalk, despite that their complexity vastly differs.
For concrete parameters p and f, let us express the expected cost of walk as a function ( ) in terms of the current integer position. Let us first assume that f and p are non-probabilistic, and let us denote by an assertion ( ) the Boolean value of p · within EHOL. Then ( ) should, in the case the else-branch is executed (i.e., ¬ ( )), bind the cost (f · ) + 1 of the recursive call plus one for the current iteration. As the cost transformer translates f · to a CPSed term fCPS · · , with the cost of its continuation Ð in our case that of the recursive call Ð this amounts to saying that fCPS should satisfy The universally quantified variable refers to the cost of the recursive call and is therefore by assumption bounded by . Let us now consider the general case. So far, in our argumentation we have neglected that the then-branch of the conditional incurs a cost depending on the supplied argument : Int → Real + . Second, the guard p may be probabilistic, hence the two branches of the conditional are potentially only executed with a certain probability and, conclusively, their expected cost could be much higher than the expected cost ( ), i.e., the value of walkCPS . Therefore, let us introduce two functions ( ) and ( ) to denote bounds for the then-and else-branch, respectively. First, we set up to indeed bind , via This formula ties the assertion ( ) to the possibly sampled Boolean outcome within the conditional continuation, whose bound is assumed to be of the shape as just derived. Finally, this assertion also relates the outcome of walkCPS's body to the bounding function ( ).
It is now standard to check that the assertions on the arguments yield that walkCPS · · · · is bounded by ( ), i.e., for the type of walkCPS, is valid.

EMBEDDING OF THE ERT CALCULUS
In Section 2, we have motivated the use of a CPS translation for reasoning about expected costs by coupling Rosendahl's program transformation approach with ideas from the expected runtime transformer of , itself presented in the form of a weakest pre-expectation calculus for reason about the expected runtime of randomized algorithms written in an imperative probabilistic language. In this section, we are going to show how the ert-calculus can be embedded into our formalism by way of a state-passing monad, thus witnessing that our approach strictly extends upon this sound and complete methodology.
The imperative language under consideration is based on Dijkstra's Guarded Command Language, additionally equipped with sampling operations. More specifically, the underlying language of programs (in the style of IMP, see e.g. [Winskel 1993]) includes assignments, sequencing, conditionals, and loops. Variable assignments and guards are however allowed to be probabilistic. A full list of program commands C can be seen in the leftmost column of Figure 12, where stands for a probabilistic expression and for a probabilistic guard. All variables are global in IMP, and without any loss of generality we can assume that any program value : Val is drawn from a discrete but otherwise arbitrary domain, while program states : Val n map the program variables 1 , . . . , to their content : Val.
The second column of Figure 12 gives a functional interpretation of imperative commands C within our source language, as a probabilistic term ⊢ C : Val n → Val n mapping initial states to final ones. From an operational perspective, empty and skip are no-ops. Whereas empty incurs no cost, skip incurs a runtime cost of one by definition. The command halt signals an abnormal termination and is interpreted as the non-terminating function Ω = letrec = ( · ). Probabilistic assignment :≈ assigns to a value sampled from the (discrete) distribution expression . Within the function interpretation of such assignments, is represented as a sampling primitive p : Val n → Val ∈ D, a primitive function upd i : Val n × Val → Val n is used to update the content of with the value sampled value, and a runtime cost of one is incurred. The interpretation of command composition, conditionals and while-loops is standard. Since guards can be probabilistic, such expressions are represented via probabilistic primitives p : Val n → Bool ∈ D, as in the case of assignments.
In the rightmost column of Figure 12 we draw the value translation on the functional interpretation of commands C. We have simplified the presentation by removing administrative redexes, and exploiting that halt † = Ω † is semantically equivalent to the constant zero function.
Correctness of the Embedding. The just described embedding can be proved correct by relating it to the so-called expected runtime transformer as defined by Kaminski et al. Let T denote the set of runtimes, i.e., the set of functions from program states to R +∞ . The expected runtime transformer expresses the expected runtime of any program C by means of a transformer ert[C] : T → T on runtimes. In particular, ert[C] applied to the constant zero function yields the expected runtime of C. The following captures the fact that what we do in Figure 12 is not different from ert[C], thus correct.
Proposition 6.1. For all imperative programs C and ⊢ : Val n → Real + ,

DISCUSSION
Expectations and AST. We have showed that the expected cost of any expression can be obtained by applying the denotational interpretation of its CPS transform to the continuation .0. However, the usefulness of the CPS translation is not limited to deriving expected costs. In particular, it can be used for computing the (pre-)expectation of any expression, as captured by the following result. As an example, the CPS translation can be used to reason about the probability of termination. Specifically, Theorem 7.1 instantiated with being set to .1 boils down to saying that the semantics of ect[ ] { } precisely gives the probability of convergence of . Giving an estimation to the probability of termination and to the expected cost are well known to be highly undecidable problems having incomparable recursion-theoretic statuses, the former being Π 2 0 -complete and the second being Σ 2 0 -complete [Kaminski and Katoen 2015]. Type-based Verification. The formal system of higher-order logic we introduced in Section 5 is a sound methodology to derive upper bounds on the expected cost of higher-order randomised programs via a CPS translation, as witnessed by Theorem 4.15 and Theorem 5.1. In EHOL, types and assertions are separated, and play different roles: the former plays the usual role of guaranteeing the absence of type errors, without providing any guarantee on the actual I/O behavior of terms, while the latter can be employed to specify such constraints. A different approach is that of refinement types, in which specifications are embedded into types. Since refinement types are well-known to be interpretable in HOL [Aguirre et al. 2017], the obtained type systems would arguably not add anything to HOL in terms of expressive power, although taking the form of a proper type system. Continuous Distributions. The CPS transformation we consider in this paper takes as input terms of a probabilistic -calculus in which sampling can be performed on discrete distributions, only. Generalizing what we do to transformation in which, on the other hand, we can also perform sampling from continuous distributions, would be extremely interesting as a first step towards moving towards Bayesian programming languages. The main obstacle, in this sense, consists in endowing the target language with an operator for integration, itself necessary for interpreting the expectation of programs which sample from continuous distributions.
Applicability. While we have shown that the expected cost of the source program is precisely reflected within the target program, and thereby our CPS translation constitutes not only a sound but also complete methodology for reasoning about expected costs, our program logic EHOL has been proven only sound for deriving upper-bounds. On the other hand, we conjecture that EHOL is also complete relative to the underlying programming logic, thereby further witnessing the strength of our overall approach. A formal proof, though, is beyond the scope of this work.
Orthogonal, it would also be interesting to implement EHOL in the style of an interactive theorem prover, and couple this implementation with the CPS translation. Such an implementation would greatly improve upon the applicability of our approach. While this is clearly feasible, a further step would be to incorporate some form of automatism for deriving upper-bounds. At least for programs whose cost analysis is not relying on too complicated functional properties, it seems feasible to incorporate template based approach resting on SMT-solvers Ð the pre-dominant approach underlying automated tools (see e.g. [Avanzini et al. 2015;Wang et al. 2020]). Ideally, one would arrive at a semi-automated analysis tool, where simple proof steps are automatically discharged and the user can focus on the non-trivial aspects of the cost analysis.

RELATED WORK
This is definitely not the first paper about randomised higher-order computation. Starting from the pioneering work by Saheb-Djaromi [Saheb-Djahromi 1978], the field has developed at a relatively slow pace, mainly due to the intrinsic difficulties one faces when giving denotational semantics to such programs [Jung and Tix 1998]. Recently, satisfactory solutions for the problem have been devised [Ehrhard et al. 2014;Goubault-Larrecq 2019;Heunen et al. 2017], and also other challenges like termination and complexity analysis or program equivalence have been tackled.
The growing interest in Bayesian programming idioms such as Anglican [Tolpin et al. 2016], Church [Goodman et al. 2008], Hakaru [Narayanan et al. 2016], themselves functional languages, has also served as a motivation for the study of higher-order probabilistic programming languages. In these languages, programs are meant to embody probabilistic models rather than algorithms, and evaluating a program consists of applying inference algorithms to the underlying model. For all this to be useful, programs are required not only to sample from (various forms of) distributions but also to condition the result of sampling to the observed data. The vehicle lambda-calculus we consider here does not have any primitive for conditioning. Noticeably, program transformations, some of them reminiscent to ours [Ramsey and Pfeffer 2002], have been used to improve the performances of inference algorithms.
Continuation-passing style transformations [Danvy and Filinski 1992;Plotkin 1975] are a pervasive tool in program transformation and compiler construction [Appel 1991]. They are, in particular, very effective as a way to lift various forms of effects away from the underlying program [Filinski 1994], this way restoring purity, and facilitating program analysis and optimizations. The kind of CPS transformation we consider here is peculiar, as it is focused on probabilistic and cost effects. CPS transformations specifically tailored for randomised -calculi have already been considered [Dal Lago and Zorzi 2012], the underlying goal being the one of targeting a calculus in which the underlying reduction strategy does not matter. CPS transformations have already found applications in the context of Anglican and other Bayesian programming languages, where they serve as a way to implement Bayesian inference (see also [Ścibior et al. 2018]).
When, on the other hand, the underlying program has higher-order functions, the range of techniques currently available is much narrower and is essentially reduced to types. Although the kind of verification technique presented in this paper is substantially different, being based on program transformation, a comparison with type-based techniques is in order.
The recent works on expected cost analysis by way of linear dependent types [Avanzini et al. 2019a] and intersection types [Dal Lago et al. 2021] aim at giving very expressive type systems in which bounds on the expected cost of the typed programs can be derived. In the first case, we are talking about a system obtained by generalizing Dal Lago and Gaboardi's ideas [Dal Lago and Gaboardi 2011] to a probabilistic -calculus, obtaining a very expressive, although not relatively complete, methodology. The feasibility of type inference is not considered. In the second case, we are faced with a type system which is complete, but unsuitable for verification: as usual in intersection-type systems [Bucciarelli et al. 2003], the expressiveness in terms of the functions (as opposed to the computations) that can be captured is very low. In other words, typing a functional program requires, in general, giving a distinct type derivation for every possible input.
Notable also, in [Wang et al. 2020], the amortized cost analysis underlying resource aware ML [Hoffmann et al. 2012] has been suited to probabilistic programs. This work sets itself apart by having a fully automated inference machinery, differently from what we do here. The two particular instances of walk given in Example 3.1 lie within the scope of [Wang et al. 2020]'s methodology, when specialized to two first-order programs. However, depending on its functional arguments, the expected cost of walk can vary between constant, to linear, or even be infinite. To the best of our knowledge, the higher-order function walk itself is beyond the scope of any automated technique, so far. Within EHOL, as shown in Section 5, we are able to derive a parametric bounding function for the higher-order combinator, encompassing these two concrete instances. This makes our treatment of this example subtly different and more general than the one in [Wang et al. 2020].

CONCLUSION
In this paper, we studied how CPS program transformations can be employed in the setting of randomised computation, particularly as a technique for reducing the problem of estimating the expected cost of a randomised program to the one of analyzing the input-output behavior of its CPS counterpart. Along the way, we proved the introduced program transformation correct, and we showed how a formal system of unary higher-order logic soundly derives upper bounds to the output-value of deterministic programs obtained via our CPS transformation. This, in turn, can be lifted back to an upper-bound on the expected cost of the initial randomized program.
We see the idea of channeling the expected cost through the underlying continuation as a natural one, which could be useful also for other calculi. As an example, extending what we have done here to calculi with continuous distributions looks feasible. Another related but orthogonal direction consists of capturing a form of (soft) conditioning primitives akin to score or observe by way of CPS, this way going towards the inference machinery of languages like Anglican. Finally, how about generalizing all this to algebraic effects? This would rely on a generic notion of expectation, which is unfortunately lacking.