Solutions for Chapters 57–59

In E-Pair, replace the premise counter pair $(q+K^{\mathsf{pair}},q)$ by $(q+a+K^{\mathsf{pair}},q+a)$; the heap and freshness premises are unchanged. The cons case is identical. For let, shift the first premise by $a$, so its residual counter and the second premise’s initial counter both increase by $a$; then shift the second premise by the same amount and rebuild the let rule. The inequality $a\ge 0$ keeps every shifted intermediate counter in ${\mathbb{Q}}_{\ge 0}$.

Since $n^2=n+2(\genfrac{}{}{0ex}{}{n}{2})$, $$-3n+3n^2=6(\genfrac{}{}{0ex}{}{n}{2}),14n+14n^2=28(\genfrac{}{}{0ex}{}{n}{1})+28(\genfrac{}{}{0ex}{}{n}{2}).$$ All binomial-basis coefficients are nonnegative even though the first monomial expansion has a negative linear coefficient.

Coefficientwise addition gives $(p_2+3,0)+(0,p_2+3)=(p_2+3,p_2+3)$, so the list-sharing rule applies after sharing the element type with itself. The first occurrence carries linear potential and pays the traversal by $\mathsf{attach}$ and the copied spine in $\mathsf{append}$. The second retains the degree-two coefficient needed by the recursive call on the tail.

Let $f(x)=f(x)$. The call $f(0)$ has no terminating big-step derivation, so the theorem’s evaluation premise cannot be supplied even if a cyclic typing annotation were written. For the heap premise, put $\mathrm{\Gamma }=x:L^{(1)}(\mathsf{int}),V(x)=\ell$, and leave $\ell$ outside the domain of $H$. Following the list clause of ${\mathrm{\Phi }}_{V,H}$ then requires $H(\ell )$, which is undefined.

On an input of length $n+1$, $\mathsf{attach}$ allocates $n$ pairs and $n$ result cons cells, and $\mathsf{append}$ copies $n$ cons cells. Thus $P(0)=0$ and $P(n+1)=P(n)+3n$. Summing gives . The local type bound is exact. The printed analyzer output is $6(\genfrac{}{}{0ex}{}{n}{2})$, twice as large, and is still safe.

For zero-potential payloads, a root with two leaf children has potential $$p_1+2(\mathsf{C}\overrightarrow{p}{)}_1=p_1+2(p_1+p_2).$$ A full tree of height $h$ satisfies $T(0,\overrightarrow{p})=0$ and $T(h+1,\overrightarrow{p})=p_1+2T(h,\mathsf{C}\overrightarrow{p})$. The recurrence depends on every node having exactly two children and therefore does not reduce an arbitrary tree to height alone.

Treat a natural number as a channel protocol $\mathsf{Nat}$. The provider type is $$\mathsf{Nat}⊸((\mathsf{Nat}\otimes \mathbf{1})\oplus \mathbf{1}).$$ The provider receives the request, selects quote or refusal, and in the quote branch sends the result channel before becoming inactive; the client sends, branches on the provider’s label, receives in the quote branch, and likewise becomes inactive. Type $\mathbf{1}$ adds no close/wait communication in the selected pi calculus.

Create sessions $x$ and $y$. Let the left process receive first on $x$ and then send on $y$, while the right process receives first on $y$ and then sends on $x$. Each endpoint can follow its local protocol, but both leading actions are inputs. Preservation has no premise that creates a redex. Such an independently composed cycle is not a closed proof term $\cdot ;\cdot ⊢P::z:\mathbf{1}$ of the selected single-conclusion calculus, so it cannot instantiate the closed-progress theorem.

One server protocol is The client dual exchanges with $\oplus$ and $⊸$ with $\otimes$, while $\mathbf{1}$ remains $\mathbf{1}$. Unfolding once substitutes $S$ for $t$; unfolding the dual substitutes $\bar{S}$ for its recursive variable. Both expose matching opposite choice and communication constructors, so the coinductive duality clause continues beneath the same guard. The only transmitted session type is the closed $\mathsf{Nat}$, so this example satisfies the chapter’s tail-recursion restriction.

For SingleAction, use a promoted body with two visible session actions; duplicating it makes the shared endpoint’s one-action interface ambiguous. For ReceivePrefix, put a send before the repeated receive; clients wait for the replicated input while the body waits on an unallocated output. For Sends, use a multicast body whose leading action is receive; the advertised recipient buffers have no messages. Each counterexample removes only the syntactic premise that connects allocation to the next operational action.

