Luis Ziliani, a.k.a. Beta

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.

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!