Chained substitutions of an application in $\lambda$-calculus, e.g. $AB[C/x][D/y]$

Question

Let $A[C/x]$ denote substitution of $C$ for $x$ in $A$.

Suppose we arrived at the expression $AB[C/x][D/y]$ and we want to manipulate it as follows:

$$ \begin{aligned} AB[C/x][D/y] &= \Big(\big((AB)[C/x]\big)[D/y]\Big)\\ &= \Big(\big((A[C/x])(B[C/x])\big)[D/y]\Big)\\ &= \Big(\big((A[C/x])[D/y]\big)\big((B[C/x])[D/y]\big)\Big)\\ &= \big(A[C/x][D/y]\big)\big(B[C/x][D/y]\big)\\ \end{aligned} $$

• Can we perform the above manipulations always?
• Or only if certain conditions hold?
  • such as $x \neq y \text{ and } \big(y \not \in \textsf{FV}(C) \text{ or } x \not \in \textsf{FV}(AB)\big)$ (see below)

---

Here's one way to arrive at $AB[C/x][D/y]$:

$\beta$-reduction is, of course, defined in terms of substitution as:

$$(\lambda x.A)\ C \rightarrow_{\beta} A[C/x]$$

Under certain conditions, we have

$$(\lambda xy.AB)\ C\ D \twoheadrightarrow_{\beta} AB[C/x][D/y]$$

Proof:

$$ \begin{aligned} (\lambda xy.AB)\ C\ D &\rightarrow_{\beta} ((\lambda y.AB)[C/x])\ D\\ &\equiv (\lambda y.(AB[C/x]))\ D &&\text{conditions: } x \neq y \text{ and } \big(y \not \in \textsf{FV}(C) \text{ or } x \not \in \textsf{FV}(AB)\big)\\ &\rightarrow_{\beta} (AB[C/x])[D/y]\\ &\equiv AB[C/x][D/y] \end{aligned} $$

Answer 1

What you described above sounds nothing but successive substitutions in lambda calculus and we certainly need some rules for it to be manipulated like you specified as referenced here:

Substitution on terms of the lambda calculus is defined by recursion on the structure of terms, as follows (note: x and y are only variables while M and N are any lambda expression):

$1. x[x := N] = N \\ 2. y[x := N] = y, \text{if}~ x ≠ y \\ 3. (M_1 M_2)[x := N] = (M_1[x := N]) (M_2[x := N]) \\ 4. (λx.M)[x := N] = λx.M \\ 5. (λy.M)[x := N] = λy.(M[x := N]), \text{if}~ x ≠ y ~\text{and}~ y ∉ FV(N) \\ 6. \text{To substitute into an abstraction, it is sometimes necessary to α-convert the expression.}$

β-reduction is defined in terms of substitution...

So in your first example if both $A,B$ are terms without abstraction, then you can always have $AB[C/x][D/y]=(A[C/x][D/y])(B[C/x][D/y])$ and further possible result may be based on the specific content of $A,B$. For example, if $A$ doesn't contain variable $x$ and $x \neq y$ then your substitution $[C/x]$ will have no effect on $A$. On the other hand, if your expressions have lambda abstraction(s), then you need to match the conditions of any of the rules 4/5/6 above to proceed accordingly.

Finally successive substitution is different from simultaneous substitution as shown from following example using your notation. If $M ≡ x_1x_2$, then the successive substitution results in $(M[x_1 /x_2])[u/x_1] ≡ [u/x_1 ](x_1x_1) ≡ uu$, while the simultaneous substitution results in $M[x_1 /x_2, u/x_1] ≡ ux_1$.