# Why is it that a lambda function requiring multiple input also requires multiple functions?

So I recently discovered lambda calculus and for the most part I understand it. However, one specific part of it that I cannot understand is this:

Let's say we define a very simple function

$$I := \lambda a.a$$

This is simple to understand, nothing confusing. However, if you add another input I will scratch my head furiously:

$$A := \lambda a.\lambda b.a+b$$

This is confusing to me for at least 2 reasons:

1. Why is it that I cannot define a function with multiple parameters like so:

$$A := \lambda a,b. a+b$$

2. How does the second function returned have access to the first parameter if they can only hold one parameter? Is there a prospective for scope? If so, how does it work?

1. You can. It is just not written with comma. Your function would then be written as $$\lambda a b. a+b$$ and this is known as uncurrying. Note that this is still $$\lambda a. \lambda b. a+b$$ in all sense, but just written differently.

2. The inner function does not need to know about variable $$a$$. Suppose we evaluate $$(\lambda a b. a+b)\ 2$$ We will get $$\lambda b. 2+b$$ which is a function that adds its argument to the number $$2$$ and does not need access to the variable $$a$$. There is no variable $$a$$ at this point if the function goes through any further evaluations.

And to directly answer your question from the title: Because by definition of $$\lambda$$-expressions, functions (abstractions) are always of $$1$$ argument. In the case of $$\lambda$$-calculus, uncurried form is just a writing convention (doesn’t change $$\lambda$$-expression’s nature). The inner workings stay the same (curried).

• Isn't $\lambda ab.a+b$ just a shorthand for $\lambda a \lambda b.a+b$? Especially because you cannot evaluate uncurried functions like this $(\lambda ab.a+b) \;2$, since the type of the argument would have to be a pair. – Asurafire Oct 10 '18 at 12:20
• It is. As I said: Uncurrying is just a writing convention – Sandro Lovnički Oct 10 '18 at 12:22
• Maybe in lamda-calculus, but probably not even there, because you can actually define a pair type. If you consider functions in programming languages as mathematical functions, there is surely a difference between the curried/uncurried version of one function. – Asurafire Oct 10 '18 at 12:25
• Thanks this answer really cleared the confusion, especially at #2. – Delupara Oct 10 '18 at 22:39
• but to make sure I get it: $\lambda a$ defines $\lambda b$ before it could be called (since $\lambda a$ is first) so when b comes to be called, $\lambda a$ already defined $\lambda b$ – Delupara Oct 10 '18 at 22:44

One view is that there are no functions of multiple parameters. A function which takes "two parameters" is a function taking a single ordered pair. In mathematics, a function $$f : A \to B$$ has one domain $$A$$ and codomain $$B$$. While it is possible to speak of functions with multiple domains, it is more customary to think of a multi-variate function $$g$$ as an ordinary function whose domain is a cartesian product, $$g : A \times B \to C$$.

So, if you would like to have functions taking two parameters in $$\lambda$$-calculus, you should not be changing how $$\lambda$$-abstraction works, but you should rather extend the calculus with ordered pairs (and people do that).

But we do not have to extend the calculus with ordered pairs, because every function of two arguments $$A \times B \to C$$ can be converted to a function of a single argument $$A$$ returning a function $$B \to C$$. This may take some getting used to, but it works perfectly. That is, there is a bijection between functions $$A \times B \to C$$ and functions $$A \to (B \to C)$$, where the latter expression is read as "functions taking an argument from $$A$$ and returning a function from $$B$$ to $$C$$". This is known as currying.

The expression $$\lambda a . \lambda b . a + b$$ should be read as a function taking an argument $$a$$ and returning the function $$\lambda b . a + b$$. It is thus an example of a multi-variate function that has been curried to take one argument at a time.