The Island Reading Room / Independent check
The same exchange,
checked twice.
The landing coordinator offers a route; the delivery coordinator responds with a proposed plan. Does a separate implementation of symmetric feedback give the same outside answer?
Inspect the check ↓
01 / A second instrument
Two implementations, one exterior question
The Reading Room experiment runs typed partial functions in JavaScript. This check re-authors the two island policies as Boolean matrices in DisCoPy’s Int construction. Each true cell says an input may reach an output. DisCoPy closes the two B wires with its trace; we compare only the A and C boundary.
A separate delivery request enters at C⁻ and may emerge as a request for an inspector report at A⁻. The inspector’s reply is another external input; neither implementation manufactures it.
02 / A small but consequential translation
The output wires change order
The Reading Room writes f : A⁺ ⊔ B⁻ ⇀ A⁻ ⊔ B⁺, following the photographed two-box convention. In DisCoPy 1.2.2, the executable interaction.Diagram constructor requires its inner map’s output columns in the order B⁺ ⊔ A⁻. The two presentations are related by a symmetry, but column 1 cannot simply be copied into column 1.
Without that translation, an available jetty falsely appears to produce the boxes plan. Explicitly relabelling the columns makes the implementations agree. DisCoPy’s 1.2.2 API prose describes the opposite codomain order; this check follows the version-pinned constructor and checks that it accepts target-positive then source-negative wires and rejects their reversal. The discrepancy is in documentation versus implementation, and neither order changes the proposed plan once the wires are labelled correctly.
03 / The bounded result
Which outside inputs reach which outputs?
Choose the two policies and a diagnostic case. The matrix shows DisCoPy’s exterior relation after B is hidden. The last column shows the separate JavaScript result for the same input. Each displayed case was generated by the checked Python reproduction, not recomputed by this page.
| Exterior input | A⁻ survey | C⁺ jetty plan | C⁺ boxes plan | C⁺ hold | JavaScript result |
|---|---|---|---|---|---|
| Loading the checked evidence… | |||||
A zero-output row can mean an absent response or a reached internal cycle. Both are undefined from outside; the Reading Room experiment shows the witness inside.
04 / A genuine difference
What if one report permits two offers?
In one extra DisCoPy case, an available jetty lets the landing coordinator offer either jetty unloading or the shore path. The delivery coordinator maps those offers to different proposed plans.
jetty availableB⁺
jetty or shoreC⁺
jetty plan or boxes plan
The Boolean relation has two marked outputs for one input. That is allowed in Int(Matrix[bool]); the original Int(Pfn) app specifies at most one output. The relation lists possibilities. It does not choose between them, claim both happen, or supply a legal game strategy. A project decision would need a further rule, preference or observation.
05 / What this establishes
A verified fragment, not the whole game
Established here
DisCoPy 1.2.2 and the existing routing model agree on all 48 exterior inputs across 12 finite deterministic cases. The check includes completed routes, missing rules and reachable cycles. DisCoPy’s Boolean matrix exposes possibilities after feedback; the JavaScript trace explains why an empty result occurred.
Still open
This does not verify general Int laws, infer a delivery policy, determine whether a real jetty is safe, or turn a routing table into a game strategy. The branching case is an intentional change of category, not an upgrade silently absorbed into the original model.
Sources and reproduction
Abramsky’s two-box GoI picture identifies the question; DisCoPy’s Int documentation motivates the independent construction, while the versioned constructor source settles the output-order discrepancy; its Boolean matrix trace supplies the computational semantics. The finite island policies, column translation and comparison are our construction.
The Python checker is versioned in the Functors repository; its generated evidence is downloadable here. Return to the interactive Reading Room →