In lambda calculus, the λ symbol is followed by a variable. Can that variable be a lambda expression

lambda-calculus

In general, in the lambda calculus syntax, the "$\lambda$" symbol is followed by a variable or identifier, but could the variable following the "$\lambda$" symbol be a lambda expression itself. For example, let

$$\lambda (\lambda x.x).y$$

be called expression $A$. In expression $A$, the first "$\lambda$" symbol is followed by a variable that is an expression "$\lambda x.x$".


In some manner, expression $A$ is similar to the following:

$$(\lambda z.y)(\lambda x.x)$$

If it is valid to do $\beta$-reduction "$[z:=(\lambda x.x)]$", then we get expression $A$:

\begin{align}
(\lambda z.y)(\lambda x.x) \\
(\lambda z.y)[z:=(\lambda x.x)] \\
\lambda (\lambda x.x).y
\end{align}


What about the following expression, let's call it expression $B$:

$$\lambda ((\lambda z.z)x).y$$

In expression $B$, the first "$\lambda$" symbol is followed by a variable that is an expression "$((\lambda x.x)x)$", which is an expression that evaluates to a single variable, namely "$x$". So would it be valid to reduce expression $B$ as follows:

\begin{align}
\lambda ((\lambda z.z)x).y \\
\lambda ((\lambda z.z)[z:=x]).y \\
\lambda (x).y \\
\lambda x.y
\end{align}


In some manner, expression $B$ is similar to the following:

$$(\lambda w.y)((\lambda z.z)x)$$

If it is valid to do $\beta$-reduction "$[w:=((\lambda z.z)x)]$", then we get expression $B$:

\begin{align}
(\lambda w.y)((\lambda z.z)x) \\
(\lambda w.y)[w:=((\lambda z.z)x)] \\
\lambda ((\lambda z.z)x).y
\end{align}

Best Answer

In the standard lambda calculus, this is not valid at all. You can only form $\lambda x$ when $x$ is a (new) variable name.

Other forms of the lambda calculus have been studied in which the $\lambda$ can be followed by an arbitrary term. Sometimes, this is called a 'pattern matching lambda calculus', since the term following the $\lambda$ sign gives us a pattern that has to match up with the argument in order to be evaluated.

For example, we could define a term $$ \text{pred} = \lambda (\lambda f.\lambda x.f z).\lambda f.\lambda x.z\,, $$ corresponding to taking the predecessor of a non-zero Church numeral. We would then have: $$ \text{pred}\;\lambda f.\lambda x.f\,(f\,x) \to \lambda f.\lambda x.f\,x\,, $$ but $$ \text{pred}\;\lambda f.\lambda x. x $$ would not reduce any further, since $\lambda f.\lambda x.x$ is not of the form $\lambda f.\lambda x.f\,z$.


As a side-note, the two examples of beta-reduction that you have given are not correct. The term $$ (\lambda z.y)(\lambda x.x) $$ reduces to $y[z:=\lambda x.x] = y$, since $y$ contains no occurrences of the variable $z$ to replace. Similarly, $$ (\lambda w.y)((\lambda z.z)x) $$ reduces to $y[w:=(\lambda z.z)x] = y$.


References

Klop, JW, van Oostrom, V & de Vrijer, RC 2008, 'Lambda calculus with patterns', Theoretical Computer Science, vol. 398, no. 1-3, pp. 16-31. https://doi.org/10.1016/j.tcs.2008.01.019