arXiv:2303.14219v2 [cs.LO] 2 Apr 2023
|Preface Clemens Grabmayer||1|
|Invited Presentation: A Computational Interpretation of Girard's Intuitionistic Proof-Nets Delia Kesner||5|
|Invited Presentation: PBPO+ Graph Rewriting in Context Jörg Endrullis||7|
|From Double Pushout Grammars to Hypergraph Lambek Grammars With and Without Exponential Modality Tikhon Pshenitsyn||9|
|On Causal Equivalence by Tracing in String Rewriting Vincent van Oostrom||27|
|A PBPO+ Graph Rewriting Tutorial Roy Overbeek and Jörg Endrullis||45|
|Ideograph: A Language for Expressing and Manipulating Structured Data Stephen Mell, Osbert Bastani and Steve Zdancewic||65|
This volume contains the post-proceedings of TERMGRAPH 2022, the Twelfth Workshop on Computing with Terms and Graphs, which took place at Technion in Haifa, Israel, on August 1, 2022. The workshop was a one-day satellite event of the conference Formal Structures of Computation and Deduction 2022 (FSCD 2022, August 2–5), and as such it was part of the two-day Pre-FLoC workshop block (July 31–August 1) of the Federated Logic Conference 2022 (FLoC 2022, July 31–August 12). The workshop was held exclusively in-person without remote presentations. It had 16 registrations from paying FloC-participants. The attendance of the workshop was very good, with more than 25 participants.
Topics. The topic of workshops in the TERMGRAPH series (see also the general webpage www.termgraph.org.uk) are graphs, and graph transformation systems as used in many areas within Computer Science: to represent data structures and algorithms, to define computation models, as a general modeling tool to study complex systems, and so on. Research in term and graph rewriting ranges from theoretical questions to practical implementation issues. Areas of research include: the modeling of first- and higher-order term rewriting by (acyclic or cyclic) graph rewriting, the use of graphical frameworks such as interaction nets and sharing graphs (optimal reduction), rewrite calculi for the semantics and analysis of functional programs, graph reduction implementations of programming languages, graphical calculi modeling concurrent and mobile computations, object-oriented systems, graphs as a model of biological or chemical systems, and automated reasoning and symbolic computation systems working on shared structures.
Previous editions. The previous 11 editions of TERMGRAPH workshops had taken place in Barcelona (2002), Rome (2004), Vienna (2006), Braga (2007), York (2009), Saarbrücken (2011), Rome (2013), Vienna (2014), Eindhoven (2016), Oxford (2018), and online but planned to be held in Paris (2020).
Steering Committee. The Steering Committee of the TERMGRAPH workshop series consists of Andrea Corradini, Maribel Fernandez, Ian Mackie, and Detlef Plump (see the list with their affiliations below).
Program Committee. In my function as Chair of the Program Committee of TERMGRAPH 2022 I was thankful that nine experts with much experience in our field agreed to join the Program Committee: Sandra Alves, Martin Avanzini, Patrick Bahr, Thierry Boy de la Tour, Wolfram Kahl, Ian Mackie, Femke van Raamsdonk, Adrian Rutle, and Kazunori Ueda (see the list with their affiliations below).
Aim. Also for this edition of TERMGRAPH our aim was to bring together researchers who work with term graphs in several settings, foster their interaction, provide a forum for presenting new ideas as well as work in progress, and enable newcomers to learn about current activities in this area.
Submission (for workshop presentations). The call for papers (see here for the final version) was distributed widely and repeatedly, and it was published on the workshop's webpage www.termgraph.org.uk/2022. Also a poster announcement (pdf) was available. With deadline of May 12, 2022, we invited submissions of extended abstracts of at most 8 pages in EPTCS style concerning original work, tutorials, work in progress, and system descriptions of term-/graph rewriting tools on any of the topics of the workshops.
Invited Speakers. We were happy that Jörg Endrullis and Delia Kesner have accepted our invitation to come to Haifa in order to give in-presence talks. Their presentations were fantastic, and indeed well-received. I want to thank both of them for coming to our workshop despite of the long journey that it involved.
Review period (for workshop presentations). In the review period after the deadline of May 12, 2022, the Program Committee approved, after a thorough discussion process, 5 extended abstracts about a diversity of topics for presentation at the workshop. The final pre-proceedings versions of these accepted abstracts were published on the workshop webpage (see www.termgraph.org.uk/2022/#accepted) already on June 21, 2022. Also the program of the workshop (see below) was fixed in time within the early registration period of FLoC.
Workshop. The workshop at Technion in Haifa was a success with good participation, probing questions after talks, and a good deal of interaction in the breaks, and afterwards. In the weeks following the workshop, we could publish, on the workshop's website, the slides of some of the presentations (see here), and some pictures taken during the sessions (see here).
Submission (for post-proceedings articles). At the end of August we invited all authors of contributed and invited talks to submit a 15-page article to the post-proceedings with deadline at the end of October. I want to thank all authors of contributed papers for submitting articles to the post-proceedings. The invited speakers submitted abstract-only contributions of their talks at the workshop.
Review period (for post-proceedings articles). In the review process for the post-proceedings after the deadline of November 2, 2022, the Program Committee accepted 3 papers directly for publication, and one conditionally after undergoing a supervised minor revision. For leading that process of revision in the mentioned case to a successful conclusion, I want to thank Ian Mackie, and, for his supporting role, Kazunori Ueda.
Acknowledgements (scientific part).
I wish to thank all authors who submitted papers, the speakers,
the invited speakers, the program committee members, and the steering committee members.
In particular, I want to thank all PC members for their work, for sharing their ideas, for contributing strongly to the discussions in the review process, and above all for their support throughout the entire process. These efforts facilitated interesting scientific discussions at the workshop. The discussions in the two review periods have sometimes led to substantial changes in the final versions of the accepted papers, which added significant value to the here published versions. This has also been reflected by reactions that we have received from the authors.
In this respect I also want to commend the authors of all accepted papers for the strong efforts they undertook in preparing their final versions. To me that is testament to the significant amount of energy that even a medium-sized one-day event like a TERMGRAPH workshop can create.
For helping me on the way decisively with the organization of the workshop, I am indebted to SC Member Maribel Fernandez.
I thank her, and PC members Patrick Bahr and Femke van Raamsdonk
for sharing with me important pieces of their experience in
organizing past editions of TERMGRAPH workshops, and organizing such an event in general.
Also, I thank the program committee and the steering committee for additional suggestions concerning organizational matters.
In particular, I am grateful to SC member Ian Mackie for also serving on the PC,
for hosting the workshop's webpage the workshop's webpage,
and for being available for advice in a number of situations.
Furthermore, I thank EasyChair for supporting the submission and selection of the contributions. Importantly, I want to thank EPTCS for hosting these proceedings. In particular, I am very grateful to editor-in-chief Rob van Glabbeek for quick and reliable help at several occasions.
Andrea Corradini, University of Pisa, Pisa, Italy
Maribel Fernandez, King's College London, London, United Kingdom
Ian Mackie, University of Sussex, Brighton, United Kingdom
Detlef Plump, University of York, York, United Kingdom
Sandra Alves, Universidade do Porto, Porto, Portugal
Martin Avanzini, INRIA Sophia Antipolis – Méditerranée, Valbonne, France
Patrick Bahr, IT University Copenhagen, Copenhagen, Denmark
Thierry Boy de la Tour, CNRS, Grenoble, France
Clemens Grabmayer (chair), Gran Sasso Science Institute, L'Aquila, Italy
Wolfram Kahl, McMaster University, Hamilton, Canada
Ian Mackie, University of Sussex, United Kingdom
Femke van Raamsdonk, Vrije Universiteit Amsterdam, Amsterdam, The Netherlands
Adrian Rutle, Western Norway University, Bergen, Norway
Kazunori Ueda, Waseda University, Tokyo, Japan
Delia Kesner: A Computational Interpretation of Girard's Intuitionistic Proof Nets
Tikhon Pshenitsyn: Transformation of DPO Grammars into Hypergraph Lambek Grammars With The Conjunctive Kleene Star
Vincent van Oostrom: Greedily Decomposing Proof Terms for String Rewriting into Multistep Derivations by Topological Multisorting
Roy Overbeek: A PBPO+ Graph Rewriting Tutorial (joint work with Jörg Endrullis)
Jörg Endrullis: PBPO+ Graph Rewriting in Context
Tim Kräuter: Formalization and analysis of BPMN using graph grammars (joint work with Harald König, Adrian Rutle, and Yngve Lamo)
Stephen Mell: Ideograph: A Language for Expressing and Manipulating Structured Data (joint work with Osbert Bastani and Steve Zdancewic)
In this talk we will present a computational interpretation of Girard's proof nets for intuitionistic linear logic. More precisely, proof nets are a graphical formalism representing bureaucracy-free proofs, i.e., the order in which independent logical rules are applied in a derivation is abstracted. Despite the obvious advantage of the graphical notation, the essence of their corresponding operational semantics is not always clear from a programming point of view, and a term syntax often provides a complementary understanding of a (bureaucracy-free) graph framework.
Our goal is to define a new term language that establishes a faithful and fine-grained Curry-Howard correspondence with Girard's intuitionistic NP, both from a static (objects) and dynamic (reductions) point of view. On the static side, we identify an equivalence relation on terms which is sound and complete with respect to the classical notion of structural equivalence for proof-nets. On the dynamic side, we show that every single (exponential) step in the term calculus translates to a different single (exponential) step in the graphical formalism, thus capturing the original Girard's granularity of proof-nets but on the level of terms.
This presentation is and concerns joint work with Roy Overbeek and Aloïs Rosset.
I give an overview of various results on graph rewriting with PBPO+ [6,7], a versatile graph rewriting formalism based in category theory. PBPO+, short for Pullback-Pushout with strong matching, is an extension of PBPO by Corradini et al. .
PBPO+ was proposed after trying to find a categorical formulation of patch graph rewriting , a set-theoretic framework which allows for a fine-grained control over the embedding of the pattern in the host graph and the transformation of this embedding through a rewrite step. This control is important for a large class of rewrite systems.
Our most important result thus far is that PBPO+ can be considered a unifying theory in the general setting of quasitoposes , because it can define a strict superset of the rewrite relations definable by DPO , SqPO , AGREE  and PBPO .
Additionally, we have shown that PBPO+ can be considered a generalization of linear term rewriting, in the sense that every linear term rewriting system can be faithfully encoded into PBPO+. Moreover, this encoding preserves termination, even on the full domain of finite graphs.