Probabilistic Lambda Calculi and Program Equivalence

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Consider two closed programs that each produce a bit. The first flips a fair coin; the second flips a coin that falls on $0$ once in three times. Write them, for the moment informally, as $\mathsf{coin}(1/2)$ and $\mathsf{coin}(1/3)$, and let a transition relation $⟶$ record which results are possible: $$\begin{array}{c}\mathsf{coin}(1/2)⟶\bar{0},\mathsf{coin}(1/2)⟶\bar{1},\\ \mathsf{coin}(1/3)⟶\bar{0},\mathsf{coin}(1/3)⟶\bar{1}.\end{array}$$ The two programs have the same reachable set $\{\bar{0},\bar{1}\}$, so every equivalence defined from the reachable set identifies them. A gambler who is paid one euro when the result is $\bar{0}$ does not identify them. The quantity that separates them — the probability that the program returns $\bar{0}$ — is not a set of successor states but a number, and the relation $⟶$ does not carry it.

Three things must therefore be built, and the chapter builds them in this order. The operational semantics must assign to each pair of terms the probability of a transition, and must accumulate those probabilities along possibly infinite reduction sequences into a subprobability distribution over results; a diverging program then contributes missing mass rather than a default value. The program equivalence must observe those numbers through arbitrary program contexts. Finally, a denotational model must compute the same numbers compositionally, and must do so exactly: an inequality between the model and the operational probabilities is not enough to decide the equivalence, and a model that identifies more terms than contexts do would answer the wrong question. The invariant that organizes the whole chapter is the equality between an operational convergence probability and a coefficient of a power series, first for ground results and then, through a family of testing programs, for every type.

The calculus pPCF

Two features of the card do work that a reader of an ordinary call-by-name PCF should notice at once.

The conditional binds its scrutinee’s value. In PCF one writes $\mathsf{if}(M,P,Q)$ and, in the branch taken when $M$ is nonzero, recovers the value of $M$ by evaluating $M$ again. Under a probabilistic semantics that second evaluation is a second experiment: it need not return what the first returned. The pPCF conditional therefore passes the predecessor of the scrutinee to the branch through the bound variable $z$, so that the outcome of the single experiment performed on $M$ is available without repeating it.

The bound variable makes the predecessor definable, which is where the mechanism is easiest to see: $$\mathsf{pred}=\lambda x^{\iota }.\mathsf{if}(x,\bar{0},z\cdot z).$$

The closed weak-normal terms of type $\iota$ are exactly the numerals, and the closed weak-normal terms of type $\sigma ⟶\tau$ are exactly the abstractions. Both facts are read off the rules: every other closed term has a leftmost outermost redex.

The next calculation exercises the value-passing conditional and produces the running program of the chapter.

Convergence probabilities

Example 171.5 multiplied labels along a path and summed over paths. That informal recipe must become a definition that also survives infinitely many paths, and the following device — reduction as a stochastic matrix — makes the sum a supremum of finite approximations.

The first clause is unambiguous because a non-weak-normal term has exactly one leftmost outermost redex, and that redex is either deterministic — giving one successor with label $1$ — or a coin, giving two successors with labels summing to $1$. Hence every row of $\mathrm{Red}(\mathrm{\Gamma },\sigma )$ sums to $1$: the matrix is stochastic, and a weak-normal term is a state that only steps to itself.

Proof of Lemma 171.7 — Monotone approximation

Proof. Fix $i\in I$ and $j\in I_1$. Then $$(S^{k+1}{)}_{i,j}=\sum _{l\in I}(S^k{)}_{i,l}{S}_{l,j}\ge (S^k{)}_{i,j}{S}_{j,j}\stackrel{j\in I_1}{=}(S^k{)}_{i,j},$$ where the inequality drops all summands except $l=j$, each of which is nonnegative. So the sequence is nondecreasing and its supremum exists in $[0,1]$. For the mass bound, exchange a supremum of a nondecreasing sequence with a countable sum of nonnegative terms: The last equality holds because a product of stochastic matrices is stochastic. ◻

The supremum in lemma 171.7 is a sum over reduction paths, which is how the calculations in this chapter are actually performed.

Proof of Lemma 171.9 — Path decomposition

Proof. Because $j$ is stationary, for each $k$ the number $(S^k{)}_{i,j}$ is the sum of the weights of all length-$k$ sequences from $i$ to $j$; grouping such a sequence by the first index at which it reaches $j$ and using $S_{j,j}=1$ for the remaining steps, $(S^k{)}_{i,j}$ is the sum of $\mathrm{wt}(w)$ over paths $w$ of length at most $k$. The paths form a countable set of nonnegative summands, so the supremum over $k$ of these partial sums is the total sum. The requirement that $j$ occurs only at the end of a path is what prevents a path from being counted twice. ◻

Observational equivalence

A single number, the probability of returning $\bar{0}$, is enough to separate $\mathsf{coin}(1/2)$ from $\mathsf{coin}(1/3)$. Terms of higher type produce no number by themselves; they must first be placed in a program that consumes them. The definition therefore quantifies over contexts.

Only the probability of the single result $\bar{0}$ is compared. This is no restriction, because the family of tests below moves any other result into that position.

Proof of Lemma 171.15 — What a test measures

Proof. Induction on $k$. For $k=0$: the term ${\mathsf{prob}}_{0}M$ contracts in one deterministic step to $\mathsf{if}(M,\bar{0},z\cdot {\mathrm{\Omega }}_{\iota })$, and by Ctx-If every reduction of $M$ is copied inside the conditional with the same label. A path from ${\mathsf{prob}}_{0}M$ to $\bar{0}$ therefore consists of that first step, a path of $M$ to some numeral $\bar{n}$, and then the contraction of $\mathsf{if}(\bar{n},\bar{0},z\cdot {\mathrm{\Omega }}_{\iota })$. The last contraction reaches $\bar{0}$ when $n=0$ and reaches ${\mathrm{\Omega }}_{\iota }[\overline{n-1}/z]={\mathrm{\Omega }}_{\iota }$ when ; no path from ${\mathrm{\Omega }}_{\iota }$ reaches a weak-normal term by exercise 171.2. Summing weights by lemma 171.9 leaves exactly the paths of $M$ to $\bar{0}$.

