Simple Types for Probabilistic Termination

While the study of probabilistic computation can be traced to the 1950s [11], the first study of the probabilistic $\lambda$-calculus in particular is considered to be by Saheb-Djahromi in the late 70s [30]. In the near half century since, many variations on higher-order probabilistic computation have been considered [10, 12, 19, 20, 26, 29]. In recent years, perhaps due to the potential for applications in machine learning and modelling of probabilistic systems, the area has seen a return to popularity [5, 6, 16, 17, 24, 31]. An important computational phenomenon in its own right, the study of probabilistic choice can also provide a “foot in the door” for understanding how more general effects might manifest, leading for instance to the recent Functional Machine Calculus (FMC) as a confluent $\lambda$-calculus with effects [3, 18] that will play a central role in our development.

In this paper we consider the problem of probabilistic termination, the probability that a given reduction mechanism reaches the normal form of a term, a key consideration for probabilistic computation and the subject of significant recent attention [4, 7, 8, 15, 22]. ¹¹1Note that this objective is distinct from almost-sure termination: it considers exact probabilities, not those converging in the limit. Almost-sure termination is more commonly studied for iterative constructs [21, 27]; extending the lambda-calculus with an almost-surely terminating iterator is the subject of future work. Termination being one of the prime considerations of type systems in general, the question of type systems for probabilistic termination is pertinent [1, 7]. Our contribution in this paper is a new typing discipline for probabilistic termination, following the recent line of work on the probabilistic event $\lambda$-calculus [9] and the FMC. Their prime features are confluence for probabilistic computation and other effects, and the encoding of multiple reduction strategies within a single calculus.

One of the greatest challenges facing the study of probabilistic computation is confluence. In most variants the outcome of duplicating a probabilistic term is strategy dependent. Consider the instruction “write down the result of flipping a coin twice”: it is ambiguous whether “twice” refers to “write” or “flipping”, and the choice of interpretation changes the possible outcomes. In most of the literature results are therefore either restricted to a single strategy, such as call–by–value or call–by–name, or rely on a modified definition of reduction. This raises the question whether it is possible to have confluence for probabilistic computation, while expressing different strategies, and rewriting without restriction on contexts, properties which lend elegance to the $\lambda$-calculus. The probabilistic event $\lambda$-calculus [9] proposes a solution to this problem by decomposing a probabilistic sum $M\oplus N$ into a choice operation $MaN$, understood as a conditional “if $a$ then $M$ else $N$”, and a probabilistic generator $\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x192.png" id="S1.p3.m8.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}.P$, representing a coin toss whose outcome is bound to the boolean variable $a$ in the term $P$, which then determines the choice for $MaN$. When in argument position $\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x193.png" id="S1.p3.m12.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}.M$ acts as a wrapper, similar to thunking in call–by–push value [25] and the bang-calculus [14, 15], protecting the operator from evaluation. These factors combine to return confluence to the calculus, allowing for arbitrary evaluation strategies with an unrestricted $\beta$-reduction.

The probabilistic event $\lambda$-calculus ($\mathrm{𝖯𝖤}\mathrm{\Lambda }$) was introduced in [9] with a simple type system, corresponding to that on the lambda-calculus. This system ignored the probabilistic elements of the calculus, and thus gave little insight into the properties of this extension. In a deterministic calculus a type system provides various safety guarantees. These may be qualitative: termination, outputs, composability; or quantitative: run time, term size. In the probabilistic setting, however, it is natural to wonder what guarantees can be made, when the behaviour of a single term can vary between iterations. If, as in the type system mentioned, the probabilities are ignored, strong results can be obtained, albeit on a fairly uninteresting fragment of the calculus. Once probability is acknowledged by the type system the guarantees made become similarly qualified: probability of termination, almost-sure termination, expected run time. Here, we consider the first of these.

