RTA 2011 was held in Novi Sad, Serbia, the last week of May, as part of the RDP 2011 federated conference, which brings together RTA and TLCA every two years.   I was not able to attend any of TLCA ’11, though the program looked quite exciting.  RTA was really great, though.  Silvia Ghilezan, who served as the conference chair for both conferences, did an outstanding job in ensuring that the conference logistics ran smoothly and pleasantly, including excursions in the local area.  For me, this was quite interesting, since my family on my wife’s side is Bulgarian, and there are a lot of cultural and linguistic similarities between the two countries (although no doubt people with longer experience would tell me there are many differences, too).  I was able, occasionally, to get somewhere using my baby Bulgarian, although the shuttle driver from the airport warned me that the languages only share about 30% of their words.

Anyhow, back to RTA.  The technical program was quite fascinating for me.  The invited talk by Sophie Tison surveyed results at the intersection of tree-automata theory and term rewriting, including so-called “preservation of recognizability”.  The idea is to study what classes of term-rewriting systems preserve recognizability of a set of terms by a tree-automaton.  That is, if a set T of terms is recognizable by a tree automaton, under what conditions (on the term-rewriting system) is the set of descendants (or alternatively, ancestors) of terms in T is recognizable by a tree automaton.  There is apparently a line of literature on this problem, which Sophie Tison surveyed in her talk, along with several other interesting variations on tree automata (particularly ones with equality and disequality constraints).  Tree automata are studied in the nice book, available online, Tree Automata Techniques and Applications (“TATA”), of which Sophie Tison is a co-author. This would make a nice topic for a CLC seminar…

I really enjoyed many talks in the program, and this post will go on forever if I transcribe my 10 pages of notes.  Let me just hit a couple exciting highlights.  Fer-Jan de Vries gave a very interesting talk related to confluence of infinitary lambda calculus.  The best thing for me about this talk was that it included a reminder of the basic fact (unknown to me before this) that infinitary lambda calculus is not convergent, under at least some notion of infinitary reduction (there are several, and they involve defining a notion of limit of an infinite reduction sequence).  A counterexample is the term $\Omega^I$, defined as follows:

• $I = \lambda x . x$
• $\Omega^I = I\ ((\lambda x. I\ (x\ x))\ (\lambda x. I\ (x\ x)))$
• $\Omega = ((\lambda x. x\ x)\ (\lambda x. x\ x))$

We have $\Omega^I$ reducing (finitarily, and also in the limit, apparently) to $\Omega$.  But we also have

$\Omega^I\ \rightarrow\ I\ \Omega^I\ \rightarrow\ I\ (I\ \Omega^I)\ \rightarrow \cdots$

The limit of this sequence is an infinitary term $I\ (I\ (I\ \cdots))$.  And that term is not joinable with $\Omega$.  Pretty weird!  Just another example of how infinity tends to defy our finitary intuitions.

There was an amazing tool talk about Anagopos, a visualization tool for lambda calculus and term rewriting reductions.  This tool can draw pretty mind-blowingly cool graphs representing reductions of lambda-calculus terms, and related things.  The two Danish (I believe) Master’s students who presented this did a fine job, both with the tool and the talk.

Ok, I guess I am transcribing my notes a bit.  There was a lot of very interesting material.  René Thiemann had some very interesting things to say about the Termination Competition.  One example: in every competition since 2004, including the 2011 edition, there have been tools producing wrong answers.   Now, the good news is that the Termination Competition has a certified division, where tools produce proofs which are then checked by certifiers based on proof assistants like Coq.  This means they get a rather high degree of confidence that results are correct, at least for this division.  René noted later that the CETA certifier has a fully verified parser — this is an interesting point, since I have read not that long ago that tools like the Compcert verified C (subset) compiler lack this, and it is actually a source of bugs for Compcert (where the rest of the compiler, which has been proven sound in Coq, is bug free).  This was discussed in the fantastic paper, which I saw referenced on Lambda the Ultimate, by John Regehr et al. entitled “Finding and Understanding Bugs in C Compilers”.  Since I saw this through LtU, I did not want to post about it independently, but man that is a great paper.  Everyone interested in compilers and verification should definitely read it.

A few quick other things, as I need to wrap this up.  I had many great conversations with very interesting people, including Georg Moser, a proof-theorist who is working now in automated complexity analysis for term-rewriting systems.  He had a very impressive paper showing that the dependency-pair framework for showing termination of term-rewriting systems gives essentially the mutliply recursive functions, which are (apparently) those derivable using only primitive recursions at type of order 1 (I always get confused about whether orders of types start at 0 or 1 — this is the type $\textit{nat}\rightarrow\textit{nat}$).  I also had a very nice conversation with Nao Hirokawa, whose clever ideas and excellent research agenda very much impressed me.  Nao is also a co-organizer of the recently announced Confluence Competition (CoCo), which will run for the first time in 2012.  I am talking with Nao about his possibly visiting me at The University of Iowa this fall sometime, which would be fun and really great for our group.  Ashish Tiwari gave a great invited talk about applications of term-rewriting to systems biology, and other topics.  This was also a really impressive talk, as Ashish summarized a bunch of very strong work with interesting applications.  Stephanie Weirich, with whom I collaborate, along with Tim Sheard, on the Trellys project, gave the sole shared invited talk between RTA and TLCA — quite an honor.  She gave a great talk, which sparked a lot of interesting conversations with people like Andreas Abel, Thorsten Altenkirch, and Peter Dybjer, all of whom I got to speak with later that day.

In the end, I emerged convinced that RTA is a gem of a conference, with a pleasant and very serious core community, which is also quite welcoming to relative newcomers (such as myself).  The acceptance rate is higher than they’d like (around 55% for this edition), which is not necessarily a bad thing if you are an aspiring author.  The next edition, RTA ’12, will be in Nagoya, Japan.  I also heard from several people that they were interested in possibly coming to the US for a later edition.  I am seriously considering proposing Iowa City, Iowa, for the next available RTA, which looks to be RTA 2015 (as 2013 is in Eindhoven, and 2014 will be with FLoC).  That would be an RDP year, so if I did propose this, and the proposal were accepted, that would bring RTA and TLCA to The University of Iowa, which would be super cool for us, and probably also for many researchers interested in types (for TLCA) and rewriting in North America.