For $k+1$: the same analysis leaves the paths of $M$ to numerals $\overline{n+1}$, each continued by ${\mathsf{prob}}_k\bar{n}$, and the induction hypothesis gives $\mathrm{Red}(\iota {)}_{{\mathsf{prob}}_k\bar{n},\bar{0}}^{\mathrm{\infty }}=\mathrm{Red}(\iota {)}_{\bar{n},\bar{k}}^{\mathrm{\infty }}$, which is $1$ when $n=k$ and $0$ otherwise. Hence the total weight is $\mathrm{Red}(\iota {)}_{M,\overline{k+1}}^{\mathrm{\infty }}$. ◻

Probabilistic coherence spaces

The equivalence of definition 171.13 quantifies over infinitely many contexts, so it cannot be decided by running programs. A model is wanted whose elements are the numbers the contexts measure. For the ground type the answer is forced: an element must be a subprobability distribution on $\mathbb{N}$. The question is what an element of a function type is, and the requirement that settles it is that a program of type $\iota ⟶\iota$ transforms subprobability distributions into subprobability distributions by a rule that is stable under composition and under limits of increasing chains.

Proof of Lemma 171.18 — Closure

Proof. The first two claims are immediate from the definition. For the third, apply the second to ${\mathcal{X}}^{⟂}$ to get ${\mathcal{X}}^{⟂}\subseteq {\mathcal{X}}^{⟂⟂⟂}$, and apply the first to $\mathcal{X}\subseteq {\mathcal{X}}^{⟂⟂}$ to get ${\mathcal{X}}^{⟂⟂⟂}\subseteq {\mathcal{X}}^{⟂}$. ◻

Clause (i) is a closure condition; clauses (ii) and (iii) say that no web point is unusable and that no coordinate is unbounded. Both are used below: (iii) bounds the coefficients of the power series to come, and (ii), sharpened in lemma 171.25, provides the arguments at which those series are compared.

Proof of Lemma 171.20 — Downward closure and increasing limits

Proof. For $u^{\prime }\in P{X}^{⟂}$ we have $⟨u,u^{\prime }⟩\le ⟨v,u^{\prime }⟩\le 1$, so $u\in P{X}^{⟂⟂}=PX$. Taking $v\in PX$ — one exists by (ii) — and $u=0$ gives $0\in PX$. For the supremum $w=\underset{k}{sup}{u}^{(k)}$ and $u^{\prime }\in P{X}^{⟂}$, $$⟨w,u^{\prime }⟩=\sum _a(\underset{k}{sup}{u}_a^{(k)})u_a^{\prime }\stackrel{monotoneconvergence}{=}\underset{k}{sup}⟨u^{(k)},u^{\prime }⟩\le 1,$$ so $w\in P{X}^{⟂⟂}=PX$. ◻

A morphism must send $PX$ to $PY$, preserve increasing limits, and compose. Power series with nonnegative coefficients do all three, and the exponents are recorded by finite multisets.

Proof of Proposition 171.24 — The arrow is a probabilistic coherence space

Proof. Closure. For $u\in ({\mathbb{R}}^{+}{)}^{|X|}$ and $v^{\prime }\in ({\mathbb{R}}^{+}{)}^{|Y|}$ let $u\otimes v^{\prime }$ be the vector on the web of $X⟶Y$ with $(u\otimes v^{\prime }{)}_{(\mu ,b)}=u^{\mu }{v}_b^{\prime }$. Then $$⟨t,u\otimes v^{\prime }⟩=\sum _{\mu ,b}{t}_{\mu ,b}{u}^{\mu }{v}_b^{\prime }=\sum _b(\sum _{\mu }{t}_{\mu ,b}{u}^{\mu })v_b^{\prime }=⟨\hat{t}(u),v^{\prime }⟩,$$ the middle step by rearranging a double sum of nonnegative terms. Hence $\hat{t}(u)\in PY=P{Y}^{⟂⟂}$ for all $u\in PX$ if and only if $⟨t,u\otimes v^{\prime }⟩\le 1$ for all $u\in PX$ and $v^{\prime }\in P{Y}^{⟂}$, that is, if and only if $t\in {\mathcal{Z}}^{⟂}$ for $\mathcal{Z}=\{u\otimes v^{\prime }\mid u\in PX,v^{\prime }\in P{Y}^{⟂}\}$. So $P(X⟶Y)={\mathcal{Z}}^{⟂}$, which is biorthogonally closed by lemma 171.18.

Clause (ii). Fix $(\mu ,b)$. By clause (iii) for $X$, put , so that $u^{\mu }\le C_{\mu }$ for every $u\in PX$. By hypothesis choose with ${\epsilon }^{\prime }{e}_b\in PY$, and set $t=({\epsilon }^{\prime }/C_{\mu })e_{(\mu ,b)}$. Then $\hat{t}(u)=({\epsilon }^{\prime }/C_{\mu })u^{\mu }{e}_b\le {\epsilon }^{\prime }{e}_b$, which lies in $PY$ by lemma 171.20; and .