One proposed type system for the $\mathrm{𝖯𝖤}\mathrm{\Lambda }$ [1], labelled $\mathrm{C}{\lambda }_{\to }$, introduces counting quantifiers as a Curry–Howard correspondent to an intuitionistic counting propositional logic. These provide a mechanism to express “proportion of truth” by quantifying the number of satisfying assignments to a formula within a given model, in the way that existential and universal quantification may be understood via the existence of a satisfying assignment, respectively the satisfaction of all assignments. By taking the assignments to a formula to describe the branches of a probabilistic computation, counting quantifiers may be used to describe probability bounds. By this mechanism, $\mathrm{C}{\lambda }_{\to }$ provides a lower bound on the probability of head normalisation. However, as illustrated in [1], the bounds provided by $\mathrm{C}{\lambda }_{\to }$ are not tight, even in situations where this would be expected (see Example 8).

In this paper we present an alternative approach to the same problem, for the same calculus, using a different inspiration, to provide improved termination bounds. Deriving from the $\mathrm{𝖯𝖤}\mathrm{\Lambda }$, the FMC provides an additional feature that, to us, seemed crucial to a natural account of probabilistic termination via the type system. First, the “machine” in question is the (simplified) Krivine machine [23], whose evaluation is closely related to head normalisation. The FMC here adds an intriguing aspect: it introduces sequential composition and identity on the machine, where the latter, the imperative skip, provides a notion of successful termination, notably absent from the machine for standard $\lambda$-calculus. Moreover, this becomes the primary interpretation of types: a type derivation in the FMC is a proof that the machine successfully terminates. Our main question for this work was how to adapt this to capture probabilistic termination. The answer, described in Section 6, is an extended sequential probabilistic event $\lambda$-calculus $\mathrm{𝖲𝖯𝖤}\mathrm{\Lambda }$, with a type system $\mathrm{𝖲𝖯𝖤}{\mathrm{\Lambda }}^{\mathbb{Q}\Rightarrow }$ that naturally describes probabilistic termination of the machine, as well as probabilistic termination of head reduction.

The type system $\mathrm{𝖲𝖯𝖤}{\mathrm{\Lambda }}^{\mathbb{Q}\Rightarrow }$ for the extended sequential calculus reflects back onto a natural type system for the original probabilistic event $\lambda$-calculus, $\mathrm{𝖯𝖤}{\mathrm{\Lambda }}^{\mathbb{Q}\to }$, which gives probabilistic head normalization in the following way: types generalize simple types by replacing the base type with a probability. Formally,

where $p\in [0,1]\cap \mathbb{Q}$ is a rational number between zero and one inclusive. The intuition is that the base type for simple types, $o$, may be understood as signifying successful evaluation, even if it is uninhabited. After all, a constant base type such as for booleans or integers signifies the successful return of a corresponding value. This further matches the interpretation in the FMC, where the type $o$ is inhabited by skip, and corresponds to termination of the machine without producing a result. Our approach, then, is to replace certain termination with a probability of termination, replacing the base type $o$ with a probability $p$. We consider the striking simplicity and natural intuition of this approach one of our main contributions.

We recall the probabilistic event lambda-calculus $\mathrm{𝖯𝖤}\mathrm{\Lambda }$ from [9]. Assume countable sets of variables, ranged over by $x,y,z$, and of events, ranged over by $a,b,c$. The former are term variables, to be instantiated by terms of the calculus, and the latter are boolean variables, to be instantiated by $\top$ (true) or $\perp$ (false). The $\mathrm{𝖯𝖤}\mathrm{\Lambda }$ extends the $\lambda$-calculus with a generator $\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x194.png" id="S2.p1.m8.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}.M$, which flips a coin and binds the result ($\top$ or $\perp$) to $a$, and a choice or conditional $MaN$, which evaluates to $M$ if $a$ is true, and to $N$ otherwise. A traditional probabilistic sum of terms, $M\oplus N$, may be encoded as $\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x195.png" id="S2.p1.m17.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}.MaN$. Generators are normally fair, with equal probability for $\top$ or $\perp$, though on occasion we may need a biased generator $\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x196.png" id="S2.p1.m20.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}{}_p$ which chooses $\top$ with probability $p$, and $\perp$ with $1-p$.

