# Evaluate this alpha substitution $[(zx)/x] \, \lambda z.xyz$

I am having difficulty with the following problem: Calculate the result of this substitution, renaming the bound variables as needed, so that substitution is defined

$$[(zx)/x] \, \lambda z.xyz$$

Attempt: If I were to simply replace $$x$$ with $$zx$$ in this expression it would yield : $$\lambda z.zxyz$$ but I am not sure if this is correct. Any tips appreciated as I honestly don't even know what the question is asking because it seems to imply I should be renaming bound variables

• Don't know if it matters, but maybe keep the parenthesis around $(zx)$ when it replaces the $x.$ – coffeemath Nov 11 '18 at 2:36
• I guess my gripe is that it just seems too simple a solution I feel like I am missing something. – IntegrateThis Nov 11 '18 at 2:42
• Since it's just substitution I'd expect it to be easy rather than involved. Disclaimer-- I'm not familiar with the lambda notation or whatever it's called. – coffeemath Nov 11 '18 at 3:06

Short answer. No, the answer proposed here is wrong. Actually, $$[(zx)/x]\, \lambda z.xyz = \lambda t.(zx)yt$$, which is completely different from $$\lambda t.(t(zx)y)$$ because application is not commutative, unlike the usual product: in general, the term $$xy$$ is the application of $$x$$ to $$y$$ (where $$x$$ and $$y$$ are intended as two arbitrary functions), which is different from $$yx$$ i.e. the application of $$y$$ to $$x$$.

Anyway, you are right when you say that $$[(zx)/x]\, \lambda z.xyz \neq \lambda z.zxyz$$. Indeed, substitution in the $$\lambda$$-calculus is not a simple replacement of something with something else, because of the problem of the capture of variables, which I explain below.

Substitution is a delicate operation in the $$\lambda$$-calculus. Indeed, the $$\lambda$$-calculus is intended as a formal system for expressing computation based on abstraction and application using variable binding and substitution, where functions are taken as first class values: every term in the $$\lambda$$-calculus represents a (computable) function. A naïve approach in the definition of substitution in the $$\lambda$$-calculus may change the meaning of the represented functions in a inconsistent way.

In the syntax of the $$\lambda$$-calculus, the $$\lambda$$ is an operator binding a variable in a function. For instance, the term $$\lambda x.x$$ represents the identity function ($$x \mapsto x$$), the term $$\lambda x. y$$ represents the constant function ($$x \mapsto y$$, i.e. everything is mapped to $$y$$). Note that the particular choice of a bound variable, in a $$\lambda$$, does not (usually) matter: for instance, the term $$\lambda x . x$$ is the same as the term $$\lambda y. y$$ because they both represents the identity function. Formally, terms in the $$\lambda$$-calculus are identified up to $$\alpha$$-equivalence, i.e. up to renaming of the bound variables.

Now, consider the term $$[x/y] \, \lambda x. y$$. Morally, it represents the constant function $$x \mapsto y$$ (everything is mapped to $$y$$) where $$y$$ is replaced by $$x$$, that is, it represent the constant function $$z \mapsto x$$ (everything is mapped to $$x$$). However, if we intended the substitution as a simple replacement, $$[x/y] \, \lambda x. y$$ would be $$\lambda x. x$$, i.e. the constant function, a completely different function from the intended one. The problem arises because the variable $$x$$ in the substitution $$[x/y]$$ has be captured by the binder $$\lambda x$$ in the term. So, in order to define substitution in a consistent way, the problem of the capture of variable has to be avoided.

The solution is defining substitution in a capture-avoiding way as follows: given the terms $$t$$ and $$u$$, the term $$[u/x]\, t$$ is obtained from $$t$$ by replacing the free (i.e. not bound by a $$\lambda$$) occurrences of $$x$$ in $$t$$ with $$u$$, provided that the bound variables of $$t$$ are not free in $$u$$; if this proviso is not fulfilled by $$t$$, then we work on a term $$t'$$ (instead of $$t$$) where this proviso holds: this is always possible thanks to $$\alpha$$-equivalence, i.e. by renaming the bound variables in $$t$$ (which does not change the meaning of $$t$$, as I explained before). For example, in $$[x/y] \, \lambda x. y$$ the variable $$x$$ in the substitution is also a bound variable in the term $$\lambda x. y$$; then, instead of performing the replacement on $$\lambda x. y$$, we do it in the $$\alpha$$-equivalent term $$\lambda z. y$$ (or $$\lambda w.y$$, it is the same) and then we get $$[x/y] \, \lambda x. y = \lambda z. x$$ (or equivalently, $$[x/y] \, \lambda x. y = \lambda w. x$$).

Coming back to your question, in the term $$[(zx)/x]\, \lambda z.xyz$$, the term $$zx$$ in the substitution contains a free variable $$z$$ that is bound in $$\lambda z.xyz$$, so before performing the substitution we have to rename the term $$\lambda z.xyz$$ in a $$\alpha$$-equivalent way, say $$\lambda w.xyw$$ (or equivalently, $$\lambda t.xyt$$, if $$t$$ stands for a variable). Therefore, $$[(zx)/x]\, \lambda z.xyz = \lambda w.(zx)yw$$ (or equivalently, $$[(zx)/x]\, \lambda z.xyz = \lambda t.(zx)yt$$).

Ok, so I figured out what was wrong. The question is basically saying, in regular English, replace a free variable by another free variable that is the product of two free variables, so the answer is

$$\lambda t.(t(zx)y)$$

• No, it isn't. Actually, $[(zx)/x] \lambda z.xyz = \lambda t. (zx)yt$. Moreover, saying that $zx$ is the product of two variables is really misleading: $zx$ is the application of the variable $z$ to the variable $x$. Note that the application is not commutative, unlike the usual product. – Taroccoesbrocco Nov 13 '18 at 6:39
• oops. Ok my bad. – IntegrateThis Nov 13 '18 at 22:02
• Maybe you should post an answer then. – IntegrateThis Nov 13 '18 at 22:15
• Done! Don't hesitate to ask more if it is unclear or too technical. – Taroccoesbrocco Nov 14 '18 at 9:20