---------------------------------------------------------------------- IFIP Working Group 1.6 on Term Rewriting Report of the annual meeting: June 26, 2016 (Porto, Portugal) Chair: Georg Moser Secretary: Ugo Dal Lago ---------------------------------------------------------------------- PARTICIPANTS Takahito Aoto Mauricio Ayala-Rincón Gilles Dowek Santiago Escobar (for Salvador Lucas) Maribel Fernández Jürgen Giesl Delia Kesner Claude Kirchner Hélène Kirchner Aart Middeldorp Georg Moser Brigitte Pientka Masahiko Sakai René Thiemann (for Vincent van Oostrom) Ashish Tiwari Yoshihito Toyama Johannes Waldmann ---------------------------------------------------------------------- AGENDA 1) Presentation by Ashish Tiwari (invited) 2) Presentation by Brigitte Pientka (invited) 3) International School on Rewriting (ISR) 4) Discussion: ISR as an IFIP event 5) Presentation by Mauricio Ayala-Rincón 6) Assessment of FSCD 7) Discussion: Future of IFIP 8) Business Meeting ---------------------------------------------------------------------- 1) Presentation by Ashish Tiwari. Title: One context unification problems solvable in polynomial time Abstract: One context unification extends first-order unification by introducing a single context variable, possibly with multiple occurrences. One context unification is known to be in NP, but it is not known to be solvable in polynomial time. In this talk, we present a polynomial time algorithm for certain interesting classes of the one context unification problem. Our algorithm is presented as an inference system that non-trivially extends the usual inference rules for first-order unification. The algorithm is of independent value as it can be used, with slight modifications, to solve other problems, such as the first-order unification problem that tolerates one clash. 2) Presentation by Brigitte Pientka. Title: Programming Coinductive Proofs Using Observations Abstract: Coinduction is a key proof technique to establish properties about systems that continue to run and produce results (i.e. network or communications protocols, I/O interaction, data streams, or processes) . Yet, mechanising coinductive proofs about formal systems and representing, generating and manipulating such proofs remains challenging. In this talk, we develop the idea of programming coinductive proofs dual to the idea of programming inductive proofs. Unlike properties about finite data which can be defined by constructing a derivation, properties about infinite data can be described by the possible observations we can make. Dual to pattern matching, a tool for analysing finite data, we develop the concept of copattern matching, which allows us to describe properties about infinite data. This leads to a symmetric proof language where pattern matching on finite and infinite data can be mixed. This is joint work with Andreas Abel, Andrew Cave, David Thibodeau, Anton Setzer. 3) International School on Rewriting - Waldmann reported on ISR 2015. ISR'15 was held on August 10-14, 2015 in Leipzig, Germany. Main organiser was Waldmann. The school had a basic and advanced track. New elements were the call for lecturers, student posters and student evaluations. Further details on ISR'15 can be found at the website: http://nfa.imn.htwk-leipzig.de/ISR2015/. Report on ISR led to an lively discussion on potential improvement of the summer school. Brigitte Pientka reported on the Oregon Programming Language Summer School. Furthermore related experiences will student posters were discussed. Moreover there was discussion on extending the scope of ISR, for example towards programming languages. Discussed potential changes: In order to adapt and broaden the topics of ISR a call for topics could be issued. Furthermore lectures could be taped and made accessible online. - Waldmann reported on (aborted) plans for ISR 2016. Gerwin Klein had proposed to host ISR in 2016 in Sydney. Gabrielle Keller should have been organiser. Due to budget cuts and a competing summer school, the plan was abandoned. - Waldmann reported on ISR 2017 in Eindhoven (as replacement for ISR 2016). Femke van Raamsdonk and Hans Zantema agreed to organise the school, which will take place from July 3-7, 2017. The school will have a basic and advanced track. - Waldmann presented the proposal of Camilo Rocha to host ISR 2018 (tentatively) from July 23-27, 2018 at the Universidad del Valle in Cali, Colombia. Delia Kesner asked whether it is likely that local students will attend. It was agreed that an ISR in Colombia would be attractive to students in South America. Brigitte Pientka asked about security and health situation. In discussion it was clarified that the security risk could be contained. The slides of the proposal are attached. Please be aware that the date of the school may change. - Vote on Proposal for ISR 2018: unanimously in favour. Thus ISR 2018 will take place in Cali, Colombia. 4) Discussion: ISR as an IFIP event - Georg Moser reported on the possibility to make ISR an official IFIP event, which would give limited funding to students from developing countries as well as support lectures for an ISR hosted in an developing country (like Colombia). Developing countries are defined according to UN classifications, see https://en.wikipedia.org/wiki/Developing_country. Pros and Cons where discussed without clear outcome. Making ISR an official IFIP event requires an application to be synchronised between WG chair and OC of ISR. Furthermore IFIP demands a fee from official events. Moreover, only limited support can be anticipated. On the other hand this would allow us to use official IFIP channels for announcements, which could increase the visibility of the summer school. It was agreed to contact the organisation chair of ISR 2018 on this and provide support if necessary. 5) Presentation by Mauricio Ayala-Rincón Title: Formalisation of Confluence 6) Assessment of FSCD - Delia Kesner and Brigitte Pientka recapitulated the status of FSCD as successor of RTA and TLCA. According to their estimate 13 RTA related topics, 13 TLCA related topics and 4 papers in new directions where published at FSCD. Two papers were considered as in the intersection between RTA and TLCA. It is commonly agreed upon that less papers on first-order automated reasoning have been submitted. Thus this area has receive less attention than in last years. On the other hand FSCD appears to be on the right track and was conceived a success by the WG. Further broadening of the scope should be envisioned. 7) Discussion: Future of IFIP - Georg Moser reported briefly on the related discussion in 2015 and the need to precise the aims of the WG in the context of FSCD due to requests from IFIP. Claude Kirchner argued that the current aims of the WG are precisely in the scope of FSCD. Everybody concured to this analysis. However, it was felt that the name of the WG is no longer adequate to the research interests of its members. It could be simplified to "Rewriting", if the members agree. This will be subject to an electronic vote. Should this vote be in favour, this change of name would require the submission of a corresponding statement to Jacques Sakarovitch, the chair of TC1. It seems that such a name change could be quickly adopted. - The WG has been invited to take part in IFIP conferences, for example, the WG could be affiliated to the IFIP World Computer Congress 2018 (see the attached project description). For now co-location with FSCD, IJCAR, FLOC is preferred. - A common domain for IFIP is discussed, for example ifip.1.6.org, so that the domain of the website does not change so frequently. The WG chair is instructed to investigate. 8) Business Meeting - Memberships, Selection of Invitees. Ashish Tiwari has been invited twice and is made member by unanimously vote. Pierre Lescanne is made honorary member by unanimously vote. Nobody is leaving the WG in this year. - RTALoop. Georg Moser reports on the current status of a restructuring of the list of open problems. The restructuring is headed by Nachum Dershowitz in joint work with Eduardo Bonelli, Jörg Endrullis and Jakob Grue Simonsen. The important new part would be a wiki-like structure which should simplify problem submission. - The possibility to have a dedicated domain for the website of the WG, also in connection with the rewriting home page, was discussed. A proposal was the domain ifip.1.6.org. The WG chair was instructed to investigate possible costs. - Vote on Location. Co-location with CADE or FSCD is discussed. The vote for FSCD is unanimously. Thus, the next annual meeting will be co-located with FSCD, 2017 in Oxford.