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!