Is the application of a free variable valid in lambda calculus

Question

Can you apply a free variable to something in lambda calculus? It is my understanding that an unbound variable equals itself, for example, $(\lambda x . y) a = y$. So, if a free variable just equals itself, then would the fully reduced form of $(\lambda x . (y x)) a$ be literally $(y a)$?

Answer 1

Yes. The terms of the lambda-calculus are given by the formation rules

• $x$ is a term for any variable $x$
• If $e_1$ and $e_2$ are terms, then so is $e_1 e_2$
• If $x$ is a variable and $e$ is a term, then $\lambda x.e$ is a term
• If $e$ is a term, then $(e)$ is a term
• Nothing else is a term

So $(\lambda x.y)a$ is a valid term, and it $\beta$-reduces to $y$.