Clause (iii). Fix $(\mu ,b)$ and let $F=\mathrm{supp}(\mu )$. By hypothesis choose with $u^{\ast }=\delta 1_F\in PX$. For any $t\in P(X⟶Y)$, dropping all summands but one, $$\hat{t}(u^{\ast }{)}_b\ge t_{\mu ,b}(u^{\ast }{)}^{\mu }=t_{\mu ,b}{\delta }^{\mathrm{\#}\mu },$$ while $\hat{t}(u^{\ast }{)}_b\le A_b$ by clause (iii) for $Y$. Hence $t_{\mu ,b}\le A_b{\delta }^{-\mathrm{\#}\mu }$, a bound depending only on $(\mu ,b)$.

Finite supports. Let $G$ be finite, let $G_2=\{b\mid \mathrm{\exists }\mu (\mu ,b)\in G\}$, and let $C=max\{C_{\mu }\mid (\mu ,b)\in G\}$ with $C_{\mu }$ as above. Choose with ${\epsilon }^{\prime }{1}_{G_2}\in PY$ and put $\eta ={\epsilon }^{\prime }/(|G|C)$. For $u\in PX$, $\widehat{\eta 1_G}(u{)}_b=\eta \sum _{\mu :(\mu ,b)\in G}{u}^{\mu }\le \eta |G|C={\epsilon }^{\prime }$ for $b\in G_2$ and $0$ otherwise, so $\widehat{\eta 1_G}(u)\le {\epsilon }^{\prime }{1}_{G_2}\in PY$, and lemma 171.20 finishes. ◻

Proof of Lemma 171.25 — The invariants of the interpreted types

Proof. Induction on $\sigma$. For $\iota$, example 171.21 gives the space, and $\epsilon =1/|F|$ makes $\epsilon 1_F$ a subprobability distribution. For $\sigma ⟶\tau$ the induction hypothesis supplies both components of the hypothesis of proposition 171.24, whose conclusion is exactly the claim. ◻

The next theorem is the reason the model can decide an equivalence. It says that a morphism is recoverable from the function it induces, so that two programs with different matrices differ at some argument — and, as the proof shows, at an argument with rational coordinates and finite support, which is the kind of argument a pPCF program can produce.

Proof of Lemma 171.26 — Coefficients from values

Proof. Induction on $|I|$. If $I=\mathrm{\varnothing }$ both sums have the single term $c_{\mathrm{\varnothing }}=f=f^{\prime }=c_{\mathrm{\varnothing }}^{\prime }$.

Let $|I|=k+1$ and fix $a\in I$, writing $I^{\prime }=I\setminus \{a\}$ and $x=(x_a,x^{\prime })$. Grouping the terms by the exponent of $x_a$, $$f(x_a,x^{\prime })=\sum _{m=0}^{\mathrm{\infty }}{g}_m(x^{\prime })x_a^m,g_m(x^{\prime })=\sum _{{\nu }^{\prime }:{\nu }^{\prime }\in {\mathcal{M}}_{\mathrm{fin}}(I^{\prime })}{c}_{{\nu }^{\prime }+m\cdot a}(x^{\prime }{)}^{{\nu }^{\prime }},$$ where ${\nu }^{\prime }+m\cdot a$ is the multiset ${\nu }^{\prime }$ extended by $m$ copies of $a$; the rearrangement is legitimate because all terms are nonnegative and the total sum is finite. Fix $x^{\prime }\in [0,A{]}^{I^{\prime }}$. Then $x_a\mapsto f(x_a,x^{\prime })$ is a power series in one variable with nonnegative coefficients $g_m(x^{\prime })$, convergent on $[0,A]$; inside its interval of convergence it may be differentiated term by term, so $g_m(x^{\prime })=\frac{1}{m!}{\partial }_{x_a}^{m}f(0,x^{\prime })$. The same computation applies to $f^{\prime }$, and $f=f^{\prime }$ gives $g_m(x^{\prime })=g_m^{\prime }(x^{\prime })$ for every $m$ and every $x^{\prime }\in [0,A{]}^{I^{\prime }}$. Each pair $g_m,g_m^{\prime }$ satisfies the hypotheses of the lemma on $I^{\prime }$, so the induction hypothesis gives $c_{{\nu }^{\prime }+m\cdot a}=c_{{\nu }^{\prime }+m\cdot a}^{\prime }$ for all ${\nu }^{\prime }$ and $m$. Every $\nu \in {\mathcal{M}}_{\mathrm{fin}}(I)$ has this form. ◻

Proof of Theorem 171.27 — Determination

Proof. One direction is trivial. For the other, suppose $t_{\mu ,b}\ne t_{\mu ,b}^{\prime }$ for some $(\mu ,b)$, and let $I=\mathrm{supp}(\mu )$, a finite set. By proposition 171.24 there is with $\delta 1_I\in PX$, and by lemma 171.20 every $u$ supported in $I$ with coordinates at most $\delta$ lies in $PX$. Consider $$f(x)=\hat{t}(x{)}_b=\sum _{\nu \in {\mathcal{M}}_{\mathrm{fin}}(I)}{t}_{\nu ,b}{x}^{\nu },f^{\prime }(x)={\hat{t}}^{\prime }(x{)}_b,x\in [0,\delta {]}^I,$$ where a vector $x$ on $I$ is read as the element of $({\mathbb{R}}^{+}{)}^{|X|}$ that vanishes outside $I$; only multisets over $I$ contribute, since $x^{\nu }=0$ as soon as $\nu$ charges a point outside $I$. Both are finite on $[0,\delta {]}^I$, being coordinates of elements of $PY$, which are bounded by clause (iii). Their coefficients differ at $\mu$, so lemma 171.26 gives a point of $[0,\delta {]}^I$ at which $f\ne f^{\prime }$. Both are continuous on that closed box: with $M_{\nu }=t_{\nu ,b}{\delta }^{\mathrm{\#}\nu }$ one has $|t_{\nu ,b}{x}^{\nu }|\le M_{\nu }$ for every $x\in [0,\delta {]}^I$, and , so the series converges uniformly on the box and its partial sums are polynomials. Hence the set where $f$ and $f^{\prime }$ differ is a nonempty relatively open subset of $[0,\delta {]}^I$ and therefore contains a point with rational coordinates. That point is supported in the finite set $I$. ◻

Adequacy

Example 171.30 computed the same distribution twice, once by summing path weights and once by iterating a power series. The two computations must agree for every closed term of ground type. One inequality follows from a single invariance equation; the other needs a logical relation, because a term of higher type has no result distribution of its own.

Proof of Lemma 171.31 — Substitution

Proof. Induction on $M$. Variable case. For $M=x$ both sides are $[[P{]]}_{\mathrm{\Gamma }}(\overrightarrow{u})$ by the variable clause; for $M=x_i$ with $x_i\ne x$ both sides are $u_i$. Application case. writing $w=[[P{]]}_{\mathrm{\Gamma }}(\overrightarrow{u})$. Binder case. For $M=\lambda y^{\rho }.M_1$ with $y$ chosen outside $\mathrm{FV}(P)\cup \{x\}\cup \mathrm{dom}(\mathrm{\Gamma })$, the abstraction clause evaluates both sides at an arbitrary $v\in P[[\rho ]]$ and the induction hypothesis for $M_1$ in the context $\mathrm{\Gamma },y:\rho$ applies; the two function forms agree at every $v$, hence the two matrices agree by theorem 171.27. The remaining formers — numerals, coins, $\mathsf{succ}$, $\mathsf{if}$, $\mathsf{fix}$ — are treated as the application case: each clause is built from the interpretations of the immediate subterms by an operation not depending on the substituted term, so the induction hypothesis may be applied to each subterm in turn. In the $\mathsf{if}$ case the third subterm is interpreted in the context extended by $z:\iota$, and the argument supplied for $z$ is $e_n$, which does not involve $P$. ◻

Proof of Theorem 171.32 — Invariance under one step

Proof. Induction on $M$. If $M$ is weak-normal the right-hand side is $1\cdot [[M{]]}_{\mathrm{\Gamma }}$. There remain the terms with a leftmost outermost redex.

Coin. $\mathsf{coin}(p){⟶}_p\bar{0}$ and $\mathsf{coin}(p){⟶}_{1-p}\bar{1}$, so the right-hand side is $p{e}_0+(1-p)e_1$, which is $[[\mathsf{coin}(p){]]}_{\mathrm{\Gamma }}$ by definition 171.29.

Beta. $(\lambda x^{\sigma }.P)N$ has the unique successor $P[N/x]$ with label $1$, and

Fixed point. $\mathsf{fix}(P)$ has the unique successor $P\mathsf{fix}(P)$ with label $1$. With $f=\widehat{[[P{]]}_{\mathrm{\Gamma }}(\overrightarrow{u})}$, where the second step holds because each coefficient of $f(v)$ is a sum of nonnegative monomials in the coordinates of $v$, and such a sum commutes with the supremum of a nondecreasing sequence.

Successor at a numeral, conditional at a numeral. $\mathsf{succ}(\bar{n})$ has successor $\overline{n+1}$, and $[[\mathsf{succ}(\bar{n}){]]}_{\mathrm{\Gamma }}=e_{n+1}$ by the $\mathsf{succ}$ clause applied to $e_n$. For $\mathsf{if}(\bar{0},P,z\cdot R)$ the successor is $P$, and the $\mathsf{if}$ clause at $[[\bar{0}]]=e_0$ leaves the single summand $[[P{]]}_{\mathrm{\Gamma }}$. For $\mathsf{if}(\overline{n+1},P,z\cdot R)$ the successor is $R[\bar{n}/z]$, and the same clause at $e_{n+1}$ leaves $[[R{]]}_{\mathrm{\Gamma },z:\iota }(\overrightarrow{u},e_n)$, which is $[[R[\bar{n}/z]{]]}_{\mathrm{\Gamma }}(\overrightarrow{u})$ by lemma 171.31.

Context cases. Let $M$ be one of $M_{1}N$, $\mathsf{succ}(M_1)$, $\mathsf{if}(M_1,P,z\cdot R)$ with $M_1$ not weak-normal. Then $M$ is not weak-normal, its successors are obtained from those of $M_1$ by the same construction, and the labels are unchanged, so ${\mathrm{Red}}_{M,M^{\prime }}=\mathrm{Red}(\mathrm{\Gamma },\iota {)}_{M_1,M_1^{\prime }}$ for the matching successor $M^{\prime }$. In each of the three clauses the interpretation of $M$ is obtained from the matrix $[[M_1{]]}_{\mathrm{\Gamma }}$ by an operation that is linear in it: for the successor and the conditional this is visible in the displayed formulas, and for the application it is the identity $\widehat{(\sum _i{\lambda }_i{t}_i)}(v)=\sum _i{\lambda }_i{\hat{t}}_i(v)$, which holds because $\hat{t}(v{)}_b=\sum _{\mu }{t}_{\mu ,b}{v}^{\mu }$ is linear in $t$. Applying that linear operation to the induction hypothesis for $M_1$ gives the claim for $M$. ◻

Proof of Theorem 171.33 — The model dominates the operational semantics

Proof. Iterating theorem 171.32 $k$ times gives $[[M]]=\sum _{M^{\prime }}\mathrm{Red}(\iota {)}_{M,M^{\prime }}^k[[M^{\prime }]]$. All summands are nonnegative, so keeping only $M^{\prime }=\bar{n}$ and reading the coordinate $n$, for which ${[[\bar{n}]]}_n=1$, gives ${[[M]]}_n\ge \mathrm{Red}(\iota {)}_{M,\bar{n}}^k$. Take the supremum over $k$; by definition 171.8 it is $\mathrm{Red}(\iota {)}_{M,\bar{n}}^{\mathrm{\infty }}$. ◻

The converse inequality cannot be proved by the same route: iterating an equation produces upper bounds on operational quantities, not lower bounds, and a term of type $\sigma ⟶\tau$ has no operational quantity at all until it is applied. The standard repair is a relation, defined by induction on types, that says at ground type “the model underestimates the operational probabilities” and at higher type “the term maps related arguments to related results”.

Proof of Lemma 171.35 — Zero and limits

Proof. Induction on $\sigma$. At $\iota$ the first claim is $0\le \mathrm{Red}(\iota {)}_{M,\bar{n}}^{\mathrm{\infty }}$ and the second is the statement that a supremum of numbers each bounded by $\mathrm{Red}(\iota {)}_{M,\bar{n}}^{\mathrm{\infty }}$ is bounded by it. At $\sigma ⟶\tau$: for the first claim, $\hat{0}(u)=0$ and the induction hypothesis at $\tau$ gives $MP{R}_{\tau }0$. For the second, let $P{R}_{\sigma }u$; then $\widehat{\underset{i}{sup}{t}^{(i)}}(u)=\underset{i}{sup}\widehat{t^{(i)}}(u)$, because each coefficient is a sum of nonnegative terms and commutes with the supremum of a nondecreasing sequence, and the induction hypothesis at $\tau$ applies to the sequence $\widehat{t^{(i)}}(u)$. ◻

Proof of Lemma 171.36 — Convergence through a conditional

Proof. Write $E[\cdot ]$ for the evaluation context $[\cdot ]N_1\cdots N_h$. By Ctx-App and Ctx-If, every step of $E[\mathsf{if}(M,P,z\cdot Q)]$ is either a step of $M$ copied with the same label, or — once $M$ has become a numeral — the contraction of the conditional. A path from $E[\mathsf{if}(M,P,z\cdot Q)]$ to $\bar{n}$ therefore factors uniquely as a path of $M$ to some numeral $\bar{m}$, the contraction of the conditional, and a path from $E[P]$ (if $m=0$) or from $E[Q[\overline{m-1}/z]]$ (if ) to $\bar{n}$. The weight of the composite path is the product of the weights of the factors, so summing over all paths by lemma 171.9 and grouping by $m$ gives the displayed equation. ◻

Proof of Lemma 171.37 — One step backwards

Proof. Induction on $\sigma$. Ground case. Let $\sigma =\iota$ and $n\in \mathbb{N}$. Because $\bar{n}$ is weak-normal, $\mathrm{Red}(\iota {)}_{M,\bar{n}}^{\mathrm{\infty }}=\sum _{M^{″}}\mathrm{Red}(\iota {)}_{M,M^{″}}\mathrm{Red}(\iota {)}_{M^{″},\bar{n}}^{\mathrm{\infty }}$, all terms being nonnegative; keeping the summand $M^{″}=M^{\prime }$ and using $u_n\le \mathrm{Red}(\iota {)}_{M^{\prime },\bar{n}}^{\mathrm{\infty }}$ gives $\mathrm{Red}(\iota {)}_{M,M^{\prime }}{u}_n\le \mathrm{Red}(\iota {)}_{M,\bar{n}}^{\mathrm{\infty }}$, which is the claim.

Arrow case. Let $\sigma =\tau ⟶\phi$. If $M$ is weak-normal, then either $M^{\prime }=M$ and $\mathrm{Red}(\sigma {)}_{M,M^{\prime }}=1$, so the hypothesis is the conclusion; or $M^{\prime }\ne M$ and $\mathrm{Red}(\sigma {)}_{M,M^{\prime }}=0$, so the conclusion is $M{R}_{\sigma }0$, which is lemma 171.35. Assume $M$ is not weak-normal and let $P{R}_{\tau }v$. Since the leftmost outermost redex of $MP$ is that of $M$, the rule Ctx-App gives $\mathrm{Red}(\phi {)}_{MP,M^{\prime }P}=\mathrm{Red}(\sigma {)}_{M,M^{\prime }}$. By hypothesis $M^{\prime }P{R}_{\phi }\hat{u}(v)$, so the induction hypothesis at $\phi$ gives $MP{R}_{\phi }\mathrm{Red}(\sigma {)}_{M,M^{\prime }}\hat{u}(v)$, and $\mathrm{Red}(\sigma {)}_{M,M^{\prime }}\hat{u}(v)=\widehat{(\mathrm{Red}(\sigma {)}_{M,M^{\prime }}u)}(v)$ by linearity of $t\mapsto \hat{t}(v)$. ◻

Proof of Theorem 171.38 — Fundamental lemma

Proof. Induction on the typing derivation. Write $\theta$ for the substitution $[P_1/x_1,\dots ,P_l/x_l]$ and assume $P_i{R}_{{\sigma }_i}{u}_i$ throughout.

Variables and numerals. $x_i\theta =P_i$ and $[[x_i{]]}_{\mathrm{\Gamma }}(\overrightarrow{u})=u_i$. For $\bar{n}$, $[[\bar{n}{]]}_{\mathrm{\Gamma }}(\overrightarrow{u})=e_n$ and $\mathrm{Red}(\iota {)}_{\bar{n},\bar{n}}^{\mathrm{\infty }}=1$.

Coin. $\mathsf{coin}(p)\theta =\mathsf{coin}(p)$ and its result distribution is $p$ at $\bar{0}$, $1-p$ at $\bar{1}$, and $0$ elsewhere, which is exactly $[[\mathsf{coin}(p){]]}_{\mathrm{\Gamma }}(\overrightarrow{u})$.

Successor. By the induction hypothesis $[[P{]]}_{\mathrm{\Gamma }}(\overrightarrow{u}{)}_n\le \mathrm{Red}(\iota {)}_{P\theta ,\bar{n}}^{\mathrm{\infty }}$ for all $n$. Every path of $P\theta$ to $\bar{n}$ yields, under Ctx-Succ followed by the contraction $\mathsf{succ}(\bar{n}){⇝}_0\overline{n+1}$, a path of $\mathsf{succ}(P\theta )$ to $\overline{n+1}$ of the same weight, so $[[\mathsf{succ}(P){]]}_{\mathrm{\Gamma }}(\overrightarrow{u}{)}_{n+1}\le \mathrm{Red}(\iota {)}_{\mathsf{succ}(P\theta ),\overline{n+1}}^{\mathrm{\infty }}$; at index $0$ the left-hand side is $0$.

Conditional. Let $M=\mathsf{if}(P,Q,z\cdot R)$ at type $\sigma ={\sigma }_1^{\prime }⟶\cdots ⟶{\sigma }_h^{\prime }⟶\iota$. The induction hypothesis gives $$\begin{array}{c}[[P{]]}_{\mathrm{\Gamma }}(\overrightarrow{u}{)}_m\le \mathrm{Red}(\iota {)}_{P\theta ,\bar{m}}^{\mathrm{\infty }}(m\in \mathbb{N}),\\ Q\theta R_{\sigma }[[Q{]]}_{\mathrm{\Gamma }}(\overrightarrow{u}),\\ R\theta [\bar{k}/z]R_{\sigma }[[R{]]}_{\mathrm{\Gamma },z:\iota }(\overrightarrow{u},e_k),\end{array}$$ the third by applying the induction hypothesis in the context $\mathrm{\Gamma },z:\iota$ with the pair $\bar{k}{R}_{\iota }{e}_k$. Let $N_j{R}_{{\sigma }_j^{\prime }}{v}_j$ for $j\le h$ and let $n\in \mathbb{N}$. Lemma 171.36 expands $\mathrm{Red}(\iota {)}_{M\theta N_1\cdots N_h,\bar{n}}^{\mathrm{\infty }}$ into the two groups of summands displayed there; bounding each factor from below by the corresponding denotational quantity, and using the definition of $R_{\sigma }$ for $Q\theta$ and for each $R\theta [\bar{k}/z]$, gives whose right-hand side is $[[M{]]}_{\mathrm{\Gamma }}(\overrightarrow{u})\hat{}(v_1)\cdots (v_h{)}_n$ by the $\mathsf{if}$ clause. This is the definition of $M\theta R_{\sigma }[[M{]]}_{\mathrm{\Gamma }}(\overrightarrow{u})$.

Application. For $M=PQ$, the induction hypothesis gives $P\theta R_{\tau ⟶\sigma }[[P{]]}_{\mathrm{\Gamma }}(\overrightarrow{u})$ and $Q\theta R_{\tau }[[Q{]]}_{\mathrm{\Gamma }}(\overrightarrow{u})$; the definition of $R$ at the arrow type applied to this pair gives $P\theta Q\theta R_{\sigma }\widehat{[[P{]]}_{\mathrm{\Gamma }}(\overrightarrow{u})}([[Q{]]}_{\mathrm{\Gamma }}(\overrightarrow{u}))$, and the right-hand side is $[[PQ{]]}_{\mathrm{\Gamma }}(\overrightarrow{u})$.

Abstraction. For $M=\lambda x^{\tau }.P$ at type $\tau ⟶\phi$, let $t=[[M{]]}_{\mathrm{\Gamma }}(\overrightarrow{u})$ and let $Q{R}_{\tau }v$. Since $(\lambda x^{\tau }.P\theta )Q{⇝}_{0}P\theta [Q/x]$ with label $1$, lemma 171.37 reduces the goal $(\lambda x^{\tau }.P\theta )Q{R}_{\phi }\hat{t}(v)$ to $P\theta [Q/x]R_{\phi }\hat{t}(v)$, and $\hat{t}(v)=[[P{]]}_{\mathrm{\Gamma },x:\tau }(\overrightarrow{u},v)$ by the abstraction clause, so the induction hypothesis in the extended context finishes the case.

Fixed point. For $M=\mathsf{fix}(P)$ let $t=[[P{]]}_{\mathrm{\Gamma }}(\overrightarrow{u})$ and $f=\hat{t}$. By lemma 171.35 it suffices to prove $\mathsf{fix}(P\theta )R_{\sigma }{f}^m(0)$ for every $m$, and this is an induction on $m$. The case $m=0$ is lemma 171.35. Assume $\mathsf{fix}(P\theta )R_{\sigma }{f}^m(0)$. Since $\mathsf{fix}(P\theta ){⇝}_{0}P\theta \mathsf{fix}(P\theta )$ with label $1$, lemma 171.37 reduces the goal at $m+1$ to $P\theta \mathsf{fix}(P\theta )R_{\sigma }{f}^{m+1}(0)$. The outer induction hypothesis gives $P\theta R_{\sigma ⟶\sigma }t$, which applied to the pair $\mathsf{fix}(P\theta )R_{\sigma }{f}^m(0)$ yields exactly $P\theta \mathsf{fix}(P\theta )R_{\sigma }f(f^m(0))$. ◻

Proof of Theorem 171.39 — Adequacy

Proof. Theorem 171.38 with the empty context gives $M{R}_{\iota }[[M]]$, that is ${[[M]]}_n\le \mathrm{Red}(\iota {)}_{M,\bar{n}}^{\mathrm{\infty }}$. Theorem 171.33 gives the reverse inequality. ◻

Proof of Lemma 171.40 — Contexts act on denotations

Proof. Induction on the derivation of $\mathrm{\Gamma }⊢C^{\mathrm{\Delta }⊢\tau }:\sigma$. For the hole, $C=[{]}^{\mathrm{\Delta }⊢\tau }$ and $C[M]=M$ with $\mathrm{\Gamma }={\mathrm{\Gamma }}^{\prime },\mathrm{\Delta }$; take $f_C$ to be the map that reads $[[M{]]}_{\mathrm{\Delta }}$ and returns the interpretation of $M$ in the larger context, which the clauses of definition 171.29 obtain by ignoring the extra coordinates. For every other rule, $C$ is a term former applied to smaller contexts $C_1,\dots ,C_r$ and possibly to terms not containing the hole; the corresponding clause of definition 171.29 expresses $[[C[M]{]]}_{\mathrm{\Gamma }}$ as an operation applied to $[[C_i[M]{]]}_{\mathrm{\Gamma }}$ and to interpretations of hole-free subterms, and composing that operation with the functions $f_{C_i}$ given by the induction hypothesis produces $f_C$. ◻

Proof of Theorem 171.41 — Denotational equality implies observational equivalence

Proof. Let $C^{\mathrm{\Gamma }⊢\sigma }$ be an observation context with $\cdot ⊢C^{\mathrm{\Gamma }⊢\sigma }:\iota$. Then  ◻

Separating two denotations by a program

Theorem 171.41 settles one implication. Its converse — if no context separates $M$ from $M^{\prime }$, then their denotations are equal — is what makes the model an answer to the original question rather than an approximation to it. Its proof must, from a single web point $a$ at which two elements $w,w^{\prime }\in P[[\sigma ]]$ differ, manufacture a pPCF program that observes the difference.

Two obstructions stand in the way, and the construction is determined by removing them.

First, the coefficient $w_a$ is not the value of any definable map at any argument. A closed term $F$ of type $\sigma ⟶\iota$ has $\widehat{[[F]]}(w{)}_0=\sum _{\mu }{t}_{\mu ,0}{w}^{\mu }$, a sum of monomials in the coordinates of $w$; no such sum is the single coordinate $w_a$. The repair is not to read $w_a$ off but to expose it as a coefficient: build a family of programs, indexed by a supply of randomness $u\in PN$, whose observation is a power series in $u$ in which the coefficient of one designated monomial is exactly $w_a$. Lemma 171.26 then converts a difference of coefficients into a difference of values at a rational argument, and $\mathrm{ran}$ below turns a rational argument into a program.

Second, the designated monomial must be multilinear, $u_0{u}_1\cdots u_{n-1}$, with each parameter used once. A parameter consumed twice would contribute $u_i^2$ and land in a different coefficient. Since a web point of an arrow type carries several subtests — one for each element of the multiset in its domain component, and one for its codomain component — each subtest must read a block of parameters disjoint from every other block. That constraint determines the whole shape of the construction: a counter $|a{|}^{\pm }$ that records how many parameters a test consumes, and a shift operator that moves a test onto its own block.

Proof of Definition 171.42 — Auxiliary programs

Verification of the four denotations. For ${\mathsf{shift}}_k$: at $k=0$ the abstraction clause gives the identity function; at $k+1$ the $\mathsf{succ}$ clause shifts the induction hypothesis by one index. For ${\mathsf{prod}}_k$: at $k=0$ the value is $e_0$, the empty product; at $k+1$ the $\mathsf{if}$ clause selects $u_0^1$ times the interpretation of ${\mathsf{prod}}_k$ and discards the diverging branch, since $[[\mathrm{\Omega }]]=0$ by exercise 171.11. For ${\mathsf{choose}}_k$: at $k=0$ the value is $0$; at $k+1$ the $\mathsf{if}$ clause contributes $u_0{w}^1$ from the zero branch and, from the summand indexed $m+1$, the value $u_{m+1}$ times the interpretation of ${\mathsf{choose}}_k\bar{m}{w}^2\cdots$, which the induction hypothesis evaluates to $w^{m+2}$ for $m+1\le k$. For $\mathrm{ran}$: the first clause is immediate, the second gives $p_0{e}_0$, and in the third the coin contributes $p_0{e}_0$ from the zero branch and $(1-p_0)$ times the shifted interpretation of the recursive call from the other, which is $(1-p_0)\sum _{i\ge 1}\frac{p_i}{1-p_0}{e}_i$. ◻

The two displays record where each block of parameters goes. The test $a^{-}$ spends its first $k$ parameters $u_0,\dots ,u_{k-1}$ on ${\mathsf{choose}}_k$, which decides which of the $k$ arguments is offered to $f$; it then gives the $i$-th argument-builder $b_i^{+}$ the block starting at ${\gamma }_i$, and the codomain test $c^{-}$ the block starting at ${\gamma }_{k+1}$. The blocks are consecutive and disjoint, which is what makes the designated monomial multilinear.

Proof of Lemma 171.44 — Parameter budget

Proof. Induction on $\sigma$. At $\iota$, the interpretations $\widehat{[[m^{+}]]}(u)=e_m$ and $\widehat{[[m^{-}]]}(u)(w)=w_m{e}_0$ do not mention $u$, and $|m{|}^{\pm }=0$.

At $\phi ⟶\psi$, read the second display of definition 171.43. The coordinates of $u$ that occur are $u_0,\dots ,u_{k-1}$; those occurring in $\widehat{[[b_i^{+}]]}(u\{{\gamma }_i\})$, which by the induction hypothesis are among $u_{{\gamma }_i},\dots ,u_{{\gamma }_i+|b_i{|}^{+}-1}$, that is among $u_{{\gamma }_i},\dots ,u_{{\gamma }_{i+1}-1}$; and those occurring in $\widehat{[[c^{-}]]}(u\{{\gamma }_{k+1}\})$, which are among $u_{{\gamma }_{k+1}},\dots ,u_{{\gamma }_{k+1}+|c{|}^{-}-1}$. The union of these index sets is $\{0,\dots ,|a{|}^{-}-1\}$ because ${\gamma }_{k+1}+|c{|}^{-}=k+\sum _i|b_i{|}^{+}+|c{|}^{-}=|a{|}^{-}$. The argument for $a^{+}$ is the same computation with $\beta$ in place of $\gamma$ and $|a{|}^{+}={\beta }_{k+1}+|c{|}^{+}$. ◻

Proof of Theorem 171.47 — Separation

Proof. Put $\phi (x)=\widehat{[[a^{-}]]}(x)(w{)}_0$ and ${\phi }^{\prime }(x)=\widehat{[[a^{-}]]}(x)(w^{\prime }{)}_0$ for $x$ ranging over the box $B=[0,1/n{]}^{\{0,\dots ,n-1\}}$, each such $x$ being read as the element of $({\mathbb{R}}^{+}{)}^{\mathbb{N}}$ that vanishes from index $n$ on. Every such $x$ lies in $PN$, since . By lemma 171.44 both functions are power series in $x_0,\dots ,x_{n-1}$ with nonnegative coefficients, and both are finite on $B$, being coordinates of elements of $PN$. By convention 171.46 their coefficients at the monomial $x_0\cdots x_{n-1}$ are $w_a$ and $w_a^{\prime }$, which differ. By lemma 171.26 the two functions are not equal on $B$.

Both are continuous on $B$: with $\delta =1/n$, the series $\sum _{\nu }{c}_{\nu }{\delta }^{\mathrm{\#}\nu }$ converges, so the series converges uniformly on $B$ by comparison, and each partial sum is a polynomial. Hence $\{x\in B\mid \phi (x)\ne {\phi }^{\prime }(x)\}$ is a nonempty relatively open subset of $B$, and therefore contains a point $q$ all of whose coordinates are rational. For that point, $\widehat{[[a^{-}]]}(q)(w{)}_0\ne \widehat{[[a^{-}]]}(q)(w^{\prime }{)}_0$, which is stronger than the stated inequality. Finally because $q\in B$. ◻

Proof of Theorem 171.48 — Observational equivalence implies denotational equality

Proof. Contrapositive. Assume $[[M{]]}_{\mathrm{\Gamma }}\ne [[M^{\prime }{]]}_{\mathrm{\Gamma }}$ with $\mathrm{\Gamma }=(x_1:{\sigma }_1,\dots ,x_l:{\sigma }_l)$. Close both terms: $N=\lambda x_1^{{\sigma }_1}.\cdots \lambda x_l^{{\sigma }_l}.M$ and $N^{\prime }=\lambda x_1^{{\sigma }_1}.\cdots \lambda x_l^{{\sigma }_l}.M^{\prime }$, both closed of type $\tau ={\sigma }_1⟶\cdots ⟶{\sigma }_l⟶\sigma$. By the abstraction clause of definition 171.29 and theorem 171.27, $w=[[N]]$ and $w^{\prime }=[[N^{\prime }]]$ differ, so $w_a\ne w_a^{\prime }$ for some $a\in |[[\tau ]]|$. Let $n=|a{|}^{-}$ and let $q_0,\dots ,q_{n-1}$ be the rationals given by theorem 171.47, so that with , $$\widehat{[[a^{-}]]}(u)(w{)}_0\ne \widehat{[[a^{-}]]}(u)(w^{\prime }{)}_0.$$ By definition 171.42, $u=[[\mathrm{ran}(q_0,\dots ,q_{n-1})]]$. Take the observation context $$C^{\mathrm{\Gamma }⊢\sigma }=a^{-}\mathrm{ran}(q_0,\dots ,q_{n-1})(\lambda x_1^{{\sigma }_1}.\cdots \lambda x_l^{{\sigma }_l}.[{]}^{\mathrm{\Gamma }⊢\sigma }),$$ which satisfies $\cdot ⊢C^{\mathrm{\Gamma }⊢\sigma }:\iota$. Its two fillings have, by definition 171.29, $[[C[M]]]=\widehat{[[a^{-}]]}(u)(w)$ and $[[C[M^{\prime }]]]=\widehat{[[a^{-}]]}(u)(w^{\prime })$. Hence $$\mathrm{Red}(\iota {)}_{C[M],\bar{0}}^{\mathrm{\infty }}\stackrel{theorem171.39}{=}{[[C[M]]]}_0\ne {[[C[M^{\prime }]]]}_0\stackrel{theorem171.39}{=}\mathrm{Red}(\iota {)}_{C[M^{\prime }],\bar{0}}^{\mathrm{\infty }},$$ so $M$ and $M^{\prime }$ are not observationally equivalent. ◻

Proof of Corollary 171.49 — Equational full abstraction

Proof. Theorem 171.41 and theorem 171.48. ◻

The boundary of the theorem

Corollary 171.49 is an equality of equivalences, not of orders, and it is proved for the frozen calculus of convention 171.1. Both restrictions are real.

Proof of Proposition 171.50 — The matrix order is finer than the pointwise order

Proof. The $\mathsf{if}$ clause of definition 171.29 applied to $[[x{]]}_{x:\iota }(u)=u$ gives $\widehat{[[M_1]]}(u)=u_0{e}_0+\sum _n{u}_{n+1}\cdot 0=u_0{e}_0$, and applying it twice gives $\widehat{[[M_2]]}(u)=u_0\cdot (u_0{e}_0)$. Since $u_0\le 1$ we have $u_0^2\le u_0$. The entries are read off definition 171.23: $u_0=u^{[0]}$ and $u_0^2=u^{[0,0]}$. ◻

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 171.20, then exercise 171.21, then the practical project exercise 171.25.

Exercise 171.20¶

★☆☆ For the two terms of example 171.16 and the two contexts $C_0={\mathsf{prob}}_0[]$ and $C_1={\mathsf{prob}}_1[]$, write the four complete reduction trees, label every edge with its probability, and confirm the four numbers $1/2$ by lemma 171.9.

Referenced from 3 locations

• Probabilistic Lambda Calculi and Program Equivalence

Exercise 171.21¶

★★☆ Write in full the case $M=\mathsf{if}(P,Q,z\cdot R)$ of theorem 171.38 for $h=1$, displaying the instance of lemma 171.36 used, the three consequences of the induction hypothesis, and the final inequality. State where the hypothesis $\bar{k}{R}_{\iota }{e}_k$ is used.

Referenced from 3 locations

• Probabilistic Lambda Calculi and Program Equivalence

Exercise 171.22¶

★★☆ Let $G_p$ be the program of example 171.5 with $\mathsf{coin}(1/2)$ replaced by $\mathsf{coin}(p)$ for a rational $p\in (0,1)$. Compute its result distribution operationally and its denotation, and determine for which pairs $p\ne p^{\prime }$ the observation context ${\mathsf{prob}}_0[]$ separates $G_p$ from $G_{p^{\prime }}$.

Referenced from 2 locations

• Probabilistic Lambda Calculi and Program Equivalence

Exercise 171.23¶

★★☆ Exhibit a closed $M:\iota$ with $[[M]]=0$ that is not ${\mathrm{\Omega }}_{\iota }$, prove $M{\approx }_{}{\mathrm{\Omega }}_{\iota }$ using theorem 171.41, and explain why no finite set of observation contexts establishes this equivalence.

Referenced from 2 locations

• Probabilistic Lambda Calculi and Program Equivalence

Exercise 171.24¶

★★★ Reconstruct the proof of theorem 171.47 for $\sigma =\iota ⟶\iota$ without appealing to convention 171.46: compute $\widehat{[[a^{-}]]}(u)(t)$ for a general $a=([b_1,\dots ,b_k],c)$ at this type, identify the coefficient of $u_0\cdots u_{k-1}$ directly, and carry out the analytic argument. State exactly which part of the general induction the computation replaces.

Referenced from 2 locations

• Probabilistic Lambda Calculi and Program Equivalence

Exercise 171.25¶

★★★ Practical project.ppcf-exact-enumerator Build an exact enumerator for the recursion-free fragment of convention 171.1: numerals, variables, $\mathsf{succ}$, $\mathsf{coin}(p)$ with $p$ a reduced rational, $\mathsf{if}$, abstraction, and application, extended by the closed terms ${\mathsf{prob}}_0$ and ${\mathsf{prob}}_1$ of definition 171.14 with ${\mathrm{\Omega }}_{\iota }$ represented as an explicit divergent constant. The program has three parts: a weak-reduction stepper implementing Det, Coin-0, Coin-1, Ctx-App, Ctx-Succ and Ctx-If with capture-avoiding substitution; an enumerator that accumulates path weights into a finite map from numerals to exact rationals, following lemma 171.9; and a stream-driven tracer that consumes a fixed list of bits and prints one line per draw, conditional and return.

The invariant to maintain is that the accumulated weights of a term never exceed $1$ and that a term with no applicable rule contributes its own weight to the divergence mass rather than to any numeral. The concrete result is the pair of exact rational tables for $M=\mathsf{coin}(1/2)$ and $N=\mathsf{if}(\mathsf{coin}(1/2),\bar{0},z\cdot \bar{1})$ together with the four context probabilities of example 171.16.

The acceptance test is decidable and exact: the tables for $M$ and for $N$ must both be $\{\bar{0}\mapsto 1/2,\bar{1}\mapsto 1/2\}$; each of the four terms $C_0[M]$, $C_1[M]$, $C_0[N]$, $C_1[N]$ must have $\mathrm{Red}(\iota {)}_{-,\bar{0}}^{\mathrm{\infty }}=1/2$; the trace on the bit stream beginning with $0$ must be $\mathtt{draw}\mathtt{0}$, $\mathtt{cond}\mathtt{0}$, $\mathtt{return}\mathtt{0}$ for $N$, and the trace on the stream beginning with $1$ must be $\mathtt{draw}\mathtt{1}$, $\mathtt{cond}\mathtt{1}$, $\mathtt{return}\mathtt{1}$; and the enumerator must report divergence mass $1/2$ for $\mathsf{if}(\mathsf{coin}(1/2),\bar{0},z\cdot {\mathrm{\Omega }}_{\iota })$. All arithmetic is on reduced rationals; a frequency obtained by sampling is not an accepted answer, and the rational tables decide equality of result distributions only, not the universal quantification over contexts in definition 171.13.

Referenced from 3 locations

• Probabilistic Lambda Calculi and Program Equivalence