-------------------------------------------------------------------------------- IFIP Working Group 1.6 on Term Rewriting Report of the annual meeting: 5 July 2023 (Rome, Italy, hybrid) Chair: Cynthia Kop Co-Chair/Secretary: Carsten Fuhs -------------------------------------------------------------------------------- PARTICIPANTS Aart Middeldorp Akihisa Yamada Alexis Rosset (online) Carsten Fuhs Christopher Lynch (online) Clemens Grabmayer Cynthia Kop David Plaisted (online) Deepak Kapur (online) Deivid Vale Delia Kesner Frédéric Blanqui Jürgen Giesl Liye Guo Luigi Liquori Makoto Hamana (online) Maria Paola Bonacina Maribel Fernández Martin Avanzini (online) Mauricio Ayala Rincón Nao Hirokawa Naoki Nishida Sandra Alves Sarah Winkler (online) Takahito Aoto (online) Temur Kutsia Thiago Felicissimo Yuta Takahasi (online) ... (overall 26 in-person participants, 9 online participants) -------------------------------------------------------------------------------- AGENDA (1) Presentation by Thomas Genet (2) The International School on Rewriting by Aart Middeldorp (3) Presentation by Temur Kutsia (4) Presentation by Frédéric Blanqui (5) Rewriting Website by Luigi Liquori (6) Business Meeting (memberships, auxiliary topics) -------------------------------------------------------------------------------- (1) 10:30 Thomas Genet Title: Using Tree Automata for Verification, at last Abstract: Tree automata are a formalism based on term rewriting to represent unbounded regular sets of terms. The first attempts to use tree automata for program verification date back to 1987. Since then, a long standing research activity has tried to improve these first results to expand their applicability, improve their verification power, or explore their theoretical limits. During those 40 years of research, this small community came up with many results but very few applications to real verification problems. Verification of cryptographic protocols being one of them. However, several recent papers from the formal verification community suggest that new applications may arise. A first application is the automatic verification of real size higher-order functional programs. Another application is the extension of SMT solvers with regular tree languages techniques to automatize the verification of programs manipulating Algebraic Data Types. (2) 11:20 Aart Middeldorp International School on Rewriting (ISR) Aart Middeldorp reported on the preparations for ISR 2024, organised by his group at the 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 two basic tracks: an introductory course on first-order term rewriting, and an introductory course on lambda calculus and type theory. There is also an advanced track with 5 courses of 4 slots each, where one slot corresponds to 90 minutes. All courses are accompanied by exercises. Maria Paola Bonacina raised the question of student numbers. Aart Middeldorp responded that the advanced track at ISR 2022 had not been well attended (4 students), but that the numbers of earlier editions of ISR (e.g., Leipzig, Eindhoven, Paris) had been well attended. Mauricio Ayala Rincón added that the numbers for the editions of ISR held in South America (e.g., Valparaíso) had also been good. Luigi Liquori pointed out that August was a good period for a summer school. (3) 11:40 Temur Kutsia Title: Symbolic techniques for quantitative extensions of equality Abstract: Quantitative extensions of equality characterize the approximation degree between objects. Fuzzy proximity and similarity relations are notable examples of such extensions. These and similar relations are used to model concepts such as vagueness, uncertainty, imprecision, imperfectness. Various approaches to formalizing quantitative information lead to the development of well-known logical, algebraic, and topological formalisms and structures such as e.g., fuzzy logic, rough logic, metric algebras, quantitative algebras, metric and proximity spaces, etc. Symbolic constraint solving is ubiquitous in many areas of mathematics and computer science. Unification, matching, anti-unification, disunification, and ordering constraints are some prominent examples that play an important role in automated reasoning, term rewriting, declarative programming, and their applications. In this talk, we present recent advances in solving unification and anti-unification constraints in theories where equality is replaced by its quantitative approximation. Our algorithms solve unification, matching, and anti-unification problems modulo fuzzy tolerance (i.e., reflexive and symmetric but not necessarily transitive) relations where mismatches between symbol names and arities are permitted. We will discuss general principles behind these techniques, show examples, present some of the algorithms, and characterize their properties. (4) 14:00 Frédéric Blanqui Title: Lambdapi, a proof assistant using rewriting Abstract: In this talk, I will present Lambdapi, a proof assistant on top of the Dedukti logical framework, which extends Edinburg's Logical Framework LF or, equivalently, Martin-Löf's logical framework, but allowing objects and types to be defined by higher-order rewriting rules, possibly modulo commutativity, or associativity and commutativity together. Dedukti is a logical framework, that is, it does not come with a predefined logic. Instead one can define its own logic in it. This is used to encode not only the terms and propositions of many different provers but also the proofs that are actually developed in those provers. This goes from automated theorem provers based on first-order logic, interactive theorem provers based on Church's simple type theory like HOL-Light or Isabelle/HOL, to rich type systems like the ones of Coq, Agda or Lean. Rewriting is a key feature for encoding the proofs of those systems in Dedukti. Moreover, once a proof is encoded in Dedukti, it can be translated to other provers, depending on the deduction rules and features of the source system that are used in it, and the deduction rules and features of the target system. However, a number of properties of rewrite systems need to be checked by users for Lambdapi to behave properly like termination, confluence and preservation of typing, aka subject reduction. To this end, Lambdapi provides some useful tools: exports to the XTC and HRS formats, a procedure for checking subject-reduction automatically, and a procedure for checking local confluence incrementally. (5) 14:50 Luigi Liquori Rewriting Website Luigi Liquori reported on progress with refreshing the portal website http://rewriting.org hosted in Nancy at Loria and originally set up by Nachum Dershowitz and Laurent Vigneron about 20 years ago. The goal would be to set up a reactive website, completely hosted at Inria, which could be viewed sensibly on any device. To this end, Alexis Rosset had done a two-months internship with Luigi Liquori, who had also consulted with Nachum Dershowitz, Pierre Lescanne, and Cynthia Kop. The URL of the website: https://rewriting.inria.fr The website should support tags, different tab-like sections, an intranet, and browser-based edit functionality. Software used for the new website includes Docker Composer and MongoDB. Current maintainers are Cynthia Kop, Luigi Liquori, and Alexis Rosset. The next steps would be to populate the page with content, analyse data from the old site, stress-test the site, propose new features, and ask for a new student to work on the site. Jürgen Giesl raised the question whether everyone with access rights would be able to change the website without moderation. Luigi Liquori responded that at the moment there was no hierarchy. Jürgen Giesl pointed to the site https://termination-portal.org/ as a related project for termination analysis with similar user logins. He mentioned the open problem list of RTA https://www.win.tue.nl/rtaloop/ and pointed to the fact that then everyone would be able to rearrange it. He also mentioned that a new PhD student had mentioned interest two days ago and enquired whether he would be able to join the project. (6) 15:15 IFIP WG 1.6 Business meeting Attendees included: Aart Middeldorp Akihisa Yamada Carsten Fuhs Christopher Lynch (online) Cynthia Kop David Plaisted (online) Delia Kesner Jürgen Giesl Luigi Liquori Maribel Fernández Martin Avanzini (online) Mauricio Ayala Rincón Naoki Nishida Sandra Alves Sarah Winkler (online) Takahito Aoto (online) The three invited speakers (Frédéric Blanqui, Temur Kutsia, Thomas Genet) were voted unanimously to be invited to join IFIP WG 1.6 via an open vote. In this context, the topic was raised how many invited presentations should be required so that someone would be invited to join the WG. Historically, 3 presentations had been required, later 2, and since a few years 1. It was discussed whether raising this number to 2 again would be a good idea for future membership. An action item was identified that these rules should be codified. Delia Kesner and Maribel Fernández suggested checking the practices in other IFIP WGs as input information. Cynthia Kop pointed out that due to the limited available time for the business meeting slot on 5 July 2023, a longer online business meeting would be held in a few weeks' time, providing opportunity for a longer discussion. One goal of the current meeting would be to collect topics for the online business meeting. Topics that were identified included: - Should an annual report be released beyond the current one? - Should a three-day standalone workshop be held by the WG? Regarding the Rewriting portal website, Aart Middeldorp enquired whether it would be integrated with the efforts proposed by Jörg Endrullis at the WG meeting in 2022 to set up a new site for the RTA List of open Problems. Cynthia Kop mentioned that Jörg Endrullis seemed busy and that there had not been updates. Luigi Liquori pointed out that reworking rewriting.org would likely take 2 months for 3-4 people and that volunteers were very welcome to contact him. Cynthia Kop thus encouraged anyone (also non-members of the WG) interested in helping with the work on rewriting.org to e-mail Luigi Liquori. Further discussions were postponed to a planned full business meeting to be held virtually in the coming weeks.