The free variables and free events of a term $M$ are written $\mathrm{𝖿𝗏}(M)$ and $\mathrm{𝖿𝖾}(M)$ respectively. Substitution is written prefix: $\{N/x\}M$ is the capture-avoiding substitution of $N$ for $x$ in $M$. For an event $a$ we define two projection functions ${\pi }_{\top }^a$ and ${\pi }_{\perp }^a$, which apply the effect of instantiating $a$ with true and false respectively, to a term $M$.

We use the standard notions of context, head context, and applicative context to define the reduction relations. Note that a head context is of the form $\lambda x_1\mathrm{\dots }\lambda x_n.\{\}{M}_1\mathrm{\dots }{M}_m$ where $m$ and $n$ are potentially zero.

A probability $p,q$ is a rational number between $0$ and $1$ inclusive. Probabilistic reduction will return a multi-(sub-)distribution [2], a finite multiset of weighted terms $ℳ$ written as $[p_1\cdot M_1,\mathrm{\dots },p_n\cdot M_n]$ whose weight $|ℳ|={\sum }_{i\le n}{p}_i$ is (at most) one.²²2We use multi-distributions rather than distributions to accommodate the reduction measure for the proof of head normalization in Appendix A.2. For simplicity, we will refer to these as distributions, and we convert implicitly between terms $M$ and the singleton distribution $[1\cdot M]$. Multiset union is written $𝒮+𝒯$, and the empty multiset as $\mathrm{\varnothing }$. A distribution $ℳ$ is scaled to $pℳ$ by multiplying each weight in $ℳ$ by $p$. The underlying probability (sub-)distribution of $ℳ$, the finite function from terms to probabilities obtained by collecting like terms $p\cdot M$ and $q\cdot M$ as $(p+q)\cdot M$, is written $\lfloor ℳ\rfloor$.

The $\mathrm{𝖯𝖤}\mathrm{\Lambda }$ features a second notion of reduction, permutative reduction ${\text{<foreignobject height="2.9pt" overflow="visible" style="--fo\_width :0.72em;--fo\_height:0.29em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 4)" width="7.2pt"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x214.png" id="S2.p5.m2.g1nest" class="ltx\_graphics ltx\_img\_landscape" width="15" height="6" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}}_{𝗉}$ [9], which gives a more fine-grained evaluation of probabilistic sums. It is this reduction for which confluence is particularly significant. The effect of permutative reduction is to bridge the gap between the decomposed operators and $MaN$ and the standard probabilistic sum $M\oplus N$, encoded as $\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x216.png" id="S2.p5.m6.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}.MaN$, by internalizing the reduction of $\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x217.png" id="S2.p5.m7.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}.M$ to the sum of its two projections [9, Proposition 29]:

$$\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x218.png" id="S2.Ex7.m1.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}.M{\text{<foreignobject height="2.9pt" overflow="visible" style="--fo\_width :0.72em;--fo\_height:0.29em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 4)" width="7.2pt"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x219.png" id="S2.Ex7.m1.g2nest" class="ltx\_graphics ltx\_img\_landscape" width="15" height="6" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}}_{𝗉}\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x220.png" id="S2.Ex7.m1.g3nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}.({\pi }_{\top }^{a}M)a({\pi }_{\perp }^{a}M)(\text{if }a\in \mathrm{𝖿𝖾}(M)).$$

In this paper we will work with projective reduction, since we are interested in termination of head reduction. We will, on occasion, consider terms where probabilistic sums are of the traditional form $M\oplus N=\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x221.png" id="S2.p5.m8.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}.MaN$ with $a\notin \mathrm{𝖿𝖾}(M),\mathrm{𝖿𝖾}(N)$. As per the above, these are effectively the normal forms of permutative reduction.

Before introducing our probabilistic type system, we recall simple types for the $\mathrm{𝖯𝖤}\mathrm{\Lambda }$ [9].

Simple types ignore the probabilistic constructs of the calculus, generator and choice, requiring only that branches of a choice have equal types. This gives the expected result: typed terms are strongly normalizing, since every possible branch of the computation is typed. For probabilistic termination, we wish to capture that a given fraction of all branches of a computation, terminates – where our notion of termination is given by head normalization.

Our approach derives from the following idea: if the base type $o$ of simple types, even if not inhabited, denotes certainty of termination, then we may generalise this to probability of termination by replacing base types with arbitrary probabilities. This yields the following notion of types.

The intuitive meaning of, for example, assigning a term $M$ a type $A\to B\to p$ is: given inputs of type $A$ and $B$, $M$ terminates with probability at least $p$. The identity term $I=\lambda x.x$ may be assigned any type $p\to p$: given an input $N$ that terminates with probability $p$, the term $IN$ does so as well. The type system will include an axiom that any term, in particular a non-terminating one such as $\mathrm{\Omega }=(\lambda x.xx)(\lambda x.xx)$, may be assigned a termination probability of zero. This is expressed by a type $A_1\to \mathrm{\dots }\to A_n\to 0$: for any inputs $A_1$ through $A_n$, the term will terminate with probability at least zero.

Note that these types generalise simple types with a single, uninhabited base type $o$. A probabilistic system with multiple base types, say integers and booleans, would pair the return type with a probability, for instance an integer with $\frac{1}{2}$ probability, or a boolean with $\frac{1}{4}$ probability. The extension of the calculus with sequencing, in Sections 5 and 6, will give a more concrete account of how probabilities interact with return values and return types.

The term $\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x222.png" id="S3.p6.m1.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}.Ma\mathrm{\Omega }$ gives a fair probabilistic choice between $M$ and $\mathrm{\Omega }$. For the computation to be well-typed regardless of the choice, $M$ and $\mathrm{\Omega }$ should have the same input types, so that they can be applied to the same arguments. Hence, if $M$ has type $A\to B\to p$, we may choose $A\to B\to 0$ for $\mathrm{\Omega }$. Then the type for $\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x223.png" id="S3.p6.m10.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}.Ma\mathrm{\Omega }$ should be $A\to B\to \frac{1}{2}p$: given arguments of type $A$ and $B$, the computation chooses $M$ with probability $\frac{1}{2}$ and so terminates with probability at least $\frac{1}{2}p$.

