Chapter 86Optional

Recursive Effects and Interaction Trees

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

The guarded corecursor of chapter 33 produces an unbounded stream, but a stream exposes only one fixed kind of observation. A server instead receives a request, chooses a response type from that request, emits the response, and repeats. A finite free-effect tree records only a bounded dialogue. Adding unrestricted recursion records the dialogue but leaves two questions unanswered: which recursive calls are productive, and when may a finite stretch of internal computation be ignored?

A dialogue determines the tree signature

Let $E : U_{i} \to U_{i}$ assign to each answer type $X$ the type $E (X)$ of events whose environment response has type $X$ . For the running server take events $Read : E (N), Write (n) : E (1) (n : N) .$ A read continuation must accept a natural number. A write continuation must accept the unique unit value. This dependence is the reason that an event is indexed by its response type.

Definition 86.1 — Guarded interaction trees ¶

Fix $R : U_{i}$ . The type $ITree (E, R)$ has three observations.

Γ ⊢ r : R

Γ ⊢ Ret (r) : ITree (E, R)

ITree-Ret

Γ ⊢ t : ITree (E, R)

Γ ⊢ Tau (t) : ITree (E, R)

ITree-Tau

Γ ⊢ e : E (X)

Γ ⊢ k : X \to ITree (E, R)

Γ ⊢ Vis (e, k) : ITree (E, R)

ITree-Vis

The constructor $Tau$ records one internal step. Recursive equations are admitted only when every recursive occurrence lies beneath $Tau$ or in a continuation supplied to $Vis$ . This is the guard condition of the frozen tree signature.

Referenced from 5 locations

The finite prefix that reads $2$ , writes $3$ , and stops is $Vis (Read, λ x . Vis (Write (x + 1), λ u . Ret (u))) .$ The type of the outer continuation is $N \to ITree (E, 1)$ ; after the answer $2$ it produces the write event. The write continuation has type $1 \to ITree (E, 1)$ . If the outer continuation were given type $1 \to ITree (E, 1)$ , ITree-Vis would reject the read node before any recursion question arose.

Definition 86.2 — The successor server ¶

The guarded equation $succServer : = Vis (Read, λ x . Vis (Write (x + 1), λ u . Tau (succServer)))$ defines an element of $ITree (E, 0)$ . Here $0$ is the empty return type. The recursive call lies below one visible read, one visible write, and one $Tau$ , so it satisfies the guard condition.

Referenced from 3 locations

Recursive Effects and Interaction Trees

Deleting both visible events leaves $spin : ITree (E, R), spin : = Tau (spin) .$ This equation is guarded, but it never returns and never performs a visible event. Guardedness gives productivity of tree observations; it does not give termination or fairness.

Sequencing preserves the visible protocol

Definition 86.3 — Guarded bind ¶

For terms of the following types, $t : ITree (E, A), k : A \to ITree (E, B),$ define $bind (t, k) : ITree (E, B)$ by the observation equations $\begin{aligned} (B i n d - R e t) & bind (Ret (a), k) & \equiv k (a), \\ (B i n d - T a u) & bind (Tau (t), k) & \equiv Tau (bind (t, k)), \\ (B i n d - V i s) & bind (Vis (e, h), k) & \equiv Vis (e, λ x . bind (h (x), k)) . \end{aligned}$ The recursive calls in the last two clauses occur below $Tau$ and $Vis$ , respectively.

Referenced from 2 locations

Recursive Effects and Interaction Trees

For $q : ITree (E, N)$ and $k : N \to ITree (E, B)$ , the expression $bind (q, k)$ is stuck when $q$ is neutral. The equations above do not inspect an unknown tree. By contrast, $\begin{aligned} bind (Tau (Ret (2)), k) & \overset{(B i n d - T a u)}{\equiv} Tau (bind (Ret (2), k)) \\ \overset{(B i n d - R e t)}{\equiv} Tau (k (2)) . \end{aligned}$ This calculation retains the internal step. The equivalence introduced below will be permitted to erase it.

Exercise 86.1 ¶

★☆☆ Calculate $bind (Tau (Tau (Ret (3))), k)$ through both silent steps. State which of the resulting equalities are judgmental and which later weak equivalence erases the two silent constructors.

Referenced from 4 locations

Finite silence is unobservable

Ordinary syntactic equality distinguishes $t$ from $Tau (t)$ . Identifying every silent computation would instead identify $spin$ with a return, because both could discard arbitrarily many silent steps. The relation must erase any finite number of silent steps while requiring an infinite silent computation to be matched by infinite silence.

