# Scaled lambda epsilon

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 $A$ and a scale $\varepsilon \in \Gamma$,

– transform a tree $T$ such that $FV(T) \cap FV(A) = \emptyset$,  into a tree $A_{\varepsilon}[T]$, by conjugating with $A \circ_{\varepsilon} \cdot$.

This can be done by recursively defining the transform $T \mapsto A_{\varepsilon}[T]$. 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 $\lambda$ from (a) does not make sense, because $A \circ_{\varepsilon} u$ 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 $B[ A \circ_{\varepsilon} u : = C]$ because of the invertibility of dilations. Indeed, $A \circ_{\varepsilon} u = C$ is equivalent with $u = A \circ_{\varepsilon^{-1}} C$, therefore we may define $B[ A \circ_{\varepsilon} u : = C]$ to mean $B[u : = A \circ_{\varepsilon^{-1}} C]$.

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 $u \in X \setminus FV(A)$ defined a relative variable $u^{\varepsilon}_{A} := A \circ_{\varepsilon} u$ (remark that relative variables are terms!).The set of relative variables is denoted by $X_{\varepsilon}(A)$.

2. The function $B \mapsto A_{\varepsilon}[B]$ is defined for any term $B \in T$ such that $FV(A) \cap FV(B) = \emptyset$. The definition is this:

–  $A_{\varepsilon}[A] = A$,

–  $A_{\varepsilon}[u] = u$ for any $u \in X \setminus FV(A)$

$A_{\varepsilon}[ B \mu C] = A \circ_{\varepsilon^{-1}} ((A \circ_{\varepsilon} A_{\varepsilon}[B]) \mu (A \circ_{\varepsilon} A_{\varepsilon}[C]))$  for  any $B, C \in T$ such that $FV(A) \cap (FV(B) \cup FV(C))= \emptyset$

–  $A_{\varepsilon}[ u \lambda B]$ is given by:

3. $B$ is a scaled term, notation $B \in T_{\varepsilon} (A)$, if there is a term $B' \in T$ such that $FV(A) \cap FV(B') = \emptyset$ and such that $B = A_{\varepsilon}[B']$.

4. Finally, the operations on scaled terms are these:

– for any $\mu \in \Gamma$ and $B, C \in T_{\varepsilon}(A)$ the scaled application (of coefficient $\mu$) is

$B \mu^{\varepsilon}_{A} C = A \circ_{\varepsilon^{-1}} ((A \circ_{\varepsilon} B) \mu (A \circ_{\varepsilon} C))$

– for any scaled variable  $u^{\varepsilon}_{A} \in X_{\varepsilon}(A)$  and any scaled term $B \in T_{\varepsilon}(A)$ the scaled abstraction is

5.    With this, we can prove that $(u^{\varepsilon}_{A} \lambda^{\varepsilon}_{A} B) 1^{\varepsilon}_{A} C = (u \lambda B) 1 C = B [ u: = C]$, which is remarkable, I think!