These considerations motivate the shape of our probabilistic type system, with one further aspect to explain. An arbitrary generator term $\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x224.png" id="S3.p7.m1.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}.M$ reduces with a fair probability to either ${\pi }_{\top }^{a}M$ or ${\pi }_{\perp }^{a}M$, which may then terminate with different probabilities. However, using projections would mean the type system loses the property of being inductive on terms. We will instead record the assignment of a truth value to $a$ in an additional context $E$, that we call an event valuation. The type derivation then projects a term $MaN$ to $M$ or to $N$ according to the value of $a$ in the event valuation $E$.

The typing rules are syntax-driven, except for the $\mathrm{𝗅𝗈𝗐}$ rule to lower a given bound. The rule is not essential to the type system, since it is already implied in the meaning of types as giving a lower bound; but for the same reason, since it is implied, including it brings more clarity than omitting it. Note further that the typing rule $\mathrm{𝗀𝖾𝗇}$ assumes a fair coin toss for the generator , which gives the resulting probability of $\frac{1}{2}p+\frac{1}{2}q$. An unfair toss $\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x226.png" id="S3.p8.m5.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}{}_r$ with ratio $r$ would give a probability $rp+(1-r)q$.

We will discuss a number of aspects of our type system. First, as a particularly natural feature, observe that the rules $\mathrm{𝗏𝖺𝗋}$, $\mathrm{𝖺𝖻𝗌}$ and $\mathrm{𝖺𝗉𝗉}$ make it conservative over standard simply-typed $\lambda$-calculus – which, interestingly, is agnostic to the choice of base types.

Second, a key difference with the simple type system of Figure 1 is that probabilistic branching occurs in the generator rule, whereas for simple types it is the choice rule. This is due to aiming for head normalization instead of strong normalization. Consider the example term $\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x233.png" id="S3.p10.m1.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}.Ma(\mathrm{\Omega }aN)$. Head reduction projects it to $M$ and $N$, removing $\mathrm{\Omega }$, which will not be reduced. This is reflected in the probabilistic type system, where the branches of the generator typing rule project to $M$ and $N$ via the event valuation. The simple type system, reflecting strong normalization, would require also $\mathrm{\Omega }$ to be typed – which of course it cannot.