Definition 86.4 — Strong and weak tree bisimulation ¶

The strong bisimulation $sbisim (t, u)$ is the greatest relation that matches equal returns, identical visible events with related continuations at every answer, and one $Tau$ on each side.

For a relation $S$ on subtrees, let $EuttF (S, t, u)$ be generated by the following rules.

a = b

EuttF (S, Ret (a), Ret (b))

Eutt-Ret

\forall x : X . S (k (x), h (x))

EuttF (S, Vis (e, k), Vis (e, h))

Eutt-Vis

S (t, u)

EuttF (S, Tau (t), Tau (u))

Eutt-Tau

EuttF (S, t, u)

EuttF (S, Tau (t), u)

Eutt-TauL

EuttF (S, t, u)

EuttF (S, t, Tau (u))

Eutt-TauR

The termination-sensitive weak equivalence $eutt (t, u)$ is the greatest fixed point of the monotone operator $S \mapsto EuttF (S, -, -)$ . The last two rules belong to the inductive layer $EuttF$ : they may remove only a finite number of unmatched silent steps before a coinductive appeal to $S$ .

Referenced from 5 locations

For every $t$ , Eutt-TauL and the matching outer form of $t$ derive $eutt (Tau (t), t) .$ No finite derivation of $EuttF$ can turn $spin$ into $Ret (r)$ : after every finite sequence of Eutt-TauL uses, the left tree is again $spin$ , whereas the right tree exposes a return. This is the first boundary at which the inductive layer matters.

Theorem 86.5 — Weak equivalence laws ¶

For each event family $E$ and return type $R$ , the relation $eutt$ on $ITree (E, R)$ is reflexive, symmetric, and transitive. Moreover, $sbisim (t, u) ⟹ eutt (t, u) .$

Referenced from 3 locations

Recursive Effects and Interaction Trees

Proof of Theorem 86.5 — Weak equivalence laws

Proof. Reflexivity uses the coinductive relation $S_{0} (t, u) : = (t = u)$ . Equal returns use Eutt-Ret; equal visible nodes use Eutt-Vis and the coinduction hypothesis pointwise; equal silent nodes use Eutt-Tau.

For symmetry, close the converse relation $S_{1} (t, u) : = eutt (u, t)$ . The return and visible cases exchange their two arguments. Eutt-TauL becomes Eutt-TauR, and Eutt-TauR becomes Eutt-TauL. Thus every generator is preserved.

Transitivity needs the strengthened relation $S_{2} (t, v) : = \exists u . eutt (t, u) \land eutt (u, v) .$ For a one-layer witness $d$ , let $strip (d)$ be its exposed return, visible, or matched-silent node together with the finite lists of left and right $Tau$ constructors removed by $d$ . Apply this operation first to the left premise. Its middle observation fixes a finite prefix of the middle tree. Apply it to the right premise and extend the shorter of the two middle prefixes by matched uses of Eutt-Tau; the two exposures now name the same middle node. This finite realignment is possible because both prefix lists come from inductive $EuttF$ derivations. If both exposed nodes are returns, their values are equal by transitivity of equality. If they are visible, both premises expose the same middle event, so the outer events coincide; apply the coinduction hypothesis to each pair of continuations. If the aligned nodes are silent, apply Eutt-Tau to the two related continuations. Every stripped constructor is restored with Eutt-TauL or Eutt-TauR. The stripping phases are finite because they are derivations in $EuttF$ . This proves that $S_{2}$ is a post-fixed point and hence lies in the greatest fixed point.

A strong bisimulation uses only the return, visible, and matched-silent cases, which are the first three weak generators. Coinduction therefore gives the last implication. ◻

Theorem 86.6 — Bind congruence and associativity ¶

Assume $eutt (t, u) and \forall a : A . eutt (k (a), h (a)) .$ Then $eutt (bind (t, k), bind (u, h)) .$ Moreover, for $k : A \to ITree (E, B)$ and $h : B \to ITree (E, C)$ , $eutt (bind (bind (t, k), h), bind (t, λ x . bind (k (x), h))) .$

Referenced from 3 locations

Recursive Effects and Interaction Trees

Proof of Theorem 86.6 — Bind congruence and associativity

