| paper | d4-conf-atal-2010-0263 |
| authors | — |
| venue | ? |
| filed under | unclassified |
| judged by | gpt-6-luna / xhigh (triple__luna__xhigh__c6r1) |
| judge confidence | medium |
| authors would recognise it | yes |
P→P discrete result → its continuous mirror
Answer: Polynomial-time solvable for both \(\sigma=\mathrm{weak}\) and \(\sigma=\mathrm{strong}\). Exact fraction output takes \(O(\tau n(m+1)+L^2)\) bit operations using bit vectors, or \(O(L^2)\) using direct literal-list comparisons. · discrete side: polynomial · adjudication: proved
full proof & adversarial review →
Theorem 7.1
statement extracted from the paper’s text layer
Given a shared protocol \(\alpha\) with explicit characterisations, a mode \(\sigma\in\{\mathrm{weak},\mathrm{strong}\}\), and a rational distribution \(\mu\) over supported types \(t=(\psi_t,\phi_t)\), what exact mass of the society has a type for which \(\alpha\) matches from \(\psi_t\) to \(\phi_t\) in mode \(\sigma\)?
Types include each agent feature relevant to matching, including role, library, initial state, and goal. For each supported type, evaluate the paper’s weak or strong matching predicate for \(\alpha\), then return \(\sum_{t\in T}\mu_t\,\mathbf{1}[\alpha\text{ matches }t]\). With explicit characterisations, this takes at most \(2\tau n\) entailment checks in the paper’s cost model, plus exact rational summation.
Covers Theorem 7.1’s characterisation-based weak and strong matching bound applied to supported initial-state and goal types; leaves the paper’s characterisation results for iterative and recursive protocols unaggregated.
The best positive case is a narrow, batch version of the paper’s own protocol-matching problem. It makes the population continuous while keeping each agent’s matching question intact.
A plausible regime is a large deployment of software agents running the same workflow and sharing the same protocol library. At a decision point, agents may differ in their current commitment state and goal, but many have the same pair of propositions. Treat \(t=(\psi_t,\phi_t)\) as an agent type, with the common library understood; any role or library differences that affect matching would also have to be part of the type. A society is a rational distribution \(\mu\) over the \(\tau\) supported types. Each actual agent still executes an ordinary protocol: \(\mu_t\) records a share of the population, not a fractional agent or protocol.
My lead anchor is Theorem 7.1, proved in this paper. It states that the worst-case complexity of both strong and weak matching is \(e+2n\) for depth-first search and \(2n\) for the authors’ characterisation-based matching method. Here \(e\) is the number of edges in the protocol syntax tree, and \(n\) is the number of paths through the protocol, equivalently the number of characterisations. Thus, in the paper’s cost model, the method reduces the bound from \(O(e+n)\) to \(O(n)\). This is an algorithmic anchor; the paper does not provide a named hardness result for protocol matching.
The continuous problem I would hand to a prover is Continuous Protocol Coverage. An instance consists of a finite supported set \(T\), binary-rational masses \(\mu_t\geq 0\) summing to one, an initial-state proposition \(\psi_t\) and goal proposition \(\phi_t\) for each type, a protocol \(\alpha\) from a shared library, and a mode \(\sigma\in\{\mathrm{weak},\mathrm{strong}\}\). The protocol’s characterisations are supplied explicitly, as in the paper’s matching method. Return the exact rational mass of types for which \(\alpha\) matches:
\[ \operatorname{Cov}_{\mathrm{weak}}(\alpha,\mu) =\sum_{t\in T:\,\psi_t\to\langle\alpha\rangle\phi_t}\mu_t, \qquad \operatorname{Cov}_{\mathrm{strong}}(\alpha,\mu) =\sum_{t\in T:\,\psi_t\to[\alpha]\phi_t}\mu_t. \]
For the selected mode, the returned rational is the solution; the matching types can also be reported as witnesses. Equivalently, a decision version can ask whether coverage is at least a supplied rational threshold \(q\). This is the same weak or strong protocol-match test the paper studies, evaluated over the supported agent types and weighted by their population mass.
Theorem 7.1 applies to each type’s matching query. Repeating the characterisation-based method over \(\tau\) types gives at most \(2\tau n\) entailment checks in the theorem’s cost model, followed by exact rational summation. That makes the mirror tractable in \(\tau\) and the explicit characterisation size. It does not establish polynomial time in a compact protocol encoding: \(n\), the number of paths, can be exponential in the syntax-tree size. Nor does it establish a new continuous-optimization result. The continuous payoff here is that a population with many agents but relatively few distinct matching types can be summarized and assessed without processing every named agent.
The authors should recognize this as an aggregate use of their problem: each type asks their exact question—does this protocol achieve this goal from this initial state?—and the population query reports what share of the deployment it serves. The mirror covers protocol matching and the paper’s characterisation-based speedup, not its entire treatment of iterative and recursive protocols. Natural follow-ups include computing coverage for every protocol in a library and finding the library’s strongest and weakest population coverage.
The weakest point is that the paper studies an individual agent selecting protocols, while coverage is a population-level deployment metric. Because types match independently, the continuous model adds aggregation rather than new matching structure. Its case depends on whether authors and referees accept that aggregate question as a sensible high-multiplicity application of their runtime matching method. In repeated deployments with millions of agents and few distinct state-goal types, I think they should.
Theorem 7.1 is a genuine algorithmic anchor, so I would not argue that the paper has nothing computational to mirror. But its result concerns one agent’s query: does this protocol match this initial state and goal? Its parameters \(e\) and \(n\) measure the protocol’s syntax tree and paths, not the population. Characterisations also have to be computed first; the paper’s experiments suggest that preprocessing pays off only after repeated queries.
The proposed coverage question is well-defined. Take types to include every relevant feature—role, library, state, and goal—and let \(\mu_t\) be their population shares. Then, for a fixed protocol, coverage is
\[
\sum_t \mu_t\,\mathbf{1}[\text{the protocol matches type }t].
\]
That is a plausible deployment statistic, especially for a fleet of similar agents. But it applies the paper’s individual matching test separately to each supported type, then sums the results. Large numbers of identical agents do not create more queries: their mass just multiplies one Boolean answer. The work is driven by the number of distinct types \(\tau\), and the continuous model adds no shared decision or constraint for the algorithm to solve.
The stronger mirror—choose a protocol from a library to maximize covered mass—does not add much structure: evaluate each candidate against the supported types and sum its coverage. Giving each type its own protocol decomposes into independent matching queries. To create a coupled population problem, one would need to add something such as protocol capacity, scarce resources, or participant compatibility. Those could be worthwhile models, but they are new constraints, not mirrors of the result proved here. And because this is a protocol-matching paper rather than a collective-choice paper, the coverage objective is an extra system-level question, not an outcome the paper itself defines.
So the best case against is that the mirror passes the population test but misses the programme’s computational target: it turns an individual matching relation into a weighted service metric, without yielding a population-level algorithmic problem from the paper’s result. I would not call that decisive. A protocol researcher could reasonably care about how much of a deployment their library serves, so a continuous mirror is plausible; the case against is strongest as an argument that it is not a worthwhile ChoCo project, rather than that no credible scenario exists.
The adversarial triple: the proponent anchors on up to three named results; the opponent sees that case and must defeat every anchor; the judge decides which case convinced it. These are the pipeline’s own outputs, generated by tools/triple_run.py — no human edited them. The paper’s own text is not reproduced here beyond the quoted statement above.