Luis Ziliani

The long and winding road… to a master thesis

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.

Making a thesis

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.

Different properties one can expect from any λ-calculus

In this post I will show two different sets of properties that any variation of λ-calculus with explicit substitutions may or must have.

The must:

1) Any substitution must end, i. e. the process of change a variable by a term must always end, no matter how you do it. Put it in another way, the calculus without the β rule must have Strong Normalization (basically, you always end up with a solution).

2) The calculus must be confluent. No matter which rules you apply, or in which order, you always find the same result.

3) Simulation of the traditional λ-calculus: There must be nothing you can do with the original λ-calculus that you can’t do with the new calculus.

The nice to have:

1) Confluence on open terms. Basically, the idea is to see if confluence still holds if you extends your calculus with meta-variables. Meta-variables acts like holes in your formula, something you can’t control. For instance, in the λx calculus shown in the previous post, this property doesn’t hold. There is no way to close (converge) this divergent steps:

1. ((λx.t) u)[y/v] → t[x/u][y/v]

2. ((λx.t) u)[y/v] → (λx.t)[y/v] u[y/v] → (λx.t[y/v]) u[y/v] → t[y/v][x/u[y/v]

If you asume that t is a classic term from the calculus, then you can find the same solution. But if it’s just a hole, there’s nothing you can do.

2) Preservation of Strong Normalization. This means that any term that always end up in a solution in the classical λ-calculus, then it will always end up in a solution in the new calculus.

These properties are needed, for instance, in proof assistants or HO unificators. If you don’t know what I’m talking about, nevermind. The idea was just to show why the interest in these properties.

So, is there a calculus with explicit substitution that has all these properties? Yes, but at a price. Other wanted (but maybe less common) properties got broken.

I will talk about these properties in posts to come. Stay tuned!

Explicit Substitutions, or Substitutions If You Need to Implement Them

As I told you before, performance is something desirable when programming a λ interpreter. The sustitutions we saw are made in one step.

I will note the beta step as →β and a substitution step as →. For instance,

(λx.x) z  →β  x[x/z]  →  z.

The computations of the traditional lambda calculus are always:

T →β T’ → → → → until no more substitutions can be made →β T” → → →…

Now, if we want to control the substitutions, one can make some computations like

T →β T’ few steps of sustitutions →β T” →β T”…

To make it clear, supose the term

(λx. y) ((λx. x x) z)

One posible reduction in the traditional λ calculus is

(λx. y) ((λx. x x) z)  →β  (λx. y) (x x)[x/z]  →  (λx. y) (x[x/z] x[x/z])  →  (λx. y) (z x[x/z])  →  (λx. y) (z z)  →  y[x/(z z)]  →  y

But a more clever path is posible, if we don’t make all the substitutions:

(λx. y) ((λx. x x) z)  →β  (λx. y) (x x)[x/z]  →  y[x/(x x)[x/z]]  →  y

So a calculus with explicit substitution is a calculus that has the substitutions as another rewriting rules. For instance, λx is the simpler calculus:

(λx. M) N →β M[x/N]
x[x/R] R
y[x/R] y
(T T’)[x/R] T[x/R] T’[x/R]
(λy.T)[x/R] (λy.T[x/R])

That’s the idea behind explicit substitutions. It’s very simple and yet has many issues I will show in future posts.