ch:interaction-trees: ch:interaction-trees

Two uses of (Bind-Tau) give All three steps are judgmental bind computations. Two finite applications of Eutt-TauL then give $\mathsf{eutt}(\mathsf{Tau}(\mathsf{Tau}(k(3))),k(3))$; that last relation is weak equivalence, not judgmental equality.

Let $B(t,u)$ relate only the pair $(\mathsf{bind}(\mathsf{spin},k),\mathsf{spin})$. Unfolding both components once gives The two continuations are again in $B$, so matched-silent coinduction proves strong bisimilarity.

Suppose $\mathsf{eutt}(\mathsf{spin},\mathsf{Ret}(b))$. A finite number of Eutt-TauL uses leaves the left observation equal to $\mathsf{Tau}(\mathsf{spin})$ again. The right observation is a return. Neither Eutt-Ret, Eutt-Vis, nor Eutt-Tau aligns these forms, and Eutt-TauR cannot apply to a return. Hence no one-layer witness exists. Termination sensitivity is exactly the requirement that asymmetric silent stripping occurs in a finite inductive derivation.

Let $G$ carry state and output events. Define $$H(\mathsf{Read}):=\mathsf{Vis}(\mathsf{Get},\mathsf{Ret}),J(\mathsf{Write}(n)):=\mathsf{Vis}(\mathsf{Emit}(n),\lambda u.\mathsf{Ret}(u)).$$ Their copair sends $\mathsf{inl}(\mathsf{Read})$ to $H$ and $\mathsf{inr}(\mathsf{Write}(n))$ to $J$. For the program that reads and writes its answer, The outer $\mathsf{inl}$ selects $H$ before the read continuation receives $x$; the inner $\mathsf{inr}$ selects $J$ after that substitution. Removing the tags would leave no branch-selection datum.

Use the coinductive relation containing, for each $t$, $$(\mathsf{map}(g,\mathsf{map}(f,t)),\mathsf{map}(g\circ f,t)).$$ At $t=\mathsf{Ret}(a)$, both sides compute to $\mathsf{Ret}(g(f(a)))$. At $t=\mathsf{Vis}(e,k)$, the two sides compute to visible nodes with the same $e$; their continuations are the displayed pair at $k(x)$, so Eutt-Vis applies. At $t=\mathsf{Tau}(u)$, both sides compute to one $\mathsf{Tau}$ around the displayed pair at $u$, so Eutt-Tau applies. If the given weak witness first strips a silent node on only one side, restore it with Eutt-TauL or Eutt-TauR. These cases form a post-fixed point, and coinduction proves the fusion equation.

Use $S_2(t,v):=\mathrm{\exists }u.\mathsf{eutt}(t,u)\wedge \mathsf{eutt}(u,v)$. Suppose the left witness strips two silent nodes and the right witness strips one before exposing aligned nodes $t_0,u_0,v_0$. Apply the matching return, visible, or paired-silent generator to $t_0$ and $v_0$; in a visible case, use the coinduction hypothesis pointwise on their continuations. Restore the left constructors by two applications of Eutt-TauL. Restore the right constructor by one application of Eutt-TauR. Thus the outer result lies in $\mathsf{EuttF}(S_2,-,-)$. Finiteness of the three restorations is the side condition needed by the nested fixed-point definition.

Define the write handler $$D(\mathsf{Write}(n)):=\mathsf{Vis}(\mathsf{Write}(n),\lambda u.\mathsf{Vis}(\mathsf{Write}(n),\mathsf{Ret})),$$ and let it preserve reads. A source prefix $\mathsf{Read};\mathsf{Write}(3);\mathsf{Read};\mathsf{Write}(5)$ becomes $$\mathsf{Read};\mathsf{Write}(3);\mathsf{Write}(3);\mathsf{Read};\mathsf{Write}(5);\mathsf{Write}(5).$$ Each doubled pair follows from (Interp-Vis) and two bind computations.

The host equation $p:=p$ has no enclosing $\mathsf{Tau}$ and no visible continuation. It therefore supplies no outer observation and violates the guard condition of definition 86.1. The frozen interpreter does not admit it as an interaction tree.