Just started studying $λ$-calculus and I came across this $λ$-term : $$λx.λy.xy$$ As far as I understand this can be read as :
- Apply $x$ to $y$
- The result of $(1)$ is probably an expression say $E_1$
- $y$ variable is a bound variable while $x$ is a free variable in the context of $E_1$
- For some input $I$ apply $E_1$ to $I$ and the result is an expression say $E_{2}$ that depends on $x$
Everything emphasized is a hypothesis. Still trying to understand this formal system of writing functions so any insight would be really helpful.
Note that, with explicit full parenthesization, the term is $\lambda x. (\lambda y. (xy))$
Thus, the meaning of the term $\lambda x. \lambda y. xy$ is the following. It is a function of two arguments (this is the meaning of the initial $\lambda x.\lambda y$) that takes the first argument (represented by the parameter $x$) and apply it to the second argument (represented by the parameter $y$), since $xy$ is the application of $x$ to $y$.
Remember that, in the $\lambda$-calculus, everything is a function and so it is standard that the argument of a function is another function.
In general, a term of the form $\lambda x. N$ has to be seen as a function $x \mapsto N$, i.e. a function that associates $x$ to $N$ (which, in turn, is another function). Hence, a term of the form $\lambda x. \lambda y. M$ has to be seen as a function $x \mapsto (y \mapsto M)$, i.e. a function that associates $x$ to a function that associates $y$ to $M$. By (de-)currying, this is equivalent to see $\lambda x. \lambda y. M$ as a function that associates a couple of arguments $(x,y)$ to $M$.