---------------------------------------------------------------------- IFIP Working Group 1.6 on Term Rewriting Report of the annual meeting: June 28, 2015 (Warsaw, Poland) Chair: Georg Moser Secretary: Ugo Dal Lago ---------------------------------------------------------------------- PROGRAM 09:15 - 10:00 Talk by Takahito Aoto (invited) 10:00 - 10:30 Coffee Break 10:30 - 11:15 Talk by Gilles Dowek (invited) 11:15 - 12:00 Talk by Stéphane Graham-Lengrand (invited) 12:00 - 12:30 Discussion on ISR (discussion chair: Aart Middeldorp) - Report on ISR'15 (Johannes Waldmann) - Report on ISR'16 (to be confirmed) - Report/Propsals for ISR'17 (Mauricio Ayala-Rincón) 12:30 - 14:00 Lunch 14:00 - 14:45 Talk by Luke Ong (invited) 14:45 - 15:15 Discussion onthe future of IFIP WG 1.6 (discussion chair: Ugo Dal Lago) - Modernisation of aims - Stand-alone events 15:15 - 16:00 Coffee Break 16:00 - 16:30 Proposal for a Joint Conference RTA/TLCA (Kris Rose) 16:30 - 17:15 Discussion on the Future of RTA/TLCA (discussion chair: Georg Moser) - FSCD Proposal 17:15 - 18:00 Business Meeting PARTICIPANTS Mauricio Ayala-Rincón Takahito Aoto Franz Baader Ugo Dal Lago Gilles Dowek Maribel Fernández Jürgen Giesl Stéphane Graham-Lengrand Giulio Guerrieri Nao Hirokawa Tetsua Ida Jianqi Li Helene Kirchner Aart Middeldorp Georg Moser Luke Ong Simona Ronchi della Rocca Kristoffer Rose Manfred Schmidt-Schauss Yoshihito Toyama Pawel Urzyczyn Femke van Raamsdonk Johannes Waldmann Hans Zantema ---------------------------------------------------------------------- 9.15 - 10.00 - Takahito Aoto (Joint work with Yoshihito Toyama). Proving Ground Confluence of TRSs by Rewriting Induction with Non-Orientable Equations. ABSTRACT: Ground confluence of term rewriting systems guarantees that all ground terms are confluent. Not confluence but ground confluence often matters in applications where not the equational validity but the inductive validity is of concern. Recently, interests for proving confluence of term rewriting systems automatically have been grown, and confluence provers have been developed. In contrast, it seems that little interests have been paid on developing tools for proving ground confluence automatically. In this talk, present a theoretically simple approach for proving ground confluence of term rewriting systems based on rewriting induction with non-orientable equations, and report on development of a ground confluence prover. QUESTIONS: - Rose asked for ground confluence for higher-order terms. Aoto replied saying that confluence in the higher-order case is usually taken to be ground confluence. - Kirchner asked whether the ordering assumption can be avoided. Aoto replied that in this case the problem would become too complex. Kirchner pointed to rewriting with constraints, and Aoto pointed out that it would indeed be interesting. - Hirokawa pointed to non-orientable equalities, and asked whether AC actions could be expressed. Aoto replied that indeed it can be represented. Hirokawa also made a comment about bounded compatibility and possible adaptation of the Aoto's framework to that. ---------------------------------------------------------------------- 10.00 - 10.30 - Coffee Break ---------------------------------------------------------------------- 10.30 - 11.15 - Gilles Dowek. Polarisation and Reachability. ABSTRACT: Polarised sequent calculus modulo theory led us to introduce polarised rewrite systems, where rules are classified into two categories: negative and positive. I will defend in this talk that this notion of polarised rewrite system is interesting in itself. As an example, I will present a method developed jointly with Guillaume Burel and Ying Jiang to decide reachability in various rewrite systems. QUESTIONS: - Rose pointed to compilers as TRS, and failure. Dowek said that he is interested, but that he does not know much about it. - Waldmann pointed to string rewriting as a way to read the presented results in the realm of string rewriting. Dowek said he will think about it. - Ayala-Rincón asked about whether complexity results can be inferred from all this. Dowek said that it would be difficult, because the complexity of the Knuth-Bendix methodology is hard to analyse. - Moser asked about the motivations for studying pushdown systems. Dowek said that decidability of CTL can be reduced to decidability of reachability in alternating pushdown systems. ---------------------------------------------------------------------- 11.15 - 12.00 - Stéphane Graham-Lengrand. Non-idempotent Intersection Types and Quantitative Information about Reduction Paths: A Survey ABSTRACT: Over the recent years, a new area in the study of intersection types has been explored. In the original spirit of intersection types, a term is of type A /\ B if it is both of type A and of type B, which naturally leads to an idempotent view of intersections: A /\ A is the same type as A. Dropping this idempotency property of intersections allows the design of resource-aware type systems, with deep connections to linear logic. This enriches typing with quantitative information about the lengths of reduction paths from typed terms. Upper bounds for these lengths -or even sometimes exact characterisations- have been provided by such typing systems, for various abstract machines and reduction strategies in the lambda-calculus and some of its variants. Among these, explicit substitution calculi proved a particularly appropriate approach to establishing such results. We will review this line of research, where typing is brought much closer to operational and denotational semantics, and discuss the connections that it opened towards neighbouring areas. QUESTIONS: - Ong asked whether any of the presented result carry over to results about resource analysis. Graham-Lengrand replied that they have not done anything, but that Ronchi Della Rocca and De Benedetti have some results in this direction, related to the resource lambda-calculus. - Waldmann asked a technical question, and Graham-Lengrand replied exhaustively. - Rose asked whether there is any context in which intersection types have a competitive advantage over existing methodologies. Graham-Lengrand replied that one reason why intersection types are useful is that by using them you can prove normalisation theorems (for, e.g. System F) without the need to refer to reducibility candidates. - Moser asked about characterising complexity classes by intersection types, and Graham-Lengrand replied that they have not, and that he is quite sceptical about that. - Moser asked about relations between linear logic, and annotated versions of it, and non-idempotent intersection types. Graham-Lengrand replied that this is indeed a topic that deserves to be investigated, and that he is optimistic about it. ---------------------------------------------------------------------- 12.00 - 12.30 - Discussion on ISR - Waldmann gave some data about ISR 2015, which will take place in Leipzig on August 2015 (see attached slides). * Rose asked about CADE association. Waldmann said that ISR will just be an affiliated event, with a link to ISR in CADE's website. - Ayala-Rincón presented some basic data about ISR 2016, which will be in Sydney, Australia (see attached slides). * Zantema was worried about the number of students, which could be quite low due to the relative remote location. Ayala-Rincón said that it is quite important that this event is officially recognised by the local University: this way, the event will be sponsored, and eventually we will be able to offer grants. * Dowek added that the SC needs to invite people from abroad, because Australia is far from the rest of the world, and the number of participants could significantly decrease. * Waldmann commented that Australia is after all not that far from Japan. * Middeldorp pointed out that the SC indeed should be very active, and suggested to the Japanese participants to send their students to ISR 2016. - Ayala-Rincón presented a proposal to host ISR 2017 and RDP (or FSCD) 2017 in Montevideo, Uruguay (see attached slides). * Kirchner asked about the dates, which are in July. * Middeldorp asked whether the proposal should be considered as valid only if FSCD is accepted. And Ayala-Rincón said that yes, this is the case. * Dowek asked whether the locals have any experience about co-locating. Ayala-Rincón replied that yes, there was something similar in Brasilia, 2009, and it was very nice. ---------------------------------------------------------------------- 14.00 - 14.45 - Luke Ong. Compositional Higher-Order Model Checking, and the Model Checking of Higher-type Böhm Trees QUESTIONS: - Dowek asked whether there is any relation to the work Zaionc, who proved that in the simply-typed lambda-calculus there is a type for which there is no grammar which generated all the closed normal forms of that type. Ong said that this sounds very closely related. - Rose pointed to continuation-passing-style, another area in which limiting the order is essential. Ong replied that CPS has been used in this context, but all what he said was about call-by-name, and that the CPS-translation is also order-sensitive, and the order can indeed blowup. - Dal Lago asked whether all this can be generalised to probabilistic schemes. Ong replied that his understanding is that if you restrict to probabilistic schemes of order 1, then the results are quite similar. - Graham-Lengrand asked about a semantic framework in which you are able to talk about the properties of Bohm-trees. Ong replied that what the community is interested at is something which is expressive, but retains decidability. An interesting open problem, then, is to have a logic matching Bohm-trees of higher-order type. - Moser asked about automation. Ong replied saying that the problem of designing efficient model checking algorithms is a very intense area of research. ---------------------------------------------------------------------- 14:45 - 15:40 Discussion on the future of IFIP WG 1.6 - Georg Moser recalled the official aims and scope of IFIP WG 1.6. He then asked whether this should be changed, enlarged, or in any way altered. In particular, many important topics, including those of three out of four invited talks to this WG, are not even mentioned. - There has been some discussion about IFIP technical committee. This WG is part of TC1, and Dal Lago will participate to the next meeting of TC1, to be held in Kyoto on July 10th. - Baader said that the role of invited speakers has been over overemphasising: the ISs should not define the scope of the WG. Moser said that he only want to underline this discrepancy. A brief discussion about the policy for inviting speakers at WG followed. - Moser asks whether the WG should continue exactly like it is now, or whether broader aims and scope should be adopted. He proposed to come up with new aims and scope, that will be later subjected to vote. - Middeldorp asked why official aims and scope are important. - Dowek said that it is indeed useful to change the topics from time to time, but of course invited talks reflect the edge of current research. - Urzyczyn asked what is the purpose, the added value, of this WG. Zantema said that ISR is, for example, an initiative of this WG. - Waldmann asked what problem Moser is trying to solve now. He said that what he would like to do is to make the WG broader and more active. - Dowek observed that there are two options: going towards FSCD, or focus on rewriting. - Rose pointed out that there are many rewriting-related activities that WG's members like to do. The question then should be: how do we exploit all this? - Urzyczyn remarked that if the FSCD's proposal is to be accepted, then RTA will dissolve, and WG 1.6 will be the only flagship group/workshop on rewriting. Instead of expanding 1.6, we could create new groups. - Moser said that is is apparently very difficult to create new working groups, and broadening the scope of WG 1.6 would be easier. Baader said this would be a nasty way of sneaking into WG 1.6 topics for which creating a new WG is not possible. - Dowek said that IFIP affiliation is not really necessary. A workshop on rewriting as a satellite workshop of FSCD, for example, would be nice. Moser did not agree: he prefers to have stand-alone meetings, avoiding this way superposition with other events. - Giesl suggested to invite young people, independent from topics? A brief discussion about the topic followed. - Moser said that the vote would be between two choices, as Dowek proposed. Something more detailed about organisation would follow. - Kirchner said that she is convinced that keeping something around rewriting is necessary. Even if, of course, there is a problem about participation. A brief discussion about participation to the WG followed. In particular, Baader suggested we should find ways to force people to come. - Kirchner said she finds it very strange to see how the community has evolved, with many new workshops independent on WG. Graham-Lengrand observed that people organising workshops like WST are (or should be) members of this WG. - Ong reported on his experience on 2.2, whose dedicated workshop he always finds it very exciting. - Waldmann mentioned, again, ISR, which is the only event that this WG is really responsible for. If this WG changes its focus, we should anyway take care of ISR. - Kirchner said that this research community really needs to have workshops. ---------------------------------------------------------------------- 15.40 - 16.00 - Coffee Break ---------------------------------------------------------------------- 16.00 - Proposal for a Joint Conference RTA/TLCA Rose explained the proposal for a new conference that is meant to replace both RTA and TLCA. Main ideas: * The new conference will be called FSCD, for Formal Structures in Computation and Deduction. * The scope will be slightly larger than the ones of RTA and TLCA, combined. * The global number of accepted papers would be smaller than the sums of the ones RTA and TLCA usually accept. * It would start next year. * Proposals for list of topics and bylaws have been made public, but are meant to be open to modifications by the SC. DISCUSSION: - Zantema asked about the name, and Rose said that FSCD is part of the proposal and it is not subject to discussion. A brief discussion about the name followed. - Giesl asked why a smaller number of accepted papers is looked for. Rose replied that acceptance ratio, relatively high in RTA and TLCA, is part of the answer. - Baader asked about the list of topics. He is not so happy with that, because the list does not include important topics for him. Ong said that the list should be as general as possible, with the precise scope decided by the PC, and the SC aiming for a broad scope. Rose said that if something is left out, then it will be covered in the full list that will come later; the list was not meant to be comprehensive, but inclusive. Some open discussion about this topic follows. - Urzyczyn explained the discussion about the list of topic done by the RTA SC and TLCA SC. It is a compromise, which does not take into account the requirements of everybody, but which is anyway inclusive. The actual list will be developed by the PC, each year. - Ong said that list is only meant to be a (rough) definition of what the new conference represents. - Rose said that there is something, from rewriting, that would be left over: awards, ISR, list of open problems. It would be nice if somebody would take care of all this. - van Raamsdonk asked whether people would vote for everything, and Rose replied affirmatively. Urzyczyn then explained the story behind the new proposal: * The starting point was a decline in submission numbers for both RTA and TLCA. * The next observation was that something like RDP would only suffice for five, maybe ten, years. * Then came VSL 2014, in which the general assembly of both RTA and TLCA decided to go for something new, of which the topics from RTA and TLCA would only partly cover the scope. * Developing the proposal took a whole year, from summer 2014 to summer 2015, and the proposal, as described by Rose, consists of a title, a list of topics and some bylaws. * The proposal should be seen as a package, and we are going to vote for the whole of it in the business meeting. If you think that the proposal is bad, just vote against it. This would avoid a possibly long, but arguably not so productive, discussion. DISCUSSION: - Rose observed that both SCs, as well as the two future PC chairs, approved the proposal without any reservation. - van Raamsdonk does not understand why FSCD should flourish immediately, while RDP is dying. Why? - Dowek said that the actual content of the list of topics is not that important, because even the first PC chairs would have the opportunity to change it. Simona Ronchi said that the list of topics is not the most important topic, but that the style in which it is written is crucial. - Giesl said that RTA has two halves: the first one is about rewriting and the lambda-calculus, while the second one is about first-order rewriting and automated deduction. The second half is clearly not represented in the TLCA community, and this is probably the main reason why many people from the rewriting community are feeling uncomfortable with the proposal. Moser observed that automated deduction has never appeared in RTA calls for papers. van Raamsdonk said that the problem is getting people feel included. Pawel highlighted that the same problem is felt on the TLCA side. A brief discussion about the list of topics followed. - Waldmann observed that if the list of topics is not important, then name and bylaws are important, but name has not been discussed. Urzyczyn recalled that bylaws will be reviewed and possibly changed by the SC. - Fernández feels uncomfortable with the list of topics, because something is not present in it, while something else is, indeed present. She argued, then, that not having the list of topics at all would be better. Urzyczyn said that, after all, we are still discussing about the list of topics. - Baader said that he finds Urzyczyn's behaviour quite offensive. - Ayala-Rincón, Rose, and van Raamsdonk then discussed about the rules about appointing the PC chair and OC chair for the next conferences. The idea of the FCSD bylaws is that the PC and OC chairs are selected by the SC slightly less than two years before the actual conference, and voted by the assembly one year before the conference. - Giesl asked why people are listening to all this, if the proposal cannot be discussed and modified. Urzyczyn said that the scenario that the BM votes against the proposal is not so unlikely. Moser said that the RTA SC has been given a mandate to design a proposal, and this is what they, together with the TLCA SC, have been doing in the last year. Dowek said that the kind of democracy used in this process has not been direct, this is the only solution guaranteeing to reach a consensus in a reasonable amount of time; if the goal is important, this is the only way to go. ---------------------------------------------------------------------- 17.20 - Business Meeting PARTICIPANTS: Franz Baader Ugo Dal Lago Jürgen Giesl Maribel Fernández Nao Hirokawa Helene Kirchner Aart Middeldorp Georg Moser Manfred Schmitt-Schauss Hans Zantema Femke van Raamsdonk Kris Rose Johannes Waldmann - Moser proposed to have the next IFIP WG 1.6 meeting in Porto, co-located with RDP/FSCD, namely during June 2016. * Baader observes that having a meeting co-located with a relatively big event could cause problems due to having too many events in parallel. Moser observed that he will try to have the working group in parallel with not-too-many events. Baader said that we could even go to a conference hotel. *Baader proposes to choose the last workshop block to provide a bridge to IJCAR 2016.* * Fernández observed that changing the format of the meeting a bit would probably help, for example by having two evenings rather than a whole day. The proposal of having the next meeting in Porto is finally approved. - Takahito Aoto and Gilles Dowek have presented twice at the WG. Moser suggested to have them as members. Everybody agrees. - Moser suggested to make the following ones honorary members: Deepak Kapur Klaus Madlener Hubert Comon Franz Baader Tobias Nipkow We vote on block and not on the single. Everybody is in favour, except one. - There are two meetings of TC1 this year (London and Kyoto). There could be proxies, not necessarily the chair or the secretary: any member could be involved. The main topics under discussion is the reorganisation of the conference. - Vote on the conditional offer to do ISR 2017 in Montevideo, Uruguay: everybody was in favour. - Vote on moving the responsibility to find an alternative location for ISR 2017 to the IRS SC: everybody was in favour.