For terms of the form $M\oplus N=\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x234.png" id="S3.p11.m1.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}.MaN$ this difference is moot: both type systems branch similarly for this construct, to $M$ and $N$. This leaves as only distinction the generalisation of types themselves, from a single base type $o$ to probabilities $p$. In accordance with the meaning of a base type as the probability of termination, simple types are then recovered by restricting to base type $p=1$. This rules out the rules $\mathrm{𝗓𝖾𝗋𝗈}$ and $\mathrm{𝗅𝗈𝗐}$, assigning a zero-weighted type $\overline{A}\to 0$ and reducing the weight of a type. It is easy to observe that the remaining rules preserve the restriction $p=1$, to give the following proposition.

Our main result for the probabilistically-typed $\mathrm{𝖯𝖤}\mathrm{\Lambda }$ is that a type $\overline{A}\to p$ guarantees head normalization with probability at least $p$. Formally, this is stated by a head reduction to a distribution of which a proportion of at least $p$ is in head-normal form.

The result will follow directly from the corresponding Theorem 22 for the expanded probabilistic calculus with sequential composition, introduced in Section 5.

In this section we will give a close comparison with the type system $\mathrm{C}{\lambda }_{\to }$ of Antonelli, Dal Lago, and Pistone [1], and demonstrate that our approach gives tighter bounds on the probability of termination.

The first distinction between $\mathrm{C}{\lambda }_{\to }$ and $\mathrm{𝖯𝖤}{\mathrm{\Lambda }}^{\mathbb{Q}\to }$ is that the former uses indexed event variables $x_a^i$ for $i\in \mathbb{N}$ instead of events $a$. However, there is no formal need for this; since the indices $i$ are static, we may replace $x_a^i$ and $x_a^j$ for distinct $i$ and $j$ simply with distinct events $a$ and $b$. This simplification extends to the semantics. Probabilities in $\mathrm{C}{\lambda }_{\to }$ are given by boolean formulas $𝒷$ over the variables $x_a^i$, indicating a subset of the space ${(2^{\mathbb{N}})}^X$ where $X$ is a finite set of events. However, since the indices $i$ are fixed and bounded, it is sufficient to consider finite spaces $2^X$. The elements of this set are the event valuations $E$ with domain $X$, and a boolean formula $𝒷$ over $X$ indicates the set of event valuations ${⟦𝒷⟧}_X=\{E\in 2^X\mid E\vDash 𝒷\}$, where $E\vDash 𝒷$ is characterized syntactically as expected:

For a set $ℰ\subseteq 2^X$ the measure ${\mu }_X(ℰ)$ is given by

where $|S|$ denotes the size of a set $S$. Then $\mu (𝒷)$ is ${\mu }_X({⟦𝒷⟧}_X)$ where $X$ is the domain of $𝒷$. This coincides with the measure $\mu (𝒷)$ over ${(2^{\mathbb{N}})}^X$ in [1], as the latter makes no essential use of the infinity offered by $\mathbb{N}$.

The second difference is the syntax of types: $\mathrm{C}{\lambda }_{\to }$ introduces probabilities through counting quantifiers ${\mathrm{C}}^p$, where $\mathrm{𝖯𝖤}{\mathrm{\Lambda }}^{\mathbb{Q}\to }$ has probabilities as base types. Types are nevertheless isomorphic: $\mathrm{C}{\lambda }_{\to }$ types $𝔰$ are of the form ${\mathrm{C}}^p({𝔰}_1\to \mathrm{\dots }\to {𝔰}_n\to o)$, with a fixed outer counting quantifier, and map 1-to-1 onto $\mathrm{𝖯𝖤}{\mathrm{\Lambda }}^{\mathbb{Q}\to }$ types $A$ of the form $A_1\to \mathrm{\dots }\to A_n\to p$ by associating the probability $p$ instead with the consequent $o$. Formally, we encode types $𝔰$ and typing contexts $\mathrm{\Gamma }$ of $\mathrm{C}{\lambda }_{\to }$ into our setting as follows.

