From the very start of my thesis, the key idea was to find a lambda calculus with explicit substitutions, indexes, and all the good properties (I refer the reader to all previous posts). In particular, having in mind a recent work from Delia Kesner: A Theory of Explicit Substitutions with Safe and Full Composition (well, to be honest, it was a previous one, but the ideas are the same). In this work, Kesner combines two concepts:Composition of Substitutions and Garbage Collection (GC). I will briefly explain these two concepts in the following sections, and conclude with some of the problem I have found trying to join these concepts with an indexed calculus.
But first, let's review what a substitution is: given two terms t and u, a variable x, the effect of substituting all the free occurrence of x in t by u is written as
t[x / u]
which, informally, is like a find and replace of x by u.
Composition of Substitutions
When having two substitutions, like in the term t[x/u][y/w], some calculus, instead of make first the inner substitution and then the outer, they compose the substitutions by joining both compositions. This is necessary to achieve metaconfluence. There are two ways for doing this:
- By using a list of substitutions: substitutions are a list [x/u, y/w, ...]
- By combining the substitutions: rules like t[x/u][y/w] →t[y/w][x/u[y/w]] (under certain conditions) are added to the calculus.
Kesner uses the second way of composing substitutions. If no restriction is made to the rules used to compose substitutions, then it's easy to loose the property Preservation of Strong Normalization. That's when the concept of Garbage Collection came to save the day.
Garbage Collection
GC needs not to be confused with the usual programming concept of Garbage Collection (remember: in lambda calculus there's not such a thing as a "memory"). The idea behind this concept is simple: throw away those substitutions that have no use, i.e. do not perform any substitution, i.e. do not change the term. In particular, in the term t[x/u], if x is not free (for instance, it does not appear) in t, then there is not going to be a replacement; therefore, t is going to remain unchanged. In that case, we said that the substitution [x / u] is garbage, and we throw it away.
When composing "garbage", one can lose the property of Preservation of Strong Normalization. By combining these two concepts, Kesner achieve a compact calculus with all the good properties. I have studied a way to perform GC in a calculus with indexes and substitutions as lists, called lambda sigma. This was particularly difficult for two reasons:
- When having a list of substitutions, all the variables in the list need to be checked.
- When having indexes, the substitution is in charge of both substituting and index updating, so we need to be careful to whose substitutions we consider garbage.
After obtaining the definition of garbage for lambda sigma, the next step was to define a calculus that does garbage collection, and proof all the basic properties for it (strong normalization of the substitution calculus, confluence, simulation). Working with an indexed calculus requires a lot of calculations, and that's how I spent a few months writing the demonstrations for all of the proofs.
The last part of the work was dedicated to think about the other properties: Confluence on Open Terms and Preservation of Strong Normalization. The first one was easily proved to not hold, but there might exist an extension to the calculus that do, but under certain conditions. For Preservation of Strong Normalization, I have proved that this calculus is "better" than the original lambda sigma, but it's an open question whether or not it has this property. As a matter of fact, until the last moment of the presentation of the thesis, I think I have a counterexample, but it turn out that the proof was ill-formed. That's why it's open, and if you ask me, I think it's very difficult to say if this property holds. Certainly, the proof (positive or negative) has to be very difficult.
Well, that's it. Now, with the invaluable help of Manas, I'm graduated, and expecting to work in my PhD at the Max Planck Institute for Software System (MPI-SWS) at Saarbruecken, Germany on January 2010.
This whole experience has been great, and I haven't enough word to thank all of the people here at Manas.
You can check-out a presentation I've perform at the MPI-SWS: Download.
Also, you might like to see my master thesis (it's in Spanish).
For any of this stuff you can ask for the Latex source. Just write me at beta the-symbol-for-at ziliani dot com dot ar.