Proof. Use coinduction with pairs of binds as the strengthened relation. After a finite number of unmatched silent steps in $t$ or $u$ , there are three aligned forms. A return pair reduces by (Bind-Ret) to $k (a)$ and $h (a)$ , related by hypothesis. A visible pair reduces by (Bind-Vis); Eutt-Vis applies, and each continuation is again a pair of binds in the coinductive relation. A matched silent pair reduces by (Bind-Tau) on both sides and uses Eutt-Tau. The unmatched constructors are restored with Eutt-TauL and Eutt-TauR. These are all generators of $EuttF$ .

For associativity, use the coinductive relation containing the displayed pair for every subtree $t$ . At a return, both sides compute to $bind (k (a), h)$ . At a visible node, the two uses of (Bind-Vis) expose the same event and put the continuation pair back in the relation. At a silent node, both uses of (Bind-Tau) expose matched silent constructors. These three cases establish the post-fixed-point obligation; congruence alone is not being used as associativity. ◻

Exercise 86.2 ¶

★★☆ Prove that $bind (spin, k)$ is strongly bisimilar to $spin$ . Then use the return case of definition 86.4 to show that it is not weakly equivalent to $Ret (b)$ for any $b : B$ . State where termination sensitivity enters both arguments.

Referenced from 3 locations

Handlers interpret one signature into another

Definition 86.7 — Handlers and interpretation ¶

A handler from $E$ to interaction trees over $F$ is a dependent function $H : \prod_{X : U_{i}} E (X) \to ITree (F, X) .$ Its interpreter $interp (H, -)$ is determined by $\begin{aligned} (I n t e r p - R e t) & interp (H, Ret (r)) & \equiv Ret (r), \\ (I n t e r p - T a u) & interp (H, Tau (t)) & \equiv Tau (interp (H, t)), \\ (I n t e r p - V i s) & interp (H, Vis (e, k)) & \equiv bind (H (e), λ x . interp (H, k (x))) . \end{aligned}$

Referenced from 2 locations

Recursive Effects and Interaction Trees

The identity handler is $trigger (e) : = Vis (e, Ret)$ . For handlers $H : E \Rightarrow ITree (F)$ and $J : F \Rightarrow ITree (G)$ , define their composite by $(J ⋄ H) (e) : = interp (J, H (e)) .$

Theorem 86.8 — Interpreter identity and composition ¶

For every interaction tree $t$ , $\begin{array}{r} eutt (interp (trigger, t), t), eutt (interp (J, interp (H, t)), interp (J ⋄ H, t)) . \end{array}$

Referenced from 2 locations

Recursive Effects and Interaction Trees

Proof of Theorem 86.8 — Interpreter identity and composition

Proof. For identity, coinduct on $t$ . In the calculation below, I-Vis abbreviates (Interp-Vis), B-Vis abbreviates (Bind-Vis), and B-Ret abbreviates (Bind-Ret). Put $q_{x} : = interp (trigger, k (x))$ . The return and silent cases follow from (Interp-Ret) and (Interp-Tau). At a visible node, $\begin{aligned} interp (trigger, Vis (e, k)) & \overset{I - V i s}{\equiv} bind (Vis (e, Ret), λ x . q_{x}) \\ \overset{B - V i s}{\equiv} Vis (e, λ x . bind (Ret (x), λ y . q_{y})) \\ \overset{B - R e t}{\equiv} Vis (e, λ x . q_{x}) . \end{aligned}$ Apply Eutt-Vis and the coinduction hypothesis.

For composition, strengthen the coinduction relation with the displayed pair of interpretations. The visible case expands the interpreter twice and uses the associativity clause of theorem 86.6. Reassociation leaves the resulting handler exactly $J ⋄ H$ . Return and silent cases use the corresponding interpreter equations. Thus all three observations match. ◻

Definition 86.9 — Tagged sums of signatures ¶

For event families $E$ and $F$ , their tagged sum is $(E +_{E} F) (X) : = E (X) + F (X) .$ Handlers $H : E \Rightarrow ITree (G)$ and $J : F \Rightarrow ITree (G)$ determine the copair $[H, J] (inl (e)) : = H (e), [H, J] (inr (f)) : = J (f) .$ The tags are retained even when $E (X) = F (X)$ ; deleting them makes it impossible to select the intended handler branch.

Referenced from 2 locations

Recursive Effects and Interaction Trees

Exercise 86.3 ¶

★★☆ Let $E$ contain reads and $F$ contain writes. Define handlers for both into a state-and-output signature $G$ , form their copair, and calculate the interpretation of one read followed by one write. Show at which step the $inl$ or $inr$ tag selects the handler.