Having connected boolean formulas $𝒷$ to event valuations $E$, and $\mathrm{C}{\lambda }_{\to }$ types to $\mathrm{𝖯𝖤}{\mathrm{\Lambda }}^{\mathbb{Q}\to }$ types, we may state the following conservativity result of $\mathrm{𝖯𝖤}{\mathrm{\Lambda }}^{\mathbb{Q}\to }$ over $\mathrm{C}{\lambda }_{\to }$.

Two observations about probabilistic $\lambda$-calculi motivate the developments in the remainder of this paper. The first is the primary role of head reduction. It is well known that head normalization corresponds closely to evaluation on the Krivine Machine [23], and sometimes the machine gives a more natural model of what is being studied. The second is that probabilistic evaluation in $\lambda$-calculi needs to account for the difference between call–by–value (cbv) and call–by–name (cbn), to which end additional constructions are introduced, sometimes ad-hoc. The $\mathrm{𝖯𝖤}\mathrm{\Lambda }$ is an example, as is the separate consideration of a cbv- and a cbn-probabilistic sum by Faggian and Ronchi Della Rocca [16], while Antonelli, Dal Lago, and Pistone [1] add to the standard cbn-application a second cbv-application.

These observations prompted us to consider probabilistic termination from the perspective of the Functional Machine Calculus (FMC) [18], a $\lambda$-calculus with computational effects. Firstly, the Krivine Machine plays a central role in the FMC (indeed it is the “M” in “FMC”), while the FMC provides the machine with a new notion of successful termination, absent from the standard $\lambda$-calculus. It is then a natural question if and how this may be used to capture the probability of successful termination. Secondly, the FMC may express both cbn and cbv behaviour, with the cbn $\lambda$-calculus a fragment and the cbv $\lambda$-calculus encoded in the syntax. The need for ad-hoc constructs to control reduction behaviour is thus avoided.

The Krivine Machine, simplified by replacing environments with substitution, evaluates a $\lambda$-term in the presence of a stack of input terms. An abstraction $\lambda x.M$ pops the top off the stack, say $N$, and continues as $\{N/x\}M$, while an application $MN$ pushes its argument $N$ and continues as $M$. A $\lambda$-term may thus be viewed as a language of instruction sequences for this machine: application–push, abstraction–pop, variable–execute.

The FMC then extends the $\lambda$-calculus with sequential composition $M;N$ and its unit, the imperative skip $\star$, with the expected semantics: concatenation of machine instructions and the empty instruction. As in models of imperative languages, skip indicates successful termination of the machine. This gives a fragment called the sequential $\lambda$-calculus.

We adopt these modifications in the $\mathrm{𝖯𝖤}\mathrm{\Lambda }$ to give the sequential probabilistic event $\lambda$-calculus ($\mathrm{𝖲𝖯𝖤}\mathrm{\Lambda }$), defined below. Following [18] we render abstraction as $⟨x⟩.M=\lambda x.M$ and application as $[N].M=MN$ to emphasise the machine behaviour of pop and push, retaining the standard syntax as a shorthand. In particular, the new notation clarifies the interaction between push and sequencing: the following three terms are equivalent, rendered first in standard notation and second with prefix application.

The full FMC further generalises to a machine with multiple independent stacks, addressed by a set of locations, in which pop and push are then parameterised to operate on the corresponding stack. This allows us to encode the effects of mutable higher-order store, input/output, and indeed probabilistic computation: the generator $\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x241.png" id="S5.p6.m1.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}.M$ of the $\mathrm{𝖯𝖤}\mathrm{\Lambda }$ is, in the FMC, an abstraction $\mathrm{𝗋𝗇𝖽}⟨a⟩.M$ parameterised to draw from a stream of random values labelled $\mathrm{𝗋𝗇𝖽}$. The $\mathrm{𝖲𝖯𝖤}\mathrm{\Lambda }$ is thus a fragment of the FMC with two locations.

