The date for the annual meeting of the IFIP WG 1.6 is Sunday, July 31, 2022. The meeting is co-located with FSCD 2022 at FLoC 2022, and will take place as a pre-conference workshop.
Abstract: Weak linearisation was defined years ago through a static characterisation of the intuitive notion of virtual redex, based on (legal) paths computed from the (syntactical) term tree. Weak-linear terms impose a linearity condition only on functions that are applied (consumed by reduction) and functions that are not applied (therefore persist in the term along any reduction) can be non-linear. This class of terms was shown to be strongly normalising with deciding typability in polynomial time. We revisit this notion through non-idempotent intersection types (also called quantitative types). By using an effective characterisation of minimal typings, based on the notion of tightness, we are able to distinguish between “consumed” and “persistent” term constructors, which allows us to define an expansion relation, between general lambda-terms and weak-linear lambda-terms, whilst preserving normal forms by reduction.
Abstract: As a transformational approach, inversion is formulated in several settings, and the basic ideas are naive and similar. To generate a better form, e.g., non-overlapping systems if possible, determinization is used as a post-process of inversion for injective functions, and is the most challenging part in developing an inversion framework. In this talk, I introduce a framework of inversion and determinization in term rewriting. First, I explain a direct inversion of deterministic CTRSs, and a direct MSV-based determinization. Next, I explain the framework proposed by Gluck and Kawabe, which uses context-free grammars as intermediate representations of CTRSs. Finally, I explain a framework based on context-free expressions.
09:30 - 10:30: Session 1
- 60' presentation Naoki Nishida
- 30' the Rewriting List of Open Problems by Jörg Endrullis
10:30 - 11:00: Break
11:00 - 12:30: Session 2
- 60' presentation Sandra Alves
- 30' the International School on Rewriting by Aart Middeldorp
12:30 - 16:00: Break
16:00 - 17:30: Session 4: business meeting (members-only)
The meetings of the working group are public, with the single exception of the business meeting.