{"id":"55162f05-d0a4-448e-89ce-eb629e37a7ec","arxiv_id":"2411.14802","paper_version":4,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"LMNtal gains principled box-copying and box-deletion constructs, enabling direct encoding and state-space exploration of MELL proof net cut elimination.","lead":"The authors extend the LMNtal graph rewriting language with new constructs for copying and deleting hierarchical boxes, and use them to encode cut elimination for multiplicative exponential linear logic proof nets. The work gives proof-net researchers an executable workbench and demonstrates the language can express the Ambient Calculus.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Correctness of the MELL encoding is explicitly deferred (Sect. 5.1); without a formal correspondence, the state-space results describe the LMNtal program, not MELL proof nets.","rationale":"The reader identified the explicit omission of a correctness proof as the weakest assumption; the manuscript itself confirms this in Section 5.1. My stress-test agrees: the load-bearing premise is that the LMNtal encoding is a faithful simulation of MELL proof-net cut elimination, including principal/auxiliary door handling and bundle cardinalities. The paper provides a runnable implementation, concrete encodings, and small state-space explorations, which are real evidence of internal consistency and practical viability, but they do not establish the claimed 'workbench' status for MELL proof nets. The new aggregate-of-process-contexts construct and the mell API are defined by example rather than by a rigorous semantics, so even the intended simulation relation is not pinned down precisely enough to verify. My proposed test—an independent reference interpreter and graph isomorphism check on the same examples—would settle whether the encoding and the observed state spaces actually correspond to MELL cut elimination. If the test passes, the conditional verdict can be upgraded; if it fails, the central claim would need to be scaled back to an empirical demonstration. Therefore the reader's CONDITIONAL verdict remains appropriate, and no change is needed.","tokens_in":19044,"tokens_out":18893,"duration_ms":176279,"concrete_test":"Implement an independent reference interpreter for MELL proof-net cut elimination (tracking formulas and Danos-Regnier correctness), run it and the LMNtal encoding on the same nets (Fig. 5(a), Fig. 16), and check that the reduction graphs are isomorphic up to the declared two-step API reductions. Pay special attention to boxes with zero auxiliary doors and to the ?w_push rule (Fig. 15), where Row 6 of Table 1 reports loss of confluence; if the reference interpreter does not reproduce that behavior, the encoding is not faithful.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim requires that the extended LMNtal rules faithfully simulate MELL cut elimination. Section 5.1 states: 'When a formal proof is required, it is necessary to establish a correspondence between the mathematical representation of each side, but we omit the details in this paper.' This is the load-bearing gap. In particular, the new construct $p[*X1,...,*Xn] (Sect. 4.1) and the mell.copy/mell.delete API rules (Sect. 4.2) are given only as example rewrite rules, with no formal semantics for the process-context aggregate and no proof that they preserve LMNtal's Link Condition or that their output is graph-isomorphic to the MELL rule's right-hand side. The mell.copy rule's handling of bundle cardinalities and the reuse of a single $a context as a fan for each auxiliary door is plausible but unverified. If any of these steps is wrong, Table 1's state counts and confluence/normalization observations would not be statements about MELL. The paper's own examples are consistent, but consistency on two hand-picked nets is not enough to support the workbench claim.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper extends the hierarchical graph rewriting language LMNtal with aggregates of process contexts ($p[*X1,...,*Xn]) and with a mell library providing mell.copy and mell.delete, in order to express the principal-door/auxiliary-door operations involved in MELL promotion boxes. It presents encodings of MELL proof net cells, promotion boxes, and cut elimination rules in extended LMNtal, reports state-space explorations for two example proof nets (one corresponding to a beta-reduction and one exercising push-equivalence rules), and sketches an encoding of the Ambient Calculus. The central claim is that LMNtal thus extended becomes a practical graph rewriting language with strong affinity to MELL proof nets and can serve as a proof-net workbench.","tokens_in":19277,"tokens_out":5733,"duration_ms":62489,"significance":"The contribution is concrete and partly verified by implementation: the mell library is implemented in SLIM, source code is provided, and the encoding figures give a clear visual account of how promotion boxes are mapped to membranes, bundles, and process contexts. The proposed aggregate-of-process-contexts construct is potentially of independent interest for graph cloning and deletion. If the encoding is faithful, the paper offers a useful two-way bridge between MELL proof nets and a general-purpose hierarchical graph rewriting language, and the push-equivalence experiments illustrate how the LMNtal toolchain can help explore rule design. However, the paper explicitly defers the formal correctness proof of the encoding, so the significance is conditional: without a correspondence result, Table 1 and the observed confluence/normalization behavior describe the LMNtal program rather than MELL proof nets.","major_comments":[{"comment":"This is the load-bearing gap of the paper. The text states: 'When a formal proof is required, it is necessary to establish a correspondence between the mathematical representation of each side, but we omit the details in this paper.' Since the paper claims that the platform 'could serve as a useful workbench for proof nets' and uses state-space results to draw conclusions about confluence and normalization, a formal correspondence is not optional. The authors should either provide a simulation/correspondence proof between MELL proof-net cut elimination and the LMNtal rewriting system, or explicitly restrict all such claims to the concrete examples shown. At minimum, the proof must cover preservation of the encoding under each rule, correct handling of principal and auxiliary doors, and the relationship between terminal LMNtal states and cut-free proof nets.","section":"Section 5.1, 'Correctness of the encoding'"},{"comment":"The new construct $p[*X1,...,*Xn] is the central language contribution, but no formal semantics is given for it. The paper needs to specify how matching of an aggregate of process contexts is defined, how the equal-cardinality constraint |*X1| = ... = |*Xn| is enforced during matching, how the resulting substitution is formed, and why the Link Condition and the structural congruence of LMNtal are preserved. Without this, the mell.copy and mell.delete rules in Section 4.2 are examples of intended behavior rather than a definition of the extended language. This is particularly important because the paper contrasts the new construct with the earlier nlmem library and claims that the extension is what makes the encoding straightforward.","section":"Section 4.1, syntax extension"},{"comment":"The confluence and normalization observations are based on two hand-picked proof nets and finite state-space exploration. These experiments are useful evidence, but they do not establish properties of MELL proof nets unless the encoding is known to be faithful. The claim that adding ?w_push 'lost confluence' (Row 6) is a statement about the LMNtal rewrite system as encoded; its transfer to MELL requires the missing correspondence proof. Additionally, the paper should clarify how the LaViT abstraction of mell API steps as single abstract states interacts with the reported state and transition counts, since Table 1 appears to count both abstract and concrete reduction steps in different places.","section":"Section 5.1, Table 1 and the push-equivalence experiments"}],"minor_comments":[{"comment":"The term 'nonlinear membrane' is used without an explicit definition; please state in one sentence what nonlinearity means here, e.g., that the membrane can be copied or deleted even when it has an unbounded number of free links.","section":"Section 2.2"},{"comment":"The figure uses both 'copy'/'kill' in the text and 'copy'/'kill' in the rule names, but the library is called nlmem.kill in the text and nlmem.delete in the figure caption; please unify the terminology.","section":"Figure 3"},{"comment":"The encoding of the ?c cell uses both an atom and a membrane, but the text does not explain why the membrane is needed for commutativity; a short explanation would help readers unfamiliar with LMNtal's ordered links.","section":"Figure 8"},{"comment":"The phrase 'strong affinity with MELL proof nets' is not defined formally; consider replacing it with a precise statement about which operations are directly expressible and which ones currently require API-level support.","section":"Abstract and Section 1"},{"comment":"In the rule promotion_weakening, the argument A of mell.delete is not present in the LHS; please clarify whether A is a fresh variable and how the link X1 is grounded in the RHS, since the intended correspondence otherwise appears ambiguous.","section":"Section 5.1, promotion_weakening rule"}],"recommendation":"major_revision","confidential_remarks":"The paper is a solid systems/design contribution, but the central correctness claim is explicitly deferred at the exact point where the reader needs a proof. I would be comfortable with major revision rather than rejection, because the encoding is concrete, the implementation exists, and a correspondence proof or a repositioned scope could plausibly be added. The state-space experiments are a useful demonstration of the toolchain, but they should not be presented as evidence about MELL properties until the encoding is validated."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Punchline: the paper delivers a real language extension—aggregates of process contexts—and a runnable implementation for MELL proof net cut elimination, but the authors openly defer the correctness proof, so what you get is a useful workbench, not a verified simulation.\n\nWhat's actually new: the $p[*X1,...,*Xn] syntax and the mell.copy/mell.delete APIs are new in LMNtal. The earlier nlmem library was approximate; this separates principal from auxiliary ports and allows non-atomic structures to absorb the cloned links. The encoding of the !-?c rule in a single rule is a genuine improvement. The state-space experiments with push-equivalence rules are a good demonstration of the tool's value, especially the observation that ?w-push breaks confluence.\n\nCredit where due: the paper is honest. Section 5.1 explicitly says the formal correspondence is omitted. The figures are clear, and the examples are hand-checkable. The implementation is available.\n\nSoft spots: as the paper admits, there is no formal proof that the LMNtal rewrite relation tracks MELL cut elimination. That means Table 1's numbers describe the encoding, not MELL itself. The new construct's semantics are given operationally, not by a formal extension of the LMNtal calculus. Also, the design is driven by the MELL box operations, so the 'strong affinity' is partly by construction. Those are real limitations, but they don't sink the paper if you read it as a tool paper.\n\nWho should read it: people working on proof nets, graph rewriting languages, or the LMNtal ecosystem. It's a solid contribution to that community.\n\nRecommendation: yes, send it to peer review. Ask the authors to either supply a correctness proof or explicitly scale the claims to 'empirical workbench'. Either way, the work is worth refereeing.","headline":"Solid tool paper for LMNtal+MELL, but the deferred correctness proof keeps the state-space results about the encoding, not about MELL.","tokens_in":19777,"tokens_out":3581,"would_cite":true,"duration_ms":35278,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03F52","68Q42"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that adding aggregates of process contexts and the mell.copy/mell.delete APIs to LMNtal makes MELL promotion-box cloning, migration, and deletion expressible directly as rewrite rules, yielding a practical proof-net…","keywords":["MELL proof nets","hierarchical graph rewriting","LMNtal","cut elimination","promotion boxes","process contexts","graph cloning","state-space exploration"],"falsifier":"Run the encoded rewrite rules on a collection of valid MELL proof nets, starting with the paper's own examples, and inspect every terminal state of the generated state space: if any terminal graph is not the encoding of a cut-free proof net—for example, it has a dangling link, a promotion box with a missing or duplicated principal door, or auxiliary-door wires reconnected to the wrong structures—then the claimed faithful encoding fails.","tokens_in":18824,"feed_emoji":"📦","tokens_out":9893,"duration_ms":91397,"temperature":0.7,"pith_summary":"This paper claims that LMNtal, a declarative hierarchical graph rewriting language, can be extended so that the box operations of MELL proof nets—cloning, migrating, and deleting promotion boxes with an unbounded number of external wires—become expressible as single rewrite rules. The key step is adding aggregates of process contexts, implemented as the mell.copy and mell.delete APIs, which let one rule copy or remove an entire membrane together with all its free links while keeping the principal door of a box distinct from its auxiliary doors. The authors encode every MELL cut-elimination rule in the extended language and run them on the existing SLIM toolchain, whose state-space explorer and LaViT visualizer let them inspect confluence and normalization behavior on example nets. If the encoding is faithful, the result is a practical workbench for experimenting with proof nets and with graph-rewrite rules for box-like structures.","feed_headline":"Graph rewriting language gains direct MELL proof-net operations","feed_subtitle":"New process-context aggregates let one rule copy or delete a promotion box, turning LMNtal into a proof-net workbench.","key_machinery":"The machinery that carries the argument is the membrane-plus-process-context encoding of a promotion box, written `{’!’(X1,X2), $p[X1|*X]}` in LMNtal, where the bundle `*X` stands for the box's indefinite number of auxiliary-door wires and `$p` for the rest of the box's contents. The new aggregate-of-process-contexts construct, `$p[*X1,*X2,...,*Xn]`, declares that a number of process contexts equal to the bundle cardinality is produced, with matching free links. The mell.copy API implements this by cloning the membrane and distributing each original free link to the corresponding ports of the copies, separating the principal door from the auxiliary doors; mell.delete is its dual, deleting the membrane and wiring the auxiliary-door bundle to a supplied structure. These two primitives are exactly what the (!-?w) and (!-?c) cut-elimination rules require, while the remaining rules are handled by the pre-existing bundle and process-context mechanisms.","core_discovery":"On the paper's own terms, the discovery is that the two previously hard operations on promotion boxes—copying a box whose auxiliary doors carry an unspecified number of wires, and deleting such a box—can be represented as first-class rewrite primitives in LMNtal, and that this is enough to encode all of MELL cut elimination directly. A promotion box is encoded as a membrane containing a process context with a bundle, written `{’!’(X1,X2), $p[X1|*X]}`; the process context captures the arbitrary interior of the box and the bundle captures its auxiliary-door wires. The new mell.copy rule clones the membrane, duplicates the interior, and reconnects each copy's principal and non-principal ports through user-supplied structures; mell.delete removes the membrane and terminates the formerly dangling auxiliary wires with a specified non-atomic structure. The authors show the resulting rules reproduce the cut-elimination behavior on examples, including the β-reduction of a simply typed λ-term, and they show that adding ?c-push-equivalence rules preserves confluence while adding ?w-push rules destroys it and makes the state space explode.","pith_inferences":["If a formal simulation proof is later supplied, it will likely have to treat the two-step mell.copy and mell.delete reductions as atomic in the abstract state space, since the paper's visualization already collapses them into single abstract states.","The non-confluence found for ?w-push suggests a general empirical method: before accepting a proposed structural equivalence on boxes, test it in this encoding for confluence and state-space growth; a uniform condition for when push rules are safe could be extracted from such experiments.","The aggregate-of-process-contexts idea is not tied to LMNtal; it amounts to a schema for cloning subgraphs with an unbounded interface, so it could be adopted as a primitive in other hierarchical graph-rewriting formalisms, though the paper demonstrates it only in LMNtal.","A natural next test is to extend mell.copy to produce multiple clones in one step, which the paper lists as future work; comparing state-space sizes would show whether the single-clone restriction is a real limitation or just a convenience."],"forward_implications":["Every MELL cut-elimination rule, including promotion-box cloning and deletion, can be written as one declarative LMNtal rewrite rule, with the two API rules expanding into small fixed sequences.","The SLIM state-space explorer and LaViT visualizer can be used to check confluence and strong normalization on concrete proof nets by observing whether all reduction paths end at a single state.","Because rewrite rules are easy to add or modify, the platform can serve as a testbed for proposed structural equivalences such as push-equivalence; the paper shows ?c-push rules preserve a single end state while ?w-push makes the state space non-confluent and explosive.","The distinguishing of principal and auxiliary doors in mell.copy and mell.delete removes the post-processing that the earlier nlmem encoding required, making the representation of boxes direct.","The same constructs are general enough to encode other models of concurrency with box-like structures, demonstrated by an encoding of the Ambient Calculus."],"supporting_citations":[{"why":"Defines LMNtal's syntax, structural congruence, process contexts, bundles, and aggregates; the base language that the paper extends.","marker":"[36]"},{"why":"Introduces MELL and proof-net cut elimination with promotion boxes; the target formalism the encoding simulates.","marker":"[16]"},{"why":"Describes the nlmem nonlinear-membrane library whose copy/kill semantics the new mell.copy and mell.delete APIs refine.","marker":"[21]"},{"why":"Reports the prior poster attempt to encode MELL proof nets in original LMNtal, the starting point that motivated the new constructs.","marker":"[32]"},{"why":"Gives the semantics of the nlmem operations via aggregates, grounding the aggregate-of-process-contexts extension.","marker":"[23]"},{"why":"Describes the SLIM runtime with state-space search and LTL model checking, the toolchain used to execute and explore the encodings.","marker":"[18]"},{"why":"Provides the LaViT visualization used to display the state spaces and abstract the two-step API reductions.","marker":"[3]"},{"why":"Supplies known confluence and strong-normalization results for push rules that the paper's ?c-push and ?w-pull experiments are compared against.","marker":"[1]"}],"fun_headline_variants":["LMNtal now copies and deletes MELL promotion boxes","MELL cut elimination becomes native rewrite in LMNtal","First-class promotion box copy and delete in LMNtal","LMNtal extended: promotion boxes copyable and deletable","Direct MELL proof-net operations in LMNtal"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the LMNtal encoding is a faithful simulation of MELL proof-net cut elimination—correctly matching box boundaries, principal and auxiliary doors, and bundle cardinalities—and the paper explicitly leaves the formal proof of that correspondence out.","fun_headline_variants_meta":{"raw":{"variants":["LMNtal now copies and deletes MELL promotion boxes","MELL cut elimination becomes native rewrite in LMNtal","First-class promotion box copy and delete in LMNtal","LMNtal extended: promotion boxes copyable and deletable","Direct MELL proof-net operations in LMNtal"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00109,"raw_usage":{"total_tokens":4591,"prompt_tokens":1018,"completion_tokens":3573,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":634,"completion_tokens_details":{"reasoning_tokens":3491}},"tokens_in":634,"tokens_out":3573,"duration_ms":24523,"temperature":1.0,"reasoning_tokens":3491,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T14:51:51.199229+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the encoded rewrite rules on a collection of valid MELL proof nets, starting with the paper's own examples, and inspect every terminal state of the generated state space: if any terminal graph is not the encoding of a cut-free proof net—for example, it has a dangling link, a promotion box with a missing or duplicated principal door, or auxiliary-door wires reconnected to the wrong structures—then the claimed faithful encoding fails.","supporting_citations":[{"cited_title":"Theoretical Computer Science 410(46), 4784–4800 (2009)","cited_arxiv_id":null,"evidence_quote":"Defines LMNtal's syntax, structural congruence, process contexts, bundles, and aggregates; the base language that the paper extends."},{"cited_title":"Computer Software 25(1), 1_124–1_150 (2008)","cited_arxiv_id":null,"evidence_quote":"Describes the nlmem nonlinear-membrane library whose copy/kill semantics the new mell.copy and mell.delete APIs refine."},{"cited_title":"In: The 21st Asian Symposium on Programming Languages and Systems SRC & Posters (2023)","cited_arxiv_id":null,"evidence_quote":"Reports the prior poster attempt to encode MELL proof nets in original LMNtal, the starting point that motivated the new constructs."},{"cited_title":"Information Technology Letters4, 9– 12 (Aug 2005), http://id.nii.ac.jp/1001/00147815/","cited_arxiv_id":null,"evidence_quote":"Gives the semantics of the nlmem operations via aggregates, grounding the aggregate-of-process-contexts extension."},{"cited_title":"Computer Software 28(4), 137–157 (2011)","cited_arxiv_id":null,"evidence_quote":"Describes the SLIM runtime with state-space search and LTL model checking, the toolchain used to execute and explore the encodings."},{"cited_title":"Computer Software27(4), 4_197– 4_214 (2010)","cited_arxiv_id":null,"evidence_quote":"Provides the LaViT visualization used to display the state spaces and abstract the two-step API reductions."},{"cited_title":"In: van Raamsdonk, F","cited_arxiv_id":null,"evidence_quote":"Supplies known confluence and strong-normalization results for push rules that the paper's ?c-push and ?w-pull experiments are compared against."}],"review_version":1}