Prerequisites. Direct starred prerequisites: chapter 57. No later core chapter depends on this route.
Walk down a list, and at each element flip a fair coin: on heads stop and return 𝗍𝗍; on tails pay one unit and continue. In the notation of the system card below this is 𝖻𝖾𝗋𝗇𝗈𝗎𝗅𝗅𝗂lst=𝗆𝖺𝗍𝖼𝗁lst𝗐𝗂𝗍𝗁[]⇒𝖿𝖿∣ℎ𝑑::𝑡𝑙⇒𝖿𝗅𝗂𝗉12{H↪𝗍𝗍∣T↪𝗍𝗂𝖼𝗄1;𝖻𝖾𝗋𝗇𝗈𝗎𝗅𝗅𝗂𝑡𝑙}. On a list of length 𝑛, the worst run pays 𝑛: every flip may come up tails. The expected payment is different. Element 𝑘 is reached only if the first 𝑘−1 flips were tails, which has probability 2−(𝑘−1), and it is charged only if flip 𝑘 is also tails; so 𝔼[cost]=𝑛∑𝑘=12−𝑘=1−2−𝑛<1. The bound 1 holds for every 𝑛 and is approached as 𝑛 grows. A worst-case analysis reports 𝑛; the truth is bounded by a constant.
The gap is not repaired by replacing each branch cost with its numerical expectation. In 𝖻𝖾𝗋𝗇𝗈𝗎𝗅𝗅𝗂 the tails branch pays 1 and then pays whatever the recursive call pays, so “the expected cost of this statement” is not a number available before the analysis of the rest of the program. What is available is a quantity assigned to the data: a potential that the program carries and spends. The chapter’s obstruction is therefore to make potential flow through a distribution over successor states rather than through a single successor, and to keep divergence visible in the soundness statement, since a probabilistic program may diverge with positive probability and still have finite expected cost.
The calculus is Wang–Kahn–Hoffmann’s linear pRaML core, frozen here. Types are 𝜏::=𝟏∣𝖻𝗈𝗈𝗅∣𝗅𝗂𝗌𝗍(𝐴)∣prob{𝑞H;𝑞T}∣arr(𝐴;𝐵),𝐴,𝐵::=⟨𝜏,𝑞⟩(𝑞∈ℚ≥0), so a potential-annotated type is a type paired with a nonnegative rational constant, and a list type 𝗅𝗂𝗌𝗍(⟨𝜏,𝑝⟩) carries 𝑝 units of potential per element. Expressions are variables, 𝗍𝗋𝗂𝗏, 𝗇𝗂𝗅, cons, list matching, 𝗅𝖾𝗍, application, 𝖿𝗎𝗇, 𝗌𝗁𝖺𝗋𝖾, 𝗍𝗂𝖼𝗄{𝑞}, the probability value 𝗉𝗋𝗈𝖻{𝑝} for rational 𝑝∈[0,1], the probabilistic branch 𝖿𝗅𝗂𝗉{𝑒1;𝑒2}(𝑝), and the branch on a stored probability 𝖿𝗅𝗂𝗉𝖲(𝑥;𝑒1,𝑒2). The potential of a value is Φ(𝑣:⟨𝜏,𝑞⟩)=𝑞+Φ(𝑣:𝜏),Φ([𝑣1,…,𝑣𝑛]:𝗅𝗂𝗌𝗍(𝐴))=∑𝑖Φ(𝑣𝑖:𝐴),Φ(𝗉𝗋𝗈𝖻(𝑝):prob{𝑞H;𝑞T})=𝑞H𝑝+𝑞T(1−𝑝), and Φ(𝑉:Γ)=∑𝑥∈dom(Γ)Φ(𝑉(𝑥):Γ(𝑥)) for an environment 𝑉 with 𝑉:Γ. The typing judgment Γ;𝑞⊢𝑒:𝐴 reads: in context Γ with 𝑞 additional units of constant potential, 𝑒 has potential-annotated type 𝐴. This is not the discrete pPCF of chapter 171, and no theorem of that chapter is imported here.
From chapter 172 this chapter uses 𝖯𝖬𝖪-bind and 𝖯𝖬𝖪-lim: subprobability measures, bind, and the limit facts proposition 172.24, proposition 172.25, together with example 172.26 for finite rational mixtures. All distributions below are over a countable set of pairs, so every integral is a sum. It uses no quasi-Borel structure, no program logic, and no inference transformation.
The deterministic potential method assigns to each state 𝑆 a nonnegative number Φ(𝑆) and requires, for each operation 𝑜 with successor state 𝑆′, Φ(𝑆)≥cost(𝑆,𝑆′)+Φ(𝑆′).(1) Summing (1) along an execution telescopes: the initial potential bounds the total cost. When 𝑜 produces a distribution over successors, the only formula that keeps the telescoping property is obtained by taking the expectation on the right: Φ(𝑆)≥𝔼𝑆′∼𝑜(𝑆)[cost(𝑆,𝑆′)+Φ(𝑆′)]=𝔼𝑆′∼𝑜(𝑆)[cost(𝑆,𝑆′)]+𝔼𝑆′∼𝑜(𝑆)[Φ(𝑆′)].(2)
Suppose (2) holds for 𝑜 at 𝑆, and for 𝑜′ at every 𝑆′ in the support of 𝑜(𝑆). Then Φ(𝑆)≥𝔼𝑆′∼𝑜(𝑆),𝑆″∼𝑜′(𝑆′)[cost(𝑆,𝑆′)+cost(𝑆′,𝑆″)]+𝔼𝑆′∼𝑜(𝑆),𝑆″∼𝑜′(𝑆′)[Φ(𝑆″)].
Proof. Substitute the hypothesis for 𝑜′ into the second summand of (2) and use linearity of expectation over the finite mixture, which is example 172.26: 𝔼𝑆′[Φ(𝑆′)]≥𝔼𝑆′[𝔼𝑆″[cost(𝑆′,𝑆″)]+𝔼𝑆″[Φ(𝑆″)]], and the iterated expectation of a nonnegative quantity over the composite is the expectation over the product, by lemma 172.19. ◻
The typing rules realize (2) syntactically. Two of them carry the whole probabilistic content.
Write Γ▹(𝑝×Γ1,(1−𝑝)×Γ2) for the sharing relation that splits the per-element potential of every binding in Γ into the two branches with the displayed weights, so that Φ(𝑉:Γ)=𝑝Φ(𝑉:Γ1)+(1−𝑝)Φ(𝑉:Γ2).(3) Then
The equation 𝑞=𝑝𝑞1+(1−𝑝)𝑞2 is (2) for the constant part of the potential and the sharing relation is (2) for the part carried by the data. Neither is an average of costs: the costs 𝑞1,𝑞2 are themselves the potentials required by the branches, determined by the analysis of those branches.
Derive the typing 𝖻𝖾𝗋𝗇𝗈𝗎𝗅𝗅𝗂:⟨𝗅𝗂𝗌𝗍(⟨𝜏,0⟩),1⟩⟶⟨𝖻𝗈𝗈𝗅,0⟩, where the list carries no potential per element and one constant unit is available per call. At the branch, the heads side returns 𝗍𝗍 and needs 𝑞1=0; the tails side pays one tick and then calls 𝖻𝖾𝗋𝗇𝗈𝗎𝗅𝗅𝗂 again, which needs one unit, so 𝑞2=1+1=2. The rule L:Flip requires 𝑞=12⋅0+12⋅2=1, the constant available. The derived bound on the expected cost is therefore 1, independently of the length of the list; by the opening calculation the true expected cost is 1−2−𝑛, so the bound is attained in the limit.
Let 𝗋𝖽𝗐𝖺𝗅𝗄 consume a list of probabilities, paying one tick per iteration, and on heads at probability 𝑝 push two new probabilities 1/5,2/5 onto the list while on tails pop the head. The derivable typing is 𝗋𝖽𝗐𝖺𝗅𝗄:⟨𝗅𝗂𝗌𝗍(prob{5;0}),1⟩⟶⟨𝟏,0⟩, whose potential on the argument [𝑝1,…,𝑝𝑛] is Φ([𝑝1,…,𝑝𝑛])=𝑛+∑1≤𝑖≤𝑛5𝑝𝑖, one unit per element for the tick and 5𝑝𝑖 for the expected future work that the 𝑖-th flip may create. On the argument [1/5,2/5] this is 2+5⋅15+5⋅25=2+1+2=5. The program may fail to terminate — the head branch lengthens the list — and the bound is finite anyway; section 177.3 is where that combination is made legitimate.
★★☆ Replace L:Flip by the rule that requires 𝑞≥max(𝑞1,𝑞2) and show that it is sound but derives the bound 2 for 𝖻𝖾𝗋𝗇𝗈𝗎𝗅𝗅𝗂. Then replace it by 𝑞≥min(𝑞1,𝑞2) and exhibit a program for which the resulting system derives a false bound.
A soundness proof must compare a typing derivation with the aggregate behavior of all runs. The trace semantics describes one run at a time, which is the wrong shape for that comparison; the following failed attempt shows what has to be repaired.
The judgment 𝑉;𝜎⊢𝑒⇓𝑝𝑣∣𝑞 says that under environment 𝑉, with 𝜎 the finite sequence of coin outcomes consumed, 𝑒 evaluates to 𝑣 with net cost 𝑞, and that the outcome sequence 𝜎 has probability 𝑝. Set [[𝑒]]⇓𝑉(𝑣,𝑞)=∑{𝑝𝜎∣𝑉;𝜎⊢𝑒⇓𝑝𝜎𝑣∣𝑞}, a subprobability distribution over pairs, since infinite traces contribute nothing.
One would like an unindexed judgment 𝑉⊢𝑒⇒𝜇 with the rules 𝑉⊢𝗍𝗋𝗂𝗏⇒𝛿(⟨⟩,0),𝑉⊢𝑒1⇒𝜇1𝑉⊢𝑒2⇒𝜇2𝑉⊢𝖿𝗅𝗂𝗉{𝑒1;𝑒2}(𝑝)⇒𝑝⋅𝜇1+(1−𝑝)⋅𝜇2. The rules are true statements about terminating programs, but as an inductive definition they define nothing for a diverging one: a program whose recursive call is itself has no finite derivation, so the relation assigns it no distribution at all, not even the zero distribution. Since the whole point is to bound the expected cost of programs that may diverge, the definition must instead be approximated from below. The repair is an index: 𝑉⊢𝑒⇒𝑛𝜇 unfolds recursion at most 𝑛 times and assigns the zero distribution — later, the distribution concentrated on a dummy value — to anything deeper.
The judgment 𝑉⊢𝑒⇒𝑛𝜇 assigns to each expression a distribution over Val×ℚ≥0, by the rules 𝑉⊢𝗍𝗂𝖼𝗄{𝑞}⇒𝑛𝛿(⟨⟩,𝑞),𝑉⊢𝗉𝗋𝗈𝖻{𝑝}⇒𝑛𝛿(𝗉𝗋𝗈𝖻(𝑝),0),𝑉⊢𝑒1⇒𝑛𝜇1𝑉⊢𝑒2⇒𝑛𝜇2𝑉⊢𝖿𝗅𝗂𝗉𝖲(𝑥;𝑒1,𝑒2)⇒𝑛+1𝑝𝜇1+(1−𝑝)𝜇2 with 𝑉(𝑥)=𝗉𝗋𝗈𝖻(𝑝), together with the evident rules for the other constructs, in which the 𝗅𝖾𝗍 rule adds the costs of the two stages and the application rule decrements the index. At index 0 every expression receives the zero subdistribution. The two semantics agree in the limit: [[𝑒]]⇒𝑉=sup𝑛𝜇𝑛 where 𝑉⊢𝑒⇒𝑛𝜇𝑛, and this supremum exists by proposition 172.24, because the 𝜇𝑛 increase pointwise.
Proof of Theorem 177.10 — Soundness for terminating mass
Proof. Since [[𝑒]]⇒𝑉 is the supremum of the 𝜇𝑛 and all summands are nonnegative, proposition 172.24 reduces the claim to: for every 𝑛, if 𝑉⊢𝑒⇒𝑛𝜇 then Φ(𝑉:Γ)+𝑞≥∑(𝑣′,𝑞′)𝜇(𝑣′,𝑞′)(Φ(𝑣′:𝐴)+𝑞′). Induct on 𝑛, with an inner induction on the typing derivation.
Index zero.𝜇=0 and the right-hand side is 0≤Φ+𝑞.
L:Tick.𝜇=𝛿(⟨⟩,𝑞) and the right-hand side is Φ(⟨⟩:⟨𝟏,0⟩)+𝑞=𝑞, which is the left-hand side because the context is empty.
L:Flip. Here 𝜇=𝑝𝜇1+(1−𝑝)𝜇2 with 𝑉⊢𝑒𝑖⇒𝑛𝜇𝑖. The inner induction hypothesis at the two premises gives Φ(𝑉:Γ𝑖)+𝑞𝑖≥∑𝜇𝑖(𝑣′,𝑞′)(Φ(𝑣′:𝐴)+𝑞′). Multiplying the first by 𝑝, the second by 1−𝑝, and adding, 𝑝(Φ(𝑉:Γ1)+𝑞1)+(1−𝑝)(Φ(𝑉:Γ2)+𝑞2)(3)=Φ(𝑉:Γ)+𝑞, while the right-hand sides combine to ∑𝜇(𝑣′,𝑞′)(Φ(𝑣′:𝐴)+𝑞′) by linearity of a finite mixture (example 172.26).
L:Let. With Γ1;𝑞⊢𝑒1:⟨𝜏,𝑝⟩ and Γ2,𝑥:𝜏;𝑝⊢𝑒2:𝐵, the semantics gives 𝜇=∑(𝑣1,𝑞1)𝜇1(𝑣1,𝑞1)⋅𝜇(𝑣1,𝑞1) shifted by the cost 𝑞1. Apply the induction hypothesis to 𝑒1, then to each 𝑒2 under the extended environment, and use lemma 177.3 with the roles of 𝑜 and 𝑜′ played by the two stages; the additive shift of the cost is exactly the first summand there.
Application. The index decreases, so the outer induction hypothesis applies to the body under the environment extended by the argument, and L:Fun supplies the typing of that body in that context.
The remaining rules — L:Var, L:Unit, L:Nil, L:Cons, L:MatL, L:Share, L:Prob, L:FlipS, and the structural rules L:Sub, L:Sup, L:Weak, L:Relax — are formal copies of the deterministic cases with the same potential bookkeeping, because their semantics is a Dirac distribution or a rearrangement of one; each is obtained from the displayed L:Let case by deleting the mixture. ◻
The distribution [[𝑒]]⇒𝑉 of definition 177.9 ignores infinite traces: they contribute no mass. So the inequality bounds the expected cost conditioned on the terminating part, weighted by its probability, and says nothing about a program that diverges with positive probability. In particular it does not entail that a well-typed program terminates almost surely. Making divergence visible requires changing the object being approximated, which is the next section.
Extend the distributions of definition 177.9 to full probability distributions over (Val∪{∘})×(ℚ≥0∪{∞}), where ∘ is a dummy value recording an unfinished evaluation; the base rule becomes 𝑉⊢𝑒⇒0𝛿(∘,0), and the 𝗅𝖾𝗍 rule propagates ∘ with the cost accumulated so far. Define 𝜇1⊑𝜇2 when ∀𝑣≠∘,𝑞:𝜇1(𝑣,𝑞)≤𝜇2(𝑣,𝑞),and∀𝑞:𝜇1((Val∪{∘})×[0,𝑞])≥𝜇2((Val∪{∘})×[0,𝑞]). On finished values this is the pointwise order; on the dummy value it points the other way, because as evaluation proceeds an unfinished run accumulates cost and its mass migrates to larger costs.
Three statements of Wang–Kahn–Hoffmann are imported at exactly these signatures.
Their Lemma 5.4: ⊑ is a partial order on these distributions, and every ⊑-increasing sequence 𝜇1⊑𝜇2⊑⋯ has a least upper bound, written ⨆𝑛𝜇𝑛.
Their Lemma 5.5: if 𝑉⊢𝑒⇒𝑛𝜇1 and 𝑉⊢𝑒⇒𝑚𝜇2 with 𝑛≤𝑚, then 𝜇1⊑𝜇2; consequently [[𝑒]]⇒𝑉=⨆𝑛𝜇𝑛 is defined and describes all executions, terminating and not.
Their Lemma 5.6: let ℎ(𝜇)=∑𝑞𝜇(∘,𝑞)⋅𝑞+∑(𝑣,𝑞):𝑣≠∘𝜇(𝑣,𝑞)⋅(Φ(𝑣:𝐴)+𝑞). If 𝜇1⊑𝜇2⊑⋯ and ℎ(𝜇𝑛)≤𝑀 for all 𝑛, then ℎ(⨆𝑛𝜇𝑛)≤𝑀.
The third is the load-bearing one: the functional ℎ is not known to be continuous for ⊑, and the imported statement is the weaker preservation of an upper bound, which is what the soundness proof needs.
Proof. Write 𝑀=Φ(𝑉:Γ)+𝑞 and let ℎ be the functional of convention 177.13. By Lemma 5.5 the distributions 𝜇𝑛 with 𝑉⊢𝑒⇒𝑛𝜇𝑛 form a ⊑-increasing sequence with supremum [[𝑒]]⇒𝑉, and by Lemma 5.6 it suffices to prove ℎ(𝜇𝑛)≤𝑀 for every 𝑛. That is the same induction as in theorem 177.10, on 𝑛 with an inner induction on the typing derivation, with one new case: at index 0 the distribution is 𝛿(∘,0), for which ℎ(𝛿(∘,0))=0≤𝑀; and in the 𝗅𝖾𝗍 case the dummy value carries the cost accumulated by the first stage, which the first summand of ℎ charges exactly once. All other cases are unchanged, because they do not produce ∘. ◻
Let Γ;𝑞⊢𝑒:𝐴 and 𝑉:Γ, and suppose 𝑒 is instrumented with ticks that charge at least one unit for each evaluation step. Then [[𝑒]]⇒𝑉(∘,𝑞′)=0 for every 𝑞′∈ℚ≥0∪{∞}; that is, 𝑒 terminates with probability one.
Proof of Corollary 177.15 — Almost sure termination, under the tick hypothesis
Proof. For finite 𝑞′: a nonterminating run performs unboundedly many steps, each charged at least one unit, so its accumulated cost exceeds every finite 𝑞′; hence the limit distribution assigns no mass to (∘,𝑞′). For 𝑞′=∞: by theorem 177.14 the first summand [[𝑒]]⇒𝑉(∘,∞)⋅∞ is bounded by Φ(𝑉:Γ)+𝑞, which is finite; a finite bound on a product with ∞ forces the probability to be 0. ◻
Without the instrumentation, a well-typed program may diverge with positive probability and still satisfy theorem 177.14: if the diverging runs accrue no cost, the first summand is 0 and the inequality holds vacuously for them. The program 𝗋𝖽𝗐𝖺𝗅𝗄 of example 177.6 is the instructive case in the other direction: it does charge one tick per iteration, so corollary 177.15 applies and it terminates almost surely, even though the head branch lengthens the list. A finite expected cost is therefore not, by itself, a termination statement; it becomes one exactly when the cost counts steps.
Two nearby analyses are recorded as separate system cards and supply no theorem here. Avanzini–Moser–Schaper analyze expected cost for an imperative language by a modular transformation into a deterministic problem; their programs, cost model, and soundness statement are not those of convention 177.1. Wang et al.’s nondeterministic analysis admits signed costs, which invalidates the monotonicity used in definition 177.12 and therefore requires a different limit argument. Neither is obtained from the other by instantiation, and no bound derived in one system is asserted in the other.
★★☆ Give a well-typed program that diverges with probability 1/2 and has a finite derived bound, compute both, and check theorem 177.14 on it term by term.
★★☆ Give a program that terminates with probability one and has infinite expected cost, and state which hypothesis of theorem 177.14 prevents the type system from deriving a finite bound for it.
★★☆ Write out the L:Flip case of theorem 177.10 in full for a concrete two-branch program, displaying the sharing equation and the mixture computation.
★★☆ Verify Φ([1/5,2/5])=5 for the typing of example 177.6, and compute the expected cost of the first two iterations exactly, checking that it does not exceed 5.
★★☆ Take the naive rules of remark 177.8 and a program whose body calls itself unconditionally. Show that no distribution 𝜇 satisfies the rules for it, and show that the indexed judgment of definition 177.9 assigns it the zero distribution at every index.
★★★Practical project.praml-linear-constraint-generator Build a linear constraint generator and solver for the fragment of convention 177.1 restricted to lists, 𝗍𝗂𝖼𝗄, stored probabilities, 𝖿𝗅𝗂𝗉, 𝖿𝗅𝗂𝗉𝖲, 𝗅𝖾𝗍, and recursive functions of one argument. The generator walks a typing derivation skeleton and emits one linear constraint per rule — the sharing equations, the mixture equation 𝑞=𝑝𝑞1+(1−𝑝)𝑞2 of L:Flip, and the tick equation — over rational unknowns; the solver minimizes the constant potential subject to the constraints, in exact rational arithmetic.
The invariant to maintain is that every emitted constraint is linear with rational coefficients and that no potential unknown is ever assigned a negative value; the solver must report infeasibility rather than returning a bound when the constraints admit no nonnegative solution.
The concrete result is a derived bound for each of the two chapter programs. The acceptance test is decidable and exact: the tool must infer the bound 1 for 𝖻𝖾𝗋𝗇𝗈𝗎𝗅𝗅𝗂 at input type 𝗅𝗂𝗌𝗍(⟨𝜏,0⟩), and the bound 5 for 𝗋𝖽𝗐𝖺𝗅𝗄 at the argument [1/5,2/5], matching 𝑛+5∑𝑖𝑝𝑖 of example 177.6; it must report infeasibility for 𝖻𝖾𝗋𝗇𝗈𝗎𝗅𝗅𝗂 when the available constant potential is fixed at 1/2; and an instrumented finite trace enumerator must confirm the expected costs 1−2−𝑛 for 𝑛=1,2,3 as exact rationals. This checker is not the authors’ unpublished working tree, and it is not the public RaML release, which is the closest published implementation companion and includes the advertised probabilistic examples; agreement of a derived bound with either is not part of the acceptance test.