My first attempt to introduce a scaled version of lambda epsilon turned out to be wrong, but now I think I have found a way. It is a bit trickier than I thought. Let me explain.
In lambda epsilon calculus we have three operations (which are not independent), namely the lambda abstraction, the application and the emergent algebra (one parameter family of) operation(s), called dilations. If we want to obtain a scaled version then we have to “conjugate” with dilations. Looking at terms as being syntactic trees, this amounts to:
– start with a term and a scale ,
– transform a tree such that , into a tree , by conjugating with .
This can be done by recursively defining the transform . Graphically, we would like to transform the elementary syntactic trees of the three operations into this:
The problem is that, while (c) is just the familiar scaled dilation, the scaled from (a) does not make sense, because is not a variable. Also, the scaled application (b) is somehow misterious.
The solution is to exploit the fact that it makes sense to make substitutions of the form because of the invertibility of dilations. Indeed, is equivalent with , therefore we may define to mean .
If we look to the rule (ext2) here, the discussion about substitution becomes:
Therefore the correct scaled lambda, instead of (a) from the first figure, should be this:
The term (syntactic tree) from the LHS should be seen as a notation for the term from the RHS.
And you know what? The scaled application, (b) from the first figure, becomes less misterious, because we can prove the following.
1. Any defined a relative variable (remark that relative variables are terms!).The set of relative variables is denoted by .
2. The function is defined for any term such that . The definition is this:
– for any
– for any such that
– is given by:
3. is a scaled term, notation , if there is a term such that and such that .
4. Finally, the operations on scaled terms are these:
– for any and the scaled application (of coefficient ) is
– for any scaled variable and any scaled term the scaled abstraction is
5. With this, we can prove that , which is remarkable, I think!