ch:interaction-nets: ch:interaction-nets

Problem and result. Implement unary interaction-net arithmetic and a validating work queue. The eight cases compute $3+2$ in four interactions, join two one-step schedules, agree on two normalization schedules, check erasure and duplication counts, enforce unordered rule uniqueness and boundary arity, and obtain work two, span one, and zero readback for the independent void candidates.

Invariant. After every accepted rewrite, each live internal port has exactly one peer, the peer map is symmetric, every peer is live and in range or is a declared boundary endpoint, and no retired port is reachable. A queue entry authorizes no write until current incidence validates it. For the HVM2 frontier, compute span from the declared dependency bit: two live independent candidates have span one, while the sequential witness has span two.

Representation. Use agent symbols with ordered auxiliary ports, unordered principal-pair rule keys, and a queue of candidate principal connections. Encode the arithmetic fragment as finite states. A general pointer graph would be closer to an engine, but the algebraic representation makes boundary and scheduling invariants decidable by structural recursion.

First complete version. Implement the zero and successor addition interactions and read back the unary result. Record the interaction count; $3+2$ must produce five after exactly four rule applications.

Remaining cases. Add two independent redexes and compare left-first with interleaved schedules. Validate rule-key uniqueness and boundary arity before enqueuing. Then add the finite erasure/duplication observations and the two-candidate work/span calculation.

A failing version. In the successor rule, recurse without incrementing the output accumulator. The mutant remains typechecking and audit-clean, but the arithmetic result and its frozen oracle disagree.

Acceptance test. Run the four commands in appendix E. Require all eight PASS lines, failure of each isolated mutation, the audit output [], and the final line

Mathematical boundary. These finite schedules illustrate local rewriting and queue validation. They illustrate the safety half of proposition 41.22 and the commuting square used by theorem 41.9. They do not prove either statement, general development independence, lambda simulation, universality, optimality, or HVM2 correctness.