-------------------------------------------------------------------------------- IFIP Working Group 1.6 on Term Rewriting Report of the annual meeting: 1 July 2024 (Nancy, France, hybrid) Chair: Cynthia Kop Co-Chair/Secretary: Carsten Fuhs -------------------------------------------------------------------------------- AGENDA (1) Presentation by Claudia Faggian (2) Presentation by Clemens Grabmayer (3) Presentation by Santiago Escobar (4) Presentation by Daniele Nantes (5) Presentation by Uwe Waldmann (6) The International School on Rewriting by René Thiemann (7) Presentation by Jean-Pierre Jouannaud: Rooted Graph Rewriting (8) Business Meeting (memberships, auxiliary topics) -------------------------------------------------------------------------------- (1) 9:00 Claudia Faggian Title: Rewriting for Bayesian inference: how to compile a higher-order probabilistic program into a Bayesian network Abstract: Probabilistic models play a crucial role to reason under uncertainty. This talk relies on rewriting theory and semantical techniques to relate two such models: on the one hand, *probabilistic programming languages*, where statistical models are specified as programs, on the other hand *Bayesian networks*, a prominent tool for probabilistic reasoning, allowing for a compact (factorized) representation of large probability distributions, and for efficient inference algorithms. The goal is integrating the efficiency of Bayesian networks---which are graphical first-order models---with the expressiveness of higher-order functional programming. Ideally, the design of the Bayesian model should be carried at high-level, in the functional language, which provides recursion and expressive constructs. Higher-order terms then compile (i.e. rewrite) into Bayesian networks, which serve as the low-level language. The groundwork for the compilation scheme are semantical tools, in particular rewriting theory and type systems. (This talk reports on work in collaboration with Ehrhard, Pagani, Pautasso, Vanoni.) (2) 9:45 Clemens Grabmayer Title: The Graph Structure of Process Interpretations of Regular Expressions Abstract: Center-stage of my talk will be a structural property of process graphs that are interpretations of regular expressions: the loop existence and elimination condition (LEE). It turned out to be instrumental for tackling axiomatization and recognition problems for Milner's process semantics of regular expressions. Next to indicating its role in my work on these problems, I want to explain how concepts and ideas from rewriting are crucial for the definition of LEE and the study of its properties. LEE is defined by a terminating loop-subgraph-elimination rewrite system. This system can be completed into a confluent system, which entails that LEE is efficiently decidable. Process interpretations of regular expressions satisfy LEE if they are `under-star-1-free', and in general if they satisfy a refinement property 1-LEE, which requires of a process graph to be refinable into a graph with LEE by means of increasing sharing through added 1-transitions (empty steps). `LEE-witnesses' are labelings of process graphs that satisfy LEE. They guarantee expressibility by a regular expression: every process graph G with a LEE-witness facilitates the efficient extraction of a regular expression whose process interpretation is bisimilar to G. Two further lemmas are of critical importance for obtaining completeness results. First, LEE is preserved under bisimulation collapse; this can be established by a stepwise collapse procedure. However, second, 1-LEE is not preserved under bisimulation collapse. Finally I report on a recent technical refinement of the extraction procedure that permits to understand LEE/1-LEE as characteristic properties for the restricted/unrestricted images of a (slightly more) compact version of the process interpretation. LEE (and resp. 1-LEE) characterizes those process graphs that are isomorphic to compact process interpretations of under-star-1-free regular expressions (resp. that refine compact process interpretations of arbitrary regular expressions). (3) 11:00 Santiago Escobar Title: Unification and Narrowing in Maude 3.4 Abstract: Maude is a language and a system based on rewriting logic. It is a mathematical modeling language thanks to its logical basis and its initial model semantics. Maude can be used in three, mutually reinforcing ways: as a declarative programming language, as an executable formal specification language, and as a formal verification system. Logical reasoning capabilities have been recently added to Maude. This talk gives an overview of the different unification and narrowing techniques available in Maude 3.4, focusing on some of the programming, modeling, and verification aspects of Maude. (4) 11:45 Daniele Nantes Title: From Pi-Calculus to Lambda-Calculus: Exploring Expressivity through Session Types and Intersection Types Abstract: In this talk, I will present recent research on the expressivity of concurrent languages, utilizing a session-typed pi-calculus that incorporates non-determinism and failure behaviour. Building on an extension of Milner's encoding from the pi-calculus to the lambda-calculus, we have discovered a novel relationship between session types and intersection types. This research introduces a translation from the session-typed pi-calculus to a resource-aware lambda-calculus with intersection types. Our translation preserves typability and operational correspondence, enabling the transfer of dynamic properties between these two languages. (5) 14:00 Uwe Waldmann Title: The Saturation Framework Abstract: Saturation theorem provers process a set of formulas by repeatedly performing two operations: first, by applying inference rules to formulas in the set, whose conclusions are then added to the set; second, by deleting formulas that are redundant, which means that they can be shown to be unnecessary to derive a contradiction. The relationship between redundancy, saturation, and static and dynamic refutational completeness was established by Bachmair and Ganzinger in the 1990s. The abstract framework for saturation theorem proving that we presented in 2020 extends the work by Bachmair and Ganzinger. In my talk, I will discuss the framework, its history, applications, and recent developments and extensions. (6) 14:45 René Thiemann International School on Rewriting (ISR) In the first part of his presentation, René Thiemann reported on the preparations for ISR 2024, organised by him, Aart Middeldorp, and Georg Moser as well as Gernot Baumgartner and Martina Ingenhaeff (all University of Innsbruck): ISR 2024 http://cl-informatik.uibk.ac.at/isr24/ takes place from 25 August to 1 September 2024 at the University Center Obergurgl, Austria. It has three tracks: A basic track on rewriting B basic track on lambda-calculus and type theory C advanced track (5 courses with 4 slots each, each slot has 1.5 hours) Tracks A and B will offer an optional test, allowing participants to obtain an ECTS certificate. The School consists of 5 days with courses and 1 day of excursion. Registration numbers at this point in time were: Track A: 8 Track B: 18 Track C: 12 René Thiemann pointed out that the fee of EUR 900 with full board was pushed to the lower limit and thanked funding by the Kurt Gödel Society, the Computer Science Department of the University of Innsbruck, the University of Innsbruck, Aurora, and the COST Action CA20111 EuroProofNet (student travel grants). In the second part of his presentation, René Thiemann addressed proposals for ISR 2026. He reported that no calls for proposals for the next ISR had been sent. He stated that the student travel grants by EuroProofNet had been helpful for raising student numbers. He concluded that given the current level of interest, making ISR annual would not be advisable. René Thiemann pointed out that according to the bylaws, proposals for ISR 2026 would have had to be presented at this IFIP WG meeting. The call for proposals would be sent likely this week. René Thiemann suggested that members of the IFIP WG 1.6 should consider whether to host ISR and which tracks might be suitable. He also suggested that WG members should think about offering a lecture for ISR if asked to do so. As the next steps for ISR 2026, he stated that proposals would be announced via the IFIP WG 1.6 mailing list, followed by an online vote. This was followed by a short discussion among meeting participants how interest in ISR could be increased, concluding the topic of ISR. (7) 15:15 Jean-Pierre Jouannaud Rooted Graph Rewriting In this presentation, honorary WG member Jean-Pierre Jouannaud presented his work on Rooted Graph Rewriting. (8) 16:30 IFIP WG 1.6 Business meeting Attendees: Aart Middeldorp (online) Carsten Fuhs Christopher Lynch (online) Cynthia Kop David Plaisted (online) Delia Kesner (online) Femke van Raamsdonk (online) Hélène Kirchner (online) Jürgen Giesl Luigi Liquori (online) Maribel Fernández (online) Mauricio Ayala-Rincón Nachum Dershowitz (online) Nao Hirokawa (online) Naoki Nishida (online) Ralf Treinen René Thiemann Sandra Alves (online) Temur Kutsia Vincent van Oostrom (online) The first point addressed in the business meeting consisted of a proposal for codified bylaws for the WG by Cynthia Kop. The bylaws were discussed in detail by the attendees of the meeting and rewritten based on this discussion. The plan would be to vote on the updated bylaws via the mailing list of the WG. The next point addressed in the business meeting was the changed approach to membership for invited speakers: in contrast to recent years, now two invited talks at the WG are considered a prerequisite for an invitation to join the WG. Cynthia Kop mentioned that in 2024 five invited speakers with similar scores had been invited rather than three per meeting as in previous years, and that this was not followed by immediate membership. She pointed out that now the WG could invite researchers, e.g., at postdoc stage and reinvite them at a more senior stage of their career. This was followed by a short discussion on the benefits of inviting early-career researchers to speak at or join the WG. The following point was the location of the next meeting of the WG. Here co-locations with FSCD 2025 in Birmingham, CADE 2025 in Stuttgart, or WST/IWC/WPTE 2025 in Leipzig were mentioned, where the availability of the last option would still need to be checked. Concerning other business, the point was raised that it would be nice to get a reminder of the programme shortly before the event, and it was mentioned that a reminder of the meeting had been sent a day before the meeting. This led to the enquiry whether the programme had been sent to IJCAR 2024 and made available on the conference website, perhaps in a joint workshop programme, followed by a remark that this was a problem also for other workshops (the IJCAR 2024 website contained links to the co-located workshops, but no collated workshop programme). As the final topic at the business meeting, Luigi Liquori provided an update on the ongoing efforts for the modernisation of the http://rewriting.org/ website. He reported that he currently had a student with a background in Human-Computer Interaction working on the updated website. The plan would be to release a beta version with full documentation and with the content of the current website hosted at Loria in the next months, followed by closing the then-obsolete Loria website. There was also some discussion on the possibility of the website being a wiki, or functioning similar to one. However, no concrete decisions were taken on this option. At this point, the meeting was closed.