I am studying Haskell and I am learning what are abstraction, substitution ($\beta$-equivalence), application, free and bound variables ($\alpha$-equivalence), but I have some doubts resolving these exercises, I don't know if my solutions are correct.
Exercise. Make the following substitutions
1. (λ x → y x x) [x:= f z]
Sol. (\x -> y x x) =>α (\w -> y w w) =>α (\w -> x w w) =>β (\w -> f z w w)
2. ((λ x → y x x) x) [y:= x]
Sol. ((\x -> y x x)x) =>α (\w -> y w w)[y:= x] = (\w -> x w w)
3. ((λ x → y x) (λ y → y x) y) [x:= f y]
Sol. aproximation, i don't know how to do it: ((\x -> y x)(\y -> y x) y) =>β
(\x -> y x)y x)[x:= f y] =>β y x [x:= f y] = y f y
4. ((λ x → λ y → y x x) y) [y:= f z]
Sol aproximation, ((\x -> (\y -> (y x x))) y) =>β ((\y -> (y x x)) y) =>α ((\y -> (y x x)) f z)
Another doubt that I have is if can I run these expressions on this website? https://lambdacalc.io/
It is a Lambda Calculus Calculator but I do not know run these tests.
Best Answer
First, let us recall the definition of substitution in the $\lambda$-calculus ($\beta$-equivalence is something different, don't mix up them):
$$ M [x := N] $$ is the term obtained from $M$ by substituting $N$ for the free occurrences of $x$ in $M$, provided that the free variables of $N$ are not bound in $M$.
If there are some free variables of $N$ that are bound in $M$, $M [x:=N]$ is obtained by first replacing $M$ with $M'$, where $M'$ is a term $\alpha$-equivalent to $M$ obtained by renaming the bound variables of $M$ by fresh variables, so that they are distinct from the free variables of $N$; then compute $M' [x := N]$.
Solutions to your exercise:
$(λ x.y x x) [x:= f z]$: the variable $x$ does not occur free in $λ x.y x x$, thus there is nothing to be substituted. Therefore, $$ (λ x.y x x) [x:= f z] = λ x.y x x $$
$((λ x . y x x) x) [y:= x]$: the variable $x$ is bound in $(λ x. y x x) x$, so before performing the substitution $[y:=x]$ we have to rename the bound variables of $(λ x . y x x) x$ using fresh variables; in this case, the first two occurrences of $x$ are bound and we rename them by the fresh variable $z$, thus $(λ x . y x x) x =_\alpha (λ z . y zz) x$. Therefore, $$ ((λ x . y x x) x) [y:= x] = ((λ z . y zz) x) [y:= x] = (λ z . x zz) x $$
$((λ x . y x) (λ y . y x) y) [x:= f y]$: the variable $y$ is free in $fy$ but bound in $(λ x . y x) (λ y . y x) y$, so before performing the substitution $[x:= fy]$ we have to rename the bound variables of $(λ x . y x) (λ y . y x) y$ using fresh variables, so that the bound variables are distinct from $f$ and $z$; in this case, the second occurrence of $y$ is bound and we rename it by the fresh variable $z$, thus $(λ x . y x) (λ y . y x) y =_\alpha (λ x . y x) (λ z . z x) y$. Note also that the first occurrence of $x$ is bound, so it shouldn't be replaced when performing the substitution. Therefore, $$ ((λ x . y x) (λ y . y x) y) [x:= fy] = ((λ x . y x) (λ z . z x) y) [x:= fy] = (λ x . y x) (λ z . z (fy)) y $$
$((λ x . λ y . y x x) y) [y:= f z]$: only the last occurrence of $y$ in $((λ x . λ y . y x x) y) $ is free, hence it is the only one to be substituted. Also, in $((λ x . λ y . y x x) y) $ the variables $f$ and $z$ are not bound, thus there is no $\alpha$-renaming to be performed. Therefore, $$((λ x . λ y . y x x) y) [y:= f z] = (λ x . λ y . y x x) (f z)$$