Luis Ziliani, a.k.a. Beta

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.

In all previous posts I've tried to teach the different aspects inside my thesis. But after going deeper and deeper, the concepts tend to complicate too much, and much more dedication from the reader is needed. After trying to add another technical post, full of strange symbols, I quit the idea. And then someone point me out that it would be best if I just talk about what kind of problems I dealt by making my thesis. That's what I will do from now on.

First, I will give a brief look at the story.

It's the first semester of 2007, I choose three different subjects: Topics of Rewritings, Theory of Models, and Introduction to the Processing of Digital Images. Those of you who know informatics will notice that the choice is quite weird: two of the subjects are purely theoretical, and the last one is purely practical. That was my idea, see which fields of the informatics fit me best. You already know the answer.

The winter holidays of 2007 ended in this southern part of the world. As I was in the last part of the career, I decided to continue my studies in rewritings, so I chose to get into the course "Rewritings, Lambda Calculus, and Explicit Substitutions". At the same moment, I talked to Alejandro Ríos to be his master's student. He accepted. But I needed to end the courses and pass the exams, so I really begun the work at the beginning of 2008.

Then, something very uncommon happened. Since 2004 I worked in Manas. But I decided that in 2008 I would put all my effort in finishing my career. The idea was to get a grant from the university, and with a few savings and my salary as teaching assistant at the university, try to survive without another job. When I was about to quit my job at Manas, my boss told me "What if we sponsor your thesis?". So that's how I end up doing my thesis in Manas.

In the next post I will talk what I've tried to do since I started.