Substitution $(20$ points$)$In class we described capture$-$avoiding substitution e$1\{$e$2/$x$\}$ in order to describe $-$reduction. We did not,however, formally define it$.$ We rectify this by giving the following inductive definition of substitution.y$\{$e$/$x$\}=($e if x $=$ yy if x$=$ y$($e$1$ e$2)\{$e$/$x$\}=$ e$1\{$e$/$x$\}$ e$2\{$e$/$x$\}($y$.$ e$)\{$e$/$x$\}=$y$.$ e if x $=$ yy$.($e$\{$e$/$x$\})$ if x$=$ y and y FV $($e$)$z$.(($e$\{$z$/$y$\})\{$e$/$x$\})$ if x$=$ y and y FV $($e$),$ wherez FV $($e$)$ FV $($e$)\{$x$\}$The function FV takes a lambda calculus expression e and returns the set of free variables of e$.$ Thus,y FV $($e$)$ if and only if y is a free variable of e$.$ For example FV $($x$.$ z y$.$ x y$)=\{$z$\},$ and for any expressione, e is a closed term if and only if FV $($e$)=.($a$)$ Give an inductive definition of the function FV $.($b$)$ Show the result of the following substitutions. $($z$.$ y y$.$ y z w$)\{($x$.$ x$)/$y$\}(($x$.$ x y$)($z$.$ x z$))\{($w$.$w w$)/$x$\}($y$.$ x y$)\{($z$.$ y z$)/$x$\}(($x$.$ w$.$w x$)$ y$.$ x y$)\{($w w$)/$x$\}($c$)$ Consider the following alternate $($and incorrect$)$ definitions for substitution for abstractions: $($y$.$ e$)\{$e$/$x$\}($for the other cases, the definition remains the same$).$ For each alternate definition give an examplesubstitution in which the original and alternate definitions produce different results, and give thoseresults.$($i$)($y$.$ e$)\{$e$/$x$\}=($y$.$ e if x $=$ yy$.($e$\{$e$/$x$\})$ if x$=$ y$($ii$)($y$.$ e$)\{$e$/$x$\}=$ y$.$ e if x$=$yy$.($e$\{$e$/$x$\})$ if x$=$ y and y FV $($e$)$z$.(($e$\{$z$/$y$\})\{$e$/$x$\})$ if x$=$ y and y FV $($e$),$ wherez FV $($e$)\{$x$\}$