Prefixing binds tighter than sequencing, $[N].M;P=([N].M);P$, and sequencing associates right, $M;N;P=M;(N;P)$. Projections and contexts extend to the $\mathrm{𝖲𝖯𝖤}\mathrm{\Lambda }$ as below; head contexts and applicative contexts are as for the $\mathrm{𝖯𝖤}\mathrm{\Lambda }$.

The interaction between sequentiality and the $\lambda$-calculus is governed by the following sequencing reduction rules. These make sequential composition right-associative, and let the prefixing of push, pop, and the generator propagate past it (as in a standard list concatenation algorithm). The result is to make the first such action on the abstract machine the leading construct.

The sequencing relation ${\text{<foreignobject height="2.9pt" overflow="visible" style="--fo\_width :0.72em;--fo\_height:0.29em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 4)" width="7.2pt"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x250.png" id="S5.p8.m2.g1nest" class="ltx\_graphics ltx\_img\_landscape" width="15" height="6" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}}_{\sigma }$ is given by closing these rules under all contexts $C$, and head sequencing ${\text{<foreignobject height="2.9pt" overflow="visible" style="--fo\_width :0.72em;--fo\_height:0.29em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 4)" width="7.2pt"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x251.png" id="S5.p8.m4.g1nest" class="ltx\_graphics ltx\_img\_landscape" width="15" height="6" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}}_{\sigma 𝗁}$ by closing under head contexts $H$ only. The $\beta$-reduction rule in $\mathrm{𝖲𝖯𝖤}\mathrm{\Lambda }$ notation is as below left, with ${\text{<foreignobject height="2.9pt" overflow="visible" style="--fo\_width :0.72em;--fo\_height:0.29em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 4)" width="7.2pt"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x252.png" id="S5.p8.m8.g1nest" class="ltx\_graphics ltx\_img\_landscape" width="15" height="6" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}}_{\beta }$ given by closing under all contexts and ${\text{<foreignobject height="2.9pt" overflow="visible" style="--fo\_width :0.72em;--fo\_height:0.29em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 4)" width="7.2pt"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x253.png" id="S5.p8.m9.g1nest" class="ltx\_graphics ltx\_img\_landscape" width="15" height="6" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}}_{\beta 𝗁}$ by closing under head contexts. Projective reduction, below right, is as previously.