Invert the provider’s $\otimes$R premise into $\mathrm{\Gamma };{\mathrm{\Delta }}_1⊢P::y:A$ and $\mathrm{\Gamma };{\mathrm{\Delta }}_2⊢Q::x:B$. Invert the client’s $\otimes$L premise into $\mathrm{\Gamma };{\mathrm{\Delta }}_3,y:A,x:B⊢R::z:C$. Cut first at the strict subformula $y:A$, obtaining $\mathrm{\Gamma };{\mathrm{\Delta }}_1,{\mathrm{\Delta }}_3,x:B⊢(\nu y)(P\mid R)::z:C$. Cut that result against $Q$ at the strict subformula $x:B$. The union ${\mathrm{\Delta }}_1,{\mathrm{\Delta }}_2,{\mathrm{\Delta }}_3$ is the original external linear context, and the resulting process is the displayed tensor reduct up to reassociation.

Take $\pi .Q=x.\mathsf{inl};P$. This is a nonreplicated guarded selection, so the restricted parallel process has the required $(\nu \tilde{n})(\pi .Q\mid R)$ form. The matching branch guard is likewise nonreplicated. Neither is an input/output prefix. An input/output-only definition would therefore declare the state non-live immediately before its principal choice contraction, preventing the closed-progress theorem from supplying that contraction.

Unfolding gives $S\simeq \mathbf{1}⊸S$, so T-Rec-Conv exposes a receive before the finite $⊸$R or $⊸$L rule is inverted. The auxiliary endpoint view is $\bar{S}=\mu t.(\mathbf{1}\otimes t)$, whose unfolding is $\mathbf{1}\otimes \bar{S}$. The carried type $\mathbf{1}$ is closed and the recursive occurrence lies in the continuation; hence the tail-recursion condition holds.

For projectability, let $p$ choose whether $r$ sends a Boolean or an integer to $s$ without informing $r$; the projections at $r$ disagree. For linearity, let independent $p$ and $r$ send differently typed values to $q$ on the same address; either value may reach the head first. For unstuckness, use $$p\to q:k_1\{{\ell }_1:q\to r:k_2⟨\mathsf{Bool}⟩.\mathsf{end},{\ell }_2:p\to r:k_2⟨\mathsf{Bool}⟩.\mathsf{end}\}.$$ The relaxed barb relation sees the $p$-to-$r$ action in the second branch, but the true rule cannot move it beneath the choice because the first branch has no action with that label. The first example fails full projection, the second has no dependency chain ordering the sends, and the third has a relaxed barb without a matching global transition. A wrong sender at a concrete queue head is instead rejected by queue typing and coherent decomposition.

Choose a fresh address $k_5$. In both bank continuations, append $B\to K:k_5⟨\mathsf{Address}⟩.\mathsf{end}$ after the $\mathsf{done}$ notification. The projection at $B$ continues with $!k_5⟨\mathsf{Address}⟩.\mathsf{end}$, and the projection at $K$ receives the address in either branch. The projection at $S$ skips the receipt action. After the final $k_3$-receive, the trace appends $({\mathsf{address}}_B{)}_{k_5}$ and consumes it. Extending only the $\mathsf{ok}$ branch would give $B$ unequal branch projections, so (Plain-Branch) would be undefined.

Let $A$ evaluate a Boolean and select yes/no to $B$. In the first branch $B$ sends $1$ to $C$; in the second it sends $0$. Projection gives $A$ the conditional and the selection, $B$ an offer whose continuations send the two distinct expressions, and $C$ a receive in both branches. Deleting the selection leaves $B$ uninformed. Its two branch projections contain sends with unequal local expressions, so their partial merge is undefined; the two receive projections at $C$ retain the same control shape and merge.

At $B\to S:k_1$, projection gives output to $B$, input to $S$, and the continuation to $K$. The $S\to K:k_2$ action is analogous. At the bank choice on $k_4$, $K$ selects and $S$ offers. Role $B$ is uninvolved, and both continuations project to the literal same local type ; hence Plain-Branch applies. The resulting types are exactly $(T_B,T_S,T_K)$ printed in the chapter. Every address occurs in one global action, so there is no pair of same-address actions to which the linearity implication applies; that condition is independently true, vacuously.

The initial queues are empty. A send row appends the item named by the sender’s outer local action to its unique empty address and advances only that sender. The following receive row checks the same sender, payload or label, and address at the head, removes it, and advances only the receiver. Thus the invariant alternates between one prescribed singleton queue and four empty queues through all four interaction pairs. If $k_2=k_4$, the debit and bank label share a queue; the proof can no longer infer from the address alone that the current singleton is the item prescribed by the receiver’s outer action. The separate dependency proof required by linearity would then be needed.

MPST assumes a coherent runtime witness—projectability, linearity, and unstuckness—and concludes preservation of a process/session/queue typing with either an unchanged or globally advanced witness. Pirouette instead assumes a location-coverage condition and defined endpoint projection, and concludes existence of a choreography step whose re-projection is below the stepped control system in ${\le }_{\mathsf{nd}}$. MPST has asynchronous typed queues but no choreography term; Pirouette has a synchronous source program and partial merge but no MPST coherence witness. Their premises and reducts therefore inhabit different judgments, so neither theorem instantiates the other.