---------------------------------------------------------------------- IFIP Working Group 1.6 on Term Rewriting Report of the annual meeting: June 2, 2011 (Novi Sad, Serbia) Chair: Juergen Giesl Secretary: Peter Schneider-Kamp 13 Participants: Takahito Aoto (for Yoshihito Toyama) Santiago Escobar (for Salvador Lucas) Juergen Giesl Bernhard Gramlich Pierre Lescanne Aart Middeldorp Georg Moser Kristoffer Rose (invited) Masahiko Sakai (invited) Manfred Schmidt-Schauss Aaron Stump (invited) Johannes Waldmann Hans Zantema ---------------------------------------------------------------------- Agenda: 1. Technical Presentations 2. International School on Rewriting (ISR) 3. Business Meeting ---------------------------------------------------------------------- 1. Technical presentations * Kristoffer Rose: Implementation Tricks That Make CRSX Tick In this presentation I will walk through the implementation tricks used in the CRSX (http://crsx.sourceforge.net) implementation of higher-order rewriting to make rewriting work fast for rules that specify compilers with symbol tables and syntax-directed rewrite schemes using higher-order facilities, such as substitution for inlining and templates, and direct manipulation of scopes and registers as first-class values. The tricks include (1) The role of sorts with linearity. (2) Bound variable reuse. (3) Weakness markers. (4) Using forcer rules to avoid duplication of work. (5) Parallellism in rewriting. (6) Completion for almost-orthogonal pattern compilation. I will also show how (some of) these tricks show up in generated C code for rules. * Manfred Schmidt-Schauss: Unification, Matching, and Rewriting of Compressed Terms An overview of the recent developments in efficient algorithms on grammar-compressed terms is given. This comprises: first-order unification, first-order matching using singleton tree grammars (STGs); an extension of congruence closure for efficiently solving the word problem of STG-compressed terms w.r.t. a set of compressed ground term equations; and efficient variants of term rewriting under STG-compression. * Masahiko Sakai: CNFs with Elementary Symmetric Clauses and Their SAT Solving We introduces clauses, called ESk-clauses or simply ES-clauses, defined based on elementary symmetric functions that return true if and only if exactly k inputs are true. By summarizing some (OR-)clauses in CNF with the equivalent ES-clause, we often obtain a shorter representation. In this talk, we present an idea that incorporates the extension into a two-literal-watching based practical solver, like Minisat, and give some experimental results. We employed a hybrid one that deals with OR-clauses by a two-literal-watching method and with ES-clauses by a full-watching method. We implemented this hybrid mechanism into Minisat, and the experiments show that this works nicely. * Hans Zantema: Triangulation Let ->_1 and ->_2 be terminating relations on a finite set satisfying (1) every element has at most one incoming ->_1 arrow, and (2) if a ->_2 b then there exists a c with c -> a and c -> b. Here -> denotes the union of ->_1 and ->_2. Then -> is terminating. In this presentation this property will be proved, and some extensions to infinite sets will be discussed. In particular, we will sketch a proof that triangulation preserves termination of codeterministic relations. Here codeterministic means the above mentioned property (1), and triangulation is a simplified version of completion: where in completion for a pattern a <- o -> b the normal forms of a and b are ordered with respect to some well-founded order, in triangulation the elements a and b are ordered themselves. This is joint work with Vincent van Oostrom. * Johannes Waldmann: How 1000 people produced 3786 relative termination problems in 72 hours The yearly ICFP programming contest was run by HTWK Leipzig in 2010, and the topic was (unsurprisingly) "relative termination of string rewriting by matrices". Of course it wasn't that obvious to the participants, as we added two levels of severe obfuscation. But once these entry barriers were cracked, participants had to solve and pose termination problems. A subset of those problems created by contest participants had been used in the 2010 Termination Competition, and it proved to be quite hard for current termination tools. We report on interesting observations that could lead to new insights in how to find matrix interpretations, and how to construct hard termination problems. We also discuss an open problem on matrix interpretations and linear derivational complexity. http://www2010.icfpcontest.org/ * Aaron Stump: Harnessing the Power of Term Rewriting Theory for New Applications Over many years, term rewriting has developed a very deep body of theoretical work on topics like termination and confluence. More recently, this work has been complemented by highly sophisticated tools, such as termination checkers and confluence checkers, implementing that theory. In this talk, I consider some new applications for both the theory and the tools, in analysis of type systems and in parsing. I will present preliminary results extending our RTA '11 paper "Type Preservation as a Confluence Problem" to more advanced type systems, in particular, Curry-style System F (also known as lambda-2). I will also sketch ideas on applying termination and confluence checkers to parsing. * Bernhard Gramlich: On (Un)Soundness of Unraveling Deterministic Conditional Rewrite Systems We study (un)soundness of transformations of conditional term rewriting systems (CTRSs) into unconditional term rewriting systems (TRSs). From a logical as well as operational point of view soundness and completeness of such transformations are indispensable. The focus here is on analyzing (un)soundness of so-called unravelings, the most basic and natural class of such transformations. We extend our previous analysis from normal 1-CTRSs to the more general class of deterministic CTRSs (DCTRSs) where extra variables in right-hand sides are allowed to a certain extent. We sketch how our previous soundness results based on weak left-linearity and on right-linearity can indeed be extended from normal 1-CTRSs to DCTRSs. Counterexamples show that such an extension to DCTRSs does not work for the previous criteria which were based on confluence and on non-erasingness, not even for right-stable systems. Yet, we prove a weaker soundness result for confluent right-stable CTRSs, namely soundness w.r.t. reduction to normal form. Finally we compare our approach and results with related ones, especially with [Nishida et al./RTA'11]. (Joint work with Karl Gmeiner and Felix Schernhammer) * Aart Middeldorp: Confluence Competition 2012 In this talk I outline ideas for an upcoming confluence competition. ---------------------------------------------------------------------- 2. International School on Rewriting (ISR) * Santiago Escobar: Report on ISR 2012 - ISR will take place on July 16-20, 2012 in Valencia. - There will again be two tracks (one for newcomers and an advanced one focusing on more recent developments). - ISR will honor Alan Turing in his Centennial Year. - A detailed schedule can be found on the web. - ISR will take place in the university of Valencia, with good connections to the city center and the airport. - Valencia has good airline connections that make it easy to reach from almost every location. - Accomodation will be provided in university residences. - The estimated amount needed to fund the lecturers is 6000 Euro. - The estimated registration fees will be 500 Euro for students with single room accomodation, 428 Euro for students with double room accomodation, 600 Euro for non-students with single room accomodation, and 528 Euro for non-students with double room accomodation. * Comments from the audience: - Will there be ECTS certificates for the courses? (J. Waldmann) - Will there be exams for the basic track? (H. Zantema) - It should be encouraged that lecturers stay for the whole week, not just for the days of their course. (A. Middeldorp) - It would be good to split lectures so that they take place on several days. (J. Waldmann) - Will the courses include homework exercises? (J. Giesl) - Will the students receive printouts of the slides? (A. Middeldorp) - It would be good to distribute posters to advertise the school. (G. Moser) * Aart Middeldorp: Report of the Chair of the ISR Steering Committee - The report on ISR 2010 was already given at the last meeting; no further report on ISR 2010 will be provided. - In 2013, a report on ISR 2012 is expected. - The next ISR after the one in 2012 is scheduled for 2014. A call for proposals will be issued before spring 2012. - It would be desirable to find a location outside of Europe. - A repository of information should be created for future organizers of ISR (containing slides of lectures, information on the budget, lists of participants, etc.) - It would be desirable to make the slides of lectures available online (after the school). They could be hosted on the website of the IFIP-WG and there could be a link from the rewriting homepage to that site. - Every WG member should send at least one student to the school. ---------------------------------------------------------------------- 3. Business meeting - There was consensus that the next IFIP WG 1.6 meeting should take place together with the next RTA in Nagoya (Japan). - Membership issues were discussed and Kristoffer Rose was invited as a new member to the WG after having been invited to the meetings in 2010 and 2011. - Since the term of Juergen Giesl as the chair of the WG ends this autumn, there will be an election of the chair, organized by the secretary of the WG. - There was agreement that non-members of the WG should be allowed to attend the meeting of the WG, except for the business meeting. - Several suggestions were made for the program of future WG meetings: * The meeting could be shortened to half a day. * There should be less technical talks and more discussions (probably panel discussions) and/or position statements. * Before the meeting, there could be a call for discussion topics. ----------------------------------------------------------------------