-------------------------------------------------------------------------------- IFIP Working Group 1.6 on Term Rewriting Report of the annual meeting: July 8, 2018 (Oxford, England) Chair: Georg Moser Secretary: Martin Avanzini -------------------------------------------------------------------------------- PARTICIPANTS Aart Middeldorp Beniamino Accatolli (invited) Brigitte Pientka Claude Kirchner Delia Kesner Femke van Raamsdonk Georg Moser Hans Zantema Hélène Kirchner Jean-Pierre Jouannaud Luigi Liquori (invited) Luke Ong Maribel Fernández Martin Avanzini (invited, secretary) Nachum Dershowitz Pierre Lescanne Takahito Aoto -------------------------------------------------------------------------------- AGENDA 1) Presentation by Beniamino Accattoli (invited) 2) Presentation by Martin Avanzini (invited) 2) Presentation by Luigi Liquori (invited) 3) Report on ISR by Frédéric Blanqui (ISR) 4) Informal report on FSCD by Helene Kirchner and Discussion on Reviewing Culture in TCS 5) Discussion on IFIP and Business Meeting -------------------------------------------------------------------------------- 1) Presentation by Beniamino Accattoli. Title: (In)Efficiency and Reasonable Cost Models Abstract: This talk is about time cost models for the λ-calculus. To allow the definition of basic complexity classes such as P or EXP directly in the lambda-calculus, a cost models has to be reasonable, that is, polynomially related to the one of Turing machines. For the lambda-calculus the existence of an evaluation strategy whose number of steps is a reasonable cost model has been a long-standing open problem. Positive answers to special cases were known since 1995, but a solution for the general case has been provided only in 2014. The problem is peculiar because some of its aspects are somewhat counterintuitive. This talk is devoted to explain the subtleties of this fundamental topic. The key point that is often misunderstood, and that is here discussed at length, is that being efficient and being reasonable are two unrelated properties of evaluation strategies. 2) Presentation by Martin Avanzini. Title: Probabilistic Term Rewriting and the Interpretation Method Abstract: In their seminal RTA'05 paper, Bournez and Garnier introduce probabilistic term rewrite system together with a technique, based on Lyapunov ranking functions, for establishing almost-sure termination of such systems. In this talk, I will present recent work with Ugo Dal Lago and Akihisa Yamda where we have revisited Bournez and Garnier's work. First, we have captured reductions of probabilistic rewrite systems in a novel way by means of multidistribution reduction sequences, thus accounting for both the nondeterminism in the choice of the redex and the probabilism intrinsic in firing each rule. Second, we have extended the interpretation method to the probabilistic setting, taking inspiration from Bournez and Garnier's termination technique. This method constitutes a significant generalisation, in particular, it is not restricted to the Reals and can be instantiated, e.g., by matrix interpretations. 2) Presentation by Luigi Liquori. Title: Why reductions must be synchronised in intersection and union typed λ-calculi Abstract: We present the ∆-calculus, an explicitly typed λ-calculus with strong pairs, projections and explicit type coercions. The calculus can be parametrized with different intersection type theories, as described in the Barendregt-Dekker-Statman book on λ-calculi with types, producing a family of ∆-calculi with related intersection typed systems. We show why annotating pure λ-calculus with intersection types is not easy: a classical example is the difficulty to decorate the bound variable of the explicitly typed polymorphic identity λx:?.x such that the type of the identity is (σ → σ) ∩ (τ → τ): previous attempts showed that the full power of the intersection type discipline can be easily lost. We show why intersection typed systems need a kind of synchronised reduction to fix the subject reduction theorem. The same issues also appear when decorating λ-calculus with union-types. We also show a rewriting-based subtyping algorithm. Finally, we show how the ∆-calculus can be raised to a ∆-framework by adding dependent-types as in the Edinburgh Logical Framework. 3) Report on ISR by Frédéric Blanqui (ISR) Proposal 2019: Frédéric Blanqui recalled the proposal for ISR 2019 to be held in Paris and reported on the recent state of the organisation of the school: - It has now been decided that the school will be held in the first week of July - It is planned to keep the costs similar to previous iterations of ISR - The organisers are in the process of contacting teachers as well as asking for grants. Poster Sessions: The possibility of having a dedicated poster session were discussed. Femke van Raamsdonk recalled the procedure at ISR 2017: - Students had the possibility to submit posters and give short presentations on their research topic. This was followed by a best poster award. - Poster sessions raised sufficient interest in students. - Presentations lasted for 10 minutes each, in a dedicated 90 minutes session. ECTS: Frédéric Blanqui raised the question of awarding credits at ISR. Aart Middeldorp, Hans Zantema and Georg Moser indicated that this may be useful to students, in particular, to demonstrate mobility. Frédéric Blanqui inquired whether an exam has to held in order to award credits. Georg Moser mentioned that this depends on the country. Hans Zantema remarked that credits should not be awarded lightly. Invitation of Lecturers: The organisers of the school are in the process of contacting lecturers, but there is also the possibility to have an open call. The list of topics is still unclear and depends on the lecturers, but there is emphasis on attracting lecturers on new topics. The IFIP group voiced their favour of having an open call. Attracting Participants: Hans Zantema raised the issue of attracting sufficient number of participants. At ISR 2017, participation was partly sponsored by a national funding body, which had a significant impact on participation numbers. It was conceived however that parts of the supported students were not genuinely interested in the topics taught at the school. Frédéric Blanqui mentioned that since ISR 2019 is held in Paris, participant numbers may be less of a problem. In this context, it was discussed whether the scope of the school should be broadened (e.g. by having lambda-calculus or higher-order rewriting in the basic track) but this discussion was inconclusive. Duration: Frédéric Blanqui asked the IFIP group about their opinion of having an additional day of lecture. Femke van Raamsdonk and Hans Zantema voiced their opinion that 5 days of material is enough, rather, they suggest a more extensive mixture of practice and theory courses. Also, more exercise lectures were suggested, as these were well received at ISR 2017. ISR 2020: Frédéric Blanqui presented the proposal for ISR 2020 at UCM, Madrid, Spain, on behalf of Narciso Martí Oliet. It is suggested by the IFIP group that an overlap with the Olympic games is avoided. Proposal period: Frédéric Blanqui proposed to shorten the proposal period for summer schools. The group is against shortening of this period. 4) Informal report on FSCD by Helene Kirchner and Discussion on Reviewing Culture in TCS Report: Helene Kirchner reported on FSCD 2018. The number of submissions are decreasing. The interaction with LIPIcs was smooth. Jean-Pierre Jouannaud raised his opinion that in order to be considered for the best paper award, the ratio of senior to junior authors should be less than 1/2. It was furthermore voiced that in parts, readability of FSCD accepted papers requires improvement and that the page limit may be increased. Reviewing Culture in TCS: Georg Moser reviewed the discussion on reviewing culture in TCS from the groups mailing list. Several additional options, such as non-anonymous reviews and reviews solely from the PC were discussed. It was noted that IFIP has no force but may provide suggestions to the FSCD committee. Change of publication model: Helene Kirchner presented a new proposal concerning the publication model of FSCD, suggesting (i) more refined categories, (ii) the submission of extended abstracts (5-6 pages) plus reference to Archive giving technical details, and (iii) the possibility of having then a special issue in a journal, e.g. LMCS. Georg Moser noted the risk of further declining submission numbers to FSCD. Delia Kesner pointed out that the success of TYPES, which follows a similar publication model based on post-proceedings. Delia Kesner suggested to experiment the publication model on a new workshop/conference, to alleviate risks for FSCD. Beniamino Accatolli suggests an alternative two phase submission, with introduction and full submission with the purpose of improving readability of introductions. It is decided that the group will work out a concrete proposal and submit it for consideration to the FSCD SC. 5) Discussion on IFIP and Business Meeting Organisation of meetings: Several options for organising future annual meetings of this IFIP WG were discussed: (i) as a standalone event; (ii) co-allocated with ISR; and (iii) co-allocated with a conference related to the interest of the WG. It was decided on (iii). Lack of Visibility: Raised by Maribel Fernández, the WG acknowledges its lack of visibility. Online material is out-dated or non-existing. It is also noted by Femke van Raamsdonk that the RTA/FSCD community is conceived as too closed from the outside. There was consensus that the WG should attract researchers from outside the field that apply rewriting technology. This could be done in the context of an annual meeting with invited talks solely dedicated to applications, or to a special event possibly co-allocated with a conference from application domains. Jean-Pierre Jouannaud proposes a Book on application, approaching external contributors. As a lightweight alternative, Delia Kesner proposes a special issue on applications. RTA list of open problems: It has been decided that the IFIP WG starts maintaining a list of open problems. As the RTA list is outdated, the new list of open problems will not be based on the RTA list, but reference it. IFIP web-page: It has been decided that the IFIP WG webpage receives its own domain. ISR 2020: The proposal for ISR 2020 at UCM in Madrid, Spain has been accepted. Membership: It has been decided to lower the number of invitations necessary to vote on membership to the IFIP WG from two to one. Georg Moser will update the by-laws accordingly.