Substitution in a complex lambda calculus formula

Question

I have the following lambda expression:

$$( (y \lambda x \rightarrow \lambda y \rightarrow f y) (\lambda f \rightarrow f y z) )[y := f x]$$

So, my questions are,

• I see $y$ before a lambda abstraction, what does that mean ? Is that y free ?
• Is it correct to put parenthesis like this in the expression ?

$$(y (\lambda x \rightarrow \lambda y \rightarrow f y)) (\lambda f \rightarrow f y z) )[y := f x]$$

Then, I would have the term $f x$ applied to the lambda expression:

$$(\lambda x \rightarrow \lambda y \rightarrow f y)$$

However, is that $f$ free ?

I learned, for example:

• a variable is bound if it is within the scope of a lambda term; otherwise, it is free.
• I can only substitute free occurrences of a variable.
• I should avoid variable capturing by using alpha conversion.

I thought I understood the basics of lambda calculus substitution, but I can't grasp this example. I clearly have gaps in my understanding.

Answer 1

I have the following lambda expression: $((yλx→λy→fy)(λf→fyz))[y:=fx]$

Uh, this is a weird syntax, I assume it should be read as $((yλx.λy.fy)(λf.fyz))[y:=fx]$.

I see $y$ before a lambda abstraction, what does that mean ? Is that $y$ free ?

A variable (or more precisely, an occurrence of a variable) isn't free in general, but only free (or bound) in a given term. Here, the first occurrence of $y$ is indeed free in the term $(yλx→λy→fy)(λf→fyz)$. But in the whole term you give it is substituted, so it doesn't even exist as a “true” variable occurrence — and thus, is neither free nor bound. (The other occurrence of $y$ is bound by $\lambda y$ in any case.)

This is where the subtility of this example arises, because you substitute $fx$ to $y$ in a λ-expression where

• $y$ appears both free and bound, which may be overcome depending on the way you define substitution (see this answer);
• $f$ appears bound, which forbids substitution without performing α-conversion first.

The minimal conversion you must do is the following (I put the fresh variables in capital letters):

$((yλx→λy→fy)(λf→fyz))[y:=fx] \\ =_α ((yλx→λy→fy)(λF→Fyz))[y:=fx] \\ = ((fx)λx→λy→fy)(λF→F(fx)z)$

but it would be cleaner (and might be required by your definition of the substitution) to convert also the bound $y$:

$((yλx→λy→fy)(λf→fyz))[y:=fx] \\ =_α ((yλx→λY→fY)(λF→Fyz))[y:=fx] \\ = ((fx)λx→λY→fY)(λF→F(fx)z) $

Is it correct to put parenthesis like this in the expression ?

I would say yes. But this depends on the way you defined the syntax of the λ-calculus, there are several valid choices for the scope of the constructors and the placing of the parentheses. (See the curious, yet very practical Krivine notation.)

Then, I would have the term $fx$ applied to the lambda expression: $(λx→λy→fy)$. However, is that $f$ free ?

Yes, these two $f$ are free.