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

  • $\begingroup$ Don't know if it matters, but maybe keep the parenthesis around $(zx)$ when it replaces the $x.$ $\endgroup$ – coffeemath Nov 11 '18 at 2:36
  • $\begingroup$ I guess my gripe is that it just seems too simple a solution I feel like I am missing something. $\endgroup$ – IntegrateThis Nov 11 '18 at 2:42
  • $\begingroup$ 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. $\endgroup$ – 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.

(Very) Long answer.

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)$

  • 1
    $\begingroup$ 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. $\endgroup$ – Taroccoesbrocco Nov 13 '18 at 6:39
  • $\begingroup$ oops. Ok my bad. $\endgroup$ – IntegrateThis Nov 13 '18 at 22:02
  • $\begingroup$ Maybe you should post an answer then. $\endgroup$ – IntegrateThis Nov 13 '18 at 22:15
  • $\begingroup$ Done! Don't hesitate to ask more if it is unclear or too technical. $\endgroup$ – Taroccoesbrocco Nov 14 '18 at 9:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.