Pith. sign in

REVIEW 3 major objections 5 minor 48 references

Enhancing a Hierarchical Graph Rewriting Language based on MELL Cut Elimination

T0 review · 3 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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…

desk verdict Solid tool paper for LMNtal+MELL, but the deferred correctness proof keeps the state-space results about the encoding, not about MELL. read the letter →

arxiv 2411.14802 v4 pith:WZ4FB56V submitted 2024-11-22 cs.PL

Kento Takyu , Kazunori Ueda This is my paper · ORCID
classification cs.PL MSC 03F5268Q42
keywords MELLproofnetshierarchicalgraphrewritingLMNtalcuteliminationpromotionboxesprocesscontextscloningstate-spaceexploration
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

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.

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 (3)
  1. [Section 5.1, 'Correctness of the encoding'] 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.
  2. [Section 4.1, syntax extension] 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.
  3. [Section 5.1, Table 1 and the push-equivalence experiments] 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.
minor comments (5)
  1. [Section 2.2] 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.
  2. [Figure 3] 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.
  3. [Figure 8] 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.
  4. [Abstract and Section 1] 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.
  5. [Section 5.1, promotion_weakening rule] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; the MELL-based design goal is restated as an affinity claim, but the concrete encodings, implementation, and independent Ambient Calculus example stand on their own.

full rationale

The paper's derivation chain is constructive rather than inferential: it designs new LMNtal constructs (aggregates of process contexts and the mell.copy/mell.delete APIs) specifically from the shape of MELL promotion-box operations, then demonstrates that the resulting encodings run on the SLIM toolchain. That the language ends up having "strong affinity" with MELL proof nets is a restatement of the design criterion rather than a derived prediction; however, no theorem or benchmark result is obtained by fitting a parameter and then re-predicting the same data. The state-space observations (Table 1 and Fig. 13) are outputs of the actual implementation on hand-written encodings and are checked against known MELL/lambda-calculus normal forms, which is an external consistency check rather than a circular reduction. The only direct self-citations ([32] and [36]) are background: the prior poster is explicitly described as only "promising" and insufficient, and [36] is an established formal language definition, not a fitted assumption. The paper itself flags its main gap in Sect. 5.1: "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." That is a correctness and completeness limitation, not a circular step; it means the state-space results describe the LMNtal program unless the correspondence is supplied, but it does not make the encoding a renamed version of its own input. Accordingly, no circular step meeting the quote-and-reduction standard was found.

Assumptions & free parameters 0 free parameters · 4 assumptions · 2 invented entities

The central contribution is a set of new language constructs; there are no numerical free parameters. The paper leans on the MELL cut elimination theorem, the existing LMNtal formal semantics, and the SLIM implementation as background assumptions. The new aggregates of process contexts and the mell.copy/mell.delete APIs are design inventions whose adequacy is shown by executable examples rather than by a formal correctness proof.

assumptions (4)
  • domain assumption MELL cut elimination is correct, confluent, and strongly normalizing as established in the literature (Girard 1987, et al.).
    The paper relies on these properties when interpreting state spaces of reductions as evidence for confluence or normalization; see Section 3, properties listed after Fig. 6.
  • domain assumption The LMNtal language has the formal semantics given in the cited paper (Ueda 2009).
    The new constructs are defined as an extension of this semantics; the paper cites [36] and says the full formal definition is there (Section 2).
  • domain assumption The SLIM runtime correctly implements both the original LMNtal semantics and the new mell library.
    The paper states 'We have confirmed that all the examples in the following sections work' (Section 4.2, Implementation). All demonstrations depend on this implementation being faithful.
  • ad hoc to paper The new aggregate syntax $p[*X1,...,*Xn] is a sound extension, with the constraint that all bundle cardinalities are equal upon matching.
    This is a newly proposed construct (Section 4.1); no proof is given that it preserves the Link Condition and other LMNtal syntactic conditions, beyond reference to prior requirements.
invented entities (2)
  • Aggregates of process contexts ($p[*X1,...,*Xn]) independent evidence
    purpose: To clone or delete a membrane with an indefinite number of free links in one rewrite step, separating principal and auxiliary ports.
    Implemented in the SLIM runtime and used in the cut elimination and Ambient Calculus encodings; could be falsified by running the examples.
  • mell.copy and mell.delete APIs independent evidence
    purpose: To provide box copying and deletion with explicit handling of principal and non-principal ports and of bundle reconnection.
    These are the concrete implementation of the new construct; their behaviour is shown in Figs. 7, 10, 11, and 24, and the code is linked.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Enhancing a Hierarchical Graph Rewriting Language based on MELL Cut Elimination." pith.science (2026). https://pith.science/paper/WZ4FB56V