$$[N].⟨x⟩.M{\text{<foreignobject height="2.9pt" overflow="visible" style="--fo\_width :0.72em;--fo\_height:0.29em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 4)" width="7.2pt"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x254.png" id="S5.Ex19.m1.g1nest" class="ltx\_graphics ltx\_img\_landscape" width="15" height="6" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}}_{\beta }\{N/x\}MH\{\text{<foreignobject height="10.1pt" overflow="visible" style="--fo\_width :0.79em;--fo\_height:1.01em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 14)" width="7.9pt" color="\#CC0000"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x255.png" id="S5.Ex19.m1.g2nest" class="ltx\_graphics ltx\_img\_portrait" width="15" height="19" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}.M\}{\text{<foreignobject height="2.9pt" overflow="visible" style="--fo\_width :0.72em;--fo\_height:0.29em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 4)" width="7.2pt"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x256.png" id="S5.Ex19.m1.g3nest" class="ltx\_graphics ltx\_img\_landscape" width="15" height="6" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}}_{\pi }[\frac{1}{2}\cdot H\{{\pi }_{\top }^{a}M\},\frac{1}{2}\cdot H\{{\pi }_{\top }^{a}M\}]$$

Head reduction ${\text{<foreignobject height="2.9pt" overflow="visible" style="--fo\_width :0.72em;--fo\_height:0.29em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 4)" width="7.2pt"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x257.png" id="S5.p8.m10.g1nest" class="ltx\_graphics ltx\_img\_landscape" width="15" height="6" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}}_{𝗁}$ is the union of all three head relations:

$${\text{<foreignobject height="2.9pt" overflow="visible" style="--fo\_width :0.72em;--fo\_height:0.29em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 4)" width="7.2pt"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x258.png" id="S5.Ex20.m1.g1nest" class="ltx\_graphics ltx\_img\_landscape" width="15" height="6" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}}_{𝗁}={\text{<foreignobject height="2.9pt" overflow="visible" style="--fo\_width :0.72em;--fo\_height:0.29em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 4)" width="7.2pt"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x259.png" id="S5.Ex20.m1.g2nest" class="ltx\_graphics ltx\_img\_landscape" width="15" height="6" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}}_{\beta 𝗁}\cup {\text{<foreignobject height="2.9pt" overflow="visible" style="--fo\_width :0.72em;--fo\_height:0.29em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 4)" width="7.2pt"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x260.png" id="S5.Ex20.m1.g3nest" class="ltx\_graphics ltx\_img\_landscape" width="15" height="6" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}}_{\sigma 𝗁}\cup {\text{<foreignobject height="2.9pt" overflow="visible" style="--fo\_width :0.72em;--fo\_height:0.29em;--fo\_depth :0em;" transform="matrix(1 0 0 -1 0 4)" width="7.2pt"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x261.png" id="S5.Ex20.m1.g4nest" class="ltx\_graphics ltx\_img\_landscape" width="15" height="6" alt="[Uncaptioned image]" style="width: 15px; height: unset; max-width: 100\%"></span></span></foreignobject>}}_{\pi }.$$

We round off by observing the shape of head-normal forms, assuming no free event variables.

Types for the sequential $\lambda$-calculus are of the form below, with the meaning: given an input stack of terms typed by $A_1$ through $A_n$, the machine will terminate successfully and return a stack with types $B_1$ through $B_m$.

For the $\mathrm{𝖲𝖯𝖤}\mathrm{\Lambda }$, we parameterize this with the probability of successful termination.

There are no base types: their rôle is subsumed by types with empty vectors $(\stackrel{p}{\Rightarrow })$. Observe that because stacks are last-in-first-out, the identity term on two elements is $⟨x⟩.⟨y⟩.[y].[x].\star$, i.e. with the order of $x$ and $y$ reversed between popping and pushing. We match this reversal in types, and assign this term the type $AB\stackrel{}{\Rightarrow }BA$. Since we want identity types to be of the form $\overline{A}\stackrel{}{\Rightarrow }\overline{A}$, in a type $\overline{A}\stackrel{p}{\Rightarrow }\overline{C}$ we consider the antecedent type vector $\overline{A}$ to be reversed, i.e.

Probabilistic $\mathrm{𝖯𝖤}\mathrm{\Lambda }$-types embed into sequential types by $\overline{A}\to p=\overline{A}\stackrel{p}{\Rightarrow }\epsilon$. With this identification, for $\mathrm{𝖯𝖤}\mathrm{\Lambda }$-terms and -types the two type systems coincide.

Every type is inhabited by a closed term. For a type $A$, define the zero term $0_A$ as follows: for $A=B_1\mathrm{\dots }{B}_m\stackrel{p}{\Rightarrow }{C}_1\mathrm{\dots }{C}_n$,

To us, what stands out about our approach is the simplicity and the natural intuition of our type system. This manifests in the transparent reasoning in our proofs, which despite using deep techniques such as abstract reducibility, give a direct and clear connection between types, machine behaviour, and reduction.

Compared with the approach in [1], the simplicity of our approach manifests in several advantages. First is to avoid the need for counting quantifiers, associating probabilities instead with base types, and the use of simple event valuations over boolean formulas. Second, it is clear that the expression of both call–by–name and call–by–value behaviour is an essential ingredient for a probabilistic calculus. We eschew the introduction of ad-hoc constructs, relying instead on a principled interpretation of cbv via sequential composition. Finally, where the main example [1, Example 6.2] requires intersection types to produce the exact bound, our approach does so directly in Example 8, while morally remaining within the realm of simple types, and strictly improving on the bounds provided by $\mathrm{C}{\lambda }_{\to }$.