Lambda calculus Clarification about free and bound variables

Question

In $(\lambda x.yx)$ y is free.

How about in $(\lambda x.xy)$ is y bound here? Some googling I've found that y is actually free, but isn't y in the scope of $\lambda x$?

Thanks!

Answer 1

If $f(x)=x^n$ we can clearly see that n is free variable.

We can think of this as $\lambda x.fxn$ and x is bound but f and n are free.

So in the main question $\lambda x.xy$, y is clearly free.

Answer 2

$y$ is in the scope of $\lambda x$ in both terms, but not bound by it. A variable can only be bound by an abstraction of the same variable. $y$ can only be bound by $\lambda y$, not by $\lambda x$.

Answer 3

$\newcommand{\abstraction}[2]{\lambda #1. #2}$ $\newcommand{\application}[2]{\left(#1 #2\right)}$ $\newcommand{\substitution}[3]{#1 \left[#2 := #3\right]}$ $\newcommand{\freevars}[1]{\operatorname{FV}\left(#1\right)}$ $\newcommand{\closedlambdaset}{\Lambda^{0}}$ $\newcommand{\lambdaexprswithfreevars}[1]{\closedlambdaset\left(#1\right)}$ $\newcommand{\subterm}[1]{\operatorname{Sub}\left(#1\right)}$ $\newcommand{\vars}[1]{\operatorname{Var}\left(#1\right)}$ $\newcommand{\context}[2]{{#1}\left[#2\right]}$ $\newcommand{\hole}{\ }$

For the sake of completeness, a variable $x$ is free in a $\lambda$-term $M$ if $x$ is not in the scope of a $\lambda x$; otherwise, $x$ occurs bound.

It is usual to inductively define $\operatorname{FV}(M)$, the set of free variables in $M$ as:

• $\operatorname{FV}(x) = \{x\}$

  the norm is to be free

• $\operatorname{FV}(\abstraction{x}{M}) = \operatorname{FV}(M) - \{x\}$

  an abstraction bounds exactly the variable it abstracts and nothing else

• $\operatorname{FV}(\application{M}{N}) = \operatorname{FV}(M) \cup \operatorname{FV}(N)$

  keep inspecting the subterms

Things may get eccentric, for instance, in $({\abstraction{y}{x y}})(y)$, $x$ is free, the $y$ on the left parenthesized term is bounded, and the last (rightmost) $y$ is free. I often prefer to index the variables to avoid confusion, but this also comes with its annoyances.