@misc{pith2026241114802,
  author       = {Pith},
  title        = {Pith review of: Enhancing a Hierarchical Graph Rewriting Language based on MELL Cut Elimination},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WZ4FB56V}},
  note         = {Machine review of arXiv:2411.14802}
}
read the original abstract

Hierarchical graph rewriting is a highly expressive computational formalism that manipulates graphs enhanced with box structures for representing hierarchies. It has provided the foundations of various graph-based modeling tools, but the design of high-level declarative languages based on hierarchical graph rewriting is still a challenge. For a solid design choice, well-established formalisms with backgrounds other than graph rewriting would provide useful guidelines. Proof nets of Multiplicative Exponential Linear Logic (MELL) is such a framework because its original formulation of cut elimination is essentially graph rewriting involving box structures, where the so-called promotion boxes with an indefinite number of non-local edges may be cloned, migrated and deleted. This work builds on LMNtal (pronounced "elemental") as a declarative language based on hierarchical (port) graph rewriting, and discusses how it can be extended to support the above operations on promotion boxes of MELL proof nets. LMNtal thus extended turns out to be a practical graph rewriting language that has a strong affinity with MELL proof nets. The language features provided are general enough to encode other well-established models of concurrency. Using the toolchain of LMNtal that provides state-space search and model checking, we implemented cut elimination rules of MELL proof nets in extended LMNtal and demonstrated that the platform could serve as a useful workbench for proof nets.

Figures

Figures reproduced from arXiv: 2411.14802 by the authors.

