| paper | d4-conf-aaai-2018-0838 |
| authors | — |
| venue | ? |
| filed under | unclassified |
| judged by | gpt-6-luna / xhigh (triple__luna__xhigh__c6r1) |
| judge confidence | medium |
| authors would recognise it | yes |
NP-hard→NP-hard discrete result → its continuous mirror
Answer: Coalition feasibility is \(\mathrm{NP}\)-hard for both affine \(\mathrm{MLL}\) and affine \(\mathrm{MALL}\); for affine \(\mathrm{MALL}\), it is moreover \(\mathrm{PSPACE}\)-hard. · discrete side: hardness · adjudication: proved
full proof & adversarial review →
Proposition 18
statement extracted from the paper’s text layer
Fix affine logic \(L\in\{\mathrm{MLL},\mathrm{MALL}\}\). An instance gives a finite type set \(T\), each type's endowment multiset \(E_t\) and goal formula \(g_t\), rational population masses \(\mu_t\) with \(\sum_{t\in T}\mu_t=1\), and rational coalition masses \(x_t\) with \(0\le x_t\le\mu_t\) and \(\sum_t x_t>0\). Decide whether there are finitely many nonzero integer templates \(k^j\in\mathbb{N}^T\), each with an affine-\(L\) proof \(\biguplus_{t\in T} E_t^{\uplus k^j_t}\vdash\bigotimes_{t\in T}g_t^{\otimes k^j_t}\), and weights \(\lambda_j\in\mathbb{R}_{\ge0}\) such that \(x_t=\sum_j\lambda_j k^j_t/\sum_{u\in T}k^j_u\) for every \(t\in T\).
Types carry complete endowment and goal profiles; a coalition's mass is allocated among finite team templates, each certified by an exact affine-logic proof, so each unit receives an integral resource bundle and meets its goal.
The template mixture partitions the population into independently certified teams and may omit coalitions feasible only under a genuinely global fluid resource semantics; the paper gives no reason those semantics coincide.
fatal: False
The mirror covers WIN for one-goal affine MLL and MALL RCRGs, the cases in Proposition 18. It leaves the other WIN bounds and the veto, dummy, and core results without continuous counterparts.
My strongest anchor is Proposition 18, proved in this paper. It states that WIN is NP-complete for one-goal affine MLL RCRGs and PSPACE-complete for one-goal affine MALL RCRGs. Here WIN asks whether a specified coalition can jointly achieve a goal for every member. The proof uses the equivalence between WIN and sequent validity for one-goal affine games (Lemma 17), with hardness from affine sequent validity (Proposition 16); the underlying logic-complexity results are cited from earlier work.
I would mirror that question as Fluid RCRG-WIN. Fix either affine MLL or affine MALL. A type \(t\) consists of a finite multiset \(E_t\) of endowment formulas and one goal formula \(g_t\). An instance gives a finite type set \(T\), rational population masses \(\mu_t\) summing to \(1\), and rational coalition masses \(x_t\) with \(0\le x_t\le\mu_t\). The question is whether the coalition of mass profile \(x\) can satisfy every member.
Here is one precise fluid semantics. A finite team template is a nonzero integer vector \(k\in\mathbb N^T\), together with an affine-logic proof that the pooled endowments of \(k_t\) agents of each type entail the tensor product of all their goals:
\[ \biguplus_{t\in T} E_t^{\uplus k_t} \;\vdash\; \bigotimes_{t\in T} g_t^{\otimes k_t}. \]
Write \(n_k=\sum_t k_t\). A fluid plan is a finite collection of such proved templates with nonnegative weights \(\lambda_j\), satisfying
\[ x_t=\sum_j \lambda_j\frac{k^j_t}{n_{k^j}} \quad\text{for each }t. \]
The weights allocate the coalition’s mass among batches; each batch follows a finite resource-use proof, scaled to its assigned mass. A solution is this finite list of templates, proofs, and weights. The continuous question is whether such a plan exists.
The regime I have in mind is a large cooperative production or logistics pool: perhaps hundreds of thousands of interchangeable units, with a handful of recurring resource-and-capability profiles and goals. A type’s formulas specify everything relevant about a unit—its stock, transformations it can perform, and what it must achieve. Thus \(N\) can be very large while \(\tau=|T|\) stays small. This is a population mirror: the decision is still whether a coalition can act so that all its members’ goals are met. Divisible resource quantities are a co-modification needed to describe fractional cohorts; the outcome space is not the object being continuized.
I expect hardness to survive, provisionally closest to hardness transfers. Proposition 18’s combinatorics sit inside the logic formulas, not in the number of agents, and the mirror keeps those formulas as the agents’ goals and capabilities. The programme’s key question is whether fluid feasibility makes that proof search easier. The paper itself does not establish a reduction to this fluid problem, so persistence of the lower bound is a conjecture to test, not a consequence of Proposition 18. The natural further questions are whether Fluid RCRG-WIN is decidable in polynomial time for fixed \(\tau\), whether it admits a separation or pricing formulation, and which affine MALL features preserve PSPACE hardness.
The high-multiplicity story is plausible because agents sharing a type are genuinely indistinguishable in the game’s data, and fractional coalition membership is meaningful in a large pool. I would not claim that every RCRG instance has such a regime, or that all the paper’s results have continuous counterparts. This case covers WIN on the one-goal affine fragments; it does not attempt to mirror the paper’s veto, dummy, or core results.
The weak point is the fluid proof semantics. MLL and MALL give the paper discrete proof rules, and there is no unique fractional interpretation forced by them. My batch definition captures fractional populations by scaling certified team plans, but a coalition that pools resources globally may have options beyond a plan assembled from separately certified batches. A broader pooled fluid semantics could change the answer or its complexity. That is a real modeling question for the authors and referee, though the population scenario and the underlying coalition question remain recognizable.
Proposition 18 is a real computational anchor, so I would not argue that the paper has nothing to mirror. My case against is that its winner condition has no natural fractional semantics supplied by the model, and the proposed fluid version does not resolve that problem.
In RCRGs, an agent’s endowment is a multiset of formulas, and winning means that some submultiset proves the tensor of every coalition member’s goals. A formula such as \(A \multimap B\) is a consumable capability; \(A \mathbin{\&} B\) and \(A \mathbin{\oplus} B\) encode different kinds of choice. These are not quantities that can simply be multiplied by a real mass. The template proposal preserves them by using exact finite proofs, but then its weights mix independently executed finite teams. It defines a plausible cohort model; it does not explain how a shared pool of fractional formula resources should support one joint proof.
The stronger alternative is to treat each type as a repeated agent profile and ask whether a large cohort with the specified type proportions can satisfy every member. That is a sensible scenario for a production pool. But a distribution over types does not specify the cohort size, while exact feasibility is a proof about integer multisets of formulas. An asymptotic version must choose what happens when exact feasibility fails at some scales: require it at every sufficiently large scale, at any scale, or allow some fraction of goals to go unmet. Those are distinct questions, and the paper’s all-members-satisfied condition does not select among them. Fractionalizing proof rules instead would require substantive choices about how capabilities and logical choices behave in a continuum.
That leaves a credible mirror, but one whose central modelling choice is still open. I can’t honestly make the universal case that no scenario is worthwhile: repeated production profiles make high multiplicity plausible, and an authors-recognized cohort or asymptotic semantics could be a useful problem. The negative case is therefore weak at its hardest point. Its best claim is narrower: Proposition 18 merits a mirror only if the authors can say what a continuous resource proof means, rather than merely attach masses to finite proofs.
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.