Lambda calculus entire expression substitution

Question

About substitution of free occurances: can we have a substitution of an entire expression(function, application), or just of a variable:

Example:

• Current expression \x.\y.(y, z)
• Expression to be replaced: \y.(y z) with p so we will have \x.p.

Is it possible?

Answer 1

Yes, it is possible. One way is to consider the substitution of occurrences. An occurrence is a string over the set {1,2,3}, and for every lambda-term M, the sub-expression M/u at occurrence u is defined as:

• M/[] = M
• M/0u = N/u, if M=\x. N
• M/1u = P/u, if M=PQ
• M/2u = Q/u, if M=PQ

(I use the symbol [] to denote the empty string.)

Now define the substitution M[u := N] as the term obtained from replacing the occurrence u with N in M. I've seen this kind of substitution in some of P.-L. Curien work.