The date for the annunal meeting WG 1.6 is Tuesday, June 30, 2020. The WG 1.6 is part of (virtualised) FSCD-IJCAR and will take place as pre-conference workshop.
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.
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.
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.
9:00-9:45: Session 1
- 15' short presentation Carsten Fuhs
- 30' discussion
15' short break
10:00-11:00: Session 2
- 15' report ISR 2019 (Paris) by Olivier Hermant
- 15' reminder ISR 2021 (Madrid) by Narciso Marti Oliet
- 15' proposal ISR 2022 (Tbilisi) by Besik Dundua and Temur Kutsia
- 15' discussion
11:00-11:30 Virtual coffee break
11:30-12:15: Session 3
- 15' short presentation Jakob Grue Simonsen
- 30' discussion
12:15-13:00: Session 4
- 15' short presentation Akihisa Yamada
- 30' discussion
13:00-14:00 Lunch break
14:00-15:30: Business Meeting
- memberships
- auxiliary topics
15:30-16:00 Virtual coffee break
16:00-17:30: Session 5
- discussion: New Models for Conferences of Interest to the WG
- panel: Damiano Mazza, Jakob Rehof, Jamie Vicary, Moshe Vardi
The meetings of the working group are public, with the single exception of the business meeting.