Referenced from 4 locations

Exercise 86.4 ¶

★★★ Define $map (f, t) : = bind (t, λ x . Ret (f (x)))$ . Prove $eutt (map (g, map (f, t)), map (g \circ f, t))$ by coinduction. Write the visible and unmatched silent cases; the return case alone is not a complete proof.

Referenced from 3 locations

Finite observation of the server

Definition 86.10 — Visible-prefix observer ¶

For a finite list $\bar{x} = [x_{0}, \dots, x_{m - 1}]$ of environment replies and a silent-step budget $b : N$ , use the partial observer ${observe}_{b, 2 m} (t, \bar{x}) .$ It skips at most $b$ consecutive $Tau$ nodes and records the first $2 m$ visible events. At a read it feeds the next $x_{q}$ to the continuation. At a write it feeds the unit value. It reports $silent - prefix$ if its entire budget is spent on $Tau$ nodes. This result is not a termination claim.

Referenced from 2 locations

Recursive Effects and Interaction Trees

Theorem 86.11 — Successor-server prefix ¶

For every $m : N$ , budget $b \geq 1$ , and input list $[x_{0}, \dots, x_{m - 1}]$ , the first $2 m$ visible events of $succServer$ are $read (x_{0}); write (x_{0} + 1); \dots; read (x_{m - 1}); write (x_{m - 1} + 1) .$ Inserting a silent prefix of length at most $b$ before any visible event preserves this prefix. Every finite insertion is therefore accepted by some finite choice of $b$ . The observer applied to $spin$ reports $silent - prefix$ at every finite budget and never reports a return.

Referenced from 3 locations

Proof of Theorem 86.11 — Successor-server prefix

Proof. Induct on the input list. The empty list requests no visible events. For $x :: \bar{x}$ , unfold definition 86.2. The first visible node is $Read$ ; feeding $x$ exposes $Write (x + 1)$ ; feeding unit exposes $Tau (succServer)$ . The observer skips this one silent node and the induction hypothesis computes the remaining prefix from $\bar{x}$ . Each additional finite silent prefix is removed by one more finite observer step, so it does not change the recorded events.

For $spin$ , every finite unfolding uses $spin \equiv Tau (spin)$ . Induction on the search budget shows that no visible or return node is reached. The observer therefore reports $silent - prefix$ rather than termination. ◻

At input $[2, 4]$ , the calculation gives $read (2); write (3); read (4); write (5) .$ This is a finite-observation theorem. It neither schedules competing servers nor proves fairness for an external event implementation.

Suggested first pass.

None of these problems is a prerequisite. Begin with exercise 86.1 and exercise 86.3; for the practical sequence, complete stages 1–3 before stages 4–5.

Exercise 86.5 ¶

★★★ Reconstruct the transitivity proof of theorem 86.5 for the case in which the left premise strips two silent nodes and the right premise strips one. Display the strengthened relation, the aligned observation, and the three rules that restore the silent nodes.

Referenced from 3 locations

Exercise 86.6 ¶

★★☆ Give a handler that maps each write event to two writes. Calculate the first four source events and the corresponding target prefix. Then give a nonproductive host-language function that the frozen guarded interpreter signature does not admit; identify the missing guard.

Referenced from 3 locations

Exercise 86.7 ¶

★★★ Practical project.recursive-effect-interpreter Build a Kappa finite observer in five declared stages: (1) the tree/event representation, (2) the visible-prefix observer, (3) the successor server, (4) a weak-step test that ignores one inserted silent step, and (5) a budgeted silent-divergence detector. Maintain the invariant that every recorded event is visible and appears in protocol order. On input [2,4], print exactly read 2; write 3; read 4; write 5; the tree with one inserted silent step must print the same prefix; and a pure silent loop must print silent-prefix, never a return. Mutating the write response from $x + 1$ to $x$ must fail the named prefix test.

Referenced from 4 locations

Sources. The tree signature, guarded bind, termination-sensitive weak bisimulation, and interpreter laws follow Xia, Zakowski, He, Hur, Malecha, Pierce, and Zdancewic’s frozen POPL interaction-tree development. Its Figure 4 uses an inductive layer inside the greatest fixed point so that only finitely many unmatched silent steps are removed. The Kappa observer checks the finite server calculation; it is not a replay of the source’s Rocq proofs. The precise source is [yXZH^+20].