-------------------------------------------------------------------------------- IFIP Working Group 1.6 on Term Rewriting Report of the annual meeting: June 30, 2020 (Paris, France, virtual) Chair: Georg Moser Secretary: Martin Avanzini -------------------------------------------------------------------------------- PARTICIPANTS Aart Middeldorp Akihisa Yamada (invited) Besik Dundua Carsten Fuhs (invited) Chris Lynch Cynthia Kop Dan Dougherty Deepak Kapur Delia Kesner Enno Folkerts Femke van Raamsdonk Florent Jacquemard Georg Moser Gilles Dowek Hans Zantema Helene Kirchner Jakob Grue Simonsen (invited) Juergen Giesl Luigi Liquori Maribel Fernandez Martin Avanzini Nachum Dershowitz Nao Hirokawa Narciso Marti-Oliet Olivier Hermant Rene Thiemann Salvador Lucas Sarah Winkler Silvia Ghilezan Takahito Aoto Temur Kutsia -------------------------------------------------------------------------------- AGENDA 1) Presentation by Carsten Fuhs (invited) 2) Report on ISR 2019 (Paris) by Olivier Hermant 3) Reminder on ISR 2021 (Madrid) by Narciso Marti-Oliet 4) Proposal for ISR 2022 (Tiblisi) by Besik Dundua and Temur Kutsia 5) Presentation by Jakob Grue Simonsen (invited) 6) Presentation by Akihisa Yamada (invited) 7) Business Meeting 8) New Models for Conferences of Interest to the WG -------------------------------------------------------------------------------- 1) Presentation by Carsten Fuhs Title: Transformational Complexity Analysis of Term Rewriting Abstract: For term rewrite systems (TRSs), automatic bound inference techniques and tools for complexity properties have been studied in several forms. Derivational complexity (dc) considers the length of the longest derivation with a TRS starting from arbitrary terms, whereas runtime complexity (rc) considers only basic terms (i.e., function calls on constructor terms) as start terms. Similarly, bound inference techniques and tools have been devised for integer transition systems (a simple form of imperative programs on integer variables), which can also be seen as a restricted kind of TRS with integer constraints. In this talk, I present transformations between different kinds of complexity properties: a complexity-equivalent transformation from dc to rc and a complexity-overapproximating transformation from (innermost) rc to complexity of integer transition systems. These transformations allow for reusing and extending existing techniques and tools for complexity analysis and for automatically finding non-trivial bounds for examples that had been out of reach of automatic analysis before. 2) Report on ISR 2019 (Paris) by Olivier Hermant Olivier Hermant gave a brief report on ISR'19: - held at MINES ParisTech - ultimately organised by F. Blanqui and O. Hermant - Student rooms were booked out and students were redirected to affordable hotels - 15 preposals for advanced courses received/3 rejected mainly based on renewal of topics and lecturers - 6 instead of 5 days schedule to accommodate large number of lectures - two student events held (5 mins student talk session and poster session) - registration fees could be held below 300Euro due to extensive sponsoring - 37 participants (13 in basic and 24 in advanced track) - end-of-school survey results: - high satisfaction - too few lambda-calculus - more time to work after lectures requested - Organisers were happy with the work/involvement of IFIP - attendance very local (29 out of 37 from France) - suggested that IFIP members get more involved with attracting students - ISR could be organised more globally (e.g. outside Europe) - one could try for broader advertisement 3) Reminder on ISR 2021 (Madrid) by Narciso Marti-Oliet Narciso Marti-Oliet reported on ISR'21 with emphasis on differences to ISR'20 planning: - ISR 2020 postponed to 2021 due to corona-pandemic - lectures were already fixed and all agreed to shift in timeframe - student registration did not open yet when decision to postpone was taken - incorporated lessions learned from ISR'19 organisation - back to 5 days with shorter courses - general open call for lectures - basic track covers rewriting (Salvador Lucas), Lambda Calculus (Jean-Jacques Levy) and unification and narrowing in Maude (by Santiago Escobar) - 10 diverse advanced tracks - concrete dates still to be fixed (taking into account FSCD dates) - price estimations (300--350Euro registration; ~45Euro student lodging) could change due to pandemic - certificate of attendance and certificate for exam planned so that students can earn ECTS points Questions by Narciso: - in case of continuation of pandemic, does it make sense to organise virtual summer school? - Georg, Temur: could be an option exceptionally; possibly only for advance track - Aart: raises question of financing; may be also an opportunity 4) Proposal for ISR 2022 (Tiblisi) by Besik Dundua and Temur Kutsia Temur Kutsia proposes Tiblisi for ISR 2020: - main venue: Tibilisi state university - large university conveniently located in city center - good and affordable access - suitable facilities - very affordable lodging - intention to have ISR part of bigger event CLAS'22 (Computational Logic Autumn summer school); sequentially and not in parallel, possibly with overlaps - extensive experience in organising schools present - usual basic/advanced track format planned - one week in second half of September targeted - estimated registration fee 200/250Euro (early/late) 5) Presentation by Jakob Grue Simonsen Title: Marginalia to Rewriting with Computability and Ordinals Abstract: We take the opportunity to address a general crowd of rewriters with a sequence of loosely connected margin notes on some fascinating aspects of rewriting that occasionally receive less attention than they deserve: junk terms, computability, and alternative uses of ordinals. 6) Presentation by Akihisa Yamada Title: Isabelle/HOL formalizations of Logically Constrained Rewriting, Sub-Birkoff and Isomorphism Theorems Abstract: Constrained rewriting is a promising model of computation that represents recursive procedural programs well. In this talk, I present an Isabelle/HOL formalization of constrained rewriting, based on the Isabelle Formalization of Rewriting (IsaFoR) library. The prerequisite notions, sorted terms, algebras, and logics, are designed carefully, so that fundamental results such as the (sub-)Birkoff theorem and the isomorphism theorem are formalized in a general and elegant manner. 7) Business Meeting Attendees: Cynthia Kop, Dan Dougherty, Deepak Kapur, Georg Moser, Gilles Dowek, Hans Zantema, Helene Kirchner, Juergen Giesl, Maria Paola Bonacina, Martin Avanzini, Masahiko Sakai, Nachum Dershowitz, Rene Thiemann, Salvador Lucas, Silvia Ghilezan, Takahito Aoto, Vincent van Oostrom - It has been voted unanimously in favor of the ISR 2022 proposal Tibilisi. - During the presentation, Narciso Marti-Oliet asked the working group about its opinion on fallback solutions should the pandemic return so that a live school is not possible. The working group discussed several options. Overall, the group has been in favor of a mixed offer where live event is combined with an online course, which also serves as a fallback in case of a pandemic. Georg Moser will convey this opinion to the ISR organisers. - The three invited speakers (Akihisa Yamada, Carsten Fuhs, Jakob Grue Simonsen) have been voted unanimously to join IFIP WG 1.6 via an open vote. - Several members have been inactive over the last years and will be contacted by Georg Moser. - Members of the working group are urged to propose candidates for the position of chairs of this working group. A vote for replacement will be initiated by the chair once candidates have been selected. 8) New Models for Conferences of Interest to the WG The WG hosted a panelist session with Damiano Mazza, Jakob Rehof, Moshe Vardi and Jamie Vicary: - Moshe Vardi presented arguments against the established model of scientific conferences/journals etc. - Damiano Mazza motivated and proposed an evolution of FSCD and its satellite workshops as a new event without formal proceedings. - Jakob Rehof urges for decoupling publication and scientific meeting. - Jamie Vicary emphasized the role of social engagement during conferences and a good online replacement should take social interactions into account.