ch:interaction-trees: ch:interaction-trees

Problem, calculus, and result. Build the finite observer for the guarded interaction-tree fragment of definition 86.1. The program must print the successor-server prefix on input $[2,4]$, preserve that prefix after one inserted silent step, classify a budgeted pure silent loop as silent-prefix, and reject the mutation that writes $x$ instead of $x+1$.

Representation and invariant. Represent visible observations by Read Nat and Write Nat; represent an internal observation by TauStep. The server consumes a finite input list and returns a finite event list. The observer erases only TauStep. The invariant is that the remaining list alternates a read of $x$ and a write of $x+1$ for each consumed input. A recursive host value would resemble the mathematical tree more closely, but it would require unchecked cyclic data or a coinductive host feature. The finite list makes the evidence boundary and termination measure explicit.

First complete version. Define server by structural recursion on inputs. The empty list returns no events. The successor branch emits Read x, then Write (x + 1), then recurses. Add structural equality on events and lists. This version already checks the exact four-event oracle.

Remaining cases in metatheory order. Add eraseTau for the weak-step test, mirroring the two asymmetric silent rules of definition 86.4. Add the budgeted process classification with distinct ImmediateReturn and PureTauLoop cases; do not report the latter as return. Finally run the same oracle against the mutated server.

A failing version. Replace Write (x + 1) by Write x. On input $[2,4]$ the first write becomes $2$, so equality with the named oracle fails at the second event.

Acceptance test. Run the four commands in appendix E. Require the exact server trace, the one-silent-step PASS, the silent-prefix classification, the mutation PASS, the final four-case summary, and audit output [].

Mathematical boundary. The run illustrates theorem 86.11. It does not prove that weak equivalence is transitive, that bind is a congruence, that interpreters compose, or that the guard condition is complete.