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.

  • 1
    $\begingroup$ The parenthesis in it would be $\lambda x.(\lambda y.(xy))$ $\endgroup$
    – DanielV
    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$.

  • $\begingroup$ 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. $\endgroup$ Jan 7 '21 at 0:19
  • $\begingroup$ @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. $\endgroup$ Jan 7 '21 at 0:28
  • $\begingroup$ 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. $\endgroup$ Jan 7 '21 at 0:46
  • 1
    $\begingroup$ @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. $\endgroup$ Jan 7 '21 at 1:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.