Figure 1
Figure 1. Syntax of LMNtal. Since LMNtal was originally developed as a model of concurrency. the hi￾erarchical graphs of LMNtal are also called processes. 0 is an inert process, p(X1, . . . ,Xn)(n ≥ 0) is an n-ary atom (a.k.a. node) with ordered links (a.k.a. edges) X1, . . . , Xn, P,P is parallel composition, m{P} is a cell formed by wrap￾ping P with an optionally named membrane { }, and T :- T is a rewrite rule. Occurrences… view at source ↗
Figure 2
Figure 2. Rewriting an LMNtal graph using process contexts and bundles. An arrowhead of each non-unary atom indicates the first argument and the ordering of atoms. $p ... A *X B copy n B n A n n n $p $p ... *X (a) nlmem.copy(A,B,C),n(B),{$p[A|*X]} $p ... n *X kill A ... *X n n n (b) nlmem.kill(A,B),n(B),{$p[A|*X]} [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Operations of the nlmem library. The application of rules in LMNtal is nondeterministic because (i) a rule may be able to rewrite different subgraphs of a given graph, and (ii) different rules may be able to rewrite the same graph. The LMNtal runtime SLIM [18] provides a nondeterministic execution mode that constructs the whole state space of rewriting, which can also be visualized using the visualization tool State… view at source ↗
Figures from the paper (21 more)
Figure 4
Figure 4. Figure 4: The components of MELL proof structure. Definition 1. An MELL proof structure is a directed acyclic multigraph that combines the cells (not to be confused with cells m{P} of LMNtal) and wires shown in [PITH_FULL_IMAGE:figures/full_fig_p005_4.png]
Figure 5
Figure 5. Figure 5: Examples of MELL proof nets, where applying cut elimination to (a) results in (b) (See Sect. 5.1 also). 1. (Cut Elimination) All cuts of an MELL proof net can be eliminated. 2. (Stability) An MELL proof net is still a proof net after cut elimination. 3. (Confluence) Cu…
Figure 6
Figure 6. Figure 6: Some of cut elimination rules of MELL proof nets involving box operations. 2. while the processing of (the free links of) bundles was the key design issue, the only functionality provided was to reconfigure them with the collection of atoms, which was found to be restr…
Figure 7
Figure 7. Figure 7: Schematic illustrations of the mell library. mell.copy(X, A1,A2,A3, B1,B2, C1,C2), {$p[X|*Z]}, {$a[A1,A2,A3]}, {$b[B1,B2]} :- {$p[X’|*Z’]}, {$p[X”|*Z”]}, $a[*Z’,*Z”,*Z], $b[X’,C1], $b[X”,C2]. The first argument of mell.copy (where mell is the prefixed module name) is l…
Figure 8
Figure 8. Figure 8: Encoding of cells and wires (MELL in red, LMNtal in blue henceforth); where a small circle in a membrane stands for a unary atom named ‘+’ and may be written as a prefix operator in textual representation. 5 Examples of Encoding 5.1 Encoding of MELL Proof Nets and Cut …
Figure 9
Figure 9. Figure 9: Encoding of a promotion box [PITH_FULL_IMAGE:figures/full_fig_p009_9.png]
Figure 10
Figure 10. Figure 10: Encoding of Rule (! - !). ?w A ! ?Γ · · · !A ?A⊥ cut ?w ?w ?w ?Γ · · · · · · 7→ $p X1 ! *X · · · X2 X3 ?w cut $p X1 ! *X · · · X2 delete ?w ?w ?w ?w · · · *X ?A⊥ ?A⊥ ?c A ! ?Γ · · · !A ?A⊥ cut A ! ?Γ · · · !A ?A⊥ cut A ! ?Γ · · · !A ?A⊥ cut ?c ?c ?c · · · 7→ $p C1 C2 …
Figure 11
Figure 11. Figure 11: Encoding of Rule (! - ?w) and Rule (! - ?c) with the mell library. promotion_promotion@@ {’!’(X1,X2), $p[X1|*X]}, {$q[X3|*Y]}, cut{+X2,+X3} :- {{’!’(X1,X2), $p[X1|*X]}, $q[X3|*Y], cut{+X2,+X3}} [PITH_FULL_IMAGE:figures/full_fig_p010_11.png]
Figure 12
Figure 12. Figure 12: (λf : n → n . λx : n . f x) (λx : n . x) →β (λx : n . x) promotion_weakening@@ {’!’(X1,X2), $p[X1|*X]}, cut{+X2,+X3}, ’?w’(X3) :- mell.delete(X,A), {$p[X|*X]}, {’?w’(A)} [PITH_FULL_IMAGE:figures/full_fig_p011_12.png]
Figure 13
Figure 13. Figure 13: State space of cut elimination applied to the proof net of [PITH_FULL_IMAGE:figures/full_fig_p012_13.png]
Figure 14
Figure 14. Figure 14: Push-equivalence. contraction_pull@@ // ?c_{pull} {’!’(X1,X2), ’?c’(I,X5), {+I,+X3,+X4}, $p[X1,X3,X4|*X]} :- {’!’(X1,X2), $p[X1,X3,X4|*X]}, ’?c’(I,X5), {+I,+X3,+X4}. contraction_push@@ // ?c_{push} {’!’(X1,X2), $p[X1,X3,X4|*X]}, ’?c’(I,X5), {+I,+X3,+X4}, :- {’!’(X1,X2…
Figure 15
Figure 15. Figure 15: LMNtal encoding of each rule in [PITH_FULL_IMAGE:figures/full_fig_p013_15.png]
Figure 16
Figure 16. Figure 16: Proof net corresponding to (λf : n→n . λx : n . f (f x)) (λx : n . x) was confirmed that both confluence and strong normalization were maintained, meaning that it is a rule that can be safely handled (Row 5). This result is consistent with the results in [1]. However,…
Figure 17
Figure 17. Figure 17: Pictorial representation of an LMNtal graph, in which F is a free link and the others are local links [PITH_FULL_IMAGE:figures/full_fig_p019_17.png]
Figure 18
Figure 18. Figure 18: Structural congruence on LMNtal processes. A.2 Semantics of LMNtal The semantics of LMNtal consists of structural congruence (A.3) and a reduction relation (A.5). A.3 Structural Congruence The syntax defined above does not yet char￾acterize LMNtal graphs because the p…
Figure 19
Figure 19. Figure 19: Reduction relation on LMNtal processes. Also, we allow p(X1, ..., Xk−1, L, Xk+1, ..., Xm), m{+L, P} (1 ≤ k ≤ m) to be written as p(X1, ..., Xk−1, m{P}, Xk+1, ..., Xm) (1 ≤ k ≤ m), where +L is a operator notation for +(L). A.5 Reduction Relation The reduction relation …
Figure 20
Figure 20. Figure 20: Sequent calculus for MELL (+ mix rules). It is known that the cut elimination theorem holds for the proof system of MELL [16] [PITH_FULL_IMAGE:figures/full_fig_p022_20.png]
Figure 21
Figure 21. Figure 21: Cut elimination rules of MELL [PITH_FULL_IMAGE:figures/full_fig_p023_21.png]
Figure 22
Figure 22. Figure 22: The proof tree corresponding to [PITH_FULL_IMAGE:figures/full_fig_p024_22.png]
Figure 23
Figure 23. Figure 23: Cut elimination rules in MELL Proof Nets (full) [PITH_FULL_IMAGE:figures/full_fig_p025_23.png]
Figure 24
Figure 24. Figure 24: LMNtal encoding of cut elimination rules (full) [PITH_FULL_IMAGE:figures/full_fig_p026_24.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

48 extracted references · 36 canonical work pages

  1. [1]

    In: van Raamsdonk, F

    Accattoli, B.: Linear Logic and Strong Normalization. In: van Raamsdonk, F. (ed.) 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), vol. 21, pp. 39–

    work page 2013

  2. [2]

    Electronic Proceedings in Theoretical Computer Science 48 (Feb 2011)

    Alves, S., Fernández, M., Mackie, I.: A new graphical calculus of proofs. Electronic Proceedings in Theoretical Computer Science 48 (Feb 2011). https://doi.org/10.4204/EPTCS.48.8

    work page doi:10.4204/eptcs.48.8 2011

  3. [3]

    Computer Software27(4), 4_197– 4_214 (2010)

    Ayano, T., Hori, T., Iwasawa, H., Ogawa, S., Ueda, K.: LMNtal Model Checking using an Integrated Development Environment. Computer Software27(4), 4_197– 4_214 (2010). https://doi.org/10.11309/jssst.27.4_197

    work page doi:10.11309/jssst.27.4_197 2010

  4. [4]

    Theoretical Computer Sci- ence 96(1), 217–248 (1992)

    Berry, G., Boudol, G.: The chemical abstract machine. Theoretical Computer Sci- ence 96(1), 217–248 (1992). https://doi.org/10.1016/0304-3975(92)90185-I

    doi:10.1016/0304-3975(92)90185-i 1992

  5. [5]

    In: Lambers, L., Weber, J

    Brenas, J.H., Echahed, R., Strecker, M.: Verifying Graph Transformation Systems with Description Logics. In: Lambers, L., Weber, J. (eds.) Graph Transformation. LNCS, vol. 10887, pp. 155–170. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-92991-0_10

    work page doi:10.1007/978-3-319-92991-0_10 2018

  6. [6]

    Theoretical Computer Science 240(1), 177–213 (2000)

    Cardelli, L., Gordon, A.D.: Mobile ambients. Theoretical Computer Science 240(1), 177–213 (2000). https://doi.org/10.1016/S0304-3975(99)00231-5

    doi:10.1016/s0304-3975(99)00231-5 2000

  7. [7]

    Cambridge University Press (2017)

    Coecke, B., Kissinger, A.: Picturing Quantum Processes: A First Course in Quan- tum Theory and Diagrammatic Reasoning. Cambridge University Press (2017)

    work page 2017

  8. [8]

    In: Graph Transformations (ICGT 2006)

    Corradini, A., Heindel, T., Hermann, F., König, B.: Sesqui-Pushout Rewriting. In: Graph Transformations (ICGT 2006). LNCS, vol. 4178, pp. 30–45. Berlin, Heidel- berg (2006). https://doi.org/10.1007/11841883_4

    work page doi:10.1007/11841883_4 2006

Show all 48 references
  1. [9]

    Archive for Mathematical Logic 28(3), 181–203 (1989)

    Danos, V., Regnier, L.: The Structure of Multiplicatives. Archive for Mathematical Logic 28(3), 181–203 (1989). https://doi.org/10.1007/bf01622878 Enhancing a Hierarchical Graph Rewriting Language 17

    1989 doi

  2. [10]

    In: Proceedings of Twelfth An- nual IEEE Symposium on Logic in Computer Science

    Di Cosmo, R., Kesner, D.: Strong normalization of explicit substitu- tions via cut elimination in proof nets. In: Proceedings of Twelfth An- nual IEEE Symposium on Logic in Computer Science. pp. 35–46 (1997). https://doi.org/10.1109/LICS.1997.614927

    1997

  3. [11]

    In: Rewriting Techniques and Applications (RTA 1999)

    Di Cosmo, R., Guerrini, S.: Strong Normalization of Proof Nets Modulo Struc- tural Congruences. In: Rewriting Techniques and Applications (RTA 1999). LNCS, vol. 1631, pp. 75–89. Springer Berlin Heidelberg (1999). https://doi.org/10.1007/3- 540-48685-2_6

    1999 doi

  4. [12]

    Journal of Computer and System Sciences 64(2), 249–283 (2002)

    Drewes, F., Hoffmann, B., Plump, D.: Hierarchical Graph Transforma- tion. Journal of Computer and System Sciences 64(2), 249–283 (2002). https://doi.org/10.1006/jcss.2001.1790

    2002

  5. [13]

    Electronic Proceedings in Theoretical Computer Science, EPTCS265, 2–19 (Feb 2018)

    Ene, N.C., Fernández, M., Pinaud, B.: Attributed hierarchical port graphs and ap- plications. Electronic Proceedings in Theoretical Computer Science, EPTCS265, 2–19 (Feb 2018). https://doi.org/10.4204/eptcs.265.2

    2018 doi

  6. [14]

    Mathematical Structures in Computer Science 4(2), 273–285 (1994)

    Fleury, A., Retoré, C.: The mix rule. Mathematical Structures in Computer Science 4(2), 273–285 (1994). https://doi.org/10.1017/S0960129500000451

    1994 doi

  7. [15]

    International Journal on Software Tools for Technology Transfer 14(1), 15–40 (Feb 2012)

    Ghamarian,A.,deMol,M.,Rensink,A.,Zambon,E.,Zimakova,M.:Modellingand analysis using GROOVE. International Journal on Software Tools for Technology Transfer 14(1), 15–40 (Feb 2012). https://doi.org/10.1007/s10009-011-0186-x

    2012 doi

  8. [16]

    Theoretical Computer Science 50(1), 1–101 (1987)

    Girard, J.Y.: Linear logic. Theoretical Computer Science 50(1), 1–101 (1987). https://doi.org/10.1016/0304-3975(87)90045-4

    1987 doi

  9. [17]

    In: Bauer, F., Brauer, W., Schwichtenberg, H

    Girard, J.Y.: Linear Logic: A Survey. In: Bauer, F., Brauer, W., Schwichtenberg, H. (eds.) Logic and Algebra of Specification. NATO ASI Series, vol. 94, pp. 63–112. Springer Berlin Heidelberg (1993). https://doi.org/10.1007/978-3-642-58041-3_3

    1993 doi

  10. [18]

    Computer Software 28(4), 137–157 (2011)

    Gocho, M., Hori, T., Ueda, K.: Evolution of the LMNtal runtime to a parallel model checker. Computer Software 28(4), 137–157 (2011). https://doi.org/10.11309/jssst.28.4_137

    2011 doi

  11. [19]

    In: [1992] Pro- ceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science

    Gonthier, G., Abadi, M., Lévy, J.J.: Linear logic without boxes. In: [1992] Pro- ceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science. pp. 223–234 (1992). https://doi.org/10.1109/LICS.1992.185535

    1992

  12. [20]

    In: Ehrhard, T., Girard, J.Y., Ruet, P., Scott, P

    Guerrini, S.: Proof Nets and the λ-Calculus. In: Ehrhard, T., Girard, J.Y., Ruet, P., Scott, P. (eds.) Linear Logic in Computer Science, pp. 65–118. London Mathematical Society Lecture Note Series, Cambridge University Press (2004). https://doi.org/10.1017/CBO9780511550850.003

    2004 doi

  13. [21]

    Computer Software 25(1), 1_124–1_150 (2008)

    Inui, A., Kudo, S., Hara, K., Mizuno, K., Kato, N., Ueda, K.: LMNtal: The Uni- fying Programming Language Based on Hierarchical Graph Rewriting. Computer Software 25(1), 1_124–1_150 (2008). https://doi.org/10.11309/jssst.25.1_124

    2008 doi

  14. [22]

    Elec- tronic Proceedings in Theoretical Computer Science 143, 54–66 (Apr 2012)

    Kissinger, A., Merry, A., Soloviev, M.: Pattern Graph Rewrite Systems. Elec- tronic Proceedings in Theoretical Computer Science 143, 54–66 (Apr 2012). https://doi.org/10.4204/EPTCS.143.5

    2012 doi

  15. [23]

    Information Technology Letters4, 9– 12 (Aug 2005), http://id.nii.ac.jp/1001/00147815/

    Kudo, S., Kato, N., Ueda, K.: Design and Implementation of Operation Constructs of Graph Structures in the LMNtal System. Information Technology Letters4, 9– 12 (Aug 2005), http://id.nii.ac.jp/1001/00147815/

    2005

  16. [24]

    In: Proceedings of the 17th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages

    Lafont, Y.: Interaction Nets. In: Proceedings of the 17th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages. pp. 95–108. POPL ’90, Association for Computing Machinery, New York, NY, USA (1989). https://doi.org/10.1145/96709.96718

    1989

  17. [25]

    In: 12th International Conference on Concurrency Theory (CONCUR ’01)

    Milner, R.: Bigraphical Reactive Systems. In: 12th International Conference on Concurrency Theory (CONCUR ’01). LNCS, vol. 2154, pp. 16–35. Springer-Verlag, Berlin, Heidelberg (2001). https://doi.org/10.1007/3-540-44685-0_2 18 K. Takyu and K.Ueda

    2001 doi

  18. [26]

    In: 34th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2024)

    Mishina, H., Ueda, K.: Introducing Quantification into a Hierarchical Graph Rewriting Language. In: 34th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2024). LNCS, vol. 14919, pp. 220–239 (2024). https://doi.org/10.1007/978-3-031-71294-4_13

    2024 doi

  19. [27]

    Muroya, K.: Hypernet semantics of programming languages. Ph.D. thesis, Univer- sity of Birmingham (2020)

    2020

  20. [28]

    Nguyên, L.T.D.: Unique perfect matchings, forbidden transitions and proof nets for linear logic with mix. Log. Methods Comput. Sci. 16 (2019). https://doi.org/10.23638/LMCS-16(1:27)2020

    2019 doi

  21. [29]

    In: Gadducci, F., Kehrer, T

    Overbeek, R., Endrullis, J., Rosset, A.: Graph Rewriting and Relabeling with PBPO+. In: Gadducci, F., Kehrer, T. (eds.) Graph Transformation (ICGT 2021). LNCS, vol. 12741, pp. 60–80. Springer, Cham (2021). https://doi.org/10.1007/978- 3-030-78946-6_4

    2021 doi

  22. [30]

    Theoretical Computer Science 411(2), 410–444 (2010)

    Pagani, M., Falco, L.T.d.: Strong normalization property for second or- der linear logic. Theoretical Computer Science 411(2), 410–444 (2010). https://doi.org/10.1016/j.tcs.2009.07.053

    2010 doi

  23. [31]

    Computer Graphics Forum31(3), 1265–1274 (2012)

    Pinaud,B.,Melançon,G.,Dubois,J.:PORGY:AVisualGraphRewritingEnviron- ment for Complex Systems. Computer Graphics Forum31(3), 1265–1274 (2012). https://doi.org/10.1111/j.1467-8659.2012.03119.x

    2012

  24. [32]

    In: The 21st Asian Symposium on Programming Languages and Systems SRC & Posters (2023)

    Takyu, K., Ueda, K.: Encoding MELL Cut Elimination into a Hierarchical Graph Rewriting Language. In: The 21st Asian Symposium on Programming Languages and Systems SRC & Posters (2023)

    2023

  25. [33]

    Torrini, P., Heckel, R.: Towards an embedding of Graph Transformation in Intu- itionisticLinearLogic.In:ElectronicProceedingsinTheoreticalComputerScience. vol. 12, pp. 99–115 (Dec 2009). https://doi.org/10.4204/EPTCS.12.7

    2009 doi

  26. [34]

    In: Grädel, E., Kahle, R

    Tranquilli, P.: Confluence of pure differential nets with promotion. In: Grädel, E., Kahle, R. (eds.) Computer Science Logic. pp. 500–514. Springer Berlin Heidelberg, Berlin, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04027-6_36

    2009 doi

  27. [35]

    Elec- tronic Notes in Theoretical Computer Science 209, 187–200 (2008)

    Ueda, K.: Encoding Distributed Process Calculi into LMNtal. Elec- tronic Notes in Theoretical Computer Science 209, 187–200 (2008). https://doi.org/10.1016/j.entcs.2008.04.012

    2008 doi

  28. [36]

    Theoretical Computer Science 410(46), 4784–4800 (2009)

    Ueda, K.: LMNtal as a hierarchical logic programming lan- guage. Theoretical Computer Science 410(46), 4784–4800 (2009). https://doi.org/10.1016/j.tcs.2009.07.043

    2009 doi

  29. [37]

    Ueda, K.: Gentle Introduction to LMNtal: Language Design and Implementation. Tutorial given at the 17th International Conference on Graph Transformation (ICGT 2024) (July 2024), https://conf.researchr.org/details/icgt-2024/icgt- 2024-research-papers/17/Gentle-Introduction-to-L...

    2024

  30. [38]

    In: Proc

    Ueda, K., Kato, N.: LMNtal: A language model with links and membranes. In: Proc. Fifth Int. Workshop on Membrane Computing (WMC 2004). LNCS, vol. 3365, pp. 110–125 (2005). https://doi.org/10.1007/978-3-540-31837-8_6

    2005 doi

  31. [39]

    Theses, Université de la Méditerranée - Aix-Marseille II (Jan 2007), https://theses.hal.science/tel-00194149

    Vaux, L.: λ-calcul différentiel et logique classique : interactions calcula- toires. Theses, Université de la Méditerranée - Aix-Marseille II (Jan 2007), https://theses.hal.science/tel-00194149

    2007

  32. [40]

    Tutorial given at the 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021) (June 2021), https://lipn.univ- paris13.fr/TLLA/2021/

    Vaux, L.: Proof nets. Tutorial given at the 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021) (June 2021), https://lipn.univ- paris13.fr/TLLA/2021/

    2021

  33. [41]

    IEEE Access 9, 133449–133460 (2021)

    Yasen, A., Ueda, K.: Revisiting graph types in HyperLMNtal: A modeling language for hypergraph rewriting. IEEE Access 9, 133449–133460 (2021). https://doi.org/10.1109/ACCESS.2021.3112903 Enhancing a Hierarchical Graph Rewriting Language 19 Appendix A LMNtal For the readers new...

    2021

  34. [43]

    A.1 Notes on the Syntax of LMNtal

    and handles rewrite rules as part of a process so that they can be placed inside membranes to express local rewriting inside them. A.1 Notes on the Syntax of LMNtal

  35. [44]

    Note that, if each ofP1 and P2 has a free link with the same name, it becomes a local link in(P1, P2)

    Parallel composition P1, P2 glues two processesP1 and P2 to build a larger process. Note that, if each ofP1 and P2 has a free link with the same name, it becomes a local link in(P1, P2). A reader may notice that the Link Con- dition may not always allow us to form(P1, P2) from...

  36. [45]

    For instance,a, (a:-b,c) may be written asa

    For readability, parallel composition may be written in a period-terminated form as well as in a comma-separated form. For instance,a, (a:-b,c) may be written asa. a:-b,c., where the comma binds tighter than ‘:-’ which in turn binds tighter than periods

  37. [46]

    This is used, for example, in the encoding of Rule (ax-cut) in Fig

    A special binary atom, called aconnector =(X, Y), also written as X= Y, fuses (or glues) two linksX and Y. This is used, for example, in the encoding of Rule (ax-cut) in Fig. 24

  38. [47]

    2.1) and named rules of the formname@@ T :- T (as in Sect

    As a practical extension to the original definition [36], the present syntax and our implementation allow named membranes of the formm{} (as in Sect. 2.1) and named rules of the formname@@ T :- T (as in Sect. 5.1)

  39. [48]

    For instance, a process a(L1,F),b(L1,L2,L3,L4),c(L2,L5,L6,L6),d(L5,L3,L4) stands for the undirected graph shown in Fig

    A term representing a process is subject to Structural Congruence defined in Section A.3, which then stands for anundirected port multigraph, i.e., a graph that allows multi-edges and self-loops. For instance, a process a(L1,F),b(L1,L2,L3,L4),c(L2,L5,L6,L6),d(L5,L3,L4) stands ...

  40. [54]

    https://doi.org/10.4230/LIPIcs.RTA.2013.39

    Dagstuhl, Germany (2013). https://doi.org/10.4230/LIPIcs.RTA.2013.39

    2013 doi

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.