# Interpretation of a term in Lambda Calculus

Just started studying $$λ$$-calculus and I came across this $$λ$$-term : $$λx.λy.xy$$ As far as I understand this can be read as :

1. Apply $$x$$ to $$y$$
2. The result of $$(1)$$ is probably an expression say $$E_1$$
3. $$y$$ variable is a bound variable while $$x$$ is a free variable in the context of $$E_1$$
4. 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.

• The parenthesis in it would be $\lambda x.(\lambda y.(xy))$ Jan 7 '21 at 0:11

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$$.
• Is this example an accurate translation of what you stated? $F(x,y)=x+y$ where by applying $x$ to $y$ is the addition of $x$ to $y$. I emphasize accurate as from what I've read $λ$ - calculus is just a formal system of writing functions. Jan 7 '21 at 0:19
• @RookieCookie - Sorry, I'm not sure to understand what you mean when you say "Is the example above an accurate translation of what you stated?". What is the example above? Anyway, your interpretation of $F(x,y) = x + y$ is not accurate. The function $F(x,y) = x + y$ can be represented in the $\lambda$-calculus formalism as $\lambda x.\lambda y. (+ x) y$, where $+$ stands for a $\lambda$-term representing addition. Note that arithmetical addition $x + y$ is a infix notation for the function $\lambda x. \lambda y. +(x,y)$, which is equivalent to say $\lambda x.\lambda y. (+ x) y$ by currying. Jan 7 '21 at 0:28
• My example was the function $F(x,y)=x+y$ .I know that it was not so accurate and I was trying to understand the intuition behind applying $x$ to $y$ but I think I get it now. One last question though how would one interpret the $λx.λy.y$ or $λx.λy.x$ term? In each case the function consists of 2 arguments but one of them is not around. $x$ argument is not around in $λx.λy.y$ and $y$ is not around in $λx.λy.x$.By not around I mean even though they are plugged in they are not used. Jan 7 '21 at 0:46
• @RookieCookie - The term $\lambda x. N$ when $x$ does not appear in $N$ represents a function that associates $x$ to a function that does not depend on $x$, i.e. it takes an argument $x$ and discard it without using it. Hence, the $\lambda$-term $\lambda x. \lambda y. y$ represents the function $x \mapsto \lambda y.y$: with every argument it associates the function $y \mapsto y$, which is the identity function. Pay attention that I'm not saying that $\lambda x. \lambda y. y$ is the identity function, but that it is the function that associates every argument to the identity function. Jan 